content: {-# LANGUAGE GADTs #-}
  
  -- From the ghc-users mailing list
  
  module Foo where
  
  data TValue t where
    TList :: [a] -> TValue [a]
  
  instance (Eq b) => Eq (TValue b) where
      (==) (TList p) (TList q) = (==) p q
  
  {- My reply to the list
  
  Here's the reasoning (I have done a bit of renaming).
  
  * The TList constructor really has type
          TList :: forall a. forall x. (a~[x]) => [x] -> TValue a
  
  * So in the pattern match we have
          (Eq b) available from the instance header
          TList p :: TValue b
          x is a skolem, existentially bound by the pattern
          p :: [x]
          b ~ [x] available from the pattern match
  
  * On the RHS we find we need (Eq [x]).
  
  * So the constraint problem we have is
          (Eq b, b~[x]) => Eq [x]
            ["Given"  =>  "Wanted"]
    Can we prove this?  From the two given constraints we can see
    that we also have Eq [x], and that certainly proves Eq [x].
  
  
  Nevertheless, it's a bit delicate.  If we didn't notice all the
  consequences of the "given" constraints, we might use the top-level Eq
  a => Eq [a] instance to solve the wanted Eq [x].  And now we need Eq
  x, which *isn't* a consequence of (Eq b, b~[x]).
  
  -}
  