Merge pull request #1389 from unisonweb/fix/1388

Fix issue with `putSymbol` which resulted in extra numbers getting appended to the name on each round trip

parser-typechecker/src/Unison/Codebase/Serialization/V1.hs

@@ -395,7 +395,7 @@ getType getVar getA = getABT getVar getA go where
     _ -> unknownTag "getType" tag
 
 putSymbol :: MonadPut m => Symbol -> m ()
-putSymbol v@(Symbol id _) = putLength id *> putText (Var.name v)
+putSymbol (Symbol id typ) = putLength id *> putText (Var.rawName typ)
 
 getSymbol :: MonadGet m => m Symbol
 getSymbol = Symbol <$> getLength <*> (Var.User <$> getText)

parser-typechecker/tests/Unison/Test/ABT.hs

@@ -7,18 +7,38 @@ import EasyTest
 import Unison.ABT as ABT
 import Unison.Symbol (Symbol(..))
 import Unison.Var as Var
+import           Unison.Codebase.Serialization    ( getFromBytes, putBytes )
+import qualified Unison.Codebase.Serialization.V1 as V1
 
 test :: Test ()
 test = scope "abt" $ tests [
   scope "freshInBoth" $
     let
-      symbol i n = Symbol i (Var.User n)
-      var i n = ABT.var $ symbol i n
       t1 = var 1 "a"
       t2 = var 0 "a"
       fresh = ABT.freshInBoth t1 t2 $ symbol 0 "a"
     in tests
       [ scope "first"  $ expect (not $ Set.member fresh (ABT.freeVars t1))
       , scope "second" $ expect (not $ Set.member fresh (ABT.freeVars t2))
-      ]
+      ],
+  scope "rename" $ do
+    -- rename x to a in \a  -> [a, x] should yield
+    --                  \a1 -> [a1, a]
+    let t1 = ABT.abs (symbol 0 "a") (ABT.tm [var 0 "a", var 0 "x"])
+        t2 = ABT.rename (symbol 0 "x") (symbol 0 "a") t1
+        fvs = toList . ABT.freeVars $ t2
+    -- make sure the variable wasn't captured
+    expectEqual fvs [symbol 0 "a"]
+    -- make sure the resulting term is alpha equiv to \a1 -> [a1, a]
+    expectEqual t2 (ABT.abs (symbol 0 "b") (ABT.tm [var 0 "b", var 0 "a"])),
+
+  -- confirmation of fix for https://github.com/unisonweb/unison/issues/1388
+  -- where symbols with nonzero freshIds did not round trip
+  scope "putSymbol" $ let
+    v = Symbol 10 (User "hi")
+    v' = getFromBytes V1.getSymbol (putBytes V1.putSymbol v)
+    in expectEqual (Just v) v'
   ]
+  where
+    symbol i n = Symbol i (Var.User n)
+    var i n = ABT.var $ symbol i n

unison-core/src/Unison/ABT.hs

@@ -244,12 +244,25 @@ into' a abt = case abt of
 
 -- | renames `old` to `new` in the given term, ignoring subtrees that bind `old`
 rename :: (Foldable f, Functor f, Var v) => v -> v -> Term f v a -> Term f v a
-rename old new t0@(Term _ ann t) = case t of
-  Var v -> if v == old then annotatedVar ann new else t0
-  Cycle body -> cycle' ann (rename old new body)
-  Abs v body -> if v == old then abs' ann v body
-                else abs' ann v (rename old new body)
-  Tm v -> tm' ann (fmap (rename old new) v)
+rename old new t0@(Term fvs ann t) =
+  if Set.notMember old fvs then t0
+  else case t of
+    Var v -> if v == old then annotatedVar ann new else t0
+    Cycle body -> cycle' ann (rename old new body)
+    Abs v body ->
+      -- v shadows old, so skip this subtree
+      if v == old then abs' ann v body
+
+      -- the rename would capture new, freshen this Abs
+      -- to make that no longer true, then proceed with
+      -- renaming `old` to `new`
+      else if v == new then
+        let v' = freshIn (Set.fromList [new,old] <> freeVars body) v
+        in abs' ann v' (rename old new (rename v v' body))
+
+      -- nothing special, just rename inside body of Abs
+      else abs' ann v (rename old new body)
+    Tm v -> tm' ann (fmap (rename old new) v)
 
 changeVars :: (Foldable f, Functor f, Var v) => Map v v -> Term f v a -> Term f v a
 changeVars m t = case out t of

unison-core/src/Unison/Var.hs

@@ -37,22 +37,25 @@ named n = typed (User n)
 refNamed :: Var v => Reference -> v
 refNamed ref = named ("ℍ" <> R.toText ref)
 
+rawName :: Type -> Text
+rawName typ = case typ of
+  User n -> n
+  Inference Ability -> "𝕖"
+  Inference Input -> "𝕒"
+  Inference Output -> "𝕣"
+  Inference Other -> "𝕩"
+  Inference PatternPureE -> "𝕞"
+  Inference PatternPureV -> "𝕧"
+  Inference PatternBindE -> "𝕞"
+  Inference PatternBindV -> "𝕧"
+  Inference TypeConstructor -> "𝕗"
+  Inference TypeConstructorArg -> "𝕦"
+  MissingResult -> "_"
+  Blank -> "_"
+  UnnamedWatch k guid -> fromString k <> "." <> guid
+
 name :: Var v => v -> Text
-name v = case typeOf v of
-  User n -> n <> showid v
-  Inference Ability -> "𝕖" <> showid v
-  Inference Input -> "𝕒" <> showid v
-  Inference Output -> "𝕣" <> showid v
-  Inference Other -> "𝕩" <> showid v
-  Inference PatternPureE -> "𝕞" <> showid v
-  Inference PatternPureV -> "𝕧" <> showid v
-  Inference PatternBindE -> "𝕞" <> showid v
-  Inference PatternBindV -> "𝕧" <> showid v
-  Inference TypeConstructor -> "𝕗" <> showid v
-  Inference TypeConstructorArg -> "𝕦" <> showid v
-  MissingResult -> "_" <> showid v
-  Blank -> "_" <> showid v
-  UnnamedWatch k guid -> fromString k <> "." <> guid <> showid v
+name v = rawName (typeOf v) <> showid v
   where
   showid (freshId -> 0) = ""
   showid (freshId -> n) = pack (show n)