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

[Alexandre Rademaker]

why I am having this error in the abbrev declaration?

import Std.Data.HashMap

namespace Test

variable {α β : Type} [Inhabited α] [Inhabited β]
  [BEq α] [BEq β] [Hashable α] [Hashable β]

structure Candidate where
  id          : α
  preferences : List β
deriving Repr, Inhabited

structure Post where
  id          : β
  capacity    : Nat
  preferences : List α
deriving Repr, Inhabited

structure MatchState where
  free        : List α
  proposals   : Std.HashMap (α × β) Bool
  assignments : Std.HashMap β (List α)
deriving Repr, Inhabited

abbrev GS := StateRefT MatchState IO

end Test

[Aaron Liu]

Since α and β are generalized out of MatchState you will have to provide them again

[Aaron Liu]

like this

abbrev GS := StateRefT (@MatchState α β _ _ _ _) IO

[Alexandre Rademaker]

It works, but I didn't understand the "generalized out of MatchState..."

[Edward van de Meent]

the issue is in two parts: firstly, instead of having @MatchState : Type, we have @MatchState : {α : Type} -> {β : Type} -> ... -> Type, due to how variable works. As a result, when you write StateRefT MatchState IO, lean creates metavariables for the α and β arguments, and then tries to synthesize the instances, but fails as the types are metavariables (so in particular it doesn't know if it should choose β or Rat or Real or what have you). the fix is telling lean explicitly what the type arguments are.

[Kyle Miller]

Design-wise, it would be much better to make alpha and beta be explicit arguments for these structures.

[Kyle Miller]

There's no way for Lean to infer alpha and beta