A fizzbuzz with strong type-safety, but still extensible to allow Bang if multiple of 7 etc

fizzbuzz-alternative.idr

import Data.So
%default total

fizz : Nat -> Bool
fizz n = (modNatNZ n 3 SIsNotZ) == 0

buzz : Nat -> Bool
buzz n = (modNatNZ n 5 SIsNotZ) == 0

data FizzT : (n: Nat) ->  Type where
  Fizz : {auto fizz : So (fizz n)} -> FizzT n
  NotFizz : {auto nfizz : So (not (fizz n)) } -> FizzT n

data BuzzT : (n: Nat) -> Type where
  Buzz : {auto buzz : So (buzz n)} -> BuzzT n
  NotBuzz : {auto nbuzz : So (not (buzz n)) } -> BuzzT n

Show (FizzT n) where 
  show Fizz = "Fizz" 
  show _ = ""

Show (BuzzT n) where 
  show Buzz = "Buzz"
  show _ = ""

fizzBuzz: (n: Nat) -> (FizzT n, BuzzT n)
fizzBuzz n  = case (choose (fizz n),choose (buzz n)) of
             (Left _,Right _) => (Fizz, NotBuzz) 
             (Right _,Left _) => (NotFizz, Buzz)
             (Left _,Left _) => (Fizz, Buzz)
             (Right _,Right _) => (NotFizz, NotBuzz)

showFizzBuzz : Nat -> String
showFizzBuzz n = let (fizzy, buzzy) = (fizzBuzz n) 
                     fizzbuzzy = (show fizzy) ++ (show buzzy) in
                     if fizzbuzzy == "" 
                        then show n 
                        else fizzbuzzy

There's a bit of duplication here though like the Show implementations.

Another implementation non extensible : https://gist.github.com/martinsson/919e35db5637767139e32f0ca61d7a44
Another shorter and more extensible, less type-safe by @FaustXVI https://gist.github.com/FaustXVI/6f54aa17e5eed4808124a03fd4cc382e