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 AllowAmbiguousTypes, TypeFamilies #-}
module ContextStack2 where
import Data.Kind (Type)
type family TF a :: Type
type instance TF (a,b) = (TF a, TF b)
-- Succeeds with new approach to fuvs
-- Aug 2016
t :: (a ~ TF (a,Int)) => Int
t = undefined
{- a ~ TF (a,Int)
~ (TF a, TF Int)
~ (TF (TF (a,Int)), TF Int)
~ (TF (TF a, TF Int), TF Int)
~ ((TF (TF a), TF (TF Int)), TF Int)
fsk ~ a
TF (a, Int) ~ fsk
-->
fsk ~ a
* fsk ~ (TF a, TF Int)
(flatten lhs)
a ~ (TF a, TF Int)
(flatten rhs)
a ~ (fsk1, TF Int)
(wk) TF a ~ fsk1
--> (rewrite inert)
fsk ~ (fsk1, TF Int)
a ~ (fsk1, TF Int)
(wk) TF a ~ fsk1
-->
fsk ~ (fsk1, TF Int)
a ~ (fsk1, TF Int)
* TF (fsk1, fsk2) ~ fsk1
(wk) TF Tnt ~ fsk2
-->
fsk ~ (fsk1, TF Int)
a ~ (fsk1, TF Int)
* fsk1 ~ (TF fsk1, TF fsk2)
(flatten rhs)
fsk1 ~ (fsk3, TF fsk2)
(wk) TF Int ~ fsk2
TF fsk1 ~ fsk3
-}
|
