diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2017-09-05 11:00:56 -0400 |
---|---|---|
committer | Ryan Scott <ryan.gl.scott@gmail.com> | 2017-09-05 11:00:57 -0400 |
commit | 0829821a6b886788a3ba6989e57e25a037bb6d05 (patch) | |
tree | 115a892a6df20303a7f0b65009f7afa589c14d2d /compiler/rename | |
parent | 24e50f988f775c6bba7d1daaee2e23c13650aa3b (diff) | |
download | haskell-0829821a6b886788a3ba6989e57e25a037bb6d05.tar.gz |
Implicitly bind kind variables in type family instance RHSes when it's sensible
Summary:
Before, there was a discrepancy in how GHC renamed type synonyms as
opposed to type family instances. That is, GHC would accept definitions like
this one:
```lang=haskell
type T = (Nothing :: Maybe a)
```
However, it would not accept a very similar type family instance:
```lang=haskell
type family T :: Maybe a
type instance T = (Nothing :: Maybe a)
```
The primary goal of this patch is to bring the renaming of type family
instances up to par with that of type synonyms, causing the latter definition
to be accepted, and fixing #14131.
In particular, we now allow kind variables on the right-hand sides of type
(and data) family instances to be //implicitly// bound by LHS type (or kind)
patterns (as opposed to type variables, which must always be explicitly
bound by LHS type patterns only). As a consequence, this allows programs
reported in #7938 and #9574 to typecheck, whereas before they would
have been rejected.
Implementation-wise, there isn't much trickery involved in making this happen.
We simply need to bind additional kind variables from the RHS of a type family
in the right place (in particular, see `RnSource.rnFamInstEqn`, which has
undergone a minor facelift).
While doing this has the upside of fixing #14131, it also made it easier to
trigger #13985, so I decided to fix that while I was in town. This was
accomplished by a careful blast of `reportFloatingKvs` in `tcFamTyPats`.
Test Plan: ./validate
Reviewers: simonpj, goldfire, austin, bgamari
Reviewed By: simonpj
Subscribers: rwbarton, thomie
GHC Trac Issues: #13985, #14131
Differential Revision: https://phabricator.haskell.org/D3872
Diffstat (limited to 'compiler/rename')
-rw-r--r-- | compiler/rename/RnSource.hs | 81 | ||||
-rw-r--r-- | compiler/rename/RnTypes.hs | 15 |
2 files changed, 67 insertions, 29 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. |