(* 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