Skip to content

Bind kind variables in type synonyms

I wonder if GHC could support the binding of kind-variables in type-synonyms (I am using standalone kind signatures):

type F :: forall a (b :: a -> Type). a -> Type
type F @_ @f x = f x 

or even (still new to VDQ):

type F :: forall a. forall (b :: a -> Type) -> a -> Type
type F @_ f x = f x 

This would mirror the term-level after proposals like Binding type variables in lambda-expressions are implemented.

Edited by John Ericson
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information