{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Main where

import Data.Type.Equality ((:~:)(..))
import System.IO.Unsafe (unsafePerformIO)

data Mode = A | B
data Settings (mode :: Mode) where
    SettingsA :: Int -> Settings 'A
    SettingsB :: String -> Settings 'B

deriving instance Show (Settings mode)

class KnownMode (mode :: Mode) where
  knownMode :: Either (mode :~: 'A) (mode :~: 'B)
instance KnownMode 'A where knownMode = Left Refl
instance KnownMode 'B where knownMode = Right Refl

-- | Which setting (A or B) I make should depend
-- on whether I choose A or B at compile-time.
makeSettings :: forall mode. KnownMode mode => IO (Settings mode)
makeSettings = do
  let x :: Settings mode = case knownMode @mode of
              Left Refl -> SettingsA 123
              Right Refl -> SettingsB "456"
  return x

main :: IO ()
main = do
  setA <- makeSettings @'A
  setB <- makeSettings @'B
  print setA
  print setB
  putStrLn "done."