search

mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

Spurious error with incorrect import #64

Closed jonsterling closed 7 years ago

jonsterling commented 7 years ago

We've noticed that if you import a nonexistent module (import not-real), you will receive a strange error that some identifier cannot be resolved, but this identifier doesn't have anything to do with the module that we failed to import.

We are guessing that the failed import is somehow messing up another import, which causes the identifier resolution error. (It seems to mess up just that imports that come before.)

I think it would be nice if when you import a nonexistent module, you got an error that said something like module 'not-real' cannot be found.

mortberg commented 7 years ago

Note that identifiers can't contain -, but if I do import not_real I indeed get the behavior you describe. I think the reason is that it ignores everything it has parsed so far and then continue from after the bad import. Because of this it has forgotten basic things defined earlier (so for example Path might not be known if it has forgotten about the prelude). Note that the REPL prints a message if this happens:

Parsed "./prelude.ctt" successfully!
...
Parsed "./bool.ctt" successfully!
./not_real.ctt does not exist
Parsed "nat.ctt" successfully!

It should be easy to change this to an error instead.

mortberg commented 7 years ago

I think I have a patch for this now: https://github.com/mortberg/cubicaltt/pull/65/files

@jonsterling Can you test it and let me know if it works properly?