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

 Ah, that's where the catch is -- of course. That makes sense. Tricky. For
 the record, Andres' workaround was

 {{{
 type family Tail (xs :: [k]) :: [k]
 type instance Tail (x ': xs) = xs

 lengthSing :: forall (xs :: [k]). SingI xs => Tagged xs Int
 lengthSing = case sing :: Sing xs of
   SNil  -> Tagged 0
   SCons -> Tagged (1 + untag (lengthSing :: Tagged (Tail xs) Int))
 }}}

 which avoids a second pattern match.

 The fact that we need a workaround at all does seem unfortunate but I
 understand better now why it's required. Tricky :)

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