Prevent eager unification with type families.

See Note [Prevent unification with type families]
in TcUnify for the details.

14 files changed, 70 insertions, 44 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index a1f757a28b..bee76d284c 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -275,4 +275,3 @@ test('T11361', normal, compile, ['-dunique-increment=-1'])
   # -dunique-increment=-1 doesn't work inside the file
 test('T11361a', normal, compile_fail, [''])
 test('T11581', normal, compile, [''])
-test('T7788', normal, compile, [''])
diff --git a/testsuite/tests/indexed-types/should_fail/T2693.stderr b/testsuite/tests/indexed-types/should_fail/T2693.stderr
index 5e925c3148..0c00711586 100644
--- a/testsuite/tests/indexed-types/should_fail/T2693.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -31,13 +31,14 @@ T2693.hs:19:23: error:
       In the expression: fst x + snd x
     • Relevant bindings include n :: a5 (bound at T2693.hs:19:7)
 
-T2693.hs:30:47: error:
+T2693.hs:29:20: error:
     • Couldn't match type ‘TFn a0’ with ‘PVR a1’
-      Expected type: [PVR a1]
-        Actual type: [TFn a0]
+      Expected type: () -> Maybe (PVR a1)
+        Actual type: () -> Maybe (TFn a0)
       The type variables ‘a0’, ‘a1’ are ambiguous
-    • In the second argument of ‘map’, namely ‘pvs’
-      In the second argument of ‘min’, namely ‘(map pvrX pvs)’
-      In the expression: (map pvrX pvs) `min` (map pvrX pvs)
-    • Relevant bindings include
-        pvs :: [TFn a0] (bound at T2693.hs:29:8)
+    • In the first argument of ‘mapM’, namely ‘g’
+      In a stmt of a 'do' block: pvs <- mapM g undefined
+      In the expression:
+        do { pvs <- mapM g undefined;
+             let n = (map pvrX pvs) `min` (map pvrX pvs);
+             undefined }
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index f3411a05cd..516bdf3802 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -2,10 +2,8 @@
 T4179.hs:26:16: error:
     • Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
                      with ‘A2 (FCon x)’
-      Expected type: x (A2 (x (A2 (FCon x) -> A3 (FCon x)))
-                        -> A3 (x (A2 (FCon x) -> A3 (FCon x))))
-                     -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
-                     -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
+      Expected type: x (A2 (FCon x) -> A3 (FCon x))
+                     -> A2 (FCon x) -> A3 (FCon x)
         Actual type: x (A2 (FCon x) -> A3 (FCon x))
                      -> A2 (x (A2 (FCon x) -> A3 (FCon x)))
                      -> A3 (x (A2 (FCon x) -> A3 (FCon x)))
diff --git a/testsuite/tests/indexed-types/should_fail/T5439.stderr b/testsuite/tests/indexed-types/should_fail/T5439.stderr
index b76b0f9362..f1ae705f5e 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -1,15 +1,13 @@
 
-T5439.hs:82:33: error:
-    • Couldn't match expected type ‘Attempt
-                                      (WaitOpResult (WaitOps rs))’
-                  with actual type ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
-    • In the second argument of ‘($)’, namely
-        ‘inj $ Failure (e :: SomeException)’
+T5439.hs:82:28: error:
+    • Couldn't match type ‘Attempt (WaitOpResult (WaitOps rs))’
+                     with ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
+      Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
+        Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
+    • In the first argument of ‘complete’, namely ‘ev’
+      In the expression: complete ev
       In a stmt of a 'do' block:
         c <- complete ev $ inj $ Failure (e :: SomeException)
-      In the expression:
-        do { c <- complete ev $ inj $ Failure (e :: SomeException);
-             return $ c || not first }
     • Relevant bindings include
         register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
           (bound at T5439.hs:64:9)
diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr
index 1f111fdd2c..b56db1398f 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr
@@ -1,10 +1,11 @@
 
 T7354.hs:28:11: error:
     • Occurs check: cannot construct the infinite type:
-        a ~ Prim [Base t a] (Base t a)
-      Expected type: a -> Base t a
-        Actual type: Prim [Base t a] (Base t a) -> Base t a
+        t1 ~ Base t (Prim [t1] t1)
+      Expected type: Prim [t1] t1 -> Base t (Prim [t1] t1)
+        Actual type: Prim [t1] t1 -> t1
     • In the first argument of ‘ana’, namely ‘alg’
       In the expression: ana alg
       In an equation for ‘foo’: foo = ana alg
-    • Relevant bindings include foo :: a -> t (bound at T7354.hs:28:1)
+    • Relevant bindings include
+        foo :: Prim [t1] t1 -> t (bound at T7354.hs:28:1)
diff --git a/testsuite/tests/indexed-types/should_fail/T7729.stderr b/testsuite/tests/indexed-types/should_fail/T7729.stderr
index 80b6fd82d9..b209c9c4b7 100644
--- a/testsuite/tests/indexed-types/should_fail/T7729.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7729.stderr
@@ -1,10 +1,10 @@
 
-T7729.hs:36:25: error:
+T7729.hs:36:14: error:
     • Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
-      Expected type: BasePrimMonad m a -> BasePrimMonad (Rand m) a
-        Actual type: BasePrimMonad m a -> t0 (BasePrimMonad m) a
+      Expected type: t0 (BasePrimMonad m) a -> Rand m a
+        Actual type: BasePrimMonad (Rand m) a -> Rand m a
       The type variable ‘t0’ is ambiguous
-    • In the second argument of ‘(.)’, namely ‘lift’
+    • In the first argument of ‘(.)’, namely ‘liftPrim’
       In the expression: liftPrim . lift
       In an equation for ‘liftPrim’: liftPrim = liftPrim . lift
     • Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/T7786.stderr b/testsuite/tests/indexed-types/should_fail/T7786.stderr
index 6cf8f8c770..a58b69e7e7 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7786.stderr
@@ -11,18 +11,20 @@ T7786.hs:86:22: error:
         Nil :: Sing xxx <- return
                              (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
 
-T7786.hs:86:22: error:
+T7786.hs:86:49: error:
     • Couldn't match type ‘xxx’
                      with ‘Intersect (BuriedUnder sub k 'Empty) inv’
       Expected type: Sing xxx
         Actual type: Sing (Intersect (BuriedUnder sub k 'Empty) inv)
-    • When checking that the pattern signature: Sing xxx
-        fits the type of its context:
-          Sing (Intersect (BuriedUnder sub k 'Empty) inv)
-      In the pattern: Nil :: Sing xxx
+    • In the first argument of ‘return’, namely
+        ‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’
       In a stmt of a 'do' block:
         Nil :: Sing xxx <- return
                              (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
+      In the expression:
+        do { Nil :: Sing xxx <- return
+                                  (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db);
+             return $ Sub db k sub }
     • Relevant bindings include
         sub :: Database sub (bound at T7786.hs:86:13)
         k :: Sing k (bound at T7786.hs:86:11)
diff --git a/testsuite/tests/indexed-types/should_compile/T7788.hs b/testsuite/tests/indexed-types/should_fail/T7788.hs
index 56f378d202..56f378d202 100644
--- a/testsuite/tests/indexed-types/should_compile/T7788.hs
+++ b/testsuite/tests/indexed-types/should_fail/T7788.hs
diff --git a/testsuite/tests/indexed-types/should_fail/T7788.stderr b/testsuite/tests/indexed-types/should_fail/T7788.stderr
new file mode 100644
index 0000000000..65c78aea3b
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_fail/T7788.stderr
@@ -0,0 +1,10 @@
+
+T7788.hs:9:7: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type: F (Id (Fix Id))
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the expression: undefined
+      In an equation for ‘foo’: foo = undefined
diff --git a/testsuite/tests/indexed-types/should_fail/T9554.stderr b/testsuite/tests/indexed-types/should_fail/T9554.stderr
index 4f8cbeba85..b62badda9d 100644
--- a/testsuite/tests/indexed-types/should_fail/T9554.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9554.stderr
@@ -9,3 +9,16 @@ T9554.hs:11:9: error:
        you're sure that type checking should terminate)
     • In the expression: x
       In an equation for ‘foo’: foo x = x
+
+T9554.hs:13:17: error:
+    • Reduction stack overflow; size = 201
+      When simplifying the following type:
+        F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F (F Bool)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+      Use -freduction-depth=0 to disable this check
+      (any upper bound you could choose might fail unpredictably with
+       minor updates to GHC, so disabling the check is recommended if
+       you're sure that type checking should terminate)
+    • In the first argument of ‘foo’, namely ‘Proxy’
+      In the expression: foo Proxy
+      In the expression:
+        case foo Proxy of { Proxy -> putStrLn "Made it!" }
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index a7dfd32f60..efa3a73bf5 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,18 +1,22 @@
 
-T9662.hs:46:4: error:
+T9662.hs:47:8: error:
     • Couldn't match type ‘k’ with ‘Int’
       ‘k’ is a rigid type variable bound by
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
         at T9662.hs:44:9
-      Expected type: Shape (((sh :. k) :. m) :. n)
-                     -> Shape (((sh :. m) :. n) :. k)
-        Actual type: Shape
+      Expected type: Exp (((sh :. m) :. n) :. k)
+                     -> Exp (((sh :. m) :. n) :. k)
+        Actual type: Exp
                        (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-                     -> Shape
+                     -> Exp
                           (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
-    • In the expression:
+    • In the first argument of ‘backpermute’, namely
+        ‘(modify
+            (atom :. atom :. atom :. atom)
+            (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’
+      In the expression:
         backpermute
           (modify
              (atom :. atom :. atom :. atom)
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 1da5824f5d..c6f29a492f 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -138,3 +138,4 @@ test('T10141', normal, compile_fail, [''])
 test('T10817', normal, compile_fail, [''])
 test('T10899', normal, compile_fail, [''])
 test('T11136', normal, compile_fail, [''])
+test('T7788', normal, compile_fail, [''])
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index ffcc050084..b8bd0b744f 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -364,7 +364,7 @@ test('T5030',
            #                        of family-applications leads to less sharing, I think
            # 2015-07-11:  201882912 reason unknown
 
-           (wordsize(64), 342331936, 10)]),
+           (wordsize(64), 653710960, 10)]),
              # Previously 530000000 (+/- 10%)
              # 17/1/13:   602993184  (x86_64/Linux)
              #            (new demand analyser)
@@ -382,7 +382,6 @@ test('T5030',
              #                          of family-applications leads to less sharing, I think
              # 2015-03-17 403932600  tweak to solver algorithm
 	     # 2015-12-11 653710960  TypeInType (see #11196)
-	     # 2016-03-14 342331936  unify type families eagerly
 
        only_ways(['normal'])
       ],
diff --git a/testsuite/tests/typecheck/should_fail/T9260.stderr b/testsuite/tests/typecheck/should_fail/T9260.stderr
index 37c37bd2f1..0773da2bf5 100644
--- a/testsuite/tests/typecheck/should_fail/T9260.stderr
+++ b/testsuite/tests/typecheck/should_fail/T9260.stderr
@@ -2,6 +2,6 @@
 T9260.hs:12:8: error:
     • Couldn't match type ‘2’ with ‘1’
       Expected type: Fin 1
-        Actual type: Fin ((0 + 1) + 1)
+        Actual type: Fin (1 + 1)
     • In the expression: Fsucc Fzero
       In an equation for ‘test’: test = Fsucc Fzero