blob: cf8c238efe42f978062c371ba6623c8bd0548693 (
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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
module T14270 (pattern App) where
import Data.Kind (Type, Constraint)
import GHC.Fingerprint (Fingerprint, fingerprintFingerprints)
import GHC.Types (RuntimeRep, TYPE, TyCon)
type (:~~:) :: k1 -> k2 -> Type
data a :~~: b where
HRefl :: a :~~: a
type TypeRep :: k -> Type
data TypeRep a where
TrTyCon :: {-# UNPACK #-} !Fingerprint -> !TyCon -> [SomeTypeRep]
-> TypeRep (a :: k)
TrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
{-# UNPACK #-} !Fingerprint
-> TypeRep (a :: k1 -> k2)
-> TypeRep (b :: k1)
-> TypeRep (a b)
TrFun :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2).
{-# UNPACK #-} !Fingerprint
-> TypeRep a
-> TypeRep b
-> TypeRep (a -> b)
data SomeTypeRep where
SomeTypeRep :: forall k (a :: k). !(TypeRep a) -> SomeTypeRep
typeRepFingerprint :: TypeRep a -> Fingerprint
typeRepFingerprint = undefined
mkTrApp :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
TypeRep (a :: k1 -> k2)
-> TypeRep (b :: k1)
-> TypeRep (a b)
mkTrApp rep@(TrApp _ (TrTyCon _ con _) (x :: TypeRep x)) (y :: TypeRep y)
| con == funTyCon -- cheap check first
, Just (IsTYPE (rx :: TypeRep rx)) <- isTYPE (typeRepKind x)
, Just (IsTYPE (ry :: TypeRep ry)) <- isTYPE (typeRepKind y)
, Just HRefl <- withTypeable x $ withTypeable rx $ withTypeable ry
$ typeRep @((->) x :: TYPE ry -> Type) `eqTypeRep` rep
= undefined
mkTrApp a b = TrApp fpr a b
where
fpr_a = typeRepFingerprint a
fpr_b = typeRepFingerprint b
fpr = fingerprintFingerprints [fpr_a, fpr_b]
pattern App :: forall k2 (t :: k2). ()
=> forall k1 (a :: k1 -> k2) (b :: k1). (t ~ a b)
=> TypeRep a -> TypeRep b -> TypeRep t
pattern App f x <- (splitApp -> Just (IsApp f x))
where App f x = mkTrApp f x
type IsApp :: k -> Type
data IsApp a where
IsApp :: forall k k' (f :: k' -> k) (x :: k'). ()
=> TypeRep f -> TypeRep x -> IsApp (f x)
splitApp :: forall k (a :: k). ()
=> TypeRep a
-> Maybe (IsApp a)
splitApp (TrApp _ f x) = Just (IsApp f x)
splitApp rep@(TrFun _ a b) = Just (IsApp (mkTrApp arr a) b)
where arr = bareArrow rep
splitApp (TrTyCon{}) = Nothing
withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
withTypeable _ _ = undefined
eqTypeRep :: forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep = undefined
typeRepKind :: TypeRep (a :: k) -> TypeRep k
typeRepKind = undefined
bareArrow :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(a :: TYPE r1) (b :: TYPE r2). ()
=> TypeRep (a -> b)
-> TypeRep ((->) :: TYPE r1 -> TYPE r2 -> Type)
bareArrow = undefined
type IsTYPE :: Type -> Type
data IsTYPE a where
IsTYPE :: forall (r :: RuntimeRep). TypeRep r -> IsTYPE (TYPE r)
isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a)
isTYPE = undefined
type Typeable :: k -> Constraint
class Typeable a where
typeRep :: Typeable a => TypeRep a
typeRep = undefined
funTyCon :: TyCon
funTyCon = undefined
instance (Typeable f, Typeable a) => Typeable (f a)
instance Typeable ((->) :: TYPE r -> TYPE s -> Type)
instance Typeable TYPE
|
