@@ -28,39 +28,60 @@ import Data.Sequences
2828import Data.Set (Set)
2929import qualified Data.Set as S
3030import Data.Text (Text)
31+import qualified Data.Text.Lazy.Builder as T
3132import Data.Traversable
33+import Debug.Trace
3234import Nix.Atoms
3335import Nix.Expr
3436
35−getType :: NExprLoc -> (Either UnifyingError NType, [(SrcSpan, Errors)])
36−getType exp =
37− let (((t, srcs), cons), errs) =
37+getType :: NExprLoc -> (NType, [(SrcSpan, Errors)], [UnifyingError])
38+getType r =
39+ let ((((t, unifying), srcs), constraints), errs) =
3840 run
3941 . runReader (M.empty :: VariableMap)
4042 . runSeqWriter @[(SrcSpan, Errors)]
4143 . runSeqWriter @(Seq Constraint)
4244 . runSeqWriter @[(TypeVariable, SrcSpan)]
45+ . runSeqWriter @[UnifyingError]
4346 . runFresh
44− $ infer exp
45− s = run . runError @UnifyingError $ solve cons
46− in ((`sub` t) <$> s, errs)
47+ $ getType' r
48+ in (t, errs, unifying)
49+
50+getType' ::
51+ Members
52+ '[ Writer (SrcSpan, Errors),
53+ Reader VariableMap,
54+ Writer (TypeVariable, SrcSpan),
55+ Writer UnifyingError,
56+ Fresh
57+ ]
58+ r =>
59+ NExprLoc ->
60+ Eff r NType
61+getType' r = do
62+ (t, constraints) <-
63+ runSeqWriter @(Seq Constraint) $
64+ infer r
65+ s <- solve (traceShowId constraints)
66+ return . close $ sub s (traceShowId t)
4767
4868newtype TypeVariable = TypeVariable Int
4969 deriving newtype (Show, Eq, Ord)
5070
5171data Constraint = !NType :~ !NType
72+ deriving stock (Eq, Ord, Show)
5273
53−newtype DeBrujin = DeBrujin {unDeBrujin :: Int}
54− deriving newtype (Eq, Ord)
55− deriving stock (Show)
74+data DeBrujin = DeBrujin !Int !Int
75+ deriving stock (Show, Eq, Ord)
5676
5777data NType
5878 = NTypeVariable !TypeVariable
5979 | NBrujin !DeBrujin
6080 | NAtomic !AtomicType
61− | List !NType
62− | NAttrSet !(Map Text NType)
6381 | !NType :-> !NType
82+ | -- These two introduce a new De Brujin binding context
83+ List !NType
84+ | NAttrSet !(Map Text NType)
6485 deriving stock (Eq, Ord, Show)
6586
6687data AtomicType
@@ -73,6 +94,43 @@ data AtomicType
7394 | URI
7495 deriving stock (Eq, Ord, Show)
7596
97+isClosed :: NType -> Bool
98+isClosed (NTypeVariable _) = False
99+isClosed (NBrujin _) = True
100+isClosed (NAtomic _) = True
101+isClosed (x :-> y) = isClosed x && isClosed y
102+isClosed (List x) = isClosed x
103+isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
104+
105+close :: NType -> NType
106+close =
107+ run
108+ . evalState @(Map TypeVariable DeBrujin) M.empty
109+ . runReader @Int 0
110+ . evalState @Int 0
111+ . close'
112+ where
113+ -- State is the sequential number, Reader is the binding context number
114+ close' :: NType -> Eff '[State Int, Reader Int, State (Map TypeVariable DeBrujin)] NType
115+ close' x@(NAtomic _) = return x
116+ close' x@(NBrujin _) = return x
117+ close' (x :-> y) = (:->) <$> close' x <*> close' y
118+ close' (NTypeVariable tv) = NBrujin <$> newbrujin tv
119+ close' (List x) = bndCtx $ List <$> close' x
120+ close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
121+
122+ bndCtx = local @Int (+ 1)
123+ newbrujin t = do
124+ get @(Map TypeVariable DeBrujin) <&> M.lookup t >>= \case
125+ Nothing -> do
126+ i <- ask
127+ j <- get
128+ modify @Int (+ 1)
129+ let x = DeBrujin i j
130+ modify @(Map TypeVariable DeBrujin) (M.insert t x)
131+ return x
132+ Just x -> return x
133+
76134class Free s where
77135 free :: s -> Set TypeVariable
78136
@@ -94,6 +152,7 @@ instance Monoid Substitution where
94152sub :: Substitution -> NType -> NType
95153sub s r = case r of
96154 NAtomic _ -> r
155+ NBrujin _ -> r
97156 NTypeVariable x -> subTV x
98157 List x -> List $ sub s x
99158 NAttrSet m -> NAttrSet $ sub s <$> m
@@ -109,7 +168,7 @@ subCon s (x :~ y) = sub s x :~ sub s y
109168 NType ->
110169 UnifyM Substitution
111170v <<- (NTypeVariable x) | v == x = return mempty
112−v <<- x | v `occursIn` x = throwError $ InfinityType x
171+v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty
113172v <<- x = return $ Substitution $ M.singleton v x
114173
115174unify :: Constraint -> UnifyM Substitution
@@ -127,7 +186,7 @@ unify (lhs :~ rhs) =
127186 s <- unify (x1 :~ x2)
128187 s' <- unify $ subCon s $ y1 :~ y2
129188 return $ s' <> s
130− (x, y) -> throwError $ CanNotUnify x y
189+ (x, y) -> tell (CanNotUnify x y) >> return mempty
131190
132191solve :: Seq Constraint -> UnifyM Substitution
133192solve Empty = return mempty
@@ -156,6 +215,7 @@ data Errors
156215 = UndefinedVariable VarName
157216 | UnexpectedType {expected :: NType, got :: NType}
158217 | KeyNotPresent Text
218+ deriving stock (Eq, Ord, Show)
159219
160220data Fresh x where
161221 Fresh :: Fresh TypeVariable
@@ -188,14 +248,15 @@ data UnifyingError
188248 | CanNotUnify NType NType
189249 deriving stock (Eq, Show)
190250
191−type UnifyM x = forall r. Members '[Error UnifyingError] r => Eff r x
251+type UnifyM x = forall r. Members '[Writer UnifyingError] r => Eff r x
192252
193253type InferEffs =
194254 '[ Fresh,
195255 Writer (TypeVariable, SrcSpan),
196256 Writer Constraint,
197257 Writer (SrcSpan, Errors),
198− Reader VariableMap
258+ Reader VariableMap,
259+ Writer UnifyingError
199260 ]
200261
201262type InferM x = forall r. Members InferEffs r => Eff r x