Test Trac #4093

testsuite/tests/ghc-regress/indexed-types/should_fail/T4093a.hs

+{-# LANGUAGE TypeFamilies #-}
+module T4093a where
+
+type family Foo x
+type instance Foo () = Maybe ()
+
+hang :: (Foo e ~ Maybe e) => Foo e
+hang = Just ()

testsuite/tests/ghc-regress/indexed-types/should_fail/T4093a.stderr

+
+T4093a.hs:8:8:
+    Couldn't match type `e' with `()'
+      `e' is a rigid type variable bound by
+          the type signature for `hang' at T4093a.hs:7:14
+    In the expression: Just ()
+    In an equation for `hang': hang = Just ()

testsuite/tests/ghc-regress/indexed-types/should_fail/T4093b.hs

+{-# LANGUAGE GADTs, EmptyDataDecls, ScopedTypeVariables, TypeFamilies #-}
+
+module T4093b where
+
+data C
+data O
+
+type family   EitherCO e a b :: *
+type instance EitherCO C a b = a
+type instance EitherCO O a b = b
+
+data MaybeC ex t where
+  JustC    :: t -> MaybeC C t
+  NothingC ::      MaybeC O t
+
+data Block (n :: * -> * -> *) e x
+
+
+blockToNodeList ::
+  forall n e x. (EitherCO e (A C O n) (A O O n) ~ A e O n,
+                 EitherCO x (A C C n) (A C O n) ~ A C x n) =>
+    Block n e x -> A e x n
+
+type A e x n = (MaybeC e (n C O), MaybeC x (n O C))
+blockToNodeList b = foldBlockNodesF (f, l) b z 
+  where
+    z :: EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))
+    z = undefined
+
+    f :: n C O -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)
+    f n _ = (JustC n, NothingC)
+
+    l :: n O C -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C C n) (A O C n)
+    l _ = undefined
+
+foldBlockNodesF  :: forall n a b c e x .
+                   ( n C O       -> a -> b
+                   , n O C       -> b -> c)
+                 -> (Block n e x -> EitherCO e a b -> EitherCO x c b)
+foldBlockNodesF _ = undefined

testsuite/tests/ghc-regress/indexed-types/should_fail/T4093b.stderr

+
+T4093b.hs:25:21:
+    Could not deduce (EitherCO
+                        x (EitherCO e (A C C n) (A O C n)) (A C O n)
+                        ~
+                      (MaybeC e (n C O), MaybeC x (n O C)))
+      from the context (EitherCO e (A C O n) (A O O n) ~ A e O n,
+                        EitherCO x (A C C n) (A C O n) ~ A C x n)
+    In the expression: foldBlockNodesF (f, l) b z
+    In an equation for `blockToNodeList':
+        blockToNodeList b
+          = foldBlockNodesF (f, l) b z
+          where
+              z ::
+                EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))
+              z = undefined
+              f ::
+                n C O
+                -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)
+              f n _ = (JustC n, NothingC)
+              ....
+
+T4093b.hs:31:13:
+    Couldn't match type `e' with `C'
+      `e' is a rigid type variable bound by
+          the type signature for `blockToNodeList' at T4093b.hs:20:12
+    In the expression: (JustC n, NothingC)
+    In an equation for `f': f n _ = (JustC n, NothingC)
+    In an equation for `blockToNodeList':
+        blockToNodeList b
+          = foldBlockNodesF (f, l) b z
+          where
+              z ::
+                EitherCO e (EitherCO e (A C O n) (A O O n)) (EitherCO e (A C O n) (A O O n))
+              z = undefined
+              f ::
+                n C O
+                -> EitherCO e (A C O n) (A O O n) -> EitherCO e (A C O n) (A O O n)
+              f n _ = (JustC n, NothingC)
+              ....

testsuite/tests/ghc-regress/indexed-types/should_fail/all.T

@@ -54,3 +54,5 @@ test('T2677', normal, compile_fail, [''])
 test('T4099', normal, compile_fail, [''])
 test('T4272', normal, compile_fail, [''])
 test('T4246', normal, compile_fail, [''])
+test('T4093a', normal, compile_fail, [''])
+test('T4093b', normal, compile_fail, [''])