merge: Eliminate Unnecessary Shadow Warning (#1264)

This PR intends to eliminate unnecessary and annoying shadow warnings.
However, the following code will not report any shadow warning even if
the pattern shadows a local variable of another parameter:

```aya
def test (A : Type) (a : A) : A
| a, A => A
```

This is because we cannot tell the parameter of a pattern, this part is
done in PatTycker, but it should can be done in desugarer.

base/src/main/java/org/aya/resolve/context/NoExportContext.java

@@ -11,9 +11,7 @@
 
 import java.nio.file.Path;
 
-/**
- * Used for `let open`
- */
+/// Used for `let open` and `example`
 public record NoExportContext(
   @NotNull Context parent,
   @NotNull ModuleSymbol<AnyVar> symbols,

base/src/main/java/org/aya/resolve/visitor/ExprResolver.java

@@ -22,13 +22,15 @@
 import org.aya.syntax.ref.AnyVar;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.GeneralizedVar;
+import org.aya.syntax.ref.LocalVar;
 import org.aya.tyck.error.ClassError;
 import org.aya.util.error.Panic;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
 
 /**
  * Resolves bindings.
@@ -194,7 +196,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
 
         // Requires exhaustiveness check, therefore must need the full data body
         enter(Where.FnPattern);
-        var clauses = match.clauses().map(this::clause);
+        var clauses = match.clauses().map(x -> clause(ImmutableSeq.empty(), x));
         exit();
 
         yield match.update(discriminant, clauses, returns);
@@ -221,19 +223,20 @@ private void addReference(@NotNull DefVar<?, ?> defVar) {
     addReference(defVar.concrete);
   }
 
-  public @NotNull Pattern.Clause clause(@NotNull Pattern.Clause clause) {
+  public @NotNull Pattern.Clause clause(@NotNull ImmutableSeq<LocalVar> telescope, @NotNull Pattern.Clause clause) {
     var mCtx = MutableValue.create(ctx);
     enter(Where.FnPattern);
-    var pats = clause.patterns.map(pa -> pa.descent(pat -> resolvePattern(pat, mCtx)));
+    var pats = clause.patterns.map(pa ->
+      pa.descent(pat -> resolvePattern(pat, telescope, mCtx)));
     exit();
     enter(Where.FnBody);
     var body = clause.expr.map(x -> x.descent(enter(mCtx.get())));
     exit();
     return clause.update(pats, body);
   }
 
-  public @NotNull WithPos<Pattern> resolvePattern(@NotNull WithPos<Pattern> pattern, MutableValue<Context> ctx) {
-    var resolver = new PatternResolver(ctx.get(), this::addReference);
+  public @NotNull WithPos<Pattern> resolvePattern(@NotNull WithPos<Pattern> pattern, @NotNull ImmutableSeq<LocalVar> telescope, MutableValue<Context> ctx) {
+    var resolver = new PatternResolver(ctx.get(), telescope, this::addReference);
     var result = pattern.descent(resolver);
     ctx.set(resolver.context());
     return result;

base/src/main/java/org/aya/resolve/visitor/PatternResolver.java

@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.resolve.visitor;
 
+import kala.collection.immutable.ImmutableSeq;
 import org.aya.generic.stmt.TyckUnit;
 import org.aya.resolve.context.Context;
 import org.aya.resolve.error.NameProblem;
@@ -10,10 +11,7 @@
 import org.aya.syntax.concrete.stmt.ModuleName;
 import org.aya.syntax.concrete.stmt.decl.DataCon;
 import org.aya.syntax.core.def.ConDefLike;
-import org.aya.syntax.ref.AnyDefVar;
-import org.aya.syntax.ref.AnyVar;
-import org.aya.syntax.ref.CompiledVar;
-import org.aya.syntax.ref.DefVar;
+import org.aya.syntax.ref.*;
 import org.aya.util.error.Panic;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.SourcePos;
@@ -25,10 +23,12 @@
 public class PatternResolver implements PosedUnaryOperator<Pattern> {
   // DIRTY!!
   private @NotNull Context context;
+  private final @NotNull ImmutableSeq<LocalVar> mercy;
   private final @NotNull Consumer<TyckUnit> parentAdd;
 
-  public PatternResolver(@NotNull Context context, @NotNull Consumer<TyckUnit> parentAdd) {
+  public PatternResolver(@NotNull Context context, @NotNull ImmutableSeq<LocalVar> mercy, @NotNull Consumer<TyckUnit> parentAdd) {
     this.context = context;
+    this.mercy = mercy;
     this.parentAdd = parentAdd;
   }
 
@@ -47,7 +47,7 @@ public PatternResolver(@NotNull Context context, @NotNull Consumer<TyckUnit> par
         }
 
         // It is not a constructor, it is a bind
-        context = context.bind(bind.bind());
+        context = context.bind(bind.bind(), this::toWarn);
         yield bind;
       }
       case Pattern.QualifiedRef qref -> {
@@ -64,13 +64,17 @@ public PatternResolver(@NotNull Context context, @NotNull Consumer<TyckUnit> par
         yield context.reportAndThrow(new NameProblem.QualifiedNameNotFoundError(qid.component(), qid.name(), pos));
       }
       case Pattern.As as -> {
-        context = context.bind(as.as());
+        context = context.bind(as.as(), this::toWarn);
         yield as;
       }
       default -> pat;
     };
   }
 
+  private boolean toWarn(@Nullable AnyVar var) {
+    return var instanceof LocalVar && !mercy.contains(var);
+  }
+
   private void addReference(@NotNull AnyDefVar defVar) {
     if (defVar instanceof DefVar<?, ?> fr) parentAdd.accept(fr.concrete);
   }

base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java

@@ -151,7 +151,7 @@ private static Reporter suppress(@NotNull Reporter reporter, @NotNull Decl decl)
     var r = new SuppressingReporter(reporter);
     decl.suppresses.forEach(suppress -> {
       switch (suppress) {
-        case Shadowing -> r.suppress(NameProblem.ShadowingWarn.class);
+        case LocalShadow -> r.suppress(NameProblem.ShadowingWarn.class);
       }
     });
     return r;

base/src/main/java/org/aya/resolve/visitor/StmtResolver.java

@@ -64,7 +64,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
             resolveElim(resolver, body.inner());
             var clausesResolver = resolver.deriveRestrictive();
             clausesResolver.reference().append(new TyckOrder.Head(decl));
-            decl.body = body.map(clausesResolver::clause);
+            decl.body = body.map(x -> clausesResolver.clause(decl.teleVars().toImmutableSeq(), x));
             addReferences(info, new TyckOrder.Body(decl), clausesResolver);
           }
           case FnBody.ExprBody(var expr) -> {
@@ -84,7 +84,9 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
           var mCtx = MutableValue.create(resolver.ctx());
           bodyResolver.reference().append(new TyckOrder.Head(data));
           bodyResolver.enter(Where.ConPattern);
-          con.patterns = con.patterns.map(pat -> pat.descent(pattern -> bodyResolver.resolvePattern(pattern, mCtx)));
+          con.patterns = con.patterns.map(pat ->
+            pat.descent(pattern ->
+              bodyResolver.resolvePattern(pattern, data.teleVars().toImmutableSeq(), mCtx)));
           bodyResolver.exit();
           resolveMemberSignature(con, bodyResolver, mCtx);
           addReferences(info, new TyckOrder.Head(con), bodyResolver);

cli-impl/src/test/java/org/aya/test/fixtures/ScopeError.java

@@ -90,4 +90,17 @@ def p (a : Bool) : Bool elim b
     open class Cls | A : Type
     def test (c : Cls) => c.B
     """;
+  @Language("Aya") String testLocalShadow = """
+    def test (A : Type) (a : A) : A =>
+      let | x : A := a
+          | x : A := a
+      in x
+    """;
+  @Language("Aya") String testLocalShadowSuppress = """
+    @suppress(LocalShadow)
+    def test (A : Type) (a : A) : A =>
+      let | x : A := a
+          | x : A := a
+      in x
+    """;
 }

cli-impl/src/test/resources/negative/ScopeError.txt

@@ -303,3 +303,18 @@ Resolving interrupted due to:
 1 error(s), 0 warning(s).
 Let's learn from that.
 
+LocalShadow:
+In file $FILE:3:8 ->
+
+  1 │   def test (A : Type) (a : A) : A =>
+  2 │     let | x : A := a
+  3 │         | x : A := a
+    │           ╰╯
+
+Warning: The name `x` shadows a previous local definition from outer scope
+
+That looks right!
+
+LocalShadowSuppress:
+That looks right!
+

cli-impl/src/test/resources/shared/src/data/list/base.aya

@@ -28,13 +28,11 @@ def rev' (buf xs : List A) : List A elim xs
 
 def rev (xs : List A) : List A => rev' [ ] xs
 
-@suppress(Shadowing)
 overlap def take (n : Nat) (xs : List A) : List A
 | _, [ ] => [ ]
 | 0, _ => [ ]
 | suc n, x :< xs => x :< (take n xs)
 
-@suppress(Shadowing)
 overlap def drop (n : Nat) (xs : List A) : List A
 | _, [ ] => [ ]
 | 0, _ => xs

cli-impl/src/test/resources/shared/src/data/list/properties.aya

@@ -29,19 +29,16 @@ def head-def (x : A) (xs : List A) : A elim xs
 | [ ] => x
 | a :< _ => a
 
-@suppress(Shadowing)
 def ++-assoc (xs ys zs : List A) : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) elim xs
 | [ ] => refl
 | x :< xs => pmap (x :<) (++-assoc xs ys zs)
 
-@suppress(Shadowing)
 private def rev'-map (f : A -> B) (buf xs : List A) : map f (rev' buf xs) = rev' (map f buf) (map f xs) elim xs
 | [ ] => refl
 | x :< xs => rev'-map f (x :< buf) xs
 
 def rev-map (f : A -> B) (xs : List A) : map f (rev xs) = rev (map f xs) => rev'-map f [ ] xs
 
-@suppress(Shadowing)
 private def rev'-++ (buf xs : List A) : rev' buf xs = rev xs ++ buf elim xs
 | [ ] => refl
 | x :< xs =>
@@ -51,7 +48,6 @@ private def rev'-++ (buf xs : List A) : rev' buf xs = rev xs ++ buf elim xs
   | step2 : (rev xs ++ [ x ]) ++ buf = rev xs ++ (x :< buf) := ++-assoc (rev xs) [ x ] buf
   in step0 <=> pinv step2 <=> pinv step1
 
-@suppress(Shadowing)
 def rev-distrib-++ (xs ys : List A) : rev (xs ++ ys) = (rev ys ++ rev xs) elim xs
 | [ ] => refl
 | x :< xs =>

cli-impl/src/test/resources/shared/src/data/vec/base.aya

@@ -1,6 +1,5 @@
 open import prelude hiding (++)
 
-@suppress(Shadowing)
 open inductive Vec (n : Nat) (A : Type) elim n
 | 0 => []
 | suc n => infixr :> A (Vec n A)

cli-impl/src/test/resources/shared/src/data/vec/properties.aya

@@ -13,7 +13,6 @@ def ++-assoc (xs : Vec n A) (ys : Vec m A) (zs : Vec o A)
 | [] => refl
 | x :> xs' => pmapd _ (\i => x :>) (++-assoc xs' ys zs)
 
-@suppress(Shadowing)
 def vmap-distrib-++ (f : A -> B) (xs : Vec n A) (ys : Vec m A) : vmap f (xs ++ ys) = vmap f xs ++ vmap f ys elim xs
 | [] => refl
 | x :> xs => pmap (f x :>) (vmap-distrib-++ f xs ys)

cli-impl/src/test/resources/shared/src/relation/binary/nat_cmp.aya

@@ -47,14 +47,13 @@ private def some-lemma {a b : Nat} (p : subTrunc a b = 0) (np : neg (subTrunc (s
 | suc a, 0 => exfalso (z≠s (pinv p))
 | suc a, suc b => pmap suc (some-lemma p np)
 
-@suppress(Shadowing)
+
 def <=-case {a b : Nat} (p : a <= b) : Sum (a < b) (a = b) =>
   match a <? b {
   | _ because reflect_true p => inl p
   | _ because reflect_false np => inr (some-lemma p np)
   }
 
-@suppress(Shadowing)
 def ¬<→>= {a b : Nat} (np : neg (a < b)) : a >= b
 | {_}, {0}, np => refl
 | {0}, {suc b}, np => exfalso (np refl)

syntax/src/main/java/org/aya/generic/Suppress.java

@@ -3,7 +3,7 @@
 package org.aya.generic;
 
 public enum Suppress {
-  Shadowing,
+  LocalShadow,
   UnimportedCon,
   UnreachableClause,
   MostGeneralSolution;