Merge pull request #5528 from unisonweb/fix-5525

Author: aryairani

parser-typechecker/src/Unison/PrettyPrintEnv/MonadPretty.hs

@@ -4,6 +4,8 @@ module Unison.PrettyPrintEnv.MonadPretty
     runPretty,
     addTypeVars,
     willCaptureType,
+    withBoundTerm,
+    withBoundTerms,
   )
 where
 
@@ -14,12 +16,15 @@ import Unison.Prelude
 import Unison.PrettyPrintEnv (PrettyPrintEnv)
 import Unison.Util.Set qualified as Set
 import Unison.Var (Var)
+import Unison.Var qualified as Var
 
 type MonadPretty v m = (Var v, MonadReader (Env v) m)
 
+-- See Note [Bound and free term variables] for an explanation of boundTerms/freeTerms
 data Env v = Env
   { boundTerms :: !(Set v),
     boundTypes :: !(Set v),
+    freeTerms :: !(Set v),
     ppe :: !PrettyPrintEnv
   }
   deriving stock (Generic)
@@ -36,12 +41,76 @@ addTypeVars = modifyTypeVars . Set.union . Set.fromList
 willCaptureType :: (MonadPretty v m) => [v] -> m Bool
 willCaptureType vs = views #boundTypes (Set.intersects (Set.fromList vs))
 
+withBoundTerm :: (MonadPretty v m) => v -> m a -> m a
+withBoundTerm v =
+  local (over #boundTerms (Set.insert (Var.reset v)))
+
+withBoundTerms :: (MonadPretty v m) => [v] -> m a -> m a
+withBoundTerms vs =
+  local (over #boundTerms (Set.union (foldMap (Set.singleton . Var.reset) vs)))
+
 runPretty :: (Var v) => PrettyPrintEnv -> Reader (Env v) a -> a
 runPretty ppe m =
   runReader
     m
     Env
       { boundTerms = Set.empty,
         boundTypes = Set.empty,
+        freeTerms = Set.empty,
         ppe
       }
+
+-- Note [Bound and free term variables]
+--
+-- When rendering a Unison file, we render top-level bindings independently, which may end up referring to each
+-- other after all are parsed together. Any individual term, therefore, may have free variables. For example,
+--
+--     foo = ... bar ...
+--               ^^^
+--               this "bar" variable is free in foo
+--
+--     bar = ...
+--     ^^^
+--     it's ultimately bound by a different top-level term rendering
+--
+-- Therefore, we pass down all free variables of a top-level term binding, so that we can decide, when rendering one of
+-- them, whether to add a leading dot.
+--
+-- Now, when do we need to add a leading dot? Basically, any time a binder introduces a var that, when rendered reset,
+-- clashes with the free var.
+--
+-- Here are a few examples using a made-up Unison syntax in which we can see whether a let is recursive or
+-- non-recursive, and using "%" to separate a var name from its unique id.
+--
+-- Example 1
+--
+--   Made-up syntax                      Actual syntax
+--   --------------                      ----------------
+--   foo%0 =                             foo =
+--     let bar%0 = bar%0                   bar = #someref -- rendered as ".bar", then parsed as var "bar"
+--     in 5                                5
+--
+--   bar%0 = ...                         bar = ...
+--
+-- In this example, we have a non-recursive let that binds a local variable called bar%0. The body of the bar%0 binding
+-- can itself refer to a different bar%0, which isn't captured, since a non-recursive let binding body can't refer to
+-- the binding.
+--
+-- So, when rendering the free bar%0 in the right-hand side, we ask: should we add a leading dot? And the answer is: is
+-- the var bar%0 in the set of all reset locally-bound vars {bar%0}? Yes? Then yes.
+--
+-- Example 2
+--
+--   Made-up syntax                      Actual syntax
+--   --------------                      ----------------
+--   foo%0 =                             foo =
+--     letrec bar%1 = do bar%0 hey%0       bar = do #someref hey -- rendered as ".bar", then parsed as var "bar"
+--            hey%0 = do bar%1             hey = do bar
+--     in 5                                5
+--
+--   bar%0 = ...                         bar = ...
+--
+-- In this example, we have a recursive let that binds a bar%1 variable, and refers to bar%0 from inside. Same
+-- situation, but variable resetting is relevant, because when walking underneath binder bar%1, we want to add its reset
+-- form (bar%0) to the set of bound variables to check against, when rendering a free var (which we assume to have
+-- unique id 0).

parser-typechecker/src/Unison/Syntax/TermPrinter.hs

@@ -217,12 +217,12 @@ pretty0
     }
   term =
     specialCases term \case
-      Var' (Var.reset -> v) -> do
+      Var' v -> do
         env <- ask
         let name =
-              if Set.member v env.boundTerms
+              if Set.member v env.freeTerms && Set.member v env.boundTerms
                 then HQ.fromName (Name.makeAbsolute (Name.unsafeParseVar v))
-                else elideFQN im $ HQ.unsafeFromVar v
+                else elideFQN im $ HQ.unsafeFromVar (Var.reset v)
         pure . parenIfInfix name ic $ styleHashQualified'' (fmt S.Var) name
       Ref' r -> do
         env <- ask
@@ -687,30 +687,21 @@ printLetBindings ::
   m [Pretty SyntaxText]
 printLetBindings context = \case
   LetBindings bindings -> traverse (printLetBinding context) bindings
-  LetrecBindings bindings -> traverse (printLetrecBinding context) bindings
+  LetrecBindings bindings ->
+    let boundVars = map fst bindings
+     in traverse (printLetrecBinding context boundVars) bindings
 
 printLetBinding :: (MonadPretty v m) => AmbientContext -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
 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.
-      --
-      -- 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.
-      renderPrettyBinding
-        <$> local (over #boundTerms (Set.insert v1)) (prettyBinding0' context (HQ.unsafeFromVar v1) binding)
+      renderPrettyBinding <$> withBoundTerm v (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) =
-  renderPrettyBinding <$> prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding
+printLetrecBinding :: (MonadPretty v m) => AmbientContext -> [v] -> (v, Term3 v PrintAnnotation) -> m (Pretty SyntaxText)
+printLetrecBinding context vs (v, binding) =
+  renderPrettyBinding <$> withBoundTerms vs (prettyBinding0' context (HQ.unsafeFromVar (Var.reset v)) binding)
 
 prettyPattern ::
   forall v loc.
@@ -735,7 +726,7 @@ prettyPattern n c@AmbientContext {imports = im} p vs patt = case patt of
   Pattern.Unbound _ -> (fmt S.DelimiterChar $ l "_", vs)
   Pattern.Var _ ->
     case vs of
-      (v : tail_vs) -> (fmt S.Var $ l $ Var.nameStr v, tail_vs)
+      (v : tail_vs) -> (fmt S.Var $ l $ Var.nameStr (Var.reset v), tail_vs)
       _ -> error "prettyPattern: Expected at least one var"
   Pattern.Boolean _ b -> (fmt S.BooleanLiteral $ if b then l "true" else l "false", vs)
   Pattern.Int _ i -> (fmt S.NumericLiteral $ (if i >= 0 then l "+" else mempty) <> l (show i), vs)
@@ -764,7 +755,7 @@ prettyPattern n c@AmbientContext {imports = im} p vs patt = case patt of
     case vs of
       (v : tail_vs) ->
         let (printed, eventual_tail) = prettyPattern n c Prefix tail_vs pat
-         in (paren (p >= Prefix) (fmt S.Var (l $ Var.nameStr v) <> fmt S.DelimiterChar (l "@") <> printed), eventual_tail)
+         in (paren (p >= Prefix) (fmt S.Var (l $ Var.nameStr (Var.reset v)) <> fmt S.DelimiterChar (l "@") <> printed), eventual_tail)
       _ -> error "prettyPattern: Expected at least one var"
   Pattern.EffectPure _ pat ->
     let (printed, eventual_tail) = prettyPattern n c Bottom vs pat
@@ -826,28 +817,28 @@ arity1Branches bs = [([pat], guard, body) | MatchCase pat guard body <- bs]
 groupCases ::
   (Ord v) =>
   [MatchCase' () (Term3 v ann)] ->
-  [([Pattern ()], [v], [(Maybe (Term3 v ann), Term3 v ann)])]
-groupCases ms = go0 ms
+  [([Pattern ()], [v], [(Maybe (Term3 v ann), ([v], Term3 v ann))])]
+groupCases = \cases
+    [] -> []
+    ms@((p1, _, AbsN' vs1 _) : _) -> go (p1, vs1) [] ms
   where
-    go0 [] = []
-    go0 ms@((p1, _, AbsN' vs1 _) : _) = go2 (p1, vs1) [] ms
-    go2 (p0, vs0) acc [] = [(p0, vs0, reverse acc)]
-    go2 (p0, vs0) acc ms@((p1, g1, AbsN' vs body) : tl)
-      | p0 == p1 && vs == vs0 = go2 (p0, vs0) ((g1, body) : acc) tl
-      | otherwise = (p0, vs0, reverse acc) : go0 ms
+    go (p0, vs0) acc [] = [(p0, vs0, reverse acc)]
+    go (p0, vs0) acc ms@((p1, g1, AbsN' vs body) : tl)
+      | p0 == p1 && vs == vs0 = go (p0, vs0) ((g1, (vs, body)) : acc) tl
+      | otherwise = (p0, vs0, reverse acc) : groupCases ms
 
 printCase ::
+  forall m v.
   (MonadPretty v m) =>
   Imports ->
   DocLiteralContext ->
   [MatchCase' () (Term3 v PrintAnnotation)] ->
   m (Pretty SyntaxText)
-printCase im doc ms0 =
+printCase im doc ms =
   PP.orElse
     <$> (PP.lines . alignGrid True <$> grid)
     <*> (PP.lines . alignGrid False <$> grid)
   where
-    ms = groupCases ms0
     justify rows =
       zip (fmap fst . PP.align' $ fmap alignPatterns rows) $ fmap gbs rows
       where
@@ -876,19 +867,19 @@ printCase im doc ms0 =
                   )
                   justified
             justified = PP.leftJustify $ fmap (\(g, b) -> (g, (arrow, b))) gbs
-    grid = traverse go ms
-    patLhs env vs pats =
-      case pats of
-        [pat] -> PP.group (fst (prettyPattern env (ac Annotation Block im doc) Bottom vs pat))
-        pats -> PP.group
-          . PP.sep (PP.indentAfterNewline "  " $ "," <> PP.softbreak)
-          . (`evalState` vs)
-          . for pats
-          $ \pat -> do
-            vs <- State.get
-            let (p, rem) = prettyPattern env (ac Annotation Block im doc) Bottom vs pat
-            State.put rem
-            pure p
+    grid = traverse go (groupCases ms)
+    patLhs :: PrettyPrintEnv -> [v] -> [Pattern ()] -> Pretty SyntaxText
+    patLhs ppe vs = \cases
+      [pat] -> PP.group (fst (prettyPattern ppe (ac Annotation Block im doc) Bottom vs pat))
+      pats -> PP.group
+        . PP.sep (PP.indentAfterNewline "  " $ "," <> PP.softbreak)
+        . (`evalState` vs)
+        . for pats
+        $ \pat -> do
+          vs <- State.get
+          let (p, rem) = prettyPattern ppe (ac Annotation Block im doc) Bottom vs pat
+          State.put rem
+          pure p
     arrow = fmt S.ControlKeyword "->"
     -- If there's multiple guarded cases for this pattern, prints as:
     -- MyPattern x y
@@ -910,7 +901,7 @@ printCase im doc ms0 =
           -- like any other variable, ex: case Foo x y | x < y -> ...
           PP.spaceIfNeeded (fmt S.DelimiterChar "|")
             <$> pretty0 (ac Control Normal im doc) g
-        printBody = pretty0 (ac Annotation Block im doc)
+        printBody (vs, body) = withBoundTerms vs (pretty0 (ac Annotation Block im doc) body)
 
 -- A pretty term binding, split into the type signature (possibly empty) and the term.
 data PrettyBinding = PrettyBinding
@@ -989,7 +980,7 @@ prettyBinding0 ::
   m PrettyBinding
 prettyBinding0 ac v tm = do
   env <- ask
-  prettyBinding0' ac v (printAnnotate env.ppe tm)
+  local (set #freeTerms (ABT.freeVars tm)) (prettyBinding0' ac v (printAnnotate env.ppe tm))
 
 prettyBinding0' ::
   (MonadPretty v m) =>

unison-src/transcripts/idempotent/fix-5525.md

@@ -0,0 +1,106 @@
+The original bug report identified the mishandling of this simple case involving shadowing, in which we previously
+erroneously rendered "bar" with a leading dot.
+
+``` ucm
+scratch/main> builtins.merge lib.builtin
+
+  Done.
+```
+
+``` unison
+foo =
+  bar =
+    match 5 with
+      1 -> 2
+      bar -> bar
+  bar
+```
+
+``` 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`:
+    
+      foo : Nat
+```
+
+``` ucm
+scratch/main> add
+
+  ⍟ I've added these definitions:
+
+    foo : Nat
+
+scratch/main> view foo
+
+  foo : Nat
+  foo =
+    bar = match 5 with
+      1   -> 2
+      bar -> bar
+    bar
+```
+
+``` ucm
+scratch/main> project.delete scratch
+```
+
+There's a more complicated case that was also previously mishandled, though, which involves a top-level binding to which
+for which we do need to add a leading dot in order to refer to.
+
+``` ucm
+scratch/main> builtins.merge lib.builtin
+
+  Done.
+```
+
+``` unison
+foo =
+  bar =
+    match 5 with
+      1 -> 2
+      bar -> bar + .bar
+  bar
+
+bar = 17
+```
+
+``` 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 foo
+
+  foo : Nat
+  foo =
+    use Nat +
+    bar = match 5 with
+      1   -> 2
+      bar -> bar + .bar
+    bar
+```
+
+``` ucm
+scratch/main> project.delete scratch
+```