[GHC] #16315: Pattern synonym implicit existential quantification

[GHC]

#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