Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / dependent / should_compile / T11711.hs
1 {-# LANGUAGE PatternSynonyms #-}
2 {-# LANGUAGE GADTs #-}
3 {-# LANGUAGE RankNTypes #-}
4 {-# LANGUAGE TypeOperators #-}
5 {-# LANGUAGE KindSignatures #-}
6 {-# LANGUAGE PolyKinds #-}
7 {-# LANGUAGE ViewPatterns #-}
8 {-# LANGUAGE TypeSynonymInstances #-}
9 {-# LANGUAGE FlexibleInstances #-}
10
11 module T11711 where
12
13 import Data.Kind (Type)
14
15 data (:~~:) (a :: k1) (b :: k2) where
16 HRefl :: a :~~: a
17
18 data TypeRep (a :: k) where
19 TrTyCon :: String -> TypeRep k -> TypeRep (a :: k)
20 TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
21 TypeRep (a :: k1 -> k2)
22 -> TypeRep (b :: k1)
23 -> TypeRep (a b)
24
25 class Typeable (a :: k) where
26 typeRep :: TypeRep a
27
28 data SomeTypeRep where
29 SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep
30
31 eqTypeRep :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
32 eqTypeRep = undefined
33
34 typeRepKind :: forall k (a :: k). TypeRep a -> TypeRep k
35 typeRepKind = undefined
36
37 instance Typeable Type where
38 typeRep = TrTyCon "Type" typeRep
39
40 funResultTy :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
41 funResultTy (SomeTypeRep f) (SomeTypeRep x)
42 | Just HRefl <- (typeRep :: TypeRep Type) `eqTypeRep` typeRepKind f
43 , TRFun arg res <- f
44 , Just HRefl <- arg `eqTypeRep` x
45 = Just (SomeTypeRep res)
46 | otherwise
47 = Nothing
48
49 trArrow :: TypeRep (->)
50 trArrow = undefined
51
52 pattern TRFun :: forall fun. ()
53 => forall arg res. (fun ~ (arg -> res))
54 => TypeRep arg
55 -> TypeRep res
56 -> TypeRep fun
57 pattern TRFun arg res <- TrApp (TrApp (eqTypeRep trArrow -> Just HRefl) arg) res