#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 simonpj):
Why not?
Because until you have matched on `SCons` we don't have `l ~ x:xs`. I think you are thinking that, because the type signature is "to the right" of the match, you can take advantage of it. But in fact it's more like the type signature encloses the pattern, so it's more like this {{{ fl (Sing (x ': xs) ::: SCons (x :: Sing x) (xs :: Sing xs)) = SCons x xs }}} Here I've used `ty ::: Pat` to put a type sig syntactically "before" the pattern. Now perhaps you would not expect to have matched yet? What about this {{{ g (Just [SCons x xs] :: Maybe [Sing (a ': as)]) = ... }}} presumably you want the pattern to match deeply first. 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 } }}} But I suppose we could say something like {{{ case v of ( p::ty -> e1; _ -> e2 } ----> case v of { p -> let (v2::ty) = v in e1 ; _ -> e2 } }}} where the type signature is not applied until after the match. I can't say I'm terribly fired up about this. I'm not sure how easy it'd be to match the signature "after" the match. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler