#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