Possible Bug

Stream: general

[James Shaker]

Hello, I’m one of @Scott Morrison 's students and I’ve got what could possibly be an issue in mathlib. I was wondering if others would be willing to take a look before I file a bug report on GitHub:

import ring_theory.algebra -- commenting this out fixes the problem

def power_series (α : Type) [comm_ring α] := ℕ → α

variables {α : Type} [comm_ring α]

def of_alpha (x : α) : power_series α
| 0 := x
| _ := 0

instance : has_coe α (power_series α) := ⟨of_alpha⟩

example (x : α) : power_series α := (x : power_series α) -- can't find defined instance

As described in the comments, the simple coercion from α to power_series α fails despite the instance being clearly defined on the line above. What’s more it works correctly when the algebra import is commented.

[Johan Commelin]

Where do you want to file a bug report? Lean doesn't take bug reports.... didn't Scott tell you this?

[Johan Commelin]

These kind of issues are really quite annoying. I don't spot anything obviously wrong.

[Johan Commelin]

Aaah I do!

[Mario Carneiro]

You shouldn't use has_coe for these kinds of coercions, it will cause lean to go in a loop

[Mario Carneiro]

There's some discussion about the coercion for option A in the file in core

[Mario Carneiro]

use has_coe_t instead

[Mario Carneiro]

I did not get a "can't find instance" error, I get a instance resolution depth overflow

[Mario Carneiro]

Oh, there is a bad instance in group_theory.coset, instance : has_coe α (quotient s) := ⟨mk⟩

[James Shaker]

Sorry that's the same issue I get, just forgot to include the specifics of the bug

[James Shaker]

has_coe_t doesn't seem to fix the issue

[James Shaker]

@Johan Commelin I think Scott was referring to posting an issue on the GitHub repo but I'm not 100% sure..

[Johan Commelin]

If you want to post issues, please post them here: https://github.com/leanprover-community/lean

[Johan Commelin]

Aaahrg! Stupid copy paste buffer fixed the link

[Johan Commelin]

Anyway, the best way to deal with such issues is by posting them here :grinning:

[Mario Carneiro]

this isn't a lean problem it's a mathlib problem

[Mario Carneiro]

it's some typeclass architecture bug

[Mario Carneiro]

but I suspect the result will be that you can't define this coercion

[James Shaker]

Should we just turn off that instance (in group_theory.coset)?

[Mario Carneiro]

working on it

[Mario Carneiro]

but I think the power_series coercion is also a bad instance

[Mario Carneiro]

for similar reasons

[James Shaker]

ok so it would be safe if I used has_coe_t?

[James Shaker]

for power_series?

[Mario Carneiro]

basically, lean will try to eagerly apply transitivity paths from the left for has_coe, so you end up reducing the problem has_coe A B to has_coe (power_series A) B and then has_coe (power_series (power_series A)) B, etc

[Mario Carneiro]

using has_coe_t will ensure that it will only apply the instance once

[Mario Carneiro]

it looks like removing the quotient_group.mk instance fixes the problem

[James Shaker]

Can I try PR-ing that, or are you already there?

[Mario Carneiro]

#1028

[Johan Commelin]

Can we use regexes to see if there are more of those evil instances in mathlib?

[Mario Carneiro]

Don't you know not to use regex for things it wasn't designed for? https://stackoverflow.com/a/1732454/890016

[Kevin Buzzard]

#1028

Even mathematicians, the most coe-est people around, usually use notation for passage to the quotient; they usually put some sort of bar over the thing they're coercing.

[Chris Hughes]

Do mathematicians use non injective coes?

[Kevin Buzzard]

That's an interesting question.

[Kevin Buzzard]

I think that sometimes mathematicians use the localization map $R\to R[1/S]$ as a coercion, perhaps because in most cases it's injective.

[Reid Barton]

How about $\mathbb{Z} \to \mathbb{Z}/n$

[Kevin Buzzard]

We coerce numerals but in general I might be tempted to write $\overline{x}$ for the image of $x\in\mathbb{Z}$. Or am I just being naive?

[Reid Barton]

I guess I had numerals in mind