[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:  (none)
            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 RyanGlScott):

 Replying to [comment:6 simonpj]:
 > Because until you have matched on `SCons` we don't have `l ~ x:xs`.  I
 think you are thinking that, because the type signature is "to the right"
 of the match, you can take advantage of it.

 The position of the type signature has nothing to do with my confusion.
 I'm confused because it's been drilled into my skull that the act of
 pattern matching on a GADT constructor in a case changes the typing rules
 (or, more precisely, it introduces new given constraints) for that case.
 The fact that I can use these given constraints for the types of
 subpatterns of `SCons ...`, but for the type of the `SCons ...` pattern
 itself, feels oddly disjointed.

 To highlight the strangeness of this further, you can do what I desire
 simply by adding another `case` expression:

 {{{#!hs
 fl :: forall (l :: [a]). Sing l -> Sing l
 fl SNil = SNil
 fl a@(SCons (x :: Sing x) (xs :: Sing xs)) =
   case a of
     (a :: Sing (x ': xs)) -> SCons x xs
 }}}

 I'd rather cut out of the middleman and just put that `Sing (x ': xs)`
 type directly on the `SCons ...` pattern.

 > To put it another way, we currently
 [https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17
 explain pattern matching in the Haskell report] via simple case
 expressions.  Currently we have
 > {{{
 > case v of ( p::ty -> e1; _ -> e2 }
 > --->
 > case (v::ty) of { p -> e2; _ -> e2 }
 > }}}

 I'm not sure where you got that rule from in the link you provided.

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