TC: strange import behavior in presence of annotations

[PaulKlint]

I encounter some hard to understand problems with analysis::m3::AST.

Suspicion: in the handling of annotations the wrong environment is used by the type checker.

Observation 1: analysis::m3::AST itself type checks and compiles ok.

Observation 2: importing analysis::m3::AST in another module is problematic:

Attempt A.

module experiments::Compiler::Examples::Tst
import lang::java::m3::AST;

gives

error("Annotation typ has already been declared with type failure({error(\"Type TypeSymbol not declared\",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2044,10,\<41,5\>,\<41,15\>))})",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2352,25,<55,0>,<55,25>))
error("Annotation typ has already been declared with type failure({error(\"Type TypeSymbol not declared\",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2044,10,\<41,5\>,\<41,15\>))})",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2274,31,<51,0>,<51,31>))
error("Type TypeSymbol not declared",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2044,10,<41,5>,<41,15>))
error("Type TypeSymbol not declared",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2279,10,<51,5>,<51,15>))
error("Type TypeSymbol not declared",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2357,10,<55,5>,<55,15>))
error("Type Message not declared",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2126,13,<43,5>,<43,18>))

Strange, since TypeSymbol is indeed imported in analysis::m3::AST , so let's import it ourselves:

Attempt B.

module experiments::Compiler::Examples::Tst
import lang::java::m3::AST;
import analysis::m3::TypeSymbol;

gives

error("Type Message not declared",|project://rascal/src/org/rascalmpl/library/analysis/m3/AST.rsc|(2126,13,<43,5>,<43,18>))

Attempt C.

Adding import Message; before or after import analysis::m3::AST

module experiments::Compiler::Examples::Tst
import lang::java::m3::AST;
import analysis::m3::TypeSymbol;
import Message;

gives the same message.

[mahills]

The quick summary of the problem is that analysis::m3::TypeSymbol isn't imported, but something that uses the TypeSymbol type from this module is, so, when I process the use of it, I get an error. This shouldn't be an error, but any uses of the function return value cannot be used as TypeSymbols in this context since the type isn't imported, so I have to be careful to not accidentally allow it into scope. I'll have to think about how to handle this -- in general, one would import both modules to make sure one could actually use the return type. I know we don't want to allow transitive imports, but allowing the import of functions with return types that have definitions that are not in scope is an anomoly in the system right now and is something we really need to think about.

[swatbot]

If we want to use a type like that pethaps we should use extend instead of import?—
Jurgen J. Vinju
CWI SWAT
INRIA Lille
UvA master software engineering
http://jurgen.vinju.org

On Wed, Mar 26, 2014 at 3:34 AM, mahills notifications@github.com wrote:

The quick summary of the problem is that analysis::m3::TypeSymbol isn't imported, but something that uses the TypeSymbol type from this module is, so, when I process the use of it, I get an error. This shouldn't be an error, but any uses of the function return value cannot be used as TypeSymbols in this context since the type isn't imported, so I have to be careful to not accidentally allow it into scope. I'll have to think about how to handle this -- in general, one would import both modules to make sure one could actually use the return type. I know we don't want to allow transitive imports, but allowing the import of functions with return types that have definitions that are not in scope is an anomoly in the system right now and is something we really need to think about.

Reply to this email directly or view it on GitHub:
#496 (comment)

[mahills]

An alternative would be to allow re-exporting types and other imported items, this would be more granular versus bringing in everything including private definitions.

Right now, from the perspective of the checker, the messages make perfect sense (even though they are wrong) -- the module has never imported a definition of either TypeSymbol or Message, so it doesn't know about them, hence the failures in trying to find the type definition that goes with each name.

[jurgenvinju]

In a way, we already have this re-export feature:

Using data X; you can define the existence of X without repeating its
constructors and without leaking its details.

In a way any function returning a data type implicitly defines its
existence.

A wild thought: could we, for every function: X f(...);

which uses a declared type X as return type, which is type correct and
properly declared in scope, we infer a public declaration in the current
module:

data X;

This way the type remains opaque for those who do not want to see it yet
may be passing it to other functions. If users do want to peep inside of X,
then they should import the definitions.

On Wed, Mar 26, 2014 at 12:42 PM, mahills notifications@github.com wrote:

An alternative would be to allow re-exporting types and other imported
items, this would be more granular versus bringing in everything including
private definitions.

Right now, from the perspective of the checker, the messages make perfect
sense (even though they are wrong) -- the module has never imported a
definition of either TypeSymbol or Message, so it doesn't know about
them, hence the failures in trying to find the type definition that goes
with each name.

Reply to this email directly or view it on GitHubhttps://github.com//issues/496#issuecomment-38673927
.

Jurgen Vinju

• Centrum Wiskunde & Informatica - SWAT

• INRIA Lille - ATEAMS

• Universiteit van Amsterdam

  www: http://jurgen.vinju.org, http://www.rascal-mpl.org,
  http://twitter.com/jurgenvinju
  skype: jurgen.vinju

[mahills]

That could be problematic. Even without any other problems, I would have a hard time checking it -- if someone entered TypeSmybol instead of TypeSymbol I wouldn't have a good way to know it is wrong. My working assumption at this point is that I'm checking the current module, but the imports into the module are type correct.

To do this, I could just add type names into the type environment if I see them and they haven't been declared yet, but that seems dangerous. This also reveals the other problem -- if X is an alias (e.g., alias X = int) or a nonterminal type, we are creating a conflict.

[swatbot]

Hi Mark,

I meant it differently. Only if the return type exists and it is correct an abstract declaration is added to the current module for export. Nothing can go wrong then in the importing module. You will get undefined errors only when you start inspecting the contents of rhe type using constructor names their, which makes sense. 
—
Jurgen J. Vinju
CWI SWAT
INRIA Lille
UvA master software engineering
http://jurgen.vinju.org

On Wed, Mar 26, 2014 at 9:15 PM, mahills notifications@github.com wrote:

That could be problematic. Even without any other problems, I would have a hard time checking it -- if someone entered TypeSmybol instead of TypeSymbol I wouldn't have a good way to know it is wrong. My working assumption at this point is that I'm checking the current module, but the imports into the module are type correct.

I guess I could just add type names into the type environment if I see them and they haven't been declared yet, but that seems dangerous. This also reveals the other problem -- if X is an alias (e.g., int) or a nonterminal type, we are creating a conflict.

Reply to this email directly or view it on GitHub:
#496 (comment)

[mahills]

From the perspective of the checker, the problem with this is that I don't know the type is correct -- I don't chase the entire import graph, I just go one level (unless I hit an extends, then I have to do more), so when I'm checking module A, which imports B, I get the signature for B but don't see things that B itself imports. I was marking these types when I found them, though, so maybe I forgot to do that with annotations, I'll have to check.

[swatbot]

Hmm.. maybe we should make this into a Skype session. Perhaps I don't
understand, or perhaps I did not explain well enough :-)

Suppose:

• we have modules A, B and C.
• A imports B,
• B imports C.
• C defines a datatype X
• B defines a function f that returns said data-type
• A calls said function and assigns the result to a variable of type X
• error: X is undefined in A because it is defined in C which was
  imported by B.

Observations:

• in B the return type of X is checked correctly. I.e. if Y was used
  instead you would have gotten an "undefined type Y" error in B. So we are
  sure that X exists in B.
• there is no definition of X literally in B, so it does not export it
  when A imports B.

So I propose to add to B, implicity:

• data X;
• but only after we know that X indeed exists.
• then when A is checked, it will import this opaque definition of X and
  the error "X is undefined" is not produced.

On Thu, Mar 27, 2014 at 12:52 PM, mahills notifications@github.com wrote:

From the perspective of the checker, the problem with this is that I don't
know the type is correct -- I don't chase the entire import graph, I just
go one level (unless I hit an extends, then I have to do more), so when I'm
checking module A, which imports B, I get the signature for B but don't see
things that B itself imports. I was marking these types when I found them,
though, so maybe I forgot to do that with annotations, I'll have to check.

Reply to this email directly or view it on GitHubhttps://github.com//issues/496#issuecomment-38793772
.

Jurgen Vinju

• Centrum Wiskunde & Informatica - SWAT

• INRIA Lille - ATEAMS

• Universiteit van Amsterdam

  www: http://jurgen.vinju.org, http://www.rascal-mpl.org,
  http://twitter.com/jurgenvinju
  skype: jurgen.vinju

[mahills]

Skype may be easier, but hopefully I can also just explain better :)

Given your scenario, assume I'm checking module A. To do so, I extract the public signature of B, which I need to properly check A. I don't check B when I do this, but assume it is correct. I don't even look at C, since A doesn't import it and B doesn't extend it. I could check B, and/or C, but then, in theory, checking an individual module would involve checking the entire Rascal library. This may be fine, especially if we can cache the information the checker generates so we don't really have to do this every time, but it makes the problem harder and potentially slower, so we don't do it right now. This may be something to talk about :)

Carrying on with the example, in this case, as part of this signature import I get the signature for f. If the return type is wrong, I don't have any way of knowing this. So, if I add X as a data type, this may be fine -- I'm just working under the assumption that X is available, since I assume B is correct. It may mask an error, though. It may also be the case that X is really an alias to a type like int, or is a nonterminal, in which case treating it as a data type may not be correct (maybe it doesn't matter -- if the programmer really cared, they would import C).

Also, assume we do actually check B. We still may not know that X is correct, since f could be defined as a Java function, and we don't check the implementation of that.

[swatbot]

Ok got it. 

Another solution is to make all defined types transitively visible, but that again needs typechecking to be incremental.
—
Jurgen J. Vinju
CWI SWAT
INRIA Lille
UvA master software engineering
http://jurgen.vinju.org

On Thu, Mar 27, 2014 at 3:37 PM, mahills notifications@github.com wrote:

Skype may be easier, but hopefully I can also just explain better :)
Given your scenario, assume I'm checking module A. To do so, I extract the public signature of B, which I need to properly check A. I don't check B when I do this, but assume it is correct. I don't even look at C, since A doesn't import it and B doesn't extend it. I could check B, and/or C, but then, in theory, checking an individual module would involve checking the entire Rascal library. This may be fine, especially if we can cache the information the checker generates so we don't really have to do this every time, but it makes the problem harder and potentially slower, so we don't do it right now. This may be something to talk about :)
Carrying on with the example, in this case, as part of this signature import I get the signature for f. If the return type is wrong, I don't have any way of knowing this. So, if I add X as a data type, this may be fine -- I'm just working under the assumption that X is available, since I assume B is correct. It may mask an error, though. It may also be the case that X is really an alias to a type like int, or is a nonterminal, in which case treating it as a data type may not be correct (maybe it doesn't matter -- if the programmer really cared, they would import C).

Also, assume we do actually check B. We still may not know that X is correct, since f could be defined as a Java function, and we don't check the implementation of that.

Reply to this email directly or view it on GitHub:
#496 (comment)

[PaulKlint]

This works now.