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
|
{-# Language ViewPatterns, TypeOperators, KindSignatures, PolyKinds,
StandaloneDeriving, GADTs, RebindableSyntax,
RankNTypes, LambdaCase, PatternSynonyms, TypeApplications #-}
module T12698 where
import GHC.Types
import Prelude hiding ( fromInteger )
import Data.Type.Equality hiding ((:~~:)(..))
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
|
