## Stream: general

### Topic: Unknown error while type-checking with use

#### Kenji Nakagawa (Aug 16 2020 at 18:16):

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 (Aug 16 2020 at 18:23):

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

#### Kevin Buzzard (Aug 16 2020 at 18:25):

existsi M is something else which sometimes works

#### Bryan Gin-ge Chen (Aug 16 2020 at 18:30):

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 (Aug 16 2020 at 18:31):

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

#### Kevin Buzzard (Aug 16 2020 at 19:20):

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 (Aug 16 2020 at 19:45):

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 (Aug 16 2020 at 20:01):

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 (Aug 16 2020 at 20:02):

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

#### Mario Carneiro (Aug 16 2020 at 20:48):

Minimized:

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


#### Mario Carneiro (Aug 16 2020 at 20:49):

It is fast if you provide ring or semiring instead

#### Mario Carneiro (Aug 16 2020 at 20:51):

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

#### Rob Lewis (Aug 16 2020 at 20:54):

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 (Aug 16 2020 at 20:55):

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 (Aug 16 2020 at 20:57):

it's something in localization

#### Mario Carneiro (Aug 16 2020 at 20:59):

src#localization_map.coe_submodules

#### Rob Lewis (Aug 16 2020 at 20:59):

Looks like a coercion instance going wrong.

#### Mario Carneiro (Aug 16 2020 at 21:01):

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

#3832

#### Rob Lewis (Aug 16 2020 at 21:06):

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

Last updated: Dec 20 2023 at 11:08 UTC