[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
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Looks absolutely right to me.   `foo`'s argument type is `Foo x` not `Foo
 Bool`.  Only ''after'' matching A do we get `Foo Bool`.  But the type
 signature is matched before we get to the A part.

 Better to consider something more like the original question:
 {{{
 data Bar x where
   MkBar :: Typeable b => a -> Bar (a,b)

 bar :: Bar x -> string
 bar (MkBar @a @b _) = show (typeRep (Proxy :: Proxy b))
 }}}
 Here you want to use mention the type variable `b`.  But there is no way
 to bring it into scope since we don't have visible type applications in
 patterns (yet #11350).

 I think that's really the right solution too.

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