Playing with dependent types in Haskell

dependent-bullshit.hs

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module Main where

import Data.Char (toUpper)
import Data.Constraint (Dict (..))
import Data.Proxy (Proxy (..))
import System.Environment (getArgs)
import System.IO (interact)
import Text.Read (readMaybe)

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

fromSBool :: SBool b -> Bool
fromSBool STrue = True
fromSBool SFalse = False

data SomeSBool where
  SomeSBool :: SBool b -> SomeSBool

withSomeSBool :: SomeSBool -> (forall (b :: Bool). SBool b -> r) -> r
withSomeSBool (SomeSBool s) f = f s

toSBool :: Bool -> SomeSBool
toSBool True = SomeSBool STrue
toSBool False = SomeSBool SFalse

class Echo (scream :: Bool) where
  echoStdin :: Proxy scream -> IO ()

instance Echo 'True where
  echoStdin _ = interact (fmap toUpper)

instance Echo 'False where
  echoStdin _ = interact id

main :: IO ()
main = do
  args <- getArgs
  let scream = case args of
        ["--scream"] -> True
        _            -> False
  withSomeSBool (toSBool scream) $
    \(sb :: SBool b) ->
      case dict @Echo sb of
        Dict -> echoStdin (Proxy @b)

dict :: (c 'True, c 'False) => SBool b -> Dict (c b)
dict STrue = Dict
dict SFalse = Dict