Fix to drop unused metavariables

Sometimes type inference uses metavariables that end up not being used at all
and that causes generalization to insert unnecessary implicit functions.  This
changes `lift*` to drop unused metavariables.

Author: polytypic

elab.ml

@@ -177,6 +177,7 @@ let elab_eff env eff =
 
 let rec elab_typ env typ l =
   Trace.elab (lazy ("[elab_typ] " ^ EL.label_of_typ typ));
+  let lift_warn = lift_warn (level ()) in
   (fun (s, zs) -> typ.at, env, s, zs, None, EL.label_of_typ typ) <<<
   match typ.it with
   | EL.PathT(exp) ->
@@ -314,6 +315,7 @@ and elab_dec env dec l =
 
 and elab_pathexp env exp l =
   Trace.elab (lazy ("[elab_pathexp] " ^ EL.label_of_exp exp));
+  let lift_warn = lift_warn (level ()) in
   let ExT(aks, t), p, zs, _ = elab_instexp env exp l in
 Trace.debug (lazy ("[ExpP] s = " ^ string_of_norm_extyp (ExT(aks, t))));
   if p = Impure then
@@ -362,6 +364,8 @@ and elab_const = function
 
 and elab_exp env exp l =
   Trace.elab (lazy ("[elab_exp] " ^ EL.label_of_exp exp));
+  let lift = lift (level ()) in
+  let lift_warn = lift_warn (level ()) in
   (fun (s, p, zs, e) -> exp.at, env, s, zs, Some e, EL.label_of_exp exp) <<<
   match exp.it with
   | EL.VarE(var) ->
@@ -395,7 +399,7 @@ Trace.debug (lazy ("[FunE] env =" ^ VarSet.fold (fun a s -> s ^ " " ^ a) (domain
       | Pure, f -> f
       | _ -> error impl.at "impure function cannot be implicit" in
     ExT([], FunT(aks, t, s, p')), Pure,
-    lift (* TODO: _warn exp.at (FunT(aks, t, s, p')) *) env (zs1 @ zs2),
+    lift (* TODO: _warn exp.at *) (FunT(aks, t, s, p')) env (zs1 @ zs2),
     IL.genE(erase_bind aks, IL.LamE(var.it, erase_typ t, e2))
 
   | EL.WrapE(var, typ) ->
@@ -606,6 +610,7 @@ t = !b:*. [= b] -> {t : [= t4.t b], u : !a:*. [= a] => [= (a, t4.u b a)]}
 
 and elab_bind env bind l =
   Trace.elab (lazy ("[elab_bind] " ^ EL.label_of_bind bind));
+  let lift_warn = lift_warn (level ()) in
   (fun (s, p, zs, e) -> bind.at, env, s, zs, Some e, EL.label_of_bind bind) <<<
   match bind.it with
   | EL.VarB(var, exp) ->
@@ -680,7 +685,7 @@ Trace.debug (lazy ("[GenE] a1 = " ^ string_of_typ (VarT(a1, BaseK))));
       match !z with
       | Undet u -> u.level >= level
       | Det _ -> assert false
-    ) (lift (add_typs aks env) zs) in
+    ) (lift level t (add_typs aks env) zs) in
   if p = Impure || zs1 = [] then
     s, p, zs1 @ zs2, e
   else begin

sub.ml

@@ -112,19 +112,21 @@ let rec materialize_typ = function
 
 (* Lifting *)
 
-let lift env zs =
+let lift bottom t env zs =
   let dom = domain_typ env in
   List.filter (fun z ->
     match !z with
     | Det _ -> false
-    | Undet u -> u.vars <- VarSet.inter u.vars dom; true
+    | Undet u ->
+      u.vars <- VarSet.inter u.vars dom;
+      u.level <= bottom || occurs_typ u t
   ) zs
 
 
 module IdSet = Set.Make(struct type t = int let compare = compare end)
 let warned_already = ref IdSet.empty
 
-let lift_warn at t env zs =
+let lift_warn bottom at t env zs =
   let dom = domain_typ env in
   List.filter (fun z ->
     match !z with
@@ -142,7 +144,7 @@ let lift_warn at t env zs =
         );
         warned_already := IdSet.add u.id !warned_already
       );
-      true
+      u.level <= bottom || occurs_typ u t
   ) zs
 
 
@@ -172,6 +174,7 @@ let rec psubst p t =
   | _ -> assert false
 
 let rec sub_typ infer_binds env t1 t2 ps =
+  let lift = lift (level ()) t1 in
   Trace.sub (lazy ("[sub_typ] t1 = " ^ string_of_norm_typ t1));
   Trace.sub (lazy ("[sub_typ] t2 = " ^ string_of_norm_typ t2));
   Trace.sub (lazy ("[sub_typ] ps = " ^
@@ -348,6 +351,7 @@ and sub_extyp infer_binds env s1 s2 ps =
   | [], [] ->
     sub_typ infer_binds env t1 t2 ps
   | _ ->
+    let lift = lift (level ()) t1 in
     let ts, zs, f =
       sub_typ infer_binds (add_typs aks1 env) t1 t2 (varTs aks2) in
     [], lift env zs,

sub.mli

@@ -9,9 +9,10 @@ val materialize_typ : Types.typ -> Fomega.exp
 
 (* Lifting *)
 
-val lift : Env.env -> Types.infer ref list -> Types.infer ref list
+val lift :
+  int -> Types.typ -> Env.env -> Types.infer ref list -> Types.infer ref list
 val lift_warn :
-  Source.region -> Types.typ -> Env.env -> Types.infer ref list ->
+  int -> Source.region -> Types.typ -> Env.env -> Types.infer ref list ->
     Types.infer ref list