76a5c700 by Jean-Alexandre Barszcz at 2020-07-28T22:51:59-04:00 [WIP] unify instead of conv_p in sform_lambda
This seems fine, but please share the code with `check_inferred` (extra points if you also share the code with `infer_type`).
Another thing: in `resolve_instances`, you resolve all instances in the "outer" context (e.g. at the point of generalization, or at top-level), whereas we should do it in the context specific to each metavar. For that `fv` needs to return not just the "context length" but the actual context and the easiest way to get that is probably to change `metavar_info` so it records the actual context. And for that you'll probably need to move definitions around so `lexp_context` can be defined between `lexp` and `metavar_info`. Maybe the better option is to move those type definitions to a separate file.
3bda7d77 by Jean-Alexandre Barszcz at 2020-07-28T22:51:59-04:00 Resolve instances in the REPL (since exprs. are not generalized)
For the non-REPL case we also need to handle the non-generalized definitions (e.g. those with a type annotation, or those that are recursive since we currently don't try to auto-generalize them).
44615264 by Jean-Alexandre Barszcz at 2020-07-28T22:51:59-04:00 [WIP] Do the set_getenv
IIRC these were missing to correctly handle the elab context for macro expansion and Elab_... primitives. Perhaps it would be simpler to call set_getenv once before macro expansion rather than everywhere where the context can change. Needs some experimentation and tests.
If you could add a comment explaining the difference (most importantly, why we need to have two entry points `lexp_parse_all` and `lexp_parse_sexp`), that would be helpful.
Stefan