Zulip Chat Archive

Stream: lean4

Topic: typeclass instance problem is stuck


Kevin Buzzard (Dec 24 2022 at 20:49):

I'm trying to investigate why we're sometime seeing big slowdowns in construction of structure instances in the mathlib4 port. I'm wondering if the following has anything to do with it. This Lean 3 code works:

-- lean 3

class CompleteLattice (α : Type _).

class Frame (α : Type _) extends CompleteLattice α.

instance Pi.completeLattice {α : Type _} {β : α  Type _} [ i, CompleteLattice (β i)] :
    CompleteLattice ( i, β i) := { }

instance Pi.frame {α : Type _} {β : α  Type _} [ i, Frame (β i)] : Frame ( i, β i) :=
  { ..Pi.completeLattice } -- works

and gets ported to this Lean 4 code which doesn't work, but which can be fixed by making beta explicit:

class CompleteLattice (α : Type _) where

class Frame (α : Type _) extends CompleteLattice α where

instance Pi.completeLattice {α : Type _} {β : α  Type _} [ i, CompleteLattice (β i)] :
    CompleteLattice ( i, β i) := { }

instance Pi.frame {α : Type _} {β : α  Type _} [ i, Frame (β i)] : Frame ( i, β i) :=
  { Pi.completeLattice with } -- fails
/-
typeclass instance problem is stuck, it is often due to metavariables
  (i : ?m.181) → CompleteLattice (?m.182 i)
-/

-- try making β explicit
instance Pi.completeLattice' {α : Type _} (β : α  Type _) [ i, CompleteLattice (β i)] :
    CompleteLattice ( i, β i) := { }

instance Pi.frame' {α : Type _} {β : α  Type _} [ i, Frame (β i)] : Frame ( i, β i) :=
  { Pi.completeLattice' β with } -- now works

I'm wondering if this has anything to do with an issue I raised about this. Should we expect Pi.frame to work in Lean 4?

Eric Wieser (Dec 24 2022 at 21:13):

So instance search is now affected by the implicitness of arguments on the instance? I think we're very sloppy about this in Lean3 because it made no difference

Mario Carneiro (Dec 24 2022 at 21:49):

I don't think the implicitness itself matters, but the two examples differ not only by that - the second example has beta passed to the instance and the first one has _ passed

Mario Carneiro (Dec 24 2022 at 21:50):

the first example also works if you pass beta:

instance Pi.frame {α : Type _} {β : α  Type _} [ i, Frame (β i)] : Frame ( i, β i) :=
  { Pi.completeLattice (β := β) with } -- ok

Mario Carneiro (Dec 24 2022 at 21:53):

I don't see how the first version can be made to work. The thing before with is elaborated without expected type, because it can have arbitrary type. Even if we did give it a type it would presumably be Frame (∀ i, β i) (presuming this is a structure update) rather than CompleteLattice (∀ i, β i).

Mario Carneiro (Dec 24 2022 at 21:55):

In this example, you don't need to give the Pi.completeLattice with part in the first place - { } also works

Kevin Buzzard (Dec 24 2022 at 22:38):

this works though, and there's not enough information to work out the type. It is mysteriously slow though (like the preceding instance), although I just tried adding the types explicitly and it doesn't make it any quicker :-(


Last updated: Dec 20 2023 at 11:08 UTC