What is TypeCast actually for?
It isn't used for retrieving type information about existential types (that would break the type system, so it is impossible). To understand TypeCast
, we first have to understand some particular details about the haskell type system. Consider the following motivating example:
data TTrue
data TFalse
class TypeEq a b c | a b -> c
instance TypeEq x x TTrue
instance TypeEq x y TFalse
The goal here is to have a boolean flag - on the type level - which tells you if two types are equal. You can use ~
for type equivalence - but this only gives you failure on type in equivalence (ie Int ~ Bool
doesn't compile as opposed to TypeEq Int Bool r
will give r ~ TFalse
as the inferred type). However, this doesn't compile - the functional dependencies conflict. The reason is simple - x x
is just an instantiation of x y
(ie x ~ y
=> x y == x x
), so according to the rules of fundeps (see the docs for full details of the rules) , the two instances must have the same value for c
(or the two values must be insantiations of one another - which they aren't).
The TypeEq
class exists in the HList
library - lets take a look how it is implemented:
class HBool b => TypeEq x y b | x y -> b
instance TypeEq x x HTrue
instance (HBool b, TypeCast HFalse b) => TypeEq x y b
-- instance TypeEq x y HFalse -- would violate functional dependency
Naturally these instance don't conflict - HTrue
is an instantiation of b
. But wait! Doesn't TypeCast HFalse b
imply that b
must be HFalse
? Yes, it does, but the compiler does not check the class instance constraint when attempting to resolve fundep conflicts. This is the key 'feature' which allows this class to exist.
As a brief note - the two instances still overlap. But with -XUndecidableInstances -XOverlappingInstances
, the compiler will choose the first instance preferentially, due to the fact that the first instance is more 'specific' (in this case, that means it has at most 2 unique types - x
and HTrue
, while the other instance has at most 3). You can find the full set of rules that UndecidableInstances
uses in the docs.
Why is TypeCast written the way it is?
If you look in the source for HList, there are multiple implementations of TypeCast
. One implementation is:
instance TypeCast x x
The straightforward instance one would assume will work. Nope! From the comments in the file containing the above definition:
A generic implementation of type cast. For this implementation to
work, we need to import it at a higher level in the module hierarchy
than all clients of the class. Otherwise, type simplification will
inline TypeCast x y, which implies compile-time unification of x and y.
That is, the type simplifier (whose job it is to remove uses of type synonyms and constant class constraints) will see that x ~ y
in TypeCast x x
since that is the only instance that matches, but only in certain situations. Since code that behaves differently in different cases is 'Very Bad', the authors of HList have a second implementation, the one in your original post. Lets take a look:
class TypeCast a b | a -> b, b -> a
class TypeCast' t a b | t a -> b, t b -> a
class TypeCast'' t a b | t a -> b, t b -> a
instance TypeCast' () a b => TypeCast a b
instance TypeCast'' t a b => TypeCast' t a b
instance TypeCast'' () a a
In this case, TypeCast x y
can never be simplified without looking at the class constraint (which the simplifier will not do!); there is no instance head which can imply x ~ y
.
However, we still need to assert that x ~ y
at some point in time - so we do it with more classes!
The only way we can know a ~ b
in TypeCast a b
is if TypeCast () a b
implies a ~ b
. This is only the case if TypeCast'' () a b
implies a ~ b
, which it does.
I can't give you the whole story unfortunatley; I don't know why
instance TypeCast' () a b => TypeCast a b
instance TypeCast' () a a
doesn't suffice (it works - I don't know why it wouldn't be used). I suspect it has something to do with error messages. I'm sure you could track down Oleg and ask him!