From e5e577865fe74ad17182346a225f8f209fa6e2e4 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 7 Sep 2024 13:46:53 -0700
Subject: [PATCH] doc: mention that `inferType` does not ensure type
 correctness (#5087)

This also adds links to the implementations of `whnf` and `inferType` to
make it easier to navigate this part of the code base.
---
 src/Lean/Meta/Basic.lean | 74 +++++++++++++++++++++++++++++++++++-----
 1 file changed, 65 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 51d55d992987..0f282175f890 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -560,16 +560,72 @@ def useEtaStruct (inductName : Name) : MetaM Bool := do
   | .all  => return true
   | .notClasses => return !isClass (← getEnv) inductName
 
-/-! WARNING: The following 4 constants are a hack for simulating forward declarations.
-   They are defined later using the `export` attribute. This is hackish because we
-   have to hard-code the true arity of these definitions here, and make sure the C names match.
-   We have used another hack based on `IO.Ref`s in the past, it was safer but less efficient. -/
-
-/-- Reduces an expression to its Weak Head Normal Form.
-This is when the topmost expression has been fully reduced,
-but may contain subexpressions which have not been reduced. -/
+/-!
+WARNING: The following 4 constants are a hack for simulating forward declarations.
+They are defined later using the `export` attribute. This is hackish because we
+have to hard-code the true arity of these definitions here, and make sure the C names match.
+We have used another hack based on `IO.Ref`s in the past, it was safer but less efficient.
+-/
+
+/--
+Reduces an expression to its *weak head normal form*.
+This is when the "head" of the top-level expression has been fully reduced.
+The result may contain subexpressions that have not been reduced.
+
+See `Lean.Meta.whnfImp` for the implementation.
+-/
 @[extern 6 "lean_whnf"] opaque whnf : Expr → MetaM Expr
-/-- Returns the inferred type of the given expression, or fails if it is not type-correct. -/
+/--
+Returns the inferred type of the given expression. Assumes the expression is type-correct.
+
+The type inference algorithm does not do general type checking.
+Type inference only looks at subterms that are necessary for determining an expression's type,
+and as such if `inferType` succeeds it does *not* mean the term is type-correct.
+If an expression is sufficiently ill-formed that it prevents `inferType` from computing a type,
+then it will fail with a type error.
+
+For typechecking during elaboration, see `Lean.Meta.check`.
+(Note that we do not guarantee that the elaborator typechecker is as correct or as efficient as
+the kernel typechecker. The kernel typechecker is invoked when a definition is added to the environment.)
+
+Here are examples of type-incorrect terms for which `inferType` succeeds:
+```lean
+import Lean
+
+open Lean Meta
+
+/--
+`@id.{1} Bool Nat.zero`.
+In general, the type of `@id α x` is `α`.
+-/
+def e1 : Expr := mkApp2 (.const ``id [1]) (.const ``Bool []) (.const ``Nat.zero [])
+#eval inferType e1
+-- Lean.Expr.const `Bool []
+#eval check e1
+-- error: application type mismatch
+
+/--
+`let x : Int := Nat.zero; true`.
+In general, the type of `let x := v; e`, if `e` does not reference `x`, is the type of `e`.
+-/
+def e2 : Expr := .letE `x (.const ``Int []) (.const ``Nat.zero []) (.const ``true []) false
+#eval inferType e2
+-- Lean.Expr.const `Bool []
+#eval check e2
+-- error: invalid let declaration
+```
+Here is an example of a type-incorrect term that makes `inferType` fail:
+```lean
+/--
+`Nat.zero Nat.zero`
+-/
+def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
+#eval inferType e3
+-- error: function expected
+```
+
+See `Lean.Meta.inferTypeImp` for the implementation of `inferType`.
+-/
 @[extern 6 "lean_infer_type"] opaque inferType : Expr → MetaM Expr
 @[extern 7 "lean_is_expr_def_eq"] opaque isExprDefEqAux : Expr → Expr → MetaM Bool
 @[extern 7 "lean_is_level_def_eq"] opaque isLevelDefEqAux : Level → Level → MetaM Bool