diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index d03c9132b0ddb795432c1a3391eeaa07333dbbf1..103fae04d03cff859e68377d896c2aa8c09ea2b2 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/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 was a stopgap solution until we could explicitly bind invisible
type/kind variables:
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 19990ed862e75012eb33ba8c0d7b476a805d4950..d7a5fa483324100ade6e5c214b47b4237168b3e0 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/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
diff --git a/docs/users_guide/9.8.1-notes.rst b/docs/users_guide/9.8.1-notes.rst
index 7ccdec7d8211563735c57406ced612e3cbf474cc..1934540cda681f83005793359f5926c5055fa722 100644
--- a/docs/users_guide/9.8.1-notes.rst
+++ b/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
~~~~~~~~
diff --git a/testsuite/tests/indexed-types/should_compile/T14131.hs b/testsuite/tests/indexed-types/should_compile/T14131.hs
index d4965aa92f6e6067e66077264cf7e5081d19c774..14d4abf54eedc79fd7bcdd7a3dedc524506f9bac 100644
--- a/testsuite/tests/indexed-types/should_compile/T14131.hs
+++ b/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)
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.hs b/testsuite/tests/indexed-types/should_compile/T15852.hs
index 65c4ae68bc11288fd98930969180d18f2155eafe..132bf138654d19ef17d30fbd56e5146228a7744a 100644
--- a/testsuite/tests/indexed-types/should_compile/T15852.hs
+++ b/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
diff --git a/testsuite/tests/indexed-types/should_compile/T15852.stderr b/testsuite/tests/indexed-types/should_compile/T15852.stderr
index 41dba2100e587b465a4524459d2892415f6293ec..7e0d37c41ecd5febd6c5ac64936729beea490cfa 100644
--- a/testsuite/tests/indexed-types/should_compile/T15852.stderr
+++ b/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]
diff --git a/testsuite/tests/indexed-types/should_fail/T14230.hs b/testsuite/tests/indexed-types/should_fail/T14230.hs
index d409ba6806c75e413c506ec5d1350d7dbb3ada92..17658c9a6e72d01093c771c0bdccea50ace24686 100644
--- a/testsuite/tests/indexed-types/should_fail/T14230.hs
+++ b/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 -> *) -> *
diff --git a/testsuite/tests/indexed-types/should_fail/T7938.hs b/testsuite/tests/indexed-types/should_fail/T7938.hs
index 246015ddf7efad9673da5d0cec01cb6a4cd3d77e..6916e127a8013a22461e232927c67353066e6075 100644
--- a/testsuite/tests/indexed-types/should_fail/T7938.hs
+++ b/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)
diff --git a/testsuite/tests/indexed-types/should_fail/T7938.stderr b/testsuite/tests/indexed-types/should_fail/T7938.stderr
index 1b79fb8e7e90cbd82980b92ab4e9861a8bf57c81..65b08fb8fe3a0ca3ef613a2b4b693a2c5ad616e6 100644
--- a/testsuite/tests/indexed-types/should_fail/T7938.stderr
+++ b/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’
diff --git a/testsuite/tests/rename/should_compile/T23512b.hs b/testsuite/tests/rename/should_compile/T23512b.hs
new file mode 100644
index 0000000000000000000000000000000000000000..77628bf5c5a863303ec55a497d820e841b912f85
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/rename/should_compile/all.T b/testsuite/tests/rename/should_compile/all.T
index ce7da37cdff50b315f474413bd5cfb4e473898c0..ad9301b273a17aa37e753e359d857679bdff9973 100644
--- a/testsuite/tests/rename/should_compile/all.T
+++ b/testsuite/tests/rename/should_compile/all.T
@@ -213,3 +213,4 @@ test('T23240', [req_th, extra_files(['T23240_aux.hs'])], multimod_compile, ['T23
test('T23318', normal, compile, ['-Wduplicate-exports'])
test('T23434', normal, compile, [''])
test('T23510b', normal, compile, [''])
+test('T23512b', normal, compile, [''])
diff --git a/testsuite/tests/rename/should_fail/T23512a.hs b/testsuite/tests/rename/should_fail/T23512a.hs
new file mode 100644
index 0000000000000000000000000000000000000000..1f96dd6b228e59e06b150ec0618d887f0848db25
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/rename/should_fail/T23512a.stderr b/testsuite/tests/rename/should_fail/T23512a.stderr
new file mode 100644
index 0000000000000000000000000000000000000000..1a5497f835c72c94e0586e61e8258f55febe1991
--- /dev/null
+++ b/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’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 0f94d023ddadbedb7ae0c39e49c1b3102932e428..c67d1460916917097d0012704c54b7d11e5cde40 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -203,3 +203,4 @@ test('T23510a', normal, compile_fail, [''])
test('T16635a', normal, compile_fail, [''])
test('T16635b', normal, compile_fail, [''])
test('T16635c', normal, compile_fail, [''])
+test('T23512a', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T15797.hs b/testsuite/tests/typecheck/should_fail/T15797.hs
index 925674fecf0ee9ecc04669eb43e5b0cb2b1b8ff6..9d475534b353d0db0c7dddf64f89e74ca1200870 100644
--- a/testsuite/tests/typecheck/should_fail/T15797.hs
+++ b/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)