cannot find synthesization order for instance

Stream: lean4

[Tomas Skrivan]

I have updated to a newer version of Lean and I'm getting an error I have not seen before.

This code

class Foo (A : Type) (B : outParam Type)

class Bar (A : outParam Type) (B : Type) extends Foo A B

Produces

cannot find synthesization order for instance @Bar.toFoo with type
  {A : outParam Type} → {B : Type} → [self : Bar A B] → Foo A B
all remaining arguments have metavariables:
  Bar A ?B

Swapping outParam might seem to be quite suspicious. My application of this is:

• Foo A B says that A is a container with values B
• Bar A B says that A is the canonical container with values B

---

More concretely, I have

class GenericArrayType (Cont : Type u) (Idx : outParam $ Type v ) (Elem : outParam $ Type w)
  ...

and

class ArrayType (Cont : outParam Type) (Idx Elem: Type) extends GenericArrayType Cont Idx Elem

I use ArrayType in notation Elem^Idx which just fetches the corresponding Cont

[Reid Barton]

That's also a word I haven't seen before

[Tomas Skrivan]

It is causing problems when just using GetElem

class ArrayType (Cont : outParam Type) (Idx Elem : Type) extends GetElem Cont Idx Elem (λ _ _ => True)

I really want this instance:

instance : ArrayType {a : FloatArray // a.size = n} (Fin n) Float := ...

so I can write Float^(Fin n) and get FloatArray

[Tomas Skrivan]

It looks like the change happened in 4544443. @Gabriel Ebner Any thoughts on this? Am I doing something bad/discouraged or was this an unintended consequence?

[Reid Barton]

Does turning off this synthInstance.checkSynthOrder option help?

[Yaël Dillies]

Have you read https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/FunLike.20issues/near/345815614. Does using SemiOutParam in places help?

[Tomas Skrivan]

I will give it a read!

[Yaël Dillies]

Disclaimer: I haven't understood the new system myself

[Tomas Skrivan]

A quick test, this does not work:

class ArrayType (T : semiOutParam Type) (I X : Type) extends GetElem T I X (λ _ _ => True)

but I have to read up on what semiOutParam is actually doing

[Tomas Skrivan]

I see that the attribute infer_tc_goals_rl disappeared. I'm assuming these changes have something to do with typeclass outparams that were causing some issues.

[Tomas Skrivan]

Reid Barton said:

Does turning off this synthInstance.checkSynthOrder option help?

Yes! This solves the problem.

But maybe I should rethink my code and have a specialized notation class.

[Gabriel Ebner]

The purpose of the check is to prevent [GenericArrayType Cont Idx Elem] [Monoid Elem] from blowing up when you have an ArrayType (Array α) (Fin n) α instance.

[Gabriel Ebner]

If you only have instances like the FloatArray one, then you should mark the Idx and Elem parameters (in ArrayType) as semiOutParam.

[Gabriel Ebner]

Although that instance will still complain about the n parameter.

[Gabriel Ebner]

(deleted)

[Tomas Skrivan]

Gabriel Ebner said:

The purpose of the check is to prevent [GenericArrayType Cont Idx Elem] [Monoid Elem] from blowing up when you have an ArrayType (Array α) (Fin n) α instance.

I do have instances for algebraic structures over arrays and I remember running into problems like this quite often but I forgot how I solved it.

I should probably revise my typeclass hierarchy.

[Yakov Pechersky]

I am running into this when trying to define a seemingly simple Category:

universe v u

inductive RelHom {S : Type u} (r : S → S → Prop) (a b : S)
| ofRel : r a b → RelHom r a b

class IsRefl (α : Type u) (r : α → α → Prop) : Prop where
  refl : ∀ a, r a a

class Quiver (V : Type u) where
  Hom : V → V → Sort v

open Quiver (Hom)

instance RelQuiver (S : Type u) (r : S → S → Prop) : Quiver S where
  Hom a b := RelHom r a b

class IsTrans (α : Type u) (r : α → α → Prop) : Prop where
  trans : ∀ a b c, r a b → r b c → r a c

class CategoryStruct (obj : Type u) extends Quiver.{v + 1} obj : Type max u (v + 1) where
  id : ∀ X : obj, Hom X X

-- cannot find synthesization order for instance instCategoryStruct with type
--  (S : Type u) → (r : S → S → Prop) → [inst : IsRefl S r] → CategoryStruct S
-- all remaining arguments have metavariables:
--  IsRefl S ?r
instance (S : Type u) (r : S → S → Prop) [IsRefl S r] : CategoryStruct S where
  Hom a b := RelHom r a b
  id  a   := .ofRel (IsRefl.refl a)

I can't tell what the issue with the IsRefl S r here.

[Kevin Buzzard]

set_option synthInstance.checkSynthOrder false solves it (see above)

[Kevin Buzzard]

Should something be an outParam?

[Yakov Pechersky]

It "solves" it, yes, but I don't know what exactly it's "solving" -- it removes the error, but turning off such an option makes me think it's hiding some other failure somewhere.

[Gabriel Ebner]

Yes, it solves it in the same way that nolint sweeps issues under the rug.

[Gabriel Ebner]

The issue in your example is that the relation r is completely undetermined. If you've an IsRefl S rel1 and and IsRefl S rel2 instance, then CategoryStruct S might use either one of them (maybe even depending on the order of the imports in the file).

[Gabriel Ebner]

In this example, I'd probably add a def Rel (A : Type u) (r : A -> A -> Prop) := A type alias and use that in the instance (i.e., CategoryStruct (Rel S r)

[Yakov Pechersky]

Why doesn't it complain about possibly overlapping instances at the RelQuiver decl, where r only factors into the body of the Quiver, not the type?

[Gabriel Ebner]

Oh, the RelQuiver instance is also super problematic, as it will always apply and never work since it can't figure out the r (and Lean will only notice this at the very end so this has the effect of disabling the other Quiver instances..).

[Gabriel Ebner]

The reason why Lean doesn't print an error for that is because that check can be implemented as a linter in mathlib.