Haskell type synonym declaration with constraint possible?

Use data and parameters, not existentials to get contexts

I think if you wanted

data Thing = Good [(Char,Int)] | Bad String | Indifferent Leg

but also sometimes

data Thing = Good [(Char,Float)] | Bad String | Indifferent Arm

You could define

data Thing num bodypart = Good [(Char,num)] | Bad String | Indifferent bodypart

or if you want to make sure num is always numeric, you could do

data Num num => Thing num bodypart = Good [(Char,num)] | Bad String | Indifferent bodypart

and finally, you could restrict the types allowed in bodypart by defining your own class:

class Body a where
   -- some useful function(s) here

instance Body Leg where
   -- define useful function(s) on Legs
instance Body Arm
   -- define useful function(s) on Arms

data (Num num,Body bodypart) => Thing num bodypart = 
                                                             Good [(Char,num)] | Bad String | Indifferent bodypart

I'd like to discourage you from using existential types via the forall constructor or via GADTs because adding the num parameter to your data type is considerably more useful in practice, even though it takes more typing.

Constraints on type synonyms?

Note that when you use a constraint like

data (Num num) => Thing num = T [(Char,num)]

really only changes the type of the constructor T to

T :: (Num num) => [(Char,num)] -> Thing num

instead of T :: [(Char,num)] -> Thing num. This means every time you use T, there needs to be a context (Num num), but that's really what you wanted - to stop people putting data in your data type that isn't numeric.

A consequence of this fact is that you can't write

type Num num => [(Char,num)]

because there's no data constructor function T for the context (Num num) to be required on; if I have a [('4',False)], it automatically matches the type [(Char,num)] because it's a synonym. The compiler can't be going running around your code looking for instances before it decides what type something is. In the data case, it's got a constructor T that tells it the type, and it can guarantee there's a Num num instance because it checked your use of the function T. No T, no context.

This corresponds to existential quantification. In pseudo-Haskell,

type NumberList = exists a . Num a => [a]

I say «pseudo» because GHC doesn't allow introducing existential quantifiers on the fly — you need to create a separate datatype for that.

Now, most of the type you'd use NumberList to the left of the arrow, where «exists» effectively changes its meaning to «forall».

That is, instead of writing

isIncreasing :: NumberList -> Bool

which is the same as

isIncreasing :: (exists a . Num a => [a]) -> Bool

you can write

isIncreasing :: forall a . Num a => [a] -> Bool

or simply

isIncreasing :: Num a => [a] -> Bool

Of course, having a type synonym seems like less code, but it has disadvantages as well. These disadvantages, by the way, are typical for object-oriented programming, which is based on the existential approach.

For example, you want to concatenate two lists. Ordinarily you would write

(++) :: forall a . [a] -> [a] -> [a]

(where again forall is unnecessary and added for clarity). Since a is the same across the entire signature, that ensures that you are concatenating lists of the same type.

How do we concatenate two numeric lists? A signature

(++) :: NumberList -> NumberList -> NumberList

wouldn't work, since one list may contain Ints and the other may contain Doubles. And the resulting NumberList has to contain values of a single type.

Or, say, you want to find the sum of the list elements.

Usually you write

sum :: Num a => [a] -> a

Notice that the result type is the same as the type of list elements. Alas, we cannot do the same for NumberList!

sum :: NumberList -> ???

What is the result type? We could apply existential quantification there as well.

sum :: NumberList -> (exists a . Num a => a)

But now the connection between the original list type and the sum type is lost — at least for Haskell's type system. If you then decide to write a function like

multiplySum :: Integer -> [Integer] -> Integer
multiplySum x ys = x * sum ys

then you'll get a type error, because sum ys may be of any type, not necessarily of type Integer.

It would work if you pushed everything to extreme and made every type existentially-quantified — but then you'd end up essentially with another object-oriented-like language with all their problems.

(That said, there are some good use cases for existential quantification, of course.)