From 5253cc6742e1f3860cd5039fdd694a4282f92080 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 24 Jul 2022 12:36:08 -0700
Subject: [PATCH] fix: compiler support for `FloatArray.casesOn` and
 `ByteArray.casesOn`

closes #1311
---
 src/library/compiler/erase_irrelevant.cpp | 12 ++++++++++++
 tests/lean/run/1311.lean                  |  7 +++++++
 2 files changed, 19 insertions(+)
 create mode 100644 tests/lean/run/1311.lean

diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index 26928e0a60..47a4081964 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -219,6 +219,16 @@ class erase_irrelevant_fn {
                            binding_body(minor));
     }
 
+    expr elim_scalar_array_cases(buffer<expr> & args) {
+        lean_always_assert(args.size() == 3);
+        expr major       = visit(args[1]);
+        expr minor       = visit_minor(args[2]);
+        lean_always_assert(is_lambda(minor));
+        return
+            ::lean::mk_let(next_name(), mk_enf_object_type(), major,
+                           binding_body(minor));
+    }
+
     expr elim_uint_cases(name const & uint_name, buffer<expr> & args) {
         lean_always_assert(args.size() == 3);
         expr major = visit(args[1]);
@@ -254,6 +264,8 @@ class erase_irrelevant_fn {
             return elim_int_cases(args);
         } else if (I_name == get_array_name()) {
             return elim_array_cases(args);
+        } else if (I_name == get_float_array_name() || I_name == get_byte_array_name()) {
+            return elim_scalar_array_cases(args);
         } else if (I_name == get_uint8_name() || I_name == get_uint16_name() || I_name == get_uint32_name() || I_name == get_uint64_name() || I_name == get_usize_name()) {
           return elim_uint_cases(I_name, args);
         } else if (I_name == get_decidable_name()) {
diff --git a/tests/lean/run/1311.lean b/tests/lean/run/1311.lean
new file mode 100644
index 0000000000..bb6c57d758
--- /dev/null
+++ b/tests/lean/run/1311.lean
@@ -0,0 +1,7 @@
+instance : DecidableEq ByteArray
+  | ⟨a⟩, ⟨b⟩ => match decEq a b with
+    | isTrue h₁  => isTrue $ congrArg ByteArray.mk h₁
+    | isFalse h₂ => isFalse $ fun h => by cases h; cases (h₂ rfl)
+
+#eval ByteArray.empty = ByteArray.empty
+#eval ByteArray.empty != ByteArray.empty.push 5