Skip to content

Commit

Permalink
Fix #11246.
Browse files Browse the repository at this point in the history
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
  • Loading branch information
Richard Eisenberg committed Feb 17, 2016
1 parent 43468fe commit 489e6ab
Show file tree
Hide file tree
Showing 5 changed files with 72 additions and 38 deletions.
47 changes: 31 additions & 16 deletions compiler/typecheck/TcHsType.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
47 changes: 28 additions & 19 deletions compiler/typecheck/TcTyClsDecls.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 }
Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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
Expand All @@ -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 [] = []
Expand Down Expand Up @@ -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
Expand All @@ -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) }
Expand All @@ -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
Expand All @@ -432,15 +436,20 @@ 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)]
-> TcM TcLclEnv -- Kind bindings
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)
Expand Down
10 changes: 7 additions & 3 deletions compiler/types/TyCon.hs
Original file line number Diff line number Diff line change
Expand Up @@ -598,6 +598,7 @@ data TyCon
| TcTyCon {
tyConUnique :: Unique,
tyConName :: Name,
tyConUnsat :: Bool, -- ^ can this tycon be unsaturated?
tyConKind :: Kind
}
deriving Typeable
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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?
Expand Down
5 changes: 5 additions & 0 deletions testsuite/tests/typecheck/should_compile/T11246.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module T11246 where

import GHC.Exts

type Key a = Any
1 change: 1 addition & 0 deletions testsuite/tests/typecheck/should_compile/all.T
Original file line number Diff line number Diff line change
Expand Up @@ -505,3 +505,4 @@ test('T11397', normal, compile, [''])
test('T11458', normal, compile, [''])
test('T11524', normal, compile, [''])
test('T11552', normal, compile, [''])
test('T11246', normal, compile, [''])

0 comments on commit 489e6ab

Please sign in to comment.