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