Fix egregious blunder in the type flattener
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 9 Apr 2014 21:47:09 +0000 (22:47 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 10 Apr 2014 07:12:51 +0000 (08:12 +0100)
In tidying up the flattener I introduced an error that no
regression test caught, giving rise to Trac #8978, #8979.
It shows up if you have a type synonym whose RHS mentions
type functions, such sas
     type family F a
     type T a = (F a, a)   -- This synonym isn't properly flattened

The fix is easy, but sadly the bug is in the released GHC 7.8.1

compiler/typecheck/TcCanonical.lhs
testsuite/tests/indexed-types/should_compile/T8978.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/T8979.hs [new file with mode: 0644]
testsuite/tests/indexed-types/should_compile/all.T
testsuite/tests/indexed-types/should_fail/T5439.stderr
testsuite/tests/indexed-types/should_fail/T5934.stderr

index cc53d03..9eecc47 100644 (file)
@@ -492,13 +492,21 @@ flatten f ctxt (FunTy ty1 ty2)
        ; return (mkFunTy xi1 xi2, mkTcFunCo Nominal co1 co2) }
 
 flatten f ctxt (TyConApp tc tys)
+
+  -- Expand type synonyms that mention type families 
+  -- on the RHS; see Note [Flattening synonyms]
+  | Just (tenv, rhs, tys') <- tcExpandTyCon_maybe tc tys
+  , any isSynFamilyTyCon (tyConsOfType rhs)
+  = flatten f ctxt (mkAppTys (substTy (mkTopTvSubst tenv) rhs) tys')
+
   -- For * a normal data type application
-  --     * type synonym application  See Note [Flattening synonyms]
   --     * data family application
+  --     * type synonym application whose RHS does not mention type families
+  --             See Note [Flattening synonyms]
   -- we just recursively flatten the arguments.
   | not (isSynFamilyTyCon tc)
-    = do { (xis,cos) <- flattenMany f ctxt tys
-         ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
+  = do { (xis,cos) <- flattenMany f ctxt tys
+       ; return (mkTyConApp tc xis, mkTcTyConAppCo Nominal tc cos) }
 
   -- Otherwise, it's a type function application, and we have to
   -- flatten it away as well, and generate a new given equality constraint
@@ -534,6 +542,9 @@ flatten _f ctxt ty@(ForAllTy {})
 
 Note [Flattening synonyms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
+Not expanding synonyms aggressively improves error messages, and
+keeps types smaller. But we need to take care.
+
 Suppose
    type T a = a -> a
 and we want to flatten the type (T (F a)).  Then we can safely flatten
@@ -541,12 +552,16 @@ the (F a) to a skolem, and return (T fsk).  We don't need to expand the
 synonym.  This works because TcTyConAppCo can deal with synonyms
 (unlike TyConAppCo), see Note [TcCoercions] in TcEvidence.
 
-Not expanding synonyms aggressively improves error messages.
+But (Trac #8979) for
+   type T a = (F a, a)    where F is a type function
+we must expand the synonym in (say) T Int, to expose the type functoin
+to the flattener.
+
 
 Note [Flattening under a forall]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Under a forall, we
-  (a) MUST apply the inert subsitution
+  (a) MUST apply the inert substitution
   (b) MUST NOT flatten type family applications
 Hence FMSubstOnly.
 
diff --git a/testsuite/tests/indexed-types/should_compile/T8978.hs b/testsuite/tests/indexed-types/should_compile/T8978.hs
new file mode 100644 (file)
index 0000000..077a07d
--- /dev/null
@@ -0,0 +1,12 @@
+{-# LANGUAGE FlexibleContexts, TypeFamilies #-}
+module T8978 where
+
+type Syn a = Associated a
+
+class Eq (Associated a) => Foo a where
+    type Associated a :: *
+    foo :: a -> Syn a -> Bool
+
+instance Foo () where
+    type Associated () = Int
+    foo _ x = x == x
diff --git a/testsuite/tests/indexed-types/should_compile/T8979.hs b/testsuite/tests/indexed-types/should_compile/T8979.hs
new file mode 100644 (file)
index 0000000..85e13ce
--- /dev/null
@@ -0,0 +1,10 @@
+{-# LANGUAGE TypeFamilies #-}
+module T8979 where
+
+type family F a
+type family G a
+
+type H a = G a
+
+f :: F (G Char) -> F (H Char)
+f a = a
index 76682ad..5f30446 100644 (file)
@@ -241,3 +241,5 @@ test('ClosedFam2', extra_clean(['ClosedFam2.o-boot', 'ClosedFam2.hi-boot']),
 test('T8651', normal, compile, [''])
 test('T8889', normal, compile, [''])
 test('T8913', normal, compile, [''])
+test('T8978', normal, compile, [''])
+test('T8979', normal, compile, [''])
index d5f0318..18af3fa 100644 (file)
@@ -1,25 +1,26 @@
-
-T5439.hs:83:28:
-    Couldn't match type ‘Attempt (HNth n0 l0) -> Attempt (HElemOf l0)’
-                  with ‘Attempt (WaitOpResult (WaitOps rs))’
-    Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))
-      Actual type: f (Attempt (WaitOpResult (WaitOps rs)))
-    Relevant bindings include
-      register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool
-        (bound at T5439.hs:65:9)
-      ev :: f (Attempt (WaitOpResult (WaitOps rs)))
-        (bound at T5439.hs:62:22)
-      ops :: WaitOps rs (bound at T5439.hs:62:18)
-      registerWaitOp :: WaitOps rs
-                        -> f (Attempt (WaitOpResult (WaitOps rs))) -> IO Bool
-        (bound at T5439.hs:62:3)
-    In the first argument of ‘complete’, namely ‘ev’
-    In the expression: complete ev
-
-T5439.hs:83:39:
-    Couldn't match expected type ‘Peano n0’
-                with actual type ‘Attempt α0’
-    In the second argument of ‘($)’, namely
-      ‘Failure (e :: SomeException)’
-    In the second argument of ‘($)’, namely
-      ‘inj $ Failure (e :: SomeException)’
+\r
+T5439.hs:83:28:\r
+    Couldn't match type ‘Attempt (HHead (HDrop n0 l0))\r
+                         -> Attempt (HElemOf l0)’\r
+                  with ‘Attempt (WaitOpResult (WaitOps rs))’\r
+    Expected type: f (Attempt (HNth n0 l0) -> Attempt (HElemOf l0))\r
+      Actual type: f (Attempt (WaitOpResult (WaitOps rs)))\r
+    Relevant bindings include\r
+      register :: Bool -> Peano n -> WaitOps (HDrop n rs) -> IO Bool\r
+        (bound at T5439.hs:65:9)\r
+      ev :: f (Attempt (WaitOpResult (WaitOps rs)))\r
+        (bound at T5439.hs:62:22)\r
+      ops :: WaitOps rs (bound at T5439.hs:62:18)\r
+      registerWaitOp :: WaitOps rs\r
+                        -> f (Attempt (WaitOpResult (WaitOps rs))) -> IO Bool\r
+        (bound at T5439.hs:62:3)\r
+    In the first argument of ‘complete’, namely ‘ev’\r
+    In the expression: complete ev\r
+\r
+T5439.hs:83:39:\r
+    Couldn't match expected type ‘Peano n0’\r
+                with actual type ‘Attempt α0’\r
+    In the second argument of ‘($)’, namely\r
+      ‘Failure (e :: SomeException)’\r
+    In the second argument of ‘($)’, namely\r
+      ‘inj $ Failure (e :: SomeException)’\r
index cf7bf87..85ab1a1 100644 (file)
@@ -1,7 +1,8 @@
-
-T5934.hs:12:7:
-    Cannot instantiate unification variable ‘a0’
-    with a type involving foralls: (forall s. GenST s) -> Int
-      Perhaps you want ImpredicativeTypes
-    In the expression: 0
-    In an equation for ‘run’: run = 0
+\r
+T5934.hs:12:7:\r
+    Cannot instantiate unification variable ‘a0’\r
+    with a type involving foralls:\r
+      (forall s. Gen (PrimState (ST s))) -> Int\r
+      Perhaps you want ImpredicativeTypes\r
+    In the expression: 0\r
+    In an equation for ‘run’: run = 0\r