@@ -54,15 +54,6 @@ type family Change (t :: k) (target :: Nat) (to :: j) :: k where
54 Change (t a :: k) target to = Change t target to a
54 Change (t a :: k) target to = Change t target to a
55 Change t _ _ = t
55 Change t _ _ = t
57−-- TODO: document this
60−type family Generalise (t :: k) (w :: *) :: k where
61− Generalise Skolem w = w
62− Generalise (t Skolem :: k) w = t w
63− Generalise (t a) w = (Generalise t w) a
66type family UnApply (a :: k) :: [*] where
57type family UnApply (a :: k) :: [*] where
67 UnApply (f x) = x ': UnApply f
58 UnApply (f x) = x ': UnApply f
68 UnApply x = '[]
59 UnApply x = '[]
@@ -80,17 +71,13 @@ type family Zip (xs :: [k]) (ys :: [l]) :: [(k, l)] where
80 Zip '[] '[] = '[]
71 Zip '[] '[] = '[]
81 Zip (x ': xs) (y ': ys) = '(x, y) ': Zip xs ys
72 Zip (x ': xs) (y ': ys) = '(x, y) ': Zip xs ys
83−type family IfEq a b t f where
87type family Infer (s :: *) (a' :: *) (a :: *) (w :: *) :: (*, *) where
74type family Infer (s :: *) (a' :: *) (a :: *) (w :: *) :: (*, *) where
88 Infer s' a' a w
75 Infer s' a' a w
89 = Infer' s' a' (PSub (Unify a' a)) w
76 = Infer' s' a' (PSub (Unify a' a)) w
91type family Infer' (s :: *) (a' :: *) (subs :: [(Nat, k)]) w :: (*, *) where
78type family Infer' (s :: *) (a' :: *) (subs :: [(Nat, k)]) w :: (*, *) where
92 Infer' s' a' '[ '(p, _)] w
79 Infer' s' a' '[ '(p, _)] w
93− = '(Generalise (UnProxied (Change s' p Skolem)) w, Generalise (UnProxied (Change a' p Skolem)) w)
80+ = '(UnProxied (Change s' p w), UnProxied (Change a' p w))
94 Infer' s' a' _ _
81 Infer' s' a' _ _
95 = '(UnProxied s', UnProxied a')
82 = '(UnProxied s', UnProxied a')