Typeclass changes between April and 4.1.0?

Stream: lean4

[Colin S. Gordon]

I had been working on a paper for some time last spring using Lean 4 typeclasses in a formalization, then left the implementation alone for a bit after submitting a paper. Since Lean 4 made its official release, I've been looking off and on to update my code, and have been stuck for a while due to what seem to be significant changes to typeclass machinery since then. The last nightly version of Lean that my code works with is leanprover/lean4:nightly-2023-04-07, at which point there seems to be a gap in the nightlies being published, and picking up the first May nightly build results in new errors that I've been unable to fix; poking around git commits from that time reveals significant changes to the typeclass code, but I've been unable to find explanations of exactly what the conceptual model of the change was. I was hoping someone could help me get my code working, or better yet, explain the general scope/shift of the changes in general so I can reason through the consequences for my development.

My actual development is fairly substantial and makes extensive use of typeclasses, but I can reproduce the same error quite simply. Consider:

class C (A B : Type) where

instance ns : C Nat String where

instance sn : C String Nat where

This much is fine, but trying to add any kind of transitivity instance gives me errors I don't recognize from earlier development versions of Lean 4:

instance trans {X Y Z}[C X Y][C Y Z] : C X Z where

results in an error

cannot find synthesization order for instance @_root_.trans with type
  {X Y Z : Type} → [inst : C X Y] → [inst : C Y Z] → C X Z
all remaining arguments have metavariables:
  C X ?Y
  C ?Y Z

The same instances are accepted by the last nightly of pre-release Lean 4 prior to the big typeclass changes.

Wondering if this was related to Y, I also tried

instance trans {X Z}[C X String][C String Z] : C X Z where

which is accepted.

I can't find any updates to the documentation for this error or written discussion of the change itself (though it's quite possible I've missed this somewhere, in which case a pointer would be quite appreciated). Is the intent to no longer support typeclass resolution where no fixed (optimal?) order is identifiable for trying to resolve typeclass parameters? Or is the change more subtle than that? In the case of my full development, no concretization of typeclass arguments like my accepted tweak above, even with reorganization of the typeclasses, is appropriate; many/most of the typeclass instances I'm using legitimately have and require parameters that do not appear in the goal instance signature, exemplified by the transitivity instance above, so I'm particularly keen to learn if such non-goal-directed variables are simply no longer supported in any form, or if there are conditions under which some versions of them might still work.

[Alex J. Best]

Yes things have changed since then lean4#2174 was merged April 10th so for example.
I'd suggest looking at docs#semiOutParam and the core implementation of docs#Coe via docs#CoeHead and docs#CoeTail to see whether your setup can be fixed using the semiOutParam decorator. In principle your trans could loop arbitrarily, so the fact that it didn't probably means there is a way to use semi-out params to fix things, maybe at the expense of needing some sort of head/tail classes like core

[Mac Malone]

If you just want to bump the code without adapting to the new requirements (at least for the moment), you can just disable this check with an option (iirc set_option synthInstance.checkSynthOrder false).

[Colin S. Gordon]

Thanks both of you!

[Colin S. Gordon]

The option certainly works for now.

[Colin S. Gordon]

I'll take a careful look at semiOutParam, looking at the docs I think my intended use case is outside the intended range of things it supports, but I'll find out.