## Stream: general

### Topic: type class issues

#### Johan Commelin (Nov 14 2018 at 19:54):

This is amazing: https://gist.githubusercontent.com/jcommelin/8736c28a8e74f3d478b1c2b7737fa513/raw/d655018af064ef75572afb17d2ffb7d051c500c0/crazy_type_class_error.lean
I feel like the algorithm could be a lot smarter here. For example, search for x_52 on that page, and go to the first match. You will be on the last line of this chunk of code:

[class_instances] (1) ?x_32 : category
(@comma {X // B X}
(@category_theory.full_subcategory (@opens X _inst_1)
(@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1))
(λ (X : @opens X _inst_1), B X))
punit
category_theory.punit_category
(@opens X _inst_1)
(@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1))
(@full_subcategory_inclusion (@opens X _inst_1)
(@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1))
B)
(@functor.of_obj (@opens X _inst_1) (@site.to_category (@opens X _inst_1) (@category_theory.site X _inst_1)) U)) := @category_theory.comma_category ?x_51 ?x_52 ?x_53 ?x_54 ?x_55 ?x_56 ?x_57 ?x_58


So basically it has already figured out all these type class instances, and it should immediately be able to fill in ?x_52 and friends. But it doesn't... and then it hits the search limit.

#### Johan Commelin (Nov 14 2018 at 20:10):

[class_instances] (4) ?x_238 : category punit := @category_theory.small_category ?x_422 ?x_423


goes all the way down to

[class_instances] (12) ?x_460 : linear_ordered_field punit := @discrete_linear_ordered_field.to_linear_ordered_field ?x_461 ?x_462


I guess it might be a good idea to insert a shortcut somewhere?

#### Reid Barton (Nov 14 2018 at 20:12):

looks like the actual solution is category punit := category_theory.punit_category

#### Reid Barton (Nov 14 2018 at 20:13):

can we use instance priority to guide the search here?

#### Reid Barton (Nov 14 2018 at 20:14):

the funny thing is that punitactually has a unique structure of all those classes it looks for

#### Johan Commelin (Nov 14 2018 at 20:15):

@Reid Barton I'm really confused, because a lot of the time it is finding that instance. But that sometimes it goes astray...

#### Reid Barton (Nov 14 2018 at 20:15):

Well, it did find it here, eventually

#### Reid Barton (Nov 14 2018 at 20:16):

Everything looks more or less fine until the max depth error

#### Johan Commelin (Nov 14 2018 at 20:18):

Hmmm, would it be good strategy if Lean is searching for an instance of foo bar to first check if maybe bar.foo exists?

#### Johan Commelin (Nov 14 2018 at 20:18):

Because that would find punit.category instantly...

#### Johan Commelin (Nov 14 2018 at 20:24):

Ahrg, this is so annoying. So now I can start writing lots of @ signs, and insert the typeclass instances manually, and the code becomes unreadable...

#### Kenny Lau (Nov 14 2018 at 20:27):

I really doubt how this will scale

#### Kenny Lau (Nov 14 2018 at 20:27):

as we get more things into mathlib

#### Mario Carneiro (Nov 14 2018 at 20:29):

I think category_theory.small_category is misnamed...

#### Reid Barton (Nov 14 2018 at 20:32):

Either :four_leaf_clover: will have to improve the instance search algorithm, or we will have to start being more careful about how we write instances, with other tradeoffs

#### Johan Commelin (Nov 14 2018 at 20:33):

@Mario Carneiro Can you elaborate?

#### Johan Commelin (Nov 14 2018 at 20:33):

I now have

obj := λ U, @limit _ (@category_theory.opposite _
(@category_theory.comma_category _ _ _ category_theory.punit_category _ _ _ _)) _ _
((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ⋙ F) _,


and I get red squiggles under the ⋙ at the end.

#### Johan Commelin (Nov 14 2018 at 20:34):

Errors:

failed to synthesize type class instance for
X : Type v,
_inst_1 : topological_space X,
B : set (opens X),
C : Type u,
𝒞 : category C,
F : category_theory.presheaf ↥B C,
U : opens Xᵒᵖ
⊢ category comma (full_subcategory_inclusion B) (functor.of_obj U)ᵒᵖ
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
⁇
inferred
category_theory.opposite
sheaf.lean:414:66: error

failed to synthesize type class instance for
X : Type v,
_inst_1 : topological_space X,
B : set (opens X),
C : Type u,
𝒞 : category C,
F : category_theory.presheaf ↥B C,
U : opens Xᵒᵖ
⊢ category comma (full_subcategory_inclusion B) (functor.of_obj U)ᵒᵖ
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
⁇
inferred
category_theory.opposite
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
𝒞
inferred
?m_1
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
𝒞
inferred
?m_1
/home/jmc/data/math/community-mathlib/category_theory/sheaf.lean:415:20: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
type mismatch, term
limits.limit.pre ?m_7 ?m_9
has type
limits.limit ?m_5 ⟶ limits.limit (?m_9 ⋙ ?m_5) : Type ?
but is expected to have type
⁇ U₁ ⟶ ⁇ U₂ : Type v
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
𝒞
inferred
?m_1
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
𝒞
inferred
?m_1
sheaf.lean:414:66: error

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
𝒞
inferred
?m_1


#### Reid Barton (Nov 14 2018 at 20:34):

instance [preorder α] : small_category α := ... got the name category_theory.small_category

#### Johan Commelin (Nov 14 2018 at 20:35):

Aaah, that's not so nice. That should be in the preorder namespace.

#### Kenny Lau (Nov 14 2018 at 20:35):

@Mario Carneiro talk about is_ring_hom.is_ring_hom

#### Mario Carneiro (Nov 14 2018 at 20:36):

what is that even?

#### Kenny Lau (Nov 14 2018 at 20:37):

https://github.com/leanprover/mathlib/blob/master/ring_theory/subring.lean#L28

#### Kenny Lau (Nov 14 2018 at 20:37):

namespace is_ring_hom

instance {S : set R} [is_subring S] : is_ring_hom (@subtype.val R S) :=
by refine {..} ; intros ; refl

end is_ring_hom


#### Kenny Lau (Nov 14 2018 at 20:37):

guess how this would be called

#### Kenny Lau (Nov 14 2018 at 20:38):

also what on earth is it with the local attribute [instance] classical.prop_decidable

#### Reid Barton (Nov 14 2018 at 20:38):

There's also some bug where Lean's normal naming strategy for an instance is not used under certain circumstances (I'm not sure exactly which)

#### Mario Carneiro (Nov 14 2018 at 20:39):

classical.prop_decidable existed long before classical.dec, I think it's in the style guide and TPIL

#### Kenny Lau (Nov 14 2018 at 20:39):

I mean, who on earth put it there

#### Kenny Lau (Nov 14 2018 at 20:39):

you don't need any classical stuff for subrings

#### Reid Barton (Nov 14 2018 at 20:39):

We could have a strategy where we don't write instances like instance [preorder α] : small_category α, but rather instance [preorder α] : small_category (preorder α), where def preorder α := α

#### Mario Carneiro (Nov 14 2018 at 20:40):

maybe it was needed once, or a mathematician wrote the file

#### Mario Carneiro (Nov 14 2018 at 20:40):

Authors: Johan Commelin


#### Kenny Lau (Nov 14 2018 at 20:41):

but curiously he was never part of the file's history

#### Reid Barton (Nov 14 2018 at 20:41):

That would cut out all the silly search starting preorder punit (actually it is not really silly, since punit could very well be a preorder, but anyways we want a different instance)

#### Mario Carneiro (Nov 14 2018 at 20:42):

I think we need to think about a more principled approach to instance priorities

#### Mario Carneiro (Nov 14 2018 at 20:44):

for preorder categories, I guess it depends on whether you view it as "a preorder is a special kind of category" or "any preorder can be equipped with a canonical category structure"

#### Kenny Lau (Nov 14 2018 at 20:44):

I think we need to refactor the typeclass search system

#### Kenny Lau (Nov 14 2018 at 20:44):

but I don't know how any of those things work

#### Kenny Lau (Nov 14 2018 at 20:45):

so I might have said nothing in the first place

#### Reid Barton (Nov 14 2018 at 20:45):

Well I'm not necessarily thinking about anything as anything, I just want to avoid these 20 pages of failed instance searches whenever I try to look for a category instance which is after the preorder one.

#### Mario Carneiro (Nov 14 2018 at 20:45):

:four_leaf_clover:

#### Kenny Lau (Nov 14 2018 at 20:45):

I think the instance search is as stupid as simp

#### Mario Carneiro (Nov 14 2018 at 20:45):

it's much worse than simp

#### Kenny Lau (Nov 14 2018 at 20:45):

and we still haven't fixed the problem with simp

#### Kenny Lau (Nov 14 2018 at 20:45):

for the love of god

#### Kenny Lau (Nov 14 2018 at 20:46):

who thought depth first search is a good idea (instance) and who thought breadth first search is a good idea (simp)

#### Kenny Lau (Nov 14 2018 at 20:46):

but I don't study CS

#### Mario Carneiro (Nov 14 2018 at 20:47):

But it's not a tactic, it's built into lean, so there is very little customization or alternatives we can try in lean 3

#### Mario Carneiro (Nov 14 2018 at 20:47):

at least not without forking lean

#### Reid Barton (Nov 14 2018 at 20:48):

OK here is a thought. What if we by convention give each instance which doesn't match against the head a lower priority

#### Reid Barton (Nov 14 2018 at 20:48):

i.e. each instance of the form \Pi a, ... : C a

#### Reid Barton (Nov 14 2018 at 20:49):

Because of course we want to match against things like ... : C (T a) first, if we're trying to find an instance C (T ...)

#### Kenny Lau (Nov 14 2018 at 20:49):

@Mario Carneiro but from your CS experience, what is the best search method?

#### Mario Carneiro (Nov 14 2018 at 20:49):

There are two essentially different kinds of instances: "parent coercions" that change the head, and things that change the type to something smaller and leave the head alone

#### Mario Carneiro (Nov 14 2018 at 20:50):

we know the search terminates in the second case because it's well founded on the structure construction, and in the first case because our tree of classes is finite

#### Johan Commelin (Nov 14 2018 at 20:50):

git grep "^instance" | wc -l
1515


#### Mario Carneiro (Nov 14 2018 at 20:50):

that last one is obviously problematic

#### Mario Carneiro (Nov 14 2018 at 20:50):

because it gets worse as you add more things anywhere in mathlib

#### Kenny Lau (Nov 14 2018 at 20:51):

I think TREE(3) is also finite so I don't really get your point

#### Kenny Lau (Nov 14 2018 at 20:51):

are we satisfied with "it will eventually terminate"?

#### Mario Carneiro (Nov 14 2018 at 20:52):

it's an important first step

#### Mario Carneiro (Nov 14 2018 at 20:52):

the next question is "how finite" of course

#### Mario Carneiro (Nov 14 2018 at 20:52):

and this depends on how much typeclass caching lean does

#### Mario Carneiro (Nov 14 2018 at 20:52):

so I'm not sure on the details

#### Mario Carneiro (Nov 14 2018 at 20:53):

We want it to be mostly linear

#### Johan Commelin (Nov 14 2018 at 20:53):

How about prioritizing type 1? Like Reid suggested?

#### Mario Carneiro (Nov 14 2018 at 20:54):

Parent coercions have a fixed priority, I don't think we can change it

#### Mario Carneiro (Nov 14 2018 at 20:54):

This is one place where I think lean is using the wrong search strategy btw

#### Reid Barton (Nov 14 2018 at 20:55):

Oh I forgot about parent coercions.

#### Kenny Lau (Nov 14 2018 at 20:55):

we don't we ask the big guys about the typeclass system in lean 4?

#### Mario Carneiro (Nov 14 2018 at 20:56):

If we call type coercions type 1 and parent / "head changing" coercions type 2, then I think we should use backward chaining for type 1 and forward chaining for type 2

#### Mario Carneiro (Nov 14 2018 at 20:57):

For example, if you prove that ordered_field real then lean will pre-calculate proofs of preorder real and a bunch of other stuff

#### Reid Barton (Nov 14 2018 at 20:57):

Are we talking about actual parent coercions like from group to monoid?

yes

#### Reid Barton (Nov 14 2018 at 20:57):

So then there are also things like preorder to category

yes

#### Reid Barton (Nov 14 2018 at 20:58):

And I guess both of those fall under type 2

#### Mario Carneiro (Nov 14 2018 at 20:58):

and if you have ordered_field A in the context then it calculates preorder A when solving typeclass problems

#### Kenny Lau (Nov 14 2018 at 20:58):

@Mario Carneiro how does this work in metamath?

#### Mario Carneiro (Nov 14 2018 at 21:00):

You get to do this stuff yourself, but there is a smallish spine so it's at most two or three theorem applications to get from anything to anything else

#### Mario Carneiro (Nov 14 2018 at 21:00):

the backward chaining stuff might be done automatically in later versions?

#### Mario Carneiro (Nov 14 2018 at 21:01):

It's all third party stuff though

#### Johan Commelin (Nov 14 2018 at 21:01):

So is there any hope we can improve the system in Lean 3?

#### Mario Carneiro (Nov 14 2018 at 21:01):

this is emphatically not part of "metamath core"

#### Mario Carneiro (Nov 14 2018 at 21:01):

priorities seem like the best option, but we need a good rule

#### Mario Carneiro (Nov 14 2018 at 21:02):

I have hope for reid's proposal

#### Reid Barton (Nov 14 2018 at 21:03):

The obvious, but more annoying variant is to raise the priority of every "type 1" instance

#### Johan Commelin (Nov 14 2018 at 21:04):

I think Mario said that those were fixed... but maybe I misunderstood which type he referred to...

#### Reid Barton (Nov 14 2018 at 21:04):

I'm also a little confused about Mario's description of the two types

#### Reid Barton (Nov 14 2018 at 21:04):

In Haskell, if we have an instance C (T a b), we call T the instance head

C is the class

#### Reid Barton (Nov 14 2018 at 21:05):

I'm not sure whether Mario is using the same terminology, or switched the classes or what

#### Mario Carneiro (Nov 14 2018 at 21:05):

I called C the head there

#### Mario Carneiro (Nov 14 2018 at 21:06):

so parent coercions change the head, i.e. C a => D a

#### Mario Carneiro (Nov 14 2018 at 21:06):

and type coercions are like C a , C b => C (T a b)

#### Reid Barton (Nov 14 2018 at 21:08):

I might be wrong in assuming instances like C a, C b => C (T a b) are more common in mathlib--in standard Haskell they're the only kind of instances you are allowed to write

#### Reid Barton (Nov 14 2018 at 21:08):

(instance C a => D a is illegal)

#### Mario Carneiro (Nov 14 2018 at 21:08):

That's not true, I think you can do parent coercions in Haskell too

#### Reid Barton (Nov 14 2018 at 21:09):

With GHC extensions

#### Reid Barton (Nov 14 2018 at 21:09):

But the effect is probably like 99% of all instances are of the C (T a b) form

#### Mario Carneiro (Nov 14 2018 at 21:12):

oh, I see, there are parent coercions but no user defined parent coercions

#### Mario Carneiro (Nov 14 2018 at 21:12):

class Test a where
test :: a -> a
class Test a => Test2 a where
test2 :: a -> a


this is okay

#### Reid Barton (Nov 14 2018 at 21:12):

There isn't even a coercion in the same sense as in Lean

#### Reid Barton (Nov 14 2018 at 21:13):

There, to write a Test2 instance, you must first write a Test instance

#### Reid Barton (Nov 14 2018 at 21:13):

The purpose of Test a => Test2 a is instead to avoid writing contexts like (Test a, Test2 a) => t

#### Mario Carneiro (Nov 14 2018 at 21:13):

that's the same as in lean

#### Reid Barton (Nov 14 2018 at 21:14):

Oh, well... I guess Lean hides the need to write the Test instance separately

#### Mario Carneiro (Nov 14 2018 at 21:14):

class Test (a : Type) := (test : a → a)
class Test2 (a : Type) extends Test a := (test2 : a → a)

instance : Test nat := {test := id}
instance : Test2 nat := {test2 := id} --requires the first instance


#### Reid Barton (Nov 14 2018 at 21:15):

But you can also write instance : Test2 nat := {test := id, test2 := id} without the first instance, which has no equivalent in Haskell

#### Mario Carneiro (Nov 14 2018 at 21:16):

Maybe lean should do that too

#### Mario Carneiro (Nov 14 2018 at 21:16):

that is essentially requiring the user to do the forward chaining thing I said

#### Reid Barton (Nov 14 2018 at 21:16):

I actually don't know off-hand how GHC solves a Test a constraint if you only have Test2 in the context

#### Reid Barton (Nov 14 2018 at 21:17):

I wouldn't be surprised if it does forward chaining in that situation

#### Mario Carneiro (Nov 14 2018 at 21:18):

you mean when you have test :: Test2 a => a -> a?

Basically, yeah.

#### Mario Carneiro (Nov 14 2018 at 21:24):

I think it is complete in Haskell's case to always saturate downwards (derive all superclasses of all the things in the context) and then backward chain from uses (without using any parent coercions)

#### Johan Commelin (Nov 15 2018 at 09:48):

Aahrg, Lean is just becoming completely unresponsive when I try to fill in the instances by hand.

#### Johan Commelin (Nov 15 2018 at 09:49):

Look at the code that I have now: this is getting pretty crazy...

def extend : presheaf X C :=
{ obj := λ U, @limit.{u v} _ (@category_theory.opposite.{v v} _
(@category_theory.comma_category.{v v v v v v}
_ (category_theory.full_subcategory.{v v} _)
_ category_theory.punit_category.{v}
_ (@site.to_category.{v} (@opens.{v} X _inst_1) (@category_theory.site.{v} X _inst_1)) _ _))
_ _
((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ⋙ F)
(limits.has_limit_of_has_limits_of_shape.{u v} _),
map := _ }


#### Kenny Lau (Nov 15 2018 at 09:54):

welcome to the club :P

#### Johan Commelin (Nov 15 2018 at 10:03):

Ok, I need to confess. I'm making a big fool out of myself. There was actually a missing assumption... so no wonder Lean couldn't find the instance. The code is now back to

def extend : presheaf X C :=
{ obj := λ U, limit ((comma.fst (full_subcategory_inclusion B) (functor.of_obj U)).op ⋙ F),
map := _ }


However it is still taking >10s to typecheck this stuff. Before I removed all the explicit instances, it also took >10s.

#### Leonardo de Moura (Nov 16 2018 at 05:23):

@Johan Commelin

Johan Commelin: So is there any hope we can improve the system in Lean 3?

To improve Lean 3, you need to fork it, and improve it yourself. The development is frozen in the main repo, and all efforts are focused on Lean 4. That being said, nobody should expect Lean 4 will solve all problems and everybody will be happy.

#### Leonardo de Moura (Nov 16 2018 at 05:25):

@Kenny Lau

Kenny Lau: we don't we ask the big guys about the typeclass system in lean 4?

We didn't get there yet. We have only random ideas on how to improve the typeclass system in lean 4.

#### Leonardo de Moura (Nov 16 2018 at 05:27):

@Kenny Lau

Kenny Lau: I think we need to refactor the typeclass search system

If you want a better typeclass system in the next few months, you should fork the current system, and refactor the typeclass search system yourself.

#### Johan Commelin (Nov 16 2018 at 05:33):

@Leonardo de Moura Ok, I was hoping that maybe we could use priorities to guide the type class system. Anyway, thanks for the input! And thanks for all you're doing for Lean (3 and 4).

#### Leonardo de Moura (Nov 16 2018 at 05:36):

@Johan Commelin Yes, priorities will help. Shortcuts will help too. Example: https://github.com/leanprover/lean/blob/master/library/init/data/int/basic.lean#L418-L429

#### Leonardo de Moura (Nov 16 2018 at 05:37):

These are just workarounds.

#### Mario Carneiro (Nov 16 2018 at 07:07):

It's not clear to me how much shortcuts actually help, though, because they make the typeclass graph even larger

#### Mario Carneiro (Nov 16 2018 at 07:08):

if you have instances from A -> B -> C and add a shortcut A -> C, then a typeclass search for some unrelated F will traverse both paths to C (and possibly the entire subtree rooted at C)

#### Mario Carneiro (Nov 16 2018 at 07:09):

Are there any plans for lean 4 to do anything with the typeclass system?

#### Leonardo de Moura (Nov 16 2018 at 07:20):

You can add the shortcuts using local attributes. In this way, you can add shortcuts to a file without affecting other files.

#### Leonardo de Moura (Nov 16 2018 at 07:21):

Sebastian and I discussed a few improvements (e.g., better indexing and caching), but as I said above these are just ideas on the whiteboard. We didn’t get there yet.

Last updated: May 11 2021 at 23:11 UTC