I learned that you can redefine ContT from transformers such that the r type parameter is made implicit (and may be specified explicitly using TypeApplications), viz.:
-- | Same as `ContT` but with the `r` made implicit
type ContT ::
forall (r :: Type).
(Type -> Type) ->
Type ->
Type
data ContT m a where
ContT ::
forall r m a.
{runContT :: (a -> m r) -> m r} ->
ContT @r m a
type ContVoid :: (Type -> Type) -> Type -> Type
type ContVoid = ContT @()
I hadn't realized this was possible in GHC. What is the larger feature called to refer to this way of defining a family of types with implicit type parameters, that is specified using forall in type definition (referring, in the example above, to the outer forall - rather than the inner forall which simply unifies the r)?
Nobody uses this (invisible dependent quantification) for this purpose (where the dependency is not used) but it is the same as giving a Type -> .. parameter, implicitly.
type EITHER :: forall (a :: Type) (b :: Type). Type
data EITHER where
LEFT :: a -> EITHER @a @b
RIGHT :: b -> EITHER @a @b
eITHER :: (a -> res) -> (b -> res) -> (EITHER @a @b -> res)
eITHER left right = \case
LEFT a -> left a
RIGHT b -> right b
You can also use "visible dependent quantification" where forall-> is the visible counterpart to forall., so forall (a :: Type) -> .. is properly like Type -> .. where a does not appear in ..:
type EITHER :: forall (a :: Type) -> forall (b :: Type) -> Type
data EITHER a b where
LEFT :: a -> EITHER a b
RIGHT :: b -> EITHER a b
eITHER :: (a -> res) -> (b -> res) -> (EITHER a b -> res)
eITHER left right = \case
LEFT a -> left a
RIGHT b -> right b