singleton-bool.hs

{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilyDependencies #-}

{-
Here are the GHC/singletons versions I used to run this:

$ nix-shell -p haskell.compiler.ghc921 --command 'cabal repl -b "singletons == 3.0.1" -b "singletons-base == 3.1"'
-}

module SingletonBool where

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

-- You might as well mark this as injective since it is:
type family F (b :: Bool) = (r :: Type) | r -> b where
  F True = Int
  F False = Char

f1 :: forall (x :: Bool). (Sing x -> F x) -> Sing x -> F x
f1 = ($)

f2 :: Sing x -> F x
f2 = \case
  STrue -> 2
  SFalse -> 'b'