Why doesn't TypeSynonymInstances allow partially applied type synonyms to be used in instance heads?

Partially applied type synonyms are not allowed in Haskell at all. A partially applied synonym is effectively a function whose inputs are the un-applied types and whose output is a type. For example, here is an encoding of boolean logic:

type True x y = x
type False x y = y
type Not b x y = b y x
type And b1 b2 x y = b1 (b2 x y) y
type Or b1 b2 x y = b1 x (b2 x y)

To decide whether two partially applied type synonyms are equal, the type checker would have to decide whether functions are equal. This is a hard problem, and in general it is undecidable.


Another issue with allowing partially applied type synonyms is that they would make type inference and instance selection essentially impossible. For example, suppose in the context of some program I wanted to use thingy at the type Int -> String -> Int -> (Int, String). thingy has type forall a b e. a -> b -> e a b, so we can unify a with Int and b with String, but if e is allowed to be a partially applied type synonym, we could have

e = FuncSynonym (,)

or

e = FuncSynonym' Int (,) where type FuncSynonym' x f a b = x -> f a b

or even

e = Const2 (Int -> (Int, String)) where Const2 a x y = a

The problem of type inference would become even worse than deciding equality of functions; it would require considering all functions with specified output on a particular input, or similar more complicated problems (imagine simply trying to unify a b with Int).

Tags:

Haskell