feat: add the nonDep field of Expr.letE to the C++ data model

This PR adds the `nonDep` field of `Expr.letE` to the C++ data model. Previously this was unused, and in followup PRs the elaborator will use it to encode `have` expressions (non-dependent `let`s). The kernel does not verify that `nonDep` is correctly applied during typechecking. Breaking change: now `Expr.updateLet!` is `Expr.updateLetE!`.

This PR also fixes a bug in `Expr.letFun?` and `Expr.letFunAppArgs?` when the body is not a lambda. In any case, these functions will be removed once the `Expr.letE (nonDep := true)` encoding of `have` expressions is complete.

Author: kmill

src/Lean/Compiler/LCNF/Level.lean

@@ -67,7 +67,7 @@ partial def normExpr (e : Expr) : M Expr := do
     | .const _ us      => return e.updateConst! (← us.mapM normLevel)
     | .sort u          => return e.updateSort! (← normLevel u)
     | .app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
-    | .letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
+    | .letE _ t v b _  => return e.updateLetE! (← normExpr t) (← normExpr v) (← normExpr b)
     | .forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
     | .lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
     | .mdata _ b       => return e.updateMData! (← normExpr b)

src/Lean/Elab/PreDefinition/WF/Preprocess.lean

@@ -117,7 +117,7 @@ builtin_dsimproc paramLet (_) := fun e => do
   let u ← getLevel e.letType!
   let body' := e.letBody!.instantiate1 <|
     mkApp2 (.const ``wfParam [u]) e.letType! (.bvar 0)
-  return .continue <| e.updateLet! e.letType! v body'
+  return .continue <| e.updateLetE! e.letType! v body'
 
 def preprocess (e : Expr) : MetaM Simp.Result := do
   unless wf.preprocess.get (← getOptions) do

src/Lean/Expr.lean

@@ -391,20 +391,19 @@ inductive Expr where
   /--
   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.
+  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
+  ```
 
+  If the `nonDep` flag is `true`, then the elaborator treats this as a *non-dependent `let`* (known as a *`have` expression*).
   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
-  ```
+  The kernel does not pay attention to `nonDep` when type checking.
   -/
   | letE (declName : Name) (type : Expr) (value : Expr) (body : Expr) (nonDep : Bool)
 
@@ -671,12 +670,14 @@ def mkSimpleThunkType (type : Expr) : Expr :=
 def mkSimpleThunk (type : Expr) : Expr :=
   mkLambda `_ BinderInfo.default (mkConst `Unit) type
 
-/--
-`.letE x t v b nonDep` is now the preferred form.
--/
-def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
+/-- Returns `let x : t := v; b`, a dependent `let` expression. If `nonDep := true`, then returns a `have`. -/
+@[inline] def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
   .letE x t v b nonDep
 
+/-- Returns `have x : t := v; b`, a non-dependent `let` expression. -/
+@[inline] def mkHave (x : Name) (t : Expr) (v : Expr) (b : Expr) : Expr :=
+  .letE x t v b true
+
 @[match_pattern] def mkAppB (f a b : Expr) := mkApp (mkApp f a) b
 @[match_pattern] def mkApp2 (f a b : Expr) := mkAppB f a b
 @[match_pattern] def mkApp3 (f a b c : Expr) := mkApp (mkAppB f a b) c
@@ -723,7 +724,7 @@ def mkStrLit (s : String) : Expr :=
 @[export lean_expr_mk_app] def mkAppEx : Expr → Expr → Expr := mkApp
 @[export lean_expr_mk_lambda] def mkLambdaEx (n : Name) (d b : Expr) (bi : BinderInfo) : Expr := mkLambda n bi d b
 @[export lean_expr_mk_forall] def mkForallEx (n : Name) (d b : Expr) (bi : BinderInfo) : Expr := mkForall n bi d b
-@[export lean_expr_mk_let] def mkLetEx (n : Name) (t v b : Expr) : Expr := mkLet n t v b
+@[export lean_expr_mk_let] def mkLetEx (n : Name) (t v b : Expr) (nonDep : Bool) : Expr := mkLet n t v b nonDep
 @[export lean_expr_mk_lit] def mkLitEx : Literal → Expr := mkLit
 @[export lean_expr_mk_mdata] def mkMDataEx : MData → Expr → Expr := mkMData
 @[export lean_expr_mk_proj] def mkProjEx : Name → Nat → Expr → Expr := mkProj
@@ -867,11 +868,18 @@ def isBinding : Expr → Bool
   | forallE .. => true
   | _          => false
 
-/-- Return `true` if the given expression is a let-expression. -/
+/-- Return `true` if the given expression is a let-expression or a have-expression. -/
 def isLet : Expr → Bool
   | letE .. => true
   | _       => false
 
+/-- Return `true` if the given expression is a non-dependent let-expression (a have-expression). -/
+def isHave : Expr → Bool
+  | letE (nonDep := nonDep) .. => nonDep
+  | _       => false
+
+@[export lean_expr_isHave] def isHaveEx : Expr → Bool := isHave
+
 /-- Return `true` if the given expression is a metadata. -/
 def isMData : Expr → Bool
   | mdata .. => true
@@ -1012,6 +1020,10 @@ def letBody! : Expr → Expr
   | letE _ _ _ b .. => b
   | _               => panic! "let expression expected"
 
+def letNonDep! : Expr → Bool
+  | letE _ _ _ _ nonDep => nonDep
+  | _                   => panic! "let expression expected"
+
 def consumeMData : Expr → Expr
   | mdata _ e => consumeMData e
   | e         => e
@@ -1842,21 +1854,28 @@ def updateLambda! (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody
   | lam n d b bi => updateLambda! (lam n d b bi) bi newDomain newBody
   | _            => panic! "lambda expected"
 
-@[inline] private unsafe def updateLet!Impl (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
+@[inline] private unsafe def updateLet!Impl (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (newNonDep : Bool) : Expr :=
   match e with
   | letE n t v b nonDep =>
-    if ptrEq t newType && ptrEq v newVal && ptrEq b newBody then
+    if ptrEq t newType && ptrEq v newVal && ptrEq b newBody && nonDep == newNonDep then
       e
     else
-      letE n newType newVal newBody nonDep
+      letE n newType newVal newBody newNonDep
   | _              => panic! "let expression expected"
 
 @[implemented_by updateLet!Impl]
-def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
+def updateLet! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (newNonDep : Bool) : Expr :=
   match e with
-  | letE n _ _ _ c => letE n newType newVal newBody c
+  | letE n _ _ _ _ => letE n newType newVal newBody newNonDep
   | _              => panic! "let expression expected"
 
+/-- Like `Expr.updateLet!` but preserves the `nonDep` flag. -/
+@[inline]
+def updateLetE! (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) : Expr :=
+  match e with
+  | letE n t v b nonDep => updateLet! (letE n t v b nonDep) newType newVal newBody nonDep
+  | _                   => panic! "let expression expected"
+
 def updateFn : Expr → Expr → Expr
   | e@(app f a), g => e.updateApp! (updateFn f g) a
   | _,           g => g
@@ -1965,7 +1984,7 @@ def letFun? (e : Expr) : Option (Name × Expr × Expr × Expr) :=
   | .app (.app (.app (.app (.const ``letFun _) t) _β) v) f =>
     match f with
     | .lam n _ b _ => some (n, t, v, b)
-    | _ => some (.anonymous, t, v, .app f (.bvar 0))
+    | _ => some (.anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
   | _ => none
 
 /--
@@ -1982,15 +2001,15 @@ def letFunAppArgs? (e : Expr) : Option (Array Expr × Name × Expr × Expr × Ex
   let rest := args.extract 4 args.size
   match f with
   | .lam n _ b _ => some (rest, n, t, v, b)
-  | _ => some (rest, .anonymous, t, v, .app f (.bvar 0))
+  | _ => some (rest, .anonymous, t, v, .app (f.liftLooseBVars 0 1) (.bvar 0))
 
 /-- Maps `f` on each immediate child of the given expression. -/
 @[specialize]
 def traverseChildren [Applicative M] (f : Expr → M Expr) : Expr → M Expr
   | e@(forallE _ d b _) => pure e.updateForallE! <*> f d <*> f b
   | e@(lam _ d b _)     => pure e.updateLambdaE! <*> f d <*> f b
   | e@(mdata _ b)       => e.updateMData! <$> f b
-  | e@(letE _ t v b _)  => pure e.updateLet! <*> f t <*> f v <*> f b
+  | e@(letE _ t v b _)  => pure e.updateLetE! <*> f t <*> f v <*> f b
   | e@(app l r)         => pure e.updateApp! <*> f l <*> f r
   | e@(proj _ _ b)      => e.updateProj! <$> f b
   | e                   => pure e

src/Lean/Meta/AbstractMVars.lean

@@ -78,7 +78,7 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
     | e@(Expr.mdata _ b)       => return e.updateMData! (← abstractExprMVars b)
     | e@(Expr.lam _ d b _)     => return e.updateLambdaE! (← abstractExprMVars d) (← abstractExprMVars b)
     | e@(Expr.forallE _ d b _) => return e.updateForallE! (← abstractExprMVars d) (← abstractExprMVars b)
-    | e@(Expr.letE _ t v b _)  => return e.updateLet! (← abstractExprMVars t) (← abstractExprMVars v) (← abstractExprMVars b)
+    | e@(Expr.letE _ t v b _)  => return e.updateLetE! (← abstractExprMVars t) (← abstractExprMVars v) (← abstractExprMVars b)
     | e@(Expr.mvar mvarId)     =>
       let decl := (← getMCtx).getDecl mvarId
       if decl.depth != (← getMCtx).depth then

src/Lean/Meta/Closure.lean

@@ -193,7 +193,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
   | Expr.proj _ _ s      => return e.updateProj! (← collect s)
   | Expr.forallE _ d b _ => return e.updateForallE! (← collect d) (← collect b)
   | Expr.lam _ d b _     => return e.updateLambdaE! (← collect d) (← collect b)
-  | Expr.letE _ t v b _  => return e.updateLet! (← collect t) (← collect v) (← collect b)
+  | Expr.letE _ t v b _  => return e.updateLetE! (← collect t) (← collect v) (← collect b)
   | Expr.app f a         => return e.updateApp! (← collect f) (← collect a)
   | Expr.mdata _ b       => return e.updateMData! (← collect b)
   | Expr.sort u          => return e.updateSort! (← collectLevel u)

src/Lean/Meta/ExprDefEq.lean

@@ -851,7 +851,7 @@ mutual
       | .proj _ _ s      => return e.updateProj! (← check s)
       | .lam _ d b _     => return e.updateLambdaE! (← check d) (← check b)
       | .forallE _ d b _ => return e.updateForallE! (← check d) (← check b)
-      | .letE _ t v b _  => return e.updateLet! (← check t) (← check v) (← check b)
+      | .letE _ t v b _  => return e.updateLetE! (← check t) (← check v) (← check b)
       | .bvar ..         => return e
       | .sort ..         => return e
       | .const ..        => return e

src/Lean/Meta/ExprLens.lean

@@ -36,8 +36,8 @@ private def lensCoord (g : Expr → M Expr) (n : Nat) (e : Expr) : M Expr := do
   | 1, .lam n y b c     => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
   | 0, .forallE _ y b _ => return e.updateForallE! (← g y) b
   | 1, .forallE n y b c => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
-  | 0, .letE _ y a b _  => return e.updateLet! (← g y) a b
-  | 1, .letE _ y a b _  => return e.updateLet! y (← g a) b
+  | 0, .letE _ y a b _  => return e.updateLetE! (← g y) a b
+  | 1, .letE _ y a b _  => return e.updateLetE! y (← g a) b
   | 2, .letE n y a b _  => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
   | 0, .proj _ _ b      => e.updateProj! <$> g b
   | n, .mdata _ a       => e.updateMData! <$> lensCoord g n a

src/Lean/Meta/InferType.lean

@@ -38,7 +38,7 @@ where
       match e with
       | .forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
       | .lam _ d b _     => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
-      | .letE _ t v b _  => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
+      | .letE _ t v b _  => return e.updateLetE! (← visit t offset) (← visit v offset) (← visit b (offset+1))
       | .mdata _ b       => return e.updateMData! (← visit b offset)
       | .proj _ _ b      => return e.updateProj! (← visit b offset)
       | .app .. =>

src/Lean/Meta/KAbstract.lean

@@ -36,7 +36,7 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := .all) : MetaM Expr :=
         | .app f a         => return e.updateApp! (← visit f offset) (← visit a offset)
         | .mdata _ b       => return e.updateMData! (← visit b offset)
         | .proj _ _ b      => return e.updateProj! (← visit b offset)
-        | .letE _ t v b _  => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
+        | .letE _ t v b _  => return e.updateLetE! (← visit t offset) (← visit v offset) (← visit b (offset+1))
         | .lam _ d b _     => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
         | .forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
         | e                => return e

src/Lean/Meta/SynthInstance.lean

@@ -135,7 +135,7 @@ partial def normExpr (e : Expr) : M Expr := do
     | .const _ us      => return e.updateConst! (← us.mapM normLevel)
     | .sort u          => return e.updateSort! (← normLevel u)
     | .app f a         => return e.updateApp! (← normExpr f) (← normExpr a)
-    | .letE _ t v b _  => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
+    | .letE _ t v b _  => return e.updateLetE! (← normExpr t) (← normExpr v) (← normExpr b)
     | .forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
     | .lam _ d b _     => return e.updateLambdaE! (← normExpr d) (← normExpr b)
     | .mdata _ b       => return e.updateMData! (← normExpr b)