Type-level eliminators in GHC!

ElimNat.hs

#!/usr/bin/env cabal
{- cabal:
build-depends: base           >= 4.12
             , singleton-nats >= 0.4.1
             , singletons     >= 2.5.1
-}

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Wno-unticked-promoted-constructors #-}
module Main where

import Data.Kind
import Data.Nat
import Data.Singletons.Prelude

-- | A type-level eliminator for 'Nat's.
type family ElimNat (p :: Nat ~> Type)
                    (s :: Nat)
                    (pZ :: p @@ Z)
                    (pS :: KindOf (PS p)) -- (pS :: forall (n :: Nat) -> (p @@ n ~> p @@ S n))
                 :: p @@ s where
  ElimNat _ Z     pZ _  = pZ
  ElimNat p (S n) pZ pS = pS n @@ ElimNat p n pZ pS
data PS (p :: Nat ~> Type) (n :: Nat) :: p @@ n ~> p @@ S n

-- | Multiply a 'Nat' by two.
type family TimesTwo (n :: Nat) :: Nat where
  TimesTwo n = ElimNat (ConstSym1 Nat) n Z Doubler
data Doubler (n :: Nat) :: Const Nat n ~> Nat
type instance Apply (Doubler _) x = S (S x)

main :: IO ()
main = mapM_ print [ SomeSing $ sing @(TimesTwo (Lit 0))
                   , SomeSing $ sing @(TimesTwo (Lit 1))
                   , SomeSing $ sing @(TimesTwo (Lit 2))
                   ]