How to change the order of type application parameters for a constructor

Question

I've got the following data type definition:

type DynamicF' :: k -> (k -> Type) -> Type
data DynamicF' k f where
  DynamicF :: Typeable a => f a -> DynamicF' k f

The thing is, generally, I'm going to be specialising k to Type. So I've provided the following type alias:

type DynamicF f = DynamicF' Type f

Then I can do things like this:

data Showable a where
  Showable :: Show a => a -> Showable a

f :: DynamicF Showable -> String
f (DynamicF @_ @a x) = g x where
  g :: Showable a -> String
  g (Showable y) = show y

This is perhaps a silly example but hopefully illustrative, but notice the pattern match:

DynamicF @_ @a x

And in particular, the underscore required for the first argument.

This is because the first type application argument seems to be against f, not a, in the DynamicF constructor.

Apparently I can change the order of these using forall blah., and perhaps using forall {blah}. like constructs.

But I'm not sure where to actually put the forall.s in this code so they I can instead just do:

f (DynamicF @a x)

in the pattern match, instead of requiring the silly underscore.

Answer 1

The right place to put the forall is in the data declaration:

type DynamicF' :: k -> (k -> Type) -> Type
data DynamicF' k f where
  DynamicF :: forall a f k. Typeable a => f a -> DynamicF' k f

If you were concerned that somehow the f and k couldn't be specified in a forall because they are part of the DynamicF' k f type, don't be. It is the type of the "result" of the constructor that determines what variables become part of the final type. For example, the following declaration works exactly like your original:

data DynamicF' doesn't match where
  DynamicF :: forall whatever you want. 
              Typeable whatever => you whatever -> DynamicF' want you

However, note that I wasn't able to duplicate your issue. The order was already forall a f k for this constructor (because the Typeable a => puts a in first position).