Commit 02aa02f1 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Ben Gamari

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.

(cherry picked from commit 68149452)
parent fbc4ebaf
......@@ -23,7 +23,6 @@ module TcHsType (
-- Type checking type and class decls
kcLookupTcTyCon, kcTyClTyVars, tcTyClTyVars,
tcDataKindSig,
DataKindCheck(..),
-- Kind-checking types
-- No kind generalisation, no checkValidType
......@@ -42,7 +41,7 @@ module TcHsType (
reportFloatingKvs,
-- Sort-checking kinds
tcLHsKindSig,
tcLHsKindSig, badKindSig,
-- Pattern type signatures
tcHsPatSigType, tcPatSig, funAppCtxt
......@@ -64,6 +63,7 @@ import TcSimplify ( solveEqualities )
import TcType
import TcHsSyn( zonkSigType )
import Inst ( tcInstBinders, tcInstBinder )
import TyCoRep( TyBinder(..) ) -- Used in tcDataKindSig
import Type
import Kind
import RdrName( lookupLocalRdrOcc )
......@@ -91,7 +91,7 @@ import PrelNames hiding ( wildCardName )
import qualified GHC.LanguageExtensions as LangExt
import Maybes
import Data.List ( partition, zipWith4, mapAccumR )
import Data.List ( partition, mapAccumR )
import Control.Monad
{-
......@@ -1955,59 +1955,54 @@ tcTyClTyVars tycon_name thing_inside
tv = binderVar binder
new_fvs = fvs `delVarSet` tv `unionVarSet` tyCoVarsOfType (tyVarKind tv)
-----------------------------------
data DataKindCheck
-- Plain old data type; better be lifted
= LiftedDataKind
-- 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)
tcDataKindSig :: [TyConBinder]
-> Kind
-> TcM ([TyConBinder], Kind)
-- GADT decls can have a (perhaps partial) kind signature
-- e.g. data T :: * -> * -> * where ...
-- This function makes up suitable (kinded) type variables for
-- the argument kinds, and checks that the result kind is indeed * if requested.
-- (Otherwise, checks to make sure that the result kind is either * or a type variable.)
-- 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.
-- e.g. data T a :: * -> * -> * where ...
-- This function makes up suitable (kinded) TyConBinders for the
-- argument kinds. E.g. in this case it might return
-- ([b::*, c::*], *)
-- Never emits constraints.
-- Returns the new TyVars, the extracted TyBinders, and the new, reduced
-- result kind (which should always be Type or a synonym thereof)
tcDataKindSig kind_check kind
= do { case kind_check of
LiftedDataKind ->
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
-- It's a little trickier than you might think: see
-- Note [TyConBinders for the result kind signature of a data type]
tcDataKindSig tc_bndrs kind
= do { loc <- getSrcSpanM
; uniqs <- newUniqueSupply
; rdr_env <- getLocalRdrEnv
; let uniqs = uniqsFromSupply us
occs = [ occ | str <- allNameStrings
, let occ = mkOccName tvName str
, isNothing (lookupLocalRdrOcc rdr_env occ) ]
-- Note [Avoid name clashes for associated data types]
-- NB: Use the tv from a binder if there is one. Otherwise,
-- we end up inventing a new Unique for it, and any other tv
-- that mentions the first ends up with the wrong kind.
extra_bndrs = zipWith4 mkTyBinderTyConBinder
tv_bndrs (repeat span) uniqs occs
; return (extra_bndrs, res_kind) }
; let new_occs = [ occ
| str <- allNameStrings
, let occ = mkOccName tvName str
, isNothing (lookupLocalRdrOcc rdr_env occ)
-- 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
(tv_bndrs, res_kind) = splitPiTys kind
lhs_tvs = map binderVar tc_bndrs
lhs_occs = map getOccName lhs_tvs
go loc occs uniqs subst acc kind
= case splitPiTy_maybe kind of
Nothing -> (reverse acc, substTy subst kind)
Just (Anon arg, kind')
-> go loc occs' uniqs' subst' (tcb : acc) kind'
where
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 check_for_type kind
......@@ -2016,7 +2011,34 @@ badKindSig check_for_type kind
text "return 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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider class C a b where
......
......@@ -667,27 +667,27 @@ tcDataFamInstDecl mb_clsinfo
; rep_tc_name <- newFamInstTyConName 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'
eta_tvs = filterOut (`elem` etad_tvs) tvs'
-- 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
-- Remember, tvs' is in arbitrary order (except kind vars are
-- first, so there is no reason to suppose that the etad_tvs
-- (obtained from the pats) are at the end (Trac #11148)
extra_pats = map (mkTyVarTy . binderVar) extra_tcbs
all_pats = pats' `chkAppend` extra_pats
orig_res_ty = mkTyConApp fam_tc all_pats
-- 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
orig_res_ty = mkTyConApp fam_tc all_pats
; (rep_tc, axiom) <- fixM $ \ ~(rec_rep_tc, _) ->
do { let ty_binders = mkTyConBindersPreferAnon full_tvs res_kind'
`chkAppend` extra_tcbs
do { let ty_binders = full_tcbs `chkAppend` extra_tcbs
; data_cons <- tcConDecls rec_rep_tc
(ty_binders, orig_res_ty) cons
; tc_rhs <- case new_or_data of
......
......@@ -877,10 +877,18 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
= tcTyClTyVars tc_name $ \ binders res_kind -> do
{ traceTc "data family:" (ppr 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
; let tycon = mkFamilyTyCon tc_name (binders `chkAppend` extra_binders)
real_res_kind
final_res_kind
(resultVariableName sig)
(DataFamilyTyCon tc_rep_name)
parent NotInjective
......@@ -1024,10 +1032,10 @@ tcDataDefn roles_info
, dd_cons = cons })
= do { tcg_env <- getGblEnv
; let hsc_src = tcg_src tcg_env
check_kind = if mk_permissive_kind hsc_src cons
then AnyDataKind
else LiftedDataKind
; (extra_bndrs, real_res_kind) <- tcDataKindSig check_kind res_kind
; (extra_bndrs, final_res_kind) <- tcDataKindSig tycon_binders res_kind
; unless (mk_permissive_kind hsc_src cons) $
checkTc (isLiftedTypeKind final_res_kind) (badKindSig True res_kind)
; let final_bndrs = tycon_binders `chkAppend` extra_bndrs
roles = roles_info tc_name
......@@ -1049,7 +1057,7 @@ tcDataDefn roles_info
; tc_rep_nm <- newTyConRepName tc_name
; return (mkAlgTyCon tc_name
final_bndrs
real_res_kind
final_res_kind
roles
(fmap unLoc cType)
stupid_theta tc_rhs
......
......@@ -96,7 +96,6 @@ module Type (
binderRelevantType_maybe, caseBinder,
isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
tyConBindersTyBinders,
mkTyBinderTyConBinder,
-- ** Common type constructors
funTyCon,
......@@ -238,9 +237,6 @@ import Pair
import ListSetOps
import Digraph
import Unique ( nonDetCmpUnique )
import SrcLoc ( SrcSpan )
import OccName ( OccName )
import Name ( mkInternalName )
import Maybes ( orElse )
import Data.Maybe ( isJust, mapMaybe )
......@@ -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),
-- because the function part might well return a
-- partially-applied type constructor; indeed, usually will!
coreView (TyConApp tc [])
coreView (TyConApp tc []) -- At the Core level, Constraint = Type
| isStarKindSynonymTyCon tc
= Just liftedTypeKind
......@@ -1516,15 +1513,6 @@ caseBinder :: TyBinder -- ^ binder to scrutinize
caseBinder (Named v) f _ = f v
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
data Foo (a :: * -> *) (c :: k)
data Foo (a :: * -> *) (b :: k)
-- 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
......@@ -179,4 +179,5 @@ test('T14555', normal, compile_fail, [''])
test('T14563', normal, compile_fail, [''])
test('T14723', normal, compile, [''])
test('T14846', 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