From 32258e5f4e55e91ae985592f7edd089464056141 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 14:39:41 -0500
Subject: [PATCH 1/7] misc: random improvements, add error handling

---
 base/src/main/java/org/aya/concrete/Expr.java          | 2 ++
 base/src/main/java/org/aya/tyck/unify/Synthesizer.java | 5 ++---
 cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java | 6 +++++-
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/base/src/main/java/org/aya/concrete/Expr.java b/base/src/main/java/org/aya/concrete/Expr.java
index df4d9ff87b..905ff7af5a 100644
--- a/base/src/main/java/org/aya/concrete/Expr.java
+++ b/base/src/main/java/org/aya/concrete/Expr.java
@@ -98,6 +98,8 @@ public Error(@NotNull SourcePos sourcePos, @NotNull Doc description) {
   }
 
   /**
+   * @param explicit whether the hole is a type-directed programming goal or
+   *                 a to-be-solved by tycking hole.
    * @author ice1000
    */
   record Hole(
diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java
index 71c18531df..c679fdd46e 100644
--- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java
+++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java
@@ -62,7 +62,7 @@ public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) {
    */
   public @Nullable Term synthesize(@NotNull Term preterm) {
     return switch (preterm) {
-      case RefTerm term -> ctx.get(term.var());
+      case RefTerm(var var) -> ctx.get(var);
       case ConCall conCall -> conCall.head().underlyingDataCall();
       case Callable.DefCall call -> Def.defResult(call.ref())
         .subst(DeltaExpander.buildSubst(Def.defTele(call.ref()), call.args()))
@@ -72,8 +72,7 @@ public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) {
         if (result == null) {
           preterm = whnf(preterm);
           yield preterm instanceof MetaTerm ? null : synthesize(preterm);
-        }
-        else yield result;
+        } else yield result;
       }
       case RefTerm.Field field -> Def.defType(field.ref());
       case FieldTerm access -> {
diff --git a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
index 4825894935..0d3129b734 100644
--- a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
+++ b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.cli.parse;
 
@@ -6,6 +6,7 @@
 import com.intellij.openapi.util.TextRange;
 import com.intellij.openapi.util.text.LineColumn;
 import com.intellij.openapi.util.text.StringUtil;
+import com.intellij.psi.TokenType;
 import com.intellij.psi.tree.IElementType;
 import com.intellij.psi.tree.TokenSet;
 import kala.collection.SeqView;
@@ -506,6 +507,9 @@ private interface LicitParser<T> extends BooleanObjBiFunction<GenericNode<?>, T>
 
   public @NotNull Expr expr(@NotNull GenericNode<?> node) {
     var pos = sourcePosOf(node);
+    if (node.is(TokenType.ERROR_ELEMENT)) {
+      return new Expr.Hole(pos, true, null);
+    }
     if (node.is(REF_EXPR)) {
       var qid = qualifiedId(node.child(QUALIFIED_ID));
       return new Expr.Unresolved(qid.sourcePos(), qid);

From de9750c53a33aa1023744c583d54fbb39e9bb2a7 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 14:59:31 -0500
Subject: [PATCH 2/7] parser: delete some unused code

---
 .../java/org/aya/concrete/error/ParseError.java  |  6 +++---
 .../java/org/aya/cli/parse/AyaGKProducer.java    | 14 +++++++++-----
 .../gen/org/aya/parser/AyaPsiElementTypes.java   |  4 +++-
 .../main/gen/org/aya/parser/AyaPsiParser.java    | 16 +++-------------
 parser/src/main/grammar/AyaPsiParser.bnf         |  4 +---
 5 files changed, 19 insertions(+), 25 deletions(-)

diff --git a/base/src/main/java/org/aya/concrete/error/ParseError.java b/base/src/main/java/org/aya/concrete/error/ParseError.java
index 4f6103de2e..2bae06ab6a 100644
--- a/base/src/main/java/org/aya/concrete/error/ParseError.java
+++ b/base/src/main/java/org/aya/concrete/error/ParseError.java
@@ -1,16 +1,16 @@
-// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.concrete.error;
 
 import org.aya.pretty.doc.Doc;
-import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
 import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.NotNull;
 
 public record ParseError(@Override @NotNull SourcePos sourcePos, @NotNull String message) implements Problem {
   @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
-    return Doc.plain("Parser error: " + message);
+    return Doc.english("Parser error: " + message);
   }
 
   @Override public @NotNull Severity level() {
diff --git a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
index 0d3129b734..d7cb8844de 100644
--- a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
+++ b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
@@ -6,7 +6,6 @@
 import com.intellij.openapi.util.TextRange;
 import com.intellij.openapi.util.text.LineColumn;
 import com.intellij.openapi.util.text.StringUtil;
-import com.intellij.psi.TokenType;
 import com.intellij.psi.tree.IElementType;
 import com.intellij.psi.tree.TokenSet;
 import kala.collection.SeqView;
@@ -507,9 +506,9 @@ private interface LicitParser<T> extends BooleanObjBiFunction<GenericNode<?>, T>
 
   public @NotNull Expr expr(@NotNull GenericNode<?> node) {
     var pos = sourcePosOf(node);
-    if (node.is(TokenType.ERROR_ELEMENT)) {
-      return new Expr.Hole(pos, true, null);
-    }
+    // if (node.is(TokenType.ERROR_ELEMENT)) {
+    //   return new Expr.Hole(pos, true, null);
+    // }
     if (node.is(REF_EXPR)) {
       var qid = qualifiedId(node.child(QUALIFIED_ID));
       return new Expr.Unresolved(qid.sourcePos(), qid);
@@ -854,7 +853,12 @@ private Arg<Pattern> unitPattern(@NotNull GenericNode<?> node) {
 
   public @Nullable Expr typeOrNull(@Nullable GenericNode<?> node) {
     if (node == null) return null;
-    return expr(node.child(EXPR));
+    var child = node.peekChild(EXPR);
+    if (child == null) {
+      reporter.report(new ParseError(sourcePosOf(node), "Expected the return type expression"));
+      return null;
+    }
+    return expr(child);
   }
 
   public @NotNull Expr typeOrHole(@Nullable GenericNode<?> node, SourcePos sourcePos) {
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
index 1a49485dcd..a6294606ff 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
@@ -1,3 +1,6 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+
 // This is a generated file. Not intended for manual editing.
 package org.aya.parser;
 
@@ -85,7 +88,6 @@ public interface AyaPsiElementTypes {
   IElementType PROJ_FIX_ID = new AyaPsiElementType("PROJ_FIX_ID");
   IElementType QUALIFIED_ID = new AyaPsiElementType("QUALIFIED_ID");
   IElementType REF_EXPR = new AyaPsiElementType("REF_EXPR");
-  IElementType SAMPLE_MODIFIERS = new AyaPsiElementType("SAMPLE_MODIFIERS");
   IElementType SIGMA_EXPR = new AyaPsiElementType("SIGMA_EXPR");
   IElementType STMT = new AyaPsiElementType("STMT");
   IElementType STRUCT_DECL = new AyaPsiElementType("STRUCT_DECL");
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
index 64da8b5184..fc82de9d69 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
@@ -1,3 +1,6 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+
 // This is a generated file. Not intended for manual editing.
 package org.aya.parser;
 
@@ -1623,19 +1626,6 @@ private static boolean repl_0(PsiBuilder b, int l) {
     return true;
   }
 
-  /* ********************************************************** */
-  // KW_EXAMPLE | KW_COUNTEREXAMPLE
-  public static boolean sampleModifiers(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "sampleModifiers")) return false;
-    if (!nextTokenIs(b, "<sample modifiers>", KW_COUNTEREXAMPLE, KW_EXAMPLE)) return false;
-    boolean r;
-    Marker m = enter_section_(b, l, _NONE_, SAMPLE_MODIFIERS, "<sample modifiers>");
-    r = consumeToken(b, KW_EXAMPLE);
-    if (!r) r = consumeToken(b, KW_COUNTEREXAMPLE);
-    exit_section_(b, l, m, r, false, null);
-    return r;
-  }
-
   /* ********************************************************** */
   // decl
   //        | importCmd
diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf
index f9a73c32a6..c8577964b8 100644
--- a/parser/src/main/grammar/AyaPsiParser.bnf
+++ b/parser/src/main/grammar/AyaPsiParser.bnf
@@ -1,5 +1,5 @@
 /*
- * Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+ * Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
  * Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
  */
 
@@ -191,8 +191,6 @@ generalize ::= KW_VARIABLE generalizeParamName+ type
 
 // declarations
 
-sampleModifiers ::= KW_EXAMPLE | KW_COUNTEREXAMPLE
-
 decl ::= fnDecl | primDecl | structDecl | dataDecl {
   mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl"
   implements="org.aya.intellij.psi.AyaPsiGenericDecl"

From ab2e0db3a57be1cc9674717fa592f542e940de50 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 15:08:15 -0500
Subject: [PATCH 3/7] parser: mutable

---
 .../java/org/aya/cli/parse/AyaGKProducer.java | 44 +++++++++----------
 1 file changed, 22 insertions(+), 22 deletions(-)

diff --git a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
index d7cb8844de..c11f447ed5 100644
--- a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
+++ b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
@@ -10,6 +10,7 @@
 import com.intellij.psi.tree.TokenSet;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableSinglyLinkedList;
 import kala.control.Either;
 import kala.control.Option;
@@ -95,10 +96,11 @@ public record AyaGKProducer(
     if (node.is(MODULE)) return ImmutableSeq.of(module(node));
     if (node.is(OPEN_CMD)) return openCmd(node);
     if (node.is(DECL)) {
-      var result = decl(node);
-      var stmts = result.component2().view().prepended(result.component1());
-      if (result.component1() instanceof Decl.TopLevel top && top.personality() == Decl.Personality.COUNTEREXAMPLE) {
-        result.component2().firstOption(stmt -> !(stmt instanceof Decl))
+      var stmts = MutableList.<Stmt>create();
+      var result = decl(node, stmts);
+      stmts.prepend(result);
+      if (result instanceof Decl.TopLevel top && top.personality() == Decl.Personality.COUNTEREXAMPLE) {
+        stmts.firstOption(stmt -> !(stmt instanceof Decl))
           .ifDefined(stmt -> reporter.report(new BadCounterexampleWarn(stmt)));
         return stmts.<Stmt>filterIsInstance(Decl.class).toImmutableSeq();
       }
@@ -222,11 +224,11 @@ public SeqView<UseHide.Name> useIdsComma(@NotNull GenericNode<?> node) {
       node.childrenOfType(STMT).flatMap(this::stmt).toImmutableSeq());
   }
 
-  public Tuple2<? extends Decl, ImmutableSeq<Stmt>> decl(@NotNull GenericNode<?> node) {
-    if (node.is(FN_DECL)) return Tuple.of(fnDecl(node), ImmutableSeq.empty());
-    if (node.is(PRIM_DECL)) return Tuple.of(primDecl(node), ImmutableSeq.empty());
-    if (node.is(DATA_DECL)) return dataDecl(node);
-    if (node.is(STRUCT_DECL)) return structDecl(node);
+  public Decl decl(@NotNull GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
+    if (node.is(FN_DECL)) return fnDecl(node);
+    if (node.is(PRIM_DECL)) return primDecl(node);
+    if (node.is(DATA_DECL)) return dataDecl(node, additional);
+    if (node.is(STRUCT_DECL)) return structDecl(node, additional);
     return unreachable(node);
   }
 
@@ -299,10 +301,10 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
     return Either.right(node.childrenOfType(BARRED_CLAUSE).map(this::bareOrBarredClause).toImmutableSeq());
   }
 
-  private @NotNull ImmutableSeq<Stmt> giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl) {
-    if (!modiSet.isReExport().data()) return ImmutableSeq.empty();
+  private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl, @NotNull MutableList<Stmt> additional) {
+    if (!modiSet.isReExport().data()) return;
 
-    return ImmutableSeq.of(new Command.Open(
+    additional.append(new Command.Open(
       modiSet.isReExport().sourcePos(),
       modiSet.accessibility().data(),
       new QualifiedID(decl.sourcePos(), decl.ref().name()),
@@ -312,8 +314,7 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
     ));
   }
 
-  public @NotNull Tuple2<TeleDecl.DataDecl, ImmutableSeq<Stmt>>
-  dataDecl(GenericNode<?> node) {
+  public @NotNull TeleDecl.DataDecl dataDecl(GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
     var modifier = moduleLikeDeclModifiersOf(node);
     var acc = modifier.accessibility().data();
     var sample = modifier.personality().data();
@@ -335,7 +336,8 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
       sample
     );
 
-    return Tuple.of(decl, giveMeOpen(modifier, decl));
+    giveMeOpen(modifier, decl, additional);
+    return decl;
   }
 
   public @NotNull TeleDecl.DataCtor dataBody(@NotNull GenericNode<?> node) {
@@ -350,7 +352,7 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
     return dataCtor(patterns(node.child(PATTERNS).child(COMMA_SEP)), node.child(DATA_CTOR));
   }
 
-  public @NotNull Tuple2<TeleDecl.StructDecl, ImmutableSeq<Stmt>> structDecl(@NotNull GenericNode<?> node) {
+  public @NotNull TeleDecl.StructDecl structDecl(@NotNull GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
     var modifier = moduleLikeDeclModifiersOf(node);
     var acc = modifier.accessibility().data();
     var sample = modifier.personality().data();
@@ -370,7 +372,8 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
       bind == null ? BindBlock.EMPTY : bindBlock(bind),
       sample
     );
-    return Tuple.of(decl, giveMeOpen(modifier, decl));
+    giveMeOpen(modifier, decl, additional);
+    return decl;
   }
 
   public @NotNull TeleDecl.StructField structField(GenericNode<?> node) {
@@ -391,7 +394,8 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
   }
 
   public @NotNull TeleDecl.PrimDecl primDecl(@NotNull GenericNode<?> node) {
-    var id = primName(node.child(PRIM_NAME));
+    var nameEl = node.child(PRIM_NAME);
+    var id = weakId(nameEl.child(WEAK_ID));
     return new TeleDecl.PrimDecl(
       id.sourcePos(),
       sourcePosOf(node),
@@ -879,10 +883,6 @@ private Arg<Pattern> unitPattern(@NotNull GenericNode<?> node) {
     return weakId(node.child(WEAK_ID));
   }
 
-  public @NotNull WithPos<String> primName(@NotNull GenericNode<?> node) {
-    return weakId(node.child(WEAK_ID));
-  }
-
   public @NotNull WithPos<String> newArgField(@NotNull GenericNode<?> node) {
     return weakId(node.child(WEAK_ID));
   }

From e323ef10461fd5eeed3c40a604b531673a688743 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 15:19:05 -0500
Subject: [PATCH 4/7] parser: add some pins

---
 .../java/org/aya/cli/parse/AyaGKProducer.java | 54 ++++++++++-----
 .../main/gen/org/aya/parser/AyaPsiParser.java | 68 +++++++++++--------
 parser/src/main/grammar/AyaPsiParser.bnf      | 15 ++--
 3 files changed, 85 insertions(+), 52 deletions(-)

diff --git a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
index c11f447ed5..1e3f31bf97 100644
--- a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
+++ b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
@@ -98,7 +98,7 @@ public record AyaGKProducer(
     if (node.is(DECL)) {
       var stmts = MutableList.<Stmt>create();
       var result = decl(node, stmts);
-      stmts.prepend(result);
+      if (result != null) stmts.prepend(result);
       if (result instanceof Decl.TopLevel top && top.personality() == Decl.Personality.COUNTEREXAMPLE) {
         stmts.firstOption(stmt -> !(stmt instanceof Decl))
           .ifDefined(stmt -> reporter.report(new BadCounterexampleWarn(stmt)));
@@ -224,7 +224,7 @@ public SeqView<UseHide.Name> useIdsComma(@NotNull GenericNode<?> node) {
       node.childrenOfType(STMT).flatMap(this::stmt).toImmutableSeq());
   }
 
-  public Decl decl(@NotNull GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
+  public @Nullable Decl decl(@NotNull GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
     if (node.is(FN_DECL)) return fnDecl(node);
     if (node.is(PRIM_DECL)) return primDecl(node);
     if (node.is(DATA_DECL)) return dataDecl(node, additional);
@@ -258,7 +258,16 @@ public Decl decl(@NotNull GenericNode<?> node, @NotNull MutableList<Stmt> additi
     return declModifiersOf(node, x -> true);
   }
 
-  public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
+  public @Nullable TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
+    var entire = sourcePosOf(node);
+    var nameOrInfix = declNameOrInfix(node.peekChild(DECL_NAME_OR_INFIX));
+    if (nameOrInfix == null) {
+      reporter.report(new ParseError(entire, "Expect function name"));
+      return null;
+    }
+    var fnBodyNode = node.peekChild(FN_BODY);
+    if (fnBodyNode == null) return null;
+
     var modifier = commonDeclModifiersOf(node);
     var acc = modifier.accessibility().data();
     var sample = modifier.personality().data();
@@ -272,16 +281,15 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
     }
     var tele = telescope(node.childrenOfType(TELE).map(x -> x)); // make compiler happy
     var bind = node.peekChild(BIND_BLOCK);
-    var nameOrInfix = declNameOrInfix(node.child(DECL_NAME_OR_INFIX));
 
-    var dynamite = fnBody(node.child(FN_BODY));
+    var dynamite = fnBody(fnBodyNode);
     if (dynamite.isRight() && inline.isDefined()) {
       var gelatin = inline.get();
       reporter.report(new BadModifierWarn(sourcePosOf(gelatin.component1()), gelatin.component2()));
     }
     return new TeleDecl.FnDecl(
       nameOrInfix.component1().sourcePos(),
-      sourcePosOf(node),
+      entire,
       sample == Decl.Personality.NORMAL ? acc : Stmt.Accessibility.Private,
       modifiers.map(Tuple2::getValue).collect(Collectors.toCollection(
         () -> EnumSet.noneOf(Modifier.class))),
@@ -314,15 +322,19 @@ private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl,
     ));
   }
 
-  public @NotNull TeleDecl.DataDecl dataDecl(GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
+  public @Nullable TeleDecl.DataDecl dataDecl(GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
+    var entire = sourcePosOf(node);
+    var nameOrInfix = declNameOrInfix(node.peekChild(DECL_NAME_OR_INFIX));
+    if (nameOrInfix == null) {
+      reporter.report(new ParseError(entire, "Expect data's name"));
+      return null;
+    }
     var modifier = moduleLikeDeclModifiersOf(node);
     var acc = modifier.accessibility().data();
     var sample = modifier.personality().data();
     var bind = node.peekChild(BIND_BLOCK);
-    var body = node.childrenOfType(DATA_BODY).map(this::dataBody).toImmutableSeq();
+    var body = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq();
     var tele = telescope(node.childrenOfType(TELE).map(x -> x));
-    var nameOrInfix = declNameOrInfix(node.child(DECL_NAME_OR_INFIX));
-    var entire = sourcePosOf(node);
     var decl = new TeleDecl.DataDecl(
       nameOrInfix.component1().sourcePos(),
       entire,
@@ -340,12 +352,13 @@ private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl,
     return decl;
   }
 
-  public @NotNull TeleDecl.DataCtor dataBody(@NotNull GenericNode<?> node) {
+  public @Nullable TeleDecl.DataCtor dataBody(@NotNull GenericNode<?> node) {
     var dataCtorClause = node.peekChild(DATA_CTOR_CLAUSE);
     if (dataCtorClause != null) return dataCtorClause(dataCtorClause);
     var dataCtor = node.peekChild(DATA_CTOR);
     if (dataCtor != null) return dataCtor(ImmutableSeq.empty(), dataCtor);
-    return unreachable(node);
+    reporter.report(new ParseError(sourcePosOf(node), "Expect a data constructor"));
+    return null;
   }
 
   public @NotNull TeleDecl.DataCtor dataCtorClause(@NotNull GenericNode<?> node) {
@@ -393,12 +406,17 @@ private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl,
     );
   }
 
-  public @NotNull TeleDecl.PrimDecl primDecl(@NotNull GenericNode<?> node) {
-    var nameEl = node.child(PRIM_NAME);
+  public @Nullable TeleDecl.PrimDecl primDecl(@NotNull GenericNode<?> node) {
+    var nameEl = node.peekChild(PRIM_NAME);
+    var entire = sourcePosOf(node);
+    if (nameEl == null) {
+      reporter.report(new ParseError(entire, "Expect a primitive's name"));
+      return null;
+    }
     var id = weakId(nameEl.child(WEAK_ID));
     return new TeleDecl.PrimDecl(
       id.sourcePos(),
-      sourcePosOf(node),
+      entire,
       id.data(),
       telescope(node.childrenOfType(TELE).map(x -> x)),
       typeOrNull(node.peekChild(TYPE))
@@ -500,7 +518,9 @@ private interface LicitParser<T> extends BooleanObjBiFunction<GenericNode<?>, T>
       LocalVar.from(teleParamName(node)), typeOrHole(null, pos), explicit));
   }
 
-  public Tuple2<@NotNull WithPos<String>, OpDecl.@Nullable OpInfo> declNameOrInfix(@NotNull GenericNode<?> node) {
+  public @Nullable Tuple2<@NotNull WithPos<String>, OpDecl.@Nullable OpInfo>
+  declNameOrInfix(@Nullable GenericNode<?> node) {
+    if (node == null) return null;
     var assoc = node.peekChild(ASSOC);
     var id = weakId(node.child(WEAK_ID));
     if (assoc == null) return Tuple.of(id, null);
@@ -859,7 +879,7 @@ private Arg<Pattern> unitPattern(@NotNull GenericNode<?> node) {
     if (node == null) return null;
     var child = node.peekChild(EXPR);
     if (child == null) {
-      reporter.report(new ParseError(sourcePosOf(node), "Expected the return type expression"));
+      reporter.report(new ParseError(sourcePosOf(node), "Expect the return type expression"));
       return null;
     }
     return expr(child);
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
index fc82de9d69..96e5f6e95b 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
@@ -439,12 +439,13 @@ private static boolean commaSep_1_0(PsiBuilder b, int l, Parser _param) {
   public static boolean dataBody(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "dataBody")) return false;
     if (!nextTokenIs(b, BAR)) return false;
-    boolean r;
-    Marker m = enter_section_(b);
+    boolean r, p;
+    Marker m = enter_section_(b, l, _NONE_, DATA_BODY, null);
     r = consumeToken(b, BAR);
+    p = r; // pin = 1
     r = r && dataBody_1(b, l + 1);
-    exit_section_(b, m, DATA_BODY, r);
-    return r;
+    exit_section_(b, l, m, r, p, null);
+    return r || p;
   }
 
   // dataCtorClause | dataCtor
@@ -525,20 +526,23 @@ public static boolean dataCtorClause(PsiBuilder b, int l) {
   }
 
   /* ********************************************************** */
-  // declModifiers* KW_DATA declNameOrInfix tele* type? dataBody* bindBlock?
+  // declModifiers*
+  //  KW_DATA declNameOrInfix
+  //  tele* type? dataBody* bindBlock?
   public static boolean dataDecl(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "dataDecl")) return false;
-    boolean r;
+    boolean r, p;
     Marker m = enter_section_(b, l, _NONE_, DATA_DECL, "<data decl>");
     r = dataDecl_0(b, l + 1);
     r = r && consumeToken(b, KW_DATA);
-    r = r && declNameOrInfix(b, l + 1);
-    r = r && dataDecl_3(b, l + 1);
-    r = r && dataDecl_4(b, l + 1);
-    r = r && dataDecl_5(b, l + 1);
-    r = r && dataDecl_6(b, l + 1);
-    exit_section_(b, l, m, r, false, null);
-    return r;
+    p = r; // pin = 2
+    r = r && report_error_(b, declNameOrInfix(b, l + 1));
+    r = p && report_error_(b, dataDecl_3(b, l + 1)) && r;
+    r = p && report_error_(b, dataDecl_4(b, l + 1)) && r;
+    r = p && report_error_(b, dataDecl_5(b, l + 1)) && r;
+    r = p && dataDecl_6(b, l + 1) && r;
+    exit_section_(b, l, m, r, p, null);
+    return r || p;
   }
 
   // declModifiers*
@@ -707,21 +711,24 @@ private static boolean fnBody_1(PsiBuilder b, int l) {
   }
 
   /* ********************************************************** */
-  // declModifiers* KW_DEF fnModifiers* declNameOrInfix tele* type? fnBody bindBlock?
+  // declModifiers*
+  //  KW_DEF fnModifiers* declNameOrInfix
+  //  tele* type? fnBody bindBlock?
   public static boolean fnDecl(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "fnDecl")) return false;
-    boolean r;
+    boolean r, p;
     Marker m = enter_section_(b, l, _NONE_, FN_DECL, "<fn decl>");
     r = fnDecl_0(b, l + 1);
     r = r && consumeToken(b, KW_DEF);
-    r = r && fnDecl_2(b, l + 1);
-    r = r && declNameOrInfix(b, l + 1);
-    r = r && fnDecl_4(b, l + 1);
-    r = r && fnDecl_5(b, l + 1);
-    r = r && fnBody(b, l + 1);
-    r = r && fnDecl_7(b, l + 1);
-    exit_section_(b, l, m, r, false, null);
-    return r;
+    p = r; // pin = 2
+    r = r && report_error_(b, fnDecl_2(b, l + 1));
+    r = p && report_error_(b, declNameOrInfix(b, l + 1)) && r;
+    r = p && report_error_(b, fnDecl_4(b, l + 1)) && r;
+    r = p && report_error_(b, fnDecl_5(b, l + 1)) && r;
+    r = p && report_error_(b, fnBody(b, l + 1)) && r;
+    r = p && fnDecl_7(b, l + 1) && r;
+    exit_section_(b, l, m, r, p, null);
+    return r || p;
   }
 
   // declModifiers*
@@ -1437,14 +1444,15 @@ public static boolean patterns(PsiBuilder b, int l) {
   public static boolean primDecl(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "primDecl")) return false;
     if (!nextTokenIs(b, KW_PRIM)) return false;
-    boolean r;
-    Marker m = enter_section_(b);
+    boolean r, p;
+    Marker m = enter_section_(b, l, _NONE_, PRIM_DECL, null);
     r = consumeToken(b, KW_PRIM);
-    r = r && primName(b, l + 1);
-    r = r && primDecl_2(b, l + 1);
-    r = r && primDecl_3(b, l + 1);
-    exit_section_(b, m, PRIM_DECL, r);
-    return r;
+    p = r; // pin = 1
+    r = r && report_error_(b, primName(b, l + 1));
+    r = p && report_error_(b, primDecl_2(b, l + 1)) && r;
+    r = p && primDecl_3(b, l + 1) && r;
+    exit_section_(b, l, m, r, p, null);
+    return r || p;
   }
 
   // tele*
diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf
index c8577964b8..40137185e1 100644
--- a/parser/src/main/grammar/AyaPsiParser.bnf
+++ b/parser/src/main/grammar/AyaPsiParser.bnf
@@ -159,7 +159,7 @@
 program ::= repl | stmts
 private stmts ::= stmt_with_recover*
 private stmt_with_recover ::= !(<<eof>>) stmt {
-  pin = 1
+  pin=1
   recoverWhile = stmt_recover
 }
 private stmt_recover ::= !(stmt_first)
@@ -204,7 +204,9 @@ bindBlock ::= (tighters | loosers)+
 tighters ::= KW_TIGHTER qualifiedId+
 loosers ::= KW_LOOSER qualifiedId+
 
-fnDecl ::= declModifiers* KW_DEF fnModifiers* declNameOrInfix tele* type? fnBody bindBlock?
+fnDecl ::= declModifiers*
+ KW_DEF fnModifiers* declNameOrInfix
+ tele* type? fnBody bindBlock? { pin=2 }
 
 fnBody ::= IMPLIES expr
          | barredClause*
@@ -221,7 +223,7 @@ openKw ::= KW_OPEN
 // This rule is used for convenience in semantic highlight.
 // see: SemanticHighlight, AyaGenericDeclImpl, AyaRunLineMarkerContributor
 primName ::= weakId
-primDecl ::= KW_PRIM primName tele* type?
+primDecl ::= KW_PRIM primName tele* type? { pin=1 }
 
 declModifiers ::= KW_PRIVATE | openKw | KW_EXAMPLE | KW_COUNTEREXAMPLE
 
@@ -237,11 +239,14 @@ structField
   implements="org.aya.intellij.psi.AyaPsiGenericDecl"
 }
 
-dataDecl ::= declModifiers* KW_DATA declNameOrInfix tele* type? dataBody* bindBlock?
+dataDecl ::= declModifiers*
+ KW_DATA declNameOrInfix
+ tele* type? dataBody* bindBlock? { pin=2 }
 
 dataBody ::= BAR (dataCtorClause | dataCtor) {
   mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl"
   implements="org.aya.intellij.psi.AyaPsiGenericDecl"
+  pin=1
 }
 
 dataCtor ::= KW_COERCE? declNameOrInfix tele* type? partialBlock? bindBlock?
@@ -395,7 +400,7 @@ pathTele ::= teleParamName
 // utilities
 private exprList ::= <<commaSep expr>>
 barred ::= expr BAR
-type ::= COLON expr { pin = 1 }
+type ::= COLON expr { pin=1 }
 doBinding ::= weakId LARROW expr {
   mixin="org.aya.intellij.psi.impl.AyaPsiNamedWeakIdImpl"
   implements="org.aya.intellij.psi.AyaPsiNamedWeakId"

From 3f0f8c8735db440fd01ba31e63740fd94d2a12f1 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 15:27:12 -0500
Subject: [PATCH 5/7] parser: add more pins

---
 .../org/aya/concrete/error/ParseError.java    |  2 +-
 .../java/org/aya/cli/parse/AyaGKProducer.java | 35 ++++++++++++-------
 .../main/gen/org/aya/parser/AyaPsiParser.java | 29 ++++++++-------
 parser/src/main/grammar/AyaPsiParser.bnf      |  3 +-
 4 files changed, 42 insertions(+), 27 deletions(-)

diff --git a/base/src/main/java/org/aya/concrete/error/ParseError.java b/base/src/main/java/org/aya/concrete/error/ParseError.java
index 2bae06ab6a..7fe45048fa 100644
--- a/base/src/main/java/org/aya/concrete/error/ParseError.java
+++ b/base/src/main/java/org/aya/concrete/error/ParseError.java
@@ -10,7 +10,7 @@
 
 public record ParseError(@Override @NotNull SourcePos sourcePos, @NotNull String message) implements Problem {
   @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
-    return Doc.english("Parser error: " + message);
+    return Doc.english(message);
   }
 
   @Override public @NotNull Severity level() {
diff --git a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
index 1e3f31bf97..f23de14244 100644
--- a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
+++ b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java
@@ -259,14 +259,16 @@ public SeqView<UseHide.Name> useIdsComma(@NotNull GenericNode<?> node) {
   }
 
   public @Nullable TeleDecl.FnDecl fnDecl(@NotNull GenericNode<?> node) {
-    var entire = sourcePosOf(node);
     var nameOrInfix = declNameOrInfix(node.peekChild(DECL_NAME_OR_INFIX));
     if (nameOrInfix == null) {
-      reporter.report(new ParseError(entire, "Expect function name"));
+      error(node.childrenView().first(), "Expect a function name");
       return null;
     }
     var fnBodyNode = node.peekChild(FN_BODY);
-    if (fnBodyNode == null) return null;
+    if (fnBodyNode == null) {
+      error(node.childrenView().first(), "Expect a function body");
+      return null;
+    }
 
     var modifier = commonDeclModifiersOf(node);
     var acc = modifier.accessibility().data();
@@ -283,13 +285,14 @@ public SeqView<UseHide.Name> useIdsComma(@NotNull GenericNode<?> node) {
     var bind = node.peekChild(BIND_BLOCK);
 
     var dynamite = fnBody(fnBodyNode);
+    if (dynamite == null) return null;
     if (dynamite.isRight() && inline.isDefined()) {
       var gelatin = inline.get();
       reporter.report(new BadModifierWarn(sourcePosOf(gelatin.component1()), gelatin.component2()));
     }
     return new TeleDecl.FnDecl(
       nameOrInfix.component1().sourcePos(),
-      entire,
+      sourcePosOf(node),
       sample == Decl.Personality.NORMAL ? acc : Stmt.Accessibility.Private,
       modifiers.map(Tuple2::getValue).collect(Collectors.toCollection(
         () -> EnumSet.noneOf(Modifier.class))),
@@ -303,8 +306,14 @@ public SeqView<UseHide.Name> useIdsComma(@NotNull GenericNode<?> node) {
     );
   }
 
-  public @NotNull Either<Expr, ImmutableSeq<Pattern.Clause>> fnBody(@NotNull GenericNode<?> node) {
+  public @Nullable Either<Expr, ImmutableSeq<Pattern.Clause>>
+  fnBody(@NotNull GenericNode<?> node) {
     var expr = node.peekChild(EXPR);
+    var implies = node.peekChild(IMPLIES);
+    if (expr == null && implies != null) {
+      error(implies, "Expect function body");
+      return null;
+    }
     if (expr != null) return Either.left(expr(expr));
     return Either.right(node.childrenOfType(BARRED_CLAUSE).map(this::bareOrBarredClause).toImmutableSeq());
   }
@@ -323,10 +332,9 @@ private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl,
   }
 
   public @Nullable TeleDecl.DataDecl dataDecl(GenericNode<?> node, @NotNull MutableList<Stmt> additional) {
-    var entire = sourcePosOf(node);
     var nameOrInfix = declNameOrInfix(node.peekChild(DECL_NAME_OR_INFIX));
     if (nameOrInfix == null) {
-      reporter.report(new ParseError(entire, "Expect data's name"));
+      error(node.childrenView().first(), "Expect a data name");
       return null;
     }
     var modifier = moduleLikeDeclModifiersOf(node);
@@ -337,7 +345,7 @@ private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl,
     var tele = telescope(node.childrenOfType(TELE).map(x -> x));
     var decl = new TeleDecl.DataDecl(
       nameOrInfix.component1().sourcePos(),
-      entire,
+      sourcePosOf(node),
       sample == Decl.Personality.NORMAL ? acc : Stmt.Accessibility.Private,
       nameOrInfix.component2(),
       nameOrInfix.component1().data(),
@@ -357,7 +365,7 @@ private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl,
     if (dataCtorClause != null) return dataCtorClause(dataCtorClause);
     var dataCtor = node.peekChild(DATA_CTOR);
     if (dataCtor != null) return dataCtor(ImmutableSeq.empty(), dataCtor);
-    reporter.report(new ParseError(sourcePosOf(node), "Expect a data constructor"));
+    error(node.childrenView().first(), "Expect a data constructor");
     return null;
   }
 
@@ -406,17 +414,20 @@ private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl<?> decl,
     );
   }
 
+  private void error(@NotNull GenericNode<?> node, @NotNull String message) {
+    reporter.report(new ParseError(sourcePosOf(node), message));
+  }
+
   public @Nullable TeleDecl.PrimDecl primDecl(@NotNull GenericNode<?> node) {
     var nameEl = node.peekChild(PRIM_NAME);
-    var entire = sourcePosOf(node);
     if (nameEl == null) {
-      reporter.report(new ParseError(entire, "Expect a primitive's name"));
+      error(node.childrenView().first(), "Expect a primitive's name");
       return null;
     }
     var id = weakId(nameEl.child(WEAK_ID));
     return new TeleDecl.PrimDecl(
       id.sourcePos(),
-      entire,
+      sourcePosOf(node),
       id.data(),
       telescope(node.childrenOfType(TELE).map(x -> x)),
       typeOrNull(node.peekChild(TYPE))
diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
index 96e5f6e95b..c0606b7383 100644
--- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
+++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
@@ -676,29 +676,18 @@ static boolean exprList(PsiBuilder b, int l) {
   }
 
   /* ********************************************************** */
-  // IMPLIES expr
+  // simpleBody
   //          | barredClause*
   public static boolean fnBody(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "fnBody")) return false;
     boolean r;
     Marker m = enter_section_(b, l, _NONE_, FN_BODY, "<fn body>");
-    r = fnBody_0(b, l + 1);
+    r = simpleBody(b, l + 1);
     if (!r) r = fnBody_1(b, l + 1);
     exit_section_(b, l, m, r, false, null);
     return r;
   }
 
-  // IMPLIES expr
-  private static boolean fnBody_0(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "fnBody_0")) return false;
-    boolean r;
-    Marker m = enter_section_(b);
-    r = consumeToken(b, IMPLIES);
-    r = r && expr(b, l + 1, -1);
-    exit_section_(b, m, null, r);
-    return r;
-  }
-
   // barredClause*
   private static boolean fnBody_1(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "fnBody_1")) return false;
@@ -1634,6 +1623,20 @@ private static boolean repl_0(PsiBuilder b, int l) {
     return true;
   }
 
+  /* ********************************************************** */
+  // IMPLIES expr
+  static boolean simpleBody(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "simpleBody")) return false;
+    if (!nextTokenIs(b, IMPLIES)) return false;
+    boolean r, p;
+    Marker m = enter_section_(b, l, _NONE_);
+    r = consumeToken(b, IMPLIES);
+    p = r; // pin = 1
+    r = r && expr(b, l + 1, -1);
+    exit_section_(b, l, m, r, p, null);
+    return r || p;
+  }
+
   /* ********************************************************** */
   // decl
   //        | importCmd
diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf
index 40137185e1..08dc76bdda 100644
--- a/parser/src/main/grammar/AyaPsiParser.bnf
+++ b/parser/src/main/grammar/AyaPsiParser.bnf
@@ -208,7 +208,8 @@ fnDecl ::= declModifiers*
  KW_DEF fnModifiers* declNameOrInfix
  tele* type? fnBody bindBlock? { pin=2 }
 
-fnBody ::= IMPLIES expr
+private simpleBody ::= IMPLIES expr { pin=1 }
+fnBody ::= simpleBody
          | barredClause*
 
 fnModifiers ::= KW_OPAQUE

From 711dcc7825dc543194aaac5ec829cdebf83bf45d Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 15:28:34 -0500
Subject: [PATCH 6/7] test: add fixture

---
 base/src/test/resources/failure/syntax/incomplete-code.aya | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 base/src/test/resources/failure/syntax/incomplete-code.aya

diff --git a/base/src/test/resources/failure/syntax/incomplete-code.aya b/base/src/test/resources/failure/syntax/incomplete-code.aya
new file mode 100644
index 0000000000..893fdbd20d
--- /dev/null
+++ b/base/src/test/resources/failure/syntax/incomplete-code.aya
@@ -0,0 +1,4 @@
+prim
+def
+def k =>
+data

From 10596dc1d59960deed5ef4408b33fc6d381994e1 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 20:52:05 +0000
Subject: [PATCH 7/7] text: update fixtures

---
 .../implicit-element-list-pattern.aya.txt     |  2 +-
 .../failure/syntax/incomplete-code.aya.txt    | 38 +++++++++++++++++++
 .../resources/failure/syntax/issue164.aya.txt |  4 +-
 .../resources/failure/syntax/issue165.aya.txt |  6 +--
 .../failure/syntax/literal-too-large.aya.txt  |  2 +-
 5 files changed, 45 insertions(+), 7 deletions(-)
 create mode 100644 base/src/test/resources/failure/syntax/incomplete-code.aya.txt

diff --git a/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt b/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt
index 9a5cdece85..e1bfce847a 100644
--- a/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt
+++ b/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt
@@ -5,7 +5,7 @@ In file $FILE:11:8 ->
   11 │   | [ _, {y} ], default => y
      │           ╰╯
 
-Error: Parser error: Implicit elements in a list pattern is disallowed
+Error: Implicit elements in a list pattern is disallowed
 
 1 error(s), 0 warning(s).
 What are you doing?
diff --git a/base/src/test/resources/failure/syntax/incomplete-code.aya.txt b/base/src/test/resources/failure/syntax/incomplete-code.aya.txt
new file mode 100644
index 0000000000..dcd9bfd7f1
--- /dev/null
+++ b/base/src/test/resources/failure/syntax/incomplete-code.aya.txt
@@ -0,0 +1,38 @@
+In file $FILE:1:0 ->
+
+  1 │   prim
+    │   ╰──╯
+  2 │   def
+  3 │   def k =>
+
+Error: Expect a primitive's name
+
+In file $FILE:2:0 ->
+
+  1 │   prim
+  2 │   def
+    │   ╰─╯
+  3 │   def k =>
+
+Error: Expect a function name
+
+In file $FILE:3:6 ->
+
+  1 │   prim
+  2 │   def
+  3 │   def k =>
+    │         ╰╯
+
+Error: Expect function body
+
+In file $FILE:4:0 ->
+
+  2 │   def
+  3 │   def k =>
+  4 │   data
+    │   ╰──╯
+
+Error: Expect a data name
+
+4 error(s), 0 warning(s).
+What are you doing?
diff --git a/base/src/test/resources/failure/syntax/issue164.aya.txt b/base/src/test/resources/failure/syntax/issue164.aya.txt
index c743a2b00c..354f6bfd5a 100644
--- a/base/src/test/resources/failure/syntax/issue164.aya.txt
+++ b/base/src/test/resources/failure/syntax/issue164.aya.txt
@@ -5,7 +5,7 @@ In file $FILE:3:26 ->
   3 │                (p : Sig A  B) : C
     │                             ╰╯
 
-Error: Parser error: Cannot parse
+Error: Cannot parse
 
 In file $FILE:8:29 ->
 
@@ -14,7 +14,7 @@ In file $FILE:8:29 ->
   8 │                 (p : Sig A B  C) : D
     │                                ╰╯
 
-Error: Parser error: Cannot parse
+Error: Cannot parse
 
 In file $FILE:1:4 ->
 
diff --git a/base/src/test/resources/failure/syntax/issue165.aya.txt b/base/src/test/resources/failure/syntax/issue165.aya.txt
index f4265b14d7..a53056bbab 100644
--- a/base/src/test/resources/failure/syntax/issue165.aya.txt
+++ b/base/src/test/resources/failure/syntax/issue165.aya.txt
@@ -1,9 +1,9 @@
-In file $FILE:1:3 ->
+In file $FILE:1:0 ->
 
   1 │   def
-    │      ╰╯
+    │   ╰─╯
 
-Error: Parser error: Cannot parse
+Error: Expect a function name
 
 1 error(s), 0 warning(s).
 What are you doing?
diff --git a/base/src/test/resources/failure/syntax/literal-too-large.aya.txt b/base/src/test/resources/failure/syntax/literal-too-large.aya.txt
index c2527941ff..9faf336fea 100644
--- a/base/src/test/resources/failure/syntax/literal-too-large.aya.txt
+++ b/base/src/test/resources/failure/syntax/literal-too-large.aya.txt
@@ -5,7 +5,7 @@ In file $FILE:3:17 ->
   3 │   def too-large => 2147483648
     │                    ╰────────╯
 
-Error: Parser error: Unsupported integer literal `2147483648`
+Error: Unsupported integer literal `2147483648`
 
 Parsing interrupted due to:
 1 error(s), 0 warning(s).