From 8c041786ea4b6fb94f23e9bb2347533f4de77d43 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Mon, 16 Dec 2024 07:42:18 +0100
Subject: [PATCH] fix: `check` must check projections (#6398)

This PR ensures `Meta.check` check projections.

closes #5660
---
 src/Lean/Meta/Check.lean     |  8 ++++-
 src/Lean/Meta/InferType.lean | 10 +++---
 tests/lean/run/5660.lean     | 61 ++++++++++++++++++++++++++++++++++++
 3 files changed, 74 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/5660.lean

diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index b6d7c2771076c..e8b20aaaff515 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -209,6 +209,12 @@ def checkApp (f a : Expr) : MetaM Unit := do
       throwAppTypeMismatch f a
   | _ => throwFunctionExpected (mkApp f a)
 
+def checkProj (structName : Name) (idx : Nat) (e : Expr) : MetaM Unit := do
+  let structType ← whnf (← inferType e)
+  let projType ← inferType (mkProj structName idx e)
+  if (← isProp structType) && !(← isProp projType) then
+    throwError "invalid projection{indentExpr (mkProj structName idx e)}\nfrom type{indentExpr structType}"
+
 private partial def checkAux (e : Expr) : MetaM Unit := do
   check e |>.run
 where
@@ -221,7 +227,7 @@ where
       | .const c lvls    => checkConstant c lvls
       | .app f a         => check f; check a; checkApp f a
       | .mdata _ e       => check e
-      | .proj _ _ e      => check e
+      | .proj s i e      => check e; checkProj s i e
       | _                => return ()
 
   checkLambdaLet (e : Expr) : MonadCacheT ExprStructEq Unit MetaM Unit :=
diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean
index 82a447c0d393a..c99fe03df2fbd 100644
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@@ -99,7 +99,9 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
   let structType ← whnf structType
   let failed {α} : Unit → MetaM α := fun _ => do
     throwError "invalid projection{indentExpr (mkProj structName idx e)}\nfrom type{indentExpr structType}"
-  matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal =>
+  matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal => do
+    unless structVal.name == structName do
+      failed ()
     let structTypeArgs := structType.getAppArgs
     if structVal.numParams + structVal.numIndices != structTypeArgs.size then
       failed ()
@@ -108,7 +110,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
       for i in [:idx] do
         ctorType ← whnf ctorType
         match ctorType with
-        | Expr.forallE _ _ body _ =>
+        | .forallE _ _ body _ =>
           if body.hasLooseBVars then
             ctorType := body.instantiate1 <| mkProj structName i e
           else
@@ -116,8 +118,8 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
         | _ => failed ()
       ctorType ← whnf ctorType
       match ctorType with
-      | Expr.forallE _ d _ _ => return d.consumeTypeAnnotations
-      | _                    => failed ()
+      | .forallE _ d _ _ => return d.consumeTypeAnnotations
+      | _                => failed ()
 
 def throwTypeExcepted {α} (type : Expr) : MetaM α :=
   throwError "type expected{indentExpr type}"
diff --git a/tests/lean/run/5660.lean b/tests/lean/run/5660.lean
new file mode 100644
index 0000000000000..2955859c28135
--- /dev/null
+++ b/tests/lean/run/5660.lean
@@ -0,0 +1,61 @@
+import Lean
+
+
+def ex : ∃ x : Nat, x = 1 :=
+  ⟨1, rfl⟩
+
+open Lean Meta
+
+/--
+error: invalid projection
+  ex.3
+from type
+  ∃ x, x = 1
+-/
+#guard_msgs in
+run_meta check (Expr.proj ``Exists 2 (mkConst ``ex)) -- should fail
+
+/--
+error: invalid projection
+  ex.1
+from type
+  ∃ x, x = 1
+-/
+#guard_msgs in
+run_meta check (Expr.proj ``Exists 0 (mkConst ``ex)) -- should fail
+
+run_meta check (Expr.proj ``Exists 1 (mkConst ``ex))
+
+def p := (1, 2)
+
+/--
+error: invalid projection
+  p.1
+from type
+  Nat × Nat
+-/
+#guard_msgs in
+run_meta check (Expr.proj ``Exists 0 (mkConst ``p)) -- should fail
+
+run_meta check (Expr.proj ``Prod 0 (mkConst ``p))
+run_meta check (Expr.proj ``Prod 1 (mkConst ``p))
+
+/--
+error: invalid projection
+  p.3
+from type
+  Nat × Nat
+-/
+#guard_msgs in
+run_meta check (Expr.proj ``Prod 2 (mkConst ``p)) -- should fail
+
+def n := 1
+
+/--
+error: invalid projection
+  n.1
+from type
+  Nat
+-/
+#guard_msgs in
+run_meta check (Expr.proj ``Nat 0 (mkConst ``n)) -- should fail