@@ -56,13 +56,13 @@ import Prelude as P
5656
5757getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [InferError], [UnifyingError], [PredicateError], A.Object)
5858getType r =
59− let ((((((((t, traceTree), inf), predicate), unifying), errs), _srcs), subs), _) =
59+ let ((((((t, traceTree), inf), predicate), unifying), errs), _srcs) =
6060 run
6161 . runReader nullSpan
6262 . evalState @(MKM.Map Pred) mempty
6363 . interpret @(Writer Pred) (\(Tell x) -> modify (<> MKM.singleton x))
6464 . evalState (M.empty :: VariableMap)
65− . runConstraintEnv
65+ . evalState @Substitution mempty
6666 . runState @[(TypeVariable, SrcSpan)] []
6767 . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))
6868 . runSeqWriter @[(SrcSpan, Errors)]
@@ -72,31 +72,7 @@ getType r =
7272 . runFreshSrc
7373 . runTreeTracer
7474 $ inferGeneral r
75− in (sub subs t, errs, inf, unifying, predicate, traceTree)
76−
77−runConstraintEnv ::
78− Members '[State VariableMap, State (MKM.Map Pred)] effs =>
79− Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : effs) a ->
80− Eff effs ((a, Substitution), Seq Constraint)
81−runConstraintEnv f = do
82− ((x, subs), cs) <-
83− runState @(Seq Constraint) Empty
84− . interpret @(Writer Constraint) (\(Tell x) -> modify (x :<|))
85− . runWriter @Substitution
86− . interpret @SubstituteEnv
87− ( \(SubstituteEnv x) -> do
88− -- modify @(Seq Constraint) (sub x <$>)
89− -- TODone: I have a feeling that variables in the env should already be closed over.
90− -- (aka this is redundant)
91− --
92− -- No, they can have type variables. E g when they are arguments in a function.
93− modify @VariableMap (sub x <$>)
94− modify @(MKM.Map Pred) (sub x)
95− tell x
96− return ()
97− )
98− $ f
99− return ((x, subs), sub subs <$> cs)
75+ in (t, errs, inf, unifying, predicate, traceTree)
10076
10177runFreshSrc ::
10278 Members '[Reader SrcSpan, Writer (TypeVariable, SrcSpan)] eff =>
@@ -113,27 +89,6 @@ runFreshSrc =
11389 MinFreshFromNow -> send MinFreshFromNow
11490 )
11591
116−captureSubstitutions ::
117− Members '[SubstituteEnv] effs =>
118− Eff (Writer Substitution : effs) a ->
119− Eff effs (a, Substitution)
120−captureSubstitutions f = do
121− (x, s) <-
122− runWriter @Substitution
123− . interpose @SubstituteEnv
124− ( \(SubstituteEnv x) -> do
125− tell x
126− subEnv x
127− )
128− $ f
129− return (x, s)
130−
131−data SubstituteEnv a where
132− SubstituteEnv :: Substitution -> SubstituteEnv ()
133−
134−subEnv :: Member SubstituteEnv r => Substitution -> Eff r ()
135−subEnv = send . SubstituteEnv
136−
13792data Constraint = !NType :~ !NType
13893 deriving stock (Eq, Ord, Show)
13994
@@ -178,6 +133,10 @@ instance Free a => Free [a] where
178133 free = foldMap free
179134 sub s = fmap (sub s)
180135
136+instance Free a => Free (Seq a) where
137+ free = foldMap free
138+ sub s = fmap (sub s)
139+
181140instance Free Substitution where
182141 free (Substitution s) = free . M.elems $ s
183142 sub new old = old <> new
@@ -200,7 +159,6 @@ newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
200159prettySubstitution :: Substitution -> A.Value
201160prettySubstitution = A.toJSON . M.mapKeysMonotonic (TL.pack . show) . fmap renderPretty . unSubstitution
202161
203−-- | @older <> newer@
204162instance Semigroup Substitution where
205163 x'@(Substitution x) <> y'@(Substitution y) = Substitution (M.unionWithKey (error "invariant") (fmap (sub y') x) (fmap (sub x') y))
206164
@@ -214,22 +172,23 @@ instance Free Constraint where
214172(<<-) ::
215173 TypeVariable ->
216174 NType ->
217− UnifyM Substitution
218−v <<- (NTypeVariable x) | v == x = return mempty
175+ UnifyM ()
176+v <<- (NTypeVariable x) | v == x = pure ()
219177v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty
220178 where
221179 occursIn :: Free x => TypeVariable -> x -> Bool
222180 occursIn t u = t `S.member` free u
223−v <<- x = return $ Substitution $ M.singleton v x
181+v <<- x = modify (Substitution (M.singleton v x) <>)
224182
225183unifyWithPriority ::
226184 -- | The range of type variables to interpret as being lower
227185 -- priority (try to replace them if possible)
228186 RS.RSet TypeVariable ->
229187 Constraint ->
230− UnifyM Substitution
231−unifyWithPriority range (lhs :~ rhs) =
232− case (lhs, rhs) of
188+ UnifyM ()
189+unifyWithPriority range (lhs :~ rhs) = do
190+ s <- get
191+ case sub s (lhs, rhs) of
233192 (x, y) | x == y -> return mempty
234193 (NTypeVariable x, NTypeVariable y) -> do
235194 if y `RS.member` range
@@ -242,30 +201,29 @@ unifyWithPriority range (lhs :~ rhs) =
242201 assertSetsMatch (tell . KeysDontMatch) (M.keysSet x) (M.keysSet y)
243202 unifySchemes range . M.elems $ M.intersectionWith (,) x y
244203 (x1 :-> y1, x2 :-> y2) -> do
245− s <- unifyWithPriority range (x1 :~ x2)
246− s' <- unifyWithPriority range $ sub s $ y1 :~ y2
247− return $ s' <> s
248− (x, y) -> tell (CanNotUnify x y) >> return mempty
204+ unifyWithPriority range (x1 :~ x2)
205+ unifyWithPriority range $ y1 :~ y2
206+ (x, y) -> tell (CanNotUnify x y)
249207
250−unifySchemes :: RS.RSet TypeVariable -> [(Scheme, Scheme)] -> UnifyM Substitution
208+unifySchemes :: RS.RSet TypeVariable -> [(Scheme, Scheme)] -> UnifyM ()
251209unifySchemes _ [] = pure mempty
252210unifySchemes range ((x, y) : rest) = do
253− s <- unifyScheme range x y
254− sub s <$> unifySchemes range (sub s rest)
211+ unifyScheme range x y
212+ unifySchemes range rest
255213
256−unifyScheme :: RS.RSet TypeVariable -> Scheme -> Scheme -> UnifyM Substitution
214+unifyScheme :: RS.RSet TypeVariable -> Scheme -> Scheme -> UnifyM ()
257215unifyScheme range (xs :=> x) (ys :=> y) = do
258− s <- solveWithPriority range (pure (x :~ y))
216+ solveWithPriority range (pure (x :~ y))
217+ s <- get
259218 let f = S.fromList . sub s
260219 assertSetsMatch (tell . ConstraintsDontMatch) (f xs) (f ys)
261− return s
262220
263221assertSetsMatch :: Ord x => Applicative f => (Set x -> f ()) -> Set x -> Set x -> f ()
264222assertSetsMatch f x y = case (x S.\\ y, y S.\\ x) of
265223 (a, b) | S.null a, S.null b -> pure ()
266224 (a, b) -> f $ a <> b
267225
268−solve :: Seq Constraint -> UnifyM Substitution
226+solve :: Seq Constraint -> UnifyM ()
269227solve = solveWithPriority mempty
270228
271229solveWithPriority ::
@@ -273,11 +231,11 @@ solveWithPriority ::
273231 -- priority (try to replace them if possible)
274232 RS.RSet TypeVariable ->
275233 Seq Constraint ->
276− UnifyM Substitution
234+ UnifyM ()
277235solveWithPriority _ Empty = return mempty
278236solveWithPriority range (rest :|> c) = do
279− s <- unifyWithPriority range c
280− sub s <$> solveWithPriority range (fmap (sub s) rest)
237+ unifyWithPriority range c
238+ solveWithPriority range rest
281239
282240data Errors
283241 = UndefinedVariable VarName
@@ -300,12 +258,11 @@ data InferError
300258 = ConflictingBindingDefinitions (NormalizedBinding' NExprLoc) (NormalizedBinding' NExprLoc)
301259 deriving stock (Show)
302260
303−type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x
261+type UnifyM x = forall r. Members '[Writer UnifyingError, State Substitution] r => Eff r x
304262
305263type InferEffs =
306264 '[ Fresh,
307265 Reader SrcSpan,
308− Writer Constraint,
309266 Writer (SrcSpan, Errors),
310267 Writer PredicateError,
311268 Writer Pred,
@@ -313,12 +270,14 @@ type InferEffs =
313270 State VariableMap,
314271 Writer UnifyingError,
315272 Writer InferError,
316− SubstituteEnv,
273+ State Substitution,
317274 TreeTracer
318275 ]
319276
320277type InferM x = forall r. Members InferEffs r => Eff r x
321278
279+type InferM' x = forall r. Members (Writer Constraint : InferEffs) r => Eff r x
280+
322281runSeqWriter :: forall s w r a. (IsSequence s, Element s ~ w) => Eff (Writer w ': r) a -> Eff r (a, s)
323282runSeqWriter = handleRelayS mempty (\s x -> return (x, s)) $ \s (Tell w) k -> k (cons w s) ()
324283
@@ -385,7 +344,7 @@ instantiate s = do
385344 modify (M.insert db t)
386345 return t
387346
388−infer :: NExprLoc -> InferM NType
347+infer :: NExprLoc -> InferM' NType
389348infer (Fix (Compose (Ann src x))) = local (const src) $ case x of
390349 NConstant a -> return . NAtomic $ case a of
391350 NURI {} -> URI
@@ -623,11 +582,9 @@ inferComponents n ((S.toList -> paths) : otherComponents) = do
623582 -- TODO: There should probably be some smarter predicate filtering
624583 schemes <- types & traverse . traverse %%~ (\t -> solveAndClose p $ sub s $ preds :=> t)
625584
626− (otherBindings, s') <-
627− captureSubstitutions $
628− withBindings (toScheme' <$> schemes) $
629− inferComponents n otherComponents
630− return $ M.unionWith mergeBindings (fmap (sub s') <$> schemes) otherBindings
585+ otherBindings <-
586+ withBindings (toScheme' <$> schemes) $ inferComponents n otherComponents
587+ return $ M.unionWith mergeBindings schemes otherBindings
631588 where
632589 bindingToNExpr :: NonEmpty VarName -> NExprLoc -> Binding NExpr
633590 bindingToNExpr name expr = NamedVar (StaticKey <$> name) (stripAnnotation expr) nullPos
@@ -730,33 +687,36 @@ showExpr :: NExpr -> Text
730687showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix
731688
732689inferGeneral :: NExprLoc -> InferM Scheme
733−inferGeneral x@(Fix (Compose (Ann src _))) = local (const src) . traceSubtree (showExpr . stripAnnotation $ x) $ do
734− (t, p, keep, s) <- inferGeneral' id $ infer x
735− solveAndClose p $ sub s $ keep :=> t
690+inferGeneral x@(Fix (Compose (Ann src _))) =
691+ local (const src) . traceSubtree (showExpr . stripAnnotation $ x) $ do
692+ (t, p, keep, s) <- inferGeneral' id $ infer x
693+ solveAndClose p $ sub s $ keep :=> t
736694
737695inferGeneral' ::
738696 (Members InferEffs r, Pretty y) =>
739697 (x -> y) ->
740− Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : r) x ->
698+ Eff (Writer Constraint : r) x ->
741699 Eff r (x, RS.RSet TypeVariable, [Pred], Substitution)
742700inferGeneral' toPretty f = do
743− (((x, subs), cs), range) <-
744− traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ f
701+ ((x, cs), range) <-
702+ traceSubtree "subexpressions" . registerTypeVariables . runSeqWriter @(Seq Constraint) $ f
745703 traceSubtree "received" $ do
746704 traceValue "type" $ renderPretty $ toPretty x
747− traceValue "substitutions" $ prettySubstitution subs
705+ get >>= traceValue "substitutions" . prettySubstitution
748706 traceValue "constraints" $ fmap renderPretty cs
749707 traceValue "range" $ T.pack . show $ range
750708 get @(MKM.Map Pred) >>= traceValue "preds" . showPreds
751− s' <- solveWithPriority range cs
752− traceValue "substitutions_after_solving" $ prettySubstitution s'
753− let s = subs <> s'
754− returnedS = Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution $ s
755− traceValue "composed_substitution" $ prettySubstitution s
709+ solveWithPriority range cs
710+ get >>= traceValue "substitutions_after_solving" . prettySubstitution
711+ (s, returnedS) <-
712+ get @Substitution
713+ <&> join bimap Substitution . M.partitionWithKey (\k _ -> k `RS.member` range) . unSubstitution
714+ put returnedS
715+ -- modify @Substitution $ Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution
716+ -- returnedS <- get @Substitution
756717 traceSubtree "returned" $ do
757718 traceValue "substitutions" $ prettySubstitution returnedS
758719 -- Filter for optimization purposes
759− subEnv returnedS
760720 preds <- get @(MKM.Map Pred)
761721 traceValue "subbed_preds" $ showPreds preds
762722 let newRange = range RS.\\ rangeFromSet (free returnedS)
@@ -796,7 +756,7 @@ solveAndClose range (cs :=> t) = do
796756 case (constraints, collectedPreds) of
797757 (Empty, []) -> return . close newRange $ solvedPreds :=> t
798758 _ -> do
799− s <- solveWithPriority newRange constraints
759+ ((), s) <- runState @Substitution mempty $ solveWithPriority newRange constraints
800760 solveAndClose newRange $ sub s $ (collectedPreds <> solvedPreds) :=> t
801761
802762solveConstraints ::