Typeclass timeout and outParam

Stream: lean4

[Tomas Skrivan]

I'm getting an odd timeout on typeclass resolution, it is a mix of addition on product type and usage of outParam. I don't really understand what is going on here, especially I do not understand what exactly outParam is doing but it is necessary here to allow the nice and simple notation ⟪x,y⟫

class SemiInner (X : Type u) (R : outParam $ Type v) where
  semiInner : X → X → R

notation "⟪" x ", " y "⟫" => SemiInner.semiInner x y

-- This is here to demonstrate the need of `outParam` in the `R` parameter
class SemiHilbert (X R) [Add R] extends Add X, SemiInner X R where
  add_inner : ∀ x y z : X, ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

instance (X Y R) [Add R] [SemiInner X R] [SemiInner Y R] : SemiInner (X × Y) R :=
{
  semiInner := λ (x,y) (x',y') => ⟪x,x'⟫ + ⟪y,y'⟫
}

class AddSemigroup (A : Type u) extends Add A where
  add_assoc (a b c : A) : (a + b) + c = a + (b + c)

instance [Add α] [Add β] : Add (α × β) := ⟨λ p q => (p.1 + q.1, p.2 + q.2)⟩

-- This works
example (X Y R) [Add R] [SemiInner X R] [SemiInner Y R] : SemiInner (X × Y) R := by infer_instance

-- This does not ... why?
set_option trace.Meta.synthInstance true in
example (X Y R) [AddSemigroup R] [SemiInner X R] [SemiInner Y R] : SemiInner (X × Y) R:= by infer_instance

How can I change the setup such that the last class inference works but I can still use the notation ⟪x,y⟫ without specifying the type R?

[Mac]

@Tomas Skrivan ypur code gives me an "unknown metavariable '?_uniq.1543'" error, which feels like a Lean bug to me.

[Tomas Skrivan]

Which version of are you running? Mine is nightly-12-15.

[Tomas Skrivan]

For me it gets stuck at an infinite loop, synthesizing instances of Add (USize × ... × USize):

    [Meta.synthInstance.resume] size: 1, Add (USize × ?m.1642) <== Add USize
    [Meta.synthInstance.resume] size: 2, Add (USize × USize) <== Add USize
    [Meta.synthInstance.newAnswer] size: 2, Add (USize × USize)
    [Meta.synthInstance.newAnswer] val: instAddProd
    [Meta.synthInstance.resume] size: 4, Add (USize × USize × USize) <== Add (USize × USize)
    [Meta.synthInstance.newAnswer] size: 4, Add (USize × USize × USize)
    [Meta.synthInstance.newAnswer] val: instAddProd
    [Meta.synthInstance.resume] size: 6, Add (USize × USize × USize × USize) <== Add (USize × USize × USize)
    [Meta.synthInstance.newAnswer] size: 6, Add (USize × USize × USize × USize)
    [Meta.synthInstance.newAnswer] val: instAddProd
    [Meta.synthInstance.resume] size: 8, Add
      (USize × USize × USize × USize × USize) <== Add (USize × USize × USize × USize)
...

[Mac]

@Tomas Skrivan I'm on Lean (version 4.0.0-nightly-2021-12-17, commit e65f3fe81032, Release).

[Tomas Skrivan]

Hmm, now I'm getting the unknown metavariable too. Not sure what changed but the trace still shows the infinite loop of synthesizing longer and longer versions of Add (USize × ... × USize)

[Tomas Skrivan]

I have tried nigtly 11-12, 12-15, 12-19 and all give the same error.

[Tomas Skrivan]

You get the timeout error when you turn of the tracing.

[Mac]

@Tomas Skrivan after looking at the trace, I figured out the problem is that the Add R instance comes first, when it should come last in the the parameter list. That is, the following modified mwe works:

class SemiInner (X : Type u) (R : outParam $ Type v) where
  semiInner : X → X → R

notation "⟪" x ", " y "⟫" => SemiInner.semiInner x y

class SemiHilbert (X R) [Add R] extends Add X, SemiInner X R where
  add_inner : ∀ x y z : X, ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

-- The `Add R` being at the end here is important
instance (X Y R) [SemiInner X R] [SemiInner Y R] [Add R] : SemiInner (X × Y) R where
  semiInner := λ (x,y) (x',y') => ⟪x,x'⟫ + ⟪y,y'⟫

class AddSemigroup (A : Type u) extends Add A where
  add_assoc (a b c : A) : (a + b) + c = a + (b + c)

instance [Add α] [Add β] : Add (α × β) := ⟨λ p q => (p.1 + q.1, p.2 + q.2)⟩

-- This works
example (X Y R) [SemiInner X R] [SemiInner Y R] [Add R] : SemiInner (X × Y) R := inferInstance

-- This works too now
example (X Y R) [SemiInner X R] [SemiInner Y R] [AddSemigroup R] : SemiInner (X × Y) R := inferInstance

The problem is that add instance synthesis is defaulting R to something other than the natural outParam result which is then causing problems in synthesis.

[Mac]

Instance synthesis works in parameter order (e.g., from left to right). If the outParam class comes first, it fixes R for the coming Add synthesis (as desired). If Add R comes first instead, it may try to choose an R itself for future synthesis (which you do not want).

[Tomas Skrivan]

Thanks a lot! I have encountered this problem before, where I had to reorder the typeclass parameters, but didn't realize that is the problem here again.
Would be nice to detect a dangerous order automatically and give a warning.

[Notification Bot]

Tomas Skrivan has marked this topic as unresolved.

[Tomas Skrivan]

I'm having more issues, I also want to define product on SemiHilbert there you cannot move Add R after SemiHilbert arguments. I'm getting timeout error again:

class SemiInner (X : Type u) (R : outParam $ Type v) where
  semiInner : X → X → R

notation "⟪" x ", " y "⟫" => SemiInner.semiInner x y

-- The `Add R` being at the end here is important
instance (X Y R) [SemiInner X R] [SemiInner Y R] [Add R] : SemiInner (X × Y) R where
  semiInner := λ (x,y) (x',y') => ⟪x,x'⟫ + ⟪y,y'⟫

class AddSemigroup (A : Type u) extends Add A where
  add_assoc (a b c : A) : (a + b) + c = a + (b + c)

instance [Add α] [Add β] : Add (α × β) := ⟨λ p q => (p.1 + q.1, p.2 + q.2)⟩

class SemiHilbert (X) (R : outParam $ Type v) [outParam $ Add R] extends Add X, SemiInner X R where
  add_inner : ∀ x y z : X, ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

instance (X Y R) [Add R] [SemiHilbert X R] [SemiHilbert Y R] : SemiHilbert (X × Y) R :=
{
  add_inner := sorry
}

-- Here I'm getting timeout again
example (X Y R) [AddSemigroup R] [SemiHilbert X R] [SemiHilbert Y R] : SemiHilbert (X × Y) R := inferInstance

It does not happen when R is not marked as outParam in the definition of SemiHilbert, but I want it there as I often want R to be automatically inferred.

[Tomas Skrivan]

The reason why I need the outParam under the R parameter in SemiHilbert is that I then want to define class Prop HasAdjoint

class HasAdjoint {X Y} (f : X → Y) {R} [Add R] [SemiHilbert X R] [SemiHilbert Y R] : Prop where
  hasAdjoint : ∃ (f' : Y → X), ∀ x y, ⟪f' y, x⟫ = ⟪y, f x⟫

variable (X Y R) [Add R] [SemiHilbert X R] [SemiHilbert Y R]

variable (f : X → Y) [HasAdjoint f]

#check f

and without the outParam the [HasAdjoint f] can't figure out what R is.

[Mac]

@Tomas Skrivan here is a working example:

class SemiInner (X : Type u) (R : outParam $ Type v) where
  semiInner : X → X → R

notation "⟪" x ", " y "⟫" => SemiInner.semiInner x y

-- The `Add R` being at the end here is important
instance (X Y R) [SemiInner X R] [SemiInner Y R] [Add R] : SemiInner (X × Y) R where
  semiInner := λ (x,y) (x',y') => ⟪x,x'⟫ + ⟪y,y'⟫

-- We set this to priority low so every other `Add` instance is tried first
instance (priority := low) [Add α] [Add β] : Add (α × β) := ⟨λ p q => (p.1 + q.1, p.2 + q.2)⟩

class SemiHilbert (X) (R : outParam $ Type v) [outParam $ Add R] extends Add X, SemiInner X R where
  add_inner : ∀ x y z : X, ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

-- Same here
instance (priority := low) (X Y R) [Add R] [SemiHilbert X R] [SemiHilbert Y R] : SemiHilbert (X × Y) R where
  add_inner := sorry

-- This comes after `SemiHilbert` because we want to try the `AddSemogroup.toAdd` instance before the `SemiHilbert.toAdd` one
class AddSemigroup (A : Type u) extends Add A where
  add_assoc (a b c : A) : (a + b) + c = a + (b + c)

-- This now works
example (X Y R) [AddSemigroup R] [SemiHilbert X R] [SemiHilbert Y R] : SemiHilbert (X × Y) R := inferInstance

class HasAdjoint {X Y} (f : X → Y) {R} [Add R] [SemiHilbert X R] [SemiHilbert Y R] : Prop where
  hasAdjoint : ∃ (f' : Y → X), ∀ x y, ⟪f' y, x⟫ = ⟪y, f x⟫

variable (X Y R) [Add R] [SemiHilbert X R] [SemiHilbert Y R]

variable (f : X → Y) [HasAdjoint f]

#check f

[Mac]

However, the man problem here that I find suspicious is that Lean's typeclass synthesis doesn't try to synthesize SemiHilbert (X × Y) R(i.e., the desired instance) first, but instead immediately tries SemiHilbert (X × Y) ?m.1657(i.e., with an metavariable output -- a produce of the outParam) which is a major cause of all this trouble.

I feel like it should try to synthesize SemiHilbert (X × Y) R first and only when that fails try SemiHilbert (X × Y) ?m.1657, but that may just be an uniformed opinion.

[Reid Barton]

[outParam $ Add R] seems to express two contradictory intents: one that the argument should be synthesized by TC instance search, the other that it should be determined by the SemiHilbert instance.

[Reid Barton]

I wonder whether this interaction of features has been properly thought through (certainly it hasn't been by me).

[Reid Barton]

I would be inclined to try {} binders for the Add R in the SemiHilbert class and instances.

[Mac]

@Reid Barton but [outParam $ Add R] wasn't the problem here?

[Reid Barton]

I think it is the core issue though--you don't want to try synthesizing Add R ever

[Reid Barton]

Instead, you want to learn it from the SemiHilbert instance

[Mac]

@Reid Barton true, an alternative way to structure this would be something like:

class SemiHilbert (X) (R : outParam $ Type v) extends SemiInner X R where
  add_X : X → X → X
  add_R : R → R → R
  add_inner : ∀ x y z : X, ⟪add_X x y, z⟫ = add_R ⟪x, z⟫ ⟪y, z⟫

instance (X R) [SemiHilbert X R] : Add X := ⟨SemiHilbert.add_X⟩
instance (X R) [SemiHilbert X R] : Add R := ⟨SemiHilbert.add_R (X := X)⟩

instance (priority := low) (X Y R) [SemiHilbert X R] [SemiHilbert Y R] : SemiHilbert (X × Y) R where
  add_X := Add.add
  add_R := Add.add
  add_inner := sorry

class AddSemigroup (A : Type u) extends Add A where
  add_assoc (a b c : A) : (a + b) + c = a + (b + c)

example (X Y R) [SemiHilbert X R] [SemiHilbert Y R] [AddSemigroup R]  : SemiHilbert (X × Y) R := inferInstance

[Reid Barton]

This looks awkward though because in the actual instances, you probably want to use existing Add instances for real etc.

[Reid Barton]

And

instance (X R) [SemiHilbert X R] : Add R

looks very dubious as there is no way to determine X

[Mac]

@Reid Barton very true, there is not really a silver bullet here, because Lean does not, afaik, provide a neat way to force Add R use the instance and R that come from SemiHilbert. [outParam $ Add R] is closest approximation, but it has the problems you mentioned.

[Tomas Skrivan]

Here is my solution using utility classes Trait X and Trait₂ X Y that fetch R based on X or X Y and there is an instance of Trait whenever there is an instance of SemiInner.

class SemiInner (X : Type u) (R : outParam $ Type v) where
  semiInner : X → X → R

notation "⟪" x ", " y "⟫" => SemiInner.semiInner x y

class Trait (X : Type u) where
  R : Type v
class Trait₂ (X : Type u) (Y : Type v) where
  R : Type w

attribute [reducible] Trait.R Trait₂.R

@[reducible] instance (X) (R : outParam $ Type v) [SemiInner X R] : Trait X := ⟨R⟩
@[reducible] instance (X Y) [Trait X] : Trait₂ X Y := ⟨Trait.R X⟩
@[reducible] instance (X Y) [Trait Y] : Trait₂ X Y := ⟨Trait.R Y⟩

-- The `Add R` being at the end here is important
instance (X Y R) [SemiInner X R] [SemiInner Y R] [Add R] : SemiInner (X × Y) R where
  semiInner := λ (x,y) (x',y') => ⟪x,x'⟫ + ⟪y,y'⟫

class AddSemigroup (A : Type u) extends Add A where
  add_assoc (a b c : A) : (a + b) + c = a + (b + c)

instance [Add α] [Add β] : Add (α × β) := ⟨λ p q => (p.1 + q.1, p.2 + q.2)⟩

class SemiHilbert (X) (R : outParam $ Type v) [outParam $ Add R] extends SemiInner X R, Add X where
  add_inner : ∀ x y z : X, ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫

-- The important bit here is that `R` is fetched with the utility class Trait and not spelled out explicitely
instance (X Y) [Trait₂ X Y] [Add (Trait₂.R X Y)]
  [SemiHilbert X (Trait₂.R X Y)]
  [SemiHilbert Y (Trait₂.R X Y)]
  : SemiHilbert (X × Y) (Trait₂.R X Y) :=
{
  add_inner := sorry
}

example (X Y R) [Add R] [SemiHilbert X R] [SemiHilbert Y R] : SemiHilbert (X × Y) R := inferInstance

example (X Y R) [AddSemigroup R] [SemiHilbert X R] [SemiHilbert Y R] : SemiHilbert (X × Y) R := inferInstance

class HasAdjoint {X Y} (f : X → Y) {R} [Add R] [SemiHilbert X R] [SemiHilbert Y R] : Prop where
  hasAdjoint : ∃ (f' : Y → X), ∀ x y, ⟪f' y, x⟫ = ⟪y, f x⟫

variable (X Y R) [Add R] [SemiHilbert X R] [shy : SemiHilbert Y R] (x x' : X) (r : R)

variable (f : X → Y) [HasAdjoint f] (x x' : X) (r : Trait₂.R X Y)

#check ⟪x, x'⟫ + r  -- This works because `Trait₂.R` is reducible

[Tomas Skrivan]

Mac said:

Tomas Skrivan here is a working example:

Nice! I was fiddling with priorities quite a bit and was unable to get it working.

[Tomas Skrivan]

Arghhh, the approach with Trait is also problematic. The SemiHilbert instance on product type causes a timeout error on

example {α β} : Add (α × β) := by infer_instance

As it does not fail properly it completely messes up other type class inferences.

[Tomas Skrivan]

Adding [Trait₂ X Y] at the beginning of the instance of SemiHilbert (X × Y) R seems to solve the above problem. The value [Trait₂ X Y] is not used at all, but is there just to safe guard a misuse of instance.

instance (X Y R) [Trait₂ X Y] [Add R] [SemiHilbert X R] [SemiHilbert Y R]
  : SemiHilbert (X × Y) R :=
{
  add_inner := sorry
}