{-# 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 snat pZ pS =
case fromSing snat of
0 -> unsafeCoerce pZ
nPlusOne -> withSomeSing (pred nPlusOne) $ \(sn :: Sing k) ->
unsafeCoerce (pS sn (elimNat @p @k sn pZ pS))