Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / patsyn / should_compile / T12698.hs
1 {-# Language ViewPatterns, TypeOperators, KindSignatures, PolyKinds,
2 StandaloneDeriving, GADTs, RebindableSyntax,
3 RankNTypes, LambdaCase, PatternSynonyms, TypeApplications #-}
4
5 module T12698 where
6
7 import GHC.Types
8 import Prelude hiding ( fromInteger )
9 import Data.Type.Equality hiding ((:~~:)(..))
10 import Data.Kind
11 import qualified Prelude
12
13 class Ty (a :: k) where ty :: T a
14 instance Ty Int where ty = TI
15 instance Ty Bool where ty = TB
16 instance Ty a => Ty [a] where ty = TA TL ty
17 instance Ty [] where ty = TL
18 instance Ty (,) where ty = TP
19
20 data AppResult (t :: k) where
21 App :: T a -> T b -> AppResult (a b)
22
23 data T :: forall k. k -> Type where
24 TI :: T Int
25 TB :: T Bool
26 TL :: T []
27 TP :: T (,)
28 TA :: T f -> T x -> T (f x)
29 deriving instance Show (T a)
30
31 splitApp :: T a -> Maybe (AppResult a)
32 splitApp = \case
33 TI -> Nothing
34 TB -> Nothing
35 TL -> Nothing
36 TP -> Nothing
37 TA f x -> Just (App f x)
38
39 data (a :: k1) :~~: (b :: k2) where
40 HRefl :: a :~~: a
41
42 eqT :: T a -> T b -> Maybe (a :~~: b)
43 eqT a b =
44 case (a, b) of
45 (TI, TI) -> Just HRefl
46 (TB, TB) -> Just HRefl
47 (TL, TL) -> Just HRefl
48 (TP, TP) -> Just HRefl
49
50 pattern List :: () => [] ~~ b => T b
51 pattern List <- (eqT (ty @(Type -> Type) @[]) -> Just HRefl)
52 where List = ty
53
54 pattern Int :: () => Int ~~ b => T b
55 pattern Int <- (eqT (ty @Type @Int) -> Just HRefl)
56 where Int = ty
57
58 pattern (:<->:) :: () => fx ~ f x => T f -> T x -> T fx
59 pattern f :<->: x <- (splitApp -> Just (App f x))
60 where f :<->: x = TA f x
61
62 pattern Foo <- List :<->: Int