Allow using joinOrderingF as a right-associative infix operator

[RyanGlScott]

A common pattern when defining compare implementations is to use the (<>) operator to chain together Ordering values, e.g.,

compare (Foo x1 y1 z1) (Foo x2 y2 z2) =
  compare x1 y2 <> compare y1 y2 <> compare z1 z2 

I'd like to be able to do the same with compareF implementations in OrdF instances. OrderingF isn't a Semigroup, so we can't use (<>), but the closest equivalent is the joinOrderingF function.

Unfortunately, it's not straightforward to use joinOrderingF in an infix fashion at the moment. Consider this specific example:

import Data.Kind (Type)
import Data.Parameterized.BoolRepr
import Data.Parameterized.Classes
import Data.Parameterized.NatRepr
import GHC.TypeNats

data Foo = MkFoo Bool Nat

data FooRepr :: Foo -> Type where
  MkFooRepr :: BoolRepr b
            -> NatRepr n
            -> FooRepr (MkFoo b n)

instance OrdF FooRepr where
  compareF (MkFooRepr b1 n1) (MkFooRepr b2 n2) =
    compareF b1 b2 `joinOrderingF` compareF n1 n2 `joinOrderingF` EQF

instance TestEquality FooRepr where
  testEquality (MkFooRepr b1 n1) (MkFooRepr b2 n2)
    | Just Refl <- testEquality b1 b2
    , Just Refl <- testEquality n1 n2
    = Just Refl
    | otherwise
    = Nothing

This will not typecheck with the way it is written above. Here is the (rather verbose) error message:

Foo.hs:24:45: error:
    • Couldn't match kind ‘j0’ with ‘Nat’
      When matching types
        ktp0 :: j0 -> *
        NatRepr :: Nat -> *
      Expected: ktp0 a0
        Actual: NatRepr n
    • ‘j0’ is untouchable
        inside the constraints: b ~ b1
        bound by a type expected by the context:
                   (b ~ b1) => OrderingF a0 b0
        at Foo.hs:24:36-49
    • In the first argument of ‘compareF’, namely ‘n1’
      In the second argument of ‘joinOrderingF’, namely ‘compareF n1 n2’
      In the first argument of ‘joinOrderingF’, namely
        ‘compareF b1 b2 `joinOrderingF` compareF n1 n2’
   |
24 |     compareF b1 b2 `joinOrderingF` compareF n1 n2 `joinOrderingF` EQF
   |                                             ^^

Foo.hs:24:67: error:
    • Could not deduce (n1 ~ n)
      from the context: x ~ 'MkFoo b n
        bound by a pattern with constructor:
                   MkFooRepr :: forall (b :: Bool) (n :: Nat).
                                BoolRepr b -> NatRepr n -> FooRepr ('MkFoo b n),
                 in an equation for ‘compareF’
        at Foo.hs:23:13-27
      or from: y ~ 'MkFoo b1 n1
        bound by a pattern with constructor:
                   MkFooRepr :: forall (b :: Bool) (n :: Nat).
                                BoolRepr b -> NatRepr n -> FooRepr ('MkFoo b n),
                 in an equation for ‘compareF’
        at Foo.hs:23:31-45
      or from: a0 ~ b0
        bound by a type expected by the context:
                   (a0 ~ b0) => OrderingF x y
        at Foo.hs:24:67-69
      Expected: OrderingF x y
        Actual: OrderingF x x
      ‘n1’ is a rigid type variable bound by
        a pattern with constructor:
          MkFooRepr :: forall (b :: Bool) (n :: Nat).
                       BoolRepr b -> NatRepr n -> FooRepr ('MkFoo b n),
        in an equation for ‘compareF’
        at Foo.hs:23:31-45
      ‘n’ is a rigid type variable bound by
        a pattern with constructor:
          MkFooRepr :: forall (b :: Bool) (n :: Nat).
                       BoolRepr b -> NatRepr n -> FooRepr ('MkFoo b n),
        in an equation for ‘compareF’
        at Foo.hs:23:13-27
    • In the second argument of ‘joinOrderingF’, namely ‘EQF’
      In the expression:
        compareF b1 b2 `joinOrderingF` compareF n1 n2 `joinOrderingF` EQF
      In an equation for ‘compareF’:
          compareF (MkFooRepr b1 n1) (MkFooRepr b2 n2)
            = compareF b1 b2 `joinOrderingF` compareF n1 n2 `joinOrderingF` EQF
    • Relevant bindings include
        n2 :: NatRepr n1 (bound at Foo.hs:23:44)
        n1 :: NatRepr n (bound at Foo.hs:23:26)
   |
24 |     compareF b1 b2 `joinOrderingF` compareF n1 n2 `joinOrderingF` EQF
   |                                                                   ^^^

But the high-level problem is that the calls to joinOrderingF are associated the wrong way. If you add some parentheses to make joinOrderingF associate to the right:

instance OrdF FooRepr where
  compareF (MkFooRepr b1 n1) (MkFooRepr b2 n2) =
    compareF b1 b2 `joinOrderingF` (compareF n1 n2 `joinOrderingF` EQF)

Then it typechecks. It's somewhat annoying to have to add all of these parentheses manually, however.

One possible solution would be marking joinOrderingF as right-associative:

infixr 6 `joinOrderingF`

Another solution would be to define a shorter, infix version of joinOrderingF like so:

infixr 6 <<>>
(<<>>) ::
  forall j k (a :: j) (b :: j) (c :: k) (d :: k).
  PC.OrderingF a b ->
  (a ~ b => PC.OrderingF c d) ->
  PC.OrderingF c d
(<<>>) = PC.joinOrderingF