GitLab

Motivation

When manipulating constraints, it is often useful to define class newtypes adapted to a single case. Consider for instance the general constrained traversal function:

type  TraversableC :: ( Type -> Type -> Constraint ) -> Type -> Type -> Constraint
class TraversableC c s t where
  traverseC :: forall f. Applicative f => ( forall a b. c a b => a -> f b ) -> s -> f t

To make use of traverseC, one often ends up needing to cook up an appropriate c that allows one to write the higher-rank function it requires. Here are some artificial examples which I hope nevertherless help illustrate the situation:

class    ( Num a, Show a, b ~ String ) => ShowyNum a b
instance ( Num a, Show a, b ~ String ) => ShowyNum a b

mapShowAbs :: forall s t. TraversableC ShowyNum s t => s -> t
mapShowAbs = runIdentity . traverseC @ShowyNum ( Identity . show . abs )


class    ( a ~ b, Integral a ) => Summy a b
instance ( a ~ b, Integral a ) => Summy a b

summy :: forall s. TraversableC Summy s s => s -> Integer
summy = getSum . getConst . traverseC @Summy @s @s ( Const . Sum . toInteger )

The problem arises when one would like to be able to introduce extra type variables in the context of the class declaration. Consider for instance a constrained traversal that needs arguments to be triples; one must currently write the following:

type Fst3, Snd3, Thrd3 :: Type -> Type
type family Fst3  t where
  Fst3  ( a, b, c ) = a
type family Snd3  t where
  Snd3  ( a, b, c ) = b
type family Thrd3 t where
  Thrd3 ( a, b, c ) = c

class    ( t1 ~ ( Fst3 t1, Snd3  t1, Thrd3 t1 )
         , t2 ~ ( Snd3 t1, Thrd3 t1, Fst3  t1 )
         )
      => Cycly t1 t2
instance ( t1 ~ ( a, b, c ), t2 ~ ( b, c, a ) )
      => Cycly t1 t2

cycleTriples :: forall s t. TraversableC Cycly s t => s -> t
cycleTriples = runIdentity . traverseC @Cycly ( \ ( a, b, c ) -> Identity ( b, c, a ) )

The problem in this case is that, for the class declaration, one is not allowed to introduce new variables beyond those bound by the header. Instead, we have to introduce type families to be able to refer to them. This also comes at the cost of readability, as in such situations one often ends up having to duplicate type family applications, as opposed to being able to give them a succint name, like one can in instances:

instance forall a b c res.
      ( res ~ SomeComplexTypeFamilyApplicationWithALongName a b c
      , C1 res ( F res )
      , C2 res res
      , C3 a b c res
      )
   => C a b c

Proposal

I'd like to be able to bind extra type variables in class declaration headers, at least in the restricted situation that these variables are uniquely determined by the variables present in the class declaration header.

I don't know the extent to which this is reasonable, so I'd like to hear from those more knowledgeable about this. At the very least, I think it would be reasonable to allow introduction of extra variables which are simply synonyms of expressions involving only the variables in the header, as these could be expanded under the hood.

If any of this seems reasonable, I'd be happy to attempt implementing this (along with writing a GHC proposal). Please let me know your thoughts.