outparam classes

Stream: lean4

[Jason Gross]

I'm getting

class Arr (α : Sort u1) (γ : outParam (Sort u2)) where
  Arr : α → α → γ

infix:70 " ~> " => Arr.Arr

class Compose (α : Sort u) (β : outParam (Sort u2)) [Arr α β] [CoeSort β (Sort u3)] where
  compose : ∀ {a b c : α}, coeSort (a ~> b) → coeSort (b ~> c) → coeSort (a ~> c)
-- invalid class, parameter #3 depends on `outParam`, but it is not an `outParam`

It seems to me like this should be valid, because Arr α β has β as an outParam and therefore by the time we need to go looking for CoeSort β _, we should have already synthesized β. Am I missing something?

[Mario Carneiro]

It sounds like you don't want beta to be an outParam of Compose

[Jason Gross]

If β is not an outParam of Compose, then tc resolution won't trigger unless β has no metas when searching for Compose. But in fact β will never be known when triggering TC search on Compose, and should always be derived as the result of synthesizing the Arr instance

[Jason Gross]

Here's the problem I don't know how to solve with typeclasses in Lean 4 currently:
I want to have two instances

Arr T1 T2
Arr T1 (Sort _)

The second argument of Arr needs to be outParam for it to trigger when I don't know the sort universe. However, it seems that then there's no way to have both instances around in a usable way. I want something where Arr T1 (Sort ?u) will trigger TC search and find the second instance, and Arr T1 T2 will trigger TC search and find the first instance. This doesn't currently seem to be possible (unless I can declare a coercion from Arr T1 T2 to Arr T1 (Sort _) and have tc resolution pick up the coercion when it tries to do the final unification?)

[Jason Gross]

Oh! Perhaps this is exactly what default instances are for

[Leonardo de Moura]

Jason Gross said:

Oh! Perhaps this is exactly what default instances are for

I didn't read your example carefully yet. We had more modest goals for the default instances (see Default instances thread). Not sure how well they will work for your scenario.