fix: skip value if type is computationally irrelevant

src/library/compiler/erase_irrelevant.cpp

@@ -405,7 +405,7 @@ class erase_irrelevant_fn {
             expr fvar  = m_lctx.mk_local_decl(ngen(), n, t, v);
             curr_fvars.push_back(fvar);
             expr new_t = mk_runtime_type(t);
-            expr new_v = visit(v);
+            expr new_v = is_enf_neutral(new_t) ? mk_enf_neutral() : visit(v);
             m_let_fvars.push_back(fvar);
             m_let_entries.emplace_back(n, new_t, new_v);
             e = let_body(e);

tests/lean/run/mjissue.lean

@@ -0,0 +1,12 @@
+def Family (α : Type _) (n : Nat) := Inhabited (Fin n → α)
+
+def all_but_last {α} {n} (f : Family α (n + 1)) : Family α n :=
+Inhabited.mk λ k => f.default ⟨k.val, Nat.lt_trans k.isLt n.lt_succ_self⟩
+
+def all : {n : Nat} → Family Prop n → Prop
+| 0, _ => True
+| n + 1, f => all (all_but_last f)
+
+def th : (n : Nat) → (f : Family Prop n) → Decidable (all f)
+| 0, f => isTrue ⟨⟩
+| n + 1, f => th n (all_but_last f)