Commit 42dda81a authored by Kim Nguyễn's avatar Kim Nguyễn

Fix a bug in toplevel definition of types:

when a type such as

type t('a) = (Int,'a)

is introduced, the variables occuring in the definitions are replaced by fresh occurences.
The variables in the left-hand-side were note renamed accordingly, yielding a type definition:

type t('a_0) = (Int, 'a_1)

when performing type substitutions, none of the occurences of 'a_1 were replaced.
parent 01e9ada9
......@@ -459,23 +459,34 @@ module IType = struct
in
let b =
List.map2 (fun ((loc,v),pl,p) (v',_,d) ->
let t = Types.Positive.substitutefree Var.Set.empty (aux loc d) in
let vars = Var.Set.fold (fun acc v -> (Var.id v,v)::acc) [] (Types.all_vars t) in
if (loc <> noloc) && (Types.is_empty t) then
let t_rhs = aux loc d in
if (loc <> noloc) && (Types.is_empty t_rhs) then
warning loc
("This definition yields an empty type for " ^ (U.to_string v));
if (List.length vars) <> (List.length pl) then
let vars_rhs = Types.all_vars t_rhs in
let vars_mapping = (* create a sequence 'a -> 'a_0 for all variables *)
List.map (fun v -> let vv = Var.mk (Ident.U.to_string v) in vv, Var.fresh vv) pl
in
let vars_lhs =
List.fold_left (fun acc (v, _) -> Var.Set.add v acc) Var.Set.empty vars_mapping
in
if not (Var.Set.subset vars_rhs vars_lhs) then
error loc
(Printf.sprintf "Definition of type %s contains unused/undeclared type variables"
(U.to_string v)
);
(Printf.sprintf "Definition of type %s contains unbound type variables"
(U.to_string v));
let t_rhs =
Types.Positive.substitute_list t_rhs
(List.map (fun (v,vt) -> v, Types.var vt) vars_mapping)
in
let al =
let a = Array.make (List.length pl) (Var.mk "dummy") in
(* List.iteri (fun i v -> a.(i) <- (List.assoc (U.to_string v) vars)) pl; *)
List.iteri (fun i v -> a.(i) <- Var.mk (Ident.U.to_string v)) pl;
List.iteri (fun i (_,v) -> a.(i) <- v) vars_mapping;
a
in
(v',t,al)
(v',t_rhs,al)
) (List.rev b) (List.rev b')
in
List.iter (fun (v,t,al) ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment