Pattern synonym implicit existential quantification

changed weight to 5

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. Here is the code that does it:

           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 --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?

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?

Yes, I wrote ticket:16315#comment:168624 in mind with the goal of rejecting the original program.

In case it wasn't clear:

Replying to [ticket:16315#comment:168624 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)

OK. Now I understand what you're doing better. Here is how I see it:

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.
But the renamer can't tell existential implicitly bound variables from universal ones.
So, the renamer brings into scope only the universals and all the implicitly bound ones. This brings more variables into scope than it should.
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.
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.
The program in this ticket observes that the difference in treatment between implicitly bound and explicitly bound is awkward.
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.
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. :)

Replying to [ticket:16315#comment:168706 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:

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 patch to implement the type-kind-variable merger.)

You have a red herring in your soup.

The following snippet is also accepted:

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.

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 ticket:16315#comment:168712.) If that's the case, then it sounds like the proper course of action is to:

Proceed with !361 (merged), as it will get rid of the awkwardness brought about by implicitly quantified variables being brought into scope.
Moreover, !361 (merged) can revert most of #14998 (closed):

* 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?

Does this sound right?

Yes, precisely.

closed

Trac metadata

Trac field	Value
Resolution	Unresolved → ResolvedFixed

changed milestone to %8.10.1

Trac metadata

Trac field	Value
Test case	- → patsyn/should_compile/T14498

mentioned in commit 5bc195b1

mentioned in issue #24 (closed)

mentioned in issue #16334 (closed)

added Pnormal label

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	RyanGlScott
Operating system
Architecture

Pattern synonym implicit existential quantification

Child items 0

Activity