content: {-# LANGUAGE TypeFamilies, GADTs, RankNTypes #-}
  
  module GADT10 where
  
  -- [Sept 2010] Now works in GHC 7.0!
  
  -- This fails with
  --
  -- GADT10.hs:37:0:
  --     All of the type variables in the constraint `x ~
  --                                                  y' are already in scope
  --         (at least one must be universally quantified here)
  --     In the type signature for `foo':
  --       foo :: EQUAL x y -> ((x ~ y) => t) -> t
  -- 
  -- GADT10.hs:38:4:
  --     Couldn't match expected type `y' against inferred type `x'
  --       `y' is a rigid type variable bound by
  --           the type signature for `foo' at GADT10.hs:8:15
  --       `x' is a rigid type variable bound by
  --           the type signature for `foo' at GADT10.hs:8:13
  --     In the pattern: EQUAL
  --     In the definition of `foo': foo EQUAL t = t
  --
  -- The first error can be fixed by using FlexibleContexts but I don't think that
  -- should be required here. In fact, if we remove RankNTypes, we get
  --
  --     Illegal polymorphic or qualified type: forall (co_wild_B1 :: x ~
  --                                                                  y).
  --                                            t
  --     In the type signature for `foo':
  --       foo :: EQUAL x y -> ((x ~ y) => t) -> t
  --
  -- which seems to contradict (at least sort of) the first error message.
  
  data EQUAL x y where
    EQUAL :: EQUAL x x
  
  foo :: EQUAL x y -> (x~y => t) -> t
  foo EQUAL t = t
  
  bar :: EQUAL x y -> x -> y
  bar equ x = foo equ x
  
  