Zulip Chat Archive

Stream: lean4

Topic: outparam classes


view this post on Zulip Jason Gross (Mar 12 2021 at 19:32):

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?

view this post on Zulip Mario Carneiro (Mar 12 2021 at 20:25):

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

view this post on Zulip Jason Gross (Mar 12 2021 at 20:28):

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

view this post on Zulip Jason Gross (Mar 12 2021 at 20:52):

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?)

view this post on Zulip Jason Gross (Mar 12 2021 at 21:40):

Oh! Perhaps this is exactly what default instances are for

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 03:08):

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.


Last updated: May 07 2021 at 13:21 UTC