feat: opaque_repr attribute to suppress "trivial structure" opt

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 ::

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
 

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
 

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
 

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

src/Init/Prelude.lean

@@ -1035,6 +1035,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`. -/
@@ -1780,6 +1781,7 @@ def 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. -/
@@ -1819,6 +1821,7 @@ def 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. -/
@@ -1858,6 +1861,7 @@ def 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. -/
@@ -1934,6 +1938,7 @@ def 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. -/
@@ -1985,6 +1990,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. -/
@@ -2268,6 +2274,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. -/
@@ -2492,6 +2499,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. -/

src/Lean/Compiler.lean

@@ -10,6 +10,7 @@ import Lean.Compiler.ClosedTermCache
 import Lean.Compiler.ExternAttr
 import Lean.Compiler.ImplementedByAttr
 import Lean.Compiler.NeverExtractAttr
+import Lean.Compiler.OpaqueReprAttr
 import Lean.Compiler.IR
 import Lean.Compiler.CSimpAttr
 import Lean.Compiler.FFI

src/Lean/Compiler/LCNF/MonoTypes.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.InferType
+import Lean.Compiler.OpaqueReprAttr
 import Lean.Compiler.LCNF.Util
 import Lean.Compiler.LCNF.BaseTypes
 import Lean.Compiler.LCNF.CompilerM
@@ -41,7 +42,7 @@ Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
 - This constructor has only one computationally relevant field.
 -/
 def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do
-  if isRuntimeBultinType declName then return none
+  if hasOpaqueReprAttribute (← getEnv) declName then return none
   let .inductInfo info ← getConstInfo declName | return none
   if info.isUnsafe || info.isRec then return none
   let [ctorName] := info.ctors | return none
@@ -128,4 +129,4 @@ def getOtherDeclMonoType (declName : Name) : CoreM Expr := do
     modifyEnv fun env => monoTypeExt.modifyState env fun s => { s with mono := s.mono.insert declName type }
     return type
 
-end Lean.Compiler.LCNF
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.ProjFns
 import Lean.Compiler.BorrowedAnnotation
+import Lean.Compiler.OpaqueReprAttr
 import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Bind
 import Lean.Compiler.LCNF.InferType
@@ -644,7 +645,7 @@ where
 
   visitProjFn (projInfo : ProjectionFunctionInfo) (e : Expr) : M Arg := do
     let typeName := projInfo.ctorName.getPrefix
-    if isRuntimeBultinType typeName then
+    if hasOpaqueReprAttribute (← getEnv) typeName then
       let numArgs := e.getAppNumArgs
       let arity := projInfo.numParams + 1
       if numArgs < arity then

src/Lean/Compiler/LCNF/Util.lean

@@ -72,22 +72,4 @@ def getCtorArity? (declName : Name) : CoreM (Option Nat) := do
   let .ctorInfo val ← getConstInfo declName | return none
   return val.numParams + val.numFields
 
-/--
-List of types that have builtin runtime support
--/
-def builtinRuntimeTypes : List Name := [
-  ``String,
-  ``UInt8, ``UInt16, ``UInt32, ``UInt64, ``USize,
-  ``Float,
-  ``Thunk, ``Task,
-  ``Array, ``ByteArray, ``FloatArray,
-  ``Nat, ``Int
-]
-
-/--
-Return `true` iff `declName` is the name of a type with builtin support in the runtime.
--/
-def isRuntimeBultinType (declName : Name) : Bool :=
-  builtinRuntimeTypes.contains declName
-
 end Lean.Compiler.LCNF

src/Lean/Compiler/OpaqueReprAttr.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Environment
+import Lean.Attributes
+
+namespace Lean
+
+builtin_initialize opaqueReprAttr : TagAttribute ←
+  registerTagAttribute `opaque_repr "instruct the compiler that this type has an opaque representation, and should not be treated as a wrapper type."
+
+@[export lean_has_opaque_repr_attribute]
+def hasOpaqueReprAttribute (env : Environment) (n : Name) : Bool :=
+  opaqueReprAttr.hasTag env n
+
+end Lean

src/library/compiler/lcnf.cpp

@@ -112,7 +112,7 @@ class to_lcnf_fn {
         name const & k        = pinfo.get_constructor();
         constructor_val k_val = env().get(k).to_constructor_val();
         name const & I_name   = k_val.get_induct();
-        if (is_runtime_builtin_type(I_name)) {
+        if (has_opaque_repr_attribute(env(), I_name)) {
             /* We should not expand projections of runtime builtin types */
             return visit_app_default(fn, args, root);
         } else {

src/library/compiler/util.cpp

@@ -376,24 +376,9 @@ bool is_llnf_void_type(expr const & e) {
     return e == *g_void_type;
 }
 
-bool is_runtime_builtin_type(name const & n) {
-    /* TODO(Leo): use an attribute? */
-    return
-        n == get_string_name() ||
-        n == get_uint8_name()  ||
-        n == get_uint16_name() ||
-        n == get_uint32_name() ||
-        n == get_uint64_name() ||
-        n == get_usize_name()  ||
-        n == get_float_name()  ||
-        n == get_thunk_name()  ||
-        n == get_task_name()   ||
-        n == get_array_name()  ||
-        n == get_mut_quot_name()  ||
-        n == get_byte_array_name()  ||
-        n == get_float_array_name()  ||
-        n == get_nat_name()    ||
-        n == get_int_name();
+extern "C" uint8 lean_has_opaque_repr_attribute(object* env, object *n);
+bool has_opaque_repr_attribute(environment const & env, name const & n) {
+    return lean_has_opaque_repr_attribute(env.to_obj_arg(), n.to_obj_arg());
 }
 
 bool is_runtime_scalar_type(name const & n) {
@@ -454,7 +439,7 @@ bool depends_on(expr const & e, name_hash_set const & s) {
 }
 
 optional<unsigned> has_trivial_structure(environment const & env, name const & I_name) {
-    if (is_runtime_builtin_type(I_name))
+    if (has_opaque_repr_attribute(env, I_name))
         return optional<unsigned>();
     inductive_val I_val = env.get(I_name).to_inductive_val();
     if (I_val.is_unsafe())

src/library/compiler/util.h

@@ -149,10 +149,10 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e);
 
 // =======================================
 
-/* Return true if `n` is the name of a type with builtin support in the code generator. */
-bool is_runtime_builtin_type(name const & n);
-inline bool is_runtime_builtin_type(expr const & e) {
-    return is_constant(e) && is_runtime_builtin_type(const_name(e));
+/* Return true if `n` has the `[opaque_repr]` attribute, used to suppress the 'trivial structure' optimization. */
+bool has_opaque_repr_attribute(environment const & env, name const & n);
+inline bool has_opaque_repr_attribute(environment const & env, expr const & e) {
+    return is_constant(e) && has_opaque_repr_attribute(env, const_name(e));
 }
 
 /* Return true if `n` is the name of a type that is treated as a scalar type by the code generator. */

src/library/constants.cpp

@@ -67,7 +67,6 @@ name const * g_ite = nullptr;
 name const * g_lc_proof = nullptr;
 name const * g_lc_unreachable = nullptr;
 name const * g_list = nullptr;
-name const * g_mut_quot = nullptr;
 name const * g_nat = nullptr;
 name const * g_nat_succ = nullptr;
 name const * g_nat_zero = nullptr;
@@ -237,8 +236,6 @@ void initialize_constants() {
     mark_persistent(g_lc_unreachable->raw());
     g_list = new name{"List"};
     mark_persistent(g_list->raw());
-    g_mut_quot = new name{"MutQuot"};
-    mark_persistent(g_mut_quot->raw());
     g_nat = new name{"Nat"};
     mark_persistent(g_nat->raw());
     g_nat_succ = new name{"Nat", "succ"};
@@ -385,7 +382,6 @@ void finalize_constants() {
     delete g_lc_proof;
     delete g_lc_unreachable;
     delete g_list;
-    delete g_mut_quot;
     delete g_nat;
     delete g_nat_succ;
     delete g_nat_zero;
@@ -491,7 +487,6 @@ name const & get_ite_name() { return *g_ite; }
 name const & get_lc_proof_name() { return *g_lc_proof; }
 name const & get_lc_unreachable_name() { return *g_lc_unreachable; }
 name const & get_list_name() { return *g_list; }
-name const & get_mut_quot_name() { return *g_mut_quot; }
 name const & get_nat_name() { return *g_nat; }
 name const & get_nat_succ_name() { return *g_nat_succ; }
 name const & get_nat_zero_name() { return *g_nat_zero; }

src/library/constants.h

@@ -69,7 +69,6 @@ name const & get_ite_name();
 name const & get_lc_proof_name();
 name const & get_lc_unreachable_name();
 name const & get_list_name();
-name const & get_mut_quot_name();
 name const & get_nat_name();
 name const & get_nat_succ_name();
 name const & get_nat_zero_name();

src/library/constants.txt

@@ -62,7 +62,6 @@ ite
 lcProof
 lcUnreachable
 List
-MutQuot
 Nat
 Nat.succ
 Nat.zero