{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE Trustworthy #-}
{-|
Module:      Data.Eliminator.TypeNats
Copyright:   (C) 2017 Ryan Scott
License:     BSD-style (see the file LICENSE)
Maintainer:  Ryan Scott
Stability:   Experimental
Portability: GHC

A crude imitation of an eliminator function for 'GHC.TypeNats.Nat'.
-}
module Data.Eliminator.TypeNats (elimNat) where

import Data.Kind (Type)
import Data.Singletons

import GHC.TypeLits.Singletons ()
import GHC.TypeNats

import Unsafe.Coerce (unsafeCoerce)

-- | Although 'Nat' is not actually an inductive data type in GHC, we can
-- (crudely) pretend that it is using this eliminator.
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 :: 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 Sing n
snat Apply p 0
pZ forall (k :: Nat). Sing k -> Apply p k -> Apply p (k + 1)
pS = forall (n' :: Nat). Sing n' -> Apply p n'
go @n Sing n
snat
  where
    go :: forall (n' :: Nat). Sing n' -> Apply p n'
    go :: forall (n' :: Nat). Sing n' -> Apply p n'
go Sing n'
snat' =
      case Sing n' -> Demote Nat
forall (a :: Nat). Sing a -> 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 (Demote Nat -> Demote Nat
forall a. Enum a => a -> a
pred 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
$ \(Sing a
sk :: 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
sk (forall (n' :: Nat). Sing n' -> Apply p n'
go @k Sing a
sk))