@@ -112,16 +112,24 @@ close (Predicate f) =
112112 close' :: Scheme -> Eff '[State Int, Reader Int, State TDeBrujinMap] Scheme
113113 close' x@(NAtomic _) = return x
114114 close' (preds :=> t) =
115− (:=>) <$> (closePred `traverse` preds) <*> case t of
116− x@(NBrujin _) -> return x
117− (NTypeVariable tv) | f tv -> NBrujin <$> newbrujin tv
118− x@(NTypeVariable _) -> return x
119− (x :-> y) -> bndCtx $ (:->) <$> close' x <*> close' y
120− (List x) -> bndCtx $ List <$> close' x
121− (NAttrSet x) -> bndCtx $ NAttrSet <$> traverse close' x
115+ (:=>) <$> (Preds <$> closePred `traverse` unPreds preds) <*> closeType t
116+
117+ closeType :: NType -> Eff '[State Int, Reader Int, State TDeBrujinMap] NType
118+ closeType = \case
119+ x@(NBrujin _) -> return x
120+ (NTypeVariable tv) | f tv -> NBrujin <$> newbrujin tv
121+ x@(NTypeVariable _) -> return x
122+ (x :-> y) -> bndCtx $ (:->) <$> close' x <*> close' y
123+ (List x) -> bndCtx $ List <$> close' x
124+ (NAttrSet x) -> bndCtx $ NAttrSet <$> traverse close' x
122125
123126 closePred :: Pred -> Eff '[State Int, Reader Int, State TDeBrujinMap] Pred
124127 closePred = \case
128+ (Update x y z) -> bndCtx $ Update <$> closeType x <*> closeType y <*> closeType z
129+ (HasField t (k, v)) -> bndCtx $ do
130+ t' <- closeType t
131+ v' <- close' v
132+ return $ HasField t' (k, v')
125133
126134 bndCtx m = do
127135 modify @TDeBrujinMap (SM.shift 1)
@@ -157,11 +165,25 @@ instance Free NType where
157165 NAttrSet m -> NAttrSet $ sub s <$> m
158166 x :-> y -> sub s x :-> sub s y
159167
160−instance Free Pred where
161− free (Update x y z) = free x <> free y <> free z
162− free (x `HasField` (_, y)) = free x <> free y
163− sub s (Update x y z) = Update (sub s x) (sub s y) (sub s z)
164− sub s (x `HasField` (t, y)) = sub s x `HasField` (t, sub s y)
168+instance Free Preds where
169+ free (Preds ps) = flip foldMap ps $ \case
170+ Update x y z -> free x <> free y <> free z
171+ x `HasField` (_, y) -> free x <> free y
172+ sub s (Preds ps) =
173+ Preds $
174+ ps >>= \case
175+ Update x y z ->
176+ let (a, x') = sub' x
177+ (b, y') = sub' y
178+ (c, z') = sub' z
179+ in Update x' y' z' : unPreds (a <> b <> c)
180+ HasField t (f, v) ->
181+ let (a, t') = sub' t
182+ in HasField t' (f, sub s v) : unPreds a
183+ where
184+ sub' t = case sub s (scheme t) of
185+ pp :=> t' -> (pp, t')
186+ NAtomic _ -> error "can not be atomic" -- this should not be an 'error'
165187
166188instance Free Scheme where
167189 free (x :=> y) = free x <> free y
@@ -170,7 +192,7 @@ instance Free Scheme where
170192 case M.lookup tv $ unSubstitution s of
171193 Nothing -> sub s x :=> NTypeVariable tv
172194 Just (newCs :=> new) -> (sub s x <> newCs) :=> new
173− Just a@(NAtomic _) -> assert (null x) a
195+ Just a@(NAtomic _) -> assert (null . unPreds $ x) a
174196 sub s (x :=> y) = sub s x :=> sub s y
175197 sub _ x@(NAtomic _) = x
176198
@@ -221,30 +243,38 @@ unifyWithPriority range (lhs :~ rhs) =
221243 case (lhs, rhs) of
222244 (NAtomic x, NAtomic y) | x == y -> return mempty
223245 (xcs :=> NTypeVariable x, ycs :=> NTypeVariable y) -> do
224− let ((_lhsCs, lhs'), (rhsCs, rhs')) =
246+ let ((lhsCs, lhs'), (rhsCs, rhs')) =
225247 if y `RS.member` range
226248 then ((ycs, y), (xcs, x))
227249 else ((xcs, x), (ycs, y))
228− lhs' <<- (rhsCs :=> NTypeVariable rhs') -- This might be wrong
229− (_ :=> NTypeVariable t, x) -> t <<- x
230− (x, _ :=> NTypeVariable t) -> t <<- x
250+ extraCs = replacing lhs' (scheme . NTypeVariable $ rhs') lhsCs
251+ newScheme = (extraCs <> rhsCs) :=> NTypeVariable rhs'
252+ -- This might come back to bite me.
253+ (<> (Substitution $ M.singleton rhs' newScheme)) <$> (lhs' <<- newScheme)
254+ (cs :=> NTypeVariable t, x) -> t <<- (replacing t x cs =>> x)
255+ (x, cs :=> NTypeVariable t) -> t <<- (replacing t x cs =>> x)
231256 (xcs :=> List x, ycs :=> List y) ->
232257 unifyWithPriority range $ (xcs =>> x) :~ (ycs =>> y)
233− (_xcs :=> NAttrSet x, _ycs :=> NAttrSet y) ->
258+ (Preds xcs :=> NAttrSet x, Preds ycs :=> NAttrSet y) ->
234259 -- TODO: what to do with predicates ?
235− foldr (\c s -> s >>= \s' -> (<> s') <$> unifyWithPriority range (sub s' c)) (pure mempty)
236− . M.elems
237− $ M.intersectionWith (:~) x y
238− (xcs :=> (x1 :-> y1), ycs :=> (x2 :-> y2)) -> do
260+ -- I don't think there should be any predicates here...
261+ assert (null xcs && null ycs) $
262+ foldr (\c s -> s >>= \s' -> (<> s') <$> unifyWithPriority range (sub s' c)) (pure mempty)
263+ . M.elems
264+ $ M.intersectionWith (:~) x y
265+ (Preds xcs :=> (x1 :-> y1), Preds ycs :=> (x2 :-> y2)) -> do
239266 s <- unifyWithPriority range (x1 :~ x2)
240267 s' <- unifyWithPriority range $ sub s $ y1 :~ y2
241268 let ss = s' <> s
242− s'' <- uncurry unifyPred . sub ss $ (xcs, ycs)
243− return $ s'' <> ss
269+ -- I don't think there should be any predicates here either...
270+ -- s'' <- uncurry unifyPred . sub ss $ (xcs, ycs)
271+ assert (null xcs && null ycs) $ return ss
244272 (x, y) -> tell (CanNotUnify x y) >> return mempty
245273
246−unifyPred :: [Pred] -> [Pred] -> UnifyM Substitution
247−unifyPred _xs _ys = pure mempty
274+replacing :: Free x => TypeVariable -> Scheme -> x -> x
275+replacing tv t x =
276+ let s = Substitution $ M.singleton tv t
277+ in sub s x
248278
249279solve :: Seq Constraint -> UnifyM Substitution
250280solve = solveWithPriority RS.empty
@@ -353,7 +383,8 @@ instantiate ::
353383instantiate = evalState M.empty . instantiateScheme
354384 where
355385 instantiateScheme :: forall. Scheme -> Eff (State (Map DeBrujin TypeVariable) ': effs) Scheme
356− instantiateScheme (ps :=> t) = (:=>) <$> traverse instantiatePred ps <*> instantiate' t
386+ instantiateScheme (ps :=> t) =
387+ (:=>) <$> (Preds <$> traverse instantiatePred (unPreds ps)) <*> instantiate' t
357388 instantiateScheme x@(NAtomic _) = return x
358389
359390 instantiatePred :: forall. Pred -> Eff (State (Map DeBrujin TypeVariable) ': effs) Pred
@@ -604,24 +635,25 @@ inferGeneral x = traceSubtree (showExpr x) $ do
604635 traceValue "type" $ renderPretty retT
605636 return retT
606637
607−solveConstraints :: [Pred] -> InferM [Pred]
608−solveConstraints ps = do
609− flip Control.Monad.filterM ps $ \case
610− HasField (NAttrSet ts) (f, t) -> case M.lookup f ts of
611− Nothing -> do
612− tell $ KeyNotPresent f (NAttrSet ts)
638+solveConstraints :: Preds -> InferM Preds
639+solveConstraints (Preds ps) =
640+ Preds <$> do
641+ flip Control.Monad.filterM ps $ \case
642+ HasField (NAttrSet ts) (f, t) -> case M.lookup f ts of
643+ Nothing -> do
644+ tell $ KeyNotPresent f (NAttrSet ts)
645+ return False
646+ Just t' -> do
647+ t ~~ t'
648+ return False
649+ HasField (NTypeVariable _) _ -> return True
650+ HasField t _ -> do
651+ tell $ NotAnAttributeSet t
613652 return False
614− Just t' -> do
615− t ~~ t'
653+ (Update (NAttrSet a) (NAttrSet b) t) -> do
654+ scheme (NAttrSet $ b <> a) ~~ scheme t
616655 return False
617− HasField (NTypeVariable _) _ -> return True
618− HasField t _ -> do
619− tell $ NotAnAttributeSet t
620− return False
621− (Update (NAttrSet a) (NAttrSet b) t) -> do
622− scheme (NAttrSet $ b <> a) ~~ scheme t
623− return False
624− _ -> return True
656+ _ -> return True
625657
626658-- | Stacks functions recursively inside each other
627659-- >>> stack [f1, f2, f3] h x