summaryrefslogtreecommitdiff
path: root/testsuite/tests/indexed-types/should_fail/T14246.hs
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