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