#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