Singletonesia.hs

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE GADTs          #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase     #-}
{-# LANGUAGE PolyKinds      #-}
{-# LANGUAGE RankNTypes     #-}
{-# LANGUAGE TypeFamilies   #-}

import           GHC.Exts

data Platform = Posix | Win
data Base = Abs | Rel
data Type = Dir | File

data Path (p :: Platform) (b :: Base) (t :: Type) where
    PosixAbsDir :: String -> Path 'Posix 'Abs 'Dir
    PosixAbsFile :: String -> Path 'Posix 'Abs 'File
    PosixRelDir :: String -> Path 'Posix 'Rel 'Dir
    PosixRelFile :: String -> Path 'Posix 'Rel 'File
    WinAbsDir :: String -> Path 'Win 'Abs 'Dir
    WinAbsFile :: String -> Path 'Win 'Abs 'File
    WinRelDir :: String -> Path 'Win 'Rel 'Dir
    WinRelFile :: String -> Path 'Win 'Rel 'File

data family Sing (x :: k)

data instance Sing (m :: Maybe a) where
    SNothing :: Sing Nothing
    SJust    :: Sing a -> Sing (Just a)

data instance Sing (p :: Platform) where
    SPosix :: Sing Posix
    SWin   :: Sing Win

data instance Sing (b :: Base) where
    SAbs :: Sing Abs
    SRel :: Sing Rel

data instance Sing (t :: Type) where
    SDir  :: Sing Dir
    SFile :: Sing File

type family DetBy (mx :: Maybe a) (x :: a) :: Constraint where
    DetBy Nothing  x = ()
    DetBy (Just y) x = x ~ y

mk
    :: Monad m
    => Sing (mp :: Maybe Platform)
    -> Sing (mb :: Maybe Base)
    -> Sing (mt :: Maybe Type)
    -> String
    -> (forall p b t. (DetBy mp p, DetBy mb b, DetBy mt t) => Path p b t -> m r)
    -> m r
mk _ _ _ _ _ = undefined

test :: IO ()
test = mk (SJust SPosix) SNothing (SJust SFile) undefined $ \case
    PosixRelFile fp -> undefined
    PosixAbsFile fp -> undefined
    -- -- both the lines give an inaccessible code warning.
    -- PosixRelDir  fp -> undefined
    -- WinAbsFile   fp -> undefined