[GHC] #16315: Pattern synonym implicit existential quantification
GHC
ghc-devs at haskell.org
Fri Feb 15 15:20:25 UTC 2019
#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
More information about the ghc-tickets
mailing list