diff options
| -rw-r--r-- | compiler/rename/RnSource.hs | 81 | ||||
| -rw-r--r-- | compiler/rename/RnTypes.hs | 15 | ||||
| -rw-r--r-- | compiler/typecheck/TcHsType.hs | 42 | ||||
| -rw-r--r-- | compiler/typecheck/TcTyClsDecls.hs | 30 | ||||
| -rw-r--r-- | docs/users_guide/8.4.1-notes.rst | 18 | ||||
| -rw-r--r-- | docs/users_guide/glasgow_exts.rst | 72 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/T14131.hs | 29 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_compile/all.T | 1 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T5515.stderr | 8 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T7938.stderr | 8 | ||||
| -rw-r--r-- | testsuite/tests/parser/should_compile/DumpRenamedAst.hs | 9 | ||||
| -rw-r--r-- | testsuite/tests/parser/should_compile/DumpRenamedAst.stderr | 263 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T13985.hs | 27 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T13985.stderr | 39 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/T9574.stderr | 4 | ||||
| -rw-r--r-- | testsuite/tests/polykinds/all.T | 3 |
16 files changed, 542 insertions, 107 deletions
diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs index cb9c960dce..0e11ece40e 100644 --- a/compiler/rename/RnSource.hs +++ b/compiler/rename/RnSource.hs @@ -54,7 +54,7 @@ import Maybes ( orElse ) import FastString import SrcLoc import DynFlags -import Util ( debugIsOn, lengthExceeds, partitionWith ) +import Util ( debugIsOn, filterOut, lengthExceeds, partitionWith ) import HscTypes ( HscEnv, hsc_dflags ) import ListSetOps ( findDupsEq, removeDups, equivClasses ) import Digraph ( SCC, flattenSCC, flattenSCCs, Node(..) @@ -720,14 +720,15 @@ rnFamInstEqn :: HsDocContext -- Just (cls,tvs) => associated, -- and gives class and tyvars of the -- parent instance delc + -> [Located RdrName] -- Kind variables from the equation's RHS -> FamInstEqn GhcPs rhs -> (HsDocContext -> rhs -> RnM (rhs', FreeVars)) -> RnM (FamInstEqn GhcRn rhs', FreeVars) -rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon = tycon - , feqn_pats = pats - , feqn_fixity = fixity - , feqn_rhs = payload }}) - rnPayload +rnFamInstEqn doc mb_cls rhs_kvars + (HsIB { hsib_body = FamEqn { feqn_tycon = tycon + , feqn_pats = pats + , feqn_fixity = fixity + , feqn_rhs = payload }}) rn_payload = do { tycon' <- lookupFamInstName (fmap fst mb_cls) tycon ; let loc = case pats of [] -> pprPanic "rnFamInstEqn" (ppr tycon) @@ -735,18 +736,25 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon = tycon (L loc _ : ps) -> combineSrcSpans loc (getLoc (last ps)) ; pat_kity_vars_with_dups <- extractHsTysRdrTyVarsDups pats + ; let pat_vars = freeKiTyVarsAllVars $ + rmDupsInRdrTyVars pat_kity_vars_with_dups -- Use the "...Dups" form because it's needed -- below to report unsed binder on the LHS - ; var_names <- mapM (newTyVarNameRn mb_cls . L loc . unLoc) $ - freeKiTyVarsAllVars $ - rmDupsInRdrTyVars pat_kity_vars_with_dups + ; pat_var_names <- mapM (newTyVarNameRn mb_cls . L loc . unLoc) pat_vars + + -- Make sure to filter out the kind variables that were explicitly + -- bound in the type patterns. + ; let payload_vars = filterOut (`elemRdr` pat_vars) rhs_kvars + ; payload_var_names <- mapM (newTyVarNameRn mb_cls) payload_vars + + ; let all_var_names = pat_var_names ++ payload_var_names -- All the free vars of the family patterns -- with a sensible binding location ; ((pats', payload'), fvs) - <- bindLocalNamesFV var_names $ + <- bindLocalNamesFV all_var_names $ do { (pats', pat_fvs) <- rnLHsTypes (FamPatCtx tycon) pats - ; (payload', rhs_fvs) <- rnPayload doc payload + ; (payload', rhs_fvs) <- rn_payload doc payload -- Report unused binders on the LHS -- See Note [Unused type variables in family instances] @@ -766,13 +774,13 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon = tycon inst_tvs = case mb_cls of Nothing -> [] Just (_, inst_tvs) -> inst_tvs - ; warnUnusedTypePatterns var_names tv_nms_used + ; warnUnusedTypePatterns pat_var_names tv_nms_used -- See Note [Renaming associated types] ; let bad_tvs = case mb_cls of Nothing -> [] Just (_,cls_tkvs) -> filter is_bad cls_tkvs - var_name_set = mkNameSet var_names + var_name_set = mkNameSet all_var_names is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs && not (cls_tkv `elemNameSet` var_name_set) @@ -781,12 +789,13 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon = tycon ; return ((pats', payload'), rhs_fvs `plusFV` pat_fvs) } ; let anon_wcs = concatMap collectAnonWildCards pats' - all_ibs = anon_wcs ++ var_names + all_ibs = anon_wcs ++ all_var_names -- all_ibs: include anonymous wildcards in the implicit -- binders In a type pattern they behave just like any -- other type variable except for being anoymous. See -- Note [Wildcards in family instances] all_fvs = fvs `addOneFV` unLoc tycon' + -- type instance => use, hence addOneFV ; return (HsIB { hsib_vars = all_ibs , hsib_closed = True @@ -796,7 +805,6 @@ rnFamInstEqn doc mb_cls (HsIB { hsib_body = FamEqn { feqn_tycon = tycon , feqn_fixity = fixity , feqn_rhs = payload' } }, all_fvs) } - -- type instance => use, hence addOneFV rnTyFamInstDecl :: Maybe (Name, [Name]) -> TyFamInstDecl GhcPs @@ -808,8 +816,10 @@ rnTyFamInstDecl mb_cls (TyFamInstDecl { tfid_eqn = eqn }) rnTyFamInstEqn :: Maybe (Name, [Name]) -> TyFamInstEqn GhcPs -> RnM (TyFamInstEqn GhcRn, FreeVars) -rnTyFamInstEqn mb_cls eqn@(HsIB { hsib_body = FamEqn { feqn_tycon = tycon }}) - = rnFamInstEqn (TySynCtx tycon) mb_cls eqn rnTySyn +rnTyFamInstEqn mb_cls eqn@(HsIB { hsib_body = FamEqn { feqn_tycon = tycon + , feqn_rhs = rhs }}) + = do { rhs_kvs <- extractHsTyRdrTyVarsKindVars rhs + ; rnFamInstEqn (TySynCtx tycon) mb_cls rhs_kvs eqn rnTySyn } rnTyFamDefltEqn :: Name -> TyFamDefltEqn GhcPs @@ -818,13 +828,14 @@ rnTyFamDefltEqn cls (FamEqn { feqn_tycon = tycon , feqn_pats = tyvars , feqn_fixity = fixity , feqn_rhs = rhs }) - = bindHsQTyVars ctx Nothing (Just cls) [] tyvars $ \ tyvars' _ -> + = do { kvs <- extractHsTyRdrTyVarsKindVars rhs + ; bindHsQTyVars ctx Nothing (Just cls) kvs tyvars $ \ tyvars' _ -> do { tycon' <- lookupFamInstName (Just cls) tycon ; (rhs', fvs) <- rnLHsType ctx rhs ; return (FamEqn { feqn_tycon = tycon' , feqn_pats = tyvars' , feqn_fixity = fixity - , feqn_rhs = rhs' }, fvs) } + , feqn_rhs = rhs' }, fvs) } } where ctx = TyFamilyCtx tycon @@ -832,9 +843,11 @@ rnDataFamInstDecl :: Maybe (Name, [Name]) -> DataFamInstDecl GhcPs -> RnM (DataFamInstDecl GhcRn, FreeVars) rnDataFamInstDecl mb_cls (DataFamInstDecl { dfid_eqn = eqn@(HsIB { hsib_body = - FamEqn { feqn_tycon = tycon }})}) - = do { (eqn', fvs) <- - rnFamInstEqn (TyDataCtx tycon) mb_cls eqn rnDataDefn + FamEqn { feqn_tycon = tycon + , feqn_rhs = rhs }})}) + = do { rhs_kvs <- extractDataDefnKindVars rhs + ; (eqn', fvs) <- + rnFamInstEqn (TyDataCtx tycon) mb_cls rhs_kvs eqn rnDataDefn ; return (DataFamInstDecl { dfid_eqn = eqn' }, fvs) } -- Renaming of the associated types in instances. @@ -914,7 +927,7 @@ Relevant tickets: #3699, #10586, #10982 and #11451. Note [Renaming associated types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Check that the RHS of the decl mentions only type variables +Check that the RHS of the decl mentions only type variables that are explicitly bound on the LHS. For example, this is not ok class C a b where type F a x :: * @@ -922,13 +935,26 @@ bound on the LHS. For example, this is not ok type F (p,q) x = (x, r) -- BAD: mentions 'r' c.f. Trac #5515 -The same thing applies to kind variables, of course (Trac #7938, #9574): +Kind variables, on the other hand, are allowed to be implicitly or explicitly +bound. As examples, this (#9574) is acceptable: class Funct f where type Codomain f :: * instance Funct ('KProxy :: KProxy o) where + -- o is implicitly bound by the kind signature + -- of the LHS type pattern ('KProxy) type Codomain 'KProxy = NatTr (Proxy :: o -> *) -Here 'o' is mentioned on the RHS of the Codomain function, but -not on the LHS. +And this (#14131) is also acceptable: + data family Nat :: k -> k -> * + -- k is implicitly bound by an invisible kind pattern + newtype instance Nat :: (k -> *) -> (k -> *) -> * where + Nat :: (forall xx. f xx -> g xx) -> Nat f g +We could choose to disallow this, but then associated type families would not +be able to be as expressive as top-level type synonyms. For example, this type +synonym definition is allowed: + type T = (Nothing :: Maybe a) +So for parity with type synonyms, we also allow: + type family T :: Maybe a + type instance T = (Nothing :: Maybe a) All this applies only for *instance* declarations. In *class* declarations there is no RHS to worry about, and the class variables @@ -1643,7 +1669,7 @@ rnTyClDecl (FamDecl { tcdFam = decl }) rnTyClDecl (SynDecl { tcdLName = tycon, tcdTyVars = tyvars, tcdFixity = fixity, tcdRhs = rhs }) = do { tycon' <- lookupLocatedTopBndrRn tycon - ; kvs <- freeKiTyVarsKindVars <$> extractHsTyRdrTyVars rhs + ; kvs <- extractHsTyRdrTyVarsKindVars rhs ; let doc = TySynCtx tycon ; traceRn "rntycl-ty" (ppr tycon <+> ppr kvs) ; bindHsQTyVars doc Nothing Nothing kvs tyvars $ \ tyvars' _ -> @@ -1993,6 +2019,7 @@ are no data constructors we allow h98_style = True badAssocRhs :: [Name] -> RnM () badAssocRhs ns = addErr (hang (text "The RHS of an associated type declaration mentions" + <+> text "out-of-scope variable" <> plural ns <+> pprWithCommas (quotes . ppr) ns) 2 (text "All such variables must be bound on the LHS")) diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index 40b52399f1..a1174f65ca 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -26,10 +26,12 @@ module RnTypes ( bindLHsTyVarBndr, bindSigTyVarsFV, bindHsQTyVars, bindLRdrNames, extractFilteredRdrTyVars, extractFilteredRdrTyVarsDups, - extractHsTyRdrTyVars, extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars, + extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars, + extractHsTyRdrTyVarsDups, extractHsTysRdrTyVars, extractHsTysRdrTyVarsDups, rmDupsInRdrTyVars, extractRdrKindSigVars, extractDataDefnKindVars, - freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars + freeKiTyVarsAllVars, freeKiTyVarsKindVars, freeKiTyVarsTypeVars, + elemRdr ) where import {-# SOURCE #-} RnSplice( rnSpliceType ) @@ -1661,6 +1663,15 @@ extractHsTyRdrTyVarsDups :: LHsType GhcPs -> RnM FreeKiTyVarsWithDups extractHsTyRdrTyVarsDups ty = extract_lty TypeLevel ty emptyFKTV +-- | Extracts the free kind variables (but not the type variables) of an +-- 'HsType'. Does not return any wildcards. +-- When the same name occurs multiple times in the type, only the first +-- occurrence is returned. +-- See Note [Kind and type-variable binders] +extractHsTyRdrTyVarsKindVars :: LHsType GhcPs -> RnM [Located RdrName] +extractHsTyRdrTyVarsKindVars ty + = freeKiTyVarsKindVars <$> extractHsTyRdrTyVars ty + -- | Extracts free type and kind variables from types in a list. -- When the same name occurs multiple times in the types, only the first -- occurrence is returned and the rest is filtered out. diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index dab708c290..bd73bf3884 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -38,6 +38,8 @@ module TcHsType ( kindGeneralize, checkExpectedKindX, instantiateTyUntilN, + reportFloatingKvs, + -- Sort-checking kinds tcLHsKindSig, @@ -1744,6 +1746,46 @@ CUSK: When we determine the tycon's final, never-to-be-changed kind in kcHsTyVarBndrs, we check to make sure all implicitly-bound kind vars are indeed mentioned in a kind somewhere. If not, error. +We also perform free-floating kind var analysis for type family instances +(see #13985). Here is an interesting example: + + type family T :: k + type instance T = (Nothing :: Maybe a) + +Upon a cursory glance, it may appear that the kind variable `a` is +free-floating above, since there are no (visible) LHS patterns in `T`. However, +there is an *invisible* pattern due to the return kind, so inside of GHC, the +instance looks closer to this: + + type family T @k :: k + type instance T @(Maybe a) = (Nothing :: Maybe a) + +Here, we can see that `a` really is bound by a LHS type pattern, so `a` is in +fact not free-floating. Contrast that with this example: + + type instance T = Proxy (Nothing :: Maybe a) + +This would looks like this inside of GHC: + + type instance T @(*) = Proxy (Nothing :: Maybe a) + +So this time, `a` is neither bound by a visible nor invisible type pattern on +the LHS, so it would be reported as free-floating. + +Finally, here's one more brain-teaser (from #9574). In the example below: + + class Funct f where + type Codomain f :: * + instance Funct ('KProxy :: KProxy o) where + type Codomain 'KProxy = NatTr (Proxy :: o -> *) + +As it turns out, `o` is not free-floating in this example. That is because `o` +bound by the kind signature of the LHS type pattern 'KProxy. To make this more +obvious, one can also write the instance like so: + + instance Funct ('KProxy :: KProxy o) where + type Codomain ('KProxy :: KProxy o) = NatTr (Proxy :: o -> *) + -} -------------------- diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index f445d83608..44492c08d9 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -1380,7 +1380,9 @@ tc_fam_ty_pats :: FamTyConShape -> [Name] -- Bound kind/type variable names -> HsTyPats GhcRn -- Type patterns -> (TcKind -> TcM r) -- Kind checker for RHS - -> TcM ([Type], r) -- Returns the type-checked patterns + -> TcM ( [TcTyVar] -- Returns the type-checked patterns, + , [TcType] -- the type variables that scope over + , r ) -- them, and the thing inside -- Check the type patterns of a type or data family instance -- type instance F <pat1> <pat2> = <type> -- The 'tyvars' are the free type variables of pats @@ -1413,7 +1415,7 @@ tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity -- Kind-check and quantify -- See Note [Quantifying over family patterns] - ; (_, result) <- tcImplicitTKBndrs tv_names $ + ; (arg_tvs, (args, stuff)) <- tcImplicitTKBndrs tv_names $ do { let loc = nameSrcSpan name lhs_fun = L loc (HsTyVar NotPromoted (L loc name)) bogus_fun_ty = pprPanic "tc_fam_ty_pats" (ppr name $$ ppr arg_pats) @@ -1428,7 +1430,7 @@ tc_fam_ty_pats (FamTyConShape { fs_name = name, fs_arity = arity ; return ((args, stuff), emptyVarSet) } - ; return result } + ; return (arg_tvs, args, stuff) } -- See Note [tc_fam_ty_pats vs tcFamTyPats] tcFamTyPats :: FamTyConShape @@ -1443,9 +1445,9 @@ tcFamTyPats :: FamTyConShape -> TcKind -> TcM a) -- NB: You can use solveEqualities here. -> TcM a -tcFamTyPats fam_shape@(FamTyConShape { fs_name = name }) mb_clsinfo - tv_names arg_pats kind_checker thing_inside - = do { (typats, (more_typats, res_kind)) +tcFamTyPats fam_shape@(FamTyConShape { fs_name = name, fs_flavor = fam_flav }) + mb_clsinfo tv_names arg_pats kind_checker thing_inside + = do { (fam_used_tvs, typats, (more_typats, res_kind)) <- solveEqualities $ -- See Note [Constraints in patterns] tc_fam_ty_pats fam_shape mb_clsinfo tv_names arg_pats kind_checker @@ -1481,7 +1483,21 @@ tcFamTyPats fam_shape@(FamTyConShape { fs_name = name }) mb_clsinfo -- bit is cleverer. ; traceTc "tcFamTyPats" (ppr name $$ ppr all_pats $$ ppr qtkvs) - -- Don't print out too much, as we might be in the knot + -- Don't print out too much, as we might be in the knot + + -- See Note [Free-floating kind vars] in TcHsType + ; let tc_flav = case fam_flav of + TypeFam -> OpenTypeFamilyFlavour + DataFam -> DataFamilyFlavour + all_mentioned_tvs = mkVarSet qtkvs + -- qtkvs has all the tyvars bound by LHS + -- type patterns + unmentioned_tvs = filterOut (`elemVarSet` all_mentioned_tvs) + fam_used_tvs + -- If there are tyvars left over, we can + -- assume they're free-floating, since they + -- aren't bound by a type pattern + ; checkNoErrs $ reportFloatingKvs name tc_flav qtkvs unmentioned_tvs ; tcExtendTyVarEnv qtkvs $ -- Extend envt with TcTyVars not TyVars, because the diff --git a/docs/users_guide/8.4.1-notes.rst b/docs/users_guide/8.4.1-notes.rst index 96fbdd4886..db573202e2 100644 --- a/docs/users_guide/8.4.1-notes.rst +++ b/docs/users_guide/8.4.1-notes.rst @@ -27,6 +27,24 @@ Language wish to; this is quite like how regular datatypes with a kind signature can omit some type variables. +- There are now fewer restrictions regarding whether kind variables can appear + on the right-hand sides of type and data family instances. Before, there was + a strict requirements that all kind variables on the RHS had to be explicitly + bound by type patterns on the LHS. Now, kind variables can be *implicitly* + bound, which allows constructions like these: :: + + data family Nat :: k -> k -> * + -- k is implicitly bound by an invisible kind pattern + newtype instance Nat :: (k -> *) -> (k -> *) -> * where + Nat :: (forall xx. f xx -> g xx) -> Nat f g + + class Funct f where + type Codomain f :: * + instance Funct ('KProxy :: KProxy o) where + -- o is implicitly bound by the kind signature + -- of the LHS type pattern ('KProxy) + type Codomain 'KProxy = NatTr (Proxy :: o -> *) + - Implicitly bidirectional pattern synonyms no longer allow bang patterns (``!``) or irrefutable patterns (``~``) on the right-hand side. Previously, this was allowed, although the bang patterns and irrefutable patterns would diff --git a/docs/users_guide/glasgow_exts.rst b/docs/users_guide/glasgow_exts.rst index bd11360acc..65f8629ccf 100644 --- a/docs/users_guide/glasgow_exts.rst +++ b/docs/users_guide/glasgow_exts.rst @@ -7659,8 +7659,23 @@ Note the following points: instance declarations of the class in which the family was declared, just as with the equations of the methods of a class. -- The variables on the right hand side of the type family equation - must, as usual, be bound on the left hand side. +- The type variables on the right hand side of the type family equation + must, as usual, be explicitly bound by the left hand side. This restriction + is relaxed for *kind* variables, however, as the right hand side is allowed + to mention kind variables that are implicitly bound. For example, these are + legitimate: :: + + data family Nat :: k -> k -> * + -- k is implicitly bound by an invisible kind pattern + newtype instance Nat :: (k -> *) -> (k -> *) -> * where + Nat :: (forall xx. f xx -> g xx) -> Nat f g + + class Funct f where + type Codomain f :: * + instance Funct ('KProxy :: KProxy o) where + -- o is implicitly bound by the kind signature + -- of the LHS type pattern ('KProxy) + type Codomain 'KProxy = NatTr (Proxy :: o -> *) - The instance for an associated type can be omitted in class instances. In that case, unless there is a default instance (see @@ -7715,15 +7730,18 @@ Note the following points: - The default declaration must mention only type *variables* on the left hand side, and the right hand side must mention only type - variables bound on the left hand side. However, unlike the associated - type family declaration itself, the type variables of the default - instance are independent of those of the parent class. + variables that are explicitly bound on the left hand side. This restriction + is relaxed for *kind* variables, however, as the right hand side is allowed + to mention kind variables that are implicitly bound on the left hand side. + +- Unlike the associated type family declaration itself, the type variables of + the default instance are independent of those of the parent class. Here are some examples: :: - class C a where + class C (a :: *) where type F1 a :: * type instance F1 a = [a] -- OK type instance F1 a = a->a -- BAD; only one default instance is allowed @@ -7738,6 +7756,21 @@ Here are some examples: type F4 a type F4 b = a -- BAD; 'a' is not in scope in the RHS + type F5 a :: [k] + type F5 a = ('[] :: [x]) -- OK; the kind variable x is implicitly + bound by an invisible kind pattern + on the LHS + + type F6 a + type F6 a = + Proxy ('[] :: [x]) -- BAD; the kind variable x is not bound, + even by an invisible kind pattern + + type F7 (x :: a) :: [a] + type F7 x = ('[] :: [a]) -- OK; the kind variable a is implicitly + bound by the kind signature of the + LHS type pattern + .. _scoping-class-params: Scoping of class parameters @@ -7760,6 +7793,33 @@ Here, the right-hand side of the data instance mentions the type variable ``d`` that does not occur in its left-hand side. We cannot admit such data instances as they would compromise type safety. +Bear in mind that it is also possible for the *right*-hand side of an +associated family instance to contain *kind* parameters (by using the +:ghc-flag:`-XPolyKinds` extension). For instance, this class and instance are +perfectly admissible: :: + + class C k where + type T :: k + + instance C (Maybe a) where + type T = (Nothing :: Maybe a) + +Here, although the right-hand side ``(Nothing :: Maybe a)`` mentions a kind +variable ``a`` which does not occur on the left-hand side, this is acceptable, +because ``a`` is *implicitly* bound by ``T``'s kind pattern. + +A kind variable can also be bound implicitly in a LHS type pattern, as in this +example: :: + + class C a where + type T (x :: a) :: [a] + + instance C (Maybe a) where + type T x = ('[] :: [Maybe a]) + +In ``('[] :: [Maybe a])``, the kind variable ``a`` is implicitly bound by the +kind signature of the LHS type pattern ``x``. + Instance contexts and associated type and data instances ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/testsuite/tests/indexed-types/should_compile/T14131.hs b/testsuite/tests/indexed-types/should_compile/T14131.hs new file mode 100644 index 0000000000..e8b15790a1 --- /dev/null +++ b/testsuite/tests/indexed-types/should_compile/T14131.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +module T14131 where + +import Data.Kind +import Data.Proxy + +data family Nat :: k -> k -> * +newtype instance Nat :: (k -> *) -> (k -> *) -> * where + Nat :: (forall xx. f xx -> g xx) -> Nat f g + +type family F :: Maybe a +type instance F = (Nothing :: Maybe a) + +class C k where + data CD :: k -> k -> * + type CT :: k + +instance C (Maybe a) where + data CD :: Maybe a -> Maybe a -> * where + CD :: forall (m :: Maybe a) (n :: Maybe a). Proxy m -> Proxy n -> CD m n + type CT = (Nothing :: Maybe a) + +class Z k where + type ZT :: Maybe k + type ZT = (Nothing :: Maybe k) diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T index dc166dc470..ad80b0cec2 100644 --- a/testsuite/tests/indexed-types/should_compile/all.T +++ b/testsuite/tests/indexed-types/should_compile/all.T @@ -267,3 +267,4 @@ test('T13662', normal, compile, ['']) test('T13705', normal, compile, ['']) test('T12369', normal, compile, ['']) test('T14045', normal, compile, ['']) +test('T14131', normal, compile, ['']) diff --git a/testsuite/tests/indexed-types/should_fail/T5515.stderr b/testsuite/tests/indexed-types/should_fail/T5515.stderr index 25fbe9f0f0..688eef697e 100644 --- a/testsuite/tests/indexed-types/should_fail/T5515.stderr +++ b/testsuite/tests/indexed-types/should_fail/T5515.stderr @@ -1,8 +1,8 @@ -T5515.hs:9:3: - The RHS of an associated type declaration mentions ‘a’ +T5515.hs:9:3: error: + The RHS of an associated type declaration mentions out-of-scope variable ‘a’ All such variables must be bound on the LHS -T5515.hs:15:3: - The RHS of an associated type declaration mentions ‘a’ +T5515.hs:15:3: error: + The RHS of an associated type declaration mentions out-of-scope variable ‘a’ All such variables must be bound on the LHS diff --git a/testsuite/tests/indexed-types/should_fail/T7938.stderr b/testsuite/tests/indexed-types/should_fail/T7938.stderr index a9b5aef499..2816e2f9f8 100644 --- a/testsuite/tests/indexed-types/should_fail/T7938.stderr +++ b/testsuite/tests/indexed-types/should_fail/T7938.stderr @@ -1,4 +1,6 @@ -T7938.hs:12:3: - The RHS of an associated type declaration mentions ‘k2’ - All such variables must be bound on the LHS +T7938.hs:12:16: error: + • Expected a type, but ‘(KP :: KProxy k2)’ has kind ‘KProxy k2’ + • In the type ‘(KP :: KProxy k2)’ + In the type instance declaration for ‘Bar’ + In the instance declaration for ‘Foo (a :: k1) (b :: k2)’ diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs index cb23ad5085..493b736df5 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.hs +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.hs @@ -1,4 +1,5 @@ -{-# LANGUAGE DataKinds, PolyKinds, TypeOperators, TypeFamilies #-} +{-# LANGUAGE DataKinds, GADTs, PolyKinds, RankNTypes, TypeOperators, + TypeFamilies #-} module DumpRenamedAst where @@ -8,4 +9,10 @@ type family Length (as :: [k]) :: Peano where Length (a : as) = Succ (Length as) Length '[] = Zero +data family Nat :: k -> k -> * +-- Ensure that the `k` in the type pattern and `k` in the kind signature have +-- the same binding site. +newtype instance Nat (a :: k -> *) :: (k -> *) -> * where + Nat :: (forall xx. f xx -> g xx) -> Nat f g + main = putStrLn "hello" diff --git a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr index 6ea6e8f2e0..60862cc110 100644 --- a/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr +++ b/testsuite/tests/parser/should_compile/DumpRenamedAst.stderr @@ -6,32 +6,32 @@ [((,) (NonRecursive) {Bag(Located (HsBind Name)): - [({ DumpRenamedAst.hs:11:1-23 } + [({ DumpRenamedAst.hs:18:1-23 } (FunBind - ({ DumpRenamedAst.hs:11:1-4 } + ({ DumpRenamedAst.hs:18:1-4 } {Name: DumpRenamedAst.main}) (MG - ({ DumpRenamedAst.hs:11:1-23 } - [({ DumpRenamedAst.hs:11:1-23 } + ({ DumpRenamedAst.hs:18:1-23 } + [({ DumpRenamedAst.hs:18:1-23 } (Match (FunRhs - ({ DumpRenamedAst.hs:11:1-4 } + ({ DumpRenamedAst.hs:18:1-4 } {Name: DumpRenamedAst.main}) (Prefix) (NoSrcStrict)) [] (Nothing) (GRHSs - [({ DumpRenamedAst.hs:11:6-23 } + [({ DumpRenamedAst.hs:18:6-23 } (GRHS [] - ({ DumpRenamedAst.hs:11:8-23 } + ({ DumpRenamedAst.hs:18:8-23 } (HsApp - ({ DumpRenamedAst.hs:11:8-15 } + ({ DumpRenamedAst.hs:18:8-15 } (HsVar - ({ DumpRenamedAst.hs:11:8-15 } + ({ DumpRenamedAst.hs:18:8-15 } {Name: putStrLn}))) - ({ DumpRenamedAst.hs:11:17-23 } + ({ DumpRenamedAst.hs:18:17-23 } (HsLit (HsString (SourceText @@ -49,9 +49,9 @@ []) [] [(TyClGroup - [({ DumpRenamedAst.hs:5:1-30 } + [({ DumpRenamedAst.hs:6:1-30 } (DataDecl - ({ DumpRenamedAst.hs:5:6-10 } + ({ DumpRenamedAst.hs:6:6-10 } {Name: DumpRenamedAst.Peano}) (HsQTvs [] @@ -65,9 +65,9 @@ []) (Nothing) (Nothing) - [({ DumpRenamedAst.hs:5:14-17 } + [({ DumpRenamedAst.hs:6:14-17 } (ConDeclH98 - ({ DumpRenamedAst.hs:5:14-17 } + ({ DumpRenamedAst.hs:6:14-17 } {Name: DumpRenamedAst.Zero}) (Nothing) (Just @@ -76,19 +76,19 @@ (PrefixCon []) (Nothing))) - ,({ DumpRenamedAst.hs:5:21-30 } + ,({ DumpRenamedAst.hs:6:21-30 } (ConDeclH98 - ({ DumpRenamedAst.hs:5:21-24 } + ({ DumpRenamedAst.hs:6:21-24 } {Name: DumpRenamedAst.Succ}) (Nothing) (Just ({ <no location info> } [])) (PrefixCon - [({ DumpRenamedAst.hs:5:26-30 } + [({ DumpRenamedAst.hs:6:26-30 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:5:26-30 } + ({ DumpRenamedAst.hs:6:26-30 } {Name: DumpRenamedAst.Peano})))]) (Nothing)))] ({ <no location info> } @@ -99,103 +99,262 @@ [] []) ,(TyClGroup - [({ DumpRenamedAst.hs:7:1-39 } + [({ DumpRenamedAst.hs:8:1-39 } (FamDecl (FamilyDecl (ClosedTypeFamily (Just - [({ DumpRenamedAst.hs:8:3-36 } + [({ DumpRenamedAst.hs:9:3-36 } (HsIB [{Name: a} ,{Name: as}] (FamEqn - ({ DumpRenamedAst.hs:8:3-8 } + ({ DumpRenamedAst.hs:9:3-8 } {Name: DumpRenamedAst.Length}) - [({ DumpRenamedAst.hs:8:10-17 } + [({ DumpRenamedAst.hs:9:10-17 } (HsParTy - ({ DumpRenamedAst.hs:8:11-16 } + ({ DumpRenamedAst.hs:9:11-16 } (HsOpTy - ({ DumpRenamedAst.hs:8:11 } + ({ DumpRenamedAst.hs:9:11 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:8:11 } + ({ DumpRenamedAst.hs:9:11 } {Name: a}))) - ({ DumpRenamedAst.hs:8:13 } + ({ DumpRenamedAst.hs:9:13 } {Name: :}) - ({ DumpRenamedAst.hs:8:15-16 } + ({ DumpRenamedAst.hs:9:15-16 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:8:15-16 } + ({ DumpRenamedAst.hs:9:15-16 } {Name: as})))))))] (Prefix) - ({ DumpRenamedAst.hs:8:21-36 } + ({ DumpRenamedAst.hs:9:21-36 } (HsAppTy - ({ DumpRenamedAst.hs:8:21-24 } + ({ DumpRenamedAst.hs:9:21-24 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:8:21-24 } + ({ DumpRenamedAst.hs:9:21-24 } {Name: DumpRenamedAst.Succ}))) - ({ DumpRenamedAst.hs:8:26-36 } + ({ DumpRenamedAst.hs:9:26-36 } (HsParTy - ({ DumpRenamedAst.hs:8:27-35 } + ({ DumpRenamedAst.hs:9:27-35 } (HsAppTy - ({ DumpRenamedAst.hs:8:27-32 } + ({ DumpRenamedAst.hs:9:27-32 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:8:27-32 } + ({ DumpRenamedAst.hs:9:27-32 } {Name: DumpRenamedAst.Length}))) - ({ DumpRenamedAst.hs:8:34-35 } + ({ DumpRenamedAst.hs:9:34-35 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:8:34-35 } + ({ DumpRenamedAst.hs:9:34-35 } {Name: as})))))))))) (True))) - ,({ DumpRenamedAst.hs:9:3-24 } + ,({ DumpRenamedAst.hs:10:3-24 } (HsIB [] (FamEqn - ({ DumpRenamedAst.hs:9:3-8 } + ({ DumpRenamedAst.hs:10:3-8 } {Name: DumpRenamedAst.Length}) - [({ DumpRenamedAst.hs:9:10-12 } + [({ DumpRenamedAst.hs:10:10-12 } (HsExplicitListTy (Promoted) (PlaceHolder) []))] (Prefix) - ({ DumpRenamedAst.hs:9:21-24 } + ({ DumpRenamedAst.hs:10:21-24 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:9:21-24 } + ({ DumpRenamedAst.hs:10:21-24 } {Name: DumpRenamedAst.Zero})))) (True)))])) - ({ DumpRenamedAst.hs:7:13-18 } + ({ DumpRenamedAst.hs:8:13-18 } {Name: DumpRenamedAst.Length}) (HsQTvs [{Name: k}] - [({ DumpRenamedAst.hs:7:20-30 } + [({ DumpRenamedAst.hs:8:20-30 } (KindedTyVar - ({ DumpRenamedAst.hs:7:21-22 } + ({ DumpRenamedAst.hs:8:21-22 } {Name: as}) - ({ DumpRenamedAst.hs:7:27-29 } + ({ DumpRenamedAst.hs:8:27-29 } (HsListTy - ({ DumpRenamedAst.hs:7:28 } + ({ DumpRenamedAst.hs:8:28 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:7:28 } + ({ DumpRenamedAst.hs:8:28 } {Name: k})))))))] {NameSet: []}) (Prefix) - ({ DumpRenamedAst.hs:7:32-39 } + ({ DumpRenamedAst.hs:8:32-39 } (KindSig - ({ DumpRenamedAst.hs:7:35-39 } + ({ DumpRenamedAst.hs:8:35-39 } (HsTyVar (NotPromoted) - ({ DumpRenamedAst.hs:7:35-39 } + ({ DumpRenamedAst.hs:8:35-39 } {Name: DumpRenamedAst.Peano}))))) (Nothing))))] [] - [])] + []) + ,(TyClGroup + [({ DumpRenamedAst.hs:12:1-30 } + (FamDecl + (FamilyDecl + (DataFamily) + ({ DumpRenamedAst.hs:12:13-15 } + {Name: DumpRenamedAst.Nat}) + (HsQTvs + [{Name: k}] + [] + {NameSet: + []}) + (Prefix) + ({ DumpRenamedAst.hs:12:17-30 } + (KindSig + ({ DumpRenamedAst.hs:12:20-30 } + (HsFunTy + ({ DumpRenamedAst.hs:12:20 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:12:20 } + {Name: k}))) + ({ DumpRenamedAst.hs:12:25-30 } + (HsFunTy + ({ DumpRenamedAst.hs:12:25 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:12:25 } + {Name: k}))) + ({ DumpRenamedAst.hs:12:30 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:12:30 } + {Name: *}))))))))) + (Nothing))))] + [] + [({ DumpRenamedAst.hs:(15,1)-(16,45) } + (DataFamInstD + (DataFamInstDecl + (HsIB + [{Name: k} + ,{Name: a}] + (FamEqn + ({ DumpRenamedAst.hs:15:18-20 } + {Name: DumpRenamedAst.Nat}) + [({ DumpRenamedAst.hs:15:22-34 } + (HsKindSig + ({ DumpRenamedAst.hs:15:23 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:15:23 } + {Name: a}))) + ({ DumpRenamedAst.hs:15:28-33 } + (HsFunTy + ({ DumpRenamedAst.hs:15:28 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:15:28 } + {Name: k}))) + ({ DumpRenamedAst.hs:15:33 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:15:33 } + {Name: *})))))))] + (Prefix) + (HsDataDefn + (NewType) + ({ <no location info> } + []) + (Nothing) + (Just + ({ DumpRenamedAst.hs:15:39-51 } + (HsFunTy + ({ DumpRenamedAst.hs:15:39-46 } + (HsParTy + ({ DumpRenamedAst.hs:15:40-45 } + (HsFunTy + ({ DumpRenamedAst.hs:15:40 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:15:40 } + {Name: k}))) + ({ DumpRenamedAst.hs:15:45 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:15:45 } + {Name: *}))))))) + ({ DumpRenamedAst.hs:15:51 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:15:51 } + {Name: *})))))) + [({ DumpRenamedAst.hs:16:3-45 } + (ConDeclGADT + [({ DumpRenamedAst.hs:16:3-5 } + {Name: DumpRenamedAst.Nat})] + (HsIB + [{Name: f} + ,{Name: g}] + ({ DumpRenamedAst.hs:16:10-45 } + (HsFunTy + ({ DumpRenamedAst.hs:16:10-34 } + (HsParTy + ({ DumpRenamedAst.hs:16:11-33 } + (HsForAllTy + [({ DumpRenamedAst.hs:16:18-19 } + (UserTyVar + ({ DumpRenamedAst.hs:16:18-19 } + {Name: xx})))] + ({ DumpRenamedAst.hs:16:22-33 } + (HsFunTy + ({ DumpRenamedAst.hs:16:22-25 } + (HsAppTy + ({ DumpRenamedAst.hs:16:22 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:16:22 } + {Name: f}))) + ({ DumpRenamedAst.hs:16:24-25 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:16:24-25 } + {Name: xx}))))) + ({ DumpRenamedAst.hs:16:30-33 } + (HsAppTy + ({ DumpRenamedAst.hs:16:30 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:16:30 } + {Name: g}))) + ({ DumpRenamedAst.hs:16:32-33 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:16:32-33 } + {Name: xx}))))))))))) + ({ DumpRenamedAst.hs:16:39-45 } + (HsAppTy + ({ DumpRenamedAst.hs:16:39-43 } + (HsAppTy + ({ DumpRenamedAst.hs:16:39-41 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:16:39-41 } + {Name: DumpRenamedAst.Nat}))) + ({ DumpRenamedAst.hs:16:43 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:16:43 } + {Name: f}))))) + ({ DumpRenamedAst.hs:16:45 } + (HsTyVar + (NotPromoted) + ({ DumpRenamedAst.hs:16:45 } + {Name: g}))))))) + (True)) + (Nothing)))] + ({ <no location info> } + []))) + (True)))))])] [] [] [] diff --git a/testsuite/tests/polykinds/T13985.hs b/testsuite/tests/polykinds/T13985.hs new file mode 100644 index 0000000000..c0555d8f69 --- /dev/null +++ b/testsuite/tests/polykinds/T13985.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeFamilies #-} +module T13985 where + +import Data.Kind +import Data.Proxy + +data family Fam +data instance Fam = MkFam (forall (a :: k). Proxy a) + +type family T +type instance T = Proxy (Nothing :: Maybe a) + +class C k where + data CD :: k + type CT :: k + +instance C Type where + data CD = forall (a :: k). CD (Proxy a) + type CT = Proxy (Nothing :: Maybe a) + +class Z a where + type ZT a + type ZT a = Proxy (Nothing :: Maybe x) diff --git a/testsuite/tests/polykinds/T13985.stderr b/testsuite/tests/polykinds/T13985.stderr new file mode 100644 index 0000000000..954dae5dcd --- /dev/null +++ b/testsuite/tests/polykinds/T13985.stderr @@ -0,0 +1,39 @@ + +T13985.hs:12:1: error: + • Kind variable ‘k’ is implicitly bound in data family + ‘Fam’, but does not appear as the kind of any + of its type variables. Perhaps you meant + to bind it (with TypeInType) explicitly somewhere? + • In the data instance declaration for ‘Fam’ + +T13985.hs:15:15: error: + • Kind variable ‘a’ is implicitly bound in type family + ‘T’, but does not appear as the kind of any + of its type variables. Perhaps you meant + to bind it (with TypeInType) explicitly somewhere? + • In the type instance declaration for ‘T’ + +T13985.hs:22:3: error: + • Kind variable ‘k’ is implicitly bound in data family + ‘CD’, but does not appear as the kind of any + of its type variables. Perhaps you meant + to bind it (with TypeInType) explicitly somewhere? + • In the data instance declaration for ‘CD’ + In the instance declaration for ‘C Type’ + +T13985.hs:23:8: error: + • Kind variable ‘a’ is implicitly bound in type family + ‘CT’, but does not appear as the kind of any + of its type variables. Perhaps you meant + to bind it (with TypeInType) explicitly somewhere? + • In the type instance declaration for ‘CT’ + In the instance declaration for ‘C Type’ + +T13985.hs:27:3: error: + • Kind variable ‘x’ is implicitly bound in type family + ‘ZT’, but does not appear as the kind of any + of its type variables. Perhaps you meant + to bind it (with TypeInType) explicitly somewhere? + Type variables with inferred kinds: (k :: *) (a :: k) + • In the default type instance declaration for ‘ZT’ + In the class declaration for ‘Z’ diff --git a/testsuite/tests/polykinds/T9574.stderr b/testsuite/tests/polykinds/T9574.stderr deleted file mode 100644 index 50b42ad590..0000000000 --- a/testsuite/tests/polykinds/T9574.stderr +++ /dev/null @@ -1,4 +0,0 @@ - -T9574.hs:11:5: - The RHS of an associated type declaration mentions ‘o’ - All such variables must be bound on the LHS diff --git a/testsuite/tests/polykinds/all.T b/testsuite/tests/polykinds/all.T index bdba4c0ca4..864e204f72 100644 --- a/testsuite/tests/polykinds/all.T +++ b/testsuite/tests/polykinds/all.T @@ -106,7 +106,7 @@ test('T9200b', normal, compile_fail, ['']) test('T9750', normal, compile, ['']) test('T9569', normal, compile, ['']) test('T9838', normal, multimod_compile, ['T9838.hs','-v0']) -test('T9574', normal, compile_fail, ['']) +test('T9574', normal, compile, ['']) test('T9833', normal, compile, ['']) test('T7908', normal, compile, ['']) test('PolyInstances', normal, compile, ['']) @@ -163,6 +163,7 @@ test('T13393', normal, compile_fail, ['']) test('T13555', normal, compile_fail, ['']) test('T13659', normal, compile_fail, ['']) test('T13625', normal, compile_fail, ['']) +test('T13985', normal, compile_fail, ['']) test('T14110', normal, compile_fail, ['']) test('BadKindVar', normal, compile_fail, ['']) test('T13738', normal, compile_fail, ['']) |