typeclass instance problem is stuck

Stream: lean4

[Kevin Buzzard]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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 :-(