From 09387da80068cebc1470baa942d85a0fd3dc76f0 Mon Sep 17 00:00:00 2001
From: Jacques Garrigue <garrigue at math.nagoya-u.ac.jp>
Date: Mon, 28 Oct 2013 11:49:29 +0000
Subject: [PATCH] Fix PR#6174 (non -rectypes)

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14246 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
---
 Changes                                                   | 1 +
 testsuite/tests/typing-gadts/pr6174.ml                    | 3 +++
 .../tests/typing-gadts/pr6174.ml.principal.reference      | 8 ++++++++
 testsuite/tests/typing-gadts/pr6174.ml.reference          | 8 ++++++++
 typing/ctype.ml                                           | 3 ++-
 5 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 testsuite/tests/typing-gadts/pr6174.ml
 create mode 100644 testsuite/tests/typing-gadts/pr6174.ml.principal.reference
 create mode 100644 testsuite/tests/typing-gadts/pr6174.ml.reference

diff --git a/Changes b/Changes
index b7445c556..baad6dee5 100644
--- a/Changes
+++ b/Changes
@@ -47,6 +47,7 @@ OCaml 4.01.1:
 
 Bug fixes:
 - PR#6173: Typing error message is worse that before
+- PR#6174: OCaml compiler loops on an example using GADTs (non -rectypes)
 
 OCaml 4.01.0:
 -------------
diff --git a/testsuite/tests/typing-gadts/pr6174.ml b/testsuite/tests/typing-gadts/pr6174.ml
new file mode 100644
index 000000000..84f79ba0e
--- /dev/null
+++ b/testsuite/tests/typing-gadts/pr6174.ml
@@ -0,0 +1,3 @@
+type _ t = C : ((('a -> 'o) -> 'o) -> ('b -> 'o) -> 'o) t
+let f : type a o. ((a -> o) -> o) t -> (a -> o) -> o =
+ fun C k -> k (fun x -> x);;
diff --git a/testsuite/tests/typing-gadts/pr6174.ml.principal.reference b/testsuite/tests/typing-gadts/pr6174.ml.principal.reference
new file mode 100644
index 000000000..647015c36
--- /dev/null
+++ b/testsuite/tests/typing-gadts/pr6174.ml.principal.reference
@@ -0,0 +1,8 @@
+
+#     Characters 118-119:
+   fun C k -> k (fun x -> x);;
+       ^
+Error: Recursive local constraint when unifying
+         (((ex#0 -> ex#1) -> ex#1) -> (ex#2 -> ex#1) -> ex#1) t
+       with ((a -> o) -> o) t
+# 
diff --git a/testsuite/tests/typing-gadts/pr6174.ml.reference b/testsuite/tests/typing-gadts/pr6174.ml.reference
new file mode 100644
index 000000000..647015c36
--- /dev/null
+++ b/testsuite/tests/typing-gadts/pr6174.ml.reference
@@ -0,0 +1,8 @@
+
+#     Characters 118-119:
+   fun C k -> k (fun x -> x);;
+       ^
+Error: Recursive local constraint when unifying
+         (((ex#0 -> ex#1) -> ex#1) -> (ex#2 -> ex#1) -> ex#1) t
+       with ((a -> o) -> o) t
+# 
diff --git a/typing/ctype.ml b/typing/ctype.ml
index aa67a9181..1bf4872ef 100644
--- a/typing/ctype.ml
+++ b/typing/ctype.ml
@@ -1660,7 +1660,8 @@ let rec local_non_recursive_abbrev visited env p ty =
         iter_type_expr (local_non_recursive_abbrev visited env p) ty
   end
 
-let local_non_recursive_abbrev = local_non_recursive_abbrev (ref [])
+let local_non_recursive_abbrev env p =
+  local_non_recursive_abbrev (ref []) env p
 
                    (*****************************)
                    (*  Polymorphic Unification  *)