diff options
| -rw-r--r-- | testsuite/tests/typing-gadts/test.ml | 19 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/test.ml.principal.reference | 2 | ||||
| -rw-r--r-- | testsuite/tests/typing-gadts/test.ml.reference | 2 | ||||
| -rw-r--r-- | typing/ctype.ml | 26 |
4 files changed, 42 insertions, 7 deletions
diff --git a/testsuite/tests/typing-gadts/test.ml b/testsuite/tests/typing-gadts/test.ml index dc219f421..a8215290a 100644 --- a/testsuite/tests/typing-gadts/test.ml +++ b/testsuite/tests/typing-gadts/test.ml @@ -518,3 +518,22 @@ let g : type a. a ty -> a = module M = struct type _ t = int end;; module M = struct type _ t = T : int t end;; module N = M;; + +(* Principality *) + +(* adding a useless equation should not break inference *) +let f : type a b. (a,b) eq -> (a,int) eq -> a -> b -> _ = fun ab aint a b -> + let Eq = ab in + let x = + let Eq = aint in + if true then a else b + in ignore x +;; (* ok *) + +let f : type a b. (a,b) eq -> (b,int) eq -> a -> b -> _ = fun ab bint a b -> + let Eq = ab in + let x = + let Eq = bint in + if true then a else b + in ignore x +;; (* ok *) diff --git a/testsuite/tests/typing-gadts/test.ml.principal.reference b/testsuite/tests/typing-gadts/test.ml.principal.reference index 21f8526d2..551f9cb2d 100644 --- a/testsuite/tests/typing-gadts/test.ml.principal.reference +++ b/testsuite/tests/typing-gadts/test.ml.principal.reference @@ -312,4 +312,6 @@ Error: This expression has type < bar : int; foo : int; .. > as 'a # module M : sig type _ t = int end # module M : sig type _ t = T : int t end # module N : sig type 'a t = 'a M.t = T : int t end +# val f : ('a, 'b) eq -> ('a, int) eq -> 'a -> 'b -> unit = <fun> +# val f : ('a, 'b) eq -> ('b, int) eq -> 'a -> 'b -> unit = <fun> # diff --git a/testsuite/tests/typing-gadts/test.ml.reference b/testsuite/tests/typing-gadts/test.ml.reference index 3b84f9240..fc62f5d57 100644 --- a/testsuite/tests/typing-gadts/test.ml.reference +++ b/testsuite/tests/typing-gadts/test.ml.reference @@ -298,4 +298,6 @@ Error: This expression has type < bar : int; foo : int; .. > as 'a # module M : sig type _ t = int end # module M : sig type _ t = T : int t end # module N : sig type 'a t = 'a M.t = T : int t end +# val f : ('a, 'b) eq -> ('a, int) eq -> 'a -> 'b -> unit = <fun> +# val f : ('a, 'b) eq -> ('b, int) eq -> 'a -> 'b -> unit = <fun> # diff --git a/typing/ctype.ml b/typing/ctype.ml index aadba8809..60b2a8122 100644 --- a/typing/ctype.ml +++ b/typing/ctype.ml @@ -1899,12 +1899,12 @@ let reify env t = in iterator t -let is_abstract_newtype env p = +let is_newtype env p = try let decl = Env.find_type p env in - not (decl.type_newtype_level = None) && - decl.type_manifest = None && - decl.type_kind = Type_abstract + decl.type_newtype_level <> None && + decl.type_kind = Type_abstract && + decl.type_private = Public with Not_found -> false let non_aliasable p decl = @@ -2176,6 +2176,18 @@ let rec unify (env:Env.t ref) t1 t2 = || has_cached_expansion p2 !a2) -> update_level !env t1.level t2; link_type t1 t2 + | (Tconstr (p1, [], _), Tconstr (p2, [], _)) + when Env.has_local_constraints !env + && is_newtype !env p1 && is_newtype !env p2 -> + (* Do not use local constraints more than necessary *) + begin try + if find_newtype_level !env p1 < find_newtype_level !env p2 then + unify env t1 (try_expand_once !env t2) + else + unify env (try_expand_once !env t1) t2 + with Cannot_expand -> + unify2 env t1 t2 + end | _ -> unify2 env t1 t2 end; @@ -2288,7 +2300,7 @@ and unify3 env t1 t1' t2 t2' = inj (List.combine tl1 tl2) | (Tconstr ((Path.Pident p) as path,[],_), Tconstr ((Path.Pident p') as path',[],_)) - when is_abstract_newtype !env path && is_abstract_newtype !env path' + when is_newtype !env path && is_newtype !env path' && !generate_equations -> let source,destination = if find_newtype_level !env path > find_newtype_level !env path' @@ -2296,12 +2308,12 @@ and unify3 env t1 t1' t2 t2' = else p',t1' in add_gadt_equation env source destination | (Tconstr ((Path.Pident p) as path,[],_), _) - when is_abstract_newtype !env path && !generate_equations -> + when is_newtype !env path && !generate_equations -> reify env t2'; local_non_recursive_abbrev !env (Path.Pident p) t2'; add_gadt_equation env p t2' | (_, Tconstr ((Path.Pident p) as path,[],_)) - when is_abstract_newtype !env path && !generate_equations -> + when is_newtype !env path && !generate_equations -> reify env t1' ; local_non_recursive_abbrev !env (Path.Pident p) t1'; add_gadt_equation env p t1' |