test: add fixtures for dt cases and stuff

aya-prover · Dec 12, 2024 · 5ade09f · 5ade09f
1 parent 2897f7b
commit 5ade09f
Show file tree

Hide file tree

Showing 3 changed files with 20 additions and 7 deletions.
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -440,11 +440,9 @@ case DepTypeTerm(var kind, var param, var body) when kind == DTKind.Sigma -> {
         // Type check the type annotation
         Term type;
         if (asBindings.isEmpty()) type = ty(returns);
-        else {
-          try (var ignored = subscope()) {
-            asBindings.forEachWith(wellArgs, (as, discr) -> localCtx().put(as, discr.type()));
-            type = ty(returns).bindTele(asBindings.view());
-          }
+        else try (var ignored = subscope()) {
+          asBindings.forEachWith(wellArgs, (as, discr) -> localCtx().put(as, discr.type()));
+          type = ty(returns).bindTele(asBindings.view());
         }
         yield new Jdg.Default(match(discriminant, expr.sourcePos(), clauses, wellArgs, type), type);
       }

diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya
@@ -69,3 +69,17 @@ module Issue1187 {
   def FunExt (f g : A -> B) (p : ∀ a -> f a = g a) => (fn a => f a) = g
   def FunExt' (f g : A -> B) (p : ∀ a -> f a = g a) => (fn a => f a) = (fn a => g a)
 }
+
+module Issue1194 {
+  def inheritMode (a : Nat) : Nat => match a { _ => 1 }
+  def synthMode (a : Nat) : Nat =>
+   match a returns Nat -> Nat { _ => fn x => x } 1
+
+  def depTy (a : Nat) (P : Nat -> Type)
+     (bc : P 0)
+     (ic : ∀ n -> P (suc n)) : P (a + a) =>
+   match a + a as x returns P x {
+    | 0 => bc
+    | suc n => ic n
+   }
+}
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -575,7 +575,8 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
       ImmutableSeq<LocalVar> asBindings = ImmutableSeq.empty();
       WithPos<Expr> returns = null;
       if (matchType != null) {
-        asBindings = matchType.child(COMMA_SEP).childrenOfType(WEAK_ID)
+        var commaSep = matchType.peekChild(COMMA_SEP);
+        if (commaSep != null) asBindings = commaSep.childrenOfType(WEAK_ID)
           .map(this::weakId)
           .map(LocalVar::from)
           .toImmutableSeq();
@@ -584,7 +585,7 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
             + discr.size() + " discriminant(s)"));
           throw new ParsingInterruptedException();
         }
-        var returnsNode = node.peekChild(EXPR);
+        var returnsNode = matchType.peekChild(EXPR);
         if (returnsNode != null) returns = expr(returnsNode);
       }
       return new WithPos<>(pos, new Expr.Match(