[GHC] #16315: Pattern synonym implicit existential quantification

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
14 messages Options
Reply | Threaded
Open this post in threaded view
|

[GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
#16315: Pattern synonym implicit existential quantification
-------------------------------------+-------------------------------------
           Reporter:  int-index      |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This code typechecks when `k` is brought into scope explicitly, but not
 implicitly (code example courtesy of RyanGlScott):

 {{{#!hs
 {-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 data T = forall k (a :: k). MkT (Proxy a)

 -- Uncomment `k` and it typechecks
 pattern P :: forall. () => forall {-k-} (a :: k). Proxy a -> T
 pattern P x = MkT (x :: Proxy (a :: k))
 }}}

 I discovered this because I was implementing https://github.com/ghc-
 proposals/ghc-proposals/blob/master/proposals/0024-no-kind-vars.rst and
 had to explicitly quantify some definitions in the test suite. Then the
 test case for #14498 stopped producing the error that it should.

 It seems indicative of an issue in typechecking pattern synonyms: I would
 expect equal treatment for implicit and explicit type/kind variables.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
#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):

 I know what is happening here. There are two different culprits in the
 codebase: the renamer and the typechecker.

 The typechecker problem is much easier to understand. When typechecking
 the body of a pattern synonym, we bring certain type variables into scope.
 [https://gitlab.haskell.org/ghc/ghc/blob/4af0a2d609651c4bae45d84d2bf7ce9fe8cca350/compiler/typecheck/TcPatSyn.hs#L386-388
 Here] is the code that does it:

 {{{#!hs
            tcExtendTyVarEnv univ_tvs                 $
            tcExtendKindEnvList [(getName (binderVar ex_tv), APromotionErr
 PatSynExPE)
                                | ex_tv <- extra_ex] $
 }}}

 We bring the universal (required) type variables into scope, of course. We
 also bring the "existential" (provided) type variables into scope so that
 if we find any occurrences of them in the pattern synonym body, we can
 throw the relevant `APromotionErr` error.

 Why did I write "existential" in scare quotes? Because the only
 existential type variables that are being brought into scope are the
 //implicitly quantified// ones (`extra_ex`). The remaining explicitly
 quantified ones (which live in `ex_bndrs`) are never brought into scope.
 Fortunately, fixing that is as simple as replacing `extra_ex` with
 `ex_bndrs` in the code above.

 However, that change alone won't be enough. There is another problem in
 that GHC treats the occurrence of `k` in the pattern synonym type
 signature as being completely different from the occurrence of `k` in the
 body. Why? It's ultimately due to the renamer. In particular, because of
 the `forall`-or-nothing rule, the only explicitly quantified type
 variables that can ever brought into scope over the body must appear in a
 `forall` at the very front of the type signature. Since `k` is quantified
 by a nested `forall`, it is never brought into scope over the body during
 renaming, so the renamer gives a different unique to the occurrence of `k`
 in the body. (This is why GHC doesn't throw an error about `k` when
 typechecking the body, since the `k` that would throw an `APromotionErr`
 is actually different from the `k` in the body.)

 I believe that we should be able to tweak things so that the renamer
 brings in the explicitly quantified universals //and// existentials from a
 pattern synonym type signature. Experimentally, this change was sufficient
 to accomplish that:

 {{{#!diff
 diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
 index 5eeca6eac2..fe6849b955 100644
 --- a/compiler/hsSyn/HsTypes.hs
 +++ b/compiler/hsSyn/HsTypes.hs
 @@ -51,7 +51,7 @@ module HsTypes (
          mkEmptyImplicitBndrs, mkEmptyWildCardBndrs,
          mkHsQTvs, hsQTvExplicit, emptyLHsQTvs, isEmptyLHsQTvs,
          isHsKindedTyVar, hsTvbAllKinded, isLHsForAllTy,
 -        hsScopedTvs, hsWcScopedTvs, dropWildCards,
 +        hsScopedTvs, hsPatSynScopedTvs, hsWcScopedTvs, dropWildCards,
          hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
          hsLTyVarName, hsLTyVarLocName, hsExplicitLTyVarNames,
          splitLHsInstDeclTy, getLHsInstDeclHead,
 getLHsInstDeclClass_maybe,
 @@ -959,6 +959,20 @@ hsScopedTvs sig_ty
    | otherwise
    = []

 +hsPatSynScopedTvs :: LHsSigType GhcRn -> [Name]
 +hsPatSynScopedTvs sig_ty
 +  | HsIB { hsib_ext = vars
 +         , hsib_body = sig_ty2 } <- sig_ty
 +  , L _ (HsForAllTy { hst_bndrs = tvs, hst_body = body }) <- sig_ty2
 +  = vars ++ map hsLTyVarName (tvs ++ body_tvs body)
 +  | otherwise
 +  = []
 +  where
 +    body_tvs :: LHsType GhcRn -> [LHsTyVarBndr GhcRn]
 +    body_tvs (L _ (HsForAllTy { hst_bndrs = tvs })) = tvs
 +    body_tvs (L _ (HsQualTy { hst_body = body }))   = body_tvs body
 +    body_tvs _                                      = []
 +
  {- Note [Scoping of named wildcards]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  Consider
 diff --git a/compiler/rename/RnBinds.hs b/compiler/rename/RnBinds.hs
 index ade67b7a49..fc5ffddfb0 100644
 --- a/compiler/rename/RnBinds.hs
 +++ b/compiler/rename/RnBinds.hs
 @@ -606,7 +606,7 @@ mkScopedTvFn sigs = \n -> lookupNameEnv env n `orElse`
 []
      get_scoped_tvs (L _ (TypeSig _ names sig_ty))
        = Just (names, hsWcScopedTvs sig_ty)
      get_scoped_tvs (L _ (PatSynSig _ names sig_ty))
 -      = Just (names, hsScopedTvs sig_ty)
 +      = Just (names, hsPatSynScopedTvs sig_ty)
      get_scoped_tvs _ = Nothing

  -- Process the fixity declarations, making a FastString -> (Located
 Fixity) map
 }}}

 Does this sound like the right approach?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 From the `Note [Pattern synonym existentials do not scope]`, it sounds
 like we aim to ''reject'' this code, not accept it. Do you find
 differently?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 Yes, I wrote comment:1 in mind with the goal of rejecting the original
 program.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 In case it wasn't clear:

 Replying to [comment:1 RyanGlScott]:
 > We also bring the "existential" (provided) type variables into scope so
 that if we find any occurrences of them in the pattern synonym body, //we
 can throw the relevant `APromotionErr` error//.

 (emphasis added)

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 You have a red herring in your soup.

 The following snippet is also accepted:

 {{{#!hs
 pattern P :: forall. () => forall k (a :: k). Proxy a -> T
 pattern P x = MkT (x :: Proxy (b :: j))
 }}}

 There's no scoping going on here, just the fact that these type variables
 are unconstrained.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 OK. If I understand you correctly, then the original program with `k`
 uncommented should be accepted. (I think you were hinting at this all
 along, but it wasn't obvious to me until comment:7.) If that's the case,
 then it sounds like the proper course of action is to:

 * Proceed with https://gitlab.haskell.org/ghc/ghc/merge_requests/374, as
 it will get rid of the awkwardness brought about by implicitly quantified
 variables being brought into scope.
 * Moreover, !374 can revert most of #14998:
   * There is no longer any need for `PatSynExPE`, since implicitly
 quantified existentials are no longer brought into scope.
   * `Note [Pattern synonym existentials do not scope]` can go away.
   * The `T14498` test case can be removed. (Or, alternatively, we could
 explicitly quantify `k` and move it to `patsyn/should_compile`.)

 Does this sound right?

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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):

 > Does this sound right?

 Yes, precisely.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16315: Pattern synonym implicit existential quantification
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:  fixed             |             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:                    |
-------------------------------------+-------------------------------------
Changes (by int-index):

 * status:  new => closed
 * resolution:   => fixed


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16315: Pattern synonym implicit existential quantification
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:  fixed             |             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:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/361
-------------------------------------+-------------------------------------
Changes (by int-index):

 * differential:   => https://gitlab.haskell.org/ghc/ghc/merge_requests/361


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:11>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16315: Pattern synonym implicit existential quantification
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.6.3
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  patsyn/should_compile/T14498
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/361
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * testcase:   => patsyn/should_compile/T14498
 * milestone:   => 8.10.1


--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:12>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #16315: Pattern synonym implicit existential quantification

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#16315: Pattern synonym implicit existential quantification
-------------------------------------+-------------------------------------
        Reporter:  int-index         |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.10.1
       Component:  Compiler          |              Version:  8.6.3
      Resolution:  fixed             |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
                                     |  patsyn/should_compile/T14498
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |  https://gitlab.haskell.org/ghc/ghc/merge_requests/361
-------------------------------------+-------------------------------------

Comment (by Marge Bot <ben+marge-bot@…>):

 In [changeset:"5bc195b1fe788e9a900a15fbe473967850517c3e/ghc"
 5bc195b1/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="5bc195b1fe788e9a900a15fbe473967850517c3e"
 Treat kind/type variables identically, demolish FKTV

 Implements GHC Proposal #24: .../ghc-proposals/blob/master/proposals/0024
 -no-kind-vars.rst
 Fixes Trac #16334, Trac #16315

 With this patch, scoping rules for type and kind variables have been
 unified: kind variables no longer receieve special treatment. This
 simplifies both the language and the implementation.

 User-facing changes
 -------------------

 * Kind variables are no longer implicitly quantified when an explicit
   forall is used:

     p ::             Proxy (a :: k)    -- still accepted
     p :: forall k a. Proxy (a :: k)    -- still accepted
     p :: forall   a. Proxy (a :: k)    -- no longer accepted

   In other words, now we adhere to the "forall-or-nothing" rule more
   strictly.

   Related function: RnTypes.rnImplicitBndrs

 * The -Wimplicit-kind-vars warning has been deprecated.

 * Kind variables are no longer implicitly quantified in constructor
   declarations:

     data T a        = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- no
 longer accepted
     data T (a :: k) = T1 (S (a :: k) | forall (b::k). T2 (S b)  -- still
 accepted

   Related function: RnTypes.extractRdrKindSigVars

 * Implicitly quantified kind variables are no longer put in front of
   other variables:

     f :: Proxy (a :: k) -> Proxy (b :: j)

     f :: forall k j (a :: k) (b :: j). Proxy a -> Proxy b   -- old order
     f :: forall k (a :: k) j (b :: j). Proxy a -> Proxy b   -- new order

   This is a breaking change for users of TypeApplications. Note that
   we still respect the dpendency order: 'k' before 'a', 'j' before 'b'.
   See "Ordering of specified variables" in the User's Guide.

   Related function: RnTypes.rnImplicitBndrs

 * In type synonyms and type family equations, free variables on the RHS
   are no longer implicitly quantified unless used in an outermost kind
   annotation:

     type T = Just (Nothing :: Maybe a)         -- no longer accepted
     type T = Just Nothing :: Maybe (Maybe a)   -- still accepted

   The latter form is a workaround due to temporary lack of an explicit
   quantification method. Ideally, we would write something along these
   lines:

     type T @a = Just (Nothing :: Maybe a)

   Related function: RnTypes.extractHsTyRdrTyVarsKindVars

 * Named wildcards in kinds are fixed (Trac #16334):

     x :: (Int :: _t)    -- this compiles, infers (_t ~ Type)

   Related function: RnTypes.partition_nwcs

 Implementation notes
 --------------------

 * One of the key changes is the removal of FKTV in RnTypes:

   - data FreeKiTyVars = FKTV { fktv_kis    :: [Located RdrName]
   -                          , fktv_tys    :: [Located RdrName] }
   + type FreeKiTyVars = [Located RdrName]

   We used to keep track of type and kind variables separately, but
   now that they are on equal footing when it comes to scoping, we
   can put them in the same list.

 * extract_lty and family are no longer parametrized by TypeOrKind,
   as we now do not distinguish kind variables from type variables.

 * PatSynExPE and the related Note [Pattern synonym existentials do not
 scope]
   have been removed (Trac #16315). With no implicit kind quantification,
   we can no longer trigger the error.

 * reportFloatingKvs and the related Note [Free-floating kind vars]
   have been removed. With no implicit kind quantification,
   we can no longer trigger the error.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16315#comment:13>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets