{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -fplugin=IfSat.Plugin #-}
module M1 where
import Data.Kind
( Type )
import Data.Constraint.If
( IfSat, ifSat, IsSat )
showFun :: forall (a :: Type). IfSat ( Show ( a -> a ) ) => ( a -> a ) -> String
showFun :: forall a. IfSat (Show (a -> a)) => (a -> a) -> String
showFun = forall (ct :: Constraint) r.
IfSat ct =>
((IsSat ct ~ 'True, ct) => r) -> ((IsSat ct ~ 'False) => r) -> r
ifSat @( Show (a -> a) ) forall a. Show a => a -> String
show ( \ a -> a
_ -> String
"<<function>>" )
test1 :: ( Bool -> Bool ) -> String
test1 :: (Bool -> Bool) -> String
test1 Bool -> Bool
fun = forall a. IfSat (Show (a -> a)) => (a -> a) -> String
showFun Bool -> Bool
fun
class C
type F :: Bool -> Type
type family F b where
F False = Float
F True = String
foo :: Float -> F (IsSat C)
foo :: Float -> F (IsSat C)
foo Float
x = Float
x