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