MkIf.hs

{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy
import Data.Type.Bool
import Data.Kind

type family IsJust t where
    IsJust ('Just _) = 'True
    IsJust _         = 'False

type family FromJust t where
    FromJust ('Just v) = v

type family IsOk (t :: SubDevMode) where
    IsOk ('SubDevMode v) = v

type family ToMaybe (t :: k) :: Maybe SubDevMode where
    ToMaybe ()         = 'Nothing
    ToMaybe (SubDev v) = 'Just v

class MkIf (t :: Bool) where
    mkIf :: Proxy t -> m a -> m b -> m (If t a b)

instance MkIf 'True where
    mkIf _ eval _ = eval

instance MkIf 'False where
    mkIf _ _ eval = eval

data SubDevMode = SubDevMode Bool                                                                                                                                                                                             
    deriving Show                                                                                                                                                                                                             
                                                                                                                                                                                                                              
data SubDev (mode :: SubDevMode) = SubDev                                                                                                                                                                                     
    deriving Show                                                                                                                                                                                                             
                                                                                                                                                                                                                              
data Dev maybeMode                                                                                                                                                                                                            
    = Dev { subDev :: If (IsJust maybeMode) (SubDev (FromJust maybeMode)) () }                                                                                                                                                
                                                                                                                                                                                                                              
deriving instance Show (If (IsJust maybeMode) (SubDev (FromJust maybeMode)) ()) => Show (Dev maybeMode)                                                                                                                       
                                                                                                                                                                                                                              
nope :: IO ()                                                                                                                                                                                                                 
nope = pure ()                                                                                                                                                                                                                
                                                                                                                                                                                                                              
mkSubDev :: IsOk mode ~ 'True => IO (SubDev mode)                                                                                                                                                                             
mkSubDev = pure SubDev                                                                                                                                                                                                        
                                                                                                                                                                                                                              
mkDev                                                                                                                                                                                                                         
    :: If (IsJust (ToMaybe a)) (SubDev (FromJust (ToMaybe a))) () ~ a                                                                                                                                                         
    => IO a -> IO (Dev (ToMaybe a))                                                                                                                                                                                           
mkDev p = do                                                                                                                                                                                                                  
    s <- p                                                                                                                                                                                                                    
    pure Dev { subDev = s }