Can I constrain a type family?

Certainly, the obvious thing would be to simply write the desired constraint directly:

class (Differentiable (D f)) => Differentiable (f :: * -> *) where

Alas, GHC gets huffy about that and refuses to play along:

ConstrainTF.hs:17:1:
    Cycle in class declaration (via superclasses):
      Differentiable -> Differentiable
    In the class declaration for `Differentiable'

So, as is often the case when attempting to describe type constraints fancy enough to leave GHC recalcitrant, we must resort to some manner of underhanded trickery.

Recalling some relevant features of GHC where type hackery is involved:

It is paranoid about type-level nontermination far out of proportion to the actual inconvenience it entails for the user.
It will cheerfully commit itself to decisions about classes and instances before it has considered all the information available.
It will dutifully attempt to check anything you've tricked it into committing to.

These are the devious principles underlying the familiar old faux-generic instances, where types are unified post-hoc with (~) in order to improve the type inference behavior of certain type hackery constructs.

In this case, however, rather than sneaking type information past GHC, we would need to somehow prevent GHC from noticing a class constraint, which is an entirely different kind of... heeeey, waaaitaminute....

import GHC.Prim

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint f = Differentiable f

class (DiffConstraint (D f)) => Differentiable (f :: * -> *) where
  type D f :: * -> *

Hoist by its own petard!

It's the real deal, too. These are accepted, as you'd hope:

instance Differentiable (K a) where
  type D (K a) = K Void
instance Differentiable I where
  type D I = K ()

But if we offer it some nonsense instead:

instance Differentiable I where
  type D I = []

GHC presents us with precisely the error message we'd like to see:

ConstrainTF.hs:29:10:
    No instance for (Differentiable [])
      arising from the superclasses of an instance declaration
    Possible fix: add an instance declaration for (Differentiable [])
    In the instance declaration for `Differentiable I'

There is one small snag, of course, namely that this:

instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

...turns out to be less than well-founded, as we've told GHC to check that, whenever (f :+: g) is Differentiable, so is (D f :+: D g), which does not end well (or at all).

The easiest way to avoid this would usually be to boilerplate on a pile of explicit base cases, but here GHC seems intent on diverging any time a Differentiable constraint appears in an instance context. I would assume it's being unnecessarily eager in checking instance constraints somehow, and could perhaps be distracted long enough with another layer of trickery, but I'm not immediately sure where to start and have exhausted my capacity for post-midnight type hackery tonight.

A bit of IRC discussion on #haskell managed to jog my memory slightly on how GHC handles class context constraints, and it appears we can patch things up a little bit by means of a pickier constraint family. Using this:

type family DiffConstraint (f :: * -> *) :: Constraint
type instance DiffConstraint (K a) = Differentiable (K a)
type instance DiffConstraint I = Differentiable I
type instance DiffConstraint (f :+: g) = (Differentiable f, Differentiable g)

We now have a much more well-behaved recursion for sums:

instance (Differentiable (D f), Differentiable (D g)) => Differentiable (f :+: g) where
  type D (f :+: g) = D f :+: D g

The recursive case cannot be so easily bisected for products, however, and applying the same changes there improved matters only insofar as I received a context reduction stack overflow rather than it simply hanging in an infinite loop.

Your best bet might be to define something using the constraints package:

import Data.Constraint

class Differentiable (f :: * -> *) where
  type D f :: * -> *
  witness :: p f -> Dict (Differentiable (D f))

then you can manually open the dictionary whenever you need to recurse.

This would let you employ the general shape of the solution in Casey's answer, but not have the compiler (or runtime) spin forever on induction.

With the new UndecidableSuperclasses in GHC 8

class Differentiable (D f) => Differentiable (f :: Type -> Type) where

works.

Can I constrain a type family?

Related

Recent Posts