type class issues

Stream: general

[Johan Commelin]

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]

[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]

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

[Reid Barton]

can we use instance priority to guide the search here?

[Reid Barton]

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

[Johan Commelin]

@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]

Well, it did find it here, eventually

[Reid Barton]

Everything looks more or less fine until the max depth error

[Johan Commelin]

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]

Because that would find punit.category instantly...

[Johan Commelin]

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]

I really doubt how this will scale

[Kenny Lau]

as we get more things into mathlib

[Mario Carneiro]

I think category_theory.small_category is misnamed...

[Reid Barton]

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]

@Mario Carneiro Can you elaborate?

[Johan Commelin]

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]

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
Additional information:
/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]

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

[Johan Commelin]

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

[Kenny Lau]

@Mario Carneiro talk about is_ring_hom.is_ring_hom

[Mario Carneiro]

what is that even?

[Kenny Lau]

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

[Kenny Lau]

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]

guess how this would be called

[Kenny Lau]

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

[Reid Barton]

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]

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

[Kenny Lau]

I mean, who on earth put it there

[Kenny Lau]

you don't need any classical stuff for subrings

[Reid Barton]

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]

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

[Mario Carneiro]

Authors: Johan Commelin

[Kenny Lau]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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]

I think we need to refactor the typeclass search system

[Kenny Lau]

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

[Kenny Lau]

so I might have said nothing in the first place

[Reid Barton]

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]

:four_leaf_clover:

[Kenny Lau]

I think the instance search is as stupid as simp

[Mario Carneiro]

it's much worse than simp

[Kenny Lau]

and we still haven't fixed the problem with simp

[Kenny Lau]

for the love of god

[Kenny Lau]

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

[Kenny Lau]

but I don't study CS

[Mario Carneiro]

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]

at least not without forking lean

[Reid Barton]

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]

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

[Reid Barton]

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]

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

[Mario Carneiro]

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]

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]

git grep "^instance" | wc -l
1515

[Mario Carneiro]

that last one is obviously problematic

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

are we satisfied with "it will eventually terminate"?

[Mario Carneiro]

it's an important first step

[Mario Carneiro]

the next question is "how finite" of course

[Mario Carneiro]

and this depends on how much typeclass caching lean does

[Mario Carneiro]

so I'm not sure on the details

[Mario Carneiro]

We want it to be mostly linear

[Johan Commelin]

How about prioritizing type 1? Like Reid suggested?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

Oh I forgot about parent coercions.

[Kenny Lau]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

yes

[Reid Barton]

So then there are also things like preorder to category

[Mario Carneiro]

yes

[Reid Barton]

And I guess both of those fall under type 2

[Mario Carneiro]

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

[Kenny Lau]

@Mario Carneiro how does this work in metamath?

[Mario Carneiro]

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]

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

[Mario Carneiro]

It's all third party stuff though

[Johan Commelin]

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

[Mario Carneiro]

this is emphatically not part of "metamath core"

[Mario Carneiro]

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

[Mario Carneiro]

I have hope for reid's proposal

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

C is the class

[Reid Barton]

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

[Mario Carneiro]

I called C the head there

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

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]

(instance C a => D a is illegal)

[Mario Carneiro]

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

[Reid Barton]

With GHC extensions

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

this is okay

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

that's the same as in lean

[Reid Barton]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

Maybe lean should do that too

[Mario Carneiro]

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

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

Basically, yeah.

[Mario Carneiro]

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]

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

[Johan Commelin]

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]

welcome to the club :P

[Johan Commelin]

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]

@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]

@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]

@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]

@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]

@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]

These are just workarounds.

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Leonardo de Moura]

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]

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.