Dependent and non-dependent `Expr.letE`

Stream: lean4

[Leni Aniva]

In inductive Expr we have the let-in expression:

  /--
  Let-expressions.

  **IMPORTANT**: The `nonDep` flag is for "local" use only. That is, a module should not "trust" its value for any purpose.
  In the intended use-case, the compiler will set this flag, and be responsible for maintaining it.
  Other modules may not preserve its value while applying transformations.

  Given an environment, a metavariable context, and a local context,
  we say a let-expression `let x : t := v; e` is non-dependent when it is equivalent
  to `(fun x : t => e) v`. In contrast, the dependent let-expression
  `let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct,
  but `(fun (n : Nat) (a : Array Nat n) (b : Array Nat 2) => a = b) 2` is not.

  The let-expression `let x : Nat := 2; Nat.succ x` is represented as
  ```
  Expr.letE `x (.const `Nat []) (.lit (.natVal 2)) (.app (.const `Nat.succ []) (.bvar 0)) true
  ```
  -/
  | letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)

What makes the example type correct? Is it because the type of the interior of the let is only determined after the argument of the let is evaluated?

[Mario Carneiro]

Within the body of a let statement, the declared variable is definitionally equal to its value. This behavior is an intrinsic part of dependent type theory as implemented in the kernel. It's not really about evaluation order per se

[Mario Carneiro]

The simplest way to define it is to say that to check that (let x : T := v; e) : U, it suffices that v : T and e[v/x] : U

[Mario Carneiro]

in other words, we never check e alone, we first expand all occurrences of x in e

[Mario Carneiro]

this is by contrast to (fun x : T => e) v : U, where to check this we need to show v : T and x : T |- e : U, which is to say that when typechecking e you don't know anything in particular about x other than its type