@@ -26,7 +26,6 @@ import Data.Act
2626import qualified Data.Aeson as A
2727import Data.Fix
2828import Data.Foldable
29−import Data.Functor.Contravariant
3029import Data.Group hiding ((~~))
3130import Data.List.NonEmpty (NonEmpty (..))
3231import qualified Data.List.NonEmpty as NE
@@ -190,35 +189,35 @@ v <<- x = return $ Substitution $ M.singleton v x
190189unifyWithPriority ::
191190 -- | The range of type variables to interpret as being lower
192191 -- priority (try to replace them if possible)
193− Predicate TypeVariable ->
192+ RS.RSet TypeVariable ->
194193 Constraint ->
195194 UnifyM Substitution
196−unifyWithPriority f (lhs :~ rhs) =
195+unifyWithPriority range (lhs :~ rhs) =
197196 case (lhs, rhs) of
198197 (x, y) | x == y -> return mempty
199198 (NTypeVariable x, NTypeVariable y) -> do
200− if getPredicate f y
199+ if y `RS.member` range
201200 then y <<- NTypeVariable x
202201 else x <<- NTypeVariable y
203202 (NTypeVariable t, x) -> t <<- x
204203 (x, NTypeVariable t) -> t <<- x
205− (List x, List y) -> unifyWithPriority f $ x :~ y
204+ (List x, List y) -> unifyWithPriority range $ x :~ y
206205 (NAttrSet x, NAttrSet y) -> do
207206 assertSetsMatch (tell . KeysDontMatch) (M.keysSet x) (M.keysSet y)
208− unifySchemes f . M.elems $ M.intersectionWith (,) x y
207+ unifySchemes range . M.elems $ M.intersectionWith (,) x y
209208 (x1 :-> y1, x2 :-> y2) -> do
210− s <- unifyWithPriority f (x1 :~ x2)
211− s' <- unifyWithPriority f $ sub s $ y1 :~ y2
209+ s <- unifyWithPriority range (x1 :~ x2)
210+ s' <- unifyWithPriority range $ sub s $ y1 :~ y2
212211 return $ s' <> s
213212 (x, y) -> tell (CanNotUnify x y) >> return mempty
214213
215−unifySchemes :: Predicate TypeVariable -> [(Scheme, Scheme)] -> UnifyM Substitution
214+unifySchemes :: RS.RSet TypeVariable -> [(Scheme, Scheme)] -> UnifyM Substitution
216215unifySchemes _ [] = pure mempty
217−unifySchemes f ((x, y) : rest) = do
218− s <- unifyScheme f x y
219− sub s <$> unifySchemes f (sub s rest)
216+unifySchemes range ((x, y) : rest) = do
217+ s <- unifyScheme range x y
218+ sub s <$> unifySchemes range (sub s rest)
220219
221−unifyScheme :: Predicate TypeVariable -> Scheme -> Scheme -> UnifyM Substitution
220+unifyScheme :: RS.RSet TypeVariable -> Scheme -> Scheme -> UnifyM Substitution
222221unifyScheme range (xs :=> x) (ys :=> y) = do
223222 s <- solveWithPriority range (pure (x :~ y))
224223 let f = S.fromList . sub s
@@ -236,13 +235,13 @@ solve = solveWithPriority mempty
236235solveWithPriority ::
237236 -- | The range of type variables to interpret as being lower
238237 -- priority (try to replace them if possible)
239− Predicate TypeVariable ->
238+ RS.RSet TypeVariable ->
240239 Seq Constraint ->
241240 UnifyM Substitution
242241solveWithPriority _ Empty = return mempty
243−solveWithPriority f (rest :|> c) = do
244− s <- unifyWithPriority f c
245− sub s <$> solveWithPriority f (fmap (sub s) rest)
242+solveWithPriority range (rest :|> c) = do
243+ s <- unifyWithPriority range c
244+ sub s <$> solveWithPriority range (fmap (sub s) rest)
246245
247246data Errors
248247 = UndefinedVariable VarName
@@ -711,7 +710,7 @@ inferGeneral' ::
711710 (Members InferEffs r, Pretty y) =>
712711 (x -> y) ->
713712 Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : r) x ->
714− Eff r (x, Predicate TypeVariable, [Pred], Substitution)
713+ Eff r (x, RS.RSet TypeVariable, [Pred], Substitution)
715714inferGeneral' toPretty f = do
716715 (((x, subs), cs), range) <-
717716 traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ f
@@ -721,7 +720,7 @@ inferGeneral' toPretty f = do
721720 traceValue "constraints" $ fmap renderPretty cs
722721 traceValue "range" $ T.pack . show $ range
723722 get @(MKM.Map Pred) >>= traceValue "preds" . showPreds
724− s' <- solveWithPriority (Predicate (`RS.member` range)) cs
723+ s' <- solveWithPriority range cs
725724 traceValue "substitutions_after_solving" $ prettySubstitution s'
726725 let s = subs <> s'
727726 returnedS = Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution $ s
@@ -731,8 +730,8 @@ inferGeneral' toPretty f = do
731730 subEnv returnedS
732731 preds <- get @(MKM.Map Pred)
733732 traceValue "subbed_preds" $ showPreds preds
734− let p = Predicate (`RS.member` range) <> Predicate (`S.notMember` free returnedS)
735− (keep', toss) = MKM.partition (getPredicate p) preds
733+ let newRange = range RS.\\ rangeFromSet (free returnedS)
734+ (keep', toss) = MKM.partition (`RS.member` newRange) preds
736735 keep = MKM.toList keep'
737736 -- At this point the only predicates only contain type variables that are only used
738737 -- in the expression. This means that all of the generated constraints and
@@ -740,11 +739,14 @@ inferGeneral' toPretty f = do
740739 traceValue "preds" $ showPreds toss
741740 traceValue "keep_preds" $ showPreds keep'
742741 put toss
743− return (x, p, keep, s)
742+ return (x, newRange, keep, s)
744743 where
745744 showPreds :: MKM.Map Pred -> Map String String
746745 showPreds = M.mapKeys show . fmap show . MKM.toMap
747746
747+rangeFromSet :: (Ord x, Enum x) => S.Set x -> RS.RSet x
748+rangeFromSet = RS.fromAscList . S.toAscList
749+
748750solveAndClose ::
749751 Members
750752 '[ Writer (TypeVariable, SrcSpan),
@@ -754,24 +756,21 @@ solveAndClose ::
754756 Writer UnifyingError
755757 ]
756758 eff =>
757− Predicate TypeVariable ->
759+ RS.RSet TypeVariable ->
758760 Scheme ->
759761 Eff eff Scheme
760−solveAndClose p (cs :=> t) = do
761− (((solvedPreds, range), constraints), collectedPreds) <-
762+solveAndClose range (cs :=> t) = do
763+ (((solvedPreds, range'), constraints), collectedPreds) <-
762764 runSeqWriter @[Pred]
763765 . runSeqWriter @(Seq Constraint)
764766 . registerTypeVariables
765767 $ solveConstraints cs
766− let newPredicate = p `pOr` Predicate (`RS.member` range)
768+ let newRange = range `RS.union` range'
767769 case (constraints, collectedPreds) of
768− (Empty, []) -> return . close newPredicate $ solvedPreds :=> t
770+ (Empty, []) -> return . close newRange $ solvedPreds :=> t
769771 _ -> do
770− s <- solveWithPriority newPredicate constraints
771− solveAndClose newPredicate $ sub s $ (collectedPreds <> solvedPreds) :=> t
772−
773−pOr :: Predicate x -> Predicate x -> Predicate x
774−pOr (Predicate f) (Predicate g) = Predicate $ \x -> f x || g x
772+ s <- solveWithPriority newRange constraints
773+ solveAndClose newRange $ sub s $ (collectedPreds <> solvedPreds) :=> t
775774
776775solveConstraints ::
777776 Members
@@ -813,8 +812,8 @@ instance Act DeBruijnContext DeBruijn where
813812
814813type TDeBruijnMap = ShiftedMap DeBruijnContext TypeVariable DeBruijn
815814
816−close :: TraversableNTypes x => Predicate TypeVariable -> x -> x
817−close (Predicate f) =
815+close :: TraversableNTypes x => RS.RSet TypeVariable -> x -> x
816+close range =
818817 run
819818 . evalState @TDeBruijnMap mempty
820819 . runReader @Int 0
@@ -827,7 +826,7 @@ close (Predicate f) =
827826 traverseNTypesWith bndCtx %%~ \case
828827 x@(TBruijn _) -> return x
829828 x@(TAtomic _) -> return x
830− (TTypeVariable tv) | f tv -> TBruijn <$> newbruijn tv
829+ (TTypeVariable tv) | tv `RS.member` range -> TBruijn <$> newbruijn tv
831830 x@(TTypeVariable _) -> return x
832831
833832 bndCtx m = do