diff options
Diffstat (limited to 'testsuite/tests')
-rw-r--r-- | testsuite/tests/patsyn/should_compile/T12698.hs | 62 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_compile/all.T | 1 |
2 files changed, 63 insertions, 0 deletions
diff --git a/testsuite/tests/patsyn/should_compile/T12698.hs b/testsuite/tests/patsyn/should_compile/T12698.hs new file mode 100644 index 0000000000..6ba45e4e85 --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T12698.hs @@ -0,0 +1,62 @@ +{-# Language ViewPatterns, TypeOperators, KindSignatures, PolyKinds, + TypeInType, StandaloneDeriving, GADTs, RebindableSyntax, + RankNTypes, LambdaCase, PatternSynonyms, TypeApplications #-} + +module T12698 where + +import GHC.Types +import Prelude hiding ( fromInteger ) +import Data.Type.Equality +import Data.Kind +import qualified Prelude + +class Ty (a :: k) where ty :: T a +instance Ty Int where ty = TI +instance Ty Bool where ty = TB +instance Ty a => Ty [a] where ty = TA TL ty +instance Ty [] where ty = TL +instance Ty (,) where ty = TP + +data AppResult (t :: k) where + App :: T a -> T b -> AppResult (a b) + +data T :: forall k. k -> Type where + TI :: T Int + TB :: T Bool + TL :: T [] + TP :: T (,) + TA :: T f -> T x -> T (f x) +deriving instance Show (T a) + +splitApp :: T a -> Maybe (AppResult a) +splitApp = \case + TI -> Nothing + TB -> Nothing + TL -> Nothing + TP -> Nothing + TA f x -> Just (App f x) + +data (a :: k1) :~~: (b :: k2) where + HRefl :: a :~~: a + +eqT :: T a -> T b -> Maybe (a :~~: b) +eqT a b = + case (a, b) of + (TI, TI) -> Just HRefl + (TB, TB) -> Just HRefl + (TL, TL) -> Just HRefl + (TP, TP) -> Just HRefl + +pattern List :: () => [] ~~ b => T b +pattern List <- (eqT (ty @(Type -> Type) @[]) -> Just HRefl) + where List = ty + +pattern Int :: () => Int ~~ b => T b +pattern Int <- (eqT (ty @Type @Int) -> Just HRefl) + where Int = ty + +pattern (:<->:) :: () => fx ~ f x => T f -> T x -> T fx +pattern f :<->: x <- (splitApp -> Just (App f x)) + where f :<->: x = TA f x + +pattern Foo <- List :<->: Int diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index d26fc84bec..4426c74733 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -60,3 +60,4 @@ test('T12108', normal, compile, ['']) test('T12484', normal, compile, ['']) test('T11987', normal, multimod_compile, ['T11987', '-v0']) test('T12615', normal, compile, ['']) +test('T12698', normal, compile, ['']) |