search

sweirich / trellys

Automatically exported from code.google.com/p/trellys
45 stars 6 forks source link

Type checker admits type declarations into context before checking a corresponding term. #7

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?
1. `trellys -t SigDefBug.trellys` or `make todo` in trunk/test

What is the expected output? What do you see instead?

Should fail type checking, but passes.

Original issue reported on code.google.com by nathan.c...@gmail.com on 17 Dec 2010 at 5:51

GoogleCodeExporter commented 9 years ago 
My plan to fix this is:
1. add a separate "signatures" list to Environment.Env with corresponding 
update/read functions.
2. change type checker to initially put decls in the signatures list, and only 
move them to the context *after* a corresponding term is checked.

Yell at me if you think this is dumb :)

Original comment by nathan.c...@gmail.com on 17 Dec 2010 at 6:00

GoogleCodeExporter commented 9 years ago 
Fixed in r44.

Original comment by nathan.c...@gmail.com on 20 Dec 2010 at 11:58