[GHC] #12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables)

[GHC]

#12018: Equality constraint not available in pattern type signature
(GADTs/ScopedTypeVariables)
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:
            Type:  bug               |               Status:  new
        Priority:  lowest            |            Milestone:
       Component:  Compiler (Type    |              Version:  7.10.3
  checker)                           |             Keywords:  GADTs,
      Resolution:                    |  ScopedTypeVariables
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 > Is this an intended design of GADTs/ScopedTypeVariables that the type
 equality constraint isn't in scope in the type signature of the pattern
 match

 Yes, it is.  The type equalities are available only "after" the match.

 For your second point I need a more complete example.  To bind an
 existential you need a pattern type sig.  Eg
 {{{
 data T where
   MkT :: a -> ([a]->Int) -> T

 f (MkT (x :: a) f) = f ([x,x] :: [a])
 }}}
 The pattern signature `(x :: a)` binds `a`. Currently that's the only way
 to bind an existential type variable.  #11350 would be a good alternative.

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