diff options
Diffstat (limited to 'testsuite/tests/saks/should_compile/saks030.hs')
-rw-r--r-- | testsuite/tests/saks/should_compile/saks030.hs | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/testsuite/tests/saks/should_compile/saks030.hs b/testsuite/tests/saks/should_compile/saks030.hs new file mode 100644 index 0000000000..93e414fbed --- /dev/null +++ b/testsuite/tests/saks/should_compile/saks030.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE PolyKinds, DataKinds, RankNTypes, TypeFamilies, + TypeApplications, TypeOperators, GADTs #-} + +module SAKS_030 where + +import Data.Kind +import Data.Type.Equality + +type T1 :: forall k (a :: k). Bool +type T2 :: k -> Bool + +type family T1 where + T1 @Bool @True = False + T1 @Bool @False = True + +type family T2 a where + T2 True = False + T2 False = True + +type SBool :: Bool -> Type +data SBool b where + STrue :: SBool True + SFalse :: SBool False + +proof_t1_eq_t2 :: SBool b -> T1 @Bool @b :~: T2 b +proof_t1_eq_t2 STrue = Refl +proof_t1_eq_t2 SFalse = Refl |