@@ -24,6 +24,8 @@ import qualified Data.List.NonEmpty as NE
2424import Data.Map.Strict (Map)
2525import qualified Data.Map.Strict as M
2626import Data.MonoTraversable
27+import Data.Range (Range (..))
28+import qualified Data.Range as R
2729import Data.Sequence (Seq (..))
2830import Data.Sequences
2931import Data.Set (Set)
@@ -61,11 +63,11 @@ getType' ::
6163 NExprLoc ->
6264 Eff r NType
6365getType' r = do
64− (t, constraints) <-
65− runSeqWriter @(Seq Constraint) $
66− infer r
67− s <- solve (traceShowId constraints)
68− return . close $ sub s (traceShowId t)
66+ ((t, s'), constraints) <-
67+ runSeqWriter @(Seq Constraint) . runWriter @Substitution $
68+ inferGeneral r
69+ s <- solve (traceShowId . fmap (subCon s') $ constraints)
70+ return . close InfiniteRange $ sub (s <> s') (traceShowId t)
6971
7072newtype TypeVariable = TypeVariable Int
7173 deriving newtype (Show, Eq, Ord)
@@ -85,23 +87,34 @@ variableNames =
8587 <> (fmap (\(n, g) -> g <> T.fromString (show n)) $ zip [1 :: Int ..] greek)
8688
8789showNType :: NType -> Text
88−showNType t = TL.toStrict . T.toLazyText $ showNType' t
90+showNType t = TL.toStrict . T.toLazyText $ showNType' 0 t
8991 where
90− greekVars = M.fromList $ zip (S.toList $ getDeBurjins t) variableNames
91− showNType' :: NType -> T.Builder
92− showNType' (NAtomic a) = showAtomicType a
93− showNType' (NBrujin b) = greekVars M.! b
94− showNType' (NTypeVariable _) = error "should not have free type variables at this point"
95− showNType' (x :-> y) = showNType' x <> " -> " <> showNType' y
96− showNType' (List x) = "[" <> showNType' x <> "]"
97− showNType' (NAttrSet x) =
98− "AttrSet {"
99− <> ( mconcat
100− . intersperse "; "
101− . fmap (\(k, v) -> T.fromText k <> " :: " <> showNType' v)
102− $ M.toList x
103− )
104− <> "}"
92+ greekVars = M.fromList . traceShowId $ zip (S.toList $ getAllDeBurjins t) variableNames
93+ showNType' :: Int -> NType -> T.Builder
94+ showNType' depth u =
95+ foralls <> case u of
96+ (NAtomic a) -> showAtomicType a
97+ (NBrujin (DeBrujin i j)) -> greekVars M.! (DeBrujin (i - depth) j)
98+ (NTypeVariable _) -> error "should not have free type variables at this point"
99+ (x :-> y) -> showNType' (depth + 1) x <> " -> " <> showNType' (depth + 1) y
100+ (List x) -> "[" <> showNType' (depth + 1) x <> "]"
101+ (NAttrSet x) ->
102+ "{ "
103+ <> ( mconcat
104+ . intersperse "; "
105+ . fmap (\(k, v) -> T.fromText k <> " = " <> showNType' (depth + 1) v)
106+ $ M.toList x
107+ )
108+ <> " }"
109+ where
110+ currBurjins = traceShowId . S.mapMonotonic (DeBrujin (- depth)) $ getDeBurjins 0 (traceShowId u)
111+ foralls =
112+ if S.null currBurjins
113+ then ""
114+ else
115+ "∀ "
116+ <> (mconcat . intersperse " " . M.elems $ M.restrictKeys greekVars currBurjins)
117+ <> ". "
105118
106119showAtomicType :: AtomicType -> T.Builder
107120showAtomicType Integer = "Integer"
@@ -116,9 +129,9 @@ data NType
116129 = NTypeVariable !TypeVariable
117130 | NBrujin !DeBrujin
118131 | NAtomic !AtomicType
119− | !NType :-> !NType
120132 | -- These two introduce a new De Brujin binding context
121− List !NType
133+ !NType :-> !NType
134+ | List !NType
122135 | NAttrSet !(Map Text NType)
123136 deriving stock (Eq, Ord, Show)
124137
@@ -132,13 +145,26 @@ data AtomicType
132145 | URI
133146 deriving stock (Eq, Ord, Show)
134147
135−getDeBurjins :: NType -> Set DeBrujin
136−getDeBurjins (NTypeVariable _) = S.empty
137−getDeBurjins (NBrujin x) = S.singleton x
138−getDeBurjins (NAtomic _) = S.empty
139−getDeBurjins (x :-> y) = getDeBurjins x <> getDeBurjins y
140−getDeBurjins (List x) = getDeBurjins x
141−getDeBurjins (NAttrSet xs) = foldMap getDeBurjins . M.elems $ xs
148+getDeBurjins :: Int -> NType -> Set Int
149+getDeBurjins _ (NTypeVariable _) = S.empty
150+getDeBurjins _ (NAtomic _) = S.empty
151+getDeBurjins n (NBrujin (DeBrujin m j)) | m == n = S.singleton j
152+getDeBurjins _ (NBrujin _) = S.empty
153+getDeBurjins n (x :-> y) = getDeBurjins (n + 1) x <> getDeBurjins (n + 1) y
154+getDeBurjins n (List x) = getDeBurjins (n + 1) x
155+getDeBurjins n (NAttrSet xs) = foldMap (getDeBurjins (n + 1)) . M.elems $ xs
156+
157+getAllDeBurjins :: NType -> Set DeBrujin
158+getAllDeBurjins =
159+ traceShowId . \case
160+ (NTypeVariable _) -> S.empty
161+ (NAtomic _) -> S.empty
162+ (NBrujin x) -> S.singleton x
163+ (x :-> y) -> bncCtx $ getAllDeBurjins x <> getAllDeBurjins y
164+ (List x) -> bncCtx $ getAllDeBurjins x
165+ (NAttrSet xs) -> bncCtx . foldMap getAllDeBurjins . M.elems $ xs
166+ where
167+ bncCtx = S.mapMonotonic (\(DeBrujin i j) -> DeBrujin (i - 1) j)
142168
143169isClosed :: NType -> Bool
144170isClosed (NTypeVariable _) = False
@@ -148,8 +174,8 @@ isClosed (x :-> y) = isClosed x && isClosed y
148174isClosed (List x) = isClosed x
149175isClosed (NAttrSet xs) = all isClosed . M.elems $ xs
150176
151−close :: NType -> NType
152−close =
177+close :: Range TypeVariable -> NType -> NType
178+close range =
153179 run
154180 . evalState @(Map TypeVariable DeBrujin) M.empty
155181 . runReader @Int 0
@@ -160,12 +186,16 @@ close =
160186 close' :: NType -> Eff '[State Int, Reader Int, State (Map TypeVariable DeBrujin)] NType
161187 close' x@(NAtomic _) = return x
162188 close' x@(NBrujin _) = return x
163− close' (x :-> y) = (:->) <$> close' x <*> close' y
164− close' (NTypeVariable tv) = NBrujin <$> newbrujin tv
189+ close' (NTypeVariable tv) | tv `R.member` range = NBrujin <$> newbrujin tv
190+ close' (x :-> y) = bndCtx $ (:->) <$> close' x <*> close' y
165191 close' (List x) = bndCtx $ List <$> close' x
166192 close' (NAttrSet x) = bndCtx $ NAttrSet <$> traverse close' x
167193
168− bndCtx = local @Int (+ 1)
194+ bndCtx m = do
195+ modify @(Map TypeVariable DeBrujin) (fmap (\(DeBrujin i j) -> DeBrujin (i + 1) j))
196+ x <- local @Int (+ 1) m
197+ modify @(Map TypeVariable DeBrujin) (fmap (\(DeBrujin i j) -> DeBrujin (i - 1) j))
198+ return x
169199 newbrujin t = do
170200 get @(Map TypeVariable DeBrujin) <&> M.lookup t >>= \case
171201 Nothing -> do
@@ -188,6 +218,7 @@ instance Free NType where
188218 free (x :-> y) = free x <> free y
189219
190220newtype Substitution = Substitution {unSubstitution :: Map TypeVariable NType}
221+ deriving newtype (Eq, Ord, Show)
191222
192223instance Semigroup Substitution where
193224 x'@(Substitution x) <> (Substitution y) = Substitution (x <> fmap (sub x') y)
@@ -218,9 +249,21 @@ v <<- x | v `occursIn` x = tell (InfinityType x) >> return mempty
218249v <<- x = return $ Substitution $ M.singleton v x
219250
220251unify :: Constraint -> UnifyM Substitution
221−unify (lhs :~ rhs) =
252+unify = unifyWithPriority EmptyRange
253+
254+unifyWithPriority ::
255+ -- | The range of type variables to interpret as being lower
256+ -- priority (try to replace them if possible)
257+ Range TypeVariable ->
258+ Constraint ->
259+ UnifyM Substitution
260+unifyWithPriority range (lhs :~ rhs) =
222261 case (lhs, rhs) of
223262 (NAtomic x, NAtomic y) | x == y -> return mempty
263+ (NTypeVariable x, NTypeVariable y) ->
264+ if y `R.member` range
265+ then x <<- NTypeVariable y
266+ else y <<- NTypeVariable x
224267 (NTypeVariable t, x) -> t <<- x
225268 (x, NTypeVariable t) -> t <<- x
226269 (List x, List y) -> unify $ x :~ y
@@ -235,10 +278,18 @@ unify (lhs :~ rhs) =
235278 (x, y) -> tell (CanNotUnify x y) >> return mempty
236279
237280solve :: Seq Constraint -> UnifyM Substitution
238−solve Empty = return mempty
239−solve (rest :|> c) = do
240− s <- unify c
241− (<> s) <$> solve (fmap (subCon (traceShowId s)) rest)
281+solve = solveWithPriority EmptyRange
282+
283+solveWithPriority ::
284+ -- | The range of type variables to interpret as being lower
285+ -- priority (try to replace them if possible)
286+ Range TypeVariable ->
287+ Seq Constraint ->
288+ UnifyM Substitution
289+solveWithPriority _ Empty = return mempty
290+solveWithPriority range (rest :|> c) = do
291+ s <- unifyWithPriority range c
292+ (<> s) <$> solveWithPriority range (fmap (subCon (traceShowId s)) rest)
242293
243294pattern Sempty <- (S.null -> True) where Sempty = S.empty
244295
@@ -265,6 +316,10 @@ data Errors
265316
266317data Fresh x where
267318 Fresh :: Fresh TypeVariable
319+ -- | Inclusive
320+ MinFreshFromNow :: Fresh TypeVariable
321+ -- | Inclusive
322+ MaxFreshUntilNow :: Fresh TypeVariable
268323
269324data ResumableExceptions x
270325
@@ -274,12 +329,24 @@ runFresh :: Runner Fresh
274329runFresh =
275330 evalState (TypeVariable 0)
276331 . reinterpret
277− ( \Fresh -> do
278− (TypeVariable old) <- get
279− put (TypeVariable $ old + 1)
280− return (TypeVariable old)
332+ ( \case
333+ Fresh -> do
334+ (TypeVariable x) <- get
335+ put (TypeVariable $ x + 1)
336+ return (TypeVariable x)
337+ MinFreshFromNow -> get
338+ MaxFreshUntilNow -> do
339+ (TypeVariable new) <- get
340+ return $ TypeVariable (new - 1)
281341 )
282342
343+registerTypeVariables :: Member Fresh r => Eff r a -> Eff r (a, Range TypeVariable)
344+registerTypeVariables m = do
345+ l <- send MinFreshFromNow
346+ a <- m
347+ r <- send MaxFreshUntilNow
348+ return (a, Range l r)
349+
283350freshSrc ::
284351 Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] r =>
285352 Eff r TypeVariable
@@ -302,7 +369,8 @@ type InferEffs =
302369 Writer Constraint,
303370 Writer (SrcSpan, Errors),
304371 Reader VariableMap,
305− Writer UnifyingError
372+ Writer UnifyingError,
373+ Writer Substitution
306374 ]
307375
308376type InferM x = forall r. Members InferEffs r => Eff r x
@@ -475,7 +543,7 @@ inferBinding bindings = do
475543 getPath path >>= \case
476544 Nothing -> return []
477545 Just name -> do
478− t <- infer r
546+ t <- inferGeneral r
479547 return $ [stack ((,) <$> name) (NAttrSet . uncurry M.singleton) t]
480548 Inherit attrSet keys src -> do
481549 vars <- case attrSet of
@@ -491,6 +559,17 @@ inferBinding bindings = do
491559 Just r -> Just (name, r)
492560 return $ M.fromListWith mergeSetTypes bindings'
493561
562+inferGeneral :: NExprLoc -> InferM NType
563+inferGeneral x = do
564+ ((t, cs), range) <- registerTypeVariables . runSeqWriter @(Seq Constraint) $ infer x
565+ s <- solveWithPriority range cs
566+ -- Filter for optimization purposes
567+ tell . Substitution . M.filterWithKey (\k _ -> k `R.notMember` range) . unSubstitution $ s
568+ return . close range $ sub s t
569+
570+-- appAll :: (a -> b -> b) -> [a] -> b -> b
571+-- appAll f xs = appEndo (mconcat $ Endo . f <$> xs)
572+
494573expectAttrSet :: Members '[Reader SrcSpan, Writer (SrcSpan, Errors)] r => NType -> Eff r VariableMap
495574expectAttrSet (NAttrSet x) = return x
496575expectAttrSet g = do