text: {-# LANGUAGE GADTs, RankNTypes #-}
  
  -- Test pattern bindings, existentials, and higher rank
  
  module T12427a where
  
  data T where
    T1 :: a -> ((forall b. [b]->[b]) -> Int) -> T
    T2 :: ((forall b. [b]->[b]) -> Int) -> T
  
  -- Inference
  -- Worked in 7.10 (probably wrongly)
  -- Failed in 8.0.1
  -- Fails in 8.2 because v is polymorphic
  --     and the T1 pattern match binds existentials,
  --     and hence bumps levels
  h11 y = case y of T1 _ v -> v
  
  -- Worked in 7.10 (probably wrongly)
  -- Failed in 8.0.1
  -- Succeeds in 8.2 because the pattern match has
  --   no existentials, so it doesn't matter than
  --   v is polymorphic
  h12 y = case y of T2 v -> v
  
  -- Inference
  -- Same results as for h11 and h12 resp
  T1 _ x1 = undefined
  T2 x2 = undefined
  
  -- Works in all versions
  h2 :: T -> (forall b. [b] -> [b]) -> Int
  h2 y = case y of T1 _ v -> v
  
  -- Checking
  -- Fails in 7.10  (head exploded)
  -- Fails in 8.0.1 (ditto)
  -- Succeeds in 8.2
  -- Fails in 8.12 (simple subsumption)
  x3 :: (forall a. a->a) -> Int
  T1 _ x3 = undefined
  