Commit 68149452 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix tcDataKindSig

This patch fixes an outright bug in tcDataKindSig, shown up in Trac
of a data type declaration.  See Note [TyConBinders for the result kind
signature of a data type]

I also took the opportunity to elminate the DataKindCheck argument
and data type from tcDataKindSig, instead moving the check to the
call site, which is easier to understand.
parent 4a331e65
...@@ -23,7 +23,6 @@ module TcHsType ( ...@@ -23,7 +23,6 @@ module TcHsType (
-- Type checking type and class decls -- Type checking type and class decls
kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars, kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
tcDataKindSig, tcDataKindSig,
DataKindCheck(..),
-- Kind-checking types -- Kind-checking types
-- No kind generalisation, no checkValidType -- No kind generalisation, no checkValidType
...@@ -41,7 +40,7 @@ module TcHsType ( ...@@ -41,7 +40,7 @@ module TcHsType (
reportFloatingKvs, reportFloatingKvs,
-- Sort-checking kinds -- Sort-checking kinds
tcLHsKindSig, tcLHsKindSig, badKindSig,
-- Pattern type signatures -- Pattern type signatures
tcHsPatSigType, tcPatSig, funAppCtxt tcHsPatSigType, tcPatSig, funAppCtxt
...@@ -63,6 +62,7 @@ import TcSimplify ( solveEqualities ) ...@@ -63,6 +62,7 @@ import TcSimplify ( solveEqualities )
import TcType import TcType
import TcHsSyn( zonkSigType ) import TcHsSyn( zonkSigType )
import Inst ( tcInstBinders, tcInstBinder ) import Inst ( tcInstBinders, tcInstBinder )
import TyCoRep( TyBinder(..) ) -- Used in tcDataKindSig
import Type import Type
import Kind import Kind
import RdrName( lookupLocalRdrOcc ) import RdrName( lookupLocalRdrOcc )
...@@ -90,7 +90,7 @@ import PrelNames hiding ( wildCardName ) ...@@ -90,7 +90,7 @@ import PrelNames hiding ( wildCardName )
import qualified GHC.LanguageExtensions as LangExt import qualified GHC.LanguageExtensions as LangExt
import Maybes import Maybes
import Data.List ( partition, zipWith4, mapAccumR ) import Data.List ( partition, mapAccumR )
import Control.Monad import Control.Monad
{- {-
...@@ -1983,59 +1983,54 @@ tcTyClTyVars tycon_name thing_inside ...@@ -1983,59 +1983,54 @@ tcTyClTyVars tycon_name thing_inside
tv = binderVar binder tv = binderVar binder
new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv) new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
----------------------------------- -----------------------------------
data DataKindCheck tcDataKindSig :: [TyConBinder]
-- Plain old data type; better be lifted -> Kind
= LiftedDataKind -> TcM ([TyConBinder], Kind)
-- Data families might have a variable return kind.
-- See See Note [Arity of data families] in FamInstEnv for more info.
| LiftedOrVarDataKind
-- Abstract data in hsig files can have any kind at all;
-- even unlifted. This is because they might not actually
-- be implemented with a data declaration at the end of the day.
| AnyDataKind
tcDataKindSig :: DataKindCheck -- ^ Do we require the result to be *?
-> Kind -> TcM ([TyConBinder], Kind)
-- GADT decls can have a (perhaps partial) kind signature -- GADT decls can have a (perhaps partial) kind signature
-- e.g. data T :: * -> * -> * where ... -- e.g. data T a :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for -- This function makes up suitable (kinded) TyConBinders for the
-- the argument kinds, and checks that the result kind is indeed * if requested. -- argument kinds. E.g. in this case it might return
-- (Otherwise, checks to make sure that the result kind is either * or a type variable.) -- ([b::*, c::*], *)
-- See Note [Arity of data families] in FamInstEnv for more info.
-- We use it also to make up argument type variables for for data instances.
-- Never emits constraints. -- Never emits constraints.
-- Returns the new TyVars, the extracted TyBinders, and the new, reduced -- It's a little trickier than you might think: see
-- result kind (which should always be Type or a synonym thereof) -- Note [TyConBinders for the result kind signature of a data type]
tcDataKindSig kind_check kind tcDataKindSig tc_bndrs kind
= do { case kind_check of = do { loc <- getSrcSpanM
LiftedDataKind -> ; uniqs <- newUniqueSupply
checkTc (isLiftedTypeKind res_kind)
(badKindSig True kind)
LiftedOrVarDataKind ->
checkTc (isLiftedTypeKind res_kind || isJust (tcGetCastedTyVar_maybe res_kind))
(badKindSig False kind)
AnyDataKind -> return ()
; span <- getSrcSpanM
; us <- newUniqueSupply
; rdr_env <- getLocalRdrEnv ; rdr_env <- getLocalRdrEnv
; let uniqs = uniqsFromSupply us ; let new_occs = [ occ
occs = [ occ | str <- allNameStrings | str <- allNameStrings
, let occ = mkOccName tvName str , let occ = mkOccName tvName str
, isNothing (lookupLocalRdrOcc rdr_env occ) ] , isNothing (lookupLocalRdrOcc rdr_env occ)
-- Note [Avoid name clashes for associated data types] -- Note [Avoid name clashes for associated data types]
, not (occ `elem` lhs_occs) ]
new_uniqs = uniqsFromSupply uniqs
subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet lhs_tvs))
; return (go loc new_occs new_uniqs subst [] kind) }
where
lhs_tvs = map binderVar tc_bndrs
lhs_occs = map getOccName lhs_tvs
-- NB: Use the tv from a binder if there is one. Otherwise, go loc occs uniqs subst acc kind
-- we end up inventing a new Unique for it, and any other tv = case splitPiTy_maybe kind of
-- that mentions the first ends up with the wrong kind. Nothing -> (reverse acc, substTy subst kind)
extra_bndrs = zipWith4 mkTyBinderTyConBinder
tv_bndrs (repeat span) uniqs occs
; return (extra_bndrs, res_kind) } Just (Anon arg, kind')
-> go loc occs' uniqs' subst' (tcb : acc) kind'
where where
(tv_bndrs, res_kind) = splitPiTys kind arg' = substTy subst arg
tv = mkTyVar (mkInternalName uniq occ loc) arg'
subst' = extendTCvInScope subst tv
tcb = TvBndr tv AnonTCB
(uniq:uniqs') = uniqs
(occ:occs') = occs
Just (Named (TvBndr tv vis), kind')
-> go loc occs uniqs subst' (tcb : acc) kind'
where
(subst', tv') = substTyVarBndr subst tv
tcb = TvBndr tv' (NamedTCB vis)
badKindSig :: Bool -> Kind -> SDoc badKindSig :: Bool -> Kind -> SDoc
badKindSig check_for_type kind badKindSig check_for_type kind
...@@ -2044,7 +2039,34 @@ badKindSig check_for_type kind ...@@ -2044,7 +2039,34 @@ badKindSig check_for_type kind
text "return kind" ]) text "return kind" ])
2 (ppr kind) 2 (ppr kind)
{- {- Note [TyConBinders for the result kind signature of a data type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given
data T (a::*) :: * -> forall k. k -> *
we want to generate the extra TyConBinders for T, so we finally get
(a::*) (b::*) (k::*) (c::k)
The function tcDataKindSig generates these extra TyConBinders from
the result kind signature.
We need to take care to give the TyConBinders
(a) OccNames that are fresh (because the TyConBinders of a TyCon
must have distinct OccNames
(b) Uniques that are fresh (obviously)
For (a) we need to avoid clashes with the tyvars declared by
the user before the "::"; in the above example that is 'a'.
And also see Note [Avoid name clashes for associated data types].
For (b) suppose we have
data T :: forall k. k -> forall k. k -> *
where the two k's are identical even up to their uniques. Surprisingly,
this can happen: see Trac #14515.
It's reasonably easy to solve all this; just run down the list with a
substitution; hence the recursive 'go' function. But it has to be
done.
Note [Avoid name clashes for associated data types] Note [Avoid name clashes for associated data types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider class C a b where Consider class C a b where
......
...@@ -667,27 +667,27 @@ tcDataFamInstDecl mb_clsinfo ...@@ -667,27 +667,27 @@ tcDataFamInstDecl mb_clsinfo
; rep_tc_name <- newFamInstTyConName fam_tc_name pats' ; rep_tc_name <- newFamInstTyConName fam_tc_name pats'
; axiom_name <- newFamInstAxiomName fam_tc_name [pats'] ; axiom_name <- newFamInstAxiomName fam_tc_name [pats']
-- Deal with any kind signature.
-- See also Note [Arity of data families] in FamInstEnv
; (extra_tcbs, final_res_kind) <- tcDataKindSig LiftedDataKind res_kind'
; let (eta_pats, etad_tvs) = eta_reduce pats' ; let (eta_pats, etad_tvs) = eta_reduce pats'
eta_tvs = filterOut (`elem` etad_tvs) tvs' eta_tvs = filterOut (`elem` etad_tvs) tvs'
-- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced -- NB: the "extra" tvs from tcDataKindSig would always be eta-reduced
full_tvs = eta_tvs ++ etad_tvs full_tcbs = mkTyConBindersPreferAnon (eta_tvs ++ etad_tvs) res_kind'
-- Put the eta-removed tyvars at the end -- Put the eta-removed tyvars at the end
-- Remember, tvs' is in arbitrary order (except kind vars are -- Remember, tvs' is in arbitrary order (except kind vars are
-- first, so there is no reason to suppose that the etad_tvs -- first, so there is no reason to suppose that the etad_tvs
-- (obtained from the pats) are at the end (Trac #11148) -- (obtained from the pats) are at the end (Trac #11148)
extra_pats = map (mkTyVarTy . binderVar) extra_tcbs -- Deal with any kind signature.
-- See also Note [Arity of data families] in FamInstEnv
; (extra_tcbs, final_res_kind) <- tcDataKindSig full_tcbs res_kind'
; checkTc (isLiftedTypeKind final_res_kind) (badKindSig True res_kind')
; let extra_pats = map (mkTyVarTy . binderVar) extra_tcbs
all_pats = pats' `chkAppend` extra_pats all_pats = pats' `chkAppend` extra_pats
orig_res_ty = mkTyConApp fam_tc all_pats orig_res_ty = mkTyConApp fam_tc all_pats
; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) -> ; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
do { let ty_binders = mkTyConBindersPreferAnon full_tvs res_kind' do { let ty_binders = full_tcbs `chkAppend` extra_tcbs
`chkAppend` extra_tcbs
; data_cons <- tcConDecls rec_rep_tc ; data_cons <- tcConDecls rec_rep_tc
(ty_binders, orig_res_ty) cons (ty_binders, orig_res_ty) cons
; tc_rhs <- case new_or_data of ; tc_rhs <- case new_or_data of
......
...@@ -881,10 +881,18 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na ...@@ -881,10 +881,18 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
= tcTyClTyVars tc_name $ \ binders res_kind -> do = tcTyClTyVars tc_name $ \ binders res_kind -> do
{ traceTc "data family:" (ppr tc_name) { traceTc "data family:" (ppr tc_name)
; checkFamFlag tc_name ; checkFamFlag tc_name
; (extra_binders, real_res_kind) <- tcDataKindSig LiftedOrVarDataKind res_kind
-- Check the kind signature, if any.
-- Data families might have a variable return kind.
-- See See Note [Arity of data families] in FamInstEnv.
; (extra_binders, final_res_kind) <- tcDataKindSig binders res_kind
; checkTc (isLiftedTypeKind final_res_kind
|| isJust (tcGetCastedTyVar_maybe final_res_kind))
(badKindSig False res_kind)
; tc_rep_name <- newTyConRepName tc_name ; tc_rep_name <- newTyConRepName tc_name
; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders) ; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
real_res_kind final_res_kind
(resultVariableName sig) (resultVariableName sig)
(DataFamilyTyCon tc_rep_name) (DataFamilyTyCon tc_rep_name)
parent NotInjective parent NotInjective
...@@ -1028,10 +1036,10 @@ tcDataDefn roles_info ...@@ -1028,10 +1036,10 @@ tcDataDefn roles_info
, dd_cons = cons }) , dd_cons = cons })
= do { tcg_env <- getGblEnv = do { tcg_env <- getGblEnv
; let hsc_src = tcg_src tcg_env ; let hsc_src = tcg_src tcg_env
check_kind = if mk_permissive_kind hsc_src cons ; (extra_bndrs, final_res_kind) <- tcDataKindSig tycon_binders res_kind
then AnyDataKind ; unless (mk_permissive_kind hsc_src cons) $
else LiftedDataKind checkTc (isLiftedTypeKind final_res_kind) (badKindSig True res_kind)
; (extra_bndrs, real_res_kind) <- tcDataKindSig check_kind res_kind
; let final_bndrs = tycon_binders `chkAppend` extra_bndrs ; let final_bndrs = tycon_binders `chkAppend` extra_bndrs
roles = roles_info tc_name roles = roles_info tc_name
...@@ -1053,7 +1061,7 @@ tcDataDefn roles_info ...@@ -1053,7 +1061,7 @@ tcDataDefn roles_info
; tc_rep_nm <- newTyConRepName tc_name ; tc_rep_nm <- newTyConRepName tc_name
; return (mkAlgTyCon tc_name ; return (mkAlgTyCon tc_name
final_bndrs final_bndrs
real_res_kind final_res_kind
roles roles
(fmap unLoc cType) (fmap unLoc cType)
stupid_theta tc_rhs stupid_theta tc_rhs
......
...@@ -96,7 +96,6 @@ module Type ( ...@@ -96,7 +96,6 @@ module Type (
binderRelevantType_maybe, caseBinder, binderRelevantType_maybe, caseBinder,
isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder, isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
tyConBindersTyBinders, tyConBindersTyBinders,
mkTyBinderTyConBinder,
-- ** Common type constructors -- ** Common type constructors
funTyCon, funTyCon,
...@@ -238,9 +237,6 @@ import Pair ...@@ -238,9 +237,6 @@ import Pair
import ListSetOps import ListSetOps
import Digraph import Digraph
import Unique ( nonDetCmpUnique ) import Unique ( nonDetCmpUnique )
import SrcLoc ( SrcSpan )
import OccName ( OccName )
import Name ( mkInternalName )
import Maybes ( orElse ) import Maybes ( orElse )
import Data.Maybe ( isJust, mapMaybe ) import Data.Maybe ( isJust, mapMaybe )
...@@ -340,7 +336,8 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc t ...@@ -340,7 +336,8 @@ coreView (TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc t
-- Its important to use mkAppTys, rather than (foldl AppTy), -- Its important to use mkAppTys, rather than (foldl AppTy),
-- because the function part might well return a -- because the function part might well return a
-- partially-applied type constructor; indeed, usually will! -- partially-applied type constructor; indeed, usually will!
coreView (TyConApp tc [])
coreView (TyConApp tc []) -- At the Core level, Constraint = Type
| isStarKindSynonymTyCon tc | isStarKindSynonymTyCon tc
= Just liftedTypeKind = Just liftedTypeKind
...@@ -1517,15 +1514,6 @@ caseBinder :: TyBinder -- ^ binder to scrutinize ...@@ -1517,15 +1514,6 @@ caseBinder :: TyBinder -- ^ binder to scrutinize
caseBinder (Named v) f _ = f v caseBinder (Named v) f _ = f v
caseBinder (Anon t) _ d = d t caseBinder (Anon t) _ d = d t
-- | Manufacture a new 'TyConBinder' from a 'TyBinder'. Anonymous
-- 'TyBinder's are still assigned names as 'TyConBinder's, so we need
-- the extra gunk with which to construct a 'Name'. Used when producing
-- tyConTyVars from a datatype kind signature. Defined here to avoid module
-- loops.
mkTyBinderTyConBinder :: TyBinder -> SrcSpan -> Unique -> OccName -> TyConBinder
mkTyBinderTyConBinder (Named (TvBndr tv argf)) _ _ _ = TvBndr tv (NamedTCB argf)
mkTyBinderTyConBinder (Anon kind) loc uniq occ
= TvBndr (mkTyVar (mkInternalName uniq occ loc) kind) AnonTCB
{- {-
%************************************************************************ %************************************************************************
......
type role Foo phantom phantom type role Foo phantom phantom
data Foo (a :: * -> *) (c :: k) data Foo (a :: * -> *) (b :: k)
-- Defined at <interactive>:3:1 -- Defined at <interactive>:3:1
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeInType #-}
module Bug where
import Data.Kind
type HRank1 ty = forall k1. k1 -> ty
type HRank2 ty = forall k2. k2 -> ty
data HREFL11 :: HRank1 (HRank1 Type) -- FAILS
data HREFL12 :: HRank1 (HRank2 Type)
data HREFL21 :: HRank2 (HRank1 Type)
data HREFL22 :: HRank2 (HRank2 Type) -- FAILS
...@@ -182,4 +182,5 @@ test('T14555', normal, compile_fail, ['']) ...@@ -182,4 +182,5 @@ test('T14555', normal, compile_fail, [''])
test('T14563', normal, compile_fail, ['']) test('T14563', normal, compile_fail, [''])
test('T14561', normal, compile_fail, ['']) test('T14561', normal, compile_fail, [''])
test('T14580', normal, compile_fail, ['']) test('T14580', normal, compile_fail, [''])
test('T14515', normal, compile, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment