Because until you have matched on `SCons` we don't have `l ~ x:xs`. I
#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: lowest | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Keywords: GADTs, Resolution: | ScopedTypeVariables Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:6 simonpj]: think you are thinking that, because the type signature is "to the right" of the match, you can take advantage of it. The position of the type signature has nothing to do with my confusion. I'm confused because it's been drilled into my skull that the act of pattern matching on a GADT constructor in a case changes the typing rules (or, more precisely, it introduces new given constraints) for that case. The fact that I can use these given constraints for the types of subpatterns of `SCons ...`, but for the type of the `SCons ...` pattern itself, feels oddly disjointed. To highlight the strangeness of this further, you can do what I desire simply by adding another `case` expression: {{{#!hs fl :: forall (l :: [a]). Sing l -> Sing l fl SNil = SNil fl a@(SCons (x :: Sing x) (xs :: Sing xs)) = case a of (a :: Sing (x ': xs)) -> SCons x xs }}} I'd rather cut out of the middleman and just put that `Sing (x ': xs)` type directly on the `SCons ...` pattern.
To put it another way, we currently [https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.1... explain pattern matching in the Haskell report] via simple case expressions. Currently we have {{{ case v of ( p::ty -> e1; _ -> e2 } ---> case (v::ty) of { p -> e2; _ -> e2 } }}}
I'm not sure where you got that rule from in the link you provided. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler