search

mortberg / cubicaltt

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

Check if some names were shadowed while loading a file #66

Closed mortberg closed 7 years ago

mortberg commented 7 years ago

This resolves https://github.com/mortberg/cubicaltt/issues/43

jonsterling commented 7 years ago

Hi @mortberg, thanks for the quick response! We tried this out, but it looks like it typechecks the module before reporting the error... I think this means that if there are type errors in the module, these will prevent the reporting of the shadowing. Since this is a common case (errors caused by shadowing), it would be nice if this check could be performed earlier, or perhaps interleaved with the checking of a module.

What do you think?

mortberg commented 7 years ago

Hmm, right. I was printing it earlier in the loop but this led to it disappearing out of my terminal when I loaded some big file so I moved it down. But actually I think it makes sense to print it as early as possible so that if typechecking fails one sees it.

mortberg commented 7 years ago

I moved it up before calling the typechecker now

mortberg commented 7 years ago

Note that I went for the fastest way to implement this, but maybe this is not the nicest way to do it. I think it would be better if the shadowing test would be done for each definitions as one checks it, however this is a bit more boring to implement as one has to traverse the environment (one could give a better error message if one does this as one would know the location of the definition that gets shadowed). I'm not sure how well my solution works for local definitions either... Anyway this is better than nothing and it leaves room for contributions. :)

jonsterling commented 7 years ago

Cool :) I think that this is certainly good enough to merge! Thanks, @mortberg

mortberg commented 7 years ago

Great, thanks for making me fix this issue!