#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: -------------------------------------+------------------------------------ Changes (by goldfire): * status: new => closed * resolution: => invalid Comment: This seems to be exactly the scenario in #6075. Essentially, GHC checks patterns from the outside working in, so it sees the type before the constructor, and before it knows about the GADT pattern match. I believe I've worked around this by doing the following painful construction: {{{ lengthSing = case sing :: Sing xs of SNil -> Tagged 0 SCons -> case sing :: Sing xs of (SCons :: Sing (x ': xs')) -> Tagged (1 + untag (lengthSing :: Tagged xs' Int)) }}} There may be a better way, but that's what I've done and it works. I suppose you could re-open as a feature request to change this behavior, if you feel so inclined. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9108#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler