From 7fbe8e3b36faabc9cfcc45e65a4b7ef042c0b068 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 20 Nov 2024 11:43:59 +0100
Subject: [PATCH] fix: `Inhabited Float` produced a bogus run-time value
 (#6136)

This PR fixes the run-time evaluation of `(default : Float)`.
---
 src/Init/Data/Float.lean               | 5 ++++-
 tests/compiler/float.lean              | 1 +
 tests/compiler/float.lean.expected.out | 1 +
 3 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/Float.lean b/src/Init/Data/Float.lean
index 3cdae65126..65ee6eb7d5 100644
--- a/src/Init/Data/Float.lean
+++ b/src/Init/Data/Float.lean
@@ -31,7 +31,7 @@ opaque floatSpec : FloatSpec := {
 structure Float where
   val : floatSpec.float
 
-instance : Inhabited Float := ⟨{ val := floatSpec.val }⟩
+instance : Nonempty Float := ⟨{ val := floatSpec.val }⟩
 
 @[extern "lean_float_add"] opaque Float.add : Float → Float → Float
 @[extern "lean_float_sub"] opaque Float.sub : Float → Float → Float
@@ -136,6 +136,9 @@ instance : ToString Float where
 
 @[extern "lean_uint64_to_float"] opaque UInt64.toFloat (n : UInt64) : Float
 
+instance : Inhabited Float where
+  default := UInt64.toFloat 0
+
 instance : Repr Float where
   reprPrec n prec := if n < UInt64.toFloat 0 then Repr.addAppParen (toString n) prec else toString n
 
diff --git a/tests/compiler/float.lean b/tests/compiler/float.lean
index 60caceed68..5ed1451e2d 100644
--- a/tests/compiler/float.lean
+++ b/tests/compiler/float.lean
@@ -15,6 +15,7 @@ def tst1 : IO Unit := do
   IO.println (Float.ofInt 0)
   IO.println (Float.ofInt 42)
   IO.println (Float.ofInt (-42))
+  IO.println (default : Float)
   IO.println (0 / 0 : Float).toUInt8
   IO.println (0 / 0 : Float).toUInt16
   IO.println (0 / 0 : Float).toUInt32
diff --git a/tests/compiler/float.lean.expected.out b/tests/compiler/float.lean.expected.out
index a4f8f92625..24730774a9 100644
--- a/tests/compiler/float.lean.expected.out
+++ b/tests/compiler/float.lean.expected.out
@@ -13,6 +13,7 @@ true
 0.000000
 42.000000
 -42.000000
+0.000000
 0
 0
 0