Joachim review

Author: kmill

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -134,8 +134,6 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
       withLocalDecl n c (← loop below d) fun x => do
         mkForallFVars #[x] (← loop below (b.instantiate1 x))
     | Expr.letE n type val body nondep =>
-      -- Turn `have`s into `let`s if they are not propositions.
-      let nondep ← pure nondep <&&> not <$> Meta.isProp type
       mapLetDecl n (← loop below type) (← loop below val) (nondep := nondep) (usedLetOnly := false) fun x => do
         loop below (body.instantiate1 x)
     | Expr.mdata d b =>

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

@@ -122,13 +122,13 @@ private def numLetsWithValueNotIsWfParam (e : Expr) (acc := 0) : Nat :=
 
 private partial def processParamLet (e : Expr) : MetaM Expr := do
   if let .letE _ t v b _ := e then
-    if let some v := isWfParam? v then
+    if let some v' := isWfParam? v then
       if ← Meta.isProp t then
-        processParamLet <| e.updateLetE! t v b
+        processParamLet <| e.updateLetE! t v' b
       else
         let u ← getLevel t
         let b' := b.instantiate1 <| mkApp2 (.const ``wfParam [u]) t (.bvar 0)
-        processParamLet <| e.updateLetE! t v b'
+        processParamLet <| e.updateLetE! t v' b'
     else
       let num := numLetsWithValueNotIsWfParam e
       assert! num > 0

src/Lean/LocalContext.lean

@@ -71,6 +71,7 @@ inductive LocalDecl where
     have type-incorrect values. This design decision allows metaprograms to not have to think about nondep `ldecl`s,
     so long as `LocalDecl` values are consumed through `LocalDecl.isLet` and `LocalDecl.value?` with `(allowNondep := false)`.
     **Rule:** never use `(generalizeNondepLet := false)` in `mkBinding`-family functions within a local context you do not own.
+    See `LocalDecl.setNondep` for some additional discussion.
   - Where then do nondep ldecls come from? Common functions are `Meta.mapLetDecl`, `Meta.withLetDecl`, and `Meta.letTelescope`.
     The `have` term syntax makes use of a nondep ldecl as well.
 
@@ -91,7 +92,11 @@ def LocalDecl.binderInfoEx : LocalDecl → BinderInfo
   | _                   => BinderInfo.default
 namespace LocalDecl
 
-/-- Returns true if this is an `ldecl`. If `allowNondep` is false (the default), then requires that `nondep` be false. -/
+/--
+Returns true if this is an `ldecl` with a visible value.
+
+If `allowNondep` is true then includes `ldecl`s with `nondep := true`, whose values are normally hidden.
+-/
 def isLet : LocalDecl → (allowNondep : Bool := false) → Bool
   | cdecl .., _ => false
   | ldecl (nondep := false) .., _ => true
@@ -143,17 +148,19 @@ def isImplementationDetail (d : LocalDecl) : Bool :=
   d.kind != .default
 
 /--
-Returns the value of the `ldecl`,
-but if the `ldecl` is nondependent and `allowNondep` is false, returns `none`.
+Returns the value of the `ldecl` if it has a visible value.
+
+If `allowNondep` is true, then allows nondependent `ldecl`s, whose values are normally hidden.
 -/
 def value? : LocalDecl → (allowNondep : Bool := false) → Option Expr
   | ldecl (nondep := false) (value := v) .., _    => some v
   | ldecl (nondep := true)  (value := v) .., true => some v
   | _,                                       _    => none
 
 /--
-Returns the value of the `ldecl`,
-but if the `ldecl` is nondependent and `allowNondep` is false, panics.
+Returns the value of the `ldecl` if it has a visible value.
+
+If `allowNondep` is true, then allows nondependent `ldecl`s, whose values are normally hidden.
 -/
 def value : LocalDecl → (allowNondep : Bool := false) → Expr
   | cdecl ..,                                _     => panic! "let declaration expected"
@@ -175,17 +182,36 @@ def setValue : LocalDecl → Expr → LocalDecl
 
 /--
 Sets the `nondep` flag of an `ldecl`, otherwise returns `cdecl`s unchanged.
-It is the responsibility of the caller to ensure that transitions are correct.
+
+This is a low-level function, and it is the responsibility of the caller to ensure that
+transitions of `nondep` are valid.
 
 Rules:
-- Setting `nondep := true` is a way to convert the ldecl into a cdecl.
-  - Caution: be sure any relevant caches are cleared so that the value does not leak.
-  - Caution: be sure that metavariables from before and after the transition are not mixed,
+- If the declaration is not under the caller's control, then setting `nondep := false` must not be done.
+  General nondependent `ldecl`s should be treated like `cdecl`s.
+  See also the docstring for `LocalDecl.ldecl` about the `value` not necessarily being type correct.
+- Setting `nondep := true` is usually fine.
+  - Caution: be sure any relevant caches are cleared so that the value associated to this `FVarId` does not leak.
+  - Caution: be sure that metavariables dependent on this declaration created before and after the transition are not mixed,
     since unification does not check "`nondep`-compatibility" of local contexts when assigning metavariables.
-- If the declaration is for a variable whose dependencies are not completely under the caller's control,
-  then setting `nondep := false` must not be done.
-- Even if the caller does have complete control, setting `nondep := false` should not be done.
-  The cautions about caches and metavariables still apply.
+
+For example, setting `nondep := false` is fine from within a telescope combinator, to update the local context
+right before calling `mkLetFVars`:
+```lean
+let lctx ← getLCtx
+letTelescope e fun xs b => do
+  let lctx' ← xs.foldlM (init := lctx) fun lctx' x => do
+    let decl ← x.fvarId!.getDecl
+    -- Clear the flag if it's not a prop.
+    let decl' := decl.setNondep <| ← pure decl.isNondep <&&> Meta.isProp decl.type
+    pure <| lctx'.addDecl decl'
+  withLCtx' lctx' do
+    mkLetFVars (usedLetOnly := false) (generalizeNondepLet := false) xs b
+```
+1. The declarations for `xs` are in the control of this metaprogram.
+2. `mkLetFVars` does make use of `MetaM` caches.
+3. Even if `e` has metavariables, these do not include `xs` in their contexts,
+   so the change of the `nondep` flag does not cause any issues in the `abstractM` system used by `mkLetFVars`.
 -/
 def setNondep : LocalDecl → Bool → LocalDecl
   | ldecl idx id n t v _ k, nd => ldecl idx id n t v nd k

src/Lean/Meta/Basic.lean

@@ -979,9 +979,10 @@ def _root_.Lean.FVarId.getBinderInfo (fvarId : FVarId) : MetaM BinderInfo :=
   return (← fvarId.getDecl).binderInfo
 
 /--
-Returns `some value` if the given free variable is a let-declaration, and `none` otherwise.
+Returns `some value` if the given free let-variable has a visible local definition in the current local context
+(using `Lean.LocalDecl.value?`), and `none` otherwise.
 
-If `allowNondep := false` (the default) then returns `none` if it is a nondependent let-declaration.
+Setting `allowNondep := true` allows access of the normally hidden value of a nondependent let declaration.
 -/
 def _root_.Lean.FVarId.getValue? (fvarId : FVarId) (allowNondep : Bool := false) : MetaM (Option Expr) :=
   return (← fvarId.getDecl).value? allowNondep
@@ -991,9 +992,10 @@ def _root_.Lean.FVarId.getUserName (fvarId : FVarId) : MetaM Name :=
   return (← fvarId.getDecl).userName
 
 /--
-Returns `true` is the free variable is a let-variable.
+Returns `true` if the free variable is a let-variable with a visible local definition in the current local context
+(using `Lean.LocalDecl.isLet`).
 
-If `allowNondep := false` (the default) then returns `false` if it is a nondependent let-declaration.
+Setting `allowNondep := true` includes nondependent let declarations, whose values are normally hidden.
 -/
 def _root_.Lean.FVarId.isLetVar (fvarId : FVarId) (allowNondep : Bool := false) : MetaM Bool :=
   return (← fvarId.getDecl).isLet allowNondep

src/Lean/Meta/Tactic/Lets.lean

@@ -224,7 +224,7 @@ partial def extractCore (fvars : List Expr) (e : Expr) (topLevel : Bool := false
       match e with
       | .bvar .. | .fvar .. | .mvar .. | .sort .. | .const .. | .lit .. => unreachable!
       | .mdata _ e'      => return e.updateMData! (← extractCore fvars e' (topLevel := topLevel))
-      | .letE n t v b nondep  => extractLetLike (!nondep) n t v b (fun t v b => pure <| e.updateLetE! t v b) (topLevel := topLevel)
+      | .letE n t v b nondep  => extractLetLike !nondep n t v b (fun t v b => pure <| e.updateLetE! t v b) (topLevel := topLevel)
       | .app ..          =>
         if e.isLetFun then
           extractLetFun e (topLevel := topLevel)