From fc413e1ed5dd29640c302983a5b0e31991686405 Mon Sep 17 00:00:00 2001
From: Mitchell Dalvi Rosen <mitchellwrosen@gmail.com>
Date: Wed, 4 Dec 2024 11:56:05 -0500
Subject: [PATCH 1/7] add failing transcript

---
 unison-src/transcripts/idempotent/fix-5427.md | 100 ++++++++++++++++++
 1 file changed, 100 insertions(+)
 create mode 100644 unison-src/transcripts/idempotent/fix-5427.md

diff --git a/unison-src/transcripts/idempotent/fix-5427.md b/unison-src/transcripts/idempotent/fix-5427.md
new file mode 100644
index 0000000000..6455f38eed
--- /dev/null
+++ b/unison-src/transcripts/idempotent/fix-5427.md
@@ -0,0 +1,100 @@
+``` ucm
+scratch/main> builtins.merge lib.builtin
+
+  Done.
+```
+
+``` unison
+foo : Nat
+foo = 17
+
+bar : Nat
+bar =
+  foo = .foo
+  foo
+
+baz : Nat
+baz = foo + foo
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+
+    ⍟ These new definitions are ok to `add`:
+    
+      bar : Nat
+      baz : Nat
+      foo : Nat
+```
+
+``` ucm
+scratch/main> add
+
+  ⍟ I've added these definitions:
+
+    bar : Nat
+    baz : Nat
+    foo : Nat
+```
+
+``` unison
+foo : Nat
+foo = 18
+
+bar : Nat
+bar =
+  foo = .foo
+  foo
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+
+    ⍟ These names already exist. You can `update` them to your
+      new definition:
+    
+      bar : Nat
+      foo : Nat
+```
+
+This should succeed, but `bar` gets printed incorrectly\!
+
+``` ucm :error
+scratch/main> update
+
+  Okay, I'm searching the branch for code that needs to be
+  updated...
+
+  That's done. Now I'm making sure everything typechecks...
+
+  Typechecking failed. I've updated your scratch file with the
+  definitions that need fixing. Once the file is compiling, try
+  `update` again.
+```
+
+``` unison :added-by-ucm scratch.u
+foo : Nat
+foo = 18
+
+bar : Nat
+bar =
+  foo = foo
+  foo
+
+-- The definitions below no longer typecheck with the changes above.
+-- Please fix the errors and try `update` again.
+
+baz : Nat
+baz =
+  use Nat +
+  foo + foo
+
+```

From 30609ee223ec9eba6bbbf8a6c794d4db514c5fb5 Mon Sep 17 00:00:00 2001
From: Mitchell Dalvi Rosen <mitchellwrosen@gmail.com>
Date: Tue, 10 Dec 2024 11:48:58 -0500
Subject: [PATCH 2/7] small term printer refactor

---
 .../src/Unison/Syntax/TermPrinter.hs          | 57 ++++++++++---------
 1 file changed, 31 insertions(+), 26 deletions(-)

diff --git a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
index e516fb404a..283bd6991f 100644
--- a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
+++ b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
@@ -209,8 +209,7 @@ pretty0
       blockContext = bc,
       infixContext = ic,
       imports = im,
-      docContext = doc,
-      elideUnit = elideUnit
+      docContext = doc
     }
   term =
     specialCases term \case
@@ -360,7 +359,7 @@ pretty0
                       ]
       LetBlock bs e ->
         let (im', uses) = calcImports im term
-         in printLet elideUnit bc bs e im' uses
+         in printLet a {imports = im'} bc bs e uses
       -- Some matches are rendered as a destructuring bind, like
       --   match foo with (a,b) -> blah
       -- becomes
@@ -641,29 +640,6 @@ pretty0
       sepList' f sep xs = fold . intersperse sep <$> traverse f xs
       varList = runIdentity . sepList' (Identity . PP.text . Var.name) PP.softbreak
 
-      printLet ::
-        Bool -> -- elideUnit
-        BlockContext ->
-        [(v, Term3 v PrintAnnotation)] ->
-        Term3 v PrintAnnotation ->
-        Imports ->
-        [Pretty SyntaxText] ->
-        m (Pretty SyntaxText)
-      printLet elideUnit sc bs e im uses = do
-        bs <- traverse printBinding bs
-        body <- body e
-        pure . paren (sc /= Block && p >= Top) . letIntro $ PP.lines (uses <> bs <> body)
-        where
-          body (Constructor' (ConstructorReference DD.UnitRef 0)) | elideUnit = pure []
-          body e = (: []) <$> pretty0 (ac Annotation Normal im doc) e
-          printBinding (v, binding) =
-            if Var.isAction v
-              then pretty0 (ac Bottom Normal im doc) binding
-              else renderPrettyBinding <$> prettyBinding0' (ac Bottom Normal im doc) (HQ.unsafeFromVar v) binding
-          letIntro = case sc of
-            Block -> id
-            Normal -> \x -> fmt S.ControlKeyword "let" `PP.hang` x
-
       nonForcePred :: Term3 v PrintAnnotation -> Bool
       nonForcePred = \case
         Constructor' (ConstructorReference DD.DocRef _) -> False
@@ -672,6 +648,35 @@ pretty0
       nonUnitArgPred :: (Var v) => v -> Bool
       nonUnitArgPred v = Var.name v /= "()"
 
+printLet ::
+  (MonadPretty v m) =>
+  AmbientContext ->
+  BlockContext ->
+  [(v, Term3 v PrintAnnotation)] ->
+  Term3 v PrintAnnotation ->
+  [Pretty SyntaxText] ->
+  m (Pretty SyntaxText)
+printLet context sc bs e uses = do
+  bs <- traverse (printLetBinding bindingContext) bs
+  body <- body e
+  pure . paren (sc /= Block && context.precedence >= Top) . letIntro $ PP.lines (uses <> bs <> body)
+  where
+    bindingContext :: AmbientContext
+    bindingContext =
+      ac Bottom Normal context.imports context.docContext
+    body = \case
+      Constructor' (ConstructorReference DD.UnitRef 0) | context.elideUnit -> pure []
+      e -> List.singleton <$> pretty0 (ac Annotation Normal context.imports context.docContext) e
+    letIntro = case sc of
+      Block -> id
+      Normal -> (fmt S.ControlKeyword "let" `PP.hang`)
+
+printLetBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
+printLetBinding context (v, binding) =
+  if Var.isAction v
+    then pretty0 context binding
+    else renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar v) binding
+
 prettyPattern ::
   forall v loc.
   (Var v) =>

From ef2df9464219608888f5576524924ba1eb406b0a Mon Sep 17 00:00:00 2001
From: Mitchell Dalvi Rosen <mitchellwrosen@gmail.com>
Date: Tue, 10 Dec 2024 12:23:15 -0500
Subject: [PATCH 3/7] add another failing transcript

---
 unison-src/transcripts/idempotent/fix-5427.md | 61 ++++++++++++++++++-
 1 file changed, 59 insertions(+), 2 deletions(-)

diff --git a/unison-src/transcripts/idempotent/fix-5427.md b/unison-src/transcripts/idempotent/fix-5427.md
index 6455f38eed..8812085e66 100644
--- a/unison-src/transcripts/idempotent/fix-5427.md
+++ b/unison-src/transcripts/idempotent/fix-5427.md
@@ -1,3 +1,60 @@
+# Issue 1
+
+``` ucm
+scratch/main> builtins.merge lib.builtin
+
+  Done.
+```
+
+``` unison
+foo : Nat
+foo = 17
+
+bar : Nat
+bar =
+  foo _ =
+    _ = foo
+    .foo
+  foo()
+```
+
+``` ucm :added-by-ucm
+  Loading changes detected in scratch.u.
+
+  I found and typechecked these definitions in scratch.u. If you
+  do an `add` or `update`, here's how your codebase would
+  change:
+
+    ⍟ These new definitions are ok to `add`:
+
+      bar : Nat
+      foo : Nat
+```
+
+``` ucm
+scratch/main> add
+
+  ⍟ I've added these definitions:
+
+    bar : Nat
+    foo : Nat
+
+scratch/main> view bar
+
+  bar : Nat
+  bar =
+    foo1 _ =
+      _ = foo
+      foo
+    foo()
+```
+
+``` ucm :hide
+scratch/main> delete.project scratch
+```
+
+# Issue 2
+
 ``` ucm
 scratch/main> builtins.merge lib.builtin
 
@@ -25,7 +82,7 @@ baz = foo + foo
   change:
 
     ⍟ These new definitions are ok to `add`:
-    
+
       bar : Nat
       baz : Nat
       foo : Nat
@@ -60,7 +117,7 @@ bar =
 
     ⍟ These names already exist. You can `update` them to your
       new definition:
-    
+
       bar : Nat
       foo : Nat
 ```

From d272484805021c75f6feb6ab4c992f0f22863c70 Mon Sep 17 00:00:00 2001
From: Mitchell Dalvi Rosen <mitchellwrosen@gmail.com>
Date: Tue, 10 Dec 2024 12:35:07 -0500
Subject: [PATCH 4/7] reset vars in a couple more places

---
 parser-typechecker/src/Unison/Syntax/TermPrinter.hs |  6 +++---
 unison-src/transcripts/idempotent/fix-5427.md       | 10 +++++-----
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
index 283bd6991f..d864435c57 100644
--- a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
+++ b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
@@ -675,7 +675,7 @@ printLetBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnot
 printLetBinding context (v, binding) =
   if Var.isAction v
     then pretty0 context binding
-    else renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar v) binding
+    else renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding
 
 prettyPattern ::
   forall v loc.
@@ -1317,7 +1317,7 @@ printAnnotate n tm =
       Set.fromList [n | v <- ABT.allVars tm, n <- varToName v]
     usedTypeNames =
       Set.fromList [n | Ann' _ ty <- ABT.subterms tm, v <- ABT.allVars ty, n <- varToName v]
-    varToName v = toList (Name.parseText (Var.name v))
+    varToName = toList . Name.parseText . Var.name . Var.reset
     go :: (Ord v) => Term2 v at ap v b -> Term2 v () () v b
     go = extraMap' id (const ()) (const ())
 
@@ -2213,7 +2213,7 @@ avoidShadowing tm (PrettyPrintEnv terms types) =
            in (HQ'.NameOnly fullName, HQ'.NameOnly resuffixifiedName)
     tweak _ p = p
     varToName :: (Var v) => v -> [Name]
-    varToName = toList . Name.parseText . Var.name
+    varToName = toList . Name.parseText . Var.name . Var.reset
 
 isLeaf :: Term2 vt at ap v a -> Bool
 isLeaf (Var' {}) = True
diff --git a/unison-src/transcripts/idempotent/fix-5427.md b/unison-src/transcripts/idempotent/fix-5427.md
index 8812085e66..cf8b25ef81 100644
--- a/unison-src/transcripts/idempotent/fix-5427.md
+++ b/unison-src/transcripts/idempotent/fix-5427.md
@@ -26,7 +26,7 @@ bar =
   change:
 
     ⍟ These new definitions are ok to `add`:
-
+    
       bar : Nat
       foo : Nat
 ```
@@ -43,9 +43,9 @@ scratch/main> view bar
 
   bar : Nat
   bar =
-    foo1 _ =
+    foo _ =
       _ = foo
-      foo
+      .foo
     foo()
 ```
 
@@ -82,7 +82,7 @@ baz = foo + foo
   change:
 
     ⍟ These new definitions are ok to `add`:
-
+    
       bar : Nat
       baz : Nat
       foo : Nat
@@ -117,7 +117,7 @@ bar =
 
     ⍟ These names already exist. You can `update` them to your
       new definition:
-
+    
       bar : Nat
       foo : Nat
 ```

From 455649784967e500ba2549b97d00c7d690d02074 Mon Sep 17 00:00:00 2001
From: Mitchell Dalvi Rosen <mitchellwrosen@gmail.com>
Date: Wed, 11 Dec 2024 19:59:27 -0500
Subject: [PATCH 5/7] distinguish between recursive and nonrecursive lets in
 term printer

---
 .../src/Unison/Syntax/TermPrinter.hs          | 155 +++++++++++++++---
 1 file changed, 131 insertions(+), 24 deletions(-)

diff --git a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
index d864435c57..09a3fc77a5 100644
--- a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
+++ b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
@@ -18,9 +18,11 @@ import Control.Lens (unsnoc)
 import Control.Monad.State (evalState)
 import Control.Monad.State qualified as State
 import Data.Char (isPrint)
+import Data.Foldable qualified as Foldable
 import Data.List
 import Data.List qualified as List
 import Data.Map qualified as Map
+import Data.Sequence qualified as Seq
 import Data.Set qualified as Set
 import Data.Text (unpack)
 import Data.Text qualified as Text
@@ -408,8 +410,7 @@ pretty0
     where
       goNormal prec tm = pretty0 (ac prec Normal im doc) tm
       specialCases term go = do
-        doc <- prettyDoc2 a term
-        case doc of
+        prettyDoc2 a term >>= \case
           Just d -> pure d
           Nothing -> notDoc go
         where
@@ -652,14 +653,14 @@ printLet ::
   (MonadPretty v m) =>
   AmbientContext ->
   BlockContext ->
-  [(v, Term3 v PrintAnnotation)] ->
+  [LetBindings v (Term3 v PrintAnnotation)] ->
   Term3 v PrintAnnotation ->
   [Pretty SyntaxText] ->
   m (Pretty SyntaxText)
 printLet context sc bs e uses = do
-  bs <- traverse (printLetBinding bindingContext) bs
+  bs <- traverse (printLetBindings bindingContext) bs
   body <- body e
-  pure . paren (sc /= Block && context.precedence >= Top) . letIntro $ PP.lines (uses <> bs <> body)
+  pure . paren (sc /= Block && context.precedence >= Top) . letIntro $ PP.lines (uses <> concat bs <> body)
   where
     bindingContext :: AmbientContext
     bindingContext =
@@ -671,12 +672,25 @@ printLet context sc bs e uses = do
       Block -> id
       Normal -> (fmt S.ControlKeyword "let" `PP.hang`)
 
+printLetBindings ::
+  (MonadPretty v m) =>
+  AmbientContext ->
+  LetBindings v (Term3 v PrintAnnotation) ->
+  m [Pretty SyntaxText]
+printLetBindings context = \case
+  LetBindings bindings -> traverse (printLetBinding context) bindings
+  LetrecBindings bindings -> traverse (printLetrecBinding context) bindings
+
 printLetBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
 printLetBinding context (v, binding) =
   if Var.isAction v
     then pretty0 context binding
     else renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding
 
+printLetrecBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
+printLetrecBinding context (v, binding) =
+  renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding
+
 prettyPattern ::
   forall v loc.
   (Var v) =>
@@ -1568,14 +1582,18 @@ allInSubBlock tm p s i =
 -- statement, need to be emitted also by this function, otherwise the `use`
 -- statement may come out at an enclosing scope instead.
 immediateChildBlockTerms ::
-  (Var vt, Var v) => Term2 vt at ap v a -> [Term2 vt at ap v a]
+  forall a ap at v vt. (Var vt, Var v) => Term2 vt at ap v a -> [Term2 vt at ap v a]
 immediateChildBlockTerms = \case
   LetBlock bs e -> concatMap doLet bs ++ handleDelay e
   _ -> []
   where
     handleDelay (Delay' b) | isLet b = [b]
     handleDelay _ = []
-    doLet (v, Ann' tm _) = doLet (v, tm)
+    doLet :: LetBindings v (Term2 vt at ap v a) -> [Term2 vt at ap v a]
+    doLet = \case
+      LetBindings bindings -> concatMap doLet2 bindings
+      LetrecBindings bindings -> concatMap doLet2 bindings
+    doLet2 (v, Ann' tm _) = doLet2 (v, tm)
     -- we don't consider 'body' to be a place we can insert a `use`
     -- clause unless it's already a let block. This avoids silliness like:
     --   x = 1 + 1
@@ -1583,8 +1601,8 @@ immediateChildBlockTerms = \case
     --   x =
     --    use Nat +
     --    1 + 1
-    doLet (v, LamsNamedOpt' _ body) = [body | not (Var.isAction v), isLet body]
-    doLet t = error (show t) []
+    doLet2 (v, LamsNamedOpt' _ body) = [body | not (Var.isAction v), isLet body]
+    doLet2 t = error (show t) []
 
 isSoftHangable :: (Var v) => Term2 vt at ap v a -> Bool
 -- isSoftHangable (Delay' d) = isLet d || isSoftHangable d || case d of
@@ -1643,42 +1661,131 @@ isBlock tm =
     Delay' _ -> True
     _ -> False
 
+-- A `LetBindings` is either:
+--
+
+-- * A list of nonrecusrive lets (e.g. let x = ... in let y = ... in let z = ... in ...), where each binding is in
+
+--   scope for all subsequent bindings.
+--
+--   In made-up syntax:
+--
+--     let
+--       x = ...
+--     in
+--       let
+--         y = ...
+--       in
+--         let
+--           z = ...
+--         in
+--           body
+--
+
+-- * A single letrec's bindings, where each binding is in scope for all subsequent bindings.
+
+--
+--   In made-up syntax:
+--
+--     letrec
+--       x = ...
+--       y = ...
+--       z = ...
+--     in
+--       body
+data LetBindings v term
+  = LetBindings [(v, term)]
+  | LetrecBindings [(v, term)]
+
+-- | A group of let bindings (with all bound variables cached at the top level for efficiency).
+--
+-- The sequence has an invariant: no two `LetBindings` in a row (that would be a single `LetBindings`).
+--
+-- For example, the bindings
+--
+--   a = ...
+--   b = ...
+--   c = ...
+--   d = ...
+--   e = ...
+--   f = ...
+--   body
+--
+-- might be two lets `a` and `b`, followed by a letrec `c` and `d`, followed by a different letrec `e`, `f`:
+--
+--   let
+--     a = ...
+--   in
+--     let
+--       b = ...
+--     in
+--       letrec
+--         c = ...
+--         d = ...
+--       in
+--         letrec
+--           e = ...
+--           f = ...
+--         in
+--           body
+data LetBindingsGroups v term
+  = LetBindingsGroups (Set v) (Seq (LetBindings v term))
+
+instance (Ord v) => Semigroup (LetBindingsGroups v term) where
+  LetBindingsGroups vs1 bs1 <> LetBindingsGroups vs2 bs2 =
+    LetBindingsGroups (Set.union vs1 vs2) (bs1 <> bs2)
+
+letBindingsToLetBindingsGroups :: (Ord v) => [(v, term)] -> LetBindingsGroups v term
+letBindingsToLetBindingsGroups bindings =
+  LetBindingsGroups (Set.fromList (map fst bindings)) (Seq.singleton (LetBindings bindings))
+
+letrecBindingsToLetBindingsGroups :: (Ord v) => [(v, term)] -> LetBindingsGroups v term
+letrecBindingsToLetBindingsGroups bindings =
+  LetBindingsGroups (Set.fromList (map fst bindings)) (Seq.singleton (LetrecBindings bindings))
+
 pattern LetBlock ::
   (Ord v) =>
-  [(v, Term2 vt at ap v a)] ->
+  [LetBindings v (Term2 vt at ap v a)] ->
   Term2 vt at ap v a ->
   Term2 vt at ap v a
-pattern LetBlock bindings body <- (unLetBlock -> Just (bindings, body))
+pattern LetBlock bindings body <-
+  (unLetBlock -> Just (LetBindingsGroups _ (Foldable.toList @Seq -> bindings), body))
 
 -- Collects nested let/let rec blocks into one minimally nested block.
 -- Handy because `let` and `let rec` blocks get rendered the same way.
 -- We preserve nesting when the inner block shadows definitions in the
 -- outer block.
 unLetBlock ::
+  forall a ap at v vt.
   (Ord v) =>
   Term2 vt at ap v a ->
-  Maybe ([(v, Term2 vt at ap v a)], Term2 vt at ap v a)
-unLetBlock t = rec t
+  Maybe (LetBindingsGroups v (Term2 vt at ap v a), Term2 vt at ap v a)
+unLetBlock = rec
   where
-    dontIntersect v1s v2s =
-      all (`Set.notMember` v2set) (fst <$> v1s)
-      where
-        v2set = Set.fromList (fst <$> v2s)
+    dontIntersect :: LetBindingsGroups v term -> LetBindingsGroups v term -> Bool
+    dontIntersect (LetBindingsGroups xs _) (LetBindingsGroups ys _) =
+      Set.disjoint xs ys
+
+    rec :: Term2 vt at ap v a -> Maybe (LetBindingsGroups v (Term2 vt at ap v a), Term2 vt at ap v a)
     rec t = case unLetRecNamed t of
       Nothing -> nonrec t
-      Just (_isTop, bindings, body) -> case rec body of
-        Just (innerBindings, innerBody)
-          | dontIntersect bindings innerBindings ->
-              Just (bindings ++ innerBindings, innerBody)
-        _ -> Just (bindings, body)
+      Just (_isTop, bindings0, body) ->
+        let bindings = letrecBindingsToLetBindingsGroups bindings0
+         in case rec body of
+              Just (innerBindings, innerBody)
+                | dontIntersect bindings innerBindings ->
+                    Just (bindings <> innerBindings, innerBody)
+              _ -> Just (bindings, body)
+
+    nonrec :: Term2 vt at ap v a -> Maybe (LetBindingsGroups v (Term2 vt at ap v a), Term2 vt at ap v a)
     nonrec t = case unLet t of
       Nothing -> Nothing
       Just (bindings0, body) ->
-        let bindings = [(v, b) | (_, v, b) <- bindings0]
+        let bindings = letBindingsToLetBindingsGroups [(v, b) | (_, v, b) <- bindings0]
          in case rec body of
               Just (innerBindings, innerBody)
                 | dontIntersect bindings innerBindings ->
-                    Just (bindings ++ innerBindings, innerBody)
+                    Just (bindings <> innerBindings, innerBody)
               _ -> Just (bindings, body)
 
 pattern LamsNamedMatch' ::

From eca815c6d5a1bbb32513e3e7f4218437e9163ea6 Mon Sep 17 00:00:00 2001
From: Mitchell Dalvi Rosen <mitchellwrosen@gmail.com>
Date: Wed, 18 Dec 2024 12:04:14 -0500
Subject: [PATCH 6/7] add bound terms to term printer environment

---
 parser-typechecker/package.yaml               |   1 +
 .../src/Unison/PrettyPrintEnv/MonadPretty.hs  |  62 ++++----
 .../src/Unison/Syntax/TermPrinter.hs          | 132 ++++++++++--------
 .../src/Unison/Syntax/TypePrinter.hs          |   9 +-
 .../unison-parser-typechecker.cabal           |   4 +-
 5 files changed, 116 insertions(+), 92 deletions(-)

diff --git a/parser-typechecker/package.yaml b/parser-typechecker/package.yaml
index d9760e15c9..a6757ae515 100644
--- a/parser-typechecker/package.yaml
+++ b/parser-typechecker/package.yaml
@@ -103,6 +103,7 @@ default-extensions:
   - ApplicativeDo
   - BangPatterns
   - BlockArguments
+  - ConstraintKinds
   - DeriveAnyClass
   - DeriveFunctor
   - DeriveGeneric
diff --git a/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs b/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs
index cace699ec8..2c7b9ae56e 100644
--- a/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs
+++ b/parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs
@@ -1,38 +1,31 @@
-{-# LANGUAGE ConstraintKinds #-}
-
-module Unison.PrettyPrintEnv.MonadPretty where
-
-import Control.Lens (views, _1, _2)
+module Unison.PrettyPrintEnv.MonadPretty
+  ( MonadPretty,
+    Env (..),
+    runPretty,
+    addTypeVars,
+    willCaptureType,
+  )
+where
+
+import Control.Lens (views)
 import Control.Monad.Reader (MonadReader, Reader, local, runReader)
 import Data.Set qualified as Set
 import Unison.Prelude
 import Unison.PrettyPrintEnv (PrettyPrintEnv)
+import Unison.Util.Set qualified as Set
 import Unison.Var (Var)
 
-type MonadPretty v m = (Var v, MonadReader (PrettyPrintEnv, Set v) m)
-
-getPPE :: (MonadPretty v m) => m PrettyPrintEnv
-getPPE = view _1
-
--- | Run a computation with a modified PrettyPrintEnv, restoring the original
-withPPE :: (MonadPretty v m) => PrettyPrintEnv -> m a -> m a
-withPPE p = local (set _1 p)
+type MonadPretty v m = (Var v, MonadReader (Env v) m)
 
-applyPPE :: (MonadPretty v m) => (PrettyPrintEnv -> a) -> m a
-applyPPE = views _1
-
-applyPPE2 :: (MonadPretty v m) => (PrettyPrintEnv -> a -> b) -> a -> m b
-applyPPE2 f a = views _1 (`f` a)
-
-applyPPE3 :: (MonadPretty v m) => (PrettyPrintEnv -> a -> b -> c) -> a -> b -> m c
-applyPPE3 f a b = views _1 (\ppe -> f ppe a b)
-
--- | Run a computation with a modified PrettyPrintEnv, restoring the original
-modifyPPE :: (MonadPretty v m) => (PrettyPrintEnv -> PrettyPrintEnv) -> m a -> m a
-modifyPPE = local . over _1
+data Env v = Env
+  { boundTerms :: !(Set v),
+    boundTypes :: !(Set v),
+    ppe :: !PrettyPrintEnv
+  }
+  deriving stock (Generic)
 
 modifyTypeVars :: (MonadPretty v m) => (Set v -> Set v) -> m a -> m a
-modifyTypeVars = local . over _2
+modifyTypeVars = local . over #boundTypes
 
 -- | Add type variables to the set of variables that need to be avoided
 addTypeVars :: (MonadPretty v m) => [v] -> m a -> m a
@@ -40,8 +33,15 @@ addTypeVars = modifyTypeVars . Set.union . Set.fromList
 
 -- | Check if a list of type variables contains any variables that need to be
 -- avoided
-willCapture :: (MonadPretty v m) => [v] -> m Bool
-willCapture vs = views _2 (not . Set.null . Set.intersection (Set.fromList vs))
-
-runPretty :: (Var v) => PrettyPrintEnv -> Reader (PrettyPrintEnv, Set v) a -> a
-runPretty ppe m = runReader m (ppe, mempty)
+willCaptureType :: (MonadPretty v m) => [v] -> m Bool
+willCaptureType vs = views #boundTypes (Set.intersects (Set.fromList vs))
+
+runPretty :: (Var v) => PrettyPrintEnv -> Reader (Env v) a -> a
+runPretty ppe m =
+  runReader
+    m
+    Env
+      { boundTerms = Set.empty,
+        boundTypes = Set.empty,
+        ppe
+      }
diff --git a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
index 09a3fc77a5..d4c9a4684b 100644
--- a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
+++ b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
@@ -68,6 +68,7 @@ import Unison.Util.Pretty qualified as PP
 import Unison.Util.SyntaxText qualified as S
 import Unison.Var (Var)
 import Unison.Var qualified as Var
+import Control.Monad.Reader (ask)
 
 type SyntaxText = S.SyntaxText' Reference
 
@@ -99,7 +100,8 @@ data AmbientContext = AmbientContext
     infixContext :: !InfixContext,
     imports :: !Imports,
     docContext :: !DocLiteralContext,
-    elideUnit :: !Bool -- `True` if a `()` at the end of a block should be elided
+    -- `True` if a `()` at the end of a block should be elided
+    elideUnit :: !Bool
   }
 
 -- Description of the position of this ABT node, when viewed in the
@@ -215,23 +217,24 @@ pretty0
     }
   term =
     specialCases term \case
-      Var' v -> pure . parenIfInfix name ic $ styleHashQualified'' (fmt S.Var) name
+      Var' v -> do
+        pure . parenIfInfix name ic $ styleHashQualified'' (fmt S.Var) name
         where
           -- OK since all term vars are user specified, any freshening was just added during typechecking
           name = elideFQN im $ HQ.unsafeFromVar (Var.reset v)
       Ref' r -> do
-        n <- getPPE
-        let name = elideFQN im $ PrettyPrintEnv.termName n (Referent.Ref r)
+        env <- ask
+        let name = elideFQN im $ PrettyPrintEnv.termName env.ppe (Referent.Ref r)
         pure . parenIfInfix name ic $ styleHashQualified'' (fmt $ S.TermReference (Referent.Ref r)) name
       TermLink' r -> do
-        n <- getPPE
-        let name = elideFQN im $ PrettyPrintEnv.termName n r
+        env <- ask
+        let name = elideFQN im $ PrettyPrintEnv.termName env.ppe r
         pure . paren (p >= Application) $
           fmt S.LinkKeyword "termLink "
             <> parenIfInfix name ic (styleHashQualified'' (fmt $ S.TermReference r) name)
       TypeLink' r -> do
-        n <- getPPE
-        let name = elideFQN im $ PrettyPrintEnv.typeName n r
+        env <- ask
+        let name = elideFQN im $ PrettyPrintEnv.typeName env.ppe r
         pure . paren (p >= Application) $
           fmt S.LinkKeyword "typeLink "
             <> parenIfInfix name ic (styleHashQualified'' (fmt $ S.TypeReference r) name)
@@ -277,13 +280,13 @@ pretty0
           Nothing -> '?' : [c]
       Blank' id -> pure $ fmt S.Blank $ l "_" <> l (fromMaybe "" (Blank.nameb id))
       Constructor' ref -> do
-        n <- getPPE
-        let name = elideFQN im $ PrettyPrintEnv.termName n conRef
+        env <- ask
+        let name = elideFQN im $ PrettyPrintEnv.termName env.ppe conRef
             conRef = Referent.Con ref CT.Data
         pure $ styleHashQualified'' (fmt $ S.TermReference conRef) name
       Request' ref -> do
-        n <- getPPE
-        let name = elideFQN im $ PrettyPrintEnv.termName n conRef
+        env <- ask
+        let name = elideFQN im $ PrettyPrintEnv.termName env.ppe conRef
             conRef = Referent.Con ref CT.Effect
         pure $ styleHashQualified'' (fmt $ S.TermReference conRef) name
       Handle' h body -> do
@@ -370,12 +373,12 @@ pretty0
       -- See `isDestructuringBind` definition.
       Match' scrutinee cs@[MatchCase pat guard (AbsN' vs body)]
         | p <= Control && isDestructuringBind scrutinee cs -> do
-            n <- getPPE
+            env <- ask
             let letIntro = case bc of
                   Block -> id
                   Normal -> \x -> fmt S.ControlKeyword "let" `PP.hang` x
             lhs <- do
-              let (lhs, _) = prettyPattern n (ac Annotation Block im doc) Application vs pat
+              let (lhs, _) = prettyPattern env.ppe (ac Annotation Block im doc) Application vs pat
               guard' <- printGuard guard
               pure $ PP.group lhs `PP.hang` guard'
             let eq = fmt S.BindingEquals "="
@@ -415,20 +418,20 @@ pretty0
           Nothing -> notDoc go
         where
           notDoc go = do
-            n <- getPPE
+            env <- ask
             let -- This predicate controls which binary functions we render as infix
                 -- operators. At the moment the policy is just to render symbolic
                 -- operators as infix.
                 binaryOpsPred :: Term3 v PrintAnnotation -> Bool
                 binaryOpsPred = \case
-                  Ref' r -> isSymbolic $ PrettyPrintEnv.termName n (Referent.Ref r)
+                  Ref' r -> isSymbolic $ PrettyPrintEnv.termName env.ppe (Referent.Ref r)
                   Var' v -> isSymbolic $ HQ.unsafeFromVar v
                   _ -> False
                 -- Gets the precedence of an infix operator, if it has one.
                 termPrecedence :: Term3 v PrintAnnotation -> Maybe Precedence
                 termPrecedence = \case
                   Ref' r ->
-                    HQ.toName (PrettyPrintEnv.termName n (Referent.Ref r))
+                    HQ.toName (PrettyPrintEnv.termName env.ppe (Referent.Ref r))
                       >>= operatorPrecedence
                         . NameSegment.toEscapedText
                         . Name.lastSegment
@@ -523,11 +526,14 @@ pretty0
               (DD.Doc, _)
                 | doc == MaybeDoc ->
                     if isDocLiteral term
-                      then applyPPE3 prettyDoc im term
+                      then do
+                        env <- ask
+                        pure (prettyDoc env.ppe im term)
                       else pretty0 (a {docContext = NoDoc}) term
               (TupleTerm' [x], _) -> do
                 let conRef = DD.pairCtorRef
-                name <- elideFQN im <$> applyPPE2 PrettyPrintEnv.termName conRef
+                env <- ask
+                let name = elideFQN im (PrettyPrintEnv.termName env.ppe conRef)
                 let pair = parenIfInfix name ic $ styleHashQualified'' (fmt (S.TermReference conRef)) name
                 x' <- pretty0 (ac Application Normal im doc) x
                 pure . paren (p >= Application) $
@@ -685,7 +691,21 @@ printLetBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnot
 printLetBinding context (v, binding) =
   if Var.isAction v
     then pretty0 context binding
-    else renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding
+    else
+      -- For a non-recursive let binding like "let x = y in z", variable "x" is not bound in "y". Yet, "x" may be free
+      -- in "y" anyway, referring to some previous binding.
+      --
+      -- In Unison we don't have a syntax, for non-recusrive let, though, we just have this:
+      --
+      --   x = y
+      --   z
+      --
+      -- So, render free "x" in "y" with a leading dot. This is because we happen to know that the only way to have
+      -- a free "x" in "y" is if "x" is a top-level binding.
+      let
+      v1 = Var.reset v
+      in
+      renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar v1) binding
 
 printLetrecBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
 printLetrecBinding context (v, binding) =
@@ -877,8 +897,8 @@ printCase im doc ms0 =
     go (pats, vs, unzip -> (guards, bodies)) = do
       guards' <- traverse printGuard guards
       bodies' <- traverse printBody bodies
-      ppe <- getPPE
-      pure (patLhs ppe vs pats, guards', bodies')
+      env <- ask
+      pure (patLhs env.ppe vs pats, guards', bodies')
       where
         noGuards = all (== Nothing) guards
         printGuard Nothing | noGuards = pure mempty
@@ -967,8 +987,8 @@ prettyBinding0 ::
   Term2 v at ap v a ->
   m PrettyBinding
 prettyBinding0 ac v tm = do
-  ppe <- getPPE
-  prettyBinding0' ac v (printAnnotate ppe tm)
+  env <- ask
+  prettyBinding0' ac v (printAnnotate env.ppe tm)
 
 prettyBinding0' ::
   (MonadPretty v m) =>
@@ -1889,7 +1909,7 @@ prettyDoc2 ::
   Term3 v PrintAnnotation ->
   m (Maybe (Pretty SyntaxText))
 prettyDoc2 ac tm = do
-  ppe <- getPPE
+  env <- ask
   let brace p =
         if PP.isMultiLine p
           then fmt S.DocDelimiter "{{" <> PP.newline <> p <> PP.newline <> fmt S.DocDelimiter "}}"
@@ -1909,11 +1929,11 @@ prettyDoc2 ac tm = do
       makeFence inner = PP.string $ replicate (max 3 $ longestRun '`' inner) '`'
       go :: Width -> Term3 v PrintAnnotation -> m (Pretty SyntaxText)
       go hdr = \case
-        (toDocTransclude ppe -> Just d) ->
+        (toDocTransclude env.ppe -> Just d) ->
           bail d
-        (toDocUntitledSection ppe -> Just ds) ->
+        (toDocUntitledSection env.ppe -> Just ds) ->
           sepBlankline ds
-        (toDocSection ppe -> Just (title, ds)) -> do
+        (toDocSection env.ppe -> Just (title, ds)) -> do
           prettyTitle <- rec title
           prettyDs <- intercalateMapM "\n\n" (go (hdr + 1)) ds
           pure $
@@ -1922,19 +1942,19 @@ prettyDoc2 ac tm = do
                 "",
                 PP.indentN (hdr + 1) prettyDs
               ]
-        (toDocParagraph ppe -> Just ds) ->
+        (toDocParagraph env.ppe -> Just ds) ->
           PP.wrap . mconcat <$> traverse rec ds
-        (toDocBulletedList ppe -> Just ds) -> do
+        (toDocBulletedList env.ppe -> Just ds) -> do
           PP.lines <$> traverse item ds
           where
             item d = ("* " <>) . PP.indentAfterNewline "  " <$> rec d
-        (toDocNumberedList ppe -> Just (n, ds)) ->
+        (toDocNumberedList env.ppe -> Just (n, ds)) ->
           PP.column2 <$> traverse item (zip [n ..] ds)
           where
             item (n, d) = (PP.group (PP.shown n <> "."),) <$> rec d
-        (toDocWord ppe -> Just t) ->
+        (toDocWord env.ppe -> Just t) ->
           pure $ PP.text t
-        (toDocCode ppe -> Just d) -> do
+        (toDocCode env.ppe -> Just d) -> do
           inner <- rec d
           let quotes =
                 -- Prefer ` if there aren't any in the inner text,
@@ -1943,67 +1963,67 @@ prettyDoc2 ac tm = do
                   then PP.string $ oneMore '\'' inner
                   else PP.string "`"
           pure $ PP.group $ quotes <> inner <> quotes
-        (toDocJoin ppe -> Just ds) -> foldMapM rec ds
-        (toDocItalic ppe -> Just d) -> do
+        (toDocJoin env.ppe -> Just ds) -> foldMapM rec ds
+        (toDocItalic env.ppe -> Just d) -> do
           inner <- rec d
           let underscores = PP.string $ oneMore '_' inner
           pure $ PP.group $ underscores <> inner <> underscores
-        (toDocBold ppe -> Just d) -> do
+        (toDocBold env.ppe -> Just d) -> do
           inner <- rec d
           let stars = PP.string $ oneMore '*' inner
           pure $ PP.group $ stars <> inner <> stars
-        (toDocStrikethrough ppe -> Just d) -> do
+        (toDocStrikethrough env.ppe -> Just d) -> do
           inner <- rec d
           let quotes = PP.string $ oneMore '~' inner
           pure $ PP.group $ quotes <> inner <> quotes
-        (toDocGroup ppe -> Just d) ->
+        (toDocGroup env.ppe -> Just d) ->
           PP.group <$> rec d
-        (toDocColumn ppe -> Just ds) ->
+        (toDocColumn env.ppe -> Just ds) ->
           PP.lines <$> traverse rec ds
-        (toDocNamedLink ppe -> Just (name, target)) ->
+        (toDocNamedLink env.ppe -> Just (name, target)) ->
           do
             name' <- rec name
             target' <- rec target
             pure $ PP.group $ "[" <> name' <> "](" <> target' <> ")"
-        (toDocLink ppe -> Just e) -> pure . PP.group $ case e of
+        (toDocLink env.ppe -> Just e) -> pure . PP.group $ case e of
           Left r -> "{type " <> tyName r <> "}"
           Right r -> "{" <> tmName r <> "}"
-        (toDocEval ppe -> Just tm) ->
+        (toDocEval env.ppe -> Just tm) ->
           do
             inner <- pretty0 ac tm
             let fence = makeFence inner
             pure $ PP.lines [fence, inner, fence]
-        (toDocEvalInline ppe -> Just tm) ->
+        (toDocEvalInline env.ppe -> Just tm) ->
           do
             inner <- pretty0 ac tm
             pure $ "@eval{" <> inner <> "}"
-        (toDocExample ppe -> Just tm) ->
+        (toDocExample env.ppe -> Just tm) ->
           do
             inner <- pretty0 ac tm
             pure $ "``" <> inner <> "``"
-        (toDocExampleBlock ppe -> Just tm) ->
+        (toDocExampleBlock env.ppe -> Just tm) ->
           do
             inner <- pretty0 ac' tm
             let fence = makeFence inner
             pure $ PP.lines ["@typecheck " <> fence, inner, fence]
           where
             ac' = ac {elideUnit = True}
-        (toDocSource ppe -> Just es) ->
+        (toDocSource env.ppe -> Just es) ->
           pure . PP.group $ "    @source{" <> intercalateMap ", " go es <> "}"
           where
             go (Left r, _anns) = "type " <> tyName r
             go (Right r, _anns) = tmName r
-        (toDocFoldedSource ppe -> Just es) ->
+        (toDocFoldedSource env.ppe -> Just es) ->
           pure . PP.group $ "    @foldedSource{" <> intercalateMap ", " go es <> "}"
           where
             go (Left r, _anns) = "type " <> tyName r
             go (Right r, _anns) = tmName r
-        (toDocSignatureInline ppe -> Just tm) ->
+        (toDocSignatureInline env.ppe -> Just tm) ->
           pure . PP.group $ "@inlineSignature{" <> tmName tm <> "}"
-        (toDocSignature ppe -> Just tms) ->
+        (toDocSignature env.ppe -> Just tms) ->
           let name = if length tms == 1 then "@signature" else "@signatures"
            in pure . PP.group $ "    " <> name <> "{" <> intercalateMap ", " tmName tms <> "}"
-        (toDocCodeBlock ppe -> Just (typ, txt)) ->
+        (toDocCodeBlock env.ppe -> Just (typ, txt)) ->
           pure $
             let txt' = PP.text txt
                 fence = makeFence txt'
@@ -2013,7 +2033,7 @@ prettyDoc2 ac tm = do
                       PP.group txt',
                       fence
                     ]
-        (toDocVerbatim ppe -> Just txt) ->
+        (toDocVerbatim env.ppe -> Just txt) ->
           pure $
             PP.group $
               PP.lines
@@ -2025,15 +2045,15 @@ prettyDoc2 ac tm = do
         tm -> bail tm
         where
           im = imports ac
-          tyName r = styleHashQualified'' (fmt $ S.TypeReference r) . elideFQN im $ PrettyPrintEnv.typeName ppe r
-          tmName r = styleHashQualified'' (fmt $ S.TermReference r) . elideFQN im $ PrettyPrintEnv.termName ppe r
+          tyName r = styleHashQualified'' (fmt $ S.TypeReference r) . elideFQN im $ PrettyPrintEnv.typeName env.ppe r
+          tmName r = styleHashQualified'' (fmt $ S.TermReference r) . elideFQN im $ PrettyPrintEnv.termName env.ppe r
           rec = go hdr
           sepBlankline = intercalateMapM "\n\n" rec
   case tm of
     -- these patterns can introduce a {{ .. }} block
-    (toDocUntitledSection ppe -> Just _) -> Just . brace <$> go 1 tm
-    (toDocSection ppe -> Just _) -> Just . brace <$> go 1 tm
-    (toDocParagraph ppe -> Just _) -> Just . brace <$> go 1 tm
+    (toDocUntitledSection env.ppe -> Just _) -> Just . brace <$> go 1 tm
+    (toDocSection env.ppe -> Just _) -> Just . brace <$> go 1 tm
+    (toDocParagraph env.ppe -> Just _) -> Just . brace <$> go 1 tm
     _ -> pure Nothing
 
 toDocJoin :: PrettyPrintEnv -> Term3 v PrintAnnotation -> Maybe [Term3 v PrintAnnotation]
diff --git a/parser-typechecker/src/Unison/Syntax/TypePrinter.hs b/parser-typechecker/src/Unison/Syntax/TypePrinter.hs
index 271546e776..90cd52943e 100644
--- a/parser-typechecker/src/Unison/Syntax/TypePrinter.hs
+++ b/parser-typechecker/src/Unison/Syntax/TypePrinter.hs
@@ -17,6 +17,7 @@ module Unison.Syntax.TypePrinter
   )
 where
 
+import Control.Monad.Reader (ask)
 import Data.Map qualified as Map
 import Unison.Builtin.Decls qualified as DD
 import Unison.HashQualified (HashQualified)
@@ -25,7 +26,7 @@ import Unison.Prelude
 import Unison.PrettyPrintEnv (PrettyPrintEnv)
 import Unison.PrettyPrintEnv qualified as PrettyPrintEnv
 import Unison.PrettyPrintEnv.FQN (Imports, elideFQN)
-import Unison.PrettyPrintEnv.MonadPretty (MonadPretty, getPPE, runPretty, willCapture)
+import Unison.PrettyPrintEnv.MonadPretty (Env (..), MonadPretty, runPretty, willCaptureType)
 import Unison.Reference (Reference, pattern Builtin)
 import Unison.Referent (Referent)
 import Unison.Settings qualified as Settings
@@ -101,8 +102,8 @@ prettyRaw im p tp = go im p tp
       DD.TupleType' xs | length xs /= 1 -> PP.parenthesizeCommas <$> traverse (go im 0) xs
       -- Would be nice to use a different SyntaxHighlights color if the reference is an ability.
       Ref' r -> do
-        n <- getPPE
-        pure $ styleHashQualified'' (fmt $ S.TypeReference r) $ elideFQN im (PrettyPrintEnv.typeName n r)
+        env <- ask
+        pure $ styleHashQualified'' (fmt $ S.TypeReference r) $ elideFQN im (PrettyPrintEnv.typeName env.ppe r)
       Cycle' _ _ -> pure $ fromString "bug: TypeParser does not currently emit Cycle"
       Abs' _ -> pure $ fromString "bug: TypeParser does not currently emit Abs"
       Ann' _ _ -> pure $ fromString "bug: TypeParser does not currently emit Ann"
@@ -125,7 +126,7 @@ prettyRaw im p tp = go im p tp
             -- are universally quantified, then we can omit the `forall` keyword
             -- only if the type variables are not bound in an outer scope
             if p < 0 && not Settings.debugRevealForalls && all Var.universallyQuantifyIfFree vs
-              then ifM (willCapture vs) (prettyForall p) (go im p body)
+              then ifM (willCaptureType vs) (prettyForall p) (go im p body)
               else paren (p >= 0) <$> prettyForall (-1)
       t@(Arrow' _ _) -> case t of
         EffectfulArrows' (Ref' DD.UnitRef) rest ->
diff --git a/parser-typechecker/unison-parser-typechecker.cabal b/parser-typechecker/unison-parser-typechecker.cabal
index 820c2bec16..0e8691bbb2 100644
--- a/parser-typechecker/unison-parser-typechecker.cabal
+++ b/parser-typechecker/unison-parser-typechecker.cabal
@@ -1,6 +1,6 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.37.0.
+-- This file has been generated from package.yaml by hpack version 0.36.0.
 --
 -- see: https://github.com/sol/hpack
 
@@ -165,6 +165,7 @@ library
       ApplicativeDo
       BangPatterns
       BlockArguments
+      ConstraintKinds
       DeriveAnyClass
       DeriveFunctor
       DeriveGeneric
@@ -285,6 +286,7 @@ test-suite parser-typechecker-tests
       ApplicativeDo
       BangPatterns
       BlockArguments
+      ConstraintKinds
       DeriveAnyClass
       DeriveFunctor
       DeriveGeneric

From 28884e3eabee3607a54c209d0160724ca0a4e038 Mon Sep 17 00:00:00 2001
From: Mitchell Dalvi Rosen <mitchellwrosen@gmail.com>
Date: Wed, 18 Dec 2024 12:53:00 -0500
Subject: [PATCH 7/7] fix let-capture issue in term renderer

---
 .../src/Unison/Syntax/TermPrinter.hs          | 29 +++++++++---------
 unison-src/transcripts/idempotent/fix-5427.md | 30 ++++++-------------
 2 files changed, 24 insertions(+), 35 deletions(-)

diff --git a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
index d4c9a4684b..717a7726d3 100644
--- a/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
+++ b/parser-typechecker/src/Unison/Syntax/TermPrinter.hs
@@ -15,6 +15,7 @@ module Unison.Syntax.TermPrinter
 where
 
 import Control.Lens (unsnoc)
+import Control.Monad.Reader (ask, local)
 import Control.Monad.State (evalState)
 import Control.Monad.State qualified as State
 import Data.Char (isPrint)
@@ -53,7 +54,7 @@ import Unison.Referent (Referent)
 import Unison.Referent qualified as Referent
 import Unison.Syntax.HashQualified qualified as HQ (unsafeFromVar)
 import Unison.Syntax.Lexer.Unison (showEscapeChar)
-import Unison.Syntax.Name qualified as Name (isSymboly, parseText, parseTextEither, toText, unsafeParseText)
+import Unison.Syntax.Name qualified as Name (isSymboly, parseText, parseTextEither, toText, unsafeParseText, unsafeParseVar)
 import Unison.Syntax.NamePrinter (styleHashQualified'')
 import Unison.Syntax.NameSegment qualified as NameSegment (toEscapedText)
 import Unison.Syntax.Precedence (InfixPrecedence (..), Precedence (..), increment, isTopLevelPrecedence, operatorPrecedence)
@@ -68,7 +69,6 @@ import Unison.Util.Pretty qualified as PP
 import Unison.Util.SyntaxText qualified as S
 import Unison.Var (Var)
 import Unison.Var qualified as Var
-import Control.Monad.Reader (ask)
 
 type SyntaxText = S.SyntaxText' Reference
 
@@ -217,11 +217,13 @@ pretty0
     }
   term =
     specialCases term \case
-      Var' v -> do
+      Var' (Var.reset -> v) -> do
+        env <- ask
+        let name =
+              if Set.member v env.boundTerms
+                then HQ.fromName (Name.makeAbsolute (Name.unsafeParseVar v))
+                else elideFQN im $ HQ.unsafeFromVar v
         pure . parenIfInfix name ic $ styleHashQualified'' (fmt S.Var) name
-        where
-          -- OK since all term vars are user specified, any freshening was just added during typechecking
-          name = elideFQN im $ HQ.unsafeFromVar (Var.reset v)
       Ref' r -> do
         env <- ask
         let name = elideFQN im $ PrettyPrintEnv.termName env.ppe (Referent.Ref r)
@@ -688,10 +690,9 @@ printLetBindings context = \case
   LetrecBindings bindings -> traverse (printLetrecBinding context) bindings
 
 printLetBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
-printLetBinding context (v, binding) =
-  if Var.isAction v
-    then pretty0 context binding
-    else
+printLetBinding context (v, binding)
+  | Var.isAction v = pretty0 context binding
+  | otherwise =
       -- For a non-recursive let binding like "let x = y in z", variable "x" is not bound in "y". Yet, "x" may be free
       -- in "y" anyway, referring to some previous binding.
       --
@@ -702,10 +703,10 @@ printLetBinding context (v, binding) =
       --
       -- So, render free "x" in "y" with a leading dot. This is because we happen to know that the only way to have
       -- a free "x" in "y" is if "x" is a top-level binding.
-      let
-      v1 = Var.reset v
-      in
-      renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar v1) binding
+      renderPrettyBinding
+        <$> local (over #boundTerms (Set.insert v1)) (prettyBinding0' context (HQ.unsafeFromVar v1) binding)
+  where
+    v1 = Var.reset v
 
 printLetrecBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
 printLetrecBinding context (v, binding) =
diff --git a/unison-src/transcripts/idempotent/fix-5427.md b/unison-src/transcripts/idempotent/fix-5427.md
index cf8b25ef81..f403f10d04 100644
--- a/unison-src/transcripts/idempotent/fix-5427.md
+++ b/unison-src/transcripts/idempotent/fix-5427.md
@@ -122,9 +122,9 @@ bar =
       foo : Nat
 ```
 
-This should succeed, but `bar` gets printed incorrectly\!
+Previously, `bar` would incorrectly print with a `foo = foo` line. Now, it works.
 
-``` ucm :error
+``` ucm
 scratch/main> update
 
   Okay, I'm searching the branch for code that needs to be
@@ -132,26 +132,14 @@ scratch/main> update
 
   That's done. Now I'm making sure everything typechecks...
 
-  Typechecking failed. I've updated your scratch file with the
-  definitions that need fixing. Once the file is compiling, try
-  `update` again.
-```
-
-``` unison :added-by-ucm scratch.u
-foo : Nat
-foo = 18
-
-bar : Nat
-bar =
-  foo = foo
-  foo
+  Everything typechecks, so I'm saving the results...
 
--- The definitions below no longer typecheck with the changes above.
--- Please fix the errors and try `update` again.
+  Done.
 
-baz : Nat
-baz =
-  use Nat +
-  foo + foo
+scratch/main> view bar
 
+  bar : Nat
+  bar =
+    foo = .foo
+    foo
 ```