Eliminate_epsilon: discriminate monomorphic identities (fix #127)

src/transform/detect_polymorphism.ml

@@ -79,7 +79,10 @@ let detect_polymorphism_in_decl ign_ts ign_ls ign_pr d =
         monomorphic, since it is checked by typing *)
      List.fold_left (fun acc (ls,_) -> acc || check_ls ign_ls ls) false indl
   | Dprop (_,pr,t) ->
-     (* todo: NE PAS TESTER le goal *)
+     (* todo: DO NOT TEST the goal. This requires skolemizing
+        type variables in the goal _before_ eliminate_epsilon
+        in the transformation chain, to avoid producing
+        polymorphic identities in monomorphic tasks *)
      not (Spr.mem pr ign_pr) &&
        let s = Term.t_ty_freevars Ty.Stv.empty t in
        not (Ty.Stv.is_empty s)

src/transform/eliminate_epsilon.ml

@@ -15,7 +15,7 @@ open Decl
 
 (* Canonical forms for epsilon terms. *)
 type canonical =
-  | Id                             (* identity lambda    (\x (x_i). x (x_i)) *)
+  | Id of Ty.ty                    (* identity lambda    (\x (x_i). x (x_i)) *)
   | Eta of term                    (* eta-expansed term  (\(x_i). t (x_i))
                                       (x_i not in t's free variables)        *)
   | Partial of lsymbol * term list (* partial application
@@ -48,7 +48,7 @@ let canonicalize x f =
         if Mvs.set_disjoint (t_freevars Mvs.empty e) (Svs.of_list rvl)
         then Eta e
         else raise Exit
-    | Tvar u, [v] when vs_equal u v -> Id
+    | Tvar u, [v] when vs_equal u v -> Id v.vs_ty
     | Tapp (ls, [fn; {t_node = Tvar u}]), v :: vl
       when ls_equal ls fs_func_app ->
         if vs_equal u v then match_apps fn vl else raise Exit
@@ -84,8 +84,7 @@ let get_canonical ls =
   let ax = create_prop_decl Paxiom pr (t_forall_close vl [] f) in
   create_param_decl cs, ax, cs
 
-let id_canonical =
-  let ty = Ty.ty_var (Ty.tv_of_string "a") in
+let id_canonical ty =
   let tyf = Ty.ty_func ty ty in
   let cs = create_fsymbol (id_fresh "identity") [] tyf in
   let vs = create_vsymbol (id_fresh "y") ty in
@@ -101,6 +100,15 @@ let get_canonical =
   let res = get_canonical ls in
   Hls.add ht ls res; res
 
+let id_canonical =
+  let ht = Ty.Hty.create 3 in fun ty ->
+  try Ty.Hty.find ht ty with Not_found ->
+  let res = id_canonical ty in
+  Ty.Hty.add ht ty res; res
+
+let poly_id_canonical =
+  id_canonical (Ty.ty_var (Ty.tv_of_string "a"))
+
 type to_elim =
   | All           (* eliminate all epsilon-terms *)
   | NonLambda     (* preserve lambda-terms *)
@@ -143,8 +151,9 @@ let rec lift_f el acc t0 =
       let vl = Mvs.keys (t_vars t0) in
       let vs, f = t_open_bound fb in
       let acc, t = match canonicalize vs f with
-        | Id ->
-            let ld, ax, cs = id_canonical in
+        | Id ty ->
+            let ld, ax, cs = if Ty.ty_closed ty then
+              id_canonical ty else poly_id_canonical in
             let abst, axml = acc in
             (ld :: abst, ax :: axml), fs_app cs [] vs.vs_ty
         | Eta t -> lift_f el acc t