@@ -294,6 +294,7 @@ type VariableMap = Map VarName NType
294294(~~) :: Member (Writer Constraint) r => NType -> NType -> Eff r ()
295295lhs ~~ rhs = tell $ lhs :~ rhs
296296
297+-- TODO: shadowed bindings are not properly restored.
297298withBindings ::
298299 (Member (State VariableMap) effs) =>
299300 VariableMap ->
@@ -305,6 +306,30 @@ withBindings bindings m = do
305306 modify @VariableMap (`M.difference` bindings)
306307 return a
307308
309+instantiate ::
310+ forall effs.
311+ Members '[Fresh, Reader SrcSpan, Writer (TypeVariable, SrcSpan)] effs =>
312+ NType ->
313+ Eff effs NType
314+instantiate = evalState M.empty . instantiate'
315+ where
316+ instantiate' :: forall. NType -> Eff (State (Map DeBrujin TypeVariable) ': effs) NType
317+ instantiate' x@(NTypeVariable _) = return x
318+ instantiate' x@(NAtomic _) = return x
319+ instantiate' (NBrujin db) = NTypeVariable <$> freshInst db
320+ instantiate' (x :-> y) = (:->) <$> instantiate' x <*> instantiate' y
321+ instantiate' (List x) = List <$> instantiate' x
322+ instantiate' (NAttrSet xs) = NAttrSet <$> traverse instantiate' xs
323+
324+ freshInst :: DeBrujin -> Eff (State (Map DeBrujin TypeVariable) ': effs) TypeVariable
325+ freshInst db = do
326+ gets (M.lookup db) >>= \case
327+ Just t -> return t
328+ Nothing -> do
329+ t <- freshSrc
330+ modify (M.insert db t)
331+ return t
332+
308333infer :: NExprLoc -> InferM NType
309334infer (Fix (Compose (Ann src x))) = runReader src $ case x of
310335 NConstant a -> return . NAtomic $ case a of
@@ -319,6 +344,7 @@ infer (Fix (Compose (Ann src x))) = runReader src $ case x of
319344 NSym var ->
320345 get @VariableMap
321346 >>= maybe (NTypeVariable <$> throwSrcTV (UndefinedVariable var)) return . M.lookup var
347+ >>= instantiate -- I have no idea if this covers all cases.
322348 NList xs -> do
323349 xs' <- traverse infer xs
324350 traverse_ tell . fmap (uncurry (:~)) $ zip xs' (tail xs')