type class inference fail

Stream: general

[Johan Commelin]

don't know how to synthesize placeholder
context:
R : Type,
_inst_1 : comm_ring.{0} R,
_inst_2 : topological_space.{0} R,
_inst_3 : @topological_ring.{0} R _inst_2 (@comm_ring.to_ring.{0} R _inst_1),
R₀ : set.{0} R,
_inst_4 : @is_subring R (@comm_ring.to_ring.{0} R _inst_1) R₀,
I : set.{0} (@coe_sort.{1 2} (set.{0} R) (@set.has_coe_to_sort.{0} R) R₀),
_inst_5 :
  @is_ideal.{0} (@coe_sort.{1 2} (set.{0} R) (@set.has_coe_to_sort.{0} R) R₀)
    (@subtype.comm_ring R (@comm_ring.to_ring.{0} R _inst_1) _inst_1 R₀ _inst_4)
    I
⊢ topological_space.{0} R

Why can this even fail?

[Kevin Buzzard]

Because type class inference is not looking at your context, maybe?

[Johan Commelin]

Right... so how is it ever supposed to figure things out if it doesn't look at my context?

[Kevin Buzzard]

example (G : Type) : comm_group G → ∀ a b : G, a * b = b * a :=
begin
admit
end

[Kevin Buzzard]

failed to synthesize type class instance for
G : Type,
a : comm_group G,
a b : G
⊢ has_mul G

[Kevin Buzzard]

The system doesn't look there

[Johan Commelin]

Shouldn't it?

[Kevin Buzzard]

That's not a question I'm qualified to answer

[Kevin Buzzard]

example (G : Type) [comm_group G] : ∀ a b : G, a * b = b * a :=
begin
admit
end

[Kevin Buzzard]

That works

[Kevin Buzzard]

the square brackets mean "add me to the type class inference system"

[Johan Commelin]

This feels extremely counterintuitive to me... after all, we go through pains to make sure there is only one instance of a class... so if there is one instance in my context there won't be any others. (I promise!)

[Kevin Buzzard]

However there are commands which explicitly add stuff to the type class inference system

[Sean Leather]

@Johan Commelin What does set_option pp.all true before that tell you?

[Kevin Buzzard]

Do you know about letI?

[Kevin Buzzard]

Maybe search for that in the type class inference thread

[Johan Commelin]

Aha, I don't know about letI.

[Kevin Buzzard]

I half-understand it

[Kevin Buzzard]

the main gotcha is that this is defined in mathlib

[Johan Commelin]

@Sean Leather I already have that set to true. You see it in the output.

[Kevin Buzzard]

so you have to import _some_ mathlib file before it works

[Johan Commelin]

Is this one of our mathematical promises playing up again?

[Kevin Buzzard]

stream:general topic:more+type+class+inference+issues leti

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/search/i.20would.20rather.20just.20make.20type.20class.20inference.20work.2E

[Kevin Buzzard]

Kenny teaching me about letI in pretty much the same situation

[Johan Commelin]

Right, so I insert

by haveI := topological_space R; exact

in the middle of my definition, and it works. Ugly!

[Kevin Buzzard]

I totally agree that it is ugly

[Kevin Buzzard]

And they have no plans to change it in Lean 4

[Kevin Buzzard]

Mario wrote all this letI and exactI and haveI when Leo made some non-trivial changes which broke a lot of stuff

[Kevin Buzzard]

For some reason, liberal type class inference was making Lean slow

[Kevin Buzzard]

for his application

[Kevin Buzzard]

so he made it stricter

[Kevin Buzzard]

and then a whole bunch of mathlib broke

[Kevin Buzzard]

and if this letI hack hadn't worked

[Kevin Buzzard]

then it would not surprise me if mathlib would still be broken

[Kevin Buzzard]

On the other hand

[Kevin Buzzard]

I'm not sure you can have "mathematician inference"

[Kevin Buzzard]

I think we're too clever

[Kevin Buzzard]

If you can formalise some nice MWE of something which you feel would be nice if it worked but doesn't work

[Kevin Buzzard]

then you could ask Sebastian or Mario why it doesn't work

[Kevin Buzzard]

but I fear the answer might be

[Kevin Buzzard]

something like "if that worked, then this important file would take 100 years to compile"

[Kevin Buzzard]

But I'm not sure, what happened with the changes to type class inference is beyond my pay grade