feat: immediate noncomputable check (#12028)

This PR gives a simpler semantics to `noncomputable`, improving
predictability as well as preparing codegen to be moved into a separate
build step without breaking immediate generation of error messages.

Specifically, `noncomputable` is now needed whenever an axiom or another
`noncomputable` def is used by a def except for the following special
cases:
* uses inside proofs, types, type formers, and constructor arguments
corresponding to (fixed) inductive parameters are ignored
* uses of functions marked `@[extern]/@[implemented_by]/@[csimp]` are
ignored
* for applications of a function marked `@[macro_inline]`,
noncomputability of the inlining is instead inspected

# Breaking change

After this change, more `noncomputable` annotations than before may be
required in exchange for improved future stability.

src/Lean/Compiler/IR/ToIR.lean

@@ -250,7 +250,8 @@ partial def lowerLet (decl : LCNF.LetDecl .pure) (k : LCNF.Code .pure) : M FnBod
     | some (.defnInfo ..) | some (.opaqueInfo ..) =>
       mkFap name irArgs
     | some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>
-      throwNamedError lean.dependsOnNoncomputable f!"`{name}` not supported by code generator; consider marking definition as `noncomputable`"
+      -- Should have been caught by `ToLCNF`
+      throwError f!"ToIR: unexpected use of noncomputable declaration `{name}`; please report this issue"
     | some (.recInfo ..) =>
       throwError f!"code generator does not support recursor `{name}` yet, consider using 'match ... with' and/or structural recursion"
     | none => panic! "reference to unbound name"

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -12,6 +12,8 @@ public import Lean.Compiler.LCNF.Bind
 public import Lean.Compiler.NeverExtractAttr
 import Lean.Meta.CasesInfo
 import Lean.Meta.WHNF
+import Lean.Compiler.NoncomputableAttr
+import Lean.AddDecl
 public section
 namespace Lean.Compiler.LCNF
 namespace ToLCNF
@@ -194,6 +196,13 @@ where
     else
       return c
 
+structure Context where
+  /--
+  Whether uses of `noncomputable` defs should be ignored; used in contexts that will be erased
+  eventually.
+  -/
+  ignoreNoncomputable : Bool := false
+
 structure State where
   /-- Local context containing the original Lean types (not LCNF ones). -/
   lctx : LocalContext := {}
@@ -219,7 +228,7 @@ structure State where
   -/
   toAny : FVarIdSet := {}
 
-abbrev M := StateRefT State CompilerM
+abbrev M := ReaderT Context <| StateRefT State CompilerM
 
 @[inline] def liftMetaM (x : MetaM α) : M α := do
   x.run' { lctx := (← get).lctx }
@@ -253,7 +262,7 @@ def toCode (result : Arg .pure) : M (Code .pure) := do
     seqToCode (← get).seq (.return fvarId)
 
 def run (x : M α) : CompilerM α :=
-  x |>.run' {}
+  x.run {} |>.run' {}
 
 /--
 Return true iff `type` is `Sort _` or `As → Sort _`.
@@ -391,6 +400,16 @@ def etaExpandN (e : Expr) (n : Nat) : M Expr := do
     Meta.forallBoundedTelescope (← Meta.inferType e) n fun xs _ =>
       Meta.mkLambdaFVars xs (mkAppN e xs)
 
+private def checkComputable (ref : Name) : M Unit := do
+  if (← read).ignoreNoncomputable then
+    return
+  if ref matches ``Quot.mk | ``Quot.lift || isExtern (← getEnv) ref || (getImplementedBy? (← getEnv) ref).isSome then
+    return
+  if isNoncomputable (← getEnv) ref then
+    throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName ref}', which is 'noncomputable'"
+  else if getOriginalConstKind? (← getEnv) ref matches some .axiom | some .quot | some .induct | some .thm then
+    throwNamedError lean.dependsOnNoncomputable f!"`{ref}` not supported by code generator; consider marking definition as `noncomputable`"
+
 /--
 Eta reduce implicits. We use this function to eliminate introduced by the implicit lambda feature,
 where it generates terms such as `fun {α} => ReaderT.pure`
@@ -606,7 +625,20 @@ where
 
   visitCtor (arity : Nat) (e : Expr) : M (Arg .pure) :=
     etaIfUnderApplied e arity do
-      visitAppDefaultConst e.getAppFn e.getAppArgs
+      let f := e.getAppFn
+      let args := e.getAppArgs
+      let env ← getEnv
+      let .const declName us := CSimp.replaceConstants env f | unreachable!
+      let ctorInfo? ← isCtor? declName
+      let args ← args.mapIdxM fun idx arg =>
+        -- We can rely on `toMono` erasing ctor params eventually; we do not do so here so that type
+        -- inference on the value is preserved.
+        withReader (fun ctx =>
+            { ignoreNoncomputable := ctx.ignoreNoncomputable || ctorInfo?.any (idx < ·.numParams) }) do
+          visitAppArg arg
+      if hasNeverExtractAttribute env declName then
+        modify fun s => {s with shouldCache := false }
+      letValueToArg <| .const declName us args
 
   visitQuotLift (e : Expr) : M (Arg .pure) := do
     let arity := 6
@@ -723,6 +755,7 @@ where
 
   visitApp (e : Expr) : M (Arg .pure) := do
     if let .const declName us := CSimp.replaceConstants (← getEnv) e.getAppFn then
+      checkComputable declName
       if declName == ``Quot.lift then
         visitQuotLift e
       else if declName == ``Quot.mk then

src/Lean/Compiler/LCNF/ToMono.lean

@@ -16,7 +16,6 @@ namespace Lean.Compiler.LCNF
 
 structure ToMonoM.State where
   typeParams : FVarIdHashSet := {}
-  noncomputableVars : Std.HashMap FVarId Name := {}
 
 abbrev ToMonoM := StateRefT ToMonoM.State CompilerM
 
@@ -25,34 +24,17 @@ def Param.toMono (param : Param .pure) : ToMonoM (Param .pure) := do
     modify fun s => { s with typeParams := s.typeParams.insert param.fvarId }
   param.update (← toMonoType param.type)
 
-def throwNoncomputableError {α : Type} (declName : Name) : ToMonoM α :=
-  throwNamedError lean.dependsOnNoncomputable m!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{.ofConstName declName}', which is 'noncomputable'"
-
-def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do
-  if let some declName := (← get).noncomputableVars.get? fvarId then
-    throwNoncomputableError declName
-
-def checkFVarUseDeferred (resultFVar fvarId : FVarId) : ToMonoM Unit := do
-  if let some declName := (← get).noncomputableVars.get? fvarId then
-    modify fun s => { s with noncomputableVars := s.noncomputableVars.insert resultFVar declName }
-
 @[inline]
-def argToMonoBase (check : FVarId → ToMonoM Unit) (arg : Arg .pure) : ToMonoM (Arg .pure) := do
+def argToMono (arg : Arg .pure) : ToMonoM (Arg .pure) := do
   match arg with
   | .erased | .type .. => return .erased
   | .fvar fvarId =>
     if (← get).typeParams.contains fvarId then
       return .erased
     else
-      check fvarId
       return arg
 
-def argToMono (arg : Arg .pure) : ToMonoM (Arg .pure) := argToMonoBase checkFVarUse arg
-
-def argToMonoDeferredCheck (resultFVar : FVarId) (arg : Arg .pure) : ToMonoM (Arg .pure) :=
-  argToMonoBase (checkFVarUseDeferred resultFVar) arg
-
-def argsToMonoWithFnType (resultFVar : FVarId) (args : Array (Arg .pure)) (type : Expr)
+def argsToMonoWithFnType (args : Array (Arg .pure)) (type : Expr)
     : ToMonoM (Array (Arg .pure)) := do
   let mut remainingType : Option Expr := some type
   let mut result := Array.emptyWithCapacity args.size
@@ -62,14 +44,14 @@ def argsToMonoWithFnType (resultFVar : FVarId) (args : Array (Arg .pure)) (type
       if d.isErased then
         pure .erased
       else
-        argToMonoDeferredCheck resultFVar arg
+        argToMono arg
     else
       remainingType := none
-      argToMonoDeferredCheck resultFVar arg
+      argToMono arg
     result := result.push monoArg
   return result
 
-def argsToMonoRedArg (resultFVar : FVarId) (args : Array (Arg .pure)) (params : Array (Param .pure))
+def argsToMonoRedArg (args : Array (Arg .pure)) (params : Array (Param .pure))
     (redArgs : Array (Arg .pure)) : ToMonoM (Array (Arg .pure)) := do
   let mut result := #[]
   let mut argIdx := 0
@@ -78,23 +60,23 @@ def argsToMonoRedArg (resultFVar : FVarId) (args : Array (Arg .pure)) (params :
     | .fvar fvarId =>
       while params[argIdx]!.fvarId != fvarId do
         argIdx := argIdx + 1
-      let arg ← argToMonoDeferredCheck resultFVar args[argIdx]!
+      let arg ← argToMono args[argIdx]!
       argIdx := argIdx + 1
       result := result.push arg
     | .erased | .type _ => pure ()
   for arg in args[params.size...*] do
-    let arg ← argToMonoDeferredCheck resultFVar arg
+    let arg ← argToMono arg
     result := result.push arg
   return result
 
-def ctorAppToMono (resultFVar : FVarId) (ctorInfo : ConstructorVal) (args : Array (Arg .pure))
+def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array (Arg .pure))
     : ToMonoM (LetValue .pure) := do
   let argsNewParams : Array (Arg .pure) := .replicate ctorInfo.numParams .erased
-  let argsNewFields ← args[ctorInfo.numParams...*].toArray.mapM (argToMonoDeferredCheck resultFVar)
+  let argsNewFields ← args[ctorInfo.numParams...*].toArray.mapM argToMono
   let argsNew := argsNewParams ++ argsNewFields
   return .const ctorInfo.name [] argsNew
 
-partial def LetValue.toMono (e : LetValue .pure) (resultFVar : FVarId) : ToMonoM (LetValue .pure) := do
+partial def LetValue.toMono (e : LetValue .pure) : ToMonoM (LetValue .pure) := do
   match e with
   | .erased | .lit .. => return e
   | .const declName _ args =>
@@ -125,48 +107,43 @@ partial def LetValue.toMono (e : LetValue .pure) (resultFVar : FVarId) : ToMonoM
       unreachable!
     else if let some (.ctorInfo ctorInfo) := (← getEnv).find? declName then
       if let some info ← hasTrivialStructure? ctorInfo.induct then
-        args[ctorInfo.numParams + info.fieldIdx]!.toLetValue.toMono resultFVar
+        args[ctorInfo.numParams + info.fieldIdx]!.toLetValue.toMono
       else
-        ctorAppToMono resultFVar ctorInfo args
+        ctorAppToMono ctorInfo args
     else
       let env ← getEnv
-      if isNoncomputable env declName && !(isExtern env declName) then
-        modify fun s => { s with noncomputableVars := s.noncomputableVars.insert resultFVar declName }
       if let some monoDecl ← getMonoDecl? declName then
         if args.size >= monoDecl.params.size then
           if let .code (.let { fvarId := resultFVar, value := .const callName _ callArgs, .. }
                              (.return retFVar)) := monoDecl.value then
             let redArgDeclName := declName ++ `_redArg
             if callName == redArgDeclName && retFVar == resultFVar then
-              let args ← argsToMonoRedArg resultFVar args monoDecl.params callArgs
+              let args ← argsToMonoRedArg args monoDecl.params callArgs
               return .const redArgDeclName [] args
-        let args ← argsToMonoWithFnType resultFVar args monoDecl.type
+        let args ← argsToMonoWithFnType args monoDecl.type
         return .const declName [] args
       else
-        let args ← args.mapM (argToMonoDeferredCheck resultFVar)
+        let args ← args.mapM argToMono
         return .const declName [] args
   | .fvar fvarId args =>
     if (← get).typeParams.contains fvarId then
       return .erased
     else
-      checkFVarUseDeferred resultFVar fvarId
-      return .fvar fvarId (← args.mapM (argToMonoDeferredCheck resultFVar))
-  | .proj structName fieldIdx baseFVar =>
-    if (← get).typeParams.contains baseFVar then
+      return .fvar fvarId (← args.mapM argToMono)
+  | .proj structName fieldIdx fvarId =>
+    if (← get).typeParams.contains fvarId then
       return .erased
-    else
-      checkFVarUseDeferred resultFVar baseFVar
-      if let some info ← hasTrivialStructure? structName then
-        if info.fieldIdx == fieldIdx then
-          return .fvar baseFVar #[]
-        else
-          return .erased
+    else if let some info ← hasTrivialStructure? structName then
+      if info.fieldIdx == fieldIdx then
+        return .fvar fvarId #[]
       else
-        return e
+        return .erased
+    else
+      return e
 
 def LetDecl.toMono (decl : LetDecl .pure) : ToMonoM (LetDecl .pure) := do
   let type ← toMonoType decl.type
-  let value ← decl.value.toMono decl.fvarId
+  let value ← decl.value.toMono
   decl.update type value
 
 def mkFieldParamsForComputedFields (ctorType : Expr) (numParams : Nat) (numNewFields : Nat)
@@ -370,11 +347,8 @@ partial def Code.toMono (code : Code .pure) : ToMonoM (Code .pure) := do
   | .fun decl k | .jp decl k => return code.updateFun! (← decl.toMono) (← k.toMono)
   | .unreach type => return .unreach (← toMonoType type)
   | .jmp fvarId args => return code.updateJmp! fvarId (← args.mapM argToMono)
-  | .return fvarId =>
-    checkFVarUse fvarId
-    return code
+  | .return .. => return code
   | .cases c =>
-    checkFVarUse c.discr
     if h : c.typeName == ``Decidable then
       decToMono c h
     else if h : c.typeName == ``Nat then

src/Lean/Compiler/LCNF/Visibility.lean

@@ -9,6 +9,8 @@ prelude
 public import Lean.Compiler.ImplementedByAttr
 import Lean.ExtraModUses
 import Lean.Compiler.Options
+import Lean.Compiler.NoncomputableAttr
+import Lean.AddDecl
 
 public section
 
@@ -139,7 +141,7 @@ where go (origDecl decl : Decl .pure) : StateT NameSet CompilerM Unit := do
     for ref in collectUsedDecls code do
       if (← get).contains ref then
         continue
-      modify (·.insert decl.name)
+      modify (·.insert ref)
       if let some localDecl := baseExt.getState (← getEnv) |>.find? ref then
         -- check transitively through local decls
         if isPrivateName localDecl.name && (← localDecl.isTemplateLike) then

tests/lean/run/10213.lean

@@ -12,7 +12,7 @@ error: invalid 'csimp' theorem, only constant replacement theorems (e.g., `@f =
 theorem bad_csimp : @funnyChoice.{0} = @id.{0} := rfl
 
 /--
-error: Tactic `native_decide` failed. Error: failed to compile definition, compiler IR check failed at `_example._nativeDecide_1._closed_0`. Error: depends on declaration 'funnyChoice', which has no executable code; consider marking definition as 'noncomputable'
+error: Tactic `native_decide` failed. Error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'funnyChoice', which is 'noncomputable'
 -/
 #guard_msgs in
 example : False := by

tests/lean/run/9806.lean

@@ -2,4 +2,5 @@ def foo : Squash (Unit → Bool) := .mk fun _ => false
 
 def bar : Squash Bool := foo.lift fun f => .mk !f ()
 
-#eval IO.println bar.lcInv
+set_option trace.Compiler.result true in
+#eval unsafeCast (β := Bool) bar

tests/lean/run/noncomputableUnused.lean

@@ -1,7 +1,7 @@
-@[noinline]
+@[macro_inline]
 noncomputable def noncomp (a : Nat) : Nat := a
 
-@[noinline]
+@[macro_inline]
 def f (_ b : Nat) : Nat := b
 
 def g (b : Nat) := f (noncomp 0) b

tests/lean/run/pow_exploit.lean

@@ -5,13 +5,13 @@ This was once an exploit of a bug in the Lean kernel relying on the Lean kernel
 falsely interpreting an expression as a Nat literal.
 -/
 
-def g.{u} : PUnit.{u} → Nat := fun _ => open Classical in if Type = Type then 0 else 0
+noncomputable def g.{u} : PUnit.{u} → Nat := fun _ => open Classical in if Type = Type then 0 else 0
 
 -- Just writing `Nat.pow (Nat.pow 10 8) 502` would also work; `Nat.pow (Nat.pow 10 8) 503` wouldn't
 def T : Nat → Prop := fun x => if x = 0 then False else True
 
 -- The kernel reduces this to a number between 10^8032 and 10^8048
-def POW! := Nat.pow (g.{0} ⟨⟩) 1
+noncomputable def POW! := Nat.pow (g.{0} ⟨⟩) 1
 
 elab "#inject_bad_proof" : command => do
   let decl : Lean.Declaration := .defnDecl {

tests/lean/run/unsafeInit.lean

@@ -1 +1 @@
-unsafe initialize no : Nat ← pure lcUnreachable
+unsafe initialize no : Nat ← pure (unsafeCast (0 : Nat))

tests/lean/run/usesOfNoncomputable.lean

@@ -46,7 +46,7 @@ universe u
 def Erased (α : Sort u) : Sort max 1 u :=
   { s : α → Prop // ∃ a, (a = ·) = s }
 
-def Erased.mk {α} (a : α) : Erased α :=
+@[macro_inline] def Erased.mk {α} (a : α) : Erased α :=
   ⟨fun b => a = b, a, rfl⟩
 
 noncomputable def Erased.out {α} : Erased α → α