Prevent eager unification with type families.
authorRichard Eisenberg <eir@cis.upenn.edu>
Sat, 19 Mar 2016 02:36:34 +0000 (22:36 -0400)
committerRichard Eisenberg <eir@cis.upenn.edu>
Mon, 21 Mar 2016 16:16:11 +0000 (12:16 -0400)
See Note [Prevent unification with type families]
in TcUnify for the details.

16 files changed:
compiler/typecheck/TcType.hs
compiler/typecheck/TcUnify.hs
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.hs [moved from testsuite/tests/indexed-types/should_compile/T7788.hs with 100% similarity]
testsuite/tests/indexed-types/should_fail/T7788.stderr [new file with mode: 0644]
testsuite/tests/indexed-types/should_fail/T9554.stderr
testsuite/tests/indexed-types/should_fail/T9662.stderr
testsuite/tests/indexed-types/should_fail/all.T
testsuite/tests/perf/compiler/all.T
testsuite/tests/typecheck/should_fail/T9260.stderr

index cf3b317..494b50d 100644 (file)
@@ -1432,6 +1432,10 @@ We have
   occurCheckExpand b (F (G b)) = F Char
 even though we could also expand F to get rid of b.
 
+The two variants of the function are to support TcUnify.checkTauTvUpdate,
+which wants to prevent unification with type families. For more on this
+point, see Note [Prevent unification with type families] in TcUnify.
+
 See also Note [occurCheckExpand] in TcCanonical
 -}
 
@@ -1449,10 +1453,10 @@ instance Applicative OccCheckResult where
       (<*>) = ap
 
 instance Monad OccCheckResult where
-  OC_OK x     >>= k = k x
-  OC_Forall   >>= _ = OC_Forall
-  OC_NonTyVar >>= _ = OC_NonTyVar
-  OC_Occurs   >>= _ = OC_Occurs
+  OC_OK x       >>= k = k x
+  OC_Forall     >>= _ = OC_Forall
+  OC_NonTyVar   >>= _ = OC_NonTyVar
+  OC_Occurs     >>= _ = OC_Occurs
 
 occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
 -- See Note [Occurs check expansion]
@@ -1466,7 +1470,6 @@ occurCheckExpand :: DynFlags -> TcTyVar -> Type -> OccCheckResult Type
 -- version of the type, which is guaranteed to be syntactically free
 -- of the given type variable.  If the type is already syntactically
 -- free of the variable, then the same type is returned.
-
 occurCheckExpand dflags tv ty
   | MetaTv { mtv_info = SigTv } <- details
                   = go_sig_tv ty
@@ -1488,7 +1491,8 @@ occurCheckExpand dflags tv ty
     -- True => fine
     fast_check (LitTy {})          = True
     fast_check (TyVarTy tv')       = tv /= tv' && fast_check (tyVarKind tv')
-    fast_check (TyConApp tc tys)   = all fast_check tys && (isTauTyCon tc || impredicative)
+    fast_check (TyConApp tc tys)   = all fast_check tys
+                                     && (isTauTyCon tc || impredicative)
     fast_check (ForAllTy (Anon a) r) = fast_check a && fast_check r
     fast_check (AppTy fun arg)     = fast_check fun && fast_check arg
     fast_check (ForAllTy (Named tv' _) ty)
index 8eeef4e..d8f1e6a 100644 (file)
@@ -49,6 +49,7 @@ import Inst
 import TyCon
 import TysWiredIn
 import Var
+import VarSet
 import VarEnv
 import ErrUtils
 import DynFlags
@@ -1440,16 +1441,91 @@ checkTauTvUpdate dflags origin t_or_k tv ty
   | otherwise
   = do { ty   <- zonkTcType ty
        ; co_k <- uType kind_origin KindLevel (typeKind ty) (tyVarKind tv)
-       ; return $ case occurCheckExpand dflags tv ty of
-           OC_OK ty2 -> Just (ty2, co_k)
-           _         -> Nothing }
+       ; if | defer_me ty ->  -- Quick test
+                -- Failed quick test so try harder
+                case occurCheckExpand dflags tv ty of
+                   OC_OK ty2 | defer_me ty2 -> return Nothing
+                             | otherwise    -> return (Just (ty2, co_k))
+                   _                        -> return Nothing
+            | otherwise   -> return (Just (ty, co_k)) }
 
   where
     kind_origin   = KindEqOrigin (mkTyVarTy tv) (Just ty) origin (Just t_or_k)
     details       = tcTyVarDetails tv
     info          = mtv_info details
 
+    impredicative = canUnifyWithPolyType dflags details
+
+    defer_me :: TcType -> Bool
+    -- Checks for (a) occurrence of tv
+    --            (b) type family applications
+    --            (c) foralls
+    -- See Note [Prevent unification with type families]
+    -- See Note [Refactoring hazard: checkTauTvUpdate]
+    defer_me (LitTy {})        = False
+    defer_me (TyVarTy tv')     = tv == tv' || defer_me (tyVarKind tv')
+    defer_me (TyConApp tc tys) = isTypeFamilyTyCon tc || any defer_me tys
+                                 || not (impredicative || isTauTyCon tc)
+    defer_me (ForAllTy bndr t) = defer_me (binderType bndr) || defer_me t
+                                 || (isNamedBinder bndr && not impredicative)
+    defer_me (AppTy fun arg)   = defer_me fun || defer_me arg
+    defer_me (CastTy ty co)    = defer_me ty || defer_me_co co
+    defer_me (CoercionTy co)   = defer_me_co co
+
+      -- We don't really care if there are type families in a coercion,
+      -- but we still can't have an occurs-check failure
+    defer_me_co co = tv `elemVarSet` tyCoVarsOfCo co
+
 {-
+Note [Prevent unification with type families]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We prevent unification with type families because of an uneasy compromise.
+It's perfectly sound to unify with type families, and it even improves the
+error messages in the testsuite. It also modestly improves performance, at
+least in some cases. But it's disastrous for test case perf/compiler/T3064.
+Here is the problem: Suppose we have (F ty) where we also have [G] F ty ~ a.
+What do we do? Do we reduce F? Or do we use the given? Hard to know what's
+best. GHC reduces. This is a disaster for T3064, where the type's size
+spirals out of control during reduction. (We're not helped by the fact that
+the flattener re-flattens all the arguments every time around.) If we prevent
+unification with type families, then the solver happens to use the equality
+before expanding the type family.
+
+It would be lovely in the future to revisit this problem and remove this
+extra, unnecessary check. But we retain it for now as it seems to work
+better in practice.
+
+Note [Refactoring hazard: checkTauTvUpdate]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+I (Richard E.) have a sad story about refactoring this code, retained here
+to prevent others (or a future me!) from falling into the same traps.
+
+It all started with #11407, which was caused by the fact that the TyVarTy
+case of defer_me didn't look in the kind. But it seemed reasonable to
+simply remove the defer_me check instead.
+
+It referred to two Notes (since removed) that were out of date, and the
+fast_check code in occurCheckExpand seemed to do just about the same thing as
+defer_me. The one piece that defer_me did that wasn't repeated by
+occurCheckExpand was the type-family check. (See Note [Prevent unification
+with type families].) So I checked the result of occurCheckExpand for any
+type family occurrences and deferred if there were any. This was done
+in commit e9bf7bb5cc9fb3f87dd05111aa23da76b86a8967 .
+
+This approach turned out not to be performant, because the expanded type
+was bigger than the original type, and tyConsOfType looks through type
+synonyms. So it then struck me that we could dispense with the defer_me
+check entirely. This simplified the code nicely, and it cut the allocations
+in T5030 by half. But, as documented in Note [Prevent unification with
+type families], this destroyed performance in T3064. Regardless, I missed this
+regression and the change was committed as
+3f5d1a13f112f34d992f6b74656d64d95a3f506d .
+
+Bottom lines:
+ * defer_me is back, but now fixed w.r.t. #11407.
+ * Tread carefully before you start to refactor here. There can be
+   lots of hard-to-predict consequences.
+
 Note [Type synonyms and the occur check]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Generally speaking we try to update a variable with type synonyms not
index a1f757a..bee76d2 100644 (file)
@@ -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, [''])
index 5e925c3..0c00711 100644 (file)
@@ -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 }
index f3411a0..516bdf3 100644 (file)
@@ -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)))
index b76b0f9..f1ae705 100644 (file)
@@ -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)
index 1f111fd..b56db13 100644 (file)
@@ -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)
index 80b6fd8..b209c9c 100644 (file)
@@ -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
index 6cf8f8c..a58b69e 100644 (file)
@@ -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_fail/T7788.stderr b/testsuite/tests/indexed-types/should_fail/T7788.stderr
new file mode 100644 (file)
index 0000000..65c78ae
--- /dev/null
@@ -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
index 4f8cbeb..b62badd 100644 (file)
@@ -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!" }
index a7dfd32..efa3a73 100644 (file)
@@ -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)
index 1da5824..c6f29a4 100644 (file)
@@ -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, [''])
index ffcc050..b8bd0b7 100644 (file)
@@ -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'])
       ],
index 37c37bd..0773da2 100644 (file)
@@ -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