Remove the type-checking knot.
[ghc.git] / testsuite / tests / polykinds / T8985.hs
1 {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators #-}
2
3 module T8985 where
4
5 import Data.Kind (Type)
6
7 data X (xs :: [k]) = MkX
8 data Y :: (k -> Type) -> [k] -> Type where
9 MkY :: f x -> Y f (x ': xs)
10
11 type family F (a :: [[Type]]) :: Type
12 type instance F xss = Y X xss
13
14 works :: Y X '[ '[ ] ] -> ()
15 works (MkY MkX) = ()
16
17 fails :: F '[ '[ ] ] -> ()
18 fails (MkY MkX) = ()