blob: dccab5e43482b21abbe418ecd2160005ca798c4a (
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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
{-# LANGUAGE TypeFamilies, ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
module T10009 where
type family F a
type family UnF a
f :: (UnF (F b) ~ b) => F b -> ()
f = error "urk"
g :: forall a. (UnF (F a) ~ a) => a -> ()
g _ = f (undefined :: F a)
{- ---------------
[G] UnF (F b) ~ b
[W] UnF (F beta) ~ beta
[W] F a ~ F beta
-------------------
[G] g1: F a ~ fsk1 fsk1 := F a
[G] g2: UnF fsk1 ~ fsk2 fsk2 := UnF fsk1
[G] g3: fsk2 ~ a
[W] w1: F beta ~ fmv1
[W] w2: UnF fmv1 ~ fmv2
[W] w3: fmv2 ~ beta
[W] w5: fsk1 ~ fmv1 -- From F a ~ F beta
-- using flat-cache
---- No progress in solving -----
-- Unflatten:
[W] w3: UnF (F beta) ~ beta
[W] w5: fsk1 ~ F beta
--- Improvement
[D] F beta ~ fmv1
[D] UnF fmv1 ~ fmv2 -- (A)
[D] fmv2 ~ beta
[D] fmv1 ~ fsk1 -- (B) From F a ~ F beta
-- NB: put fmv on left
--> rewrite (A) with (B), and match with g2
[D] F beta ~ fmv1
[D] fmv2 ~ fsk2 -- (C)
[D] fmv2 ~ beta -- (D)
[D] fmv1 ~ fsk1
--> rewrite (D) with (C) and re-orient
[D] F beta ~ fmv1
[D] fmv2 ~ fsk2
[D] beta ~ fsk2 -- (E)
[D] fmv1 ~ fsk1
-- Now we can unify beta!
-}
{-
-----
Inert: [G] fsk_amA ~ b_amr
[G] UnF fsk_amy ~ fsk_amA
[G} F b_amr ~ fsk_amy
wl: [W] F b_amr ~ F b_amt
work item: [W] UnF (F b_amt) ~ b_amt
b_amt is the unification variable
===> b_amt := s_amF
Inert: [G] fsk_amA ~ b_amr
[G] UnF fsk_amy ~ fsk_amA
[G} F b_amr ~ fsk_amy
wl: [W] F b_amr ~ F b_amt
[W] UnF s_amD ~ s_amF
work item: [W] F b_amt ~ s_amD
===>
wl: [W] F b_amr ~ F b_amt
[W] UnF s_amD ~ s_amF
Inert: [G] fsk_amA ~ b_amr
[G] UnF fsk_amy ~ fsk_amA
[G} F b_amr ~ fsk_amy
[W] F s_amF ~ s_amD
===>
wl: [W] F b_amr ~ F b_amt
Inert: [G] fsk_amA ~ b_amr
[G] UnF fsk_amy ~ fsk_amA
[G} F b_amr ~ fsk_amy
[W] F s_amF ~ s_amD
[W] UnF s_amD ~ s_amF
===>
Inert: [G] fsk_amA ~ b_amr
[G] UnF fsk_amy ~ fsk_amA
[G} F b_amr ~ fsk_amy
[W] UnF s_amD ~ s_amF
[W] F s_amF ~ s_amD
wl:
work-item: [W] F b_amr ~ F b_amt
--> fsk_amy ~ s_amD
--> s_amD ~ fsk_amy
===>
Inert: [G] fsk_amA ~ b_amr
[G] UnF fsk_amy ~ fsk_amA
[G} F b_amr ~ fsk_amy
[W] UnF s_amD ~ s_amF
[W] F s_amF ~ s_amD
[W] s_amD ~ fsk_amy
wl:
work item: [D] UnF s_amD ~ s_amF
--> [D] UnF fsk_amy ~ s_amF
--> [D] s_amF ~ fsk_amA
===>
Inert: [G] fsk_amA ~ b_amr
[G] UnF fsk_amy ~ fsk_amA
[G} F b_amr ~ fsk_amy
[W] UnF s_amD ~ s_amF
[W] F s_amF ~ s_amD
[W] s_amD ~ fsk_amy
[D] s_amF ~ fsk_amA
wl:
work item: [D] F s_amF ~ s_amD
--> F fsk_amA ~ s_amD
--> s_amd ~ b_amr
-}
|
