Type-level programming https://mail.haskell.org/pipermail/haskell-cafe/2022-January/135029.html

Countdown.hs

{-# LANGUAGE TypeFamilies, DataKinds, ConstraintKinds, UndecidableInstances, TypeApplications, ScopedTypeVariables #-}

module Countdown where

import Data.Proxy
import GHC.TypeNats
import Data.Kind
import qualified Fcf as F

data C2 :: Nat -> F.Exp Constraint
type instance F.Eval (C2 x) =
  (KnownNat x,
     IsBool (F.Eval (x F.> 0)),
     F.Eval (F.If (F.Eval (x F.> 0))
       (C2 (x - 1))
       (F.Pure (() :: Constraint))))

class IsBool b where
  getBool :: SBool b

instance IsBool 'True where
  getBool = STrue

instance IsBool 'False where
  getBool = SFalse

data SBool (a :: Bool) where
  SFalse :: SBool 'False
  STrue :: SBool 'True

countdown :: forall n. F.Eval (C2 n) => Proxy n -> String
countdown _ =
  case getBool @(F.Eval (n F.> 0)) of
    STrue -> show (natVal @n Proxy) ++ " " ++ countdown @(n-1) Proxy
    SFalse -> "boom"