diff --git a/primer-benchmark/src/Benchmarks.hs b/primer-benchmark/src/Benchmarks.hs
index 200535e7b..0a3c6d7b6 100644
--- a/primer-benchmark/src/Benchmarks.hs
+++ b/primer-benchmark/src/Benchmarks.hs
@@ -23,7 +23,7 @@ import Primer.App.Utils (forgetProgTypecache)
 import Primer.Eval (
   NormalOrderOptions (UnderBinders),
   RunRedexOptions (RunRedexOptions, pushAndElide),
-  ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets),
+  ViewRedexOptions (ViewRedexOptions, aggressiveElision, avoidShadowing, groupedLets),
  )
 import Primer.EvalFull (
   Dir (Syn),
@@ -104,7 +104,7 @@ benchmarks =
   ]
   where
     evalOptionsN = UnderBinders
-    evalOptionsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+    evalOptionsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
     evalOptionsR = RunRedexOptions{pushAndElide = True}
     evalTestMPureLogs e maxEvals =
       evalTestM (maxID e)
diff --git a/primer/gen/Primer/Gen/Core/Raw.hs b/primer/gen/Primer/Gen/Core/Raw.hs
index 3137cc075..580a7b2c4 100644
--- a/primer/gen/Primer/Gen/Core/Raw.hs
+++ b/primer/gen/Primer/Gen/Core/Raw.hs
@@ -141,13 +141,16 @@ genLetrec = Letrec <$> genMeta <*> genLVarName <*> genExpr <*> genType <*> genEx
 genCase :: ExprGen Expr
 genCase = Case <$> genMeta <*> genExpr <*> Gen.list (Range.linear 0 5) genBranch <*> Gen.choice [pure CaseExhaustive, CaseFallback <$> genExpr]
   where
-    genBranch = CaseBranch <$> genScrut <*> Gen.list (Range.linear 0 5) genBind <*> genExpr
+    genBranch = CaseBranch <$> genScrut <*> genBinds (Range.linear 0 5) <*> genExpr
     genScrut =
       Gen.choice
         [ PatCon <$> genValConName
         , PatPrim <$> genPrimCon
         ]
-    genBind = Bind <$> genMeta <*> genLVarName
+    genBinds r = do
+      ns0 <- Gen.set r genLVarName
+      ns <- Gen.shuffle $ toList ns0
+      traverse (\n -> Bind <$> genMeta <*> pure n) ns
 
 genPrim :: ExprGen Expr
 genPrim = PrimCon <$> genMeta <*> genPrimCon
diff --git a/primer/gen/Primer/Gen/Core/Typed.hs b/primer/gen/Primer/Gen/Core/Typed.hs
index 57e75b18c..55088c782 100644
--- a/primer/gen/Primer/Gen/Core/Typed.hs
+++ b/primer/gen/Primer/Gen/Core/Typed.hs
@@ -37,6 +37,7 @@ import Control.Monad.Morph (hoist)
 import Control.Monad.Reader (mapReaderT)
 import Data.List.Extra (nubSortOn)
 import Data.Map qualified as M
+import Data.Set qualified as S
 import Hedgehog (
   GenT,
   MonadGen,
@@ -470,9 +471,11 @@ genChk ty = do
                         ]
                     fmap (Just . (,fb)) . for vcs $ \(c, params) -> do
                       ns <- for params $ \nt -> (,nt) <$> genLVarNameAvoiding [ty, nt]
+                      unless (distinct $ map fst ns) Gen.discard
                       let binds = map (Bind () . fst) ns
                       CaseBranch (PatCon c) binds <$> local (extendLocalCxts ns) (genChk ty)
             pure $ Case () e brs fb
+    distinct xs = length xs == S.size (S.fromList xs)
     casePrim :: WT (Maybe (GenT WT ExprG))
     casePrim = do
       primGens <- genPrimCon
diff --git a/primer/primer.cabal b/primer/primer.cabal
index 06dd2fddd..5139c42ea 100644
--- a/primer/primer.cabal
+++ b/primer/primer.cabal
@@ -233,6 +233,7 @@ test-suite primer-test
     Tests.Questions
     Tests.Refine
     Tests.Serialization
+    Tests.Shadowing
     Tests.Subst
     Tests.Transform
     Tests.Typecheck
diff --git a/primer/src/Primer/App.hs b/primer/src/Primer/App.hs
index 136cbe579..2862583fb 100644
--- a/primer/src/Primer/App.hs
+++ b/primer/src/Primer/App.hs
@@ -195,6 +195,7 @@ import Primer.Def (
   defAST,
  )
 import Primer.Def.Utils (globalInUse, typeInUse)
+import Primer.Eval (AvoidShadowing (AvoidShadowing))
 import Primer.Eval qualified as Eval
 import Primer.Eval.Detail (EvalDetail)
 import Primer.Eval.Redex (EvalLog, RunRedexOptions (RunRedexOptions, pushAndElide), ViewRedexOptions (ViewRedexOptions, groupedLets))
@@ -596,11 +597,12 @@ handleEvalRequest ::
 handleEvalRequest req = do
   app <- ask
   let prog = appProg app
-  result <- runFreshM app $ Eval.step (allTypes prog) (allDefs prog) (evalReqExpr req) Syn (evalReqRedex req)
+  let as = AvoidShadowing
+  result <- runFreshM app $ Eval.step as (allTypes prog) (allDefs prog) (evalReqExpr req) Syn (evalReqRedex req)
   case result of
     Left err -> throwError' err
     Right (expr, detail) -> do
-      redexes <- Eval.redexes (allTypes prog) (allDefs prog) Syn expr
+      redexes <- Eval.redexes as (allTypes prog) (allDefs prog) Syn expr
       pure
         EvalResp
           { evalRespExpr = expr
@@ -616,7 +618,7 @@ handleEvalFullRequest ::
 handleEvalFullRequest (EvalFullReq{evalFullReqExpr, evalFullCxtDir, evalFullMaxSteps, evalFullOptions}) = do
   app <- ask
   let prog = appProg app
-  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
   let optsR = RunRedexOptions{pushAndElide = True}
   result <- runFreshM app $ evalFull evalFullOptions optsV optsR (allTypes prog) (allDefs prog) evalFullMaxSteps evalFullCxtDir evalFullReqExpr
   pure $ case result of
diff --git a/primer/src/Primer/Core/Transform.hs b/primer/src/Primer/Core/Transform.hs
index de149df0d..f575b11b0 100644
--- a/primer/src/Primer/Core/Transform.hs
+++ b/primer/src/Primer/Core/Transform.hs
@@ -4,6 +4,7 @@ module Primer.Core.Transform (
   renameTyVar,
   renameTyVarExpr,
   unfoldApp,
+  unfoldAPP,
   unfoldTApp,
   decomposeTAppCon,
   foldTApp,
@@ -214,6 +215,13 @@ unfoldApp = second reverse . go
     go (App _ f x) = let (g, args) = go f in (g, x : args)
     go e = (e, [])
 
+-- | Unfold a nested term-level type application into the application head and a list of arguments.
+unfoldAPP :: Expr' a b c -> (Expr' a b c, [Type' b c])
+unfoldAPP = second reverse . go
+  where
+    go (APP _ f x) = let (g, args) = go f in (g, x : args)
+    go e = (e, [])
+
 -- | Unfold a nested type-level application into the application head and a list of arguments.
 unfoldTApp :: Type' a b -> (Type' a b, [Type' a b])
 unfoldTApp = second reverse . go
diff --git a/primer/src/Primer/Eval.hs b/primer/src/Primer/Eval.hs
index cc8612db5..994aef6db 100644
--- a/primer/src/Primer/Eval.hs
+++ b/primer/src/Primer/Eval.hs
@@ -5,6 +5,7 @@ module Primer.Eval (
   -- The public API of this module
   step,
   redexes,
+  AvoidShadowing (..),
   RunRedexOptions (..),
   ViewRedexOptions (..),
   NormalOrderOptions (..),
@@ -68,7 +69,7 @@ import Primer.Eval.Redex (
   EvalLog (..),
   MonadEval,
   RunRedexOptions (RunRedexOptions, pushAndElide),
-  ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets),
+  ViewRedexOptions (ViewRedexOptions, aggressiveElision, avoidShadowing, groupedLets),
   lookupEnclosingLet,
   runRedex,
   runRedexTy,
@@ -90,21 +91,22 @@ import Primer.Zipper (
 -- Returns the new expression and its redexes.
 step ::
   MonadEval l m =>
+  AvoidShadowing ->
   TypeDefMap ->
   DefMap ->
   Expr ->
   Dir ->
   ID ->
   m (Either EvalError (Expr, EvalDetail))
-step tydefs globals expr d i = runExceptT $ do
+step as tydefs globals expr d i = runExceptT $ do
   (cxt, nodeZ) <- maybe (throwError (NodeNotFound i)) pure (findNodeByID i d expr)
   case nodeZ of
     Left (d', z) -> do
-      (node', detail) <- tryReduceExpr tydefs globals cxt d' (target z)
+      (node', detail) <- tryReduceExpr as tydefs globals cxt d' (target z)
       let expr' = unfocusExpr $ replace node' z
       pure (expr', detail)
     Right z -> do
-      (node', detail) <- tryReduceType globals cxt (target z)
+      (node', detail) <- tryReduceType as globals cxt (target z)
       let expr' = unfocusExpr $ unfocusType $ replace node' z
       pure (expr', detail)
 
@@ -124,13 +126,17 @@ findNodeByID i =
 
 -- We hardcode a permissive set of options for the interactive eval
 -- (i.e. these see more redexes)
-evalOpts :: ViewRedexOptions
-evalOpts =
+evalOpts :: AvoidShadowing -> ViewRedexOptions
+evalOpts as =
   ViewRedexOptions
     { groupedLets = True
     , aggressiveElision = True
+    , avoidShadowing = case as of AvoidShadowing -> True; NoAvoidShadowing -> False
     }
 
+data AvoidShadowing = AvoidShadowing | NoAvoidShadowing
+  deriving stock (Show, Bounded, Enum)
+
 -- | Return the IDs of nodes which are reducible.
 -- We assume that the expression is well scoped. There are no
 -- guarantees about whether we will claim that an ill-sorted variable
@@ -143,18 +149,19 @@ evalOpts =
 redexes ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  AvoidShadowing ->
   TypeDefMap ->
   DefMap ->
   Dir ->
   Expr ->
   m [ID]
-redexes tydefs globals =
+redexes as tydefs globals =
   (ListT.toList .)
     . foldMapExpr
       UnderBinders
       FMExpr
-        { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex evalOpts tydefs globals d (target ez))
-        , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType evalOpts (target tz))
+        { expr = \ez d -> liftMaybeT . runReaderT (getID ez <$ viewRedex (evalOpts as) tydefs globals d (target ez))
+        , ty = \tz -> runReader (whenJust (getID tz) <$> viewRedexType (evalOpts as) (target tz))
         }
   where
     liftMaybeT :: Monad m' => MaybeT m' a -> ListT m' a
@@ -179,14 +186,15 @@ reductionOpts =
 tryReduceExpr ::
   forall l m.
   (MonadEval l m, MonadError EvalError m) =>
+  AvoidShadowing ->
   TypeDefMap ->
   DefMap ->
   Cxt ->
   Dir ->
   Expr ->
   m (Expr, EvalDetail)
-tryReduceExpr tydefs globals cxt dir expr =
-  runMaybeT (flip runReaderT cxt $ viewRedex evalOpts tydefs globals dir expr) >>= \case
+tryReduceExpr as tydefs globals cxt dir expr =
+  runMaybeT (flip runReaderT cxt $ viewRedex (evalOpts as) tydefs globals dir expr) >>= \case
     Just r -> runRedex reductionOpts r
     _ -> throwError NotRedex
 
@@ -194,11 +202,12 @@ tryReduceType ::
   ( MonadEval l m
   , MonadError EvalError m
   ) =>
+  AvoidShadowing ->
   DefMap ->
   Cxt ->
   Type ->
   m (Type, EvalDetail)
-tryReduceType _globals cxt =
-  flip runReader cxt . viewRedexType evalOpts <&> \case
+tryReduceType as _globals cxt =
+  flip runReader cxt . viewRedexType (evalOpts as) <&> \case
     Just r -> runRedexTy reductionOpts r
     _ -> throwError NotRedex
diff --git a/primer/src/Primer/Eval/Redex.hs b/primer/src/Primer/Eval/Redex.hs
index 71bcf6738..feafc5173 100644
--- a/primer/src/Primer/Eval/Redex.hs
+++ b/primer/src/Primer/Eval/Redex.hs
@@ -43,6 +43,7 @@ import Optics (
   getting,
   ifiltered,
   isnd,
+  preview,
   summing,
   to,
   traverseOf,
@@ -165,6 +166,7 @@ import Primer.Typecheck.Utils (
 import Primer.Zipper (
   LetBinding,
   LetBinding' (LetBind, LetTyBind, LetrecBind),
+  bindersBelow,
   bindersBelowTy,
   focus,
   getBoundHereDn,
@@ -189,6 +191,9 @@ data ViewRedexOptions = ViewRedexOptions
   -- down) (@False@). E.g. in @let x=e in C s t@ (where @s@ and @t@
   -- do not refer to @x@) whether we reduce to @C s t@ or
   -- @C (let x = e in s) (let x = e in t)@.
+  , avoidShadowing :: Bool
+  -- ^ Whether to introduce extra renamings to avoid shadowing
+  -- (note that we will always rename to avoid capture where necessary).
   }
 
 newtype RunRedexOptions = RunRedexOptions
@@ -253,7 +258,13 @@ data Redex
       , varID :: ID
       -- ^ Where was the occurrence (used for details)
       }
-  | -- letrec x = t : T in x  ~>  letrec x = t : T in t : T
+  | -- letrec x = t : T in x  ~>  (letrec x = t : T in t) : T
+    -- Note that a different choice would be reducing to a term with t:T
+    -- inside the letrec. We do not do this for two reasons: firstly
+    -- (since the recursive binder does not scope over the type) this
+    -- would immediately reduce in one step to the reduct we actually
+    -- emit; secondly this intermediate step can introduce shadowing,
+    -- for example in letrec x = x : ∀x.x in x.
     InlineLetrec
       { var :: LVarName
       -- ^ What variable are we inlining
@@ -519,6 +530,15 @@ _freeVarsLetBinding =
 _freeVarsLetTypeBinding :: Fold LetTypeBinding TyVarName
 _freeVarsLetTypeBinding = _LetTypeBind % _2 % getting _freeVarsTy % _2
 
+boundVarsLetBinding :: LetBinding -> Set Name
+boundVarsLetBinding = \case
+  LetBind _ e -> bindersBelow $ focus e
+  LetrecBind _ e t -> bindersBelow (focus e) <> S.map unLocalName (bindersBelowTy (focus t))
+  LetTyBind l -> S.map unLocalName $ boundVarsLetBindingTy l
+
+boundVarsLetBindingTy :: LetTypeBinding -> Set TyVarName
+boundVarsLetBindingTy (LetTypeBind _ t) = bindersBelowTy (focus t)
+
 data Dir = Syn | Chk
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON Dir
@@ -526,10 +546,11 @@ data Dir = Syn | Chk
 viewCaseRedex ::
   forall l m.
   (MonadLog (WithSeverity l) m, ConvertLogMessage EvalLog l) =>
+  ViewRedexOptions ->
   TypeDefMap ->
   Expr ->
   MaybeT m Redex
-viewCaseRedex tydefs = \case
+viewCaseRedex opts tydefs = \case
   orig@(Case _ scrut [] (CaseFallback rhs)) -> do
     -- If we have @case e of _ -> t@, then this reduces to @t@ without inspecting @e@
     -- i.e. a @case@ which does not actually discriminate is lazy
@@ -617,7 +638,7 @@ viewCaseRedex tydefs = \case
        the last doesn't need any renaming.)
     -}
     renameBindings meta scrutinee branches fallbackBranch patterns orig =
-      let avoid = freeVars scrutinee
+      let avoid = freeVars scrutinee <> mwhen opts.avoidShadowing (bindersBelow $ focus scrutinee)
           binders = maybe mempty (S.fromList . map (unLocalName . bindName)) patterns
        in hoistMaybe
             $ if S.disjoint avoid binders
@@ -689,7 +710,8 @@ viewRedex opts tydefs globals dir = \case
     , null letBindings
     , n <- letBindingName $ snd letBinding1
     , not opts.aggressiveElision || n `S.member` freeVars expr'
-    , S.disjoint (getBoundHereDn expr') (setOf (_2 % (_freeVarsLetBinding `summing` to letBindingName)) letBinding1) ->
+    , S.disjoint (getBoundHereDn expr') (setOf (_2 % (_freeVarsLetBinding `summing` to letBindingName)) letBinding1)
+    , not opts.avoidShadowing || S.disjoint (getBoundHereDn expr') (boundVarsLetBinding . snd $ letBinding1) ->
         pure
           $ PushLet
             { bindings = pure $ first getID letBinding1
@@ -700,7 +722,8 @@ viewRedex opts tydefs globals dir = \case
     , not $ isLeaf body
     , (_, unused) <- partitionLets (letBinding1 : letBindings) body
     , not opts.aggressiveElision || null unused
-    , S.disjoint (getBoundHereDn body) (setOf (folded % _2 % (_freeVarsLetBinding `summing` to letBindingName)) $ letBinding1 : letBindings) ->
+    , S.disjoint (getBoundHereDn body) (setOf (folded % _2 % (_freeVarsLetBinding `summing` to letBindingName)) $ letBinding1 : letBindings)
+    , not opts.avoidShadowing || S.disjoint (getBoundHereDn body) (foldMap' (boundVarsLetBinding . snd) $ letBinding1 : letBindings) ->
         pure
           $ PushLet
             { bindings = first getID <$> letBinding1 :| letBindings
@@ -731,12 +754,12 @@ viewRedex opts tydefs globals dir = \case
             , orig
             }
   l@(Lam meta var body) -> do
-    avoid <- cxtToAvoid
+    avoid <- liftA2 (<>) cxtToAvoid $ when' opts.avoidShadowing cxtToAvoidShadow
     if unLocalName var `S.member` avoid
       then pure $ RenameBindingsLam{var, meta, body, avoid, orig = l}
       else mzero
   l@(LAM meta v body) -> do
-    avoid <- cxtToAvoid
+    avoid <- liftA2 (<>) cxtToAvoid $ when' opts.avoidShadowing cxtToAvoidShadow
     if unLocalName v `S.member` avoid
       then pure $ RenameBindingsLAM{tyvar = v, meta, body, avoid, orig = l}
       else mzero
@@ -772,19 +795,23 @@ viewRedex opts tydefs globals dir = \case
         }
   APP{} -> mzero
   e@(Case meta scrutinee branches fallbackBranch) -> do
-    avoid <- cxtToAvoid
+    avoid <- liftA2 (<>) cxtToAvoid $ when' opts.avoidShadowing cxtToAvoidShadow
     -- TODO: we arbitrarily decide that renaming takes priority over reducing the case
     -- This is good for evalfull, but bad for interactive use.
     -- Maybe we want to offer both. See
     -- https://github.com/hackworthltd/primer/issues/734
     if getBoundHereDn e `S.disjoint` avoid
-      then lift $ viewCaseRedex tydefs e
+      then lift $ viewCaseRedex opts tydefs e
       else pure $ RenameBindingsCase{meta, scrutinee, branches, fallbackBranch, avoid, orig = e}
   orig@(Ann _ expr ty) | Chk <- dir, concreteTy ty -> pure $ Upsilon{expr, ann = ty, orig}
   _ -> mzero
   where
     isLeaf = null . children
 
+-- | As 'when', but with a monoidal return
+when' :: (Applicative f, Monoid a) => Bool -> f a -> f a
+when' b m = if b then m else pure mempty
+
 -- Decompose @let a = s in let b0 = t0 in ... let bn = tn in e@
 -- into @(LetBind a s, let b0=t0 in ... e, [LetBind b0 t0, ..., LetBind bn tn], e)@
 -- I.e. a combination of two views: first let & all lets.
@@ -856,7 +883,8 @@ viewRedexType opts = \case
     , not $ isLeaf ty'
     , null letBindings
     , not opts.aggressiveElision || letTypeBindingName' (snd letBinding1) `S.member` freeVarsTy ty'
-    , S.disjoint (getBoundHereDnTy ty') (setOf (_2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) letBinding1) ->
+    , S.disjoint (getBoundHereDnTy ty') (setOf (_2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) letBinding1)
+    , not opts.avoidShadowing || S.disjoint (getBoundHereDnTy ty') (boundVarsLetBindingTy . snd $ letBinding1) ->
         purer
           $ PushLetType
             { bindings = pure $ first getID letBinding1
@@ -867,7 +895,8 @@ viewRedexType opts = \case
     , not $ isLeaf body
     , (_, unused) <- partitionLetsTy (letBinding1 : letBindings) body
     , not opts.aggressiveElision || null unused
-    , S.disjoint (getBoundHereDnTy body) (setOf (folded % _2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) (letBinding1 : letBindings)) ->
+    , S.disjoint (getBoundHereDnTy body) (setOf (folded % _2 % (_freeVarsLetTypeBinding `summing` to letTypeBindingName')) (letBinding1 : letBindings))
+    , not opts.avoidShadowing || S.disjoint (getBoundHereDnTy body) (foldMap' (boundVarsLetBindingTy . snd) $ letBinding1 : letBindings) ->
         purer
           $ PushLetType
             { bindings = first getID <$> letBinding1 :| letBindings
@@ -895,7 +924,7 @@ viewRedexType opts = \case
             , orig
             }
   orig@(TForall meta origBinder kind body) -> do
-    avoid <- cxtToAvoidTy
+    avoid <- liftA2 (<>) cxtToAvoidTy $ when' opts.avoidShadowing cxtToAvoidTyShadow
     pure
       $ if origBinder `S.member` avoid
         then
@@ -931,6 +960,21 @@ cxtToAvoidTy = do
   Cxt cxt <- ask
   pure $ foldMap' (setOf (_LetTyBind % _LetTypeBind % (_1 `summing` _2 % getting _freeVarsTy % _2))) cxt
 
+-- We may want to push some let bindings (the Cxt) under a
+-- binder; what variable names must the binder avoid for this to
+-- not cause shadowing?
+-- (NB: this does not include 'cxtToAvoid' which must additionally
+-- be avoided else capture may occur)
+cxtToAvoidShadow :: MonadReader Cxt m => m (S.Set Name)
+cxtToAvoidShadow = do
+  Cxt cxt <- ask
+  pure $ foldMap' boundVarsLetBinding cxt
+
+cxtToAvoidTyShadow :: MonadReader Cxt m => m (S.Set TyVarName)
+cxtToAvoidTyShadow = do
+  Cxt cxt <- ask
+  pure $ foldMap' (maybe mempty boundVarsLetBindingTy . preview _LetTyBind) cxt
+
 -- TODO: deal with metadata. https://github.com/hackworthltd/primer/issues/6
 runRedex :: forall l m. MonadEval l m => RunRedexOptions -> Redex -> m (Expr, EvalDetail)
 runRedex opts = \case
@@ -950,7 +994,7 @@ runRedex opts = \case
             }
     pure (expr, LocalVarInline details)
   InlineLetrec{var, expr, ty, letID, varID} -> do
-    expr' <- letrec var (pure expr) (pure ty) $ ann (regenerateExprIDs expr) (regenerateTypeIDs ty)
+    expr' <- ann (letrec var (pure expr) (pure ty) $ regenerateExprIDs expr) (regenerateTypeIDs ty)
     let details =
           LocalVarInlineDetail
             { letID
diff --git a/primer/src/Primer/Typecheck.hs b/primer/src/Primer/Typecheck.hs
index 896b5012f..45f92553f 100644
--- a/primer/src/Primer/Typecheck.hs
+++ b/primer/src/Primer/Typecheck.hs
@@ -919,6 +919,7 @@ checkBranch t (vc, args) (CaseBranch nb patterns rhs) =
     -- We check an invariant due to paranoia
     assertCorrectCon
     sh <- asks smartHoles
+    unless (distinct $ bindName <$> patterns) $ throwError' $ DuplicateBinders $ bindName <$> patterns
     (fixedPats, fixedRHS) <- case (length args == length patterns, sh) of
       (False, NoSmartHoles) -> throwError' CaseBranchWrongNumberPatterns
       -- if the branch is nonsense, replace it with a sensible pattern and an empty hole
diff --git a/primer/src/Primer/Typecheck/TypeError.hs b/primer/src/Primer/Typecheck/TypeError.hs
index 70e313ae1..e2dc30d03 100644
--- a/primer/src/Primer/Typecheck/TypeError.hs
+++ b/primer/src/Primer/Typecheck/TypeError.hs
@@ -3,7 +3,7 @@ module Primer.Typecheck.TypeError (TypeError (..)) where
 import Foreword
 
 import Primer.Core (Expr, Pattern)
-import Primer.Core.Meta (TmVarRef, TyConName, ValConName)
+import Primer.Core.Meta (LVarName, TmVarRef, TyConName, ValConName)
 import Primer.Core.Type (Type')
 import Primer.JSON (CustomJSON (..), FromJSON, PrimerJSON, ToJSON)
 import Primer.Name (Name)
@@ -35,6 +35,9 @@ data TypeError
   | -- | Either wrong number, wrong constructors or wrong order. The fields are @name of the ADT@, @branches given@, @wildcard/fallback branch given@
     WrongCaseBranches TyConName [Pattern] Bool
   | CaseBranchWrongNumberPatterns
+  | -- | One AST node binds the same name twice
+    -- (currently this can only happen in a case branch)
+    DuplicateBinders [LVarName]
   | KindError KindError
   deriving stock (Eq, Show, Read, Generic)
   deriving (FromJSON, ToJSON) via PrimerJSON TypeError
diff --git a/primer/src/Primer/Zipper.hs b/primer/src/Primer/Zipper.hs
index 9357cf606..2d685e614 100644
--- a/primer/src/Primer/Zipper.hs
+++ b/primer/src/Primer/Zipper.hs
@@ -67,6 +67,7 @@ module Primer.Zipper (
   SomeNode (..),
   findNodeWithParent,
   findTypeOrKind,
+  FoldAbove' (FA),
 ) where
 
 import Foreword
@@ -428,7 +429,9 @@ getBoundHereUp e = getBoundHere (current e) (Just $ prior e)
 
 -- Get the names bound within the focussed subtree
 bindersBelow :: ExprZ -> S.Set Name
-bindersBelow = foldBelow getBoundHereDn
+bindersBelow = foldBelow $ \e ->
+  getBoundHereDn e
+    <> maybe mempty (S.map unLocalName . bindersBelowTy . focusOnlyType) (focusType $ focus e)
 
 -- Get all names bound by this layer of an expression, for any child.
 -- E.g. for a "match" we get all vars bound by each branch.
diff --git a/primer/test/Tests/Action/Available.hs b/primer/test/Tests/Action/Available.hs
index 278915a0a..e78703b9d 100644
--- a/primer/test/Tests/Action/Available.hs
+++ b/primer/test/Tests/Action/Available.hs
@@ -7,7 +7,6 @@ module Tests.Action.Available where
 import Foreword
 
 import Control.Monad.Log (WithSeverity)
-import Data.Bitraversable (bitraverse)
 import Data.ByteString.Lazy.Char8 qualified as BS
 import Data.List.Extra (enumerate, partition)
 import Data.Map qualified as M
@@ -17,7 +16,6 @@ import Data.Text.Lazy qualified as TL
 import GHC.Err (error)
 import Hedgehog (
   GenT,
-  LabelName,
   PropertyT,
   annotate,
   annotateShow,
@@ -34,6 +32,7 @@ import Optics (ix, toListOf, (%), (.~), (^..), _head)
 import Primer.Action (
   ActionError (CaseBindsClash, CaseBranchAlreadyExists, NameCapture),
   Movement (Child1, Child2),
+  ProgAction,
   enterType,
   move,
   moveExpr,
@@ -91,9 +90,12 @@ import Primer.Core (
   HasID (_id),
   ID,
   Kind' (..),
+  KindMeta,
   ModuleName (ModuleName, unModuleName),
   Pattern (PatPrim),
+  TyConName,
   Type,
+  TypeMeta,
   getID,
   mkSimpleModuleName,
   moduleNamePretty,
@@ -154,7 +156,13 @@ import Primer.Test.App (
  )
 import Primer.Test.TestM (evalTestM)
 import Primer.Test.Util (clearMeta, clearTypeMeta, testNoSevereLogs)
-import Primer.TypeDef (ASTTypeDef (astTypeDefConstructors), TypeDef (TypeDefAST, TypeDefPrim), ValCon (..), astTypeDefParameters, forgetTypeDefMetadata, typeDefAST)
+import Primer.TypeDef (
+  ASTTypeDef (astTypeDefConstructors),
+  ValCon (..),
+  astTypeDefParameters,
+  forgetTypeDefMetadata,
+  typeDefAST,
+ )
 import Primer.Typecheck (
   CheckEverythingRequest (CheckEverything, toCheck, trusted),
   SmartHoles (NoSmartHoles, SmartHoles),
@@ -274,16 +282,6 @@ unit_def_in_use =
               @?= [Available.Input Available.RenameDef, Available.NoInput Available.DuplicateDef]
         )
 
--- | A helper type for 'tasty_available_actions_actions',
--- describing where a particular option came from.
-data Provenance
-  = -- | This option was offered by the 'Available.options' API
-    Offered
-  | -- | This option is free-form entry. For example, this simulates
-    -- renaming a definition to a hand-entered name.
-    StudentProvided
-  deriving stock (Show)
-
 tasty_available_actions_accepted :: Property
 tasty_available_actions_accepted = withTests 500
   $ withDiscards 2000
@@ -294,173 +292,18 @@ tasty_available_actions_accepted = withTests 500
     -- We only test SmartHoles mode (which is the only supported student-facing
     -- mode - NoSmartHoles is only used for internal sanity testing etc)
     a <- forAllT $ genApp SmartHoles cxt
-    let allTypes = progAllTypeDefsMeta $ appProg a
-        allTypes' = forgetTypeDefMetadata . snd <$> allTypes
-    let allDefs = progAllDefs $ appProg a
-        allDefs' = snd <$> allDefs
-    let isMutable = \case
-          Editable -> True
-          NonEditable -> False
-    let genDef :: Map name (Editable, def) -> GenT WT (Maybe (LabelName, (Editable, (name, def))))
-        genDef m =
-          second (\(n, (e, t)) -> (e, (n, t)))
-            <<$>> case partition (isMutable . fst . snd) $ Map.toList m of
-              ([], []) -> pure Nothing
-              (mut, []) -> Just . ("all mut",) <$> Gen.element mut
-              ([], immut) -> Just . ("all immut",) <$> Gen.element immut
-              (mut, immut) -> Just . ("mixed mut/immut",) <$> Gen.frequency [(9, Gen.element mut), (1, Gen.element immut)]
-    (defMut, typeOrTermDef) <-
-      maybe discard (\(t, x) -> label t >> pure x)
-        =<< forAllT
-          ( Gen.choice
-              [ second (second Left) <<$>> genDef allTypes
-              , second (second Right) <<$>> genDef allDefs
-              ]
-          )
-    collect defMut
-    case typeOrTermDef of
-      Left (_, t) ->
-        label "type" >> case t of
-          TypeDefPrim{} -> label "Prim"
-          TypeDefAST{} -> label "AST"
-      Right (_, t) ->
-        label "term" >> case t of
-          DefPrim{} -> label "Prim"
-          DefAST{} -> label "AST"
-    (loc, acts) <- case typeOrTermDef of
-      Left (defName, def) ->
-        (fmap snd . forAllWithT fst) case typeDefAST def of
-          Nothing -> Gen.discard
-          Just def' ->
-            let typeDefSel = SelectionTypeDef . TypeDefSelection defName
-                forTypeDef = ("forTypeDef", (typeDefSel Nothing, Available.forTypeDef l defMut allTypes' allDefs' defName def'))
-             in Gen.frequency
-                  [ (1, pure forTypeDef)
-                  ,
-                    ( 2
-                    , case astTypeDefParameters def' of
-                        [] -> pure forTypeDef
-                        ps -> do
-                          (p, k) <- Gen.element ps
-                          let typeDefParamNodeSel = typeDefSel . Just . TypeDefParamNodeSelection . TypeDefParamSelection p
-                          Gen.frequency
-                            [
-                              ( 1
-                              , pure
-                                  ( "forTypeDefParamNode"
-                                  ,
-                                    ( typeDefParamNodeSel Nothing
-                                    , Available.forTypeDefParamNode p l defMut allTypes' allDefs' defName def'
-                                    )
-                                  )
-                              )
-                            ,
-                              ( 3
-                              , do
-                                  let allKindIDs = \case
-                                        KHole m -> [getID m]
-                                        KType m -> [getID m]
-                                        KFun m k1 k2 -> [getID m] <> allKindIDs k1 <> allKindIDs k2
-                                  id <- Gen.element @[] $ allKindIDs k
-                                  pure
-                                    ( "forTypeDefParamKindNode"
-                                    ,
-                                      ( typeDefParamNodeSel $ Just id
-                                      , Available.forTypeDefParamKindNode p id l defMut allTypes' allDefs' defName def'
-                                      )
-                                    )
-                              )
-                            ]
-                    )
-                  ,
-                    ( 5
-                    , case astTypeDefConstructors def' of
-                        [] -> pure forTypeDef
-                        cs -> do
-                          ValCon{valConName, valConArgs} <- Gen.element cs
-                          let typeDefConsNodeSel = typeDefSel . Just . TypeDefConsNodeSelection . TypeDefConsSelection valConName
-                              forTypeDefConsNode = ("forTypeDefConsNode", (typeDefConsNodeSel Nothing, Available.forTypeDefConsNode l defMut allTypes' allDefs' defName def'))
-                          case valConArgs of
-                            [] -> pure forTypeDefConsNode
-                            as ->
-                              Gen.frequency
-                                [ (1, pure forTypeDefConsNode)
-                                ,
-                                  ( 5
-                                  , do
-                                      (n, t) <- Gen.element $ zip [0 ..] as
-                                      i <- Gen.element $ t ^.. typeIDs
-                                      pure
-                                        ( "forTypeDefConsFieldNode"
-                                        ,
-                                          ( typeDefConsNodeSel . Just $ TypeDefConsFieldSelection n i
-                                          , Available.forTypeDefConsFieldNode valConName n i l defMut allTypes' allDefs' defName def'
-                                          )
-                                        )
-                                  )
-                                ]
-                    )
-                  ]
-      Right (defName, def) ->
-        fmap (first (SelectionDef . DefSelection defName) . snd)
-          . forAllWithT fst
-          . Gen.frequency
-          $ catMaybes
-            [ Just (1, pure ("forDef", (Nothing, Available.forDef (snd <$> allDefs) l defMut defName)))
-            , defAST def <&> \d' -> (2,) $ do
-                let ty = astDefType d'
-                    ids = ty ^.. typeIDs
-                i <- Gen.element ids
-                let hedgehogMsg = "forSig id " <> show i
-                pure (hedgehogMsg, (Just $ NodeSelection SigNode i, Available.forSig l defMut ty i))
-            , defAST def <&> \d' -> (7,) $ do
-                let expr = astDefExpr d'
-                    ids = expr ^.. exprIDs
-                i <- Gen.element ids
-                let hedgehogMsg = "forBody id " <> show i
-                pure (hedgehogMsg, (Just $ NodeSelection BodyNode i, Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i))
-            ]
+    (def'', loc, action) <- forAllT $ genAction l a
+    annotateShow def''
     annotateShow loc
-    case acts of
-      [] -> label "no offered actions" >> success
-      acts' -> do
-        def <-
-          bitraverse
-            (maybe (annotate "primitive type def" >> failure) pure . typeDefAST . snd)
-            (maybe (annotate "primitive def" >> failure) pure . defAST . snd)
-            typeOrTermDef
-        action <- forAllT $ Gen.element acts'
-        collect action
-        case action of
-          Available.NoInput act' -> do
-            progActs <-
-              either (\e -> annotateShow e >> failure) pure
-                $ toProgActionNoInput (map snd $ progAllDefs $ appProg a) def loc act'
-            actionSucceeds (handleEditRequest progActs) a
-          Available.Input act' -> do
-            Available.Options{Available.opts, Available.free} <-
-              maybe (annotate "id not found" >> failure) pure
-                $ Available.options
-                  (map snd $ progAllTypeDefs $ appProg a)
-                  (map snd $ progAllDefs $ appProg a)
-                  (progCxt $ appProg a)
-                  l
-                  def
-                  loc
-                  act'
-            let opts' = [Gen.element $ (Offered,) <$> opts | not (null opts)]
-            let opts'' =
-                  opts' <> case free of
-                    Available.FreeNone -> []
-                    Available.FreeVarName -> [(StudentProvided,) . (\t -> Available.Option t Nothing False) <$> (unName <$> genName)]
-                    Available.FreeInt -> [(StudentProvided,) . (\t -> Available.Option t Nothing False) <$> (show <$> genInt)]
-                    Available.FreeChar -> [(StudentProvided,) . (\t -> Available.Option t Nothing False) . T.singleton <$> genChar]
-            case opts'' of
-              [] -> annotate "no options" >> success
-              options -> do
-                opt <- forAllT $ Gen.choice options
-                progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def loc (snd opt) act'
-                actionSucceedsOrCapture (fst opt) (handleEditRequest progActs) a
+    annotateShow action
+    let (_defName, def) = (bimap fst fst def'', bimap snd snd def'')
+    collect action
+    pa <- toProgAction l a (def, loc, action)
+    case pa of
+      NoOpt progActs -> actionSucceeds (handleEditRequest progActs) a
+      OptOffered _ progActs -> actionSucceeds (handleEditRequest progActs) a
+      OptGen _ progActs -> actionSucceedsOrCapture (handleEditRequest progActs) a
+      NoOfferedOpts -> annotate "no options" >> success
   where
     runEditAppMLogs ::
       HasCallStack =>
@@ -476,34 +319,221 @@ tasty_available_actions_accepted = withTests 500
         (Right _, a') -> ensureSHNormal a'
     -- If we submit our own name rather than an offered one, then
     -- we should expect that name capture/clashing may happen
-    actionSucceedsOrCapture :: HasCallStack => Provenance -> EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT ()
-    actionSucceedsOrCapture p m a = do
+    actionSucceedsOrCapture :: HasCallStack => EditAppM (PureLog (WithSeverity ())) ProgError a -> App -> PropertyT WT ()
+    actionSucceedsOrCapture m a = do
       a' <- runEditAppMLogs m a
-      case (p, a') of
-        (StudentProvided, (Left (ActionError NameCapture), _)) -> do
+      case a' of
+        (Left (ActionError NameCapture), _) -> do
           label "name-capture with entered name"
           annotate "ignoring name capture error as was generated name, not offered one"
-        (StudentProvided, (Left (ActionError (CaseBindsClash{})), _)) -> do
+        (Left (ActionError (CaseBindsClash{})), _) -> do
           label "name-clash with entered name"
           annotate "ignoring name clash error as was generated name, not offered one"
-        (StudentProvided, (Left DefAlreadyExists{}, _)) -> do
+        (Left DefAlreadyExists{}, _) -> do
           label "rename def name clash with entered name"
           annotate "ignoring def already exists error as was generated name, not offered one"
-        (StudentProvided, (Left (ActionError (CaseBranchAlreadyExists (PatPrim _))), _)) -> do
+        (Left (ActionError (CaseBranchAlreadyExists (PatPrim _))), _) -> do
           label "add duplicate primitive case branch"
           annotate "ignoring CaseBranchAlreadyExistsPrim error as was generated constructor"
-        (StudentProvided, (Left (TypeDefAlreadyExists _), _)) -> do
+        (Left (TypeDefAlreadyExists _), _) -> do
           pure ()
-        (StudentProvided, (Left (ConAlreadyExists _), _)) -> do
+        (Left (ConAlreadyExists _), _) -> do
           pure ()
-        (StudentProvided, (Left (TypeDefModifyNameClash _), _)) -> do
+        (Left (TypeDefModifyNameClash _), _) -> do
           pure ()
-        (_, (Left err, _)) -> annotateShow err >> failure
-        (_, (Right _, a'')) -> ensureSHNormal a''
+        (Left err, _) -> annotateShow err >> failure
+        (Right _, a'') -> ensureSHNormal a''
     ensureSHNormal a = case checkAppWellFormed a of
       Left err -> annotateShow err >> failure
       Right a' -> TypeCacheAlpha a === TypeCacheAlpha a'
 
+genAction ::
+  forall m.
+  Monad m =>
+  Level ->
+  App ->
+  GenT
+    m
+    ( Either
+        (TyConName, ASTTypeDef TypeMeta KindMeta)
+        (GVarName, Def)
+    , Selection' ID
+    , Maybe Available.Action
+    )
+genAction l a = do
+  let allTypes = progAllTypeDefsMeta $ appProg a
+      allASTTypes = M.mapMaybe (traverse typeDefAST) allTypes
+      allTypes' = forgetTypeDefMetadata . snd <$> allTypes
+  let allDefs = progAllDefs $ appProg a
+      allDefs' = snd <$> allDefs
+  let isMutable = \case
+        Editable -> True
+        NonEditable -> False
+  let genDef :: Map name (Editable, def) -> GenT m (Maybe (Editable, (name, def)))
+      genDef m =
+        (\(n, (e, t)) -> (e, (n, t)))
+          <<$>> case partition (isMutable . fst . snd) $ Map.toList m of
+            ([], []) -> pure Nothing
+            (mut, []) -> Just <$> Gen.element mut
+            ([], immut) -> Just <$> Gen.element immut
+            (mut, immut) -> Just <$> Gen.frequency [(9, Gen.element mut), (1, Gen.element immut)]
+  (defMut, typeOrTermDef) <-
+    maybe Gen.discard pure
+      =<< Gen.choice
+        [ second Left <<$>> genDef allASTTypes
+        , second Right <<$>> genDef allDefs
+        ]
+  (loc, acts) <- case typeOrTermDef of
+    Left (defName, def) ->
+      let typeDefSel = SelectionTypeDef . TypeDefSelection defName
+          forTypeDef =
+            ( typeDefSel Nothing
+            , Available.forTypeDef l defMut allTypes' allDefs' defName def
+            )
+       in Gen.frequency
+            [ (1, pure forTypeDef)
+            ,
+              ( 2
+              , case astTypeDefParameters def of
+                  [] -> pure forTypeDef
+                  ps -> do
+                    (p, k) <- Gen.element ps
+                    let typeDefParamNodeSel = typeDefSel . Just . TypeDefParamNodeSelection . TypeDefParamSelection p
+                    Gen.frequency
+                      [
+                        ( 1
+                        , pure
+                            ( typeDefParamNodeSel Nothing
+                            , Available.forTypeDefParamNode p l defMut allTypes' allDefs' defName def
+                            )
+                        )
+                      ,
+                        ( 3
+                        , do
+                            let allKindIDs = \case
+                                  KHole m -> [getID m]
+                                  KType m -> [getID m]
+                                  KFun m k1 k2 -> [getID m] <> allKindIDs k1 <> allKindIDs k2
+                            id <- Gen.element @[] $ allKindIDs k
+                            pure
+                              ( typeDefParamNodeSel $ Just id
+                              , Available.forTypeDefParamKindNode p id l defMut allTypes' allDefs' defName def
+                              )
+                        )
+                      ]
+              )
+            ,
+              ( 5
+              , case astTypeDefConstructors def of
+                  [] -> pure forTypeDef
+                  cs -> do
+                    ValCon{valConName, valConArgs} <- Gen.element cs
+                    let typeDefConsNodeSel = typeDefSel . Just . TypeDefConsNodeSelection . TypeDefConsSelection valConName
+                        forTypeDefConsNode =
+                          ( typeDefConsNodeSel Nothing
+                          , Available.forTypeDefConsNode l defMut allTypes' allDefs' defName def
+                          )
+                    case valConArgs of
+                      [] -> pure forTypeDefConsNode
+                      as ->
+                        Gen.frequency
+                          [ (1, pure forTypeDefConsNode)
+                          ,
+                            ( 5
+                            , do
+                                (n, t) <- Gen.element $ zip [0 ..] as
+                                i <- Gen.element $ t ^.. typeIDs
+                                pure
+                                  ( typeDefConsNodeSel . Just $ TypeDefConsFieldSelection n i
+                                  , Available.forTypeDefConsFieldNode valConName n i l defMut allTypes' allDefs' defName def
+                                  )
+                            )
+                          ]
+              )
+            ]
+    Right (defName, def) ->
+      fmap (first (SelectionDef . DefSelection defName))
+        . Gen.frequency
+        $ catMaybes
+          [ Just (1, pure (Nothing, Available.forDef (snd <$> allDefs) l defMut defName))
+          , defAST def <&> \d' -> (2,) $ do
+              let ty = astDefType d'
+                  ids = ty ^.. typeIDs
+              i <- Gen.element ids
+              pure (Just $ NodeSelection SigNode i, Available.forSig l defMut ty i)
+          , defAST def <&> \d' -> (7,) $ do
+              let expr = astDefExpr d'
+                  ids = expr ^.. exprIDs
+              i <- Gen.element ids
+              pure (Just $ NodeSelection BodyNode i, Available.forBody (snd <$> progAllTypeDefs (appProg a)) l defMut expr i)
+          ]
+  case acts of
+    [] -> pure (typeOrTermDef, loc, Nothing)
+    acts' -> do
+      action <- Gen.element acts'
+      pure (typeOrTermDef, loc, Just action)
+
+data PA
+  = NoOpt [ProgAction]
+  | -- | An option the API offered
+    OptOffered Option [ProgAction]
+  | -- | A free-form "student provided" option
+    OptGen Option [ProgAction]
+  | -- | An 'ActionInput' but with no offered options
+    NoOfferedOpts
+
+toProgAction ::
+  Monad m =>
+  Level ->
+  App ->
+  ( Either (ASTTypeDef TypeMeta KindMeta) Def
+  , Selection' ID
+  , Maybe Available.Action
+  ) ->
+  PropertyT m PA
+toProgAction l a (def, loc, action) = do
+  def' <- case (defAST <$> def, action) of
+    (Left d, _) -> pure $ Left d
+    (Right Nothing, Nothing) -> discard
+    (Right Nothing, Just act) -> do
+      annotate "Expected no action to be available on a primitive"
+      annotateShow def
+      annotateShow act
+      failure
+    (Right (Just d), _) -> pure $ Right d
+  case action of
+    Nothing -> discard
+    Just action' -> case action' of
+      Available.NoInput act' -> do
+        progActs <-
+          either (\e -> annotateShow e >> failure) pure
+            $ toProgActionNoInput (map snd $ progAllDefs $ appProg a) def' loc act'
+        pure $ NoOpt progActs
+      Available.Input act' -> do
+        Available.Options{Available.opts, Available.free} <-
+          maybe (annotate "id not found" >> failure) pure
+            $ Available.options
+              (map snd $ progAllTypeDefs $ appProg a)
+              (map snd $ progAllDefs $ appProg a)
+              (progCxt $ appProg a)
+              l
+              def'
+              loc
+              act'
+        let opts' = [Gen.element $ (OptOffered,) <$> opts | not (null opts)]
+        let opts'' =
+              opts' <> case free of
+                Available.FreeNone -> []
+                Available.FreeVarName -> [(OptGen,) . (\t -> Available.Option t Nothing False) <$> (unName <$> genName)]
+                Available.FreeInt -> [(OptGen,) . (\t -> Available.Option t Nothing False) <$> (show <$> genInt)]
+                Available.FreeChar -> [(OptGen,) . (\t -> Available.Option t Nothing False) . T.singleton <$> genChar]
+        case opts'' of
+          [] -> pure NoOfferedOpts
+          options -> do
+            (mkPA, opt) <- forAllWithT (show . snd) $ Gen.choice options
+            progActs <- either (\e -> annotateShow e >> failure) pure $ toProgActionInput def' loc opt act'
+            pure $ mkPA opt progActs
+
 -- 'Raise' works when moving checkable terms into synthesisable position
 unit_raise_sh :: Assertion
 unit_raise_sh =
diff --git a/primer/test/Tests/Eval.hs b/primer/test/Tests/Eval.hs
index 159c785c8..9251883a8 100644
--- a/primer/test/Tests/Eval.hs
+++ b/primer/test/Tests/Eval.hs
@@ -5,6 +5,7 @@ module Tests.Eval where
 import Foreword
 
 import Data.List (delete)
+import Data.List.Extra (enumerate)
 import Data.Map.Strict qualified as Map
 import Data.Set qualified as Set
 import Hedgehog (annotateShow, assert, discard, failure, label, success, (===))
@@ -45,6 +46,7 @@ import Primer.Core.Utils (exprIDs, forgetMetadata)
 import Primer.Def (ASTDef (..), Def (..), DefMap)
 import Primer.Eval (
   ApplyPrimFunDetail (..),
+  AvoidShadowing (NoAvoidShadowing),
   BetaReductionDetail (..),
   BindRenameDetail (..),
   CaseReductionDetail (..),
@@ -105,14 +107,22 @@ import Tests.Gen.Core.Typed (checkTest)
 -- | A helper for these tests
 runTryReduce :: HasCallStack => TypeDefMap -> DefMap -> Cxt -> (Expr, ID) -> IO (Either EvalError (Expr, EvalDetail))
 runTryReduce tys globals locals (expr, i) = do
-  let (r, logs) = evalTestM i $ runPureLogT $ runExceptT $ tryReduceExpr @EvalLog tys globals locals Syn expr
+  let (r, logs) =
+        evalTestM i
+          $ runPureLogT
+          $ runExceptT
+          $ tryReduceExpr @EvalLog NoAvoidShadowing tys globals locals Syn expr
   assertNoSevereLogs logs
   pure r
 
 -- For use in assertions
 runTryReduceType :: HasCallStack => DefMap -> Cxt -> (Type, ID) -> IO (Either EvalError (Type, EvalDetail))
 runTryReduceType globals locals (ty, i) = do
-  let (r, logs) = evalTestM i $ runPureLogT $ runExceptT $ tryReduceType @EvalLog globals locals ty
+  let (r, logs) =
+        evalTestM i
+          $ runPureLogT
+          $ runExceptT
+          $ tryReduceType @EvalLog NoAvoidShadowing globals locals ty
   assertNoSevereLogs logs
   pure r
 
@@ -728,7 +738,10 @@ unit_tryReduce_prim_fail_unreduced_args = do
 
 runStep :: ID -> TypeDefMap -> DefMap -> (Expr, ID) -> IO (Either EvalError (Expr, EvalDetail))
 runStep i' tys globals (e, i) = do
-  let (r, logs) = evalTestM i' $ runPureLogT $ step @EvalLog tys globals e Syn i
+  let (r, logs) =
+        evalTestM i'
+          $ runPureLogT
+          $ step @EvalLog NoAvoidShadowing tys globals e Syn i
   assertNoSevereLogs logs
   pure r
 
@@ -942,7 +955,7 @@ unit_findNodeByID_capture_type =
 -- | A helper for these tests
 redexes' :: TypeDefMap -> DefMap -> Dir -> Expr -> IO (Set ID)
 redexes' types prims d e = do
-  let (rs, logs) = runPureLog $ redexes types prims d e
+  let (rs, logs) = runPureLog $ redexes NoAvoidShadowing types prims d e
   assertNoSevereLogs @EvalLog logs
   pure $ Set.fromList rs
 
@@ -1399,12 +1412,13 @@ tasty_type_preservation =
         $ propertyWT testModules
         $ do
           let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
+          as <- forAllT $ Gen.element enumerate
           tds <- asks typeDefs
           (dir, t, ty) <- genDirTm
-          rs <- failWhenSevereLogs $ redexes @EvalLog tds globs dir t
+          rs <- failWhenSevereLogs $ redexes @EvalLog as tds globs dir t
           when (null rs) discard
           r <- forAllT $ Gen.element rs
-          s <- failWhenSevereLogs $ step @EvalLog tds globs t dir r
+          s <- failWhenSevereLogs $ step @EvalLog as tds globs t dir r
           case s of
             Left err -> annotateShow err >> failure
             Right (s', _) ->
@@ -1433,22 +1447,23 @@ tasty_redex_independent =
         $ propertyWT testModules
         $ do
           let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
+          as <- forAllT $ Gen.element enumerate
           tds <- asks typeDefs
           (dir, t, _) <- genDirTm
           annotateShow dir
           annotateShow t
-          rs <- failWhenSevereLogs $ redexes @EvalLog tds globs dir t
+          rs <- failWhenSevereLogs $ redexes @EvalLog as tds globs dir t
           when (length rs <= 1) discard
           i <- forAllT $ Gen.element rs
           j <- forAllT $ Gen.element $ delete i rs
-          s <- failWhenSevereLogs $ step @EvalLog tds globs t dir i
+          s <- failWhenSevereLogs $ step @EvalLog as tds globs t dir i
           case s of
             Left err -> annotateShow err >> failure
             Right (s', siDetails) -> do
               annotateShow s'
               if elemOf exprIDs j s'
                 then do
-                  sj <- failWhenSevereLogs $ step @EvalLog tds globs t dir j
+                  sj <- failWhenSevereLogs $ step @EvalLog as tds globs t dir j
                   case (sj, siDetails) of
                     (Right (_, BindRename{}), _) -> success
                     (_, PushLetDown{}) -> success
@@ -1458,5 +1473,5 @@ tasty_redex_independent =
                     (Right (_, PushLetDown{}), RemoveAnn{}) -> success
                     (Right (_, PushLetDown{}), LetRemoval{}) -> success
                     (Right (_, PushLetDownTy{}), TLetRemoval{}) -> success
-                    _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog tds globs dir s')
+                    _ -> assert . elem j =<< failWhenSevereLogs (redexes @EvalLog as tds globs dir s')
                 else success
diff --git a/primer/test/Tests/EvalFull.hs b/primer/test/Tests/EvalFull.hs
index f97c1e894..7a51080e1 100644
--- a/primer/test/Tests/EvalFull.hs
+++ b/primer/test/Tests/EvalFull.hs
@@ -378,7 +378,7 @@ unit_12 =
         expect <- con0 cTrue `ann` tcon tBool
         pure (expr, expect)
    in do
-        s <- evalFullTestExactSteps maxID builtinTypes mempty 10 Syn e
+        s <- evalFullTestExactSteps maxID builtinTypes mempty 9 Syn e
         s ~== expected
 
 unit_13 :: Assertion
@@ -529,8 +529,8 @@ unit_letrec_body_first =
           (con cCons [lvar "x", lvar "xs"])
           (tcon tList `tapp` tEmptyHole)
       (expr, maxID) = create $ lx $ lxs (lvar "xs")
-      expected1 = create' $ lx $ lxs $ con cCons [lvar "x", lvar "xs"] `ann` (tcon tList `tapp` tEmptyHole)
-      expected2 = create' $ lx (lxs $ con cCons [lvar "x", lvar "xs"]) `ann` (tcon tList `tapp` tEmptyHole)
+      expected1 = create' $ lx $ lxs (con cCons [lvar "x", lvar "xs"]) `ann` (tcon tList `tapp` tEmptyHole)
+      expected2 = create' $ lx (lxs (con cCons [lvar "x", lvar "xs"])) `ann` (tcon tList `tapp` tEmptyHole)
       expected3 = create' $ con cCons [lx $ lvar "x", lx $ lxs $ lvar "xs"] `ann` (tcon tList `tapp` tEmptyHole)
    in do
         e1 <- evalFullTest maxID builtinTypes mempty 1 Syn expr
@@ -796,7 +796,7 @@ tasty_open_closed_agree_base_types :: Property
 tasty_open_closed_agree_base_types = withDiscards 1000
   $ propertyWT testModules
   $ do
-    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
     let optsR = RunRedexOptions{pushAndElide = True}
     ty <- forAllT $ Gen.element @[] [tBool, tNat, tInt]
     tm' <- forAllT $ genChk $ TCon () ty
@@ -836,7 +836,7 @@ tasty_resume = withDiscards 2000
 -- A helper for tasty_resume, and tasty_resume_regression
 resumeTest :: [Module] -> Dir -> Expr -> PropertyT WT ()
 resumeTest mods dir t = do
-  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
   let optsR = RunRedexOptions{pushAndElide = True}
   let globs = foldMap' moduleDefsQualified mods
   tds <- asks typeDefs
@@ -1122,7 +1122,6 @@ unit_let_self_capture =
           , expr4
           , expected4a
           , expected4b
-          , expected4c
           )
         , maxID
         ) = create $ do
@@ -1136,19 +1135,12 @@ unit_let_self_capture =
           -- We do not need to do anything special for letrec
           e4 <- lAM "a" $ lam "f" $ lam "x" $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "x")
           expect4a <-
-            lAM "a"
-              $ lam "f"
-              $ lam "x"
-              $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a")
-              $ (lvar "f" `app` lvar "x")
-              `ann` tvar "a"
-          expect4b <-
             lAM "a"
               $ lam "f"
               $ lam "x"
               $ letrec "x" (lvar "f" `app` lvar "x") (tvar "a") (lvar "f" `app` lvar "x")
               `ann` tvar "a"
-          expect4c <-
+          expect4b <-
             lAM "a"
               $ lam "f"
               $ lam "x"
@@ -1165,7 +1157,6 @@ unit_let_self_capture =
             , e4
             , expect4a
             , expect4b
-            , expect4c
             )
       s1 n = evalFullTest maxID mempty mempty n Chk expr1
       s2 n = evalFullTest maxID mempty mempty n Chk expr2
@@ -1189,7 +1180,6 @@ unit_let_self_capture =
         s3 3 >>= (<~==> Right expected3b)
         s4 1 >>= (<~==> Left (TimedOut expected4a))
         s4 2 >>= (<~==> Left (TimedOut expected4b))
-        s4 3 >>= (<~==> Left (TimedOut expected4c))
 
 -- | @spanM p mxs@ returns a tuple where the first component is the
 -- values coming from the longest prefix of @mxs@ all of which satisfy
@@ -1256,7 +1246,7 @@ tasty_type_preservation = withTests 1000
   $ withDiscards 2000
   $ propertyWT testModules
   $ do
-    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
     let optsR = RunRedexOptions{pushAndElide = True}
     let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
     tds <- asks typeDefs
@@ -1827,7 +1817,7 @@ tasty_unique_ids = withTests 1000
   $ withDiscards 2000
   $ propertyWT testModules
   $ do
-    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
     let optsR = RunRedexOptions{pushAndElide = True}
     let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
     tds <- asks typeDefs
@@ -1902,16 +1892,30 @@ unit_case_prim =
 
 -- * Utilities
 
-evalFullTest :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
-evalFullTest id_ tydefs globals n d e = do
+evalFullTest' ::
+  HasCallStack =>
+  ViewRedexOptions ->
+  ID ->
+  TypeDefMap ->
+  DefMap ->
+  TerminationBound ->
+  Dir ->
+  Expr ->
+  IO (Either EvalFullError Expr)
+evalFullTest' optsV id_ tydefs globals n d e = do
   let optsN = UnderBinders
-  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
   let optsR = RunRedexOptions{pushAndElide = True}
   let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR tydefs globals n d e
   assertNoSevereLogs logs
   distinctIDs r
   pure r
 
+evalFullTest :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
+evalFullTest = evalFullTest' ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
+
+evalFullTestAvoidShadowing :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO (Either EvalFullError Expr)
+evalFullTestAvoidShadowing = evalFullTest' ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = True}
+
 evalFullTestExactSteps :: HasCallStack => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> IO Expr
 evalFullTestExactSteps id_ tydefs globals n d e = do
   s <- evalFullTest id_ tydefs globals (n - 1) d e
@@ -1931,7 +1935,7 @@ evalFullTestClosed gl id_ tydefs globals n d e = do
   let gl' = case gl of
         GroupedLets -> True
         SingleLets -> False
-  let optsV = ViewRedexOptions{groupedLets = gl', aggressiveElision = True}
+  let optsV = ViewRedexOptions{groupedLets = gl', aggressiveElision = True, avoidShadowing = False}
   let optsR = RunRedexOptions{pushAndElide = True}
   let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR tydefs globals n d e
   assertNoSevereLogs logs
@@ -1941,7 +1945,7 @@ evalFullTestClosed gl id_ tydefs globals n d e = do
 evalFullTasty :: MonadTest m => ID -> TypeDefMap -> DefMap -> TerminationBound -> Dir -> Expr -> m (Either EvalFullError Expr)
 evalFullTasty id_ tydefs globals n d e = do
   let optsN = UnderBinders
-  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+  let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
   let optsR = RunRedexOptions{pushAndElide = True}
   let (r, logs) = evalTestM id_ $ runPureLogT $ evalFull @EvalLog optsN optsV optsR tydefs globals n d e
   testNoSevereLogs logs
diff --git a/primer/test/Tests/Prelude/Utils.hs b/primer/test/Tests/Prelude/Utils.hs
index 2dab33ad6..fb73cd7e5 100644
--- a/primer/test/Tests/Prelude/Utils.hs
+++ b/primer/test/Tests/Prelude/Utils.hs
@@ -10,7 +10,7 @@ import Primer.Core.DSL (apps', create', gvar)
 import Primer.Eval (
   NormalOrderOptions (UnderBinders),
   RunRedexOptions (RunRedexOptions, pushAndElide),
-  ViewRedexOptions (ViewRedexOptions, aggressiveElision, groupedLets),
+  ViewRedexOptions (ViewRedexOptions, aggressiveElision, avoidShadowing, groupedLets),
  )
 import Primer.EvalFull (Dir (Chk), EvalFullError, EvalLog, TerminationBound, evalFull)
 import Primer.Log (runPureLogT)
@@ -55,7 +55,7 @@ functionOutput f args = functionOutput' f (map Left args)
 functionOutput' :: GVarName -> [Either (TestM Expr) (TestM Type)] -> TerminationBound -> Either EvalFullError Expr
 functionOutput' f args depth =
   let optsN = UnderBinders
-      optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True}
+      optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = False}
       optsR = RunRedexOptions{pushAndElide = True}
       (r, logs) = evalTestM 0 $ runPureLogT $ do
         e <- apps' (gvar f) $ bimap lift lift <$> args
diff --git a/primer/test/Tests/Shadowing.hs b/primer/test/Tests/Shadowing.hs
new file mode 100644
index 000000000..86681f192
--- /dev/null
+++ b/primer/test/Tests/Shadowing.hs
@@ -0,0 +1,325 @@
+{-# LANGUAGE ViewPatterns #-}
+
+module Tests.Shadowing where
+
+import Foreword
+
+import Data.Data (Data)
+import Data.Generics.Uniplate.Data qualified as U
+import Data.List.Extra (enumerate)
+import Data.Set qualified as Set
+import Hedgehog (annotateShow, discard, failure, forAll, label, success, (===))
+import Hedgehog.Gen qualified as Gen
+import Hedgehog.Range qualified as Range
+import Primer.Action.Available (Action (NoInput), NoInputAction (LetToRec))
+import Primer.App (App, appProg, handleEditRequest, progAllDefs, progAllTypeDefs, runEditAppM)
+import Primer.Core (
+  Expr,
+  Expr' (Case, Var),
+  LocalName (unLocalName),
+  TmVarRef (GlobalVarRef),
+  Type',
+ )
+import Primer.Core.DSL (ann, app, create, create', lam, let_, lvar, tEmptyHole, tfun)
+import Primer.Core.Utils (freeGlobalVars)
+import Primer.Def (Def, astDefExpr, defAST, defType)
+import Primer.Eval (
+  AvoidShadowing (AvoidShadowing),
+  Dir (Syn),
+  NormalOrderOptions (StopAtBinders, UnderBinders),
+  RunRedexOptions (RunRedexOptions, pushAndElide),
+  ViewRedexOptions (ViewRedexOptions, aggressiveElision, avoidShadowing, groupedLets),
+  redexes,
+  step,
+ )
+import Primer.EvalFull (EvalFullError (..), EvalLog, evalFullStepCount)
+import Primer.Gen.App (genApp)
+import Primer.Gen.Core.Typed (forAllT, propertyWT)
+import Primer.Log (runPureLog)
+import Primer.Module (builtinModule, moduleDefsQualified, primitiveModule)
+import Primer.Name (Name)
+import Primer.Test.Util (failWhenSevereLogs)
+import Primer.TypeDef (ASTTypeDef (..), TypeDef, typeDefAST, typeDefParameters, valConArgs)
+import Primer.Typecheck (Cxt (typeDefs), SmartHoles (SmartHoles))
+import Primer.Zipper (
+  FoldAbove' (FA, current, prior),
+  Loc' (InExpr),
+  bindersAbove,
+  focus,
+  focusOn,
+  focusOnlyType,
+  focusType,
+  getBoundHereUp,
+  getBoundHereUpTy,
+  target,
+ )
+import Tasty (Property, withDiscards, withTests)
+import Test.Tasty.HUnit (Assertion)
+import Tests.Action.Available (PA (..), genAction, toProgAction)
+import Tests.Eval.Utils (genDirTm, testModules)
+import Tests.EvalFull (evalFullTestAvoidShadowing, (<~==>))
+import Tests.Gen.Core.Typed (propertyWTInExtendedGlobalCxt)
+
+{-
+Evaluation can result in variable shadowing even when there are no repeated binders in the initial term.
+We detect this shadowing and rename to avoid it.
+  (λf. f f : (? -> ?) -> ?) (λg y. g y)
+reduces in 4 steps to
+  (let g = (let f = λg y. g y : ? -> ? in f : ?) in λy. g y) : ? : ?
+if we did not worry about shadowing, we would then push the 'let g' and get
+  (λy. let g = (let f = λg y. g y : ? -> ? in f : ?) in g y) : ? : ?
+where the 'y' is shadowed.
+However, we instead do a renaming step and get
+  (let g = (let f = λg y. g y : ? -> ? in f : ?) in λz. let y = z in g y) : ? : ?
+-}
+unit_shadow_no_reused_binders :: Assertion
+unit_shadow_no_reused_binders =
+  let ((e, expect), maxID) = create $ do
+        e0 <-
+          ( lam "f" (lvar "f" `app` lvar "f")
+              `ann` ((tEmptyHole `tfun` tEmptyHole) `tfun` tEmptyHole)
+            )
+            `app` lam "g" (lam "y" $ lvar "g" `app` lvar "y")
+        e4 <-
+          ( let_
+              "g"
+              ( let_
+                  "f"
+                  (lam "g" (lam "y" $ lvar "g" `app` lvar "y") `ann` (tEmptyHole `tfun` tEmptyHole))
+                  (lvar "f")
+                  `ann` tEmptyHole
+              )
+              (lam "y" $ lvar "g" `app` lvar "y")
+              `ann` tEmptyHole
+            )
+            `ann` tEmptyHole
+        let z = "a88"
+        e5 <-
+          ( let_
+              "g"
+              ( let_
+                  "f"
+                  (lam "g" (lam "y" $ lvar "g" `app` lvar "y") `ann` (tEmptyHole `tfun` tEmptyHole))
+                  (lvar "f")
+                  `ann` tEmptyHole
+              )
+              (lam z $ let_ "y" (lvar z) $ lvar "g" `app` lvar "y")
+              `ann` tEmptyHole
+            )
+            `ann` tEmptyHole
+        pure (e0, [(0, e0), (4, e4), (5, e5)])
+   in do
+        for_ @[] expect $ \(s, ex) -> do
+          a <- evalFullTestAvoidShadowing maxID mempty mempty s Syn e
+          a <~==> Left (TimedOut ex)
+
+-- We use this type to compute a "tree of binders", which are a view of
+-- an expression (or type) where we only care about the tree shape and
+-- what subtrees binders scope over. (In fact, we don't strictly preserve
+-- the tree shape, as it is sometimes easier to insert extra empty nodes.)
+-- The 'a' parameter (node labels) are only needed for implementation of
+-- 'binderTree'
+data Tree a b = Node a [(b, Tree a b)]
+  deriving stock (Functor, Show)
+
+instance Bifunctor Tree where
+  bimap f g (Node a xs) = Node (f a) $ map (bimap g (bimap f g)) xs
+
+foldTree :: (a -> [(b, c)] -> c) -> Tree a b -> c
+foldTree f (Node a xs) = f a $ map (second $ foldTree f) xs
+
+-- NB: there are no children in kinds, so we need not look in the metadata
+-- NB: any binder in types (∀ only) scopes over all type children
+binderTreeTy :: forall b c. (Data b, Data c, Eq b, Eq c) => Type' b c -> Tree () (Set Name)
+binderTreeTy = noNodeLabels' . go
+  where
+    go :: Type' b c -> Tree (Type' b c) (Set Name)
+    go = U.para $ \ty children ->
+      Node ty $ map (\c@(Node c' _) -> (Set.map unLocalName $ getBoundHereUpTy FA{prior = c', current = ty}, c)) children
+
+-- Note this DOES NOT check if anything in the metadata's TypeCache
+-- is shadowed (or is shadowing); (see 'binderTree'). Currently
+-- it happens that we can ascribe a type of '∀a. _' to
+-- a subterm that happens to be under an 'a' binder. See
+-- https://github.com/hackworthltd/primer/issues/556
+noShadowing :: (Data a, Data b, Data c, Eq a, Eq b, Eq c) => Expr' a b c -> Shadowing
+noShadowing = checkShadowing . binderTree
+
+noShadowingTy :: (Data b, Data c, Eq b, Eq c) => Type' b c -> Shadowing
+noShadowingTy = checkShadowing . binderTreeTy
+
+noNodeLabels' :: Tree a' b' -> Tree () b'
+noNodeLabels' = bimap (const ()) identity
+
+binderTree :: forall a b c. (Data a, Data b, Data c, Eq a, Eq b, Eq c) => Expr' a b c -> Tree () (Set Name)
+binderTree = noNodeLabels' . go
+  where
+    noNodeLabels :: Tree () b' -> Tree (Maybe a') b'
+    noNodeLabels = bimap (const Nothing) identity
+    go :: Expr' a b c -> Tree (Maybe (Expr' a b c)) (Set Name)
+    go = U.para $ \e exprChildren' ->
+      let exprChildren =
+            map
+              ( \c@(Node c' _) ->
+                  ( case c' of
+                      Nothing -> mempty -- no term binders scope over metadata or type children
+                      Just c'' -> getBoundHereUp $ FA{prior = c'', current = e}
+                  , c
+                  )
+              )
+              exprChildren'
+          typeChildren = case target . focusOnlyType <$> focusType (focus e) of
+            Just ty -> [binderTreeTy ty]
+            Nothing -> mempty
+       in {-
+             -- We don't include metadata. see
+             -- https://github.com/hackworthltd/primer/issues/556
+             metaChildren = case e ^. _exprMetaLens % _type of
+               Nothing -> mempty
+               Just (TCChkedAt ty) -> [binderTreeTy ty]
+               Just (TCSynthed ty) -> [binderTreeTy ty]
+               Just (TCEmb (TCBoth ty1 ty2)) -> [binderTreeTy ty1, binderTreeTy ty2]
+             -}
+
+          Node (Just e) $ exprChildren <> map ((mempty,) . noNodeLabels) typeChildren {- <> metaChildren-}
+
+data Shadowing = ShadowingExists (Set Name) | ShadowingNotExists
+  deriving stock (Eq, Show)
+
+checkShadowing :: Tree () (Set Name) -> Shadowing
+checkShadowing t =
+  let shadows = fst $ foldTree f t
+   in if Set.null shadows
+        then ShadowingNotExists
+        else ShadowingExists shadows
+  where
+    f :: () -> [(Set Name, (Set Name, Set Name))] -> (Set Name, Set Name)
+    f () xs =
+      let allSubtreeBinds = Set.unions $ map (snd . snd) xs
+          bindsHere = Set.unions $ map fst xs
+          allBinds = bindsHere <> allSubtreeBinds
+          shadowing = Set.unions $ map (\(newBinders, (oldShadows, oldBinders)) -> oldShadows <> Set.intersection newBinders oldBinders) xs
+       in (shadowing, allBinds)
+
+-- Check evaluation does not introduce shadowing, except in some known cases
+tasty_eval_full_shadow :: Property
+tasty_eval_full_shadow = withTests 500
+  $ withDiscards 2000
+  $ propertyWTInExtendedGlobalCxt testModules
+  $ do
+    let optsV = ViewRedexOptions{groupedLets = True, aggressiveElision = True, avoidShadowing = True}
+    let optsR = RunRedexOptions{pushAndElide = True}
+    let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
+    optsN <- forAll $ Gen.element @[] [StopAtBinders, UnderBinders]
+    tds <- asks typeDefs
+    (dir, t, _ty) <- genDirTm
+    unless (noShadowing t == ShadowingNotExists) discard
+    when (isKnownShadow optsN t) discard
+    n <- forAll $ Gen.integral (Range.linear 1 20)
+    (_steps, s) <- failWhenSevereLogs $ evalFullStepCount @EvalLog optsN optsV optsR tds globs n dir t
+    annotateShow s
+    noShadowing (getEvalResultExpr s) === ShadowingNotExists
+  where
+    -- Inlining a global under a binder may cause shadowing, as we don't track
+    -- what new binders this may bring into scope
+    -- This can be a global term definition, or a case reduction bringing in part of a global type defininiton
+    isKnownShadow UnderBinders e = not $ Set.null (freeGlobalVars e) && null [() | Case{} <- U.universe e]
+    isKnownShadow StopAtBinders _ = False
+
+tasty_eval_shadow :: Property
+tasty_eval_shadow =
+  withDiscards 2000
+    $ propertyWTInExtendedGlobalCxt testModules
+    $ do
+      let globs = foldMap' moduleDefsQualified $ create' $ sequence testModules
+      tds <- asks typeDefs
+      (dir, t, _ty) <- genDirTm
+      unless (noShadowing t == ShadowingNotExists) discard
+      rs <- failWhenSevereLogs $ redexes @EvalLog AvoidShadowing tds globs dir t
+      when (null rs) discard
+      i <- forAllT $ Gen.element rs
+      when (isKnownShadow $ focusOn i t) discard
+      s <- failWhenSevereLogs $ step @EvalLog AvoidShadowing tds globs t dir i
+      case s of
+        Left err -> annotateShow err >> failure
+        Right (s', _) -> do
+          annotateShow s
+          noShadowing s' === ShadowingNotExists
+  where
+    -- Inlining a global under a binder may cause shadowing, as we don't track
+    -- what new binders this may bring into scope
+    isKnownShadow (Just (InExpr ez@(target -> Var _ (GlobalVarRef _)))) = not $ Set.null $ bindersAbove ez
+    isKnownShadow _ = False
+
+getEvalResultExpr :: Either EvalFullError Expr -> Expr
+getEvalResultExpr = \case
+  Left (TimedOut e) -> e
+  Right e -> e
+
+tasty_available_actions_shadow :: Property
+tasty_available_actions_shadow = withDiscards 2000
+  $ propertyWT []
+  $ do
+    l <- forAllT $ Gen.element enumerate
+    cxt <- forAllT $ Gen.choice $ map sequence [[], [builtinModule], [builtinModule, primitiveModule]]
+    a <- forAllT $ genApp SmartHoles cxt
+    unless (all ((== ShadowingNotExists) . snd) $ noShadowingApp a) discard
+    (def', loc, act) <- forAllT $ genAction l a
+    let (defName, def) = (bimap fst fst def', bimap snd snd def')
+    annotateShow defName
+    annotateShow def
+    annotateShow loc
+    annotateShow act
+    progActs' <- toProgAction l a (def, loc, act)
+    progActs <- case progActs' of
+      NoOpt progActs -> pure progActs
+      OptOffered _ progActs -> pure progActs
+      OptGen _ _ -> discard
+      NoOfferedOpts -> discard
+    let (res, _logs) = runPureLog $ runEditAppM (handleEditRequest progActs) a
+    let isKnownShadow = case act of
+          Just (NoInput LetToRec) ->
+            {- The following action can introduce shadowing
+            let bar = (let bar = ? in ?) in ?
+            ~>
+            letrec bar = (let bar = ? in ?) : ? in ?
+            -}
+            True
+          _ -> False
+    case (res, isKnownShadow) of
+      ((Left err, _), _) -> annotateShow err >> failure
+      ((Right _, _), True) -> label "known shadowing case" >> success
+      ((Right _, a'), False) -> do
+        label "not known shadowing case"
+        annotateShow a'
+        for_ (noShadowingApp a') $ \(d, s) -> do
+          unless (s == ShadowingNotExists) $ annotateShow d
+          s === ShadowingNotExists
+
+noShadowingApp :: App -> [(Either (TypeDef () ()) Def, Shadowing)]
+noShadowingApp a =
+  let p = appProg a
+      tds = snd <$> toList (progAllTypeDefs p)
+      ds = snd <$> toList (progAllDefs p)
+   in map (\d -> (Left d, noShadowingTypeDef d)) tds <> map (\d -> (Right d, noShadowingDef d)) ds
+  where
+    combineShadow ShadowingNotExists s = s
+    combineShadow s ShadowingNotExists = s
+    combineShadow (ShadowingExists x) (ShadowingExists y) = ShadowingExists $ x <> y
+    noShadowingTypeDef = checkShadowing . binderTreeTypeDef
+    noShadowingDef d =
+      let sty = (noShadowingTy $ defType d)
+          stm = (noShadowing . astDefExpr <$> defAST d)
+       in sty & maybe identity (flip combineShadow) stm
+
+binderTreeTypeDef :: (Data a, Data b, Eq a, Eq b) => TypeDef a b -> Tree () (Set Name)
+binderTreeTypeDef ty =
+  Node
+    ()
+    [
+      ( Set.fromList $ unLocalName . fst <$> typeDefParameters ty
+      , Node () $ (mempty,) . bindersVC <$> (astTypeDefConstructors =<< toList (typeDefAST ty))
+      )
+    ]
+  where
+    bindersVC vc = Node () $ valConArgs vc <&> (mempty,) . binderTreeTy
diff --git a/primer/test/Tests/Typecheck.hs b/primer/test/Tests/Typecheck.hs
index 8824a366b..7fcacb93f 100644
--- a/primer/test/Tests/Typecheck.hs
+++ b/primer/test/Tests/Typecheck.hs
@@ -51,6 +51,7 @@ import Primer.Builtins (
   tList,
   tMaybe,
   tNat,
+  tPair,
  )
 import Primer.Builtins.DSL (
   listOf,
@@ -517,6 +518,15 @@ unit_case_branches =
   ann (case_ (con0 cZero `ann` tcon tNat) [branch' (["M"], "C") [] $ lvar "x"]) (tcon tBool)
     `smartSynthGives` ann (case_ (con0 cZero `ann` tcon tNat) [branch cZero [] emptyHole, branch cSucc [("a9", Nothing)] emptyHole]) (tcon tBool) -- Fragile name here "a9"
 
+unit_case_distinct_binds :: Assertion
+unit_case_distinct_binds =
+  ( case_
+      (emptyHole `ann` (tcon tPair `tapp` tEmptyHole `tapp` tEmptyHole))
+      [branch cMakePair [("x", Nothing), ("x", Nothing)] emptyHole]
+      `ann` tEmptyHole
+  )
+    `expectFailsWith` const (DuplicateBinders ["x", "x"])
+
 unit_remove_hole :: Assertion
 unit_remove_hole =
   ann (lam "x" $ hole (lvar "x")) (tfun (tcon tNat) (tcon tNat))
diff --git a/primer/test/Tests/Zipper.hs b/primer/test/Tests/Zipper.hs
index b13e9e020..d763da520 100644
--- a/primer/test/Tests/Zipper.hs
+++ b/primer/test/Tests/Zipper.hs
@@ -3,10 +3,12 @@ module Tests.Zipper where
 
 import Foreword
 
+import Data.Set qualified as Set
 import Hedgehog hiding (Property, property)
 import Hedgehog.Gen qualified as Gen
 import Optics ((^..))
 import Primer.Core
+import Primer.Core.DSL (aPP, ann, branch', case_, create', emptyHole, hole, ktype, lAM, lam, tEmptyHole, tapp, tforall, thole)
 import Primer.Core.Utils (exprIDs)
 import Primer.Gen.Core.Raw (
   evalExprGen,
@@ -15,6 +17,7 @@ import Primer.Gen.Core.Raw (
  )
 import Primer.Zipper
 import Tasty (Property, property)
+import Test.Tasty.HUnit (Assertion, (@?=))
 
 -- | @unfocus . focus == id@
 tasty_focus_unfocus_roundtrip :: Property
@@ -43,3 +46,21 @@ tasty_focusOn_succeeds_on_valid_ids = property $ do
       Just (InBind (BindCase b)) -> getID (target b) === i
       Just (InKind k) -> getID (target k) === i
       _ -> annotateShow i >> failure
+
+unit_binders_below_type :: Assertion
+unit_binders_below_type =
+  let t = create' $ tapp tEmptyHole $ tforall "a" ktype $ thole $ tforall "b" ktype tEmptyHole
+   in bindersBelowTy (focus t) @?= Set.fromList ["a", "b"]
+
+unit_binders_below :: Assertion
+unit_binders_below =
+  let e =
+        create'
+          $ ann
+            ( lam "x"
+                $ case_
+                  (lAM "y" emptyHole)
+                  [branch' (["M"], "C") [("z", Nothing), ("w", Nothing)] $ aPP (hole $ lam "v" emptyHole) (tapp tEmptyHole $ tforall "a" ktype $ tforall "b" ktype tEmptyHole)]
+            )
+            (thole $ tforall "c" ktype tEmptyHole)
+   in bindersBelow (focus e) @?= Set.fromList ["x", "y", "z", "w", "v", "a", "b", "c"]
diff --git a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment
index 81ac37f9c..cf5aa2c64 100644
--- a/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment
+++ b/primer/test/outputs/available-actions/M.comprehensive/Expert-Editable.fragment
@@ -47,12 +47,12 @@ Output
                     ( Options
                         { opts =
                             [ Option
-                                { option = "α"
+                                { option = "γ"
                                 , context = Nothing
                                 , matchesType = False
                                 }
                             , Option
-                                { option = "γ"
+                                { option = "α1"
                                 , context = Nothing
                                 , matchesType = False
                                 }
@@ -231,12 +231,12 @@ Output
                     ( Options
                         { opts =
                             [ Option
-                                { option = "α"
+                                { option = "γ"
                                 , context = Nothing
                                 , matchesType = False
                                 }
                             , Option
-                                { option = "γ"
+                                { option = "α1"
                                 , context = Nothing
                                 , matchesType = False
                                 }
@@ -971,12 +971,12 @@ Output
                     ( Options
                         { opts =
                             [ Option
-                                { option = "α"
+                                { option = "γ"
                                 , context = Nothing
                                 , matchesType = False
                                 }
                             , Option
-                                { option = "γ"
+                                { option = "α1"
                                 , context = Nothing
                                 , matchesType = False
                                 }