LICIT: Insert implicit parameters the right way

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -116,7 +116,19 @@ public void solveMetas() {
   }
 
   public @NotNull Result checkNoZonk(@NotNull Expr expr, @Nullable Term type) {
-    return expr.accept(this, type);
+    if (type == null) return expr.accept(this, null);
+    else if (type instanceof FormTerm.Pi pi && needImplicitParamIns(expr, pi)) {
+      var implicitParam = new Term.Param(new LocalVar(ANONYMOUS_PREFIX), pi.param().type(), false);
+      var body = localCtx.with(implicitParam, () ->
+        checkNoZonk(expr, pi.substBody(implicitParam.toTerm()))).wellTyped;
+      return new Result(new IntroTerm.Lambda(implicitParam, body), pi);
+    } else return expr.accept(this, type);
+  }
+
+  private static boolean needImplicitParamIns(@NotNull Expr expr, @NotNull FormTerm.Pi type) {
+    return !type.param().explicit()
+      && (expr instanceof Expr.LamExpr ex && ex.param().explicit()
+      || !(expr instanceof Expr.LamExpr));
   }
 
   public @NotNull Result checkExpr(@NotNull Expr expr, @Nullable Term type) {

base/src/test/resources/success/issue659-param.aya

@@ -0,0 +1,2 @@
+def imConst {A : Set} (a : A) : Pi {ignoreMe ignoreThis : A} -> A => a
+def imId {A : Set} : Pi {ignoreMe : A} -> A -> Pi {ignoreThis : A} -> A => \ a => a