fix: make sure OfScientific Float instance is never unfolded during…

… type class resolution

This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818

Type class resolution was diverging when trying to synthesize
```lean
 HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
```
and Lean was diverging while unfolding
```lean
 instance : OfScientific Float where
   ofScientific m s e :=
     if s then
       let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
       let m := (m <<< (3 * e + s)) / 5^e
       Float.ofBinaryScientific m (-4 * e - s)
     else
       Float.ofBinaryScientific (m * 5^e) e
```
was being unfolded.

Anothe potential solution for the problem above is to erase the
`optParam` annotations before performing type class resolution.

src/Init/Data/OfScientific.lean

@@ -23,6 +23,14 @@ def Float.ofBinaryScientific (m : Nat) (e : Int) : Float :=
   let e := e + s
   m.toFloat.scaleB e
 
+protected opaque Float.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float :=
+  if s then
+    let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
+    let m := (m <<< (3 * e + s)) / 5^e
+    Float.ofBinaryScientific m (-4 * e - s)
+  else
+    Float.ofBinaryScientific (m * 5^e) e
+
 /-
   The `OfScientifi Float` must have priority higher than `mid` since
   the default instance `Neg Int` has `mid` priority.
@@ -32,13 +40,7 @@ def Float.ofBinaryScientific (m : Nat) (e : Int) : Float :=
 -/
 @[defaultInstance mid+1]
 instance : OfScientific Float where
-  ofScientific m s e :=
-    if s then
-      let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
-      let m := (m <<< (3 * e + s)) / 5^e
-      Float.ofBinaryScientific m (-4 * e - s)
-    else
-      Float.ofBinaryScientific (m * 5^e) e
+  ofScientific := Float.ofScientific
 
 @[export lean_float_of_nat]
 def Float.ofNat (n : Nat) : Float :=

tests/lean/run/floatOptParam.lean

@@ -0,0 +1 @@
+def foo (a : Float := 0.0) (b : Float := 1.0) : Float := a - b