Test Trac #8985

testsuite/tests/polykinds/T8985.hs

+{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators #-}
+
+module T8905 where
+
+data X (xs :: [k]) = MkX
+data Y :: (k -> *) -> [k] -> * where
+  MkY :: f x -> Y f (x ': xs)
+
+type family F (a :: [[*]]) :: *
+type instance F xss = Y X xss
+
+works :: Y X '[ '[ ] ] -> ()
+works (MkY MkX) = ()
+
+fails :: F '[ '[ ] ] -> ()
+fails (MkY MkX) = ()

testsuite/tests/polykinds/all.T

@@ -99,3 +99,4 @@ test('T8616', normal, compile_fail,[''])
 test('T8566a', expect_broken(8566), compile,[''])
 test('T7481', normal, compile_fail,[''])
 test('T8705', normal, compile, [''])
+test('T8985', normal, compile, [''])