@@ -54,15 +54,6 @@ type family Change (t :: k) (target :: Nat) (to :: j) :: k where
5454 Change (t a :: k) target to = Change t target to a
5555 Change t _ _ = t
5656
57−-- TODO: document this
58−data Skolem
59−
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
64− Generalise t _ = t
65−
6657type family UnApply (a :: k) :: [*] where
6758 UnApply (f x) = x ': UnApply f
6859 UnApply x = '[]
@@ -80,17 +71,13 @@ type family Zip (xs :: [k]) (ys :: [l]) :: [(k, l)] where
8071 Zip '[] '[] = '[]
8172 Zip (x ': xs) (y ': ys) = '(x, y) ': Zip xs ys
8273
83−type family IfEq a b t f where
84− IfEq a a t _ = t
85− IfEq _ _ _ f = f
86−
8774type family Infer (s :: *) (a' :: *) (a :: *) (w :: *) :: (*, *) where
8875 Infer s' a' a w
8976 = Infer' s' a' (PSub (Unify a' a)) w
9077
9178type family Infer' (s :: *) (a' :: *) (subs :: [(Nat, k)]) w :: (*, *) where
9279 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))
9481 Infer' s' a' _ _
9582 = '(UnProxied s', UnProxied a')
9683