Polymorphic constraint

Question

I have some contrived type:

{-# LANGUAGE DeriveFunctor #-}

data T a = T a deriving (Functor)

... and that type is the instance of some contrived class:

class C t where
    toInt :: t -> Int

instance C (T a) where
    toInt _ = 0

How can I express in a function constraint that T a is an instance of some class for all a?

For example, consider the following function:

f t = toInt $ fmap Left t

Intuitively, I would expect the above function to work since toInt works on T a for all a, but I cannot express that in the type. This does not work:

f :: (Functor t, C (t a)) => t a -> Int

... because when we apply fmap the type has become Either a b. I can't fix this using:

f :: (Functor t, C (t (Either a b))) => t a -> Int

... because b does not represent a universally quantified variable. Nor can I say:

f :: (Functor t, C (t x)) => t a -> Int

... or use forall x to suggest that the constraint is valid for all x.

So my question is if there is a way to say that a constraint is polymorphic over some of its type variables.

I assume that something like class C t where toInt :: t a -> Int won't work, and you need C to be of kind * -> Constraint? Would kind polymorphism help here? — C. A. McCann
@C.A.McCann The concrete type constructor I have in mind is Proxy from pipes and the concrete class is Monad. I'm type-classing utility functions for proxy-like types, which is why the constraint is there. Following your suggestion, I'd then define a MonadP class specialized to the shape of the Proxy type constructor and use that as a constraint instead. The disadvantage is that if users wanted to write proxy utility functions polymorphic in the proxy-like type, they'd have to rebind do notation to use MonadP instead. — Gabriella Gonzalez
You can't do it directly, but it's possible to simulate, as in Roman's answer. Here's the relevant GHC ticket: hackage.haskell.org/trac/ghc/ticket/2893 — glaebhoerl

Roman Cheplyaka Roman Cheplyaka · Accepted Answer · 2012-10-04T00:06:35

Using the constraints package:

{-# LANGUAGE FlexibleContexts, ConstraintKinds, DeriveFunctor, TypeOperators #-}

import Data.Constraint
import Data.Constraint.Forall

data T a = T a deriving (Functor)

class C t where
    toInt :: t -> Int

instance C (T a) where
    toInt _ = 0

f :: ForallF C T => T a -> Int
f t = (toInt $ fmap Left t) \\ (instF :: ForallF C T :- C (T (Either a b)))

Polymorphic constraint

1 Answers