#11700: pattern match bug -------------------------------------+------------------------------------- Reporter: TobyGoodwin | Owner: Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 7.10.3 checker) | Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: | typecheck/should_compile/T11700, | ExPat, ExPatFail Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * testcase: => typecheck/should_compile/T11700, ExPat, ExPatFail * status: new => closed * resolution: => fixed Comment: Well that has been lurking a long time. It was caused by the fact that when the pattern binds dictionaries (which this one does), we make an implication constraint, and bump the `TcLevel`. Normally that doesn't happen because GHC complains about a pattern binding that binds existential variables. But this one doesn't! It only binds constraints! Anyway it demonstrated to me that the way we were dealing with existentials in pattern bindings was all wrong... better to ''use'' the machinery of implication constraints, rather than cut across it. Here's the new method (a Note in `TcBinds`). Much nicer! And it actually allows more programs too. {{{ {- Note [Existentials in pattern bindings] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider (typecheck/should_compile/ExPat): data T where MkT :: Integral a => a -> Int -> T and suppose t :: T. Which of these pattern bindings are ok? E1. let { MkT p _ = t } in <body> E2. let { MkT _ q = t } in <body> E3. let { MkT (toInteger -> r) _ = t } in <body> Well (E1) is clearly wrong becuase the existential 'a' escapes. What type could 'p' possibly have? But (E2) is fine, despite the existential pattern, because q::Int, and nothing escapes. Even (E3) is fine. The existential pattern binds a dictionary for (Integral a) which the view pattern can use to convert the a-valued field to an Integer, so r :: Integer. An easy way to see all three is to imagine the desugaring. For (2) it would look like let q = case t of MkT _ q' -> q' in <body> We typecheck pattern bindings as follows: 1. In tcLhs we bind q'::alpha, for each varibable q bound by the pattern, where q' is a fresh name, and alpha is a fresh unification variable; it will be the monomorphic verion of q that we later generalise It's very important that these fresh unification variables alpha are born here, not deep under implications as would happen if we allocated them when we encountered q during tcPat. 2. Still in tcLhs, we build a little environment mappting "q" -> q':alpha, and pass that to tcLetPet. 3. Then tcLhs invokes tcLetPat to typecheck the patter as usual: - When tcLetPat finds an existential constructor, it binds fresh type variables and dictionaries as usual, and emits an implication constraint. - When tcLetPat finds a variable (TcPat.tcPatBndr) it looks it up in the little environment, which should always succeed. And uses tcSubTypeET to connect the type of that variable with the expected type of the pattern. And that's it! The implication constraints check for the skolem escape. It's quite simple and neat, and more exressive than before e.g. GHC 8.0 rejects (E2) and (E3). }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11700#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler