Unknown error while type-checking with `use`

Stream: general

[Kenji Nakagawa]

For some reason, lean just dies after the use M line, and sometimes (eventually?), you can get unknown error while type-checking theorem (this might not be verbatim), although interestingly, using tauto at that point doesn't throw this error (also this seems to have been an error with a week ago mathlib, as well as current). Additionally, having R being an integral domain resolves this.

import ring_theory.fractional_ideal

lemma nonfield_has_prime (R : Type*) [comm_ring R] (nonfield : ∃(I : ideal R), ⊥ < I ∧ I < ⊤ ) : ∃(P : ideal R), P.is_prime ∧ ⊥ < P :=
begin
  rcases nonfield with ⟨I, gt_bot, lt_top⟩,
  have ne_top : I ≠ ⊤, exact ne_of_lt lt_top,
  rcases ideal.exists_le_maximal I ne_top with ⟨M, maximal, gei⟩,
  have hm := ideal.is_maximal.is_prime maximal,
  have gt_bot : ⊥ < M, exact gt_of_ge_of_gt gei gt_bot,
  use M,
   --exact ideal.is_maximal.is_prime maximal, exact gt_bot,
  --tauto,
end

[Alex J. Best]

Try refine ⟨M, _, _⟩, instead for now

[Kevin Buzzard]

existsi M is something else which sometimes works

[Bryan Gin-ge Chen]

There's definitely something weird here. For me, the yellow bars just don't go away if the use M, line is present. If I comment it out then Lean quickly finishes.

[Bryan Gin-ge Chen]

existsi M and refine ⟨M, _, _⟩, work though.

[Kevin Buzzard]

This is the well-known "use bug"; use was written because existsi was bad at type unification; I've never seen a situation where neither of them work ;-)

[Rob Lewis]

I think I've asked before for a #mwe of the "well-known use bug," preferably as a mathlib issue so it doesn't get lost. Ideally the example has fewer imports than this one.

[Rob Lewis]

The problem in this case is that the elaborator doesn't recognize that M itself isn't a proof of ∃ (P : ideal R), P.is_prime ∧ ⊥ < P. You can see that refine M times out too.

[Rob Lewis]

Why? I have no idea. The elaborator trace options aren't helping at all.

[Mario Carneiro]

Minimized:

example (R : Type*) [comm_ring R] : true :=
by { suffices M : submodule R R, exact M }

[Mario Carneiro]

It is fast if you provide ring or semiring instead

[Mario Carneiro]

It is also fast with R : Type instead of R : Type*, so maybe it has something to do with the universe unification

[Rob Lewis]

Hmm, with what imports? This is fast:

import algebra.module.submodule

example (R : Type*) [comm_ring R] : true :=
by { suffices M : submodule R R, exact M }

[Mario Carneiro]

import ring_theory.fractional_ideal

universe u
example (R : Type u) [comm_ring R] : true :=
by { suffices M : submodule R R, exact M }

[Mario Carneiro]

it's something in localization

[Mario Carneiro]

src#localization_map.coe_submodules

[Rob Lewis]

Looks like a coercion instance going wrong.

[Mario Carneiro]

yeah this is a bad instance, that coe can loop and it leaves f free

[Mario Carneiro]

#3832

[Rob Lewis]

Maybe add a comment explaining why it's not an instance?