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