@@ -24,6 +24,7 @@ import Control.Monad.Freer.TreeTracer
24import Control.Monad.Freer.Writer
24import Control.Monad.Freer.Writer
25import Data.Act
25import Data.Act
26import qualified Data.Aeson as A
26import qualified Data.Aeson as A
27import Data.Fix
28import Data.Fix
28import Data.Foldable
29import Data.Foldable
29import Data.Group hiding ((~~))
30import Data.Group hiding ((~~))
@@ -61,7 +62,7 @@ getType r =
61 . runReader nullSpan
62 . runReader nullSpan
62 . evalState @(MKM.Map Pred) mempty
63 . evalState @(MKM.Map Pred) mempty
63 . interpret @(Writer Pred) (\(Tell x) -> modify (<> MKM.singleton x))
64 . interpret @(Writer Pred) (\(Tell x) -> modify (<> MKM.singleton x))
64− . evalState (M.empty :: VariableMap)
65+ . runReader (M.empty :: VariableMap)
65 . evalState @Substitution mempty
66 . evalState @Substitution mempty
66 . runState @[(TypeVariable, SrcSpan)] []
67 . runState @[(TypeVariable, SrcSpan)] []
67 . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))
68 . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))
@@ -86,6 +87,11 @@ runFreshSrc =
86 src <- ask @SrcSpan
87 src <- ask @SrcSpan
87 tell (v, src)
88 tell (v, src)
91+ v <- send $ FreshSub x
89 MinFreshFromNow -> send MinFreshFromNow
95 MinFreshFromNow -> send MinFreshFromNow
@@ -183,7 +189,7 @@ v <<- x = modify (Substitution (M.singleton v x) <>)
183unifyWithPriority ::
189unifyWithPriority ::
184 -- | The range of type variables to interpret as being lower
190 -- | The range of type variables to interpret as being lower
185 -- priority (try to replace them if possible)
191 -- priority (try to replace them if possible)
186− RS.RSet TypeVariable ->
192+ RS.RSet RangeTypeVariable ->
187 Constraint ->
193 Constraint ->
188 UnifyM ()
194 UnifyM ()
189unifyWithPriority range (lhs :~ rhs) = do
195unifyWithPriority range (lhs :~ rhs) = do
@@ -191,7 +197,7 @@ unifyWithPriority range (lhs :~ rhs) = do
191 case sub s (lhs, rhs) of
197 case sub s (lhs, rhs) of
192 (x, y) | x == y -> return mempty
198 (x, y) | x == y -> return mempty
193 (NTypeVariable x, NTypeVariable y) -> do
199 (NTypeVariable x, NTypeVariable y) -> do
194− if y `RS.member` range
200+ if rangeTypeVariable y `RS.member` range
195 then y <<- NTypeVariable x
201 then y <<- NTypeVariable x
196 else x <<- NTypeVariable y
202 else x <<- NTypeVariable y
197 (NTypeVariable t, x) -> t <<- x
203 (NTypeVariable t, x) -> t <<- x
@@ -205,13 +211,13 @@ unifyWithPriority range (lhs :~ rhs) = do
205 unifyWithPriority range $ y1 :~ y2
211 unifyWithPriority range $ y1 :~ y2
206 (x, y) -> tell (CanNotUnify x y)
212 (x, y) -> tell (CanNotUnify x y)
208−unifySchemes :: RS.RSet TypeVariable -> [(Scheme, Scheme)] -> UnifyM ()
214+unifySchemes :: RS.RSet RangeTypeVariable -> [(Scheme, Scheme)] -> UnifyM ()
209unifySchemes _ [] = pure mempty
215unifySchemes _ [] = pure mempty
210unifySchemes range ((x, y) : rest) = do
216unifySchemes range ((x, y) : rest) = do
211 unifyScheme range x y
217 unifyScheme range x y
212 unifySchemes range rest
218 unifySchemes range rest
214−unifyScheme :: RS.RSet TypeVariable -> Scheme -> Scheme -> UnifyM ()
220+unifyScheme :: RS.RSet RangeTypeVariable -> Scheme -> Scheme -> UnifyM ()
215unifyScheme range (xs :=> x) (ys :=> y) = do
221unifyScheme range (xs :=> x) (ys :=> y) = do
216 solveWithPriority range (pure (x :~ y))
222 solveWithPriority range (pure (x :~ y))
@@ -229,7 +235,7 @@ solve = solveWithPriority mempty
229solveWithPriority ::
235solveWithPriority ::
230 -- | The range of type variables to interpret as being lower
236 -- | The range of type variables to interpret as being lower
231 -- priority (try to replace them if possible)
237 -- priority (try to replace them if possible)
232− RS.RSet TypeVariable ->
238+ RS.RSet RangeTypeVariable ->
233 Seq Constraint ->
239 Seq Constraint ->
234 UnifyM ()
240 UnifyM ()
235solveWithPriority _ Empty = return mempty
241solveWithPriority _ Empty = return mempty
@@ -267,7 +273,7 @@ type InferEffs =
267 Writer PredicateError,
273 Writer PredicateError,
268 Writer Pred,
274 Writer Pred,
269 State (MKM.Map Pred),
275 State (MKM.Map Pred),
270− State VariableMap,
276+ Reader VariableMap,
271 Writer UnifyingError,
277 Writer UnifyingError,
272 Writer InferError,
278 Writer InferError,
273 State Substitution,
279 State Substitution,
@@ -304,17 +310,12 @@ type VariableMap = Map VarName Scheme
304(~~) :: Member (Writer Constraint) r => NType -> NType -> Eff r ()
310(~~) :: Member (Writer Constraint) r => NType -> NType -> Eff r ()
305lhs ~~ rhs = tell $ lhs :~ rhs
311lhs ~~ rhs = tell $ lhs :~ rhs
307−-- TODO: shadowed bindings are not properly restored.
308withBindings ::
313withBindings ::
309− (Member (State VariableMap) effs) =>
314+ (Member (Reader VariableMap) effs) =>
310 VariableMap ->
315 VariableMap ->
311 Eff effs a ->
316 Eff effs a ->
312 Eff effs a
317 Eff effs a
313−withBindings bindings m = do
318+withBindings bindings = local (bindings <>)
314− modify (bindings <>)
316− modify @VariableMap (`M.difference` bindings)
319instantiate ::
320instantiate ::
320 forall effs.
321 forall effs.
@@ -356,7 +357,7 @@ infer (Fix (Compose (Ann src x))) = local (const src) $ case x of
356 NEnvPath {} -> return . NAtomic $ Path
357 NEnvPath {} -> return . NAtomic $ Path
357 NStr {} -> return $ NAtomic String
358 NStr {} -> return $ NAtomic String
358 NSym var ->
359 NSym var ->
359− get @VariableMap
360+ ask @VariableMap
360 >>= maybe (scheme . NTypeVariable <$> throwTV (UndefinedVariable var)) return . M.lookup var
361 >>= maybe (scheme . NTypeVariable <$> throwTV (UndefinedVariable var)) return . M.lookup var
361 >>= instantiate -- I have no idea if this covers all cases.
362 >>= instantiate -- I have no idea if this covers all cases.
362 NList xs -> do
363 NList xs -> do
@@ -413,8 +414,7 @@ infer (Fix (Compose (Ann src x))) = local (const src) $ case x of
414 NTypeVariable <$> case path of
415 NTypeVariable <$> case path of
415 Just p -> do
416 Just p -> do
416− (set', var) <- lookupAttrSet p
417+ (_, var) <- lookupAttrSet setT p
418 return var
418 return var
419 Nothing -> fresh
419 Nothing -> fresh
420 case def of
420 case def of
@@ -563,27 +563,30 @@ inferComponents :: NormalizedBinding NExprLoc -> [Set (NonEmpty VarName)] -> Inf
563inferComponents _ [] = pure M.empty
563inferComponents _ [] = pure M.empty
564inferComponents n ((S.toList -> paths) : otherComponents) = do
564inferComponents n ((S.toList -> paths) : otherComponents) = do
565 let bindings = catMaybes $ paths <&> \path -> (path,) <$> lookupExpr path n
565 let bindings = catMaybes $ paths <&> \path -> (path,) <$> lookupExpr path n
566− (types, p, preds, s) <-
567− traceSubtree (showExpr . bindingsToNExpr $ bindings)
566+ (schemes, schemes') <- traceSubtree (showExpr . bindingsToNExpr $ bindings) $ do
567+ (types, p, preds, s) <-
568− . inferGeneral' (NAttrSet . fmap toScheme)
568+ inferGeneral' (NAttrSet . fmap toScheme) $
570− tvsExprs <- for bindings (\(a, b) -> (a,b,) . NTypeVariable <$> fresh)
570+ tvsExprs <- for bindings (\(a, b) -> (a,b,) . NTypeVariable <$> fresh)
571− let tvsExprs' =
571+ let tvsExprs' =
572− foldl' (M.unionWith mergeBindings) M.empty $
572+ foldl' (M.unionWith mergeBindings) M.empty $
573− fmap (\(a, b, c) -> normalize a (b, c)) tvsExprs
573+ fmap (\(a, b, c) -> normalize a (b, c)) tvsExprs
574− tvs = toScheme . fmap snd <$> tvsExprs'
574+ tvs = toScheme . fmap snd <$> tvsExprs'
576− -- (type, tv)
576+ -- (type, tv)
577− tvsTypes <-
577+ tvsTypes <-
578− withBindings tvs $
578+ withBindings tvs $
579− tvsExprs' & traverse . traverse . _1 %%~ infer
579+ tvsExprs' & traverse . traverse . _1 %%~ infer
580− for_ tvsTypes $ traverse (uncurry (~~))
580+ for_ tvsTypes $ traverse (uncurry (~~))
581− return $ fmap fst <$> tvsTypes
581+ return $ fmap fst <$> tvsTypes
582− -- TODO: There should probably be some smarter predicate filtering
582+ -- TODO: There should probably be some smarter predicate filtering
583− schemes <- types & traverse . traverse %%~ (\t -> solveAndClose p $ sub s $ preds :=> t)
583+ schemes <- types & traverse . traverse %%~ (\t -> solveAndClose p $ sub s $ preds :=> t)
584+ let schemes' = toScheme' <$> schemes
585+ traceValue "resulting_type" $ renderPretty . scheme $ NAttrSet schemes'
586+ return (schemes, schemes')
585 otherBindings <-
588 otherBindings <-
586− withBindings (toScheme' <$> schemes) $ inferComponents n otherComponents
589+ withBindings schemes' $ inferComponents n otherComponents
587 return $ M.unionWith mergeBindings schemes otherBindings
590 return $ M.unionWith mergeBindings schemes otherBindings
589 bindingToNExpr :: NonEmpty VarName -> NExprLoc -> Binding NExpr
592 bindingToNExpr :: NonEmpty VarName -> NExprLoc -> Binding NExpr
@@ -690,13 +693,15 @@ inferGeneral :: NExprLoc -> InferM Scheme
690inferGeneral x@(Fix (Compose (Ann src _))) =
693inferGeneral x@(Fix (Compose (Ann src _))) =
691 local (const src) . traceSubtree (showExpr . stripAnnotation $ x) $ do
694 local (const src) . traceSubtree (showExpr . stripAnnotation $ x) $ do
692 (t, p, keep, s) <- inferGeneral' id $ infer x
695 (t, p, keep, s) <- inferGeneral' id $ infer x
693− solveAndClose p $ sub s $ keep :=> t
696+ res <- solveAndClose p $ sub s $ keep :=> t
697+ traceValue "resuting_type" $ renderPretty res
695inferGeneral' ::
700inferGeneral' ::
696 (Members InferEffs r, Pretty y) =>
701 (Members InferEffs r, Pretty y) =>
697 (x -> y) ->
702 (x -> y) ->
698 Eff (Writer Constraint : r) x ->
703 Eff (Writer Constraint : r) x ->
699− Eff r (x, RS.RSet TypeVariable, [Pred], Substitution)
704+ Eff r (x, RS.RSet RangeTypeVariable, [Pred], Substitution)
700inferGeneral' toPretty f = do
705inferGeneral' toPretty f = do
701 ((x, cs), range) <-
706 ((x, cs), range) <-
702 traceSubtree "subexpressions" . registerTypeVariables . runSeqWriter @(Seq Constraint) $ f
707 traceSubtree "subexpressions" . registerTypeVariables . runSeqWriter @(Seq Constraint) $ f
@@ -710,7 +715,7 @@ inferGeneral' toPretty f = do
710 get >>= traceValue "substitutions_after_solving" . prettySubstitution
715 get >>= traceValue "substitutions_after_solving" . prettySubstitution
711 (s, returnedS) <-
716 (s, returnedS) <-
712 get @Substitution
717 get @Substitution
713− <&> join bimap Substitution . M.partitionWithKey (\k _ -> k `RS.member` range) . unSubstitution
718+ <&> join bimap Substitution . M.partitionWithKey (\k _ -> rangeTypeVariable k `RS.member` range) . unSubstitution
714 put returnedS
719 put returnedS
715 -- modify @Substitution $ Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution
720 -- modify @Substitution $ Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution
716 -- returnedS <- get @Substitution
721 -- returnedS <- get @Substitution
@@ -718,9 +723,8 @@ inferGeneral' toPretty f = do
718 traceValue "substitutions" $ prettySubstitution returnedS
723 traceValue "substitutions" $ prettySubstitution returnedS
719 -- Filter for optimization purposes
724 -- Filter for optimization purposes
720 preds <- get @(MKM.Map Pred)
725 preds <- get @(MKM.Map Pred)
721− traceValue "subbed_preds" $ showPreds preds
722 let newRange = range RS.\\ rangeFromSet (free returnedS)
726 let newRange = range RS.\\ rangeFromSet (free returnedS)
723− (keep', toss) = MKM.partition (`RS.member` newRange) preds
727+ (keep', toss) = MKM.partition ((`RS.member` newRange) . rangeTypeVariable) preds
724 keep = MKM.toList keep'
728 keep = MKM.toList keep'
725 -- At this point the only predicates only contain type variables that are only used
729 -- At this point the only predicates only contain type variables that are only used
726 -- in the expression. This means that all of the generated constraints and
730 -- in the expression. This means that all of the generated constraints and
@@ -733,8 +737,8 @@ inferGeneral' toPretty f = do
733 showPreds :: MKM.Map Pred -> Map String String
737 showPreds :: MKM.Map Pred -> Map String String
734 showPreds = M.mapKeys show . fmap show . MKM.toMap
738 showPreds = M.mapKeys show . fmap show . MKM.toMap
736−rangeFromSet :: (Ord x, Enum x) => S.Set x -> RS.RSet x
740+rangeFromSet :: S.Set TypeVariable -> RS.RSet RangeTypeVariable
737−rangeFromSet = RS.fromAscList . S.toAscList
741+rangeFromSet = RS.fromAscList . fmap rangeTypeVariable . S.toAscList
739solveAndClose ::
743solveAndClose ::
@@ -743,20 +747,21 @@ solveAndClose ::
743 Writer UnifyingError
747 Writer UnifyingError
746− RS.RSet TypeVariable ->
750+ RS.RSet RangeTypeVariable ->
747 Scheme ->
751 Scheme ->
748 Eff eff Scheme
752 Eff eff Scheme
749−solveAndClose range (cs :=> t) = do
753+solveAndClose range (cs :=> t) = evalState @Substitution mempty $ do
750 (((solvedPreds, range'), constraints), collectedPreds) <-
754 (((solvedPreds, range'), constraints), collectedPreds) <-
751 runSeqWriter @[Pred]
755 runSeqWriter @[Pred]
752 . runSeqWriter @(Seq Constraint)
756 . runSeqWriter @(Seq Constraint)
753 . registerTypeVariables
757 . registerTypeVariables
754− $ solveConstraints cs
758+ $ solveConstraints range cs
755 let newRange = range `RS.union` range'
759 let newRange = range `RS.union` range'
756 case (constraints, collectedPreds) of
760 case (constraints, collectedPreds) of
757 (Empty, []) -> return . close newRange $ solvedPreds :=> t
761 (Empty, []) -> return . close newRange $ solvedPreds :=> t
759− ((), s) <- runState @Substitution mempty $ solveWithPriority newRange constraints
763+ solveWithPriority newRange constraints
760 solveAndClose newRange $ sub s $ (collectedPreds <> solvedPreds) :=> t
765 solveAndClose newRange $ sub s $ (collectedPreds <> solvedPreds) :=> t
762solveConstraints ::
767solveConstraints ::
@@ -764,30 +769,43 @@ solveConstraints ::
764 '[ Fresh,
769 '[ Fresh,
765 Writer Pred,
770 Writer Pred,
766 Writer PredicateError,
771 Writer PredicateError,
767− Writer Constraint
772+ Writer Constraint,
773+ Writer UnifyingError,
777+ RS.RSet RangeTypeVariable ->
770 [Pred] ->
778 [Pred] ->
771 Eff effs [Pred]
779 Eff effs [Pred]
772−solveConstraints ps = do
780+solveConstraints _ [] = pure []
773− flip Control.Monad.filterM ps $ \case
781+solveConstraints range (p : ps) = case p of
774− HasField (NAttrSet ts) (f, t) -> case M.lookup f ts of
782+ HasField (NAttrSet ts) (f, t) -> case M.lookup f ts of
775− Nothing -> do
783+ Nothing -> do
776− tell $ KeyNotPresent f (NAttrSet ts)
784+ tell $ KeyNotPresent f (NAttrSet ts)
777− return False
785+ solveConstraints range ps
778− Just t' -> do
786+ Just t' -> do
779− x <- instantiate t
787+ x <- instantiate t
780− y <- instantiate t'
788+ y <- instantiate t'
782− return False
790+ solveConstraints range ps
783− HasField (NTypeVariable _) _ -> return True
791+ HasField tv@(NTypeVariable _) (k, v) -> do
792+ let sameAttrSet :: Pred -> Either Scheme Pred
794+ HasField t (k', v') | t == tv, k == k' -> Left v'
796+ (same, different) = partitionWith sameAttrSet ps
797+ (unifyScheme range v) `traverse_` same
798+ (p :) <$> solveConstraints range different
784− HasField t _ -> do
799+ HasField t _ -> do
785− tell $ NotAnAttributeSet t
800+ tell $ NotAnAttributeSet t
786− return False
801+ solveConstraints range ps
787− (Update (NAttrSet a) (NAttrSet b) t) -> do
802+ (Update (NAttrSet a) (NAttrSet b) t) -> do
788− (NAttrSet $ b <> a) ~~ t
803+ (NAttrSet $ b <> a) ~~ t
789− return False
804+ solveConstraints range ps
790− _ -> return True
805+ _ -> (p :) <$> solveConstraints range ps
807+partitionWith :: (a -> Either b c) -> [a] -> ([b], [c])
808+partitionWith f = partitionEithers . map f
792newtype DeBruijnContext = DeBruijnContext (Sum Int)
810newtype DeBruijnContext = DeBruijnContext (Sum Int)
793 deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
811 deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
@@ -797,7 +815,7 @@ instance Act DeBruijnContext DeBruijn where
798type TDeBruijnMap = ShiftedMap DeBruijnContext TypeVariable DeBruijn
816type TDeBruijnMap = ShiftedMap DeBruijnContext TypeVariable DeBruijn
800−close :: TraversableNTypes x => RS.RSet TypeVariable -> x -> x
818+close :: TraversableNTypes x => RS.RSet RangeTypeVariable -> x -> x
801close range =
819close range =
803 . evalState @TDeBruijnMap mempty
821 . evalState @TDeBruijnMap mempty
@@ -811,7 +829,7 @@ close range =
811 traverseNTypesWith bndCtx %%~ \case
829 traverseNTypesWith bndCtx %%~ \case
812 x@(TBruijn _) -> return x
830 x@(TBruijn _) -> return x
813 x@(TAtomic _) -> return x
831 x@(TAtomic _) -> return x
814− (TTypeVariable tv) | tv `RS.member` range -> TBruijn <$> newbruijn tv
832+ (TTypeVariable tv) | rangeTypeVariable tv `RS.member` range -> TBruijn <$> newbruijn tv
815 x@(TTypeVariable _) -> return x
833 x@(TTypeVariable _) -> return x
817 bndCtx m = do
835 bndCtx m = do
@@ -866,18 +884,22 @@ lookupAttrSet ::
869 AttrSetPath ->
888 AttrSetPath ->
870 Eff r (NType, TypeVariable)
889 Eff r (NType, TypeVariable)
890+lookupAttrSet n = \case
871−lookupAttrSet (NESingle p) = do
891+ (NESingle p) -> do
872− set <- NTypeVariable <$> fresh
892+ var <- getSubTV n
874− tell (HasField set (p, scheme . NTypeVariable $ var))
893+ tell (HasField n (p, scheme . NTypeVariable $ var))
875− return (set, var)
894+ return (n, var)
876−lookupAttrSet (p :|| ps) = do
895+ (p :|| ps) -> do
877− set <- NTypeVariable <$> fresh
878− (innerSet, var) <- lookupAttrSet ps
896+ (innerSet, var) <- lookupAttrSet n ps
897+ set <- NTypeVariable <$> getSubTV n
879− tell $ HasField set (p, scheme innerSet)
898+ tell $ HasField set (p, scheme innerSet)
880− return (set, var)
899+ return (set, var)
901+ getSubTV (NTypeVariable tv) = freshSub tv
882-- NonEmpty patterns
904-- NonEmpty patterns