From 84d0d37a9a0e1eb5e82d1ba579bc1d602ce1ce63 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Samuel=20G=C3=A9lineau?= <gelisam+github@gmail.com>
Date: Sat, 1 Feb 2025 23:41:44 -0500
Subject: [PATCH 1/4] monadic Pretty

I want to thread a state throughout the value being pretty-printed, so I
have to change all the pretty-printing code to be monadic. to make this
easier to review, this commit only contains the refactoring, I am not
yet making use of the new state.
---
 src/Expander/Error.hs | 319 ++++++++-------
 src/Expander/Task.hs  |   2 +-
 src/Pretty.hs         | 914 ++++++++++++++++++++++++------------------
 src/Util/Store.hs     |  10 +-
 4 files changed, 712 insertions(+), 533 deletions(-)

diff --git a/src/Expander/Error.hs b/src/Expander/Error.hs
index c4134733..0ed78573 100644
--- a/src/Expander/Error.hs
+++ b/src/Expander/Error.hs
@@ -16,6 +16,7 @@ import Data.Text (Text)
 import Data.Sequence (Seq)
 import qualified Data.Text as T
 import Data.Foldable
+import Data.Traversable (for)
 
 import Core
 import Datatype
@@ -108,49 +109,63 @@ data SyntacticCategory
   deriving Show
 
 instance Pretty VarInfo ExpansionErr where
-  pp env (Ambiguous p x candidates) =
-    hang 4 $
-      text "Ambiguous identifier in phase" <+> pp env p <+> line <>
-      text "Identifier:" <+> pp env x <> line <>
+  pp env (Ambiguous p x candidates) = do
+    ppP <- pp env p
+    ppX <- pp env x
+    pure $ hang 4 $
+      text "Ambiguous identifier in phase" <+> ppP <+> line <>
+      text "Identifier:" <+> ppX <> line <>
       text "Scope set of the identifier:" <> line <>
         viaShow (_stxScopeSet x) <> line <>
       text "Scope sets of the candidates:" <> line <>
         vsep [viaShow c | c <- toList candidates]
-  pp env (Unknown x) = text "Unknown:" <+> pp env x
-  pp env (NoProgress tasks) =
-    hang 4 $
+  pp env (Unknown x) = do
+    ppX <- pp env x
+    pure $ text "Unknown:" <+> ppX
+  pp env (NoProgress tasks) = do
+    ppTasks <- mapM (pp env) tasks
+    pure $ hang 4 $
       text "No progress was possible:" <> line <>
-      vsep (map (pp env) tasks)
-  pp env (NotIdentifier stx) =
-    text "Not an identifier:" <+> pp env stx
-  pp env (NotEmpty stx) =
-    hang 2 $ group $ vsep [text "Expected (), but got", pp env stx]
-  pp env (NotCons stx) =
-    hang 2 $ group $ vsep [text "Expected non-empty parens, but got", pp env stx]
-  pp env (NotConsCons stx) =
-    hang 2 $ group $ vsep [text "Expected parens with at least 2 entries, but got", pp env stx]
-  pp env (NotList stx) =
-    hang 2 $ group $ vsep [text "Expected parens, but got", pp env stx]
-  pp env (NotInteger stx) =
-    hang 2 $ group $
-    vsep [ text "Expected integer literal, but got"
-         , pp env stx
-         ]
-  pp env (NotString stx) =
-    hang 2 $ group $
-    vsep [ text "Expected string literal, but got"
-         , pp env stx
-         ]
-  pp env (NotModName stx) =
-    hang 2 $ group $
-    vsep [ text "Expected module name (string or `kernel'), but got"
-         , pp env stx
-         ]
-  pp env (NotRightLength lengths0 stx) =
-    hang 2 $ group $
-    vsep [ text "Expected" <+> alts lengths0 <+> text "entries between parentheses, but got"
-         , pp env stx
-         ]
+      vsep ppTasks
+  pp env (NotIdentifier stx) = do
+    ppStx <- pp env stx
+    pure $ text "Not an identifier:" <+> ppStx
+  pp env (NotEmpty stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Expected (), but got", ppStx]
+  pp env (NotCons stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Expected non-empty parens, but got", ppStx]
+  pp env (NotConsCons stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Expected parens with at least 2 entries, but got", ppStx]
+  pp env (NotList stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Expected parens, but got", ppStx]
+  pp env (NotInteger stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group
+         $ vsep [ text "Expected integer literal, but got"
+                , ppStx
+                ]
+  pp env (NotString stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group
+         $ vsep [ text "Expected string literal, but got"
+                , ppStx
+                ]
+  pp env (NotModName stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group
+         $ vsep [ text "Expected module name (string or `kernel'), but got"
+                , ppStx
+                ]
+  pp env (NotRightLength lengths0 stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group
+         $ vsep [ text "Expected" <+> alts lengths0 <+> text "entries between parentheses, but got"
+                , ppStx
+                ]
     where
       alts :: [Natural] -> Doc ann
       alts []
@@ -161,119 +176,155 @@ instance Pretty VarInfo ExpansionErr where
         = viaShow len1 <+> "or" <+> viaShow len2
       alts (len:lengths)
         = viaShow len <> "," <+> alts lengths
-  pp env (NotVec stx) =
-    hang 2 $ group $ vsep [text "Expected square-bracketed vec but got", pp env stx]
-  pp env (NotImportSpec stx) =
-    hang 2 $ group $ vsep [text "Expected import spec but got", pp env stx]
-  pp env (NotExportSpec stx) =
-    hang 2 $ group $ vsep [text "Expected export spec but got", pp env stx]
-  pp env (UnknownPattern stx) =
-    hang 2 $ group $ vsep [text "Unknown pattern",  pp env stx]
-  pp env (MacroRaisedSyntaxError err) =
+  pp env (NotVec stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Expected square-bracketed vec but got", ppStx]
+  pp env (NotImportSpec stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Expected import spec but got", ppStx]
+  pp env (NotExportSpec stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Expected export spec but got", ppStx]
+  pp env (UnknownPattern stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Unknown pattern",  ppStx]
+  pp env (MacroRaisedSyntaxError err) = do
     let locs = view syntaxErrorLocations err
-        msg = text "Syntax error from macro:" <> line <>
-              pp env (view syntaxErrorMessage err)
-    in hang 4 $ group $
-       case locs of
-         [] -> msg
-         (Syntax l : ls) ->
-           pp env (view stxSrcLoc l) <> text ":" <> line <> msg <>
-           case ls of
-             [] -> mempty
-             more -> text "Additional locations:" <> line <> vsep [pp env loc | Syntax (Stx _ loc _) <- more]
-  pp env (MacroEvaluationError p err) =
-    hang 4 $ group $
-    vsep [text "Error at phase" <+> pp env p <> text ":",
-          pp env err]
-  pp env (ValueNotMacro val) =
-    text "Not a macro monad value:" <+> pp env val
-  pp env (ValueNotSyntax val) =
-    hang 4 $ group $ text "Not a syntax object: " <> line <> pp env val
+    ppErr <- pp env (view syntaxErrorMessage err)
+    let ppMsg = text "Syntax error from macro:" <> line <>
+                ppErr
+    ppBlock <- case locs of
+      [] -> pure ppMsg
+      (Syntax l : ls) -> do
+        ppSrcLoc <- pp env (view stxSrcLoc l)
+        ppLs <- case ls of
+          [] -> pure mempty
+          more -> do
+            ppMore <- for more $ \(Syntax (Stx _ loc _)) ->
+              pp env loc
+            pure $ text "Additional locations:" <> line <> vsep ppMore
+        pure (ppSrcLoc <> text ":" <> line <> ppMsg <> ppLs)
+    pure $ hang 4 $ group ppBlock
+  pp env (MacroEvaluationError p err) = do
+    ppP <- pp env p
+    ppErr <- pp env err
+    pure $ hang 4 $ group
+         $ vsep [text "Error at phase" <+> ppP <> text ":",
+                 ppErr]
+  pp env (ValueNotMacro val) = do
+    ppVal <- pp env val
+    pure $ text "Not a macro monad value:" <+> ppVal
+  pp env (ValueNotSyntax val) = do
+    ppVal <- pp env val
+    pure $ hang 4 $ group $ text "Not a syntax object: " <> line <> ppVal
   pp _env (NoSuchFile filename) =
-    text "User error; no such file: " <> string filename
-  pp env (NotExported (Stx _ loc x) p) =
-    group $ hang 4 $ vsep [ pp env loc <> text ":"
-                          , text "Not available at phase" <+> pp env p <> text ":" <+> pp env x
+    pure $ text "User error; no such file: " <> string filename
+  pp env (NotExported (Stx _ loc x) p) = do
+    ppLoc <- pp env loc
+    ppP <- pp env p
+    ppX <- pp env x
+    pure $ group $ hang 4 $ vsep [ ppLoc <> text ":"
+                          , text "Not available at phase" <+> ppP <> text ":" <+> ppX
                           ]
   pp env (ImportError err) = pp env err
   pp _env (InternalError str) =
-    text "Internal error during expansion! This is a bug in the implementation." <> line <> string str
+    pure $ text "Internal error during expansion! This is a bug in the implementation." <> line <> string str
   pp _env (ReaderError txt) =
-    vsep (map text (T.lines txt))
-  pp env (WrongSyntacticCategory stx is shouldBe) =
-    hang 2 $ group $
-    vsep [ pp env stx <> text ":"
-         , group $ vsep [ group $ hang 2 $
-                          vsep [ text "Used in a position expecting"
-                               , pp env (unMortise shouldBe)
+    pure $ vsep (map text (T.lines txt))
+  pp env (WrongSyntacticCategory stx is shouldBe) = do
+    ppStx <- pp env stx
+    ppIs <- pp env (unTenon is)
+    ppShouldBe <- pp env (unMortise shouldBe)
+    pure $ hang 2 $ group
+         $ vsep [ ppStx <> text ":"
+                , group $ vsep [ group $ hang 2 $
+                                 vsep [ text "Used in a position expecting"
+                                      , ppShouldBe
+                                      ]
+                               , group $ hang 2 $
+                                 vsep [ text "but is valid in a position expecting"
+                                      , ppIs
+                                      ]
                                ]
-                        , group $ hang 2 $
-                          vsep [ text "but is valid in a position expecting"
-                               , pp env (unTenon is)
-                               ]
-                        ]
-         ]
-  pp env (NotValidType stx) =
-    hang 2 $ group $ vsep [text "Not a type:", pp env stx]
+                ]
+  pp env (NotValidType stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Not a type:", ppStx]
   pp env (TypeCheckError err) = pp env err
-  pp env (WrongArgCount stx ctor wanted got) =
-    hang 2 $
-    vsep [ text "Wrong number of arguments for constructor" <+> pp env ctor
-         , text "Wanted" <+> viaShow wanted
-         , text "Got" <+> viaShow got
-         , text "At" <+> align (pp env stx)
-         ]
-  pp env (NotAConstructor stx) =
-    hang 2 $ group $ vsep [text "Not a constructor in", pp env stx]
-  pp env (WrongTypeArity stx ctor arity got) =
-    hang 2 $ vsep [ text "Incorrect arity for" <+> pp env ctor
+  pp env (WrongArgCount stx ctor wanted got) = do
+    ppCtor <- pp env ctor
+    ppStx <- pp env stx
+    pure $ hang 2
+         $ vsep [ text "Wrong number of arguments for constructor" <+> ppCtor
+                , text "Wanted" <+> viaShow wanted
+                , text "Got" <+> viaShow got
+                , text "At" <+> align (ppStx)
+                ]
+  pp env (NotAConstructor stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "Not a constructor in", ppStx]
+  pp env (WrongTypeArity stx ctor arity got) = do
+    ppCtor <- pp env ctor
+    ppStx <- pp env stx
+    pure $ hang 2 $ vsep [ text "Incorrect arity for" <+> ppCtor
                   , text "Wanted" <+> viaShow arity
                   , text "Got" <+> viaShow got
-                  , text "In" <+> align (pp env stx)
+                  , text "In" <+> align (ppStx)
                   ]
-  pp env (KindMismatch loc k1 k2) =
-    hang 2 $ group $ vsep [ text "Kind mismatch at" <+>
-                            maybe (text "unknown location") (pp env) loc <> text "."
-                          , group $ vsep [pp env k1, text "≠", pp env k2]
+  pp env (KindMismatch loc k1 k2) = do
+    ppLoc <- maybe (pure $ text "unknown location") (pp env) loc
+    ppK1 <- pp env k1
+    ppK2 <- pp env k2
+    pure $ hang 2 $ group $ vsep [ text "Kind mismatch at" <+>
+                            ppLoc <> text "."
+                          , group $ vsep [ppK1, text "≠", ppK2]
                           ]
-  pp env (CircularImports current stack) =
-    hang 2 $ vsep [ group $ vsep [ text "Circular imports while importing", pp env current]
-                  , group $ hang 2 $ vsep (text "Context:" : map (pp env) stack)]
+  pp env (CircularImports current stack) = do
+    ppCurrent <- pp env current
+    ppStack <- mapM (pp env) stack
+    pure $ hang 2 $ vsep [ group $ vsep [ text "Circular imports while importing", ppCurrent]
+                  , group $ hang 2 $ vsep (text "Context:" : ppStack)]
 
 instance Pretty VarInfo TypeCheckError where
-  pp env (TypeMismatch loc shouldBe got specifically) =
-    group $ vsep [ group $ hang 2 $ vsep [ text "Type mismatch at"
-                                         , maybe (text "unknown location") (pp env) loc <> text "."
-                                         ]
-                 , group $ vsep $
-                   [ group $ hang 2 $ vsep [ text "Expected"
-                                           , pp env shouldBe
-                                           ]
-                   , group $ hang 2 $ vsep [ text "but got"
-                                           , pp env got
-                                           ]
-                   ] ++
-                   case specifically of
-                     Nothing -> []
-                     Just (expected', got') ->
-                       [ hang 2 $ group $ vsep [text "Specifically,"
-                                               , group (vsep [ pp env expected'
-                                                             , text "doesn't match" <+> pp env got'
-                                                             ])
-                                               ]
+  pp env (TypeMismatch loc shouldBe got specifically) = do
+    ppLoc <- maybe (pure $ text "unknown location") (pp env) loc
+    ppShouldBe <- pp env shouldBe
+    ppGot <- pp env got
+    ppSpec <- case specifically of
+      Nothing -> pure []
+      Just (expected', got') -> do
+        ppE <- pp env expected'
+        ppG <- pp env got'
+        pure [ hang 2 $ group $ vsep [text "Specifically,"
+                                    , group (vsep [ ppE
+                                                , text "doesn't match" <+> ppG
+                                                ])
+                                    ]
+            ]
+    pure $ group $ vsep [ group $ hang 2 $ vsep [ text "Type mismatch at"
+                                                , ppLoc <> text "."
+                                                ]
+                       , group $ vsep $
+                         [ group $ hang 2 $ vsep [ text "Expected"
+                                                , ppShouldBe
+                                                ]
+                         , group $ hang 2 $ vsep [ text "but got"
+                                                , ppGot
+                                                ]
+                         ] ++ ppSpec
                        ]
-                 ]
 
-  pp env (OccursCheckFailed ptr ty) =
-    hang 2 $ group $ vsep [ text "Occurs check failed:"
-                          , group (vsep [viaShow ptr, "≠", pp env ty])
+  pp env (OccursCheckFailed ptr ty) = do
+    ppTy <- pp env ty
+    pure $ hang 2 $ group $ vsep [ text "Occurs check failed:"
+                          , group (vsep [viaShow ptr, "≠", ppTy])
                           ]
 
 
 instance Pretty VarInfo SyntacticCategory where
-  pp _env ExpressionCat = text "an expression"
-  pp _env ModuleCat = text "a module"
-  pp _env TypeCat = text "a type"
-  pp _env DeclarationCat = text "a top-level declaration or example"
-  pp _env PatternCaseCat = text "a pattern"
-  pp _env TypePatternCaseCat = text "a typecase pattern"
+  pp _env ExpressionCat = pure $ text "an expression"
+  pp _env ModuleCat = pure $ text "a module"
+  pp _env TypeCat = pure $ text "a type"
+  pp _env DeclarationCat = pure $ text "a top-level declaration or example"
+  pp _env PatternCaseCat = pure $ text "a pattern"
+  pp _env TypePatternCaseCat = pure $ text "a typecase pattern"
diff --git a/src/Expander/Task.hs b/src/Expander/Task.hs
index d4a3707b..8be4d2b3 100644
--- a/src/Expander/Task.hs
+++ b/src/Expander/Task.hs
@@ -110,4 +110,4 @@ instance ShortShow ExpanderTask where
   shortShow (AwaitingTypePattern _ _ _ _) = "(AwaitingTypePattern _ _ _ _)"
 
 instance Pretty VarInfo ExpanderTask where
-  pp _ task = string (shortShow task)
+  pp _ task = pure $ string (shortShow task)
diff --git a/src/Pretty.hs b/src/Pretty.hs
index 86b409bd..73d24476 100644
--- a/src/Pretty.hs
+++ b/src/Pretty.hs
@@ -11,12 +11,14 @@ module Pretty (Doc, Pretty(..), string, text, viaShow, (<+>), (<>), align, hang,
 import Control.Lens hiding (List)
 import Control.Monad.State
 import qualified Data.HashMap.Strict as HM
+import Util.Set (Set)
 import qualified Util.Set as Set
 import Prettyprinter hiding (Pretty(..), angles, parens)
 import qualified Prettyprinter as PP
 import Prettyprinter.Render.Text (putDoc, renderStrict)
 import Data.Sequence (Seq)
 import Data.Text (Text)
+import Data.Traversable (for)
 import qualified Data.Text as T
 import qualified Data.Foldable as F
 import System.FilePath (takeFileName)
@@ -41,6 +43,7 @@ import Unique
 import Value
 import World
 
+import Util.Store (Store)
 import qualified Util.Store as St
 
 text :: Text -> Doc ann
@@ -59,28 +62,52 @@ vec :: Doc ann -> Doc ann
 vec doc = text "[" <> align (group doc) <> "]"
 
 pretty :: Pretty ann a => a -> Text
-pretty x = renderStrict (layoutPretty defaultLayoutOptions (pp Env.empty x))
+pretty x
+  = renderStrict
+  $ layoutPretty defaultLayoutOptions
+  $ flip evalState St.empty
+  $ pp Env.empty x
 
 prettyPrint :: Pretty ann a => a -> IO ()
-prettyPrint x = putDoc (pp Env.empty x)
+prettyPrint x
+  = putDoc
+  $ flip evalState St.empty
+  $ pp Env.empty x
 
 prettyPrintLn :: Pretty ann a => a -> IO ()
-prettyPrintLn x = putDoc (pp Env.empty x) >> putStrLn ""
+prettyPrintLn x = do
+  prettyPrint x
+  putStrLn ""
 
 prettyEnv :: Pretty ann a => Env Var v -> a -> Text
-prettyEnv env x =
-  renderStrict (layoutPretty defaultLayoutOptions (pp (fmap (const ()) env) x))
+prettyEnv env x
+  = renderStrict
+  $ layoutPretty defaultLayoutOptions
+  $ flip evalState St.empty
+  $ pp (fmap (const ()) env) x
 
 prettyPrintEnv :: Pretty ann a => Env Var v -> a -> IO ()
-prettyPrintEnv env x =
-  putDoc (pp (fmap (const ()) env) x)
-
+prettyPrintEnv env x
+  = putDoc
+  $ flip evalState St.empty
+  $ pp (fmap (const ()) env) x
+
+
+-- Internally, the type of 'id' might be represented as @MetaPtr 183 -> MetaPtr
+-- 186@, with some information about the unification variables indicating that
+-- 183 and 186 are the same. When we print this, we would prefer to show
+-- something like @?1 -> ?1@. To achieve this, the caller (who has access to the
+-- information about the unification variables) must zonk the type into @MetaPtr
+-- 183 -> MetaPtr 183@, and the pretty-printer must keep track of which
+-- unification variables it has already printed and which number it used for
+-- each.
+type Renumbering = Store MetaPtr Int
 
 class Pretty ann a | a -> ann where
-  pp :: Env Var () -> a -> Doc ann
+  pp :: Env Var () -> a -> State Renumbering (Doc ann)
 
 instance Pretty ann (Doc ann) where
-  pp _env doc = doc
+  pp _env doc = pure doc
 
 data VarInfo
   = BindingSite Var
@@ -93,121 +120,143 @@ instance Pretty VarInfo Core where
 instance (PrettyBinder VarInfo typePat, PrettyBinder VarInfo pat, Pretty VarInfo core) =>
          Pretty VarInfo (CoreF typePat pat core) where
   pp env (CoreVar v) =
-    annotate (UseSite v) $
+    pure $ annotate (UseSite v) $
     case Env.lookupIdent v env of
       Nothing -> string ("!!" ++ show v ++ "!!")
       Just (Stx _ _ x) -> text x
-  pp env (CoreLet x@(Stx _ _ y) v def body) =
-    hang 2 $ group $
-    vsep [ text "let" <+> hang 2 (group (vsep [ pp env y <+> text "="
-                                              , pp env def
-                                              ])) <+> text "in"
-         , pp (env <> Env.singleton v x ()) body
-         ]
-  pp env (CoreLetFun f@(Stx _ _ g) fv x@(Stx _ _ y) v def body) =
-    hang 2 $ group $
-    vsep [ text "flet" <+>
-           hang 2 (group (vsep [ pp env g <+> pp env y <+> text "="
-                               , pp (env <> Env.singleton fv f () <> Env.singleton v x ()) def
-                               ])) <+>
-           text "in"
-         , pp (env <> Env.singleton fv f ()) body
-         ]
-  pp env (CoreLam n@(Stx _ _ x) v body) =
-    hang 2 $ group $
-    text "λ" <> annotate (BindingSite v) (text x) <> "." <> line <>
-    pp (env <> Env.singleton v n ()) body
-  pp env (CoreApp fun arg) =
-    hang 2 $ parens (pp env fun <> line <> pp env arg)
+  pp env (CoreLet x@(Stx _ _ y) v def body) = do
+    ppY <- pp env y
+    ppDef <- pp env def
+    ppBody <- pp (env <> Env.singleton v x ()) body
+    pure $ hang 2 $ group $
+      vsep [ text "let" <+> hang 2 (group (vsep [ ppY <+> text "="
+                                               , ppDef
+                                               ])) <+> text "in"
+           , ppBody
+           ]
+  pp env (CoreLetFun f@(Stx _ _ g) fv x@(Stx _ _ y) v def body) = do
+    ppG <- pp env g
+    ppY <- pp env y
+    ppDef <- pp (env <> Env.singleton fv f () <> Env.singleton v x ()) def
+    ppBody <- pp (env <> Env.singleton fv f ()) body
+    pure $ hang 2 $ group $
+      vsep [ text "flet" <+>
+             hang 2 (group (vsep [ ppG <+> ppY <+> text "="
+                                 , ppDef
+                                 ])) <+>
+             text "in"
+           , ppBody
+           ]
+  pp env (CoreLam n@(Stx _ _ x) v body) = do
+    ppBody <- pp (env <> Env.singleton v n ()) body
+    pure $ hang 2 $ group $
+      text "λ" <> annotate (BindingSite v) (text x) <> "." <> line <>
+      ppBody
+  pp env (CoreApp fun arg) = do
+    ppFun <- pp env fun
+    ppArg <- pp env arg
+    pure $ parens (ppFun <> line <> ppArg)
   pp env (CoreCtor ctor []) = pp env ctor
-  pp env (CoreCtor ctor args) =
-    hang 2 $ parens $ pp env ctor <+> group (vsep (map (pp env) args))
-  pp env (CoreDataCase _ scrut cases) =
-    hang 2 $ group $
-    vsep [ text "case" <+> pp env scrut <+> "of"
-         , encloseSep (flatAlt mempty (text "{" <> space))
-                      (flatAlt mempty (space <> text "}"))
-                      (flatAlt mempty (space <> text ";" <> space)) $
-           map (\(pat, rhs) ->
-                   let (ppPat, env') = ppBind env pat
-                   in hang 2 $ group $
-                      vsep [ppPat <+> text "↦",
-                            pp (env <> env') rhs])
-            cases
-         ]
-  pp _env (CoreString str) = text (T.pack (show str))
-  pp env (CoreError what) =
-    text "error" <+> pp env what
-  pp env (CorePureMacro arg) =
-    text "pure" <+> pp env arg
-  pp env (CoreBindMacro act k) =
-    hang 2 $ group (pp env act <+> text ">>=") <+> pp env k
-  pp env (CoreSyntaxError err) =
-    group $ text "syntax-error" <+> pp env err
-  pp env (CoreIdentEq how e1 e2) =
-    group $ text opName <+> pp env e1 <+> pp env e2
+  pp env (CoreCtor ctor args) = do
+    ppCtor <- pp env ctor
+    ppArgs <- mapM (pp env) args
+    pure $ hang 2 $ parens $ ppCtor <+> group (vsep ppArgs)
+  pp env (CoreDataCase _ scrut cases) = do
+    ppScrut <- pp env scrut
+    ppCases <- for cases $ \(pat, rhs) -> do
+      (ppPat, env') <- ppBind env pat
+      ppRhs <- pp (env <> env') rhs
+      pure $ hang 2 $ group $ vsep [ppPat <+> text "↦", ppRhs]
+    pure $ hang 2 $ group $
+      vsep [ text "case" <+> ppScrut <+> "of"
+           , encloseSep (flatAlt mempty (text "{" <> space))
+                        (flatAlt mempty (space <> text "}"))
+                        (flatAlt mempty (space <> text ";" <> space)) ppCases
+           ]
+  pp _env (CoreString str) = pure $ text (T.pack (show str))
+  pp env (CoreError what) = do
+    ppWhat <- pp env what
+    pure $ text "error" <+> ppWhat
+  pp env (CorePureMacro arg) = do
+    ppArg <- pp env arg
+    pure $ text "pure" <+> ppArg
+  pp env (CoreBindMacro act k) = do
+    ppAct <- pp env act
+    ppK <- pp env k
+    pure $ hang 2 $ group (ppAct <+> text ">>=") <+> ppK
+  pp env (CoreSyntaxError err) = do
+    ppErr <- pp env err
+    pure $ group $ text "syntax-error" <+> ppErr
+  pp env (CoreIdentEq how e1 e2) = do
+    ppE1 <- pp env e1
+    ppE2 <- pp env e2
+    pure $ group $ text opName <+> ppE1 <+> ppE2
     where
       opName =
         case how of
           Free -> "free-identifier=?"
           Bound -> "bound-identifier=?"
-  pp env (CoreLog msg) =
-    group (hang 2 (vsep ["log", pp env msg]))
-  pp _env CoreMakeIntroducer =
-    text "make-introducer"
-  pp _ CoreWhichProblem =
-    text "which-problem"
-  pp env (CoreSyntax stx) =
-    pp env stx
-  pp env (CoreCase _ scrut pats) =
-    hang 2 $ group $
-    group (hang 2 $ text "syntax-case" <+> pp env scrut <+> "of") <> line <>
-    vsep [ parens $ hang 2 $
-           let (b, env') = ppBind env pat
-           in group (group (b <+> "=>") <> line <> pp (env <> env') body)
-         | (pat, body) <- pats
-         ]
-  pp _env (CoreInteger s) = viaShow s
+  pp env (CoreLog msg) = do
+    ppMsg <- pp env msg
+    pure $ group (hang 2 (vsep ["log", ppMsg]))
+  pp _env CoreMakeIntroducer = pure $ text "make-introducer"
+  pp _ CoreWhichProblem = pure $ text "which-problem"
+  pp env (CoreSyntax stx) = pp env stx
+  pp env (CoreCase _ scrut pats) = do
+    ppScrut <- pp env scrut
+    ppPats <- for pats $ \(pat, body) -> do
+      (b, env') <- ppBind env pat
+      ppBody <- pp (env <> env') body
+      pure $ parens $ hang 2 $ group (group (b <+> "=>") <> line <> ppBody)
+    pure $ hang 2 $ group $
+      group (hang 2 $ text "syntax-case" <+> ppScrut <+> "of") <> line <>
+      vsep ppPats
+  pp _env (CoreInteger s) = pure $ viaShow s
   pp env (CoreIdent x) = pp env x
   pp env (CoreEmpty e) = pp env e
   pp env (CoreCons e) = pp env e
   pp env (CoreList e) = pp env e
   pp env (CoreIntegerSyntax i) = pp env i
   pp env (CoreStringSyntax s) = pp env s
-  pp env (CoreReplaceLoc loc stx) =
-    group $ hang 2 $ vsep [ text "replace-loc"
-                          , pp env loc
-                          , pp env stx
-                          ]
-  pp env (CoreTypeCase _ scrut pats) =
-    hang 2 $ group $
-    group (hang 2 $ text "type-case" <+> pp env scrut <+> "of") <> line <>
-    vsep [ parens $ hang 2 $
-           let (b, env') = ppBind env pat
-           in group (group (b <+> "=>") <> line <> pp (env <> env') body)
-         | (pat, body) <- pats
-         ]
+  pp env (CoreReplaceLoc loc stx) = do
+    ppLoc <- pp env loc
+    ppStx <- pp env stx
+    pure $ group $ hang 2 $ vsep [ text "replace-loc"
+                                 , ppLoc
+                                 , ppStx
+                                 ]
+  pp env (CoreTypeCase _ scrut pats) = do
+    ppScrut <- pp env scrut
+    ppPats <- for pats $ \(pat, body) -> do
+      (b, env') <- ppBind env pat
+      ppBody <- pp (env <> env') body
+      pure $ parens $ hang 2 $ group (group (b <+> "=>") <> line <> ppBody)
+    pure $ hang 2 $ group $
+      group (hang 2 $ text "type-case" <+> ppScrut <+> "of") <> line <>
+      vsep ppPats
 
 instance Pretty VarInfo core => Pretty VarInfo (SyntaxError core) where
-  pp env err =
-    angles $
-    pp env (view syntaxErrorMessage err) <> text ";" <+>
-    concatWith (\d1 d2 -> d1 <> text "," <+> d2)
-               (map (pp env) (view syntaxErrorLocations err))
+  pp env err = do
+    ppMsg <- pp env (view syntaxErrorMessage err)
+    ppLocs <- mapM (pp env) (view syntaxErrorLocations err)
+    pure $ angles $ ppMsg <> text ";" <+> concatWith (\d1 d2 -> d1 <> text "," <+> d2) ppLocs
 
 class PrettyBinder ann a | a -> ann where
-  ppBind :: Env Var () -> a -> (Doc ann, Env Var ())
+  ppBind :: Env Var () -> a -> State Renumbering (Doc ann, Env Var ())
+
 
 instance PrettyBinder VarInfo a => PrettyBinder VarInfo (TyF a) where
-  ppBind env t =
+  ppBind env t = do
     let subs = ppBind env <$> t
-    in (pp env (fst <$> subs), foldMap snd subs) 
+    sub <- sequence subs
+    doc <- pp env (fmap fst sub)
+    pure (doc, foldMap snd sub)
 
 newtype BinderPair = BinderPair (Ident, Var)
 
 instance PrettyBinder VarInfo BinderPair where
   ppBind _env (BinderPair (ident@(Stx _ _ n), x)) =
-    (annotate (BindingSite x) (text n), Env.singleton x ident ())
+    pure (annotate (BindingSite x) (text n), Env.singleton x ident ())
 
 instance PrettyBinder VarInfo TypePattern where
   ppBind env (TypePattern t) =
@@ -221,101 +270,113 @@ instance PrettyBinder VarInfo ConstructorPattern where
 instance PrettyBinder VarInfo a => PrettyBinder VarInfo (ConstructorPatternF a) where
   ppBind env (CtorPattern ctor subPats) =
     case subPats of
-      [] -> (pp env ctor, Env.empty)
-      _nonEmpty ->
-        let subDocs = map (ppBind env) subPats
-            env' = foldr (<>) Env.empty (map snd subDocs)
-        in (pp env ctor <+> hsep (map fst subDocs),
-            env')
+      [] -> do
+        doc <- pp env ctor
+        pure (doc, Env.empty)
+      _nonEmpty -> do
+        subDocs <- mapM (ppBind env) subPats
+        doc <- pp env ctor
+        pure (doc <+> hsep (map fst subDocs),
+              foldr (<>) Env.empty (map snd subDocs))
   ppBind _env (PatternVar ident@(Stx _ _ n) x) =
-    (annotate (BindingSite x) (text n), Env.singleton x ident ())
+    pure (annotate (BindingSite x) (text n), Env.singleton x ident ())
 
 instance PrettyBinder VarInfo SyntaxPattern where
   ppBind _env (SyntaxPatternIdentifier ident@(Stx _ _ x) v) =
-    (annotate (BindingSite v) (text x), Env.singleton v ident ())
+    pure (annotate (BindingSite v) (text x), Env.singleton v ident ())
   ppBind _env (SyntaxPatternInteger ident@(Stx _ _ x) v) =
-    (parens $ text "integer" <+> annotate (BindingSite v) (text x), Env.singleton v ident ())
+    pure (parens $ text "integer" <+> annotate (BindingSite v) (text x), Env.singleton v ident ())
   ppBind _env (SyntaxPatternString ident@(Stx _ _ x) v) =
-    (parens $ text "string" <+> annotate (BindingSite v) (text x), Env.singleton v ident ())
+    pure (parens $ text "string" <+> annotate (BindingSite v) (text x), Env.singleton v ident ())
   ppBind _env SyntaxPatternEmpty =
-    (text "()", Env.empty)
+    pure (text "()", Env.empty)
   ppBind _env (SyntaxPatternCons ida@(Stx _ _ xa) va idd@(Stx _ _ xd) vd) =
-    (parens (text "cons" <+>
+    pure (parens (text "cons" <+>
              annotate (BindingSite va) (text xa) <+>
              annotate (BindingSite vd) (text xd)),
      Env.insert vd idd () $ Env.singleton va ida ())
   ppBind _env (SyntaxPatternList vars) =
-    (vec $
+    pure (vec $
      hsep [annotate (BindingSite v) (text x)
           | (Stx _ _ x, v) <- vars
           ],
      foldr (\(x, v) e -> Env.insert x v () e) Env.empty [(v, x) | (x, v) <- vars])
-  ppBind _env SyntaxPatternAny = (text "_", Env.empty)
+  ppBind _env SyntaxPatternAny = pure (text "_", Env.empty)
 
 instance Pretty VarInfo core => Pretty VarInfo (ScopedIdent core) where
-  pp env ident =
-    text "ident" <+>
-    pp env (view scopedIdentIdentifier ident) <+>
-    pp env (view scopedIdentScope ident)
+  pp env ident = do
+    ppIdent <- pp env (view scopedIdentIdentifier ident)
+    ppScope <- pp env (view scopedIdentScope ident)
+    pure $ text "ident" <+> ppIdent <+> ppScope
 
 instance Pretty VarInfo core => Pretty VarInfo (ScopedEmpty core) where
-  pp env e =
-    text "()" <> angles (pp env (view scopedEmptyScope e))
+  pp env e = do
+    ppScope <- pp env (view scopedEmptyScope e)
+    pure $ text "()" <> angles ppScope
 
 instance Pretty VarInfo core => Pretty VarInfo (ScopedCons core) where
-  pp env pair =
-    text "cons-from" <>
-    parens (pp env (view scopedConsHead pair) <> text "," <+>
-            pp env (view scopedConsTail pair)) <>
-    angles (pp env (view scopedConsScope pair))
+  pp env pair = do
+    ppHead <- pp env (view scopedConsHead pair)
+    ppTail <- pp env (view scopedConsTail pair)
+    ppScope <- pp env (view scopedConsScope pair)
+    pure $ text "cons-from" <>
+      parens (ppHead <> text "," <+> ppTail) <>
+      angles ppScope
 
 instance Pretty VarInfo core => Pretty VarInfo (ScopedList core) where
-  pp env xs =
-    vec (hsep $ map (pp env) (view scopedListElements xs)) <>
-    angles (pp env (view scopedListScope xs))
+  pp env xs = do
+    ppElements <- mapM (pp env) (view scopedListElements xs)
+    ppScope <- pp env (view scopedListScope xs)
+    pure $ vec (hsep ppElements) <> angles ppScope
 
 instance Pretty VarInfo core => Pretty VarInfo (ScopedInteger core) where
-  pp env s =
-    pp env (view scopedInteger s) <>
-    angles (pp env (view scopedIntegerScope s))
+  pp env s = do
+    ppInteger <- pp env (view scopedInteger s)
+    ppScope <- pp env (view scopedIntegerScope s)
+    pure $ ppInteger <> angles ppScope
 
 instance Pretty VarInfo core => Pretty VarInfo (ScopedString core) where
-  pp env s =
-    pp env (view scopedString s) <>
-    angles (pp env (view scopedStringScope s))
-
+  pp env s = do
+    ppString <- pp env (view scopedString s)
+    ppScope <- pp env (view scopedStringScope s)
+    pure $ ppString <> angles ppScope
 
 instance PrettyBinder VarInfo CompleteDecl where
   ppBind env (CompleteDecl d) = ppBind env d
 
 instance PrettyBinder VarInfo (Seq CompleteDecl) where
-  ppBind env decls = over _1 vsep
-                   $ foldr go (\e -> (mempty, e)) decls mempty
+  ppBind env decls = do
+    (docs, env') <- F.foldrM go ([], mempty) decls
+    pure (vsep docs, env')
     where
       go :: CompleteDecl
-         -> (Env Var () -> ([Doc VarInfo], Env Var ()))
-         -> (Env Var () -> ([Doc VarInfo], Env Var ()))
-      go decl cc e = let (doc, e') = ppBind (env <> e) decl
-                         (docs, e'') = cc (e <> e')
-                     in (doc:docs, e'')
+         -> ([Doc VarInfo], Env Var ())
+         -> State Renumbering ([Doc VarInfo], Env Var ())
+      go decl (docs, e) = do
+        (doc, e') <- ppBind (env <> e) decl
+        pure (doc:docs, e <> e')
 
 instance Pretty VarInfo Kind where
-  pp _   KStar        = text "*"
-  pp env (KFun k1 k2) = parens (pp env k1 <+> text "→" <+> pp env k2)
-  pp _   (KMetaVar v) = text "META" <> viaShow v -- TODO make it look better
+  pp _   KStar        = pure $ text "*"
+  pp env (KFun k1 k2) = do
+    ppK1 <- pp env k1
+    ppK2 <- pp env k2
+    pure $ parens (ppK1 <+> text "→" <+> ppK2)
+  pp _   (KMetaVar v) = pure $ text "META" <> viaShow v -- TODO make it look better
 
 instance Pretty VarInfo (Scheme Ty) where
-  pp env (Scheme [] t) =
-    pp env t
-  pp env (Scheme argKinds t) =
-    text "∀" <>
-    (align $ group $
-     vsep [ group $
-            vsep (zipWith ppArgKind typeVarNames argKinds) <> text "."
-          , pp env t
-          ])
+  pp env (Scheme [] t) = pp env t
+  pp env (Scheme argKinds t) = do
+    ppT <- pp env t
+    ppArgKinds <- mapM (pp env) argKinds
+    pure $ text "∀" <>
+      (align $ group $
+       vsep [ group $
+              vsep (zipWith ppArgKind typeVarNames ppArgKinds) <> text "."
+            , ppT
+            ])
     where
-      ppArgKind varName kind = parens (text varName <+> text ":" <+> pp env kind)
+      ppArgKind varName kind = parens (text varName <+> text ":" <+> kind)
 
 typeVarNames :: [Text]
 typeVarNames =
@@ -332,325 +393,377 @@ typeVarNames =
                , base <- greek
                ]
 
-
 instance Pretty VarInfo TypeConstructor where
-  pp _   TSyntax        = text "Syntax"
-  pp _   TInteger       = text "Integer"
-  pp _   TString        = text "String"
-  pp _   TOutputPort    = text "Output-Port"
-  pp _   TFun           = text "(→)"
-  pp _   TMacro         = text "Macro"
-  pp _   TIO            = text "IO"
-  pp _   TType          = text "Type"
+  pp _   TSyntax        = pure $ text "Syntax"
+  pp _   TInteger       = pure $ text "Integer"
+  pp _   TString        = pure $ text "String"
+  pp _   TOutputPort    = pure $ text "Output-Port"
+  pp _   TFun           = pure $ text "(→)"
+  pp _   TMacro         = pure $ text "Macro"
+  pp _   TIO            = pure $ text "IO"
+  pp _   TType          = pure $ text "Type"
   pp env (TDatatype t)  = pp env t
-  pp _   (TSchemaVar n) = text $ typeVarNames !! fromIntegral n
-  pp _   (TMetaVar v)   = text "META" <> viaShow v -- TODO
+  pp _   (TSchemaVar n) = pure $ text $ typeVarNames !! fromIntegral n
+  pp _   (TMetaVar v)   = pure $ text "META" <> viaShow v -- TODO
 
 instance Pretty VarInfo a => Pretty VarInfo (TyF a) where
-  pp _ (TyF TFun []) =
-    parens (text "→")
-  pp env (TyF TFun [a]) =
-    parens (text "→" <+> pp env a)
-  pp env (TyF TFun [a, b]) =
-    parens $ align $ group $ vsep [pp env a <+> text "→", pp env b]
-  pp env (TyF ctor args) =
+  pp _ (TyF TFun []) = pure $ parens (text "→")
+  pp env (TyF TFun [a]) = do
+    ppA <- pp env a
+    pure $ parens (text "→" <+> ppA)
+  pp env (TyF TFun [a, b]) = do
+    ppA <- pp env a
+    ppB <- pp env b
+    pure $ parens $ align $ group $ vsep [ppA <+> text "→", ppB]
+  pp env (TyF ctor args) = do
+    ppCtor <- pp env ctor
     case args of
-      [] -> pp env ctor
-      more -> parens (align $ group $ pp env ctor <+> vsep (map (pp env) more))
+      [] -> pure ppCtor
+      more -> do
+        ppMore <- mapM (pp env) more
+        pure $ parens $ align $ group $ ppCtor <+> vsep ppMore
 
 instance Pretty VarInfo Datatype where
-  pp _ d = text (view (datatypeName . datatypeNameText) d)
+  pp _ d = pure $ text (view (datatypeName . datatypeNameText) d)
 
 instance Pretty VarInfo Constructor where
-  pp _ c = text (view (constructorName . constructorNameText) c)
+  pp _ c = pure $ text (view (constructorName . constructorNameText) c)
 
 instance Pretty VarInfo Ty where
   pp env (Ty t) = pp env t
 
 instance (Pretty VarInfo s, Pretty VarInfo t, PrettyBinder VarInfo a, Pretty VarInfo b) =>
          PrettyBinder VarInfo (Decl t s a b) where
-  ppBind env (Define n@(Stx _ _ x) v t e) =
-    let env' = Env.singleton v n ()
-    in (hang 4 $ group $
-        vsep [ text "define" <+>
-               annotate (BindingSite v) (text x) <+> text ":"
-             , pp env t
-             , text ":="
-             , pp (env <> env') e
-             ],
-        env')
-  ppBind env (DefineMacros macros) =
-    (hang 4 $ text "define-macros" <> line <>
-     vsep [hang 2 $ group $
-           annotate (MacroBindingSite v) (text x) <+> text "↦" <> line <> pp env e -- TODO phase-specific binding environments in pprinter
-          | (Stx _ _ x, v, e) <- macros
-          ],
-     mempty)
-  ppBind env (Data (Stx _ _ x) _dn argKinds ctors) =
-    (hang 2 $ group $
-     vsep ( text "data" <+> text x <+>
-            hsep [ parens (text α <+> ":" <+> pp env k)
-                 | α <- typeVarNames
-                 | k <- argKinds
-                 ] <+>
-            text "="
-          : punc (space <> text "|")
-            [ case args of
-                [] -> text c
-                more ->
-                  hang 2 $
-                  text c <+>
-                  group (vsep [ pp env a | a <- more ])
-            | (Stx _ _ c, _cn, args) <- ctors
-            ]
-          )
-    , mempty)
-  ppBind env (Meta d) =
-    let (doc, env') = ppBind env d
-    in (hang 4 $ text "meta" <> line <> doc, env')
-  ppBind env (Import spec) =
-    (hang 4 $ text "import" <+> pp env spec, mempty)
-  ppBind env (Export x) =
-    (hang 4 $ text "export" <+> pp env x, mempty)
-  ppBind env (Example loc t e) =
-    (hang 4 $
-     text "example@" <> pp env loc <+>
-     align (group (vsep [ group (pp env e) <+> text ":"
-                        , pp env t
-                        ])),
-     mempty)
-  ppBind env (Run _loc e) =
-    (hang 4 $
-     text "run" <+> align (pp env e),
-     mempty)
+  ppBind env (Define n@(Stx _ _ x) v t e) = do
+    ppT <- pp env t
+    ppE <- pp (env <> Env.singleton v n ()) e
+    pure (hang 4 $ group $
+          vsep [ text "define" <+>
+                 annotate (BindingSite v) (text x) <+> text ":"
+               , ppT
+               , text ":="
+               , ppE
+               ],
+          Env.singleton v n ())
+  ppBind env (DefineMacros macros) = do
+    ppMacros <- for macros $ \(Stx _ _ x, v, e) -> do
+      ppE <- pp env e
+      pure $ hang 2 $ group $
+        annotate (MacroBindingSite v) (text x) <+> text "↦" <> line <> ppE
+    pure (hang 4 $ text "define-macros" <> line <> vsep ppMacros, mempty)
+  ppBind env (Data (Stx _ _ x) _dn argKinds ctors) = do
+    ppArgKinds <- mapM (pp env) argKinds
+    ppCtors <- for ctors $ \(Stx _ _ c, _cn, args) -> do
+      ppArgs <- mapM (pp env) args
+      pure $ case ppArgs of
+        [] -> text c
+        more -> hang 2 $ text c <+> group (vsep ppArgs)
+    pure (hang 2 $ group $
+            vsep ( text "data" <+> text x <+>
+                   hsep [ parens (text α <+> ":" <+> kind)
+                        | α <- typeVarNames
+                        | kind <- ppArgKinds
+                        ] <+>
+                   text "="
+                 : punc (space <> text "|") ppCtors
+                 )
+           , mempty)
+  ppBind env (Meta d) = do
+    (doc, env') <- ppBind env d
+    pure (hang 4 $ text "meta" <> line <> doc, env')
+  ppBind env (Import spec) = do
+    ppSpec <- pp env spec
+    pure (hang 4 $ text "import" <+> ppSpec, mempty)
+  ppBind env (Export x) = do
+    ppX <- pp env x
+    pure (hang 4 $ text "export" <+> ppX, mempty)
+  ppBind env (Example loc t e) = do
+    ppLoc <- pp env loc
+    ppT <- pp env t
+    ppE <- pp env e
+    pure (hang 4 $
+            text "example@" <> ppLoc <+>
+            align (group (vsep [ group (ppE) <+> text ":"
+                               , ppT
+                               ])),
+            mempty)
+  ppBind env (Run _loc e) = do
+    ppE <- pp env e
+    pure (hang 4 $
+            text "run" <+> align ppE,
+            mempty)
 
 instance Pretty VarInfo ExportSpec where
-  pp env (ExportIdents ids) =
-    text "{" <> align (vsep [pp env x | (Stx _ _ x) <- ids]) <> text "}"
-  pp env (ExportRenamed spec rens) =
-    align $ hang 2 $ group $
-      pp env spec <> line <>
+  pp env (ExportIdents ids) = do
+    ppIds <- mapM (pp env) ids
+    pure $ text "{" <> align (vsep ppIds) <> text "}"
+  pp env (ExportRenamed spec rens) = do
+    ppSpec <- pp env spec
+    let ppRens = map (\(x, y) -> text x <+> text "↦" <+> text y) rens
+    pure $ align $ hang 2 $ group $
+      ppSpec <> line <>
       text "renaming" <+> text "{" <>
-      (align $ group $ vsep [text x <+> text "↦" <+> text y
-                            | (x, y) <- rens
-                            ]) <>
+      (align $ group $ vsep ppRens) <>
       text "}"
-  pp env (ExportPrefixed spec p) =
-    align $ hang 2 $ group $
-    vsep [ text "(" <> align (group (pp env spec)) <> ")"
-         , text "with" <+> text "prefix"
-         , text p
-         ]
-  pp env (ExportShifted spec i) =
-    align $ hang 2 $ group $
-    vsep [ text "(" <> align (group (pp env spec)) <> ")"
-         , text "shifted" <+> text "by"
-         , viaShow i
-         ]
+  pp env (ExportPrefixed spec p) = do
+    ppSpec <- pp env spec
+    pure $ align $ hang 2 $ group $
+      vsep [ text "(" <> align (group ppSpec) <> ")"
+           , text "with" <+> text "prefix"
+           , text p
+           ]
+  pp env (ExportShifted spec i) = do
+    ppSpec <- pp env spec
+    pure $ align $ hang 2 $ group $
+      vsep [ text "(" <> align (group ppSpec) <> ")"
+           , text "shifted" <+> text "by"
+           , viaShow i
+           ]
 
 instance Pretty VarInfo ImportSpec where
   pp env (ImportModule mn) = pp env mn
-  pp env (ImportOnly spec ids) = group $ vsep [ text "only"
-                                              , pp env spec
-                                              , parens (group (vsep (map (pp env) ids)))
-                                              ]
-  pp env (ShiftImports spec i) = pp env spec <+> "⇑" <+> viaShow i
-  pp env (RenameImports spec rens) = group $ vsep [ text "rename"
-                                                  , pp env spec
-                                                  , group (vsep [pp env x <+> pp env y | (x, y) <- rens])
-                                                  ]
-  pp env (PrefixImports spec pref) = group $ vsep [ text "prefix"
-                                                  , pp env spec
-                                                  , viaShow pref
-                                                  ]
+  pp env (ImportOnly spec ids) = do
+    ppSpec <- pp env spec
+    ppIds <- mapM (pp env) ids
+    pure $ group $ vsep [ text "only"
+                          , ppSpec
+                          , parens (group (vsep ppIds))
+                          ]
+  pp env (ShiftImports spec i) = do
+    ppSpec <- pp env spec
+    pure $ ppSpec <+> "⇑" <+> viaShow i
+  pp env (RenameImports spec rens) = do
+    ppSpec <- pp env spec
+    ppRens <- mapM (\(x, y) -> (<+>) <$> pp env x <*> pp env y) rens
+    pure $ group $ vsep [ text "rename"
+                        , ppSpec
+                        , group (vsep ppRens)
+                        ]
+  pp env (PrefixImports spec pref) = do
+    ppSpec <- pp env spec
+    pure $ group $ vsep [ text "prefix"
+                        , ppSpec
+                        , viaShow pref
+                        ]
 
 instance Pretty VarInfo ModuleName where
-  pp _ n = text (moduleNameText n)
+  pp _ n = pure $ text (moduleNameText n)
 
 instance (Functor f, Traversable f, PrettyBinder VarInfo a) => Pretty VarInfo (Module f a) where
-  pp env m =
-    hang 4 $
-    text "module" <+> pp env (view moduleName m) <> line <>
-    concatWith terpri (fst (runState (traverse go (view moduleBody m)) env))
-
+  pp env m = do
+    let modName = view moduleName m
+    let body = view moduleBody m
+    ppModName <- pp env modName
+    ppBody <- flip evalStateT env $ traverse go body
+    pure $ hang 4 $
+      text "module" <+> ppModName <> line <>
+      concatWith terpri ppBody
     where
       terpri d1 d2 = d1 <> line <> d2
-      go :: a -> State (Env Var ()) (Doc VarInfo)
-      go d =
-        do thisEnv <- get
-           let (doc, newEnv) = ppBind thisEnv d
-           put (thisEnv <> newEnv)
-           return doc
+      go :: a -> StateT (Env Var ()) (State Renumbering) (Doc VarInfo)
+      go d = do
+        thisEnv <- get
+        (doc, newEnv) <- lift $ ppBind thisEnv d
+        put (thisEnv <> newEnv)
+        pure doc
 
 instance Pretty VarInfo SrcLoc where
-  pp env loc =
-    string (takeFileName (view srcLocFilePath loc)) <> text ":" <>
-    pp env (view srcLocStart loc) <> text "-" <>
-    pp env (view srcLocEnd loc)
+  pp env loc = do
+    ppStart <- pp env (view srcLocStart loc)
+    ppEnd <- pp env (view srcLocEnd loc)
+    pure $ string (takeFileName (view srcLocFilePath loc)) <> text ":" <>
+      ppStart <> text "-" <>
+      ppEnd
 
 instance Pretty VarInfo SrcPos where
-  pp _env pos =
-    viaShow (view srcPosLine pos) <> text "." <>
-    viaShow (view srcPosCol pos)
+  pp _env pos = pure $ viaShow (view srcPosLine pos) <> text "." <> viaShow (view srcPosCol pos)
 
 instance Pretty VarInfo a => Pretty VarInfo (Stx a) where
-  pp env (Stx _ loc v) =
-    text "#" <>
-    (align . group)
-      (text "[" <> pp env loc <> text "]" <> line' <> text "<" <>
-       align (pp env v) <>
-       text ">")
+  pp env (Stx _ loc v) = do
+    ppLoc <- pp env loc
+    ppV <- pp env v
+    pure $ text "#" <>
+      (align . group)
+        (text "[" <> ppLoc <> text "]" <> line' <> text "<" <>
+         align ppV <>
+         text ">")
 
 instance Pretty VarInfo Syntax where
   pp env (Syntax e) = pp env e
 
 instance Pretty VarInfo (ExprF Syntax) where
-  pp _   (Id x)      = text x
-  pp _   (String s)  = viaShow s
-  pp _   (Integer s) = viaShow s
-  pp env (List xs)   = parens (group (vsep (map (pp env . syntaxE) xs)))
+  pp _   (Id x)      = pure $ text x
+  pp _   (String s)  = pure $ viaShow s
+  pp _   (Integer s) = pure $ viaShow s
+  pp env (List xs)   = do
+    ppXs <- mapM (pp env . syntaxE) xs
+    pure $ parens (group (vsep ppXs))
 
 instance Pretty VarInfo Closure where
-  pp _ _ = text "#<closure>"
+  pp _ _ = pure $ text "#<closure>"
 
 instance Pretty VarInfo Value where
   pp env (ValueClosure c) = pp env c
   pp env (ValueSyntax stx) = pp env stx
   pp env (ValueMacroAction act) = pp env act
-  pp _env (ValueIOAction _) = "#<IO action>"
-  pp _env (ValueOutputPort _) = "#<output port>"
-  pp _env (ValueInteger s) = viaShow s
-  pp _env (ValueCtor c []) =
-    parens $
-    text (view (constructorName . constructorNameText) c)
-  pp env (ValueCtor c args) =
-    parens $
-    text (view (constructorName . constructorNameText) c) <+>
-    align (group (vsep (map (pp env) args)))
-  pp _env (ValueType ptr) = text "#t<" <> viaShow ptr <> text ">"
-  pp _env (ValueString str) = text (T.pack (show str))
+  pp _env (ValueIOAction _) = pure "#<IO action>"
+  pp _env (ValueOutputPort _) = pure "#<output port>"
+  pp _env (ValueInteger s) = pure $ viaShow s
+  pp _env (ValueCtor c []) = pure $ parens $ text (view (constructorName . constructorNameText) c)
+  pp env (ValueCtor c args) = do
+    ppArgs <- mapM (pp env) args
+    pure $ parens $ text (view (constructorName . constructorNameText) c) <+> align (group (vsep ppArgs))
+  pp _env (ValueType ptr) = pure $ text "#t<" <> viaShow ptr <> text ">"
+  pp _env (ValueString str) = pure $ text (T.pack (show str))
 
 instance Pretty VarInfo MacroAction where
-  pp env (MacroActionPure v) =
-    text "pure" <+> pp env v
-  pp env (MacroActionBind v k) =
-    group $
-      group (pp env v <> line <> text ">>=") <> line <>
-      pp env k
-  pp env (MacroActionSyntaxError err) =
-    text "syntax-error" <+> pp env err
-  pp env (MacroActionIdentEq how v1 v2) =
-    group $ parens $ vsep [text opName, pp env v1, pp env v2]
+  pp env (MacroActionPure v) = do
+    ppV <- pp env v
+    pure $ text "pure" <+> ppV
+  pp env (MacroActionBind v k) = do
+    ppV <- pp env v
+    ppK <- pp env k
+    pure $ group $
+      group (ppV <> line <> text ">>=") <> line <>
+      ppK
+  pp env (MacroActionSyntaxError err) = do
+    ppErr <- pp env err
+    pure $ text "syntax-error" <+> ppErr
+  pp env (MacroActionIdentEq how v1 v2) = do
+    ppV1 <- pp env v1
+    ppV2 <- pp env v2
+    pure $ group $ parens $ vsep [text opName, ppV1, ppV2]
     where
       opName =
         case how of
           Free  -> "free-identifier=?"
           Bound -> "bound-identifier=?"
-  pp env (MacroActionLog stx) =
-    hang 2 $ group $ vsep [text "log", pp env stx]
-  pp _env MacroActionIntroducer =
-    text "make-introducer"
-  pp _env MacroActionWhichProblem =
-    text "which-problem"
-  pp env (MacroActionTypeCase venv _loc ptr cases) =
-    hang 2 $
-    text "type-case" <+> text "#t<" <> viaShow ptr <> text ">" <+> text "of" <> line <>
-    vsep (map ppCase cases)
-    where
-      ppCase (pat, c) =
-        let (patDoc, env') = ppBind env pat
-        in hang 2 $ group $ vsep [patDoc <+> "↦", pp (fmap (const ()) venv <> env') c]
+  pp env (MacroActionLog stx) = do
+    ppStx <- pp env stx
+    pure $ hang 2 $ group $ vsep [text "log", ppStx]
+  pp _env MacroActionIntroducer = pure $ text "make-introducer"
+  pp _env MacroActionWhichProblem = pure $ text "which-problem"
+  pp env (MacroActionTypeCase venv _loc ptr cases) = do
+    ppCases <- for cases $ \(pat, c) -> do
+      (patDoc, env') <- ppBind env pat
+      ppC <- pp (fmap (const ()) venv <> env') c
+      pure $ hang 2 $ group $ vsep [patDoc <+> "↦", ppC]
+    pure $ hang 2 $
+      text "type-case" <+> text "#t<" <> viaShow ptr <> text ">" <+> text "of" <> line <>
+      vsep ppCases
 
 instance Pretty VarInfo Phase where
-  pp _env p = text "p" <> viaShow (phaseNum p)
+  pp _env p = pure $ text "p" <> viaShow (phaseNum p)
 
 instance Pretty VarInfo a => Pretty VarInfo (World a) where
-  pp env w =
-    vsep $ map (hang 4)
+  pp env w = do
+    ppModules <- for (HM.toList (view worldModules w)) $ \(_modName, mod) -> do
+      pp env mod
+    ppVisited <- for (HM.toList (view worldVisited w)) $ \(modName, phases) -> do
+      ppModName <- pp env modName
+      ppPhases <- mapM (pp env) (Set.toList phases)
+      pure $ hang 4 $ ppModName <> line <> text "{" <> group (vsep ppPhases) <> text "}"
+    ppEnvs <- for (St.toList $ view worldEnvironments w) $ \(p, rho) -> do
+      ppPhase <- pp env p
+      ppRho <- pp env rho
+      pure $ hang 4 $ ppPhase <> line <> ppRho
+    pure $ vsep $ map (hang 4)
       [vsep [ text "Expanded modules"
-            , vsep [ pp env m
-                   | (_, m) <- HM.toList (view worldModules w)
-                   ]
+            , vsep ppModules
             ]
       , vsep [ text "Modules visited"
-             , vsep [ hang 4 $
-                      pp env mn <> line <>
-                      text "{" <> group (vsep (map (pp env) ps)) <> text "}"
-                    | (mn, Set.toList -> ps) <- HM.toList (view worldVisited w)
-                    ]
+             , vsep ppVisited
              ]
       , vsep [ text "Environments"
-             , hang 4 $
-               vsep [ hang 4 $
-                      pp env p <> line <>
-                      pp env rho
-                    | (p, rho) <- St.toList $ view worldEnvironments w
-                    ]
+             , hang 4 $ vsep ppEnvs
              ]
       ]
 
 instance Pretty VarInfo Text where
-  pp _ = text
+  pp _ = pure . text
 
 instance Pretty VarInfo a => Pretty VarInfo (Env Var a) where
-  pp env rho =
-    vsep [ hang 4 $ viaShow x <+> pp env n <> line <> pp env v
-         | (x, n, v) <- Env.toList rho
-         ]
+  pp env rho = do
+    ppRho <- for (Env.toList rho) $ \(x, n, v) -> do
+      ppN <- pp env n
+      ppV <- pp env v
+      pure $ hang 4 $ viaShow x <+> ppN <> line <> ppV
+    pure $ vsep ppRho
 
 instance Pretty VarInfo a => Pretty VarInfo (Env MacroVar a) where
-  pp env rho =
-    vsep [ hang 4 $ viaShow x <+> pp env n <> line <> pp env v
-         | (x, n, v) <- Env.toList rho
-         ]
+  pp env rho = do
+    ppRho <- for (Env.toList rho) $ \(x, n, v) -> do
+      ppN <- pp env n
+      ppV <- pp env v
+      pure $ hang 4 $ viaShow x <+> ppN <> line <> ppV
+    pure $ vsep ppRho
 
 instance Pretty VarInfo CompleteModule where
   pp env (Expanded em _ ) = pp env em
-  pp env (KernelModule p) = text "⟨kernel module" <> text "@" <> pp env p <> "⟩"
+  pp env (KernelModule p) = do
+    ppPhase <- pp env p
+    pure $ text "⟨kernel module" <> text "@" <> ppPhase <> "⟩"
 
 instance Pretty VarInfo Binding where
-  pp _env (Binding b) = text "b" <> viaShow (hashUnique b)
+  pp _env (Binding b) = pure $ text "b" <> viaShow (hashUnique b)
 
 instance Pretty VarInfo loc => Pretty VarInfo (BindingInfo loc) where
-  pp env (BoundLocally loc) = pp env loc <> text ":" <+> text "local"
-  pp env (Defined loc) = pp env loc <> text ":" <+> text "defined"
-  pp env (Imported loc) = pp env loc <> text ":" <+> text "import"
+  pp env (BoundLocally loc) = do
+    ppLoc <- pp env loc
+    pure $ ppLoc <> text ":" <+> text "local"
+  pp env (Defined loc) = do
+    ppLoc <- pp env loc
+    pure $ ppLoc <> text ":" <+> text "defined"
+  pp env (Imported loc) = do
+    ppLoc <- pp env loc
+    pure $ ppLoc <> text ":" <+> text "import"
 
 instance Pretty VarInfo EvalError where
-  pp env (EvalErrorUnbound x) = text "Unbound:" <+> pp env (Core (CoreVar x))
+  pp env (EvalErrorUnbound x) = do
+    ppX <- pp env (Core (CoreVar x))
+    pure $ text "Unbound:" <+> ppX
   pp _env (EvalErrorType (TypeError expected got)) =
-    text "Expected a(n)" <+> text expected <+> "but got a(n)" <+> text got
-  pp env (EvalErrorCase blame val) =
-    group $ hang 2 $ vsep [text "No case matched at" <+> pp env blame <> ":" , pp env val]
-  pp env (EvalErrorUser (Syntax (Stx _ loc msg))) =
-    group $ hang 2 $ vsep [pp env loc <> ":", pp env msg]
-  pp env (EvalErrorIdent v) = text "Attempt to bind identifier to non-value: " <+> pp env v
+    pure $ text "Expected a(n)" <+> text expected <+> "but got a(n)" <+> text got
+  pp env (EvalErrorCase blame val) = do
+    ppBlame <- pp env blame
+    ppVal <- pp env val
+    pure $ group $ hang 2 $ vsep [text "No case matched at" <+> ppBlame <> ":" , ppVal]
+  pp env (EvalErrorUser (Syntax (Stx _ loc msg))) = do
+    ppLoc <- pp env loc
+    ppMsg <- pp env msg
+    pure $ group $ hang 2 $ vsep [ppLoc <> ":", ppMsg]
+  pp env (EvalErrorIdent v) = do
+    ppV <- pp env v
+    pure $ text "Attempt to bind identifier to non-value: " <+> ppV
 
 instance Pretty VarInfo EvalResult where
-  pp env (ExampleResult loc valEnv coreExpr sch val) =
+  pp env (ExampleResult loc valEnv coreExpr sch val) = do
     let varEnv = fmap (const ()) valEnv
-    in group $ hang 2 $
-       vsep [ text "Example at" <+> pp env loc <> text ":"
-            , hang 2 $ group $
-              vsep [ pp varEnv coreExpr <+> text ":"
-                   , pp varEnv sch
-                   ] <+> text "↦"
-            , pp varEnv val
-            ]
-  pp _env (IOResult _) = text "IO action"
-
+    ppLoc <- pp env loc
+    ppCoreExpr <- pp varEnv coreExpr
+    ppSch <- pp varEnv sch
+    ppVal <- pp varEnv val
+    pure $ group $ hang 2 $
+      vsep [ text "Example at" <+> ppLoc <> text ":"
+           , hang 2 $ group $
+             vsep [ ppCoreExpr <+> text ":"
+                  , ppSch
+                  ] <+> text "↦"
+           , ppVal
+           ]
+  pp _env (IOResult _) = pure $ text "IO action"
 
 instance Pretty VarInfo BindingTable where
-  pp env bs =
-    group $ hang 2 $ vsep $
-    punc (text ",") [ group $ hang 2 $
-                      pp env n <+> text "↦" <> line <>
-                      text "{" <> group (vsep [ pp env scs <+> text "↦" <+>
-                                                pp env b <+> text "@" <+>
-                                                pp env info
-                                              | (scs, b, info) <- F.toList xs]) <> text "}"
-                    | (n, xs) <- HM.toList $ view bindings bs
-                    ]
+  pp env bs = do
+    ppBindings <- for (HM.toList $ view bindings bs) $ \(name, triples) -> do
+      ppName <- pp env name
+      ppTriples <- for (F.toList triples) $ \(scs, b, info) -> do
+        ppScs <- pp env scs
+        ppB <- pp env b
+        ppInfo <- pp env info
+        pure $ ppScs <+> text "↦" <+> ppB <+> text "@" <+> ppInfo
+      pure $ group $ hang 2 $ ppName <+> text "↦" <> line <> text "{" <> group (vsep ppTriples) <> text "}"
+    pure $ group $ hang 2 $ vsep $ punc (text ",") ppBindings
 
 punc :: Doc VarInfo -> [Doc VarInfo] -> [Doc VarInfo]
 punc _ [] = []
@@ -658,20 +771,27 @@ punc _ [d] = [d]
 punc doc (d1:d2:ds) = (d1 <> doc) : punc doc (d2:ds)
 
 instance Pretty VarInfo Scope where
-  pp _env = viaShow
+  pp _env = pure . viaShow
 
 instance Pretty VarInfo ScopeSet where
-  pp env scs =
+  pp env scs = do
     let (allPhases, phases) = contents scs
-    in text "⟨" <> align (group (ppSet allPhases <> text "," <> line <> ppMap (ppSet <$> phases) <> "⟩"))
-
+    ppAllPhases <- ppSet allPhases
+    ppPhases <- ppStore phases
+    pure $ text "⟨" <> align (group (ppAllPhases <> text "," <> line <> ppPhases <> "⟩"))
     where
       commaSep = group . concatWith (\x y -> x <> text "," <> line <> y)
-      ppSet s =
-        text "{" <> commaSep (map (pp env) (Set.toList s)) <> text "}"
-      ppMap m =
-        group (vsep [group (viaShow k <+> text "↦" <> line <> v) | (k, v) <- St.toList m])
-
+      ppSet :: Set Scope -> State Renumbering (Doc VarInfo)
+      ppSet s = do
+        ppS <- mapM (pp env) (Set.toList s)
+        pure $ text "{" <> commaSep ppS <> text "}"
+      
+      ppStore :: Store Phase (Set Scope) -> State Renumbering (Doc VarInfo)
+      ppStore m = do
+        ppM <- for (St.toList m) $ \(p, scopes) -> do
+          ppScopes <- ppSet scopes
+          pure $ group (viaShow p <+> text "↦" <> line <> ppScopes)
+        pure $ group (vsep ppM)
 
 instance Pretty VarInfo KlisterPathError where
-  pp _ = ppKlisterPathError
+  pp _ = pure . ppKlisterPathError
diff --git a/src/Util/Store.hs b/src/Util/Store.hs
index 26960169..3f9fa721 100644
--- a/src/Util/Store.hs
+++ b/src/Util/Store.hs
@@ -14,7 +14,8 @@
 -- | wrapper over IntMap for our purposes
 
 module Util.Store
-  ( lookup
+  ( empty
+  , lookup
   , singleton
   , insert
   , toList
@@ -23,6 +24,7 @@ module Util.Store
   , unionWith
   , mapKeys
   , mapMaybeWithKey
+  , size
   )
 where
 
@@ -67,6 +69,9 @@ instance HasKey p => At (Store p v) where
 instance (c ~ d) => Each (Store c a) (Store d b) a b where
   each = traversed
 
+empty :: Store p v
+empty = Store IM.empty
+
 lookup :: HasKey p => p -> Store p v -> Maybe v
 lookup ptr graph = getKey ptr `IM.lookup` unStore graph
 
@@ -94,3 +99,6 @@ mapMaybeWithKey f s = Store $! IM.mapMaybeWithKey (f . fromKey) (unStore s)
 
 mapKeys :: HasKey p => (p -> p) -> Store p v -> Store p v
 mapKeys f s = Store $! IM.mapKeys (getKey . f . fromKey) (unStore s)
+
+size :: Store p v -> Int
+size = IM.size . unStore
\ No newline at end of file

From 8c6a1fb99de0e6572393c80c6f1f320d27e3947c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Samuel=20G=C3=A9lineau?= <gelisam+github@gmail.com>
Date: Sun, 2 Feb 2025 23:23:13 -0500
Subject: [PATCH 2/4] example which prints a MetaVar

---
 examples/non-examples/type-errors/not-a-function.golden | 2 ++
 examples/non-examples/type-errors/not-a-function.kl     | 3 +++
 2 files changed, 5 insertions(+)
 create mode 100644 examples/non-examples/type-errors/not-a-function.golden
 create mode 100644 examples/non-examples/type-errors/not-a-function.kl

diff --git a/examples/non-examples/type-errors/not-a-function.golden b/examples/non-examples/type-errors/not-a-function.golden
new file mode 100644
index 00000000..34171405
--- /dev/null
+++ b/examples/non-examples/type-errors/not-a-function.golden
@@ -0,0 +1,2 @@
+Type mismatch at not-a-function.kl:3.11-3.13.
+Expected (Integer → META(MetaPtr 53790)) but got Integer
diff --git a/examples/non-examples/type-errors/not-a-function.kl b/examples/non-examples/type-errors/not-a-function.kl
new file mode 100644
index 00000000..6f30e930
--- /dev/null
+++ b/examples/non-examples/type-errors/not-a-function.kl
@@ -0,0 +1,3 @@
+#lang kernel
+
+(example (42 23))

From 45d119ed791a4e0bafd0ec8cf4e299748096874f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Samuel=20G=C3=A9lineau?= <gelisam+github@gmail.com>
Date: Sun, 2 Feb 2025 23:39:55 -0500
Subject: [PATCH 3/4] make the output deterministic

---
 .../non-examples/type-errors/not-a-function.golden     |  2 +-
 src/Pretty.hs                                          | 10 +++++++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/examples/non-examples/type-errors/not-a-function.golden b/examples/non-examples/type-errors/not-a-function.golden
index 34171405..8df9f320 100644
--- a/examples/non-examples/type-errors/not-a-function.golden
+++ b/examples/non-examples/type-errors/not-a-function.golden
@@ -1,2 +1,2 @@
 Type mismatch at not-a-function.kl:3.11-3.13.
-Expected (Integer → META(MetaPtr 53790)) but got Integer
+Expected (Integer → ?1) but got Integer
diff --git a/src/Pretty.hs b/src/Pretty.hs
index 73d24476..bfa6062f 100644
--- a/src/Pretty.hs
+++ b/src/Pretty.hs
@@ -404,7 +404,15 @@ instance Pretty VarInfo TypeConstructor where
   pp _   TType          = pure $ text "Type"
   pp env (TDatatype t)  = pp env t
   pp _   (TSchemaVar n) = pure $ text $ typeVarNames !! fromIntegral n
-  pp _   (TMetaVar v)   = pure $ text "META" <> viaShow v -- TODO
+  pp _   (TMetaVar v)   = do
+    renumbering <- get
+    case St.lookup v renumbering of
+      Just n -> do
+        pure $ text "?" <> viaShow n
+      Nothing -> do
+        let n = St.size renumbering + 1
+        put (St.insert v n renumbering)
+        pure $ text "?" <> viaShow n
 
 instance Pretty VarInfo a => Pretty VarInfo (TyF a) where
   pp _ (TyF TFun []) = pure $ parens (text "→")

From 12533777a37a831367ad384d3fae35372e5d339b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Samuel=20G=C3=A9lineau?= <gelisam+github@gmail.com>
Date: Sun, 2 Feb 2025 23:59:54 -0500
Subject: [PATCH 4/4] example with more MetaVars

---
 examples/non-examples/type-errors/not-a-function.golden | 2 +-
 examples/non-examples/type-errors/not-a-function.kl     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/examples/non-examples/type-errors/not-a-function.golden b/examples/non-examples/type-errors/not-a-function.golden
index 8df9f320..61cfe153 100644
--- a/examples/non-examples/type-errors/not-a-function.golden
+++ b/examples/non-examples/type-errors/not-a-function.golden
@@ -1,2 +1,2 @@
 Type mismatch at not-a-function.kl:3.11-3.13.
-Expected (Integer → ?1) but got Integer
+Expected (Integer → (?1 → ?2)) but got Integer
diff --git a/examples/non-examples/type-errors/not-a-function.kl b/examples/non-examples/type-errors/not-a-function.kl
index 6f30e930..2f747862 100644
--- a/examples/non-examples/type-errors/not-a-function.kl
+++ b/examples/non-examples/type-errors/not-a-function.kl
@@ -1,3 +1,3 @@
-#lang kernel
+#lang "prelude.kl"
 
-(example (42 23))
+(example (42 4 2))