Instance-based predicate type?

Question

To create a type class that accepts natures like Z, (SZ), (S (SZ)), etc., you can simply declare instances recursively as such:

data Z data S a class Type a instance Type Z instance Type (S a) 

Is it possible to instantiate a type class based on level predicates? For example, I want to say:

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

Where :+: is the addition of a type level, and == is the level correspondence at the level from Data.Type.Equality , therefore instances are created only for pairs of nats that are up to 8.

Are notations like this available in Haskell? If not, how would this be done?

Edit: This post was inspired by a Haskell Wiki article on intelligent constructors declaring an InBounds class type to statically verify that the phantom type argument passed to the intelligent constructor was in a certain Nat s range, the intelligent constructor was:

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

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

 construct :: (Type ab) => a -> b -> MyType ab construct _ _ = MyType >>> Expected a type, but a has kind Nat… 

The Haskell file wiki example works because it does not use DataKinds, is it possible to pass a type of Nat type to a level value function?

Answer 1

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

 {-# LANGUAGE KindSignatures, DataKinds, MultiParamTypeClasses, FlexibleInstances, GADTs #-} import GHC.TypeLits class Type (a :: Nat) (b :: Nat) instance (a + b) ~ 8 => Type ab 

Remember that this is not necessarily as useful as it might look - the equality constraint does not in any way list all combinations that are up to 8, but allows all instances of Nat be an instance, it only requires proof that they add up to 8. This is a proof, which you can use, but I doubt that Haskell still just naturalizes the character that does this job very well.

Answer 2

You can write a level level function

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

And then

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

Of course you need to include a bunch of extensions.

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