fix: new compiler type checker

src/Lean/Compiler/Check.lean

@@ -65,13 +65,24 @@ where
       checkCases casesInfo args
     else
       let mut fType ← inferType f
+      let mut j := 0
       for i in [:args.size] do
         let arg := args[i]!
         if fType.isAnyType then
           return ()
-        let .forallE _ d b _ := fType.headBeta | throwError "function expected at{indentExpr e}\narrow type expected{indentExpr fType}"
+        fType := fType.headBeta
+        let (d, b) ←
+          match fType with
+          | .forallE _ d b _ => pure (d, b)
+          | _ =>
+            fType := fType.instantiateRevRange j i args |>.headBeta
+            match fType with
+            | .forallE _ d b _ => j := i; pure (d, b)
+            | _ =>
+              if fType.isAnyType then return ()
+              throwError "function expected at{indentExpr e}\narrow type expected{indentExpr fType}"
         let argType ← inferType arg
-        let expectedType := d.instantiateRevRange 0 i args
+        let expectedType := d.instantiateRevRange j i args
         unless compatibleTypes argType expectedType do
           throwError "type mismatch at LCNF application{indentExpr e}\nargument {arg} has type{indentExpr argType}\nbut is expected to have type{indentExpr expectedType}"
         unless isTypeFormerType d || d.erased do

src/Lean/Compiler/InferType.lean

@@ -59,15 +59,19 @@ mutual
     else
       let f := e.getAppFn
       let args := e.getAppArgs
+      let mut j := 0
       let mut fType ← inferType f
-      for _ in [:args.size] do
+      for i in [:args.size] do
         fType := fType.headBeta
         match fType with
         | .forallE _ _ b _ => fType := b
         | _ =>
-          if fType.isAnyType then return anyTypeExpr
-          throwError "function expected{indentExpr f}"
-      return fType.instantiateRev args
+          match fType.instantiateRevRange j i args |>.headBeta with
+          | .forallE _ _ b _ => j := i; fType := b
+          | _ =>
+            if fType.isAnyType then return anyTypeExpr
+            throwError "function expected{indentExpr f}"
+      return fType.instantiateRevRange j args.size args |>.headBeta
 
   partial def inferProjType (structName : Name) (idx : Nat) (s : Expr) : InferTypeM Expr := do
     let failed {α} : Unit → InferTypeM α := fun _ =>

tests/lean/run/lcnf1.lean

@@ -45,5 +45,7 @@ def Vec.head : Vec α (n+1) → α
 
 #eval Compiler.compile #[``Lean.Elab.Term.reportStuckSyntheticMVar]
 
-set_option trace.Compiler.step true
 #eval Compiler.compile #[``Lean.Elab.Term.synthesizeSyntheticMVars]
+
+set_option trace.Compiler.step true
+#eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl]