summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJacques Garrigue <garrigue at math.nagoya-u.ac.jp>2003-11-07 01:06:55 +0000
committerJacques Garrigue <garrigue at math.nagoya-u.ac.jp>2003-11-07 01:06:55 +0000
commitb719914d644dc26e29fb4dcd8176789baee82dfd (patch)
tree0788fdd9d078e78967d327dab32bb46b281cfea4
parent010106506ce2be5da039fc7377fec42255c52cac (diff)
downloadocaml-b719914d644dc26e29fb4dcd8176789baee82dfd.tar.gz
fix PR#1917
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@5896 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
-rw-r--r--typing/ctype.ml38
1 files changed, 11 insertions, 27 deletions
diff --git a/typing/ctype.ml b/typing/ctype.ml
index 3323f8e7b8..db972546f3 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -1004,26 +1004,6 @@ let apply env params body args =
(* Abbreviation expansion *)
(****************************)
-
-(* Search whether the expansion has been memorized. *)
-let rec find_expans p1 =
- function
- Mnil ->
- None
- | Mcons (p2, ty0, ty, _) when Path.same p1 p2 ->
- (* assert
- begin match (repr ty).desc with
- Tconstr (p3, _, _) when Path.same p2 p3-> false
- | _ -> true
- end;
- assert (repr ty0 != repr ty); *)
- Some ty
- | Mcons (_, _, _, rem) ->
- find_expans p1 rem
- | Mlink {contents = rem} ->
- find_expans p1 rem
-
-
(*
If the environnement has changed, memorized expansions might not
be correct anymore, and so we flush the cache. This is safe but
@@ -1404,14 +1384,18 @@ let rec unify env t1 t2 =
and unify2 env t1 t2 =
(* Second step: expansion of abbreviations *)
- let t1' = expand_head env t1 in
- let t2' = expand_head env t2 in
- (* Expansion may have changed the representative of the types... *)
- let t1' = expand_head env t1' in
- let t2' = expand_head env t2' in
- if t1' == t2' then () else
-
+ let rec expand_both t1 t2 =
+ let t1' = expand_head env t1 in
+ let t2' = expand_head env t2 in
+ (* Expansion may have changed the representative of the types... *)
+ if t1' == t1 && t2' == t2 then (t1,t2) else
+ expand_both t1' t2'
+ in
+ let t1', t2' = expand_both t1 t2 in
let t1 = repr t1 and t2 = repr t2 in
+ (* Expansion may have changed the original types too... *)
+ if t1 == t2 || t1' == t2' then () else
+
if (t1 == t1') || (t2 != t2') then
unify3 env t1 t1' t2 t2'
else