fix: compiler constant folding bug for Bool (#13989)

This PR fixes a bug in the constant folding for `Bool` wherein the
compiler incorrectly determined
0-ary functions that participate in constant folding to be equal to
`false`.

Author: hargoniX

src/Lean/Compiler/LCNF/Simp/ConstantFold.lean

@@ -89,8 +89,11 @@ instance : Literal String where
   mkLit := mkStringLit
 
 def getBoolLit (fvarId : FVarId) : CompilerM (Option Bool) := do
-  let some (.const ctor [] #[]) ← findLetValue? fvarId | return none
-  return ctor == ``Bool.true
+  let some (.const name [] #[]) ← findLetValue? fvarId | return none
+  match name with
+  | ``Bool.true => return some true
+  | ``Bool.false => return some false
+  | _ => return none
 
 def mkBoolLit (b : Bool) : FolderM (LetValue .pure) :=
   let ctor := if b then ``Bool.true else ``Bool.false

tests/elab/compile_bool_const_fold_bug.lean

@@ -0,0 +1,10 @@
+/-! This is a regression test for a bug in the LCNF simp constant folder for Bool -/
+
+@[noinline]
+def myBool := true
+
+def a := (Bool.decEq myBool true).decide
+
+/-- info: true -/
+#guard_msgs in
+#eval a