F* performs a syntactic check to make sure an implementation file defines all vals in the signature. This mostly works fine for normal code, but if the val is spliced in from a syntax extension blob, then it is missed entirely. This means We can have
val foo : ...
in the interface, without any implementation to back it up. Or, more dangerously, have
let fooo = ...
in the implementation, mistakenly believing we are using it to implement foo, but the types could be completely unrelated.
This PR makes the typechecker env track names with a "missing" definition, and error out at the end of checking a module if any remain. (This is only ever called in batch mode.)
F* performs a syntactic check to make sure an implementation file defines all
vals in the signature. This mostly works fine for normal code, but if thevalis spliced in from a syntax extension blob, then it is missed entirely. This means We can havein the interface, without any implementation to back it up. Or, more dangerously, have
in the implementation, mistakenly believing we are using it to implement
foo, but the types could be completely unrelated.This PR makes the typechecker env track names with a "missing" definition, and error out at the end of checking a module if any remain. (This is only ever called in batch mode.)
Mostly in support of https://github.com/FStarLang/pulse/pull/121.
Given this, we could consider completely removing the syntactic check.