[Git][ghc/ghc][wip/sand-witch/dib-instances] Type/data instances: require that variables on the RHS are mentioned on the LHS (#23512)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Wed Jun 14 08:41:11 UTC 2023
Andrei Borzenkov pushed to branch wip/sand-witch/dib-instances at Glasgow Haskell Compiler / GHC
Commits:
7cd6812b by Andrei Borzenkov at 2023-06-14T12:40:59+04:00
Type/data instances: require that variables on the RHS are mentioned on the LHS (#23512)
GHC Proposal #425 "Invisible binders in type declarations" restricts the
scope of type and data family instances as follows:
In type family and data family instances, require that every variable
mentioned on the RHS must also occur on the LHS.
For example, here are three equivalent type instance definitions accepted before this patch:
type family F1 a :: k
type instance F1 Int = Any :: j -> j
type family F2 a :: k
type instance F2 @(j -> j) Int = Any :: j -> j
type family F3 a :: k
type instance forall j. F3 Int = Any :: j -> j
- In F1, j is implicitly quantified and it occurs only on the RHS;
- In F2, j is implicitly quantified and it occurs both on the LHS and the RHS;
- In F3, j is explicitly quantified.
Now F1 is rejected with an out-of-scope error, while F2 and F3 continue to be accepted.
- - - - -
15 changed files:
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Rename/Module.hs
- docs/users_guide/9.8.1-notes.rst
- testsuite/tests/indexed-types/should_compile/T14131.hs
- testsuite/tests/indexed-types/should_compile/T15852.hs
- testsuite/tests/indexed-types/should_compile/T15852.stderr
- testsuite/tests/indexed-types/should_fail/T14230.hs
- testsuite/tests/indexed-types/should_fail/T7938.hs
- testsuite/tests/indexed-types/should_fail/T7938.stderr
- + testsuite/tests/rename/should_compile/T23512b.hs
- testsuite/tests/rename/should_compile/all.T
- + testsuite/tests/rename/should_fail/T23512a.hs
- + testsuite/tests/rename/should_fail/T23512a.stderr
- testsuite/tests/rename/should_fail/all.T
- testsuite/tests/typecheck/should_fail/T15797.hs
Changes:
=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -1799,8 +1799,7 @@ one exists:
a free variable 'a', which we implicitly quantify over. That is why we can
also use it to the left of the double colon: 'Left a
-The logic resides in extractHsTyRdrTyVarsKindVars. We use it both for type
-synonyms and type family instances.
+The logic resides in extractHsTyRdrTyVarsKindVars.
This is something of a stopgap solution until we can explicitly bind invisible
type/kind variables:
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -634,14 +634,10 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
rnFamEqn :: HsDocContext
-> AssocTyFamInfo
- -> FreeKiTyVars
- -- ^ Additional kind variables to implicitly bind if there is no
- -- explicit forall. (See the comments on @all_imp_vars@ below for a
- -- more detailed explanation.)
-> FamEqn GhcPs rhs
-> (HsDocContext -> rhs -> RnM (rhs', FreeVars))
-> RnM (FamEqn GhcRn rhs', FreeVars)
-rnFamEqn doc atfi extra_kvars
+rnFamEqn doc atfi
(FamEqn { feqn_tycon = tycon
, feqn_bndrs = outer_bndrs
, feqn_pats = pats
@@ -652,19 +648,8 @@ rnFamEqn doc atfi extra_kvars
-- all_imp_vars represent the implicitly bound type variables. This is
-- empty if we have an explicit `forall` (see
-- Note [forall-or-nothing rule] in GHC.Hs.Type), which means
- -- ignoring:
- --
- -- - pat_kity_vars, the free variables mentioned in the type patterns
- -- on the LHS of the equation, and
- -- - extra_kvars, which is one of the following:
- -- * For type family instances, extra_kvars are the free kind
- -- variables mentioned in an outermost kind signature on the RHS
- -- of the equation.
- -- (See Note [Implicit quantification in type synonyms] in
- -- GHC.Rename.HsType.)
- -- * For data family instances, extra_kvars are the free kind
- -- variables mentioned in the explicit return kind, if one is
- -- provided. (e.g., the `k` in `data instance T :: k -> Type`).
+ -- ignoring pat_kity_vars, the free variables mentioned in the type patterns
+ -- on the LHS of the equation
--
-- Some examples:
--
@@ -678,8 +663,6 @@ rnFamEqn doc atfi extra_kvars
-- type family G :: Maybe a
-- type instance forall a. G = (Nothing :: Maybe a)
-- -- all_imp_vars = []
- -- type instance G = (Nothing :: Maybe a)
- -- -- all_imp_vars = [a]
--
-- data family H :: k -> Type
-- data instance forall k. H :: k -> Type where ...
@@ -690,7 +673,7 @@ rnFamEqn doc atfi extra_kvars
--
-- For associated type family instances, exclude the type variables
-- bound by the instance head with filterInScopeM (#19649).
- ; all_imp_vars <- filterInScopeM $ pat_kity_vars ++ extra_kvars
+ ; all_imp_vars <- filterInScopeM $ pat_kity_vars
; bindHsOuterTyVarBndrs doc mb_cls all_imp_vars outer_bndrs $ \rn_outer_bndrs ->
do { (pats', pat_fvs) <- rnLHsTypeArgs (FamPatCtx tycon) pats
@@ -727,21 +710,12 @@ rnFamEqn doc atfi extra_kvars
-- associated family instance but not bound on the LHS, then reject
-- that type variable as being out of scope.
-- See Note [Renaming associated types].
- -- Per that Note, the LHS type variables consist of:
- --
- -- - The variables mentioned in the instance's type patterns
- -- (pat_fvs), and
- --
- -- - The variables mentioned in an outermost kind signature on the
- -- RHS. This is a subset of `rhs_fvs`. To compute it, we look up
- -- each RdrName in `extra_kvars` to find its corresponding Name in
- -- the LocalRdrEnv.
- ; extra_kvar_nms <- mapMaybeM (lookupLocalOccRn_maybe . unLoc) extra_kvars
- ; let lhs_bound_vars = pat_fvs `extendNameSetList` extra_kvar_nms
- improperly_scoped cls_tkv =
+ -- Per that Note, the LHS type variables consist of the variables
+ -- mentioned in the instance's type patterns (pat_fvs)
+ ; let improperly_scoped cls_tkv =
cls_tkv `elemNameSet` rhs_fvs
-- Mentioned on the RHS...
- && not (cls_tkv `elemNameSet` lhs_bound_vars)
+ && not (cls_tkv `elemNameSet` pat_fvs)
-- ...but not bound on the LHS.
bad_tvs = filter improperly_scoped inst_head_tvs
; unless (null bad_tvs) (addErr (TcRnBadAssocRhs bad_tvs))
@@ -786,7 +760,7 @@ rnFamEqn doc atfi extra_kvars
--
-- type instance F a b c = Either a b
-- ^^^^^
- lhs_loc = case map lhsTypeArgSrcSpan pats ++ map getLocA extra_kvars of
+ lhs_loc = case map lhsTypeArgSrcSpan pats of
[] -> panic "rnFamEqn.lhs_loc"
[loc] -> loc
(loc:locs) -> loc `combineSrcSpans` last locs
@@ -845,10 +819,9 @@ data ClosedTyFamInfo
rnTyFamInstEqn :: AssocTyFamInfo
-> TyFamInstEqn GhcPs
-> RnM (TyFamInstEqn GhcRn, FreeVars)
-rnTyFamInstEqn atfi eqn@(FamEqn { feqn_tycon = tycon, feqn_rhs = rhs })
- = rnFamEqn (TySynCtx tycon) atfi extra_kvs eqn rnTySyn
- where
- extra_kvs = extractHsTyRdrTyVarsKindVars rhs
+rnTyFamInstEqn atfi eqn@(FamEqn { feqn_tycon = tycon })
+ = rnFamEqn (TySynCtx tycon) atfi eqn rnTySyn
+
rnTyFamDefltDecl :: Name
-> TyFamDefltDecl GhcPs
@@ -859,11 +832,9 @@ rnDataFamInstDecl :: AssocTyFamInfo
-> DataFamInstDecl GhcPs
-> RnM (DataFamInstDecl GhcRn, FreeVars)
rnDataFamInstDecl atfi (DataFamInstDecl { dfid_eqn =
- eqn@(FamEqn { feqn_tycon = tycon
- , feqn_rhs = rhs })})
- = do { let extra_kvs = extractDataDefnKindVars rhs
- ; (eqn', fvs) <-
- rnFamEqn (TyDataCtx tycon) atfi extra_kvs eqn rnDataDefn
+ eqn@(FamEqn { feqn_tycon = tycon })})
+ = do { (eqn', fvs) <-
+ rnFamEqn (TyDataCtx tycon) atfi eqn rnDataDefn
; return (DataFamInstDecl { dfid_eqn = eqn' }, fvs) }
-- Renaming of the associated types in instances.
@@ -949,10 +920,7 @@ a class, we must check that all of the type variables mentioned on the RHS are
properly scoped. Specifically, the rule is this:
Every variable mentioned on the RHS of a type instance declaration
- (whether associated or not) must be either
- * Mentioned on the LHS, or
- * Mentioned in an outermost kind signature on the RHS
- (see Note [Implicit quantification in type synonyms])
+ (whether associated or not) must be mentioned on the LHS
Here is a simple example of something we should reject:
@@ -962,8 +930,7 @@ Here is a simple example of something we should reject:
type F Int x = z
Here, `z` is mentioned on the RHS of the associated instance without being
-mentioned on the LHS, nor is `z` mentioned in an outermost kind signature. The
-renamer will reject `z` as being out of scope without much fuss.
+mentioned on the LHS. The renamer will reject `z` as being out of scope without much fuss.
Things get slightly trickier when the instance header itself binds type
variables. Consider this example (adapted from #5515):
@@ -1055,10 +1022,8 @@ Some additional wrinkles:
Note that the `o` in the `Codomain 'KProxy` instance should be considered
improperly scoped. It does not meet the criteria for being explicitly
- quantified, as it is not mentioned by name on the LHS, nor does it meet the
- criteria for being implicitly quantified, as it is used in a RHS kind
- signature that is not outermost (see Note [Implicit quantification in type
- synonyms]). However, `o` /is/ bound by the instance header, so if this
+ quantified, as it is not mentioned by name on the LHS.
+ However, `o` /is/ bound by the instance header, so if this
program is not rejected by the renamer, the typechecker would treat it as
though you had written this:
@@ -1070,6 +1035,12 @@ Some additional wrinkles:
If the user really wants the latter, it is simple enough to communicate
their intent by mentioning `o` on the LHS by name.
+* Historical note: Previously we had to add type variables from the outermost
+ kind signature on the RHS to the scope of associated type family instance,
+ i.e. GHC did implicit quantification over them. But now that we implement
+ GHC Proposal #425 "Invisible binders in type declarations"
+ we don't need to do this anymore.
+
Note [Type family equations and occurrences]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In most data/type family equations, the type family name used in the equation
=====================================
docs/users_guide/9.8.1-notes.rst
=====================================
@@ -19,6 +19,22 @@ Language
This feature is guarded behind :extension:`TypeAbstractions`.
+- In accordance with GHC proposal `#425
+ <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0425-decl-invis-binders.rst>`_
+ GHC no longer implicitly quantifies over type variables that appear only in the RHS of type and
+ data family instances. This code will no longer work: ::
+
+ type family F1 a :: k
+ type instance F1 Int = Any :: j -> j
+
+ Instead you should write::
+
+ type instance F1 @(j -> j) Int = Any :: j -> j
+
+ Or::
+
+ type instance forall j . F1 Int = Any :: j -> j
+
Compiler
~~~~~~~~
=====================================
testsuite/tests/indexed-types/should_compile/T14131.hs
=====================================
@@ -9,21 +9,21 @@ import Data.Kind
import Data.Proxy
data family Nat :: k -> k -> Type
-newtype instance Nat :: (k -> Type) -> (k -> Type) -> Type where
+newtype instance Nat :: forall k . (k -> Type) -> (k -> Type) -> Type where
Nat :: (forall xx. f xx -> g xx) -> Nat f g
type family F :: Maybe a
-type instance F = (Nothing :: Maybe a)
+type instance F @a = (Nothing :: Maybe a)
class C k where
data CD :: k -> k -> Type
type CT :: k
instance C (Maybe a) where
- data CD :: Maybe a -> Maybe a -> Type where
+ data CD @(Maybe a) :: Maybe a -> Maybe a -> Type where
CD :: forall a (m :: Maybe a) (n :: Maybe a). Proxy m -> Proxy n -> CD m n
- type CT = (Nothing :: Maybe a)
+ type CT @(Maybe a) = (Nothing :: Maybe a)
class Z k where
type ZT :: Maybe k
- type ZT = (Nothing :: Maybe k)
+ type ZT @k = (Nothing :: Maybe k)
=====================================
testsuite/tests/indexed-types/should_compile/T15852.hs
=====================================
@@ -7,4 +7,4 @@ import Data.Kind
import Data.Proxy
data family DF a (b :: k)
-data instance DF (Proxy c) :: Proxy j -> Type
+data instance DF @(Proxy j) (Proxy c) :: Proxy j -> Type
=====================================
testsuite/tests/indexed-types/should_compile/T15852.stderr
=====================================
@@ -3,10 +3,10 @@ TYPE CONSTRUCTORS
roles nominal nominal nominal
COERCION AXIOMS
axiom T15852.D:R:DFProxyProxy0 ::
- forall k1 k2 (c :: k1) (j :: k2).
- DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 c j
+ forall k1 k2 (j :: k1) (c :: k2).
+ DF (Proxy c) = T15852.R:DFProxyProxy k1 k2 j c
FAMILY INSTANCES
- data instance forall {k1} {k2} {c :: k1} {j :: k2}.
+ data instance forall {k1} {k2} {j :: k1} {c :: k2}.
DF (Proxy c) -- Defined at T15852.hs:10:15
Dependent modules: []
-Dependent packages: [base-4.17.0.0]
+Dependent packages: [base-4.18.0.0]
=====================================
testsuite/tests/indexed-types/should_fail/T14230.hs
=====================================
@@ -8,4 +8,4 @@ class C k where
data CD :: k -> k -> *
instance C (Maybe a) where
- data CD :: (k -> *) -> (k -> *) -> *
+ data forall k . CD :: (k -> *) -> (k -> *) -> *
=====================================
testsuite/tests/indexed-types/should_fail/T7938.hs
=====================================
@@ -9,4 +9,4 @@ class Foo (a :: k1) (b :: k2) where
type Bar a
instance Foo (a :: k1) (b :: k2) where
- type Bar a = (KP :: KProxy k2)
+ type forall k2 . Bar a = (KP :: KProxy k2)
=====================================
testsuite/tests/indexed-types/should_fail/T7938.stderr
=====================================
@@ -1,5 +1,5 @@
-T7938.hs:12:17: error: [GHC-83865]
+T7938.hs:12:29: error: [GHC-83865]
• Expected a type, but ‘KP :: KProxy k2’ has kind ‘KProxy k2’
• In the type ‘(KP :: KProxy k2)’
In the type instance declaration for ‘Bar’
=====================================
testsuite/tests/rename/should_compile/T23512b.hs
=====================================
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies, TypeAbstractions #-}
+module T23512b where
+import GHC.Types
+
+type family F2 a :: k
+type instance F2 @(j -> j) Int = Any :: j -> j
+
+type family F3 a :: k
+type instance forall j. F3 Int = Any :: j -> j
=====================================
testsuite/tests/rename/should_compile/all.T
=====================================
@@ -212,3 +212,4 @@ test('T22122', [expect_broken(22122), extra_files(['T22122_aux.hs'])], multimod_
test('T23240', [req_th, extra_files(['T23240_aux.hs'])], multimod_compile, ['T23240', '-v0'])
test('T23318', normal, compile, ['-Wduplicate-exports'])
test('T23434', normal, compile, [''])
+test('T23512b', normal, compile, [''])
=====================================
testsuite/tests/rename/should_fail/T23512a.hs
=====================================
@@ -0,0 +1,9 @@
+{-# LANGUAGE TypeFamilies #-}
+module T23512a where
+import GHC.Types
+
+type family F1 a :: k
+type instance F1 Int = Any :: j -> j
+
+data family D :: k -> Type
+data instance D :: k -> Type
=====================================
testsuite/tests/rename/should_fail/T23512a.stderr
=====================================
@@ -0,0 +1,6 @@
+
+T23512a.hs:6:31: error: [GHC-76037] Not in scope: type variable ‘j’
+
+T23512a.hs:6:36: error: [GHC-76037] Not in scope: type variable ‘j’
+
+T23512a.hs:9:20: error: [GHC-76037] Not in scope: type variable ‘k’
=====================================
testsuite/tests/rename/should_fail/all.T
=====================================
@@ -198,3 +198,4 @@ test('RnUnexpectedStandaloneDeriving', normal, compile_fail, [''])
test('RnStupidThetaInGadt', normal, compile_fail, [''])
test('PackageImportsDisabled', normal, compile_fail, [''])
test('ImportLookupIllegal', normal, compile_fail, [''])
+test('T23512a', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_fail/T15797.hs
=====================================
@@ -13,7 +13,7 @@ import Data.Kind
class Ríki (obj :: Type) where
type Obj :: obj -> Constraint
- type Obj = Bæ @k :: k -> Constraint
+ type forall k . Obj = Bæ @k :: k -> Constraint
class Bæ (a :: k)
instance Bæ @k (a :: k)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7cd6812b3911d336bf8791ffdb5bc0ea98b2d7b7
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/7cd6812b3911d336bf8791ffdb5bc0ea98b2d7b7
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230614/db1c0836/attachment-0001.html>
More information about the ghc-commits
mailing list