#16315: Pattern synonym implicit existential quantification -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: | Keywords: 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 goldfire): OK. Now I understand what you're doing better. Here is how I see it: 1. The renamer really shouldn't bring any of the existentials into scope, as existentials in a pattern synonym type don't scope over the (entire) pattern synonym body. 2. But the renamer can't tell existential implicitly bound variables from universal ones. 3. So, the renamer brings into scope only the universals and all the implicitly bound ones. This brings more variables into scope than it should. 4. The pattern synonym body then is renamed with some extra variables in scope, so more uniques match between the body and the type than morally should. In addition, less implicit quantification happens in the body than morally should. 5. The type-checker must deal with this unfolding disaster by duplicating the renamer's strange behavior: it brings into scope implicitly-bound existentials, just so that weird out-of-scope errors don't happen in the body. But it arranges to error if these are encountered, regardless. 6. The program in this ticket observes that the difference in treatment between implicitly bound and explicitly bound is awkward. 7. Your proposed solution is just to bring all existentials into scope in both the renamer and the type-checker, so that treatment is uniform. This is done even though existentials really shouldn't scope over the body. 8. This ticket is all about uniformity. The behavior in both the explicit case and the implicit case is, by itself, correct. But it's awkward for GHC's behavior to depend on the user's choice of implicit vs explicit binding. Is that a fair assessment? If so, I advocate: do nothing. This problem goes away when type variables and kind variables are treated identically, because if the user writes a `forall`, they will have to bind the kind variables explicitly anyway. If the user does not write a `forall`, then no scoping of type variables happens, so there's no problem here. And, the patch as written actually makes GHC's behavior worse, in that it's further from the ideal of "existentials do not scope". The only reason to do this patch is that we cannot achieve the ideal, and this patch does indeed (and correctly, as far as I can tell) make the behavior more uniform. So I do think the best way to fix this problem is to ignore it and wait for it to go away. :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16315#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler