pat: better impl in case of ind-ind

Author: HoshinoTented

Diff for: base/src/main/java/org/aya/tyck/error/PatternProblem.java

@@ -129,6 +129,11 @@ record ImplicitDisallowed(@Override @NotNull WithPos<Pattern> pattern) implement
   record UnimportedConName(
     @Override @NotNull WithPos<Pattern.Bind> pattern
   ) implements PatternProblem {
+    @Override
+    public @NotNull Severity level() {
+      return Severity.WARN;
+    }
+
     @Override
     public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.vcat(

Diff for: base/src/main/java/org/aya/tyck/pat/PatternTycker.java

@@ -13,11 +13,12 @@
 import org.aya.generic.term.DTKind;
 import org.aya.normalize.Normalizer;
 import org.aya.syntax.compile.JitCon;
+import org.aya.syntax.compile.JitData;
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
+import org.aya.syntax.concrete.stmt.decl.DataDecl;
 import org.aya.syntax.core.Jdg;
-import org.aya.syntax.core.def.ConDef;
-import org.aya.syntax.core.def.ConDefLike;
+import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.pat.PatMatcher;
 import org.aya.syntax.core.pat.PatToTerm;
@@ -156,10 +157,10 @@ public record TyckResult(
 
         // report after tyRef.set, the error message requires it
         if (whnf(type) instanceof DataCall call) {
-          var unimportedCon = call.ref().body()
-            .filter(con -> con.name().equals(bind.name()));
+          var unimportedCon = collectConNames(call.ref())
+            .anyMatch(it -> it.equals(bind.name()));
 
-          if (unimportedCon.isNotEmpty()) {
+          if (unimportedCon) {
             fail(new PatternProblem.UnimportedConName(pattern.replace(bindPat)));
           }
         }
@@ -479,6 +480,17 @@ private record Selection(
     };
   }
 
+  private static @NotNull SeqView<String> collectConNames(@NotNull DataDefLike call) {
+    return switch (call) {
+      case JitData jitData -> jitData.body().view().map(AnyDef::name);
+      case DataDef.Delegate delegate -> {
+        // the core may be unchecked!
+        var concrete = (DataDecl) delegate.ref.concrete;
+        yield concrete.body.view().map(it -> it.ref.name());
+      }
+    };
+  }
+
   /**
    * Check whether {@param con} is available under {@param type}
    */