fix: move the new compiler's noncomputable check into toMono (#8523)

This PR moves the new compiler's noncomputable check into toMono,
matching the recent change in the old compiler. This is mildly more
complicated because we can't throw an error at the mere use of a
constant, we need to check for a later relevant use. This is still a bit
more conservative than it could theoretically be around join points and
local functions, but it's hard to imagine that mattering in practice
(and we can easily enable it if it does).

src/Lean/Compiler/LCNF/ToMono.lean

@@ -4,13 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Compiler.ExternAttr
 import Lean.Compiler.LCNF.MonoTypes
 import Lean.Compiler.LCNF.InferType
+import Lean.Compiler.NoncomputableAttr
 
 namespace Lean.Compiler.LCNF
 
 structure ToMonoM.State where
   typeParams : FVarIdSet := {}
+  noncomputableVars : FVarIdMap Name := {}
 
 abbrev ToMonoM := StateRefT ToMonoM.State CompilerM
 
@@ -24,6 +27,11 @@ def isTrivialConstructorApp? (declName : Name) (args : Array Arg) : ToMonoM (Opt
   let some info ← hasTrivialStructure? ctorInfo.induct | return none
   return args[ctorInfo.numParams + info.fieldIdx]!.toLetValue
 
+def checkFVarUse (fvarId : FVarId) : ToMonoM Unit := do
+  if (← get).noncomputableVars.contains fvarId then
+    let declName := (← get).noncomputableVars.find! fvarId
+    throwError f!"failed to compile definition, consider marking it as 'noncomputable' because it depends on '{declName}', which is 'noncomputable'"
+
 def argToMono (arg : Arg) : ToMonoM Arg := do
   match arg with
   | .erased | .type .. => return .erased
@@ -31,6 +39,7 @@ def argToMono (arg : Arg) : ToMonoM Arg := do
     if (← get).typeParams.contains fvarId then
       return .erased
     else
+      checkFVarUse fvarId
       return arg
 
 def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array Arg) : ToMonoM LetValue := do
@@ -42,7 +51,7 @@ def ctorAppToMono (ctorInfo : ConstructorVal) (args : Array Arg) : ToMonoM LetVa
   let argsNew := argsNew ++ (← args[ctorInfo.numParams:].toArray.mapM argToMono)
   return .const ctorInfo.name [] argsNew
 
-partial def LetValue.toMono (e : LetValue) : ToMonoM LetValue := do
+partial def LetValue.toMono (e : LetValue) (fvarId : FVarId) : ToMonoM LetValue := do
   match e with
   | .erased | .lit .. => return e
   | .const declName _ args =>
@@ -55,30 +64,36 @@ partial def LetValue.toMono (e : LetValue) : ToMonoM LetValue := do
       -- and Bool have the same runtime representation.
       return args[1]!.toLetValue
     else if let some e' ← isTrivialConstructorApp? declName args then
-      e'.toMono
+      e'.toMono fvarId
     else if let some (.ctorInfo ctorInfo) := (← getEnv).find? declName then
       ctorAppToMono ctorInfo args
     else
+      let env ← getEnv
+      if isNoncomputable env declName && !(isExtern env declName) then
+        modify fun s => { s with noncomputableVars := s.noncomputableVars.insert fvarId declName }
       return .const declName [] (← args.mapM argToMono)
   | .fvar fvarId args =>
     if (← get).typeParams.contains fvarId then
       return .erased
     else
+      checkFVarUse fvarId
       return .fvar fvarId (← args.mapM argToMono)
   | .proj structName fieldIdx fvarId =>
     if (← get).typeParams.contains fvarId then
       return .erased
-    else if let some info ← hasTrivialStructure? structName then
-      if info.fieldIdx == fieldIdx then
-        return .fvar fvarId #[]
-      else
-        return .erased
     else
-      return e
+      checkFVarUse fvarId
+      if let some info ← hasTrivialStructure? structName then
+        if info.fieldIdx == fieldIdx then
+          return .fvar fvarId #[]
+        else
+          return .erased
+      else
+        return e
 
 def LetDecl.toMono (decl : LetDecl) : ToMonoM LetDecl := do
   let type ← toMonoType decl.type
-  let value ← decl.value.toMono
+  let value ← decl.value.toMono decl.fvarId
   decl.update type value
 
 mutual
@@ -222,8 +237,11 @@ partial def Code.toMono (code : Code) : ToMonoM Code := 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 .. => return code
+  | .return fvarId =>
+    checkFVarUse fvarId
+    return code
   | .cases c =>
+    checkFVarUse c.discr
     if h : c.typeName == ``Decidable then
       decToMono c h
     else if h : c.typeName == ``Nat then