#12018: Equality constraint not available in pattern type signature (GADTs/ScopedTypeVariables) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: 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):
Is this an intended design of GADTs/ScopedTypeVariables that the type equality constraint isn't in scope in the type signature of the pattern match
Yes, it is. The type equalities are available only "after" the match. For your second point I need a more complete example. To bind an existential you need a pattern type sig. Eg {{{ data T where MkT :: a -> ([a]->Int) -> T f (MkT (x :: a) f) = f ([x,x] :: [a]) }}} The pattern signature `(x :: a)` binds `a`. Currently that's the only way to bind an existential type variable. #11350 would be a good alternative. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/12018#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler