Ensure API calls do not introduce shadowing (#559)

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)

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

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

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

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

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

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,26 +186,28 @@ 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
 
 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