(* This case cannot be inferred *)
- | Plambda (kind, var, aty, body)
- | Plambda (kind, var, obtype, body) -> (* Read var type from the provided type *)
let ltp, lbtp = match OL.lexp_whnf t (ectx_to_lctx ctx) with
let latp, lbtp = match OL.lexp_whnf t (ectx_to_lctx ctx) with | Arrow(kind, _, ltp, _, lbtp) -> ltp, lbtp | expr -> lexp_fatal tloc expr "Expected Type Arrow ( _ -> _ )" in
let _ = match aty with
| Some paty
-> let laty, lasort = _lexp_p_infer paty ctx trace in
elab_check_sort ctx lasort (Some var) laty;
let _ = match obtype with
| Some btype
-> let body_type, lasort = _lexp_p_infer btype ctx trace in
elab_check_sort ctx lasort (Some var) body_type; () (* FIXME: Check `conv_p aty ltp`! *) | _ -> () in
let nctx = env_extend ctx var Variable ltp in
let nctx = env_extend ctx var Variable latp in let lbody = lexp_check body lbtp nctx in
mkLambda(kind, var, ltp, lbody)
mkLambda(kind, var, latp, lbody)
AFAICT this does nothing more than rename a few local vars, right? I think we have a pretty messy code w.r.t to naming, so I'd be generally happy to see some such renaming to clarify the code.
But here I'm confused: you used the name `body_type` for a variable which holds the type of the *argument* rather than the type of the body.
What am I missing?
match nosusp ltp with
Please use lexp_lwhnf instead of nosusp. We used to not have whnf, which is why we used nosusp everywhere, but nowadays whnf works well and is hence a much better choice (except at those few places where we need to be careful to keep the non-normalized form, obviously).
Stefan