{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies      #-}
{-# LANGUAGE TypeOperators     #-}


import           Data.Proxy
import           GHC.TypeLits


-- we use DataKinds to lift FizzBuzzItems to the type system level

data FizzBuzzItem = Number Nat
                  | Fizz
                  | Buzz
                  | FizzBuzz


-- the result family associates the four possible boolean conditions to a resulting item

type family FizzBuzzResult (d3 :: Bool) (d5 :: Bool) (n :: Nat) where
  FizzBuzzResult 'False 'False n = 'Number n
  FizzBuzzResult 'True  'False n = 'Fizz
  FizzBuzzResult 'False 'True  n = 'Buzz
  FizzBuzzResult 'True  'True  n = 'FizzBuzz


-- GetFizzBuzz is simply a type-level function from type-level number to item
-- you can call it in GHCI with:
--   :t (Proxy :: Proxy (GetFizzBuzz 15))

type GetFizzBuzz (n :: Nat) = FizzBuzzResult (Mod n 3 <=? 0) (Mod n 5 <=? 0) n


-- to go further: let's have a runtime value!
-- we add overlapping instances for proxies of our type-level items

instance {-# OVERLAPPING #-} Show (Proxy 'Fizz)     where show = const "Fizz"
instance {-# OVERLAPPING #-} Show (Proxy 'Buzz)     where show = const "Buzz"
instance {-# OVERLAPPING #-} Show (Proxy 'FizzBuzz) where show = const "FizzBuzz"

instance {-# OVERLAPPING #-} KnownNat n => Show (Proxy ('Number n)) where
  show = show . natVal . toNatProxy
    where toNatProxy :: Proxy ('Number n) -> Proxy n
          toNatProxy = const Proxy


-- and we introduce a function that does the string output
-- you can call it in GHCI with
--   fb (Proxy :: Proxy 12)

fb :: Show (Proxy (GetFizzBuzz n)) => Proxy (n :: Nat) -> String
fb = show . toResult
  where toResult :: Proxy (n :: Nat) -> Proxy (GetFizzBuzz n)
        toResult = const Proxy