[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 simonpj):

 >  Why not?

 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.  But in fact it's more like
 the type signature encloses the pattern, so it's more like this
 {{{
 fl (Sing (x ': xs) ::: SCons (x :: Sing x) (xs :: Sing xs)) = SCons x xs
 }}}
 Here I've used `ty ::: Pat` to put a type sig syntactically "before" the
 pattern. Now perhaps you would not expect to have matched yet?

 What about this
 {{{
 g (Just [SCons x xs] :: Maybe [Sing (a ': as)]) = ...
 }}}
 presumably you want the pattern to match deeply first.

 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 }
 }}}
 But I suppose we could say something like
 {{{
 case v of ( p::ty -> e1; _ -> e2 }
 ---->
 case v of { p -> let (v2::ty) = v in e1
           ; _ -> e2 }
 }}}
 where the type signature is not applied until after the match.

 I can't say I'm terribly fired up about this.

 I'm not sure how easy it'd be to match the signature "after" the match.

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