Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / indexed-types / should_fail / T14246.hs
1 {-# LANGUAGE RankNTypes, GADTs, TypeOperators, PolyKinds, DataKinds, TypeFamilies, AllowAmbiguousTypes, UndecidableInstances, TypeInType #-}
2
3 module T14246 where
4
5 import Data.Kind
6
7 data Nat = Z | S Nat
8
9 data Vect :: Nat -> Type -> Type where
10 Nil :: Vect Z a
11 Cons :: a -> Vect n a -> Vect (S n) a
12
13 data Label a = Label a
14
15 data L
16
17 type family KLN (n :: k) :: Nat where
18 KLN (f :: v -> k) = S (KLN (forall t. f t))
19 KLN (f :: Type) = Z
20
21 type family Reveal (n :: k) (l :: Vect (KLN n) L) :: Type where
22 Reveal (f :: v -> k) (Cons (Label (t :: v)) l) = Reveal (f t) l
23 Reveal (a :: Type) Nil = a