[GHC] #13430: Can't scope type variables when pattern matching on GADTs

[GHC]

#13430: Can't scope type variables when pattern matching on GADTs
-------------------------------------+-------------------------------------
           Reporter:  crockeea       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.0.2
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I was very surprised that the following doesn't compile:

 {{{
 {-# LANGUAGE GADTs, ScopedTypeVariables #-}

 data Foo x where
   A :: Foo Bool
   B :: Foo Int

 foo :: Foo x -> ()
 foo (A :: Foo Bool) = ()
 }}}

 GHC says that it couldn't match the type `y` with `Bool`. See [this
 question](http://stackoverflow.com/questions/42824949/type-inference-with-
 gadts) for a simple motivating example. As someone there pointed out, the
 situation would be improved with type application (#11350), but this
 ticket is about bringing the output type in scope with
 `ScopedTypeVariables`.

 This most closely reminds me of #1823 (!), but that was resolved many
 moons ago. This behavior also exists in 7.10.3.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/13430>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler