equation compiler failing

Stream: general

[Sky Wilshaw]

The equation compiler keeps on giving me the same error message:

equation compiler failed to create auxiliary declaration 'f_map_core._main._pack'
nested exception message:
infer type failed, unknown variable
  H

This error happens in a variety of cases, and I can't find a good minimal example. In the simplest case, I have a hypothesis hy which exactly matches the goal, and replacing a sorry with exact hy causes this error to be emitted. Does anyone know some general tips for helping the equation compiler understand what I've written?

[Mario Carneiro]

this needs a #mwe

[Mario Carneiro]

it might have something to do with mutual recursion, it is difficult to understand what is happening without an example

[Sky Wilshaw]

Yeah, unfortunately whenever I try to minify my example the problem goes away - the strange thing is that I never use the variable H at all so it must be internal to the equation compiler

[Mario Carneiro]

then minify everything else?

[Sky Wilshaw]

Thanks for your help, the issue's fixed now. It turns out that the equation compiler was also failing due to issues related to a well-founded relation - I thought the errors were independent but after solving the latter, the former went away.

[Mario Carneiro]

I still would like to see an example, because it sounds like a bug

[Sky Wilshaw]

noncomputable def test : ℕ → ℕ
| x := have this : {i : ℕ | ∀ y (hyx : y < x), have y < x, from hyx, test y ≠ i}.nonempty, begin
    by_contradiction,
    have hfinite : {i : ℕ | ∃ y < x, have y < x := ‹_›, test y = i}.finite := sorry,
    rw ← cardinal.lt_aleph_0_iff_finite at hfinite,
    have : ℵ₀ = #{i : ℕ | ∃ y < x, have y < x := ‹_›, test y = i}
      + #{i : ℕ | ∀ y < x, have y < x := ‹_›, test y ≠ i},
    { rw ← cardinal.mk_nat,
      rw ← cardinal.mk_univ,
      rw ← cardinal.mk_union_of_disjoint,
      congr',
      rw set.union_def,
      refine (set.eq_univ_of_forall (λ z, _)).symm,
      dsimp,
      by_cases ∃ (y : ℕ) (H : y < x), test y = z,
      { left, exact h },
      { right, push_neg at h, exact h },
      sorry },
    rw set.not_nonempty_iff_eq_empty at h,
    rw h at this,
    simp at this, rw this at hfinite,
    simp at hfinite, exact hfinite
  end, this.some

This has an incorrect proof that recursive applications are decreasing - the important thing is that the first error emitted by lean is the equation compiler one.

[Sky Wilshaw]

It can probably still be reduced, but I don't have time for that right now

[Mario Carneiro]

what are the imports?

[Sky Wilshaw]

I think

import data.set.basic
import set_theory.cardinal.basic

open_locale cardinal

should suffice