[GHC] #9108: GADTs and pattern type annotations?

[GHC]

#9108: GADTs and pattern type annotations?
-------------------------------------+------------------------------------
        Reporter:  edsko             |            Owner:
            Type:  bug               |           Status:  closed
        Priority:  normal            |        Milestone:
       Component:  Compiler          |          Version:  7.8.2
      Resolution:  invalid           |         Keywords:
Operating System:  Unknown/Multiple  |     Architecture:  Unknown/Multiple
 Type of failure:  None/Unknown      |       Difficulty:  Unknown
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+------------------------------------

Comment (by simonpj):

 There is a slightly nicer encoding than Richards:
 {{{
 lengthSing = case (sing :: Sing xs, sing) of
   (SNil, _) -> Tagged 0
   (SCons, _ :: Sing (x ': xs')) -> Tagged (1 + untag (lengthSing :: Tagged
 xs' Int))
 }}}
 We could try to make pattern signatures behave like this all the time.
 It's not even hard to do; I tried it and got these testsuite failures in
 `typecheck/` alone:
 {{{
 Unexpected failures:
    should_compile  T7827 [exit code non-0] (normal)
    should_compile  tc194 [exit code non-0] (normal)
    should_compile  tc211 [stderr mismatch] (normal)
    should_fail     T5691 [stderr mismatch] (normal)
 }}}
 One reason is that it doesn't work for 'foralls'.  Currently this works
 (just), and is quite convenient:
 {{{
 f  = \(x :: forall a. a -> a) -> (x True, x 'v')
 }}}
 But if you imagine applying the type signature "after the match", we'd end
 up unifying a forall type with a unification variable, which isn't
 allowed.


 Another thing that bugs me is that the unification that arises from a
 pattern signature gives rise to a coercion.  What do we do with that
 coercion under the "match first then apply signature" story?

 I'm not sure what to do here.

 Simon

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