Commit 489e6ab5 authored by eir@cis.upenn.edu's avatar eir@cis.upenn.edu

Fix #11246.

We have to instantiate any invisible arguments to type families
right away. This is now done in tcTyCon in TcHsType.

testcase: typecheck/should_compile/T11246
parent 43468fe3
......@@ -984,29 +984,17 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
; case thing of
ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
ATcTyCon tc_tc -> do { data_kinds <- xoptM LangExt.DataKinds
; unless (isTypeLevel (mode_level mode) ||
data_kinds) $
promotionErr name NoDataKindsTC
ATcTyCon tc_tc -> do { check_tc tc_tc
; tc <- get_loopy_tc name tc_tc
; return (mkNakedTyConApp tc [], tyConKind tc_tc) }
; handle_tyfams tc tc_tc }
-- mkNakedTyConApp: see Note [Type-checking inside the knot]
-- NB: we really should check if we're at the kind level
-- and if the tycon is promotable if -XNoTypeInType is set.
-- But this is a terribly large amount of work! Not worth it.
AGlobal (ATyCon tc)
-> do { type_in_type <- xoptM LangExt.TypeInType
; data_kinds <- xoptM LangExt.DataKinds
; unless (isTypeLevel (mode_level mode) ||
data_kinds ||
isKindTyCon tc) $
promotionErr name NoDataKindsTC
; unless (isTypeLevel (mode_level mode) ||
type_in_type ||
isLegacyPromotableTyCon tc) $
promotionErr name NoTypeInTypeTC
; return (mkTyConApp tc [], tyConKind tc) }
-> do { check_tc tc
; handle_tyfams tc tc }
AGlobal (AConLike (RealDataCon dc))
-> do { data_kinds <- xoptM LangExt.DataKinds
......@@ -1026,6 +1014,33 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
_ -> wrongThingErr "type" thing name }
where
check_tc :: TyCon -> TcM ()
check_tc tc = do { type_in_type <- xoptM LangExt.TypeInType
; data_kinds <- xoptM LangExt.DataKinds
; unless (isTypeLevel (mode_level mode) ||
data_kinds ||
isKindTyCon tc) $
promotionErr name NoDataKindsTC
; unless (isTypeLevel (mode_level mode) ||
type_in_type ||
isLegacyPromotableTyCon tc) $
promotionErr name NoTypeInTypeTC }
-- if we are type-checking a type family tycon, we must instantiate
-- any invisible arguments right away. Otherwise, we get #11246
handle_tyfams :: TyCon -- the tycon to instantiate (might be loopy)
-> TyCon -- a non-loopy version of the tycon
-> TcM (TcType, TcKind)
handle_tyfams tc tc_tc
| mightBeUnsaturatedTyCon tc_tc
= return (ty, tc_kind)
| otherwise
= instantiateTyN 0 ty tc_kind
where
ty = mkNakedTyConApp tc []
tc_kind = tyConKind tc_tc
get_loopy_tc :: Name -> TyCon -> TcM TyCon
-- Return the knot-tied global TyCon if there is one
-- Otherwise the local TcTyCon; we must be doing kind checking
......
......@@ -148,8 +148,8 @@ tcTyClGroup tyclds
-- Also extend the local type envt with bindings giving
-- the (polymorphic) kind of each knot-tied TyCon or Class
-- See Note [Type checking recursive type and class declarations]
tcExtendKindEnv2 [ mkTcTyConPair name kind
| (name, kind) <- names_w_poly_kinds ] $
tcExtendKindEnv2 [ mkTcTyConPair name kind unsat
| (name, kind, unsat) <- names_w_poly_kinds ] $
-- Kind and type check declarations for this group
mapM (tcTyClDecl rec_flags) decls }
......@@ -170,7 +170,7 @@ tcTyClGroup tyclds
; tcExtendTyConEnv tyclss $
tcAddImplicits tyclss }
zipRecTyClss :: [(Name, Kind)]
zipRecTyClss :: [(Name, Kind, Bool)]
-> [TyCon] -- Knot-tied
-> [(Name,TyThing)]
-- Build a name-TyThing mapping for the TyCons bound by decls
......@@ -179,7 +179,7 @@ zipRecTyClss :: [(Name, Kind)]
-- because typechecking types (in, say, tcTyClDecl) looks at
-- this outer constructor
zipRecTyClss kind_pairs rec_tycons
= [ (name, ATyCon (get name)) | (name, _kind) <- kind_pairs ]
= [ (name, ATyCon (get name)) | (name, _kind, _unsat) <- kind_pairs ]
where
rec_tc_env :: NameEnv TyCon
rec_tc_env = foldr add_tc emptyNameEnv rec_tycons
......@@ -260,10 +260,11 @@ See also Note [Kind checking recursive type and class declarations]
-}
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind)]
kcTyClGroup :: TyClGroup Name -> TcM [(Name,Kind,Bool)]
-- Kind check this group, kind generalize, and return the resulting local env
-- This bindds the TyCons and Classes of the group, but not the DataCons
-- See Note [Kind checking for type and class decls]
-- Third return value is whether or not the tycon can appear unsaturated
kcTyClGroup (TyClGroup { group_tyclds = decls })
= do { mod <- getModule
; traceTc "kcTyClGroup" (text "module" <+> ppr mod $$ vcat (map ppr decls))
......@@ -301,21 +302,22 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
; return res }
where
generalise :: TcTypeEnv -> Name -> TcM (Name, Kind)
generalise :: TcTypeEnv -> Name -> TcM (Name, Kind, Bool)
-- For polymorphic things this is a no-op
generalise kind_env name
= do { let kc_kind = case lookupNameEnv kind_env name of
Just (ATcTyCon tc) -> tyConKind tc
_ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
= do { let (kc_kind, kc_unsat) = case lookupNameEnv kind_env name of
Just (ATcTyCon tc) -> ( tyConKind tc
, mightBeUnsaturatedTyCon tc )
_ -> pprPanic "kcTyClGroup" (ppr name $$ ppr kind_env)
; kvs <- kindGeneralize kc_kind
; kc_kind' <- zonkTcTypeToType emptyZonkEnv kc_kind
-- Make sure kc_kind' has the final, zonked kind variables
; traceTc "Generalise kind" (vcat [ ppr name, ppr kc_kind, ppr kvs, ppr kc_kind' ])
; return (name, mkInvForAllTys kvs kc_kind') }
; return (name, mkInvForAllTys kvs kc_kind', kc_unsat) }
generaliseTCD :: TcTypeEnv
-> LTyClDecl Name -> TcM [(Name, Kind)]
-> LTyClDecl Name -> TcM [(Name, Kind, Bool)]
generaliseTCD kind_env (L _ decl)
| ClassDecl { tcdLName = (L _ name), tcdATs = ats } <- decl
= do { first <- generalise kind_env name
......@@ -331,14 +333,15 @@ kcTyClGroup (TyClGroup { group_tyclds = decls })
; return [res] }
generaliseFamDecl :: TcTypeEnv
-> FamilyDecl Name -> TcM (Name, Kind)
-> FamilyDecl Name -> TcM (Name, Kind, Bool)
generaliseFamDecl kind_env (FamilyDecl { fdLName = L _ name })
= generalise kind_env name
mkTcTyConPair :: Name -> TcKind -> (Name, TcTyThing)
mkTcTyConPair :: Name -> TcKind -> Bool -- ^ can the tycon appear unsaturated?
-> (Name, TcTyThing)
-- Makes a binding to put in the local envt, binding
-- a name to a TcTyCon with the specified kind
mkTcTyConPair name kind = (name, ATcTyCon (mkTcTyCon name kind))
mkTcTyConPair name kind unsat = (name, ATcTyCon (mkTcTyCon name kind unsat))
mk_thing_env :: [LTyClDecl Name] -> [(Name, TcTyThing)]
mk_thing_env [] = []
......@@ -383,7 +386,7 @@ getInitialKind decl@(ClassDecl { tcdLName = L _ name, tcdTyVars = ktvs, tcdATs =
do { inner_prs <- getFamDeclInitialKinds ats
; return (constraintKind, inner_prs) }
; cl_kind <- zonkTcType cl_kind
; let main_pr = mkTcTyConPair name cl_kind
; let main_pr = mkTcTyConPair name cl_kind True
; return (main_pr : inner_prs) }
getInitialKind decl@(DataDecl { tcdLName = L _ name
......@@ -397,7 +400,7 @@ getInitialKind decl@(DataDecl { tcdLName = L _ name
Nothing -> return liftedTypeKind
; return (res_k, ()) }
; decl_kind <- zonkTcType decl_kind
; let main_pr = mkTcTyConPair name decl_kind
; let main_pr = mkTcTyConPair name decl_kind True
inner_prs = [ (unLoc con, APromotionErr RecDataConPE)
| L _ con' <- cons, con <- getConNames con' ]
; return (main_pr : inner_prs) }
......@@ -419,7 +422,8 @@ getFamDeclInitialKind :: FamilyDecl Name
-> TcM [(Name, TcTyThing)]
getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
, fdTyVars = ktvs
, fdResultSig = L _ resultSig })
, fdResultSig = L _ resultSig
, fdInfo = info })
= do { (fam_kind, _) <-
kcHsTyVarBndrs (famDeclHasCusk decl) ktvs $ \_ _ ->
do { res_k <- case resultSig of
......@@ -432,7 +436,12 @@ getFamDeclInitialKind decl@(FamilyDecl { fdLName = L _ name
| otherwise -> newMetaKindVar
; return (res_k, ()) }
; fam_kind <- zonkTcType fam_kind
; return [ mkTcTyConPair name fam_kind ] }
; return [ mkTcTyConPair name fam_kind unsat ] }
where
unsat = case info of
DataFamily -> True
OpenTypeFamily -> False
ClosedTypeFamily _ -> False
----------------
kcSynDecls :: [SCC (LTyClDecl Name)]
......@@ -440,7 +449,7 @@ kcSynDecls :: [SCC (LTyClDecl Name)]
kcSynDecls [] = getLclEnv
kcSynDecls (group : groups)
= do { (n,k) <- kcSynDecl1 group
; tcExtendKindEnv2 [ mkTcTyConPair n k ] $
; tcExtendKindEnv2 [ mkTcTyConPair n k False ] $
kcSynDecls groups }
kcSynDecl1 :: SCC (LTyClDecl Name)
......
......@@ -598,6 +598,7 @@ data TyCon
| TcTyCon {
tyConUnique :: Unique,
tyConName :: Name,
tyConUnsat :: Bool, -- ^ can this tycon be unsaturated?
tyConKind :: Kind
}
deriving Typeable
......@@ -1216,11 +1217,13 @@ mkTupleTyCon name kind arity tyvars con sort parent
-- TcErrors sometimes calls typeKind.
-- See also Note [Kind checking recursive type and class declarations]
-- in TcTyClsDecls.
mkTcTyCon :: Name -> Kind -> TyCon
mkTcTyCon name kind
mkTcTyCon :: Name -> Kind -> Bool -- ^ Can this be unsaturated?
-> TyCon
mkTcTyCon name kind unsat
= TcTyCon { tyConUnique = getUnique name
, tyConName = name
, tyConKind = kind }
, tyConKind = kind
, tyConUnsat = unsat }
-- | Create an unlifted primitive 'TyCon', such as @Int#@
mkPrimTyCon :: Name -> Kind -> [Role] -> PrimRep -> TyCon
......@@ -1509,6 +1512,7 @@ isTypeSynonymTyCon _ = False
mightBeUnsaturatedTyCon :: TyCon -> Bool
mightBeUnsaturatedTyCon (SynonymTyCon {}) = False
mightBeUnsaturatedTyCon (FamilyTyCon { famTcFlav = flav}) = isDataFamFlav flav
mightBeUnsaturatedTyCon (TcTyCon { tyConUnsat = unsat }) = unsat
mightBeUnsaturatedTyCon _other = True
-- | Is this an algebraic 'TyCon' declared with the GADT syntax?
......
module T11246 where
import GHC.Exts
type Key a = Any
......@@ -505,3 +505,4 @@ test('T11397', normal, compile, [''])
test('T11458', normal, compile, [''])
test('T11524', normal, compile, [''])
test('T11552', normal, compile, [''])
test('T11246', 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