Type level predicate based instances?

Question

To create a type class that accepts the type-level naturals Z, (S Z), (S (S Z))... etc, you can simply declare the instances recursively as such:

data Z
data S a

class Type a

instance Type Z
instance Type (S a)

Is it possible to create a type class instance based on type level predicates? For example, I want to be able to say:

{-# LANGUAGE MultiParamTypeClasses #-}
class Type a b
instance Type x y when (x :+: y == 8)

Where :+: is type level addition, and == is type-level equality from Data.Type.Equality, so that instances are only created for pairs of nats that add up to 8.

Is notation similar to this available in Haskell? If not, how would something like this be accomplished?

Edit: This post was inspired by the Haskell wiki article on smart constructors, where a type class InBounds was declared to statically verify that the phantom type argument passed to a smart constructor was in some range of Nats, the smart constructor was:

resistor :: InBounds size => size -> Resistor size
resistor _ = Resistor

Trying to do something similar in my example (after using leftaroundabout's answer) gives me an error:

construct :: (Type a b) => a -> b -> MyType a b
construct _ _ = MyType

>>> Expected a type, but a has kind Nat…

The example from the Haskell wiki works because it doesn't use DataKinds, is it possible to pass a type of kind Nat to a value-level function?

Answer 1

You need to use not an equality predicate but an equality constraint (which is baked into the language, enable with -XGADTs).

{-# LANGUAGE KindSignatures, DataKinds, MultiParamTypeClasses, FlexibleInstances, GADTs #-}

import GHC.TypeLits

class Type (a :: Nat) (b :: Nat)

instance (a + b) ~ 8 => Type a b

Mind that this isn't necessarily as useful as it might look – the equality constraint does not in some way enumerate all combinations that add up to 8, rather it allows all Nat-pairs to be instance, only demands a proof that they add up to 8. This proof you can use, but I doubt Haskell's still just sort-of-dependently typed nature makes this work really well.

Answer 2

You could write a type level function

type family NatEq (a :: Nat) (b :: Nat) :: Bool
type instance NatEq 0 0 = True
...

And then

instance Type' (NatEq (a + b) 8) a b => Type a b
class Type' (x :: Bool) (a :: Nat) (b :: Nat) where ...
instance Type' True a b where ...
-- If you wanted a different behaviour otherwise:
-- instance Type' False a b where ...

You will need to enable a bunch of extensions, of course.

This works fine if a and b are constants, so that a+b can be reduced to 8 (or another constant). If they are not constants, don't expect GHC to prove the equation for you. That is (using Int instead of Nat), don't expect Type x (8-x) to be solved.