{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeInType          #-}
{-# LANGUAGE TypeOperators       #-}

module GHC.TypeLits.Util where

import           Data.Kind
import           Data.Proxy
import           Data.Singletons
import           Data.Singletons.Prelude.Num
import           Data.Singletons.TypeLits
import           Data.Type.Equality
import           GHC.TypeLits
import           Unsafe.Coerce

data Inductive :: Nat -> Type where
    NatZ :: Inductive 0
    NatS :: KnownNat n => !(Proxy n) -> Inductive (n + 1)

inductive
    :: forall n. KnownNat n
    => Proxy n
    -> Inductive n
inductive p = case sameNat p (Proxy @0) of
    Just Refl -> NatZ
    Nothing   -> case sn %:- SNat @1 of
      SNat -> case unsafeCoerce Refl :: ((n - 1) + 1) :~: n of
        Refl -> NatS (Proxy @(n - 1))
  where
    sn :: Sing n
    sn = SNat