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.

This does what you want, I think: {-# LANGUAGE ExistentialQuantification #-} module Exist where data Showable = forall a. (Show a) => Showable a instance Show Showable where showsPrec p (Showable a) = showsPrec p a show (Showable a) = show a -- You have to use the default implementation of showList -- because a list could be heterogeneous data T a = forall b. (Show b) => T b a extShow :: T a -> Showable extShow (T b _) = Showable b -- ryan