@@ -9,7 +9,6 @@ module Tix.Typechecker
99 )
1010where
1111
12−import Control.Exception (assert)
1312import Control.Lens hiding (Empty, List, cons, equality, set, set')
1413import Control.Monad
1514import Control.Monad.Freer
@@ -27,6 +26,7 @@ import Data.Foldable
2726import Data.Functor.Contravariant
2827import Data.Group hiding ((~~))
2928import Data.List.NonEmpty (NonEmpty (..))
29+import qualified Data.Map.MultiKey.Strict as MKM
3030import Data.Map.Shifted.Strict (ShiftedMap (..))
3131import qualified Data.Map.Shifted.Strict as SM
3232import Data.Map.Strict (Map)
@@ -51,8 +51,10 @@ import Tix.Types
5151
5252getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [UnifyingError], [PredicateError], A.Object)
5353getType r =
54− let (((((((t, traceTree), predicate), unifying), errs), srcs), subs), _) =
54+ let (((((((t, traceTree), predicate), unifying), errs), _srcs), subs), _) =
5555 run
56+ . evalState @(MKM.Map Pred) mempty
57+ . interpret @(Writer Pred) (\(Tell x) -> modify (<> MKM.singleton x))
5658 . evalState (M.empty :: VariableMap)
5759 . runConstraintEnv
5860 . runState @[(TypeVariable, SrcSpan)] []
@@ -66,7 +68,7 @@ getType r =
6668 in (sub subs t, errs, unifying, predicate, traceTree)
6769
6870runConstraintEnv ::
69− Member (State VariableMap) effs =>
71+ Members '[State VariableMap, State (MKM.Map Pred)] effs =>
7072 Eff (SubstituteEnv : Writer Substitution : Writer Constraint : State (Seq Constraint) : effs) a ->
7173 Eff effs ((a, Substitution), Seq Constraint)
7274runConstraintEnv =
@@ -79,6 +81,7 @@ runConstraintEnv =
7981 -- TODO: I have a feeling that variables in the env should already be closed over.
8082 -- (aka this is redundant)
8183 modify @VariableMap (sub x <$>)
84+ modify @(MKM.Map Pred) (sub x)
8285 tell x
8386 return ()
8487 )
@@ -89,53 +92,12 @@ data SubstituteEnv a where
8992subEnv :: Member SubstituteEnv r => Substitution -> Eff r ()
9093subEnv = send . SubstituteEnv
9194
92−data Constraint = !Scheme :~ !Scheme
95+data Constraint = !NType :~ !NType
9396 deriving stock (Eq, Ord, Show)
9497
9598instance Pretty Constraint where
9699 pretty (x :~ y) = pretty x <+> "~" <+> pretty y
97100
98−newtype DeBruijnContext = DeBruijnContext (Sum Int)
99− deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
100−
101−instance Act DeBruijnContext DeBruijn where
102− act (DeBruijnContext (Sum n)) (DeBruijn i j) = DeBruijn (i + n) j
103−
104−type TDeBruijnMap = ShiftedMap DeBruijnContext TypeVariable DeBruijn
105−
106−close :: Predicate TypeVariable -> Scheme -> Scheme
107−close (Predicate f) =
108− run
109− . evalState @TDeBruijnMap mempty
110− . runReader @Int 0
111− . evalState @Int 0
112− . close'
113− where
114− -- State is the sequential number, Reader is the binding context number
115− close' :: Scheme -> Eff '[State Int, Reader Int, State TDeBruijnMap] Scheme
116− close' =
117− traverseNTypesWith bndCtx %%~ \case
118− x@(TBruijn _) -> return x
119− x@(TAtomic _) -> return x
120− (TTypeVariable tv) | f tv -> TBruijn <$> newbruijn tv
121− x@(TTypeVariable _) -> return x
122−
123− bndCtx m = do
124− modify @TDeBruijnMap (SM.shift 1)
125− x <- local @Int (+ 1) m
126− modify @TDeBruijnMap (SM.shift (-1))
127− return x
128− newbruijn t = do
129− get @TDeBruijnMap <&> SM.lookup t >>= \case
130− Nothing -> do
131− i <- ask
132− j <- get
133− modify @Int (+ 1)
134− let x = DeBruijn i j
135− modify @TDeBruijnMap (SM.insert t x)
136− return x
137− Just x -> return x
138−
139101class Free s where
140102 free :: s -> Set TypeVariable
141103 sub :: Substitution -> s -> s
@@ -150,7 +112,9 @@ instance Free NType where
150112
151113 sub s r = case r of
152114 NBruijn _ -> r
153− NTypeVariable x -> NTypeVariable x -- it should be substituted higher in Scheme
115+ NTypeVariable x -> case M.lookup x $ unSubstitution s of
116+ Nothing -> NTypeVariable x
117+ Just t -> t
154118 List x -> List $ sub s x
155119 NAttrSet m -> NAttrSet $ sub s <$> m
156120 x :-> y -> sub s x :-> sub s y
@@ -162,25 +126,12 @@ instance Free Preds where
162126 x `HasField` (_, y) -> free x <> free y
163127 sub s (Preds ps) =
164128 Preds $
165− ps >>= \case
166− Update x y z ->
167− let (a, x') = sub' x
168− (b, y') = sub' y
169− (c, z') = sub' z
170− in Update x' y' z' : unPreds (a <> b <> c)
171− HasField t (f, v) ->
172− let (a, t') = sub' t
173− in HasField t' (f, sub s v) : unPreds a
174− where
175− sub' t = case sub s (scheme t) of
176− pp :=> t' -> (pp, t')
129+ ps <&> \case
130+ Update x y z -> Update (sub s x) (sub s y) (sub s z)
131+ HasField t (f, v) -> HasField (sub s t) (f, sub s v)
177132
178133instance Free Scheme where
179134 free (x :=> y) = free x <> free y
180− sub s (x :=> NTypeVariable tv) =
181− case M.lookup tv $ unSubstitution s of
182− Nothing -> sub s x :=> NTypeVariable tv
183− Just (newCs :=> new) -> (sub s x <> newCs) :=> new
184135 sub s (x :=> y) = sub s x :=> sub s y
185136
186137instance Free a => Free [a] where
@@ -195,7 +146,15 @@ instance (Free a, Free b) => Free (a, b) where
195146 free (a, b) = free a <> free b
196147 sub s (a, b) = (sub s a, sub s b)
197148
198−newtype Substitution = Substitution {unSubstitution :: Map TypeVariable Scheme}
149+instance Free (MKM.Map Pred) where
150+ free = MKM.keys
151+ sub subs@(Substitution s) mkm@(MKM.Map m _) = m'
152+ where
153+ vals = S.toList . fold . M.elems $ M.restrictKeys m (M.keysSet s)
154+ f = appEndo $ foldMap (Endo . MKM.delete) vals
155+ m' = f mkm <> MKM.fromList (unPreds . sub subs $ Preds vals)
156+
157+newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
199158 deriving newtype (Eq, Ord, Show)
200159 deriving stock (Data)
201160
@@ -215,9 +174,9 @@ instance Free Constraint where
215174
216175(<<-) ::
217176 TypeVariable ->
218− Scheme ->
177+ NType ->
219178 UnifyM Substitution
220−v <<- ([] :=> NTypeVariable x) | v == x = return mempty
179+v <<- (NTypeVariable x) | v == x = return mempty
221180v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty
222181 where
223182 occursIn :: Free x => TypeVariable -> x -> Bool
@@ -227,65 +186,47 @@ v <<- x = return $ Substitution $ M.singleton v x
227186unifyWithPriority ::
228187 -- | The range of type variables to interpret as being lower
229188 -- priority (try to replace them if possible)
230− RS.RSet TypeVariable ->
189+ Predicate TypeVariable ->
231190 Constraint ->
232191 UnifyM Substitution
233−unifyWithPriority range (lhs :~ rhs) =
192+unifyWithPriority f (lhs :~ rhs) =
234193 case (lhs, rhs) of
235− (_ :=> NAtomic x, _ :=> NAtomic y) | x == y -> return mempty
236− (xcs :=> NTypeVariable x, ycs :=> NTypeVariable y) -> do
237− let ((lhsCs, lhs'), (rhsCs, rhs')) =
238− if y `RS.member` range
239− then ((ycs, y), (xcs, x))
240− else ((xcs, x), (ycs, y))
241− extraCs = replacing lhs' (scheme . NTypeVariable $ rhs') lhsCs
242− newScheme = (extraCs <> rhsCs) :=> NTypeVariable rhs'
243− -- This might come back to bite me.
244− (<> (Substitution $ M.singleton rhs' newScheme)) <$> (lhs' <<- newScheme)
245− (cs :=> NTypeVariable t, x) -> t <<- (replacing t x cs =>> x)
246− (x, cs :=> NTypeVariable t) -> t <<- (replacing t x cs =>> x)
247− (xcs :=> List x, ycs :=> List y) ->
248− unifyWithPriority range $ (xcs =>> x) :~ (ycs =>> y)
249− (Preds xcs :=> NAttrSet x, Preds ycs :=> NAttrSet y) ->
250− -- TODO: what to do with predicates ?
251− -- I don't think there should be any predicates here...
252− assert (null xcs && null ycs) $
253− foldr (\c s -> s >>= \s' -> (<> s') <$> unifyWithPriority range (sub s' c)) (pure mempty)
254− . M.elems
255− $ M.intersectionWith (:~) x y
256− (Preds xcs :=> (x1 :-> y1), Preds ycs :=> (x2 :-> y2)) -> do
257− s <- unifyWithPriority range (x1 :~ x2)
258− s' <- unifyWithPriority range $ sub s $ y1 :~ y2
259− let ss = s' <> s
260− -- I don't think there should be any predicates here either...
261− -- s'' <- uncurry unifyPred . sub ss $ (xcs, ycs)
262− assert (null xcs && null ycs) $ return ss
194+ (NAtomic x, NAtomic y) | x == y -> return mempty
195+ (NTypeVariable x, NTypeVariable y) -> do
196+ if getPredicate f y
197+ then y <<- NTypeVariable x
198+ else x <<- NTypeVariable y
199+ (NTypeVariable t, x) -> t <<- x
200+ (x, NTypeVariable t) -> t <<- x
201+ (List x, List y) -> unifyWithPriority f $ x :~ y
202+ (NAttrSet _x, NAttrSet _y) -> error "TODO: This should be handled in a special way"
203+ -- foldr (\c s -> s >>= \s' -> (<> s') <$> unifyWithPriority f (sub s' c)) (pure mempty)
204+ -- . M.elems
205+ -- $ M.intersectionWith (:~) x y
206+ (x1 :-> y1, x2 :-> y2) -> do
207+ s <- unifyWithPriority f (x1 :~ x2)
208+ s' <- unifyWithPriority f $ sub s $ y1 :~ y2
209+ return $ s' <> s
263210 (x, y) -> tell (CanNotUnify x y) >> return mempty
264211
265−replacing :: Free x => TypeVariable -> Scheme -> x -> x
266−replacing tv t x =
267− let s = Substitution $ M.singleton tv t
268− in sub s x
269−
270212solve :: Seq Constraint -> UnifyM Substitution
271−solve = solveWithPriority RS.empty
213+solve = solveWithPriority mempty
272214
273215solveWithPriority ::
274216 -- | The range of type variables to interpret as being lower
275217 -- priority (try to replace them if possible)
276− RS.RSet TypeVariable ->
218+ Predicate TypeVariable ->
277219 Seq Constraint ->
278220 UnifyM Substitution
279221solveWithPriority _ Empty = return mempty
280−solveWithPriority range (rest :|> c) = do
281− s <- unifyWithPriority range c
222+solveWithPriority f (rest :|> c) = do
223+ s <- unifyWithPriority f c
282224 -- TODO: This should probably be (s <>)
283− (<> s) <$> solveWithPriority range (fmap (sub s) rest)
225+ (<> s) <$> solveWithPriority f (fmap (sub s) rest)
284226
285227data Errors
286228 = UndefinedVariable VarName
287229 | UnexpectedType {expected :: Scheme, got :: Scheme}
288− | KeyNotPresent' Text
289230 deriving stock (Eq, Ord, Show)
290231
291232freshSrc ::
@@ -298,8 +239,8 @@ freshSrc = do
298239 return v
299240
300241data UnifyingError
301− = InfinityType Scheme
302− | CanNotUnify Scheme Scheme
242+ = InfinityType NType
243+ | CanNotUnify NType NType
303244 deriving stock (Eq, Show)
304245
305246data PredicateError
@@ -315,6 +256,8 @@ type InferEffs =
315256 Writer Constraint,
316257 Writer (SrcSpan, Errors),
317258 Writer PredicateError,
259+ Writer Pred,
260+ State (MKM.Map Pred),
318261 State VariableMap,
319262 Writer UnifyingError,
320263 SubstituteEnv,
@@ -349,7 +292,7 @@ throwSrcTV e = do
349292
350293type VariableMap = Map VarName Scheme
351294
352−(~~) :: Member (Writer Constraint) r => Scheme -> Scheme -> Eff r ()
295+(~~) :: Member (Writer Constraint) r => NType -> NType -> Eff r ()
353296lhs ~~ rhs = tell $ lhs :~ rhs
354297
355298-- TODO: shadowed bindings are not properly restored.
@@ -366,20 +309,25 @@ withBindings bindings m = do
366309
367310instantiate ::
368311 forall effs.
369− Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] effs =>
312+ Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan), Writer Pred] effs =>
370313 Scheme ->
371− Eff effs Scheme
372−instantiate = evalState M.empty . instantiateScheme
314+ Eff effs NType
315+instantiate s = do
316+ (Preds cs :=> t) <- runReader 0 . evalState M.empty . instantiateScheme $ s
317+ tell `traverse_` cs
318+ return t
373319 where
374− instantiateScheme :: forall. Scheme -> Eff (State (Map DeBruijn TypeVariable) ': effs) Scheme
320+ instantiateScheme :: forall. Scheme -> Eff (State (Map DeBruijn TypeVariable) ': Reader Int ': effs) Scheme
375321 instantiateScheme =
376− traverseNTypes %%~ \case
322+ traverseNTypesWith (local @Int (+ 1)) %%~ \case
377323 (TBruijn db) -> TTypeVariable <$> freshInst db
378324 x@(TAtomic _) -> return x
379325 x@(TTypeVariable _) -> return x
380326
381− freshInst :: DeBruijn -> Eff (State (Map DeBruijn TypeVariable) ': effs) TypeVariable
382− freshInst db = do
327+ freshInst :: DeBruijn -> Eff (State (Map DeBruijn TypeVariable) ': Reader Int ': effs) TypeVariable
328+ freshInst (DeBruijn i j) = do
329+ x <- ask @Int
330+ let db = DeBruijn (i - x) j
383331 gets (M.lookup db) >>= \case
384332 Just t -> return t
385333 Nothing -> do
@@ -387,17 +335,17 @@ instantiate = evalState M.empty . instantiateScheme
387335 modify (M.insert db t)
388336 return t
389337
390−infer :: NExprLoc -> InferM Scheme
338+infer :: NExprLoc -> InferM NType
391339infer (Fix (Compose (Ann src x))) = runReader src $ case x of
392− NConstant a -> return . scheme . NAtomic $ case a of
340+ NConstant a -> return . NAtomic $ case a of
393341 NURI {} -> URI
394342 NInt {} -> Integer
395343 NFloat {} -> Float
396344 NBool {} -> Bool
397345 NNull {} -> Null
398− NLiteralPath {} -> return . scheme . NAtomic $ Path
399− NEnvPath {} -> return . scheme . NAtomic $ Path
400− NStr {} -> return $ scheme $ NAtomic String
346+ NLiteralPath {} -> return . NAtomic $ Path
347+ NEnvPath {} -> return . NAtomic $ Path
348+ NStr {} -> return $ NAtomic String
401349 NSym var ->
402350 get @VariableMap
403351 >>= maybe (scheme . NTypeVariable <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
@@ -406,8 +354,8 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
406354 xs' <- traverse infer xs
407355 traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')
408356 case xs' of
409− [] -> scheme . NTypeVariable <$> freshSrc
410− y : _ -> return . scheme $ List y
357+ [] -> NTypeVariable <$> freshSrc
358+ y : _ -> return $ List y
411359 NUnary NNeg y -> do
412360 t <- infer y
413361 -- TODO: Infer either Float or Integer
@@ -415,24 +363,25 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
415363 return t
416364 NUnary NNot y -> do
417365 t <- infer y
418− t ~~ scheme (NAtomic Bool)
366+ t ~~ NAtomic Bool
419367 return t
420368 NBinary NUpdate lhs rhs -> do
421369 lhsT <- infer lhs
422370 rhsT <- infer rhs
423− res <- scheme . NTypeVariable <$> freshSrc
424− return $ [lhsT // rhsT $ res] =>> res
371+ res <- NTypeVariable <$> freshSrc
372+ tell (lhsT // rhsT $ res)
373+ return res
425374 NBinary NApp lhs rhs -> do
426375 lhst <- infer lhs
427376 rhst <- infer rhs
428− rest <- scheme . NTypeVariable <$> freshSrc
429− lhst ~~ (scheme $ rhst :-> rest)
377+ rest <- NTypeVariable <$> freshSrc
378+ lhst ~~ (rhst :-> rest)
430379 return rest
431380 NBinary NConcat lhs rhs -> do
432381 lhst <- infer lhs
433382 rhst <- infer rhs
434− t <- scheme . NTypeVariable <$> freshSrc
435− let listt = scheme $ List t
383+ t <- NTypeVariable <$> freshSrc
384+ let listt = List t
436385 lhst ~~ listt
437386 rhst ~~ listt
438387 return $ listt
@@ -453,7 +402,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
453402 setT <- infer r
454403 path <- getPath path'
455404 resT <-
456− scheme . NTypeVariable <$> case path of
405+ NTypeVariable <$> case path of
457406 Just p -> do
458407 (set', var) <- lookupAttrSet p
459408 setT ~~ set'
@@ -466,7 +415,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
466415 defT <- infer defR
467416 defT ~~ resT
468417 return resT
469− NSet NNonRecursive xs -> scheme . NAttrSet <$> inferBinding xs
418+ NSet NNonRecursive xs -> NAttrSet <$> inferBinding xs
470419 NHasAttr attrSet path -> do
471420 setT <- infer attrSet
472421 -- this should infer optional type
@@ -475,66 +424,66 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
475424 (paramT, varMap :: VariableMap) <- case param of
476425 Param name -> do
477426 t <- freshSrc
478− return (scheme $ NTypeVariable t, M.singleton name . scheme $ NTypeVariable t)
427+ return (NTypeVariable t, M.singleton name . scheme $ NTypeVariable t)
479428 ParamSet set variadic binding -> do
480429 setBindings <-
481430 M.fromList <$> set
482431 `for` ( \(name, def) -> do
483432 t <- case def of
484− Nothing -> scheme . NTypeVariable <$> freshSrc
433+ Nothing -> NTypeVariable <$> freshSrc
485434 Just def' -> infer def'
486− return (name, t)
435+ return (name, scheme t) -- TODO: This is bad: it probably shouldn't be a scheme
487436 )
488− let setT = scheme . NAttrSet $ setBindings
489− return (setT, maybe M.empty (`M.singleton` setT) binding <> setBindings)
437+ let setT = NAttrSet $ setBindings
438+ return (setT, maybe M.empty (`M.singleton` scheme setT) binding <> setBindings)
490439 bodyT <- withBindings varMap $ infer body
491− return . scheme $ paramT :-> bodyT
440+ return $ paramT :-> bodyT
492441 NLet bindings body -> do
493442 bindingsT <- inferBinding bindings
494443 withBindings bindingsT $ infer body
495444 NIf cond t f -> do
496445 condT <- infer cond
497− condT ~~ scheme (NAtomic Bool)
446+ condT ~~ NAtomic Bool
498447 tT <- infer t
499448 fT <- infer f
500449 tT ~~ fT
501450 return tT
502− NWith set body -> do
503− -- TODO: implement fallback variable lookup -> specify that the set should have the key.
504− setT <- infer set
505− vars <- expectAttrSet setT
506− withBindings vars $ infer body
507− where
508− -- Deprecated
509− expectAttrSet ::
510− Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r =>
511− Scheme ->
512− Eff r VariableMap
513− expectAttrSet (_ :=> NAttrSet x) = return x
514− expectAttrSet g = do
515− throwSrc
516− UnexpectedType
517− { expected = scheme $ NAttrSet M.empty,
518− got = g
519− }
520− return M.empty
451+ -- NWith set body -> do
452+ -- -- TODO: implement fallback variable lookup -> specify that the set should have the key.
453+ -- setT <- infer set
454+ -- vars <- expectAttrSet setT
455+ -- withBindings vars $ infer body
456+ -- where
457+ -- -- Deprecated
458+ -- expectAttrSet ::
459+ -- Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r =>
460+ -- Scheme ->
461+ -- Eff r VariableMap
462+ -- expectAttrSet (_ :=> NAttrSet x) = return x
463+ -- expectAttrSet g = do
464+ -- throwSrc
465+ -- UnexpectedType
466+ -- { expected = scheme $ NAttrSet M.empty,
467+ -- got = g
468+ -- }
469+ -- return M.empty
521470 NAssert cond body -> do
522471 condT <- infer cond
523− condT ~~ scheme (NAtomic Bool)
472+ condT ~~ NAtomic Bool
524473 infer body
525− NSynHole _ -> scheme . NTypeVariable <$> freshSrc
474+ NSynHole _ -> NTypeVariable <$> freshSrc
526475 where
527476 equality lhs rhs = do
528477 lhst <- infer lhs
529478 rhst <- infer rhs
530479 lhst ~~ rhst
531− return . scheme $ NAtomic Bool
480+ return $ NAtomic Bool
532481 comparison lhs rhs = do
533482 lhst <- infer lhs
534483 rhst <- infer rhs
535484 -- TODO: Infer lhst and rhst are either Integer or Double or String
536485 lhst ~~ rhst
537− return . scheme $ NAtomic Bool
486+ return $ NAtomic Bool
538487 math lhs rhs = do
539488 lhst <- infer lhs
540489 rhst <- infer rhs
@@ -544,9 +493,9 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
544493 logic lhs rhs = do
545494 lhst <- infer lhs
546495 rhst <- infer rhs
547− rhst ~~ scheme (NAtomic Bool)
548− lhst ~~ scheme (NAtomic Bool)
549− return . scheme $ NAtomic Bool
496+ rhst ~~ NAtomic Bool
497+ lhst ~~ NAtomic Bool
498+ return $ NAtomic Bool
550499
551500inferBinding :: [Binding (Fix NExprLocF)] -> InferM' (Map VarName Scheme)
552501inferBinding bindings = do
@@ -588,29 +537,81 @@ renderPretty = renderLazy . layoutPretty defaultLayoutOptions . pretty
588537showExpr :: Fix NExprLocF -> Text
589538showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.group . prettyNix . stripAnnotation
590539
591−-- TODO: There is no need to solve predicates in types that have already been closed.
592540inferGeneral :: NExprLoc -> InferM Scheme
593−inferGeneral x = traceSubtree (showExpr x) $ do
594− (((t, subs), cs), range) <-
595− traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ infer x
596− traceSubtree "received" $ do
597− traceValue "type" $ renderPretty t
598− traceValue "substitutions" $ prettySubstitution subs
599− traceValue "constraints" $ fmap renderPretty cs
600− traceValue "range" $ T.pack . show $ range
601− s' <- solveWithPriority range cs
602− traceValue "substitutions_after_solving" $ prettySubstitution s'
603− let s = subs <> s'
604− returnedS = Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution $ s
605− traceSubtree "returned" $ do
606− traceValue "substitutions" $ prettySubstitution returnedS
607− -- Filter for optimization purposes
608− subEnv returnedS
609− let retT = close (Predicate (`RS.member` range) <> Predicate (`S.notMember` free returnedS)) $ sub s t
610− traceValue "type" $ renderPretty retT
611− return retT
612−
613−solveConstraints :: Preds -> InferM Preds
541+inferGeneral x@(Fix (Compose (Ann src _))) = runReader src $
542+ traceSubtree (showExpr x) $ do
543+ (((t, subs), cs), range) <-
544+ traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ infer x
545+ traceSubtree "received" $ do
546+ traceValue "type" $ renderPretty t
547+ traceValue "substitutions" $ prettySubstitution subs
548+ traceValue "constraints" $ fmap renderPretty cs
549+ traceValue "range" $ T.pack . show $ range
550+ get @(MKM.Map Pred) >>= traceValue "preds" . showPreds
551+ s' <- solveWithPriority (Predicate (`RS.member` range)) cs
552+ traceValue "substitutions_after_solving" $ prettySubstitution s'
553+ let s = subs <> s'
554+ returnedS = Substitution . M.filterWithKey (\k _ -> k `RS.notMember` range) . unSubstitution $ s
555+ traceSubtree "returned" $ do
556+ traceValue "substitutions" $ prettySubstitution returnedS
557+ -- Filter for optimization purposes
558+ subEnv returnedS
559+ preds <- get @(MKM.Map Pred)
560+ traceValue "subbed_preds" $ showPreds preds
561+ let p = Predicate (`RS.member` range) <> Predicate (`S.notMember` free returnedS)
562+ (MKM.toList -> keep, toss) = MKM.partition (getPredicate p) preds
563+ -- At this point the only predicates only contain type variables that are only used
564+ -- in the expression. This means that all of the generated constraints and
565+ -- substitutions can be safely restricted to this expression.
566+ retT <- solveAndClose p $ sub s $ Preds keep :=> t
567+ traceValue "preds" $ showPreds toss
568+ put toss
569+ traceValue "type" $ renderPretty retT
570+ return retT
571+ where
572+ showPreds :: MKM.Map Pred -> Map String String
573+ showPreds = M.mapKeys show . fmap show . MKM.toMap
574+
575+solveAndClose ::
576+ Members
577+ '[ Writer (TypeVariable, SrcSpan),
578+ Reader SrcSpan,
579+ Fresh,
580+ Writer PredicateError,
581+ Writer UnifyingError
582+ ]
583+ eff =>
584+ Predicate TypeVariable ->
585+ Scheme ->
586+ Eff eff Scheme
587+solveAndClose p (cs :=> t) = do
588+ (((Preds solvedPreds, range), constraints), collectedPreds) <-
589+ runSeqWriter @[Pred]
590+ . runSeqWriter @(Seq Constraint)
591+ . registerTypeVariables
592+ $ solveConstraints cs
593+ let newPredicate = p `pOr` Predicate (`RS.member` range)
594+ case (constraints, collectedPreds) of
595+ (Empty, []) -> return . close newPredicate $ Preds solvedPreds :=> t
596+ _ -> do
597+ s <- solveWithPriority newPredicate constraints
598+ solveAndClose newPredicate $ sub s $ Preds (collectedPreds <> solvedPreds) :=> t
599+
600+pOr :: Predicate x -> Predicate x -> Predicate x
601+pOr (Predicate f) (Predicate g) = Predicate $ \x -> f x || g x
602+
603+solveConstraints ::
604+ Members
605+ '[ Fresh,
606+ Reader SrcSpan,
607+ Writer (TypeVariable, SrcSpan),
608+ Writer Pred,
609+ Writer PredicateError,
610+ Writer Constraint
611+ ]
612+ effs =>
613+ Preds ->
614+ Eff effs Preds
614615solveConstraints (Preds ps) =
615616 Preds <$> do
616617 flip Control.Monad.filterM ps $ \case
@@ -619,17 +620,60 @@ solveConstraints (Preds ps) =
619620 tell $ KeyNotPresent f (NAttrSet ts)
620621 return False
621622 Just t' -> do
622− t ~~ t'
623+ x <- instantiate t
624+ y <- instantiate t'
625+ x ~~ y
623626 return False
624627 HasField (NTypeVariable _) _ -> return True
625628 HasField t _ -> do
626629 tell $ NotAnAttributeSet t
627630 return False
628631 (Update (NAttrSet a) (NAttrSet b) t) -> do
629− scheme (NAttrSet $ b <> a) ~~ scheme t
632+ (NAttrSet $ b <> a) ~~ t
630633 return False
631634 _ -> return True
632635
636+newtype DeBruijnContext = DeBruijnContext (Sum Int)
637+ deriving newtype (Eq, Ord, Show, Semigroup, Monoid, Group, Num)
638+
639+instance Act DeBruijnContext DeBruijn where
640+ act (DeBruijnContext (Sum n)) (DeBruijn i j) = DeBruijn (i + n) j
641+
642+type TDeBruijnMap = ShiftedMap DeBruijnContext TypeVariable DeBruijn
643+
644+close :: Data x => Predicate TypeVariable -> x -> x
645+close (Predicate f) =
646+ run
647+ . evalState @TDeBruijnMap mempty
648+ . runReader @Int 0
649+ . evalState @Int 0
650+ . close'
651+ where
652+ -- State is the sequential number, Reader is the binding context number
653+ -- close' :: NType -> Eff '[State Int, Reader Int, State TDeBruijnMap] NType
654+ close' =
655+ traverseNTypesWith bndCtx %%~ \case
656+ x@(TBruijn _) -> return x
657+ x@(TAtomic _) -> return x
658+ (TTypeVariable tv) | f tv -> TBruijn <$> newbruijn tv
659+ x@(TTypeVariable _) -> return x
660+
661+ bndCtx m = do
662+ modify @TDeBruijnMap (SM.shift 1)
663+ x <- local @Int (+ 1) m
664+ modify @TDeBruijnMap (SM.shift (-1))
665+ return x
666+ newbruijn t = do
667+ get @TDeBruijnMap <&> SM.lookup t >>= \case
668+ Nothing -> do
669+ i <- ask
670+ j <- get
671+ modify @Int (+ 1)
672+ let x = DeBruijn i j
673+ modify @TDeBruijnMap (SM.insert t x)
674+ return x
675+ Just x -> return x
676+
633677-- | Stacks functions recursively inside each other
634678-- >>> stack [f1, f2, f3] h x
635679-- f1 (h $ f2 (h $ f3 x))
@@ -677,16 +721,19 @@ lookupAttrSet ::
677721 '[ Reader SrcSpan,
678722 Writer (SrcSpan, Errors),
679723 Writer (TypeVariable, SrcSpan),
724+ Writer Pred,
680725 Fresh
681726 ]
682727 r =>
683728 AttrSetPath ->
684− Eff r (Scheme, TypeVariable)
729+ Eff r (NType, TypeVariable)
685730lookupAttrSet (p :| []) = do
686731 set <- NTypeVariable <$> freshSrc
687732 var <- freshSrc
688− return ([HasField set (p, scheme . NTypeVariable $ var)] :=> set, var)
733+ tell (HasField set (p, scheme . NTypeVariable $ var))
734+ return (set, var)
689735lookupAttrSet (p :| (pp : ps)) = do
690736 set <- NTypeVariable <$> freshSrc
691737 (innerSet, var) <- lookupAttrSet (pp :| ps)
692− return ([HasField set (p, innerSet)] :=> set, var)
738+ tell $ HasField set (p, scheme innerSet)
739+ return (set, var)