Quantified constraints which specify associated type instances
I have come across a situation which I believe could benefit from the ability to refine quantified constraints by adding constraints on the associated type instance declarations. For instance, consider a class with an associated type:
class C a where
type T a :: Type
...
From what I understand, a quantified constraint of the form ( forall a. C a => C (f a) )
will be soluble when there is an instance of the form
instance forall a. C a => C (f a)
My suggestion is to provide the ability to specify quantified constraints which restrict the associated type family instance declarations. In this case, we might want to insist upon the equation type T (f a) = f (T a)
. One possible notation would use tuple and equality constraints (mirroring how one would encode this using Dict
):
forall a. C a => ( C (f a), T (f a) ~ f (T a) )
In solving this quantified constraint, we would discard all class instances which are not of the following form:
instance forall a. C a => C (f a) where
type T (f a) = f (T a)
(I don't know how flexible we can afford to be in verifying this property, e.g. if the type family instance equations are not exactly as specified by the equality constraint but are equivalent to them, say after applying substitutions or using other equality constraints that might be available.)
Example
To illustrate, I was working with the Syntactic
type class
class Syntactic a where
type Internal a
toAST :: a -> AST (Internal a)
fromAST :: AST (Internal a) -> a
and I wanted to restrict attention to functors F
that are compatible with this type class, i.e. which have an instance declaration of the form
instance Syntactic a => Syntactic (F a) where
type Internal (F a) = F (Internal a)
However, while I can write a quantified constraint forall a. Syntactic a => Syntactic (f a)
, I cannot specify the additional requirement on the associated type family instance equation, so GHC will complain at use-sites:
* Could not deduce: Internal (f a) ~ f (Internal a)
This can be worked around using Dict ( Syntactic (f a), Internal (f a) ~ f (Internal a) )
, unfortunately forgoing the use of quantified constraints and introducing indirections (requiring matching on Dict
to make the instances visible to GHC). Other than that I don't know of any tricks to bypass this limitation, but I may well be missing something (quite likely, as I don't have much experience with quantified constraints).