@@ -10,7 +10,6 @@ where
1010
1111import Control.Monad
1212import Control.Monad.Freer
13−import Control.Monad.Freer.Error
1413import Control.Monad.Freer.Internal (handleRelayS)
1514import Control.Monad.Freer.Reader
1615import Control.Monad.Freer.State
@@ -19,7 +18,6 @@ import Data.Act
1918import Data.Fix
2019import Data.Foldable
2120import Data.Functor
22−import Data.Functor.Classes
2321import Data.Group
2422import Data.List.NonEmpty (NonEmpty (..))
2523import qualified Data.List.NonEmpty as NE
@@ -40,43 +38,48 @@ import Data.Text (Text)
4038import qualified Data.Text.Lazy as TL
4139import qualified Data.Text.Lazy.Builder as T
4240import Data.Traversable
43−import Debug.Trace
4441import Nix.Atoms
4542import Nix.Expr
4643
44+runConstraintEnv ::
45+ Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : effs) a ->
46+ Eff effs ((a, Substitution), Seq Constraint)
47+runConstraintEnv =
48+ runState @(Seq Constraint) Empty
49+ . interpret @(Writer Constraint) (\(Tell x) -> modify (x :<|))
50+ . runWriter @Substitution
51+ . interpret @(SubstituteEnv)
52+ ( \(SubstituteEnv x) -> do
53+ modify @(Seq Constraint) (subCon x <$>)
54+ tell x
55+ return ()
56+ )
57+
4758getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError])
4859getType r =
49− let ((((t, unifying), srcs), constraints), errs) =
60+ let (((((t, unifying), errs), srcs), subs), _) =
5061 run
51− . runReader (M.empty :: VariableMap)
62+ . runConstraintEnv
63+ . runState @[(TypeVariable, SrcSpan)] []
64+ . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))
5265 . runSeqWriter @[(SrcSpan, Errors)]
53− . runSeqWriter @(Seq Constraint)
54− . runSeqWriter @[(TypeVariable, SrcSpan)]
5566 . runSeqWriter @[UnifyingError]
67+ . runReader (M.empty :: VariableMap)
5668 . runFresh
57− $ getType' r
58− in (t, errs, unifying)
69+ $ inferGeneral r
70+ in (sub subs t, errs, unifying)
5971
60−getType' ::
61− Members
62− '[ Writer (SrcSpan, Errors),
63− Reader VariableMap,
64− Writer (TypeVariable, SrcSpan),
65− Writer UnifyingError,
66− Fresh
67− ]
68− r =>
69− NExprLoc ->
70− Eff r NType
71−getType' r = do
72− ((t, s'), constraints) <-
73− runSeqWriter @(Seq Constraint) . runWriter @Substitution $
74− inferGeneral r
75− s <- solve (traceShowId . fmap (subCon s') $ constraints)
76− return . close InfiniteRange $ sub (s <> s') (traceShowId t)
72+data SubstituteEnv a where
73+ SubstituteEnv :: Substitution -> SubstituteEnv ()
74+
75+subEnv :: Member SubstituteEnv r => Substitution -> Eff r ()
76+subEnv = send . SubstituteEnv
7777
7878newtype TypeVariable = TypeVariable Int
79− deriving newtype (Show, Eq, Ord)
79+ deriving newtype (Eq, Ord)
80+
81+instance Show TypeVariable where
82+ show (TypeVariable n) = "〚" <> show n <> "〛"
8083
8184data Constraint = !NType :~ !NType
8285 deriving stock (Eq, Ord, Show)
@@ -175,7 +178,7 @@ getDeBurjins' n (NAttrSet xs) = foldMap (getDeBurjins' (n + 1)) . M.elems $ xs
175178-- binding context number.
176179getAllDeBurjins :: NType -> Set DeBrujin
177180getAllDeBurjins =
178− traceShowId . \case
181+ \case
179182 (NTypeVariable _) -> S.empty
180183 (NAtomic _) -> S.empty
181184 (NBrujin x) -> S.singleton x
@@ -206,6 +209,7 @@ close range =
206209 close' x@(NAtomic _) = return x
207210 close' x@(NBrujin _) = return x
208211 close' (NTypeVariable tv) | tv `R.member` range = NBrujin <$> newbrujin tv
212+ close' x@(NTypeVariable _) = return x
209213 close' (x :-> y) = bndCtx $ (:->) <$> close' x <*> close' y
210214 close' (List x) = bndCtx $ List <$> close' x
211215 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
@@ -239,6 +243,7 @@ instance Free NType where
239243newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
240244 deriving newtype (Eq, Ord, Show)
241245
246+-- | Prefers the left
242247instance Semigroup Substitution where
243248 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
244249
@@ -308,25 +313,13 @@ solveWithPriority ::
308313solveWithPriority _ Empty = return mempty
309314solveWithPriority range (rest :|> c) = do
310315 s <- unifyWithPriority range c
311− (<> s) <$> solveWithPriority range (fmap (subCon (traceShowId s)) rest)
316+ (<> s) <$> solveWithPriority range (fmap (subCon s) rest)
312317
313−pattern Sempty <- (S.null -> True) where Sempty = S.empty
318+-- pattern Sempty <- (S.null -> True) where Sempty = S.empty
314319
315320occursIn :: Free x => TypeVariable -> x -> Bool
316321occursIn t x = t `S.member` free x
317322
318−data SchemeX x = Scheme (Set TypeVariable) x
319− deriving stock (Eq, Ord, Show)
320−
321−instance Show1 SchemeX where
322− liftShowsPrec s _ p (Scheme Sempty x) = s p x
323− liftShowsPrec s _ p (Scheme tvs x) = ((("forall " <> show tvs)) <>) <> s p x
324−
325−instance Eq1 SchemeX where
326− liftEq eq (Scheme ts1 x1) (Scheme ts2 x2) = ts1 == ts2 && eq x1 x2
327−
328−-- type SchemeS = SchemeX NType
329−
330323data Errors
331324 = UndefinedVariable VarName
332325 | UnexpectedType {expected :: NType, got :: NType}
@@ -338,8 +331,6 @@ data Fresh x where
338331 -- | Inclusive
339332 MinFreshFromNow :: Fresh TypeVariable
340333
341−data ResumableExceptions x
342−
343334type Runner effect = forall effs a. Eff (effect ': effs) a -> Eff effs a
344335
345336runFresh :: Runner Fresh
@@ -384,7 +375,7 @@ type InferEffs =
384375 Writer (SrcSpan, Errors),
385376 Reader VariableMap,
386377 Writer UnifyingError,
387− Writer Substitution
378+ SubstituteEnv
388379 ]
389380
390381type InferM x = forall r. Members InferEffs r => Eff r x
@@ -482,12 +473,19 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
482473 lhst ~~ rhst
483474 return $ NAtomic Bool
484475 NBinary op lhs rhs
485− | op `elem` [NLt, NLte, NGt, NGte, NPlus, NMinus, NMult, NDiv] -> do
476+ | op `elem` [NLt, NLte, NGt, NGte] -> do
486477 lhst <- infer lhs
487478 rhst <- infer rhs
488479 -- TODO: Infer lhst and rhst are either Integer or Double
489480 lhst ~~ rhst
490481 return $ NAtomic Bool
482+ NBinary op lhs rhs
483+ | op `elem` [NPlus, NMinus, NMult, NDiv] -> do
484+ lhst <- infer lhs
485+ rhst <- infer rhs
486+ -- TODO: Infer lhst and rhst are either Integer or Double
487+ lhst ~~ rhst
488+ return $ lhst
491489 NBinary op lhs rhs | op `elem` [NAnd, NOr, NImpl] -> do
492490 lhst <- infer lhs
493491 rhst <- infer rhs
@@ -573,17 +571,25 @@ inferBinding bindings = do
573571 Just r -> Just (name, r)
574572 return $ M.fromListWith mergeSetTypes bindings'
575573
574+-- traceShowMStack :: (HasCallStack, Applicative f, Show a) => a -> f ()
575+-- traceShowMStack = withFrozenCallStack $ traceShowMStack' ""
576+
577+-- traceShowMStack' :: (HasCallStack, Applicative f, Show a) => String -> a -> f ()
578+-- traceShowMStack' s a = withFrozenCallStack $ do
579+-- case getCallStack callStack of
580+-- (_ : (x, _) : _) -> traceM $ x <> " " <> s <> " \t" <> show a
581+-- _ -> traceM $ s <> " \t" <> show a
582+
576583inferGeneral :: NExprLoc -> InferM NType
577584inferGeneral x = do
578− ((t, cs), range) <- registerTypeVariables . runSeqWriter @(Seq Constraint) $ infer x
579− s <- solveWithPriority range cs
585+ (((t, subs), cs), range) <- registerTypeVariables . runConstraintEnv $ infer x
586+ s' <- solveWithPriority range cs
587+ let s = subs <> s'
588+ returnedS = Substitution . M.filterWithKey (\k _ -> k `R.notMember` range) . unSubstitution $ s
580589 -- Filter for optimization purposes
581− tell . Substitution . M.filterWithKey (\k _ -> k `R.notMember` range) . unSubstitution $ s
590+ subEnv returnedS
582591 return . close range $ sub s t
583592
584−-- appAll :: (a -> b -> b) -> [a] -> b -> b
585−-- appAll f xs = appEndo (mconcat $ Endo . f <$> xs)
586−
587593expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap
588594expectAttrSet (NAttrSet x) = return x
589595expectAttrSet g = do