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.