Stefan pushed to branch master at Stefan / Typer

Commits: 85d12bf5 by Stefan Monnier at 2020-04-07T22:21:39-04:00 * src/elab.ml (infer_and_generalize_type): Add more exceptions

Don't generalize over the level of the final return type if it doesn't appear elsewhere.

* btl/builtins.typer (Eq_cast): Give a name to the proof arg.

- - - - -

2 changed files:

- btl/builtins.typer - src/elab.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -48,7 +48,7 @@ Eq_refl : ((x : ?t) ≡> Eq x x); % FIXME: `Eq ?x ?x` causes an error! Eq_refl = Built-in "Eq.refl";

Eq_cast : (x : ?) ≡> (y : ?) - ≡> Eq x y + ≡> (p : Eq x y) ≡> (f : ? -> ?) ≡> f x -> f y; %% FIXME: I'd like to just say:

===================================== src/elab.ml ===================================== @@ -374,6 +374,9 @@ let rec meta_to_var ids o (e : lexp) = mkVar (name, o + IMap.find id ids) else match metavar_lookup id with | MVal e -> loop (push_susp e s) + (* FIXME: The substitution applied before calling `meta_to_var` + * make it impossible for the metavar to refer to the newly + * introduced variables. *) | _ -> e in loop e

@@ -1034,10 +1037,10 @@ and lexp_check_decls (ectx : elab_context) (* External context. *) and infer_and_generalize_type (ctx : elab_context) se name = let nctx = ectx_new_scope ctx in let t = infer_type se nctx name in - (* FIXME: We should not generalize over metavars which only occur on the rightmost + (* We should not generalize over metavars which only occur on the rightmost * side of arrows in type annotations (aka declarations), since there's no * way for the callee to return something of the proper type if those - * metavar's don't also occur somewhere in the arguments. + * metavars don't also occur somewhere in the arguments. * E.g. for annotations like * * x : ?; @@ -1050,16 +1053,21 @@ and infer_and_generalize_type (ctx : elab_context) se name = * * since there can't be corresponding definitions. So replace the final * return type with some arbitrary closed constant before computing the - * set of free metavars. *) - match OL.lexp_whnf t (ectx_to_lctx ctx) with - (* There's no point generalizing a single metavar, and it's useful - * to keep it ungeneralized so we can use `x : ?` to declare that - * `x` will be defined later without specifying its type yet. *) - | Metavar _ -> t - | _ -> let g = generalize nctx t in - g (fun _ne name t l e - -> mkArrow (Aerasable, name, t, l, e)) - t + * set of free metavars. + * The same argument holds for other *positive* positions, e.g. + * + * f : (? -> Int) -> Int; + * + * But we don't bother trying to catch all cases currently. + *) + let rec strip_rettype t = match t with + | Arrow (ak, v, t1, l, t2) -> Arrow (ak, v, t1, l, strip_rettype t2) + | Sort _ | Metavar _ -> type0 (* Abritrary closed constant. *) + | _ -> t in + let g = generalize nctx (strip_rettype t) in + g (fun _ne name t l e + -> mkArrow (Aerasable, name, t, l, e)) + t

and infer_and_generalize_def (ctx : elab_context) se = let nctx = ectx_new_scope ctx in

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/85d12bf59e470f20c8d866a33029c9f3c1...