blob: 28a354be272211c78956b7f41438ce759734c7bd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
{-# 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) = ()
|
