Fix some possible variable capture problems

- Unison.ABT.changeVars is not capture avoiding substitution, but was
  being used as such.
- Sequence pattern compilation needs to make up variables sometimes, and
  it may not have been avoiding all possible conflicts.

parser-typechecker/src/Unison/Runtime/ANF.hs

@@ -270,9 +270,9 @@ letFloater rec vbs e = do
       rn v = Map.findWithDefault v v shadowMap
       shvs = Set.fromList $ map (rn.fst) vbs
   modify (\(cvs, ctx, dcmp) -> (cvs<>shvs, ctx, dcmp))
-  fvbs <- traverse (\(v, b) -> (,) (rn v) <$> rec' (ABT.changeVars shadowMap b)) vbs
+  fvbs <- traverse (\(v, b) -> (,) (rn v) <$> rec' (ABT.renames shadowMap b)) vbs
   modify (\(vs,ctx,dcmp) -> (vs, ctx ++ fvbs, dcmp))
-  pure $ ABT.changeVars shadowMap e
+  pure $ ABT.renames shadowMap e
   where
   rec' b@(LamsNamed' vs bd) = lam' (ABT.annotation b) vs <$> rec bd
   rec' b = rec b
@@ -307,7 +307,7 @@ floater _   rec (Let1Named' v b e)
   | LamsNamed' vs bd <- b
   = Just $ rec bd
        >>= lamFloater (null $ ABT.freeVars b) b (Just v) a vs
-       >>= \lv -> rec $ ABT.changeVars (Map.singleton v lv) e
+       >>= \lv -> rec $ ABT.renames (Map.singleton v lv) e
   where a = ABT.annotation b
 
 floater top rec tm@(LamsNamed' vs bd)

parser-typechecker/src/Unison/Runtime/Pattern.hs

@@ -22,7 +22,7 @@ import Data.Set (Set, member)
 import qualified Data.Set as Set
 
 import Unison.ABT
-  (absChain', visitPure, pattern AbsN', changeVars)
+  (absChain', visitPure, pattern AbsN', renames)
 import Unison.Builtin.Decls (builtinDataDecls, builtinEffectDecls)
 import Unison.DataDeclaration (declFields)
 import Unison.Pattern
@@ -93,7 +93,14 @@ builtinDataSpec = Map.fromList decls
 -- should be matched against when decomposing a matrix.
 data PatternMatrix v
   = PM { _rows :: [PatternRow v] }
-  deriving Show
+  deriving (Show)
+
+usedVars :: Ord v => PatternMatrix v -> Set v
+usedVars (PM rs) = foldMap usedR rs
+  where
+  usedR (PR ps g b)
+    = foldMap usedP ps <> foldMap freeVars g <> freeVars b
+  usedP = foldMap Set.singleton
 
 -- Heuristics guide the pattern compilation. They inspect the
 -- pattern matrix and (may) choose a variable to split on next.
@@ -334,18 +341,19 @@ splitRowBuiltin _ r = [(P.Unbound (), [([], r)])]
 -- failure.
 splitRowSeq
   :: Var v
-  => v
+  => Set v
+  -> v
   -> SeqMatch
   -> PatternRow v
   -> [([P.Pattern v], PatternRow v)]
-splitRowSeq v m r@(PR (break ((==v).loc) -> (pl, sp : pr)) g b)
+splitRowSeq avoid0 v m r@(PR (break ((==v).loc) -> (pl, sp : pr)) g b)
   = case decomposeSeqP avoid m sp of
       Cover sps -> 
         [(sps, PR (pl ++ filter refutable sps ++ pr) g b)]
       Disjoint -> []
       Overlap -> [([], r)]
-  where avoid = maybe mempty freeVars g <> freeVars b
-splitRowSeq _ _ r = [([], r)]
+  where avoid = avoid0 <> maybe mempty freeVars g <> freeVars b
+splitRowSeq _ _ _ r = [([], r)]
 
 -- Renames the variables annotating the patterns in a row, for once a
 -- canonical choice has been made.
@@ -356,8 +364,8 @@ renameRow m (PR p0 g0 b0) = PR p g b
     | Just v <- Map.lookup k m = v
     | otherwise = k
   p = (fmap.fmap) access p0
-  g = changeVars m <$> g0
-  b = changeVars m b0
+  g = renames m <$> g0
+  b = renames m b0
 
 -- Chooses a common set of variables for use when decomposing
 -- patterns into multiple sub-patterns. It is too naive to simply use
@@ -422,10 +430,11 @@ matchPattern vrs = \case
 -- matricies for subsequent compilation.
 splitMatrixSeq
   :: Var v
-  => v
+  => Set v
+  -> v
   -> PatternMatrix v
   -> [(P.Pattern (), [(v,PType)], PatternMatrix v)]
-splitMatrixSeq v (PM rs)
+splitMatrixSeq avoid v (PM rs)
   = cases
   where
   ms = decideSeqPat $ take 1 . dropWhile ((/=v).loc) . matches =<< rs
@@ -433,7 +442,7 @@ splitMatrixSeq v (PM rs)
     | m `elem` [E,C,S] = vrs
     | otherwise = (fmap.fmap) (const $ PData Rf.listRef) vrs
   cases = ms <&> \m ->
-    let frs = rs >>= splitRowSeq v m
+    let frs = rs >>= splitRowSeq avoid v m
         (vrs, pm) = buildMatrix frs
     in (matchPattern vrs m, hint m vrs, pm)
 
@@ -572,7 +581,7 @@ compile spec ctx m@(PM (r:rs))
   , rf == Rf.listRef
   = match () (var () v)
       $ buildCaseBuiltin spec ctx
-     <$> splitMatrixSeq v m
+     <$> splitMatrixSeq (Map.keysSet ctx <> usedVars m) v m
   | PData rf <- ty
   , rf `member` builtinCase
   = match () (var () v)
@@ -651,8 +660,8 @@ mkRow sv (MatchCase (normalizeSeqP -> p0) g0 (AbsN' vs b))
   = state $ \w -> case runState (prepareAs p0 sv) (w, vs, mempty) of
       (p, (w, [], rn)) -> (,w)
         $ PR (filter refutable [p])
-             (changeVars rn <$> g)
-             (changeVars rn b)
+             (renames rn <$> g)
+             (renames rn b)
       _ -> error "mkRow: not all variables used"
   where
   g = case g0 of

unison-core/src/Unison/ABT.hs

@@ -269,6 +269,35 @@ rename old new t0@(Term fvs ann t) =
       else abs' ann v (rename old new body)
     Tm v -> tm' ann (fmap (rename old new) v)
 
+renames
+  :: (Foldable f, Functor f, Var v)
+  => Map v v -> Term f v a -> Term f v a
+renames rn0 t0@(Term fvs ann t)
+  | Map.null rn = t0
+  | Var v <- t
+  , Just u <- Map.lookup v rn
+  = annotatedVar ann u
+  | Cycle body <- t
+  = cycle' ann (renames rn body)
+  | Abs v body <- t
+  , (u, rn) <- mangle (freeVars body) v rn
+  , not $ Map.null rn
+  = abs' ann u (renames rn body)
+  | Tm body <- t
+  = tm' ann (renames rn <$> body)
+  | otherwise = t0
+  where
+  rn = Map.restrictKeys rn0 fvs
+  mangle fvs v m
+    | any (==v) vs
+    , u <- freshIn (fvs <> Set.fromList vs) v
+    = (u, Map.insert v u m)
+    | otherwise = (v, Map.delete v m)
+    where
+    vs = toList m
+
+-- Note: this does not do capture-avoiding renaming. It actually
+-- renames bound variables using the map as well.
 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
   Abs v body -> case Map.lookup v m of