@@ -26,7 +26,6 @@ import Data.Functor
2626import Data.Functor.Contravariant
2727import Data.Group hiding ((~~))
2828import Data.List.NonEmpty (NonEmpty (..))
29−import qualified Data.List.NonEmpty as NE
3029import Data.Map.Shifted.Strict (ShiftedMap (..))
3130import qualified Data.Map.Shifted.Strict as SM
3231import Data.Map.Strict (Map)
@@ -49,9 +48,9 @@ import Nix.Expr
4948import Nix.Pretty
5049import Tix.Types
5150
52−getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [UnifyingError], A.Object)
51+getType :: NExprLoc -> (Scheme, [(SrcSpan, Errors)], [UnifyingError], [PredicateError], A.Object)
5352getType r =
54− let ((((((t, traceTree), unifying), errs), srcs), subs), _) =
53+ let (((((((t, traceTree), predicate), unifying), errs), srcs), subs), _) =
5554 run
5655 . evalState (M.empty :: VariableMap)
5756 . runConstraintEnv
@@ -59,10 +58,11 @@ getType r =
5958 . interpret @(Writer (TypeVariable, SrcSpan)) (\(Tell x) -> modify (x :))
6059 . runSeqWriter @[(SrcSpan, Errors)]
6160 . runSeqWriter @[UnifyingError]
61+ . runSeqWriter @[PredicateError]
6262 . runFresh
6363 . runTreeTracer
6464 $ inferGeneral r
65− in (sub subs t, errs, unifying, traceTree)
65+ in (sub subs t, errs, unifying, predicate, traceTree)
6666
6767runConstraintEnv ::
6868 Member (State VariableMap) effs =>
@@ -157,13 +157,11 @@ instance Free NType where
157157 NAttrSet m -> NAttrSet $ sub s <$> m
158158 x :-> y -> sub s x :-> sub s y
159159
160−instance Free Pred
161−
162−-- free (x `Update` y) = free x <> free y
163−-- free (x `HasField` (_, y)) = free x <> free y
164−
165−-- sub s (x `Update` y) = sub s x `Update` sub s y
166−-- sub s (x `HasField` (t, y)) = sub s x `HasField` (t, sub s y)
160+instance Free Pred where
161+ free (Update x y z) = free x <> free y <> free z
162+ free (x `HasField` (_, y)) = free x <> free y
163+ sub s (Update x y z) = Update (sub s x) (sub s y) (sub s z)
164+ sub s (x `HasField` (t, y)) = sub s x `HasField` (t, sub s y)
167165
168166instance Free Scheme where
169167 free (x :=> y) = free x <> free y
@@ -230,17 +228,13 @@ unifyWithPriority range (lhs :~ rhs) =
230228 lhs' <<- (rhsCs :=> NTypeVariable rhs') -- This might be wrong
231229 (_ :=> NTypeVariable t, x) -> t <<- x
232230 (x, _ :=> NTypeVariable t) -> t <<- x
233− (xcs :=> List x, ycs :=> List y) -> do
234− s <- unifyWithPriority range $ x :~ y
235− s' <- uncurry unifyPred . sub s $ (xcs, ycs)
236− return $ s <> s'
237− (xcs :=> NAttrSet x, ycs :=> NAttrSet y) -> do
238− s <-
239− foldr (\c s -> s >>= \s' -> (<> s') <$> unifyWithPriority range (sub s' c)) (pure mempty)
240− . M.elems
241− $ M.intersectionWith (:~) x y
242− s' <- uncurry unifyPred . sub s $ (xcs, ycs)
243− return $ s <> s'
231+ (xcs :=> List x, ycs :=> List y) ->
232+ unifyWithPriority range $ (xcs =>> x) :~ (ycs =>> y)
233+ (_xcs :=> NAttrSet x, _ycs :=> NAttrSet y) ->
234+ -- TODO: what to do with predicates ?
235+ foldr (\c s -> s >>= \s' -> (<> s') <$> unifyWithPriority range (sub s' c)) (pure mempty)
236+ . M.elems
237+ $ M.intersectionWith (:~) x y
244238 (xcs :=> (x1 :-> y1), ycs :=> (x2 :-> y2)) -> do
245239 s <- unifyWithPriority range (x1 :~ x2)
246240 s' <- unifyWithPriority range $ sub s $ y1 :~ y2
@@ -250,8 +244,7 @@ unifyWithPriority range (lhs :~ rhs) =
250244 (x, y) -> tell (CanNotUnify x y) >> return mempty
251245
252246unifyPred :: [Pred] -> [Pred] -> UnifyM Substitution
253−unifyPred [] [] = return mempty
254−unifyPred _ _ = undefined
247+unifyPred _xs _ys = pure mempty
255248
256249solve :: Seq Constraint -> UnifyM Substitution
257250solve = solveWithPriority RS.empty
@@ -273,7 +266,7 @@ occursIn t x = t `S.member` free x
273266data Errors
274267 = UndefinedVariable VarName
275268 | UnexpectedType {expected :: Scheme, got :: Scheme}
276− | KeyNotPresent Text
269+ | KeyNotPresent' Text
277270 deriving stock (Eq, Ord, Show)
278271
279272freshSrc ::
@@ -290,6 +283,11 @@ data UnifyingError
290283 | CanNotUnify Scheme Scheme
291284 deriving stock (Eq, Show)
292285
286+data PredicateError
287+ = KeyNotPresent Text NType
288+ | NotAnAttributeSet NType
289+ deriving stock (Eq, Show)
290+
293291type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x
294292
295293type InferEffs =
@@ -297,6 +295,7 @@ type InferEffs =
297295 Writer (TypeVariable, SrcSpan),
298296 Writer Constraint,
299297 Writer (SrcSpan, Errors),
298+ Writer PredicateError,
300299 State VariableMap,
301300 Writer UnifyingError,
302301 SubstituteEnv,
@@ -359,8 +358,8 @@ instantiate = evalState M.empty . instantiateScheme
359358
360359 instantiatePred :: forall. Pred -> Eff (State (Map DeBrujin TypeVariable) ': effs) Pred
361360 instantiatePred = \case
362− -- instantiatePred (x `Update` y) = Update <$> instantiate' x <*> instantiate' y
363− -- instantiatePred (x `HasField` (f, y)) = HasField <$> instantiate' x <*> ((f,) <$> instantiate' y)
361+ (Update x y z) -> Update <$> instantiate' x <*> instantiate' y <*> instantiate' z
362+ (x `HasField` (f, y)) -> HasField <$> instantiate' x <*> ((f,) <$> instantiate y)
364363
365364 instantiate' :: forall. NType -> Eff (State (Map DeBrujin TypeVariable) ': effs) NType
366365 instantiate' x@(NTypeVariable _) = return x
@@ -411,11 +410,8 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
411410 NBinary NUpdate lhs rhs -> do
412411 lhsT <- infer lhs
413412 rhsT <- infer rhs
414− lhsT ~~ rhsT
415− lhs' <- expectAttrSet lhsT
416− rhs' <- expectAttrSet rhsT
417− forM_ (M.toList $ M.intersectionWith (,) lhs' rhs') (\(_, (a, b)) -> a ~~ b)
418− return . scheme . NAttrSet $ rhs' <> lhs'
413+ res <- scheme . NTypeVariable <$> freshSrc
414+ return $ [lhsT // rhsT $ res] =>> res
419415 NBinary NApp lhs rhs -> do
420416 lhst <- infer lhs
421417 rhst <- infer rhs
@@ -446,19 +442,24 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
446442 NSelect r path' def -> do
447443 setT <- infer r
448444 path <- getPath path'
449− resT <- case path of
450− Just p -> lookupAttrSet p setT
451− Nothing -> scheme . NTypeVariable <$> freshSrc
445+ resT <-
446+ scheme . NTypeVariable <$> case path of
447+ Just p -> do
448+ (set', var) <- lookupAttrSet p
449+ setT ~~ set'
450+ return var
451+ Nothing -> freshSrc
452452 case def of
453453 Nothing -> return ()
454454 Just defR -> do
455+ -- this should infer optional type
455456 defT <- infer defR
456457 defT ~~ resT
457458 return resT
458459 NSet NNonRecursive xs -> scheme . NAttrSet <$> inferBinding xs
459460 NHasAttr attrSet path -> do
460461 setT <- infer attrSet
461− expectAttrSet setT
462+ -- this should infer optional type
462463 return setT
463464 NAbs param body -> do
464465 (paramT, varMap :: VariableMap) <- case param of
@@ -489,9 +490,24 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
489490 tT ~~ fT
490491 return tT
491492 NWith set body -> do
493+ -- TODO: implement fallback variable lookup -> specify that the set should have the key.
492494 setT <- infer set
493495 vars <- expectAttrSet setT
494496 withBindings vars $ infer body
497+ where
498+ -- Deprecated
499+ expectAttrSet ::
500+ Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r =>
501+ Scheme ->
502+ Eff r VariableMap
503+ expectAttrSet (_ :=> NAttrSet x) = return x
504+ expectAttrSet g = do
505+ throwSrc
506+ UnexpectedType
507+ { expected = scheme $ NAttrSet M.empty,
508+ got = g
509+ }
510+ return M.empty
495511 NAssert cond body -> do
496512 condT <- infer cond
497513 condT ~~ NAtomic Bool
@@ -531,20 +547,30 @@ inferBinding bindings = do
531547 Nothing -> return []
532548 Just name -> do
533549 t <- inferGeneral r
534− return $ [stack ((,) <$> name) (scheme . NAttrSet . uncurry M.singleton) t]
550+ return [stack ((,) <$> name) (scheme . NAttrSet . uncurry M.singleton) t]
535551 Inherit attrSet keys src -> do
536− vars <- case attrSet of
537− Just attr -> do
538− t <- infer attr
539− expectAttrSet t
540− Nothing -> get @VariableMap
541552 names <- catMaybes <$> traverse getKeyName keys
542− return $
543− catMaybes $
544− names <&> \name -> case M.lookup name vars of
545− Nothing -> Nothing
546− Just r -> Just (name, r)
553+ attrSet' <- infer `traverse` attrSet
554+ names' <- for names $ \name ->
555+ fmap (name,) <$> do
556+ case attrSet' of
557+ Just t -> do
558+ (s', var) <- lookupAttrSet (pure name)
559+ s' ~~ t
560+ return $ Just . scheme . NTypeVariable $ var
561+ Nothing -> do
562+ vars <- get @VariableMap
563+ return $ case M.lookup name vars of
564+ Nothing -> Nothing
565+ Just r -> Just r
566+ return $ catMaybes names'
547567 return $ M.fromListWith mergeSetTypes bindings'
568+ where
569+ -- This seems fishy
570+ mergeSetTypes :: Scheme -> Scheme -> Scheme
571+ mergeSetTypes (xcs :=> NAttrSet ks) (ycs :=> NAttrSet ks') =
572+ (xcs <> ycs) :=> NAttrSet (M.unionWith mergeSetTypes ks ks')
573+ mergeSetTypes _ x = x
548574
549575renderPretty :: Pretty x => x -> TL.Text
550576renderPretty = renderLazy . layoutPretty defaultLayoutOptions . pretty
@@ -555,7 +581,12 @@ showExpr = TL.toStrict . renderLazy . layoutPretty defaultLayoutOptions . P.grou
555581inferGeneral :: NExprLoc -> InferM Scheme
556582inferGeneral x = traceSubtree (showExpr x) $ do
557583 (((t, subs), cs), range) <-
558− traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ infer x
584+ traceSubtree "subexpressions" . registerTypeVariables . runConstraintEnv $ do
585+ infer x >>= \case
586+ (cs :=> t) -> do
587+ cs' <- solveConstraints cs
588+ return $ cs' :=> t
589+ u -> return u
559590 traceSubtree "received" $ do
560591 traceValue "type" $ renderPretty t
561592 traceValue "substitutions" $ prettySubstitution subs
@@ -573,16 +604,24 @@ inferGeneral x = traceSubtree (showExpr x) $ do
573604 traceValue "type" $ renderPretty retT
574605 return retT
575606
576−-- | Deprecated
577−expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => Scheme -> Eff r VariableMap
578−expectAttrSet (_ :=> NAttrSet x) = return x
579−expectAttrSet g = do
580− throwSrc
581− UnexpectedType
582− { expected = scheme $ NAttrSet M.empty,
583− got = g
584− }
585− return M.empty
607+solveConstraints :: [Pred] -> InferM [Pred]
608+solveConstraints ps = do
609+ flip Control.Monad.filterM ps $ \case
610+ HasField (NAttrSet ts) (f, t) -> case M.lookup f ts of
611+ Nothing -> do
612+ tell $ KeyNotPresent f (NAttrSet ts)
613+ return False
614+ Just t' -> do
615+ t ~~ t'
616+ return False
617+ HasField (NTypeVariable _) _ -> return True
618+ HasField t _ -> do
619+ tell $ NotAnAttributeSet t
620+ return False
621+ (Update (NAttrSet a) (NAttrSet b) t) -> do
622+ scheme (NAttrSet $ b <> a) ~~ scheme t
623+ return False
624+ _ -> return True
586625
587626-- | Stacks functions recursively inside each other
588627-- >>> stack [f1, f2, f3] h x
@@ -597,12 +636,6 @@ stack (g :| gs) h x = g $ f gs
597636(>>.=) :: (Applicative f, Monad t, Traversable t) => t a -> (a -> f (t b)) -> f (t b)
598637ta >>.= f = join <$> traverse f ta
599638
600−-- | Deprecated
601−mergeSetTypes :: Scheme -> Scheme -> Scheme
602−mergeSetTypes (xcs :=> NAttrSet ks) (ycs :=> NAttrSet ks') =
603− (xcs <> ycs) :=> NAttrSet (M.unionWith mergeSetTypes ks ks')
604−mergeSetTypes _ x = x
605−
606639-- TODO: process variables
607640antiAntiQuote :: Antiquoted (NString r) r -> Maybe Text
608641antiAntiQuote (Plain s) = unNString s
@@ -632,7 +665,6 @@ getPath path = sequence <$> traverse getKeyName path
632665
633666type AttrSetPath = NonEmpty Text
634667
635−-- | Deprecated
636668lookupAttrSet ::
637669 Members
638670 '[ Reader SrcSpan,
@@ -642,23 +674,12 @@ lookupAttrSet ::
642674 ]
643675 r =>
644676 AttrSetPath ->
645− Scheme ->
646− Eff r Scheme
647−lookupAttrSet path = go (NE.toList path)
648− where
649− go ::
650− Members
651− '[ Reader SrcSpan,
652− Writer (SrcSpan, Errors),
653− Writer (TypeVariable, SrcSpan),
654− Fresh
655− ]
656− r =>
657− [VarName] ->
658− Scheme ->
659− Eff r Scheme
660− go [] x = return x
661− go (p : ps) x = do
662− expectAttrSet x <&> M.lookup p >>= \case
663− Nothing -> scheme . NTypeVariable <$> throwSrcTV (KeyNotPresent p)
664− Just t -> go ps t
677+ Eff r (Scheme, TypeVariable)
678+lookupAttrSet (p :| []) = do
679+ set <- NTypeVariable <$> freshSrc
680+ var <- freshSrc
681+ return ([HasField set (p, scheme . NTypeVariable $ var)] :=> set, var)
682+lookupAttrSet (p :| (pp : ps)) = do
683+ set <- NTypeVariable <$> freshSrc
684+ (innerSet, var) <- lookupAttrSet (pp :| ps)
685+ return ([HasField set (p, innerSet)] :=> set, var)