feat: opaque_repr attr to suppress "trivial structure" opt (pt 2)

Author: digama0

Diff for: src/Init/Core.lean

@@ -38,6 +38,7 @@ attribute [simp] namedPattern
   Thunks are "lazy" values that are evaluated when first accessed using `Thunk.get/map/bind`.
   The value is then stored and not recomputed for all further accesses. -/
 -- NOTE: the runtime has special support for the `Thunk` type to implement this behavior
+@[opaque_repr]
 structure Thunk (α : Type u) : Type u where
   /-- Constructs a new thunk from a function `Unit → α`
   that will be called when the thunk is forced. -/
@@ -359,6 +360,7 @@ possibly being computed on another thread. This is similar to `Future` in Scala,
 
 The tasks have an overridden representation in the runtime.
 -/
+@[opaque_repr]
 structure Task (α : Type u) : Type u where
   /-- `Task.pure (a : α)` constructs a task that is already resolved with value `a`. -/
   pure ::

Diff for: src/Init/Data/ByteArray/Basic.lean

@@ -10,6 +10,7 @@ import Init.Data.UInt.Basic
 import Init.Data.Option.Basic
 universe u
 
+@[opaque_repr]
 structure ByteArray where
   data : Array UInt8
 

Diff for: src/Init/Data/Float.lean

@@ -26,6 +26,7 @@ opaque floatSpec : FloatSpec := {
   decLe := fun _ _ => inferInstanceAs (Decidable True)
 }
 
+@[opaque_repr]
 structure Float where
   val : floatSpec.float
 

Diff for: src/Init/Data/FloatArray/Basic.lean

@@ -9,6 +9,7 @@ import Init.Data.Float
 import Init.Data.Option.Basic
 universe u
 
+@[opaque_repr]
 structure FloatArray where
   data : Array Float
 

Diff for: src/Init/Data/Int/Basic.lean

@@ -37,6 +37,7 @@ and larger numbers use an arbitrary precision "bignum" library
 (usually [GMP](https://gmplib.org/)). A "small number" is an integer
 that can be encoded with 63 bits (31 bits on 32-bits architectures).
 -/
+@[opaque_repr]
 inductive Int : Type where
   /-- A natural number is an integer (`0` to `∞`). -/
   | ofNat   : Nat → Int

Diff for: src/Init/Prelude.lean

@@ -1041,6 +1041,7 @@ This type is special-cased by both the kernel and the compiler:
   to 2^63 directly and larger numbers use an arbitrary precision "bignum"
   library (usually [GMP](https://gmplib.org/)).
 -/
+@[opaque_repr]
 inductive Nat where
   /-- `Nat.zero`, normally written `0 : Nat`, is the smallest natural number.
   This is one of the two constructors of `Nat`. -/
@@ -1820,6 +1821,7 @@ abbrev UInt8.size : Nat := 256
 The type of unsigned 8-bit integers. This type has special support in the
 compiler to make it actually 8 bits rather than wrapping a `Nat`.
 -/
+@[opaque_repr]
 structure UInt8 where
   /-- Unpack a `UInt8` as a `Nat` less than `2^8`.
   This function is overridden with a native implementation. -/
@@ -1859,6 +1861,7 @@ abbrev UInt16.size : Nat := 65536
 The type of unsigned 16-bit integers. This type has special support in the
 compiler to make it actually 16 bits rather than wrapping a `Nat`.
 -/
+@[opaque_repr]
 structure UInt16 where
   /-- Unpack a `UInt16` as a `Nat` less than `2^16`.
   This function is overridden with a native implementation. -/
@@ -1898,6 +1901,7 @@ abbrev UInt32.size : Nat := 4294967296
 The type of unsigned 32-bit integers. This type has special support in the
 compiler to make it actually 32 bits rather than wrapping a `Nat`.
 -/
+@[opaque_repr]
 structure UInt32 where
   /-- Unpack a `UInt32` as a `Nat` less than `2^32`.
   This function is overridden with a native implementation. -/
@@ -1974,6 +1978,7 @@ abbrev UInt64.size : Nat := 18446744073709551616
 The type of unsigned 64-bit integers. This type has special support in the
 compiler to make it actually 64 bits rather than wrapping a `Nat`.
 -/
+@[opaque_repr]
 structure UInt64 where
   /-- Unpack a `UInt64` as a `Nat` less than `2^64`.
   This function is overridden with a native implementation. -/
@@ -2040,6 +2045,7 @@ for the platform's architecture.
 For example, if running on a 32-bit machine, USize is equivalent to UInt32.
 Or on a 64-bit machine, UInt64.
 -/
+@[opaque_repr]
 structure USize where
   /-- Unpack a `USize` as a `Nat` less than `USize.size`.
   This function is overridden with a native implementation. -/
@@ -2323,6 +2329,7 @@ def List.get {α : Type u} : (as : List α) → Fin as.length → α
 The compiler overrides the data representation of this type to a byte sequence,
 and both `String.utf8ByteSize` and `String.length` are cached and O(1).
 -/
+@[opaque_repr]
 structure String where
   /-- Pack a `List Char` into a `String`. This function is overridden by the
   compiler and is O(n) in the length of the list. -/
@@ -2547,6 +2554,7 @@ as they are used "linearly" all updates will be performed destructively on the
 array, so it has comparable performance to mutable arrays in imperative
 programming languages.
 -/
+@[opaque_repr]
 structure Array (α : Type u) where
   /-- Convert a `List α` into an `Array α`. This function is overridden
   to `List.toArray` and is O(n) in the length of the list. -/

Diff for: tests/lean/opaqueReprAttr.lean

@@ -0,0 +1,40 @@
+namespace MkAndValAreOptimizedAway
+
+structure MyZero where
+  val : Nat
+
+def MyZero.valImpl (_self : MyZero) : Nat := 0
+attribute [implemented_by MyZero.valImpl] MyZero.val
+
+unsafe def MyZero.mkImpl (_val : Nat) : MyZero := unsafeCast 0
+attribute [implemented_by MyZero.mkImpl] MyZero.mk
+
+#eval (MyZero.mk 1).val -- 1
+
+end MkAndValAreOptimizedAway
+
+namespace UsingAttr
+
+@[opaque_repr]
+structure MyZero where
+  val : Nat
+
+def MyZero.valImpl (_self : MyZero) : Nat := 0
+attribute [implemented_by MyZero.valImpl] MyZero.val
+
+unsafe def MyZero.mkImpl (_val : Nat) : MyZero := unsafeCast 0
+attribute [implemented_by MyZero.mkImpl] MyZero.mk
+
+#eval (MyZero.mk 1).val -- 0
+
+-- FIXME: it would be nice if we didn't have to override casesOn too
+@[inline] def MyZero.casesOnImpl {motive : MyZero → Sort u} (t : MyZero)
+    (mk : ∀ val, motive { val }) : motive t := mk _
+attribute [implemented_by MyZero.casesOnImpl] MyZero.casesOn
+
+-- we need a blackBox here because the compiler will optimize
+-- `(MyZero.mk n).casesOn f` to `f n` otherwise (and this is desirable, even for opaque_repr types)
+@[noinline] def blackBox := @id
+#eval ((blackBox (MyZero.mk 1)).casesOn fun n => n : Nat) -- 0
+
+end UsingAttr

Diff for: tests/lean/opaqueReprAttr.lean.expected.out

@@ -0,0 +1,3 @@
+1
+0
+0