[Haskell-cafe] Help understanding type error

[Matthew Brecknell]

Levi Stephen:
> I have a data type:
> 
> > data T a = forall b. (Show b) => T b a
> 
> and I want to use/extract 'b' from this.

You can't. (Well, I believe you can if you have prior knowledge of the
actual type of the existentially wrapped "b", and you're willing to use
an "unsafe" coerce, but I've never tried.)

Existential types are useful as a kind of type-erasure. Consider the
type of the "T" constructor:

T :: Show b => b -> a -> T a

Clearly, the type of the first component disappears in the construction
of the return value. The advantage of this is that you can construct
values using different types in the first component, but treat all of
the constructed values as the same type. But as a consequence, you
cannot retrieve the type that was used to construct any given "T a".

> > extShow (T b _) = b

In practical terms, the return type of this function would have to be
the concrete type that was previously used to construct the parameter
value, but that type is no longer known. In more technical terms (if you
can excuse my amateur type theory), the type of the first component is
existentially bound to the data constructor, which means it can't be
referenced outside the scope of the pattern match. With that, maybe you
can make more sense of the error message:

> This gives the following compilation error:
> 
> extest.hs:5:0:
>      Inferred type is less polymorphic than expected
>        Quantified type variable `b' escapes
>      When checking an existential match that binds
> 	$dShow :: {Show b}
> 	b :: b
>      The pattern(s) have type(s): T t
>      The body has type: b
>      In the definition of `extShow': extShow (T b _) = b
> 
> I tried adding a type signature:
> 
> > extShow' :: (Show b) => T a -> b
> > extShow' (T b _) = b

The meaning of your type signature is: Given any type "a", any type "b"
in class "Show", and a value of type "T a", return a value of type "b".
In particular, the type "b" of the return value is determined by the
environment of the call to extShow'. It is not the same as the of the
"b" hidden within the existential wrapper. Hence the failure to match
those two types indicated in the error message:

> Now I get a different error:
> 
> extest.hs:8:19:
>      Couldn't match expected type `b' (a rigid variable)
> 	   against inferred type `b1' (a rigid variable)
>        `b' is bound by the type signature for `extShow'' at
>        extest.hs:7:18
>        `b1' is bound by the pattern for `T' at extest.hs:8:10-14
>      In the expression: b
>      In the definition of `extShow'': extShow' (T b _) = b
> 
> It seems (to newbie me ;) ) like it should be possible to extract the
> first part 
> of T, and deduce that it is an instance of the class 'Show'.

Not quite. You know that it has a type in the class "Show", but you
cannot extract the actual type. The only thing you can do is to apply
methods from the Show class, and you must do so within the scope of the
pattern match, so that the actual type (which is unknown) does not
escape. That's why the following snippet works:

> The following seems ok:
> 
> > doShow (T b _) = putStrLn (show b)

It sounds like you've already read the section on existential types in
the GHC user guide. If not, check it out for details of the rules.