#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