Allow eager unification with type families.
authorRichard Eisenberg <eir@cis.upenn.edu>
Tue, 15 Mar 2016 02:09:36 +0000 (22:09 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Tue, 15 Mar 2016 03:50:52 +0000 (23:50 -0400)
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:
compiler/typecheck/TcUnify.hs
testsuite/tests/indexed-types/should_compile/T7788.hs [moved from testsuite/tests/indexed-types/should_fail/T7788.hs with 100% similarity]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/indexed-types/should_fail/T2693.stderr
testsuite/tests/indexed-types/should_fail/T4179.stderr
testsuite/tests/indexed-types/should_fail/T5439.stderr
testsuite/tests/indexed-types/should_fail/T7354.stderr
testsuite/tests/indexed-types/should_fail/T7729.stderr
testsuite/tests/indexed-types/should_fail/T7786.stderr
testsuite/tests/indexed-types/should_fail/T7788.stderr [deleted file]
testsuite/tests/indexed-types/should_fail/T9554.stderr
testsuite/tests/indexed-types/should_fail/T9662.stderr
testsuite/tests/indexed-types/should_fail/all.T

index a87f304..affdd59 100644 (file)
@@ -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
index bee76d2..a1f757a 100644 (file)
@@ -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, [''])
index 1d5ebef..b41e19f 100644 (file)
@@ -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)
index 1a2a18b..0dfa2db 100644 (file)
@@ -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)))
index f1ae705..b0cf937 100644 (file)
@@ -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
index b56db13..1f111fd 100644 (file)
@@ -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)
index e892eea..aa71a97 100644 (file)
@@ -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
index a58b69e..6cf8f8c 100644 (file)
@@ -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 (file)
index 65c78ae..0000000
+++ /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
index b62badd..4f8cbeb 100644 (file)
@@ -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!" }
index efa3a73..a7dfd32 100644 (file)
@@ -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)
index fa76360..1da5824 100644 (file)
@@ -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, [''])