blob: ed82f2a35b55728c98210852a64b6ffe85b229dc (
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
|
{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies,
TypeOperators, RankNTypes #-}
module T7294 where
import Data.Kind (Type)
data Nat = Zero | Succ Nat
data Vec :: Type -> Nat -> Type where
Nil :: Vec a Zero
Cons :: a -> Vec a n -> Vec a (Succ n)
type family (m :: Nat) :< (n :: Nat) :: Bool
type instance m :< Zero = False
type instance Zero :< Succ n = True
type instance Succ n :< Succ m = n :< m
data SNat :: Nat -> Type where
SZero :: SNat Zero
SSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
nth :: ((k :< n) ~ True) => Vec a n -> SNat k -> a
nth (Cons x _) SZero = x
nth (Cons _ xs) (SSucc k) = nth xs k
nth Nil _ = undefined
|
