#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 RyanGlScott): Replying to [comment:5 goldfire]:
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.
You lost me here. The problem is that if you write out the kind variable in the original program explicitly: {{{#!hs pattern P :: forall. () => forall k (a :: k). Proxy a -> T pattern P x = MkT (x :: Proxy (a :: k)) }}} Then GHC //accepts// it, contrary to the claims of `Note [Pattern synonym existentials do not scope]`. So no, this problem won't go away when type and kind variables are treated identically. (In fact, int-index had to specifically mark this test case as `expect_broken` in his [https://gitlab.haskell.org/ghc/ghc/merge_requests/361 patch] to implement the type-kind-variable merger.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16315#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler