Allow eager unification with type families.

Previously, checkTauTvUpdate, used in the eager unifier (TcUnify)
right before writing to a metavar, refused to write a metavar to
a type involving type functions. The reason for this was given
in a Note, but the Note didn't make all that much sense and even
admitted that it was a bit confused. The Note, in turn, referred
to another Note, which it was quite sceptical of, as well.

The type-family check was slowing down performance, so I tried
removing it, running the tests referred to in the Note. The tests
all passed without the check. Looking at more test results, I
saw several error messages improve without the check, and some cases
where GHC looped (T7788, in particular) it now doesn't.

So, all in all, quite a win: Two hairy Notes removed, several lines
of code removed, better performance, and improved output.

[skip ci]

13 files changed, 40 insertions, 138 deletions

diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index a87f30479e..affdd59617 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -50,7 +50,6 @@ import TyCon
 import TysWiredIn
 import Var
 import VarEnv
-import NameEnv
 import ErrUtils
 import DynFlags
 import BasicTypes
@@ -1450,47 +1449,15 @@ checkTauTvUpdate dflags origin t_or_k tv ty
   = do { ty   <- zonkTcType ty
        ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
        ; return $ case occurCheckExpand dflags tv ty of
-           OC_OK ty2 | type_fam_free ty2 -> Just (ty2, co_k)
-           _                             -> Nothing }
+           OC_OK ty2 -> Just (ty2, co_k)
+           _         -> Nothing }
 
   where
     kind_origin   = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k)
     details       = tcTyVarDetails tv
     info          = mtv_info details
 
-    -- See Note [Conservative unification check]
-    type_fam_free :: TcType -> Bool
-    type_fam_free = not . any isTypeFamilyTyCon . nameEnvElts . tyConsOfType
-
 {-
-Note [Conservative unification check]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When unifying (tv ~ rhs), w try to avoid creating deferred constraints
-only for efficiency.  However, we do not unify if
-  a) There's an occurs check (tv is in fvs(rhs)) (established by occurCheckExpand)
-     (see Note [Type synonyms and the occur check])
-  b) There's a type-function call in 'rhs'
-
-We always defer type-function calls, even if it's be perfectly safe to
-unify, eg (a ~ F [b]).  Reason: this ensures that the constraint
-solver gets to see, and hence simplify the type-function call, which
-in turn might simplify the type of an inferred function.  Test ghci046
-is a case in point.
-
-More mysteriously, test T7010 gave a horrible error
-  T7010.hs:29:21:
-    Couldn't match type `Serial (ValueTuple Float)' with `IO Float'
-    Expected type: (ValueTuple Vector, ValueTuple Vector)
-      Actual type: (ValueTuple Vector, ValueTuple Vector)
-because an insoluble type function constraint got mixed up with
-a soluble one when flattening.  I never fully understood this, but
-deferring type-function applications made it go away :-(.
-T5853 also got a less-good error message with more aggressive
-unification of type functions.
-
-Moreover the Note [Type family sharing] gives another reason, but
-again I'm not sure if it's really valid.
-
 Note [Type synonyms and the occur check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Generally speaking we try to update a variable with type synonyms not
@@ -1516,41 +1483,6 @@ the underlying definition of the type synonym.
 The same applies later on in the constraint interaction code; see TcInteract,
 function @occ_check_ok@.
 
-Note [Type family sharing]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-We must avoid eagerly unifying type variables to types that contain function symbols,
-because this may lead to loss of sharing, and in turn, in very poor performance of the
-constraint simplifier. Assume that we have a wanted constraint:
-{
-  m1 ~ [F m2],
-  m2 ~ [F m3],
-  m3 ~ [F m4],
-  D m1,
-  D m2,
-  D m3
-}
-where D is some type class. If we eagerly unify m1 := [F m2], m2 := [F m3], m3 := [F m4],
-then, after zonking, our constraint simplifier will be faced with the following wanted
-constraint:
-{
-  D [F [F [F m4]]],
-  D [F [F m4]],
-  D [F m4]
-}
-which has to be flattened by the constraint solver. In the absence of
-a flat-cache, this may generate a polynomially larger number of
-flatten skolems and the constraint sets we are working with will be
-polynomially larger.
-
-Instead, if we defer the unifications m1 := [F m2], etc. we will only
-be generating three flatten skolems, which is the maximum possible
-sharing arising from the original constraint.  That's why we used to
-use a local "ok" function, a variant of TcType.occurCheckExpand.
-
-HOWEVER, we *do* now have a flat-cache, which effectively recovers the
-sharing, so there's no great harm in losing it -- and it's generally
-more efficient to do the unification up-front.
-
 Note [Non-TcTyVars in TcUnify]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Because the same code is now shared between unifying types and unifying
diff --git a/testsuite/tests/indexed-types/should_fail/T7788.hs b/testsuite/tests/indexed-types/should_compile/T7788.hs
index 56f378d202..56f378d202 100644
--- a/testsuite/tests/indexed-types/should_fail/T7788.hs
+++ b/testsuite/tests/indexed-types/should_compile/T7788.hs
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index bee76d284c..a1f757a28b 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -275,3 +275,4 @@ 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 1d5ebefb9d..b41e19f3e1 100644
--- a/testsuite/tests/indexed-types/should_fail/T2693.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T2693.stderr
@@ -31,14 +31,13 @@ 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:29:20: error:
+T2693.hs:30:47: error:
     • Couldn't match type ‘TFn a0’ with ‘PVR a1’
       The type variables ‘a0’, ‘a1’ are ambiguous
-      Expected type: () -> Maybe (PVR a1)
-        Actual type: () -> Maybe (TFn a0)
-    • 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 }
+      Expected type: [PVR a1]
+        Actual type: [TFn a0]
+    • 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)
diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr
index 1a2a18bebf..0dfa2dbf3e 100644
--- a/testsuite/tests/indexed-types/should_fail/T4179.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr
@@ -3,8 +3,10 @@ T4179.hs:26:16: error:
     • Couldn't match type ‘A2 (x (A2 (FCon x) -> A3 (FCon x)))’
                      with ‘A2 (FCon x)’
       NB: ‘A2’ is a type function, and may not be injective
-      Expected type: x (A2 (FCon x) -> A3 (FCon x))
-                     -> A2 (FCon x) -> A3 (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)))
         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 f1ae705f5e..b0cf937cc7 100644
--- a/testsuite/tests/indexed-types/should_fail/T5439.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T5439.stderr
@@ -1,11 +1,10 @@
 
-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
+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)’
       In a stmt of a 'do' block:
         c <- complete ev $ inj $ Failure (e :: SomeException)
     • Relevant bindings include
diff --git a/testsuite/tests/indexed-types/should_fail/T7354.stderr b/testsuite/tests/indexed-types/should_fail/T7354.stderr
index b56db1398f..1f111fdd2c 100644
--- a/testsuite/tests/indexed-types/should_fail/T7354.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7354.stderr
@@ -1,11 +1,10 @@
 
 T7354.hs:28:11: error:
     • Occurs check: cannot construct the infinite type:
-        t1 ~ Base t (Prim [t1] t1)
-      Expected type: Prim [t1] t1 -> Base t (Prim [t1] t1)
-        Actual type: Prim [t1] t1 -> t1
+        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
     • 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 :: Prim [t1] t1 -> t (bound at T7354.hs:28:1)
+    • Relevant bindings include foo :: a -> 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 e892eea3c0..aa71a9774a 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:14: error:
+T7729.hs:36:25: error:
     • Couldn't match type ‘BasePrimMonad m’ with ‘t0 (BasePrimMonad m)’
       The type variable ‘t0’ is ambiguous
-      Expected type: t0 (BasePrimMonad m) a -> Rand m a
-        Actual type: BasePrimMonad (Rand m) a -> Rand m a
-    • In the first argument of ‘(.)’, namely ‘liftPrim’
+      Expected type: BasePrimMonad m a -> BasePrimMonad (Rand m) a
+        Actual type: BasePrimMonad m a -> t0 (BasePrimMonad m) a
+    • In the second argument of ‘(.)’, namely ‘lift’
       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 a58b69e7e7..6cf8f8c770 100644
--- a/testsuite/tests/indexed-types/should_fail/T7786.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T7786.stderr
@@ -11,20 +11,18 @@ T7786.hs:86:22: error:
         Nil :: Sing xxx <- return
                              (buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)
 
-T7786.hs:86:49: error:
+T7786.hs:86:22: 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)
-    • In the first argument of ‘return’, namely
-        ‘(buryUnder (dbKeys sub) k Nil `intersectPaths` dbKeys db)’
+    • 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 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_fail/T7788.stderr b/testsuite/tests/indexed-types/should_fail/T7788.stderr
deleted file mode 100644
index 65c78aea3b..0000000000
--- a/testsuite/tests/indexed-types/should_fail/T7788.stderr
+++ /dev/null
@@ -1,10 +0,0 @@
-
-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 b62badda9d..4f8cbeba85 100644
--- a/testsuite/tests/indexed-types/should_fail/T9554.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9554.stderr
@@ -9,16 +9,3 @@ 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 efa3a73bf5..a7dfd32f60 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,22 +1,18 @@
 
-T9662.hs:47:8: error:
+T9662.hs:46:4: 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: Exp (((sh :. m) :. n) :. k)
-                     -> Exp (((sh :. m) :. n) :. k)
-        Actual type: Exp
+      Expected type: Shape (((sh :. k) :. m) :. n)
+                     -> Shape (((sh :. m) :. n) :. k)
+        Actual type: Shape
                        (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
-                     -> Exp
+                     -> Shape
                           (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
-    • In the first argument of ‘backpermute’, namely
-        ‘(modify
-            (atom :. atom :. atom :. atom)
-            (\ (sh :. k :. m :. n) -> (sh :. m :. n :. k)))’
-      In the expression:
+    • 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 fa763607db..1da5824f5d 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -132,7 +132,6 @@ test('T9662', normal, compile_fail, [''])
 test('T7862', normal, compile, [''])
 test('T9896', normal, compile_fail, [''])
 test('T6088', normal, compile_fail, [''])
-test('T7788', normal, compile_fail, [''])
 test('T8550', normal, compile_fail, [''])
 test('T9554', normal, compile_fail, [''])
 test('T10141', normal, compile_fail, [''])