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