{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Data.Eliminator.TypeNats (elimNat) where
import Data.Kind (Type)
import Data.Singletons
import Data.Singletons.TypeLits
import GHC.TypeNats
import Unsafe.Coerce (unsafeCoerce)
elimNat :: forall (p :: Nat ~> Type) (n :: Nat).
Sing n
-> Apply p 0
-> (forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1))
-> Apply p n
elimNat :: Sing n
-> Apply p 0
-> (forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1))
-> Apply p n
elimNat Sing n
snat Apply p 0
pZ forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1)
pS =
case Sing n -> Demote Nat
forall k (a :: k). SingKind k => Sing a -> Demote k
fromSing Sing n
snat of
Demote Nat
0 -> Apply p 0 -> Apply p n
forall a b. a -> b
unsafeCoerce Apply p 0
pZ
Demote Nat
nPlusOne -> Demote Nat -> (forall (a :: Nat). Sing a -> Apply p n) -> Apply p n
forall k r.
SingKind k =>
Demote k -> (forall (a :: k). Sing a -> r) -> r
withSomeSing (Natural -> Natural
forall a. Enum a => a -> a
pred Natural
Demote Nat
nPlusOne) ((forall (a :: Nat). Sing a -> Apply p n) -> Apply p n)
-> (forall (a :: Nat). Sing a -> Apply p n) -> Apply p n
forall a b. (a -> b) -> a -> b
$ \(sn :: Sing k) ->
Apply p (a + 1) -> Apply p n
forall a b. a -> b
unsafeCoerce (Sing a -> Apply p a -> Apply p (a + 1)
forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1)
pS Sing a
sn (Sing a
-> Apply p 0
-> (forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1))
-> Apply p a
forall (p :: Nat ~> *) (n :: Nat).
Sing n
-> Apply p 0
-> (forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1))
-> Apply p n
elimNat @p @k Sing a
sn Apply p 0
pZ forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1)
pS))