## Stream: general

### Topic: Possible Bug

#### James Shaker (May 14 2019 at 04:34):

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 (May 14 2019 at 04:35):

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

#### Johan Commelin (May 14 2019 at 04:36):

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

Aaah I do!

#### Mario Carneiro (May 14 2019 at 04:41):

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

#### Mario Carneiro (May 14 2019 at 04:41):

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

#### Mario Carneiro (May 14 2019 at 04:41):

use has_coe_t instead

#### Mario Carneiro (May 14 2019 at 04:42):

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

#### Mario Carneiro (May 14 2019 at 04:47):

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

#### James Shaker (May 14 2019 at 04:47):

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

#### James Shaker (May 14 2019 at 04:48):

has_coe_t doesn't seem to fix the issue

#### James Shaker (May 14 2019 at 04:49):

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

#### Johan Commelin (May 14 2019 at 04:51):

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

#### Johan Commelin (May 14 2019 at 04:51):

Aaahrg! Stupid copy paste buffer fixed the link

#### Johan Commelin (May 14 2019 at 04:52):

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

#### Mario Carneiro (May 14 2019 at 04:52):

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

#### Mario Carneiro (May 14 2019 at 04:53):

it's some typeclass architecture bug

#### Mario Carneiro (May 14 2019 at 04:53):

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

#### James Shaker (May 14 2019 at 04:54):

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

working on it

#### Mario Carneiro (May 14 2019 at 04:54):

but I think the power_series coercion is also a bad instance

#### Mario Carneiro (May 14 2019 at 04:54):

for similar reasons

#### James Shaker (May 14 2019 at 04:54):

ok so it would be safe if I used has_coe_t?

#### James Shaker (May 14 2019 at 04:54):

for power_series?

#### Mario Carneiro (May 14 2019 at 04:55):

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 (May 14 2019 at 04:55):

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

#### Mario Carneiro (May 14 2019 at 04:56):

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

#### James Shaker (May 14 2019 at 04:59):

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

#1028

#### Johan Commelin (May 14 2019 at 05:08):

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

#### Mario Carneiro (May 14 2019 at 05:10):

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

#### Kevin Buzzard (May 14 2019 at 17:54):

#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 (May 14 2019 at 17:57):

Do mathematicians use non injective coes?

#### Kevin Buzzard (May 14 2019 at 18:13):

That's an interesting question.

#### Kevin Buzzard (May 14 2019 at 18:14):

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 (May 14 2019 at 18:15):

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

#### Kevin Buzzard (May 14 2019 at 18:17):

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 (May 14 2019 at 18:17):

I guess I had numerals in mind

Last updated: May 11 2021 at 00:31 UTC