Commit f8618a9b authored by Richard Eisenberg's avatar Richard Eisenberg

Remove the type-checking knot.

Bug #15380 hangs because a knot-tied TyCon ended up in a kind.
Looking at the code in tcInferApps, I'm amazed this hasn't happened
before! I couldn't think of a good way to fix it (with dependent
types, we can't really keep types out of kinds, after all), so
I just went ahead and removed the knot.

This was remarkably easy to do. In tcTyVar, when we find a TcTyCon,
just use it. (Previously, we looked up the knot-tied TyCon and used
that.) Then, during the final zonk, replace TcTyCons with the real,
full-blooded TyCons in the global environment. It's all very easy.

The new bit is explained in the existing
Note [Type checking recursive type and class declarations]
in TcTyClsDecls.

Naturally, I removed various references to the knot and the
zonkTcTypeInKnot (and related) functions. Now, we can print types
during type checking with abandon!

NB: There is a teensy error message regression with this patch,
around the ordering of quantified type variables. This ordering
problem is fixed (I believe) with the patch for #14880. The ordering
affects only internal variables that cannot be instantiated with
any kind of visible type application.

There is also a teensy regression around the printing of types
in TH splices. I think this is really a TH bug and will file
separately.

Test case: dependent/should_fail/T15380
parent 1df50a0f
......@@ -844,27 +844,27 @@ isMarkedStrict _ = True -- All others are strict
-- | Build a new data constructor
mkDataCon :: Name
-> Bool -- ^ Is the constructor declared infix?
-> TyConRepName -- ^ TyConRepName for the promoted TyCon
-> [HsSrcBang] -- ^ Strictness/unpack annotations, from user
-> [FieldLabel] -- ^ Field labels for the constructor,
-- if it is a record, otherwise empty
-> [TyVar] -- ^ Universals.
-> [TyVar] -- ^ Existentials.
-> [TyVarBinder] -- ^ User-written 'TyVarBinder's.
-- These must be Inferred/Specified.
-- See @Note [TyVarBinders in DataCons]@
-> [EqSpec] -- ^ GADT equalities
-> ThetaType -- ^ Theta-type occuring before the arguments proper
-> [Type] -- ^ Original argument types
-> Type -- ^ Original result type
-> RuntimeRepInfo -- ^ See comments on 'TyCon.RuntimeRepInfo'
-> TyCon -- ^ Representation type constructor
-> ConTag -- ^ Constructor tag
-> ThetaType -- ^ The "stupid theta", context of the data
-- declaration e.g. @data Eq a => T a ...@
-> Id -- ^ Worker Id
-> DataConRep -- ^ Representation
-> Bool -- ^ Is the constructor declared infix?
-> TyConRepName -- ^ TyConRepName for the promoted TyCon
-> [HsSrcBang] -- ^ Strictness/unpack annotations, from user
-> [FieldLabel] -- ^ Field labels for the constructor,
-- if it is a record, otherwise empty
-> [TyVar] -- ^ Universals.
-> [TyVar] -- ^ Existentials.
-> [TyVarBinder] -- ^ User-written 'TyVarBinder's.
-- These must be Inferred/Specified.
-- See @Note [TyVarBinders in DataCons]@
-> [EqSpec] -- ^ GADT equalities
-> KnotTied ThetaType -- ^ Theta-type occuring before the arguments proper
-> [KnotTied Type] -- ^ Original argument types
-> KnotTied Type -- ^ Original result type
-> RuntimeRepInfo -- ^ See comments on 'TyCon.RuntimeRepInfo'
-> KnotTied TyCon -- ^ Representation type constructor
-> ConTag -- ^ Constructor tag
-> ThetaType -- ^ The "stupid theta", context of the data
-- declaration e.g. @data Eq a => T a ...@
-> Id -- ^ Worker Id
-> DataConRep -- ^ Representation
-> DataCon
-- Can get the tag from the TyCon
......@@ -1429,8 +1429,8 @@ buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
where
binders = mkTyConBindersPreferAnon ktvs liftedTypeKind
buildSynTyCon :: Name -> [TyConBinder] -> Kind -- ^ /result/ kind
-> [Role] -> Type -> TyCon
buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind -- ^ /result/ kind
-> [Role] -> KnotTied Type -> TyCon
buildSynTyCon name binders res_kind roles rhs
= mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
where
......
......@@ -8,7 +8,7 @@
module BuildTyCl (
buildDataCon,
buildPatSyn,
TcMethInfo, buildClass,
TcMethInfo, MethInfo, buildClass,
mkNewTyConRhs,
newImplicitBinder, newTyConRepName
) where
......@@ -104,10 +104,11 @@ buildDataCon :: FamInstEnvs
-> [TyVar] -- Existentials
-> [TyVarBinder] -- User-written 'TyVarBinder's
-> [EqSpec] -- Equality spec
-> ThetaType -- Does not include the "stupid theta"
-> KnotTied ThetaType -- Does not include the "stupid theta"
-- or the GADT equalities
-> [Type] -> Type -- Argument and result types
-> TyCon -- Rep tycon
-> [KnotTied Type] -- Arguments
-> KnotTied Type -- Result types
-> KnotTied TyCon -- Rep tycon
-> NameEnv ConTag -- Maps the Name of each DataCon to its
-- ConTag
-> TcRnIf m n DataCon
......@@ -213,7 +214,8 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
------------------------------------------------------
type TcMethInfo -- A temporary intermediate, to communicate
type TcMethInfo = MethInfo -- this variant needs zonking
type MethInfo -- A temporary intermediate, to communicate
-- between tcClassSigs and buildClass.
= ( Name -- Name of the class op
, Type -- Type of the class op
......@@ -237,7 +239,7 @@ buildClass :: Name -- Name of the class/tycon (they have the same Name)
-> [FunDep TyVar] -- Functional dependencies
-- Super classes, associated types, method info, minimal complete def.
-- This is Nothing if the class is abstract.
-> Maybe (ThetaType, [ClassATItem], [TcMethInfo], ClassMinimalDef)
-> Maybe (KnotTied ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
-> TcRnIf m n Class
buildClass tycon_name binders roles fds Nothing
......
......@@ -443,7 +443,7 @@ checkFamInstConsistency directlyImpMods
-- as quickly as possible, so that we aren't typechecking
-- values with inconsistent axioms in scope.
--
-- See also Note [Tying the knot] and Note [Type-checking inside the knot]
-- See also Note [Tying the knot]
-- for why we are doing this at all.
; let check_now = famInstEnvElts env1
; mapM_ (checkForConflicts (emptyFamInstEnv, env2)) check_now
......
......@@ -18,7 +18,7 @@ module TcEnv(
tcExtendGlobalEnv, tcExtendTyConEnv,
tcExtendGlobalEnvImplicit, setGlobalTypeEnv,
tcExtendGlobalValEnv,
tcLookupLocatedGlobal, tcLookupGlobal,
tcLookupLocatedGlobal, tcLookupGlobal, tcLookupGlobalOnly,
tcLookupTyCon, tcLookupClass,
tcLookupDataCon, tcLookupPatSyn, tcLookupConLike,
tcLookupLocatedGlobalId, tcLookupLocatedTyCon,
......@@ -229,6 +229,15 @@ tcLookupGlobal name
Failed msg -> failWithTc msg
}}}
-- Look up only in this module's global env't. Don't look in imports, etc.
-- Panic if it's not there.
tcLookupGlobalOnly :: Name -> TcM TyThing
tcLookupGlobalOnly name
= do { env <- getGblEnv
; return $ case lookupNameEnv (tcg_type_env env) name of
Just thing -> thing
Nothing -> pprPanic "tcLookupGlobalOnly" (ppr name) }
tcLookupDataCon :: Name -> TcM DataCon
tcLookupDataCon name = do
thing <- tcLookupGlobal name
......
......@@ -34,8 +34,9 @@ module TcHsSyn (
zonkTyVarBindersX, zonkTyVarBinderX,
emptyZonkEnv, mkEmptyZonkEnv,
zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
zonkCoToCo, zonkSigType,
zonkEvBinds, zonkTcEvBinds
zonkCoToCo,
zonkEvBinds, zonkTcEvBinds,
zonkTcMethInfoToMethInfo
) where
#include "HsVersions.h"
......@@ -47,11 +48,13 @@ import Id
import IdInfo
import TcRnMonad
import PrelNames
import BuildTyCl ( TcMethInfo, MethInfo )
import TcType
import TcMType
import TcEnv ( tcLookupGlobalOnly )
import TcEvidence
import TysPrim
import TyCon ( isUnboxedTupleTyCon )
import TyCon
import TysWiredIn
import TyCoRep( CoercionHole(..) )
import Type
......@@ -1675,11 +1678,20 @@ zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
zonk_tycomapper :: TyCoMapper ZonkEnv TcM
zonk_tycomapper = TyCoMapper
{ tcm_smart = True -- Establish type invariants
-- See Note [Type-checking inside the knot] in TcHsType
, tcm_tyvar = zonkTyVarOcc
, tcm_covar = zonkCoVarOcc
, tcm_hole = zonkCoHole
, tcm_tybinder = \env tv _vis -> zonkTyBndrX env tv }
, tcm_tybinder = \env tv _vis -> zonkTyBndrX env tv
, tcm_tycon = zonkTcTyConToTyCon }
-- Zonk a TyCon by changing a TcTyCon to a regular TyCon
zonkTcTyConToTyCon :: TcTyCon -> TcM TyCon
zonkTcTyConToTyCon tc
| isTcTyCon tc = do { thing <- tcLookupGlobalOnly (getName tc)
; case thing of
ATyCon real_tc -> return real_tc
_ -> pprPanic "zonkTcTyCon" (ppr tc $$ ppr thing) }
| otherwise = return tc -- it's already zonked
-- Confused by zonking? See Note [What is zonking?] in TcMType.
zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
......@@ -1691,18 +1703,19 @@ zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion
zonkCoToCo = mapCoercion zonk_tycomapper
zonkSigType :: TcType -> TcM Type
-- Zonk the type obtained from a user type signature
-- We want to turn any quantified (forall'd) variables into TyVars
-- but we may find some free TcTyVars, and we want to leave them
-- completely alone. They may even have unification variables inside
-- e.g. f (x::a) = ...(e :: a -> a)....
-- The type sig for 'e' mentions a free 'a' which will be a
-- unification SigTv variable.
zonkSigType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_tv)
zonkTcMethInfoToMethInfo :: TcMethInfo -> TcM MethInfo
zonkTcMethInfoToMethInfo (name, ty, gdm_spec)
= do { ty' <- zonkTcTypeToType emptyZonkEnv ty
; gdm_spec' <- zonk_gdm gdm_spec
; return (name, ty', gdm_spec') }
where
zonk_unbound_tv :: UnboundTyVarZonker
zonk_unbound_tv tv = return (mkTyVarTy tv)
zonk_gdm :: Maybe (DefMethSpec (SrcSpan, TcType))
-> TcM (Maybe (DefMethSpec (SrcSpan, Type)))
zonk_gdm Nothing = return Nothing
zonk_gdm (Just VanillaDM) = return (Just VanillaDM)
zonk_gdm (Just (GenericDM (loc, ty)))
= do { ty' <- zonkTcTypeToType emptyZonkEnv ty
; return (Just (GenericDM (loc, ty'))) }
zonkTvSkolemising :: UnboundTyVarZonker
-- This variant is used for the LHS of rules
......
......@@ -68,8 +68,8 @@ import TcValidity
import TcUnify
import TcIface
import TcSimplify
import TcHsSyn
import TcType
import TcHsSyn( zonkSigType )
import Inst ( tcInstTyBinders, tcInstTyBinder )
import TyCoRep( TyBinder(..) ) -- Used in tcDataKindSig
import Type
......@@ -82,7 +82,6 @@ import ConLike
import DataCon
import Class
import Name
import NameEnv
import NameSet
import VarEnv
import TysWiredIn
......@@ -114,13 +113,6 @@ to do this on un-desugared types. Luckily, desugared types are close enough
to HsTypes to make the error messages sane.
During type-checking, we perform as little validity checking as possible.
This is because some type-checking is done in a mutually-recursive knot, and
if we look too closely at the tycons, we'll loop. This is why we always must
use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon.
The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType
will repair this for us. Note that zonkTcType *is* safe within a knot, and
can be done repeatedly with no ill effect: it just squeezes out metavariables.
Generally, after type-checking, you will want to do validity checking, say
with TcValidity.checkValidType.
......@@ -139,20 +131,12 @@ but not all:
- Similarly, also a GHC extension, we look through synonyms before complaining
about the form of a class or instance declaration
- Ambiguity checks involve functional dependencies, and it's easier to wait
until knots have been resolved before poking into them
- Ambiguity checks involve functional dependencies
Also, in a mutually recursive group of types, we can't look at the TyCon until we've
finished building the loop. So to keep things simple, we postpone most validity
checking until step (3).
Knot tying
~~~~~~~~~~
During step (1) we might fault in a TyCon defined in another module, and it might
(via a loop) refer back to a TyCon defined in this module. So when we tie a big
knot around type declarations with ARecThing, so that the fault-in code can get
the TyCon being defined.
%************************************************************************
%* *
Check types AND do validity checking
......@@ -202,8 +186,7 @@ kcHsSigType skol_info names (HsIB { hsib_body = hs_ty
kcHsSigType _ _ (XHsImplicitBndrs _) = panic "kcHsSigType"
tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
-- Does not do validity checking; this must be done outside
-- the recursive class declaration "knot"
-- Does not do validity checking
tcClassSigType skol_info names sig_ty
= addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
tc_hs_sig_type_and_gen skol_info sig_ty liftedTypeKind
......@@ -224,7 +207,7 @@ tcHsSigType ctxt sig_ty
-- Generalise here: see Note [Kind generalisation]
; do_kind_gen <- decideKindGeneralisationPlan sig_ty
; ty <- if do_kind_gen
then tc_hs_sig_type_and_gen skol_info sig_ty kind
then tc_hs_sig_type_and_gen skol_info sig_ty kind >>= zonkTcType
else tc_hs_sig_type skol_info sig_ty kind
; checkValidType ctxt ty
......@@ -238,7 +221,7 @@ tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
-- solve equalities,
-- and then kind-generalizes.
-- This will never emit constraints, as it uses solveEqualities interally.
-- No validity checking, but it does zonk en route to generalization
-- No validity checking or zonking
tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
= HsIBRn { hsib_vars = sig_vars }
, hsib_body = hs_ty }) kind
......@@ -249,11 +232,9 @@ tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
-- kind variables floating about, immediately prior to
-- kind generalisation
-- We use the "InKnot" zonker, because this is called
-- on class method sigs in the knot
; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
; ty1 <- zonkPromoteType $ mkSpecForAllTys tkvs ty
; kvs <- kindGeneralize ty1
; zonkSigType (mkInvForAllTys kvs ty1) }
; return (mkInvForAllTys kvs ty1) }
tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
......@@ -280,6 +261,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
-- E.g. class C (a::*) (b::k->k)
-- data T a b = ... deriving( C Int )
-- returns ([k], C, [k, Int], [k->k])
-- Return values are fully zonked
tcHsDeriv hs_ty
= do { cls_kind <- newMetaKindVar
-- always safe to kind-generalize, because there
......@@ -287,7 +269,8 @@ tcHsDeriv hs_ty
; ty <- checkNoErrs $
-- avoid redundant error report with "illegal deriving", below
tc_hs_sig_type_and_gen (SigTypeSkol DerivClauseCtxt) hs_ty cls_kind
; cls_kind <- zonkTcType cls_kind
; cls_kind <- zonkTcTypeToType emptyZonkEnv cls_kind
; ty <- zonkTcTypeToType emptyZonkEnv ty
; let (tvs, pred) = splitForAllTys ty
; let (args, _) = splitFunTys cls_kind
; case getClassPredTys_maybe pred of
......@@ -330,6 +313,7 @@ tcDerivStrategy user_ctxt mds thing_inside
cls_kind <- newMetaKindVar
ty' <- checkNoErrs $
tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) ty cls_kind
ty' <- zonkTcTypeToType emptyZonkEnv ty'
let (via_tvs, via_pred) = splitForAllTys ty'
tcExtendTyVarEnv via_tvs $ do
(thing_tvs, thing) <- thing_inside
......@@ -347,6 +331,7 @@ tcHsClsInstType :: UserTypeCtxt -- InstDeclCtxt or SpecInstCtxt
tcHsClsInstType user_ctxt hs_inst_ty
= setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
; inst_ty <- zonkTcTypeToType emptyZonkEnv inst_ty
; checkValidInstance user_ctxt hs_inst_ty inst_ty }
----------------------------------------------
......@@ -920,7 +905,7 @@ bigConstraintTuple arity
tcInferApps :: TcTyMode
-> Maybe (VarEnv Kind) -- ^ Possibly, kind info (see above)
-> LHsType GhcRn -- ^ Function (for printing only)
-> TcType -- ^ Function (could be knot-tied)
-> TcType -- ^ Function
-> TcKind -- ^ Function kind (zonked)
-> [LHsType GhcRn] -- ^ Args
-> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
......@@ -943,7 +928,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
go :: Int -- the # of the next argument
-> [TcType] -- already type-checked args, in reverse order
-> TCvSubst -- instantiating substitution
-> TcType -- function applied to some args, could be knot-tied
-> TcType -- function applied to some args
-> [TyBinder] -- binders in function kind (both vis. and invis.)
-> TcKind -- function kind body (not a Pi-type)
-> [LHsType GhcRn] -- un-type-checked args
......@@ -975,8 +960,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
-- nakedSubstTy: see Note [The well-kinded type invariant]
; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
tc_lhs_type mode arg exp_kind
; traceTc "tcInferApps (vis 1)" (vcat [ ppr exp_kind
, ppr (typeKind arg') ])
; traceTc "tcInferApps (vis 1)" (ppr exp_kind)
; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
; go (n+1) (arg' : acc_args) subst'
(mkNakedAppTy fun arg') -- See Note [The well-kinded type invariant]
......@@ -1004,7 +988,6 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
zapped_subst = zapTCvSubst subst
hs_ty = mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args)
-- | Applies a type to a list of arguments.
-- Always consumes all the arguments, using 'matchExpectedFunKind' as
-- necessary. If you wish to apply a type to a list of HsTypes, this is
......@@ -1012,14 +995,14 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
-- Used for type-checking types only.
tcTyApps :: TcTyMode
-> LHsType GhcRn -- ^ Function (for printing only)
-> TcType -- ^ Function (could be knot-tied)
-> TcType -- ^ Function
-> TcKind -- ^ Function kind (zonked)
-> [LHsType GhcRn] -- ^ Args
-> TcM (TcType, TcKind) -- ^ (f args, result kind) result kind is zonked
-- Precondition: see precondition for tcInferApps
tcTyApps mode orig_hs_ty fun_ty fun_ki args
= do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
; return (ty' `mkNakedCastTy` mkRepReflCo ki', ki') }
; return (ty' `mkNakedCastTy` mkNomReflCo ki', ki') }
-- The mkNakedCastTy is for (IT3) of Note [The tcType invariant]
--------------------------
......@@ -1027,7 +1010,7 @@ tcTyApps mode orig_hs_ty fun_ty fun_ki args
-- Obeys Note [The tcType invariant]
checkExpectedKind :: HasDebugCallStack
=> HsType GhcRn -- type we're checking (for printing)
-> TcType -- type we're checking (might be knot-tied)
-> TcType -- type we're checking
-> TcKind -- the known kind of that type
-> TcKind -- the expected kind
-> TcM TcType
......@@ -1158,13 +1141,11 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
(isTypeLevel (mode_level mode))
(promotionErr name TyConPE)
; check_tc tc_tc
; tc <- get_loopy_tc name tc_tc
; handle_tyfams tc tc_tc }
-- mkNakedTyConApp: see Note [Type-checking inside the knot]
; handle_tyfams tc_tc }
AGlobal (ATyCon tc)
-> do { check_tc tc
; handle_tyfams tc tc }
; handle_tyfams tc }
AGlobal (AConLike (RealDataCon dc))
-> do { data_kinds <- xoptM LangExt.DataKinds
......@@ -1179,7 +1160,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
ConstrainedDataConPE pred
Nothing -> pure ()
; let tc = promoteDataCon dc
; return (mkNakedTyConApp tc [], tyConKind tc) }
; return (mkTyConApp tc [], tyConKind tc) }
APromotionErr err -> promotionErr name err
......@@ -1194,51 +1175,35 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
-- 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)
-> TcTyCon -- a non-loopy version of the tycon
handle_tyfams :: TyCon -- the tycon to instantiate
-> TcM (TcType, TcKind)
handle_tyfams tc tc_tc
| mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
handle_tyfams tc
| mightBeUnsaturatedTyCon tc || mode_unsat mode
-- This is where mode_unsat is used
= do { tc_kind <- zonkTcType (tyConKind tc_tc) -- (IT6) of Note [The tcType invariant]
; traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
; return (mkNakedTyConApp tc [] `mkNakedCastTy` mkRepReflCo tc_kind, tc_kind) }
= do { tc_kind <- zonkTcType (tyConKind tc) -- (IT6) of Note [The tcType invariant]
; traceTc "tcTyVar2a" (ppr tc $$ ppr tc_kind)
; return (mkTyConApp tc [] `mkNakedCastTy` mkNomReflCo tc_kind, tc_kind) }
-- the mkNakedCastTy ensures (IT5) of Note [The tcType invariant]
| otherwise
= do { tc_kind <- zonkTcType (tyConKind tc_tc)
= do { tc_kind <- zonkTcType (tyConKind tc)
; let (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
; (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
; (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc))
tc_kind_bndrs tc_inner_ki
; let is_saturated = tc_args `lengthAtLeast` tyConArity tc_tc
; let is_saturated = tc_args `lengthAtLeast` tyConArity tc
tc_ty
| is_saturated = mkNakedTyConApp tc tc_args `mkNakedCastTy` mkRepReflCo kind
| is_saturated = mkTyConApp tc tc_args `mkNakedCastTy` mkNomReflCo kind
-- mkNakedCastTy is for (IT5) of Note [The tcType invariant]
| otherwise = mkNakedTyConApp tc tc_args
| otherwise = mkTyConApp tc tc_args
-- if the tycon isn't yet saturated, then we don't want mkNakedCastTy,
-- because that means we'll have an unsaturated type family
-- We don't need it anyway, because we can be sure that the
-- type family kind will accept further arguments (because it is
-- not yet saturated)
-- tc and tc_ty must not be traced here, because that would
-- force the evaluation of a potentially knot-tied variable (tc),
-- and the typechecker would hang, as per #11708
; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
; traceTc "tcTyVar2b" (vcat [ ppr tc <+> dcolon <+> ppr tc_kind
, ppr kind ])
; return (tc_ty, kind) }
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
-- but we still want to return a TyCon of some sort to use in
-- error messages
get_loopy_tc name tc_tc
= do { env <- getGblEnv
; case lookupNameEnv (tcg_type_env env) name of
Just (ATyCon tc) -> return tc
_ -> do { traceTc "lk1 (loopy)" (ppr name)
; return tc_tc } }
-- We cannot promote a data constructor with a context that contains
-- constraints other than equalities, so error if we find one.
-- See Note [Constraints handled in types] in Inst.
......@@ -1252,34 +1217,6 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
| otherwise = True
{-
Note [Type-checking inside the knot]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we are checking the argument types of a data constructor. We
must zonk the types before making the DataCon, because once built we
can't change it. So we must traverse the type.
BUT the parent TyCon is knot-tied, so we can't look at it yet.
So we must be careful not to use "smart constructors" for types that
look at the TyCon or Class involved.
* Hence the use of mkNakedXXX functions. These do *not* enforce
the invariants (for example that we use (FunTy s t) rather
than (TyConApp (->) [s,t])).
* The zonking functions establish invariants (even zonkTcType, a change from
previous behaviour). So we must never inspect the result of a
zonk that might mention a knot-tied TyCon. This is generally OK
because we zonk *kinds* while kind-checking types. And the TyCons
in kinds shouldn't be knot-tied, because they come from a previous
mutually recursive group.
* TcHsSyn.zonkTcTypeToType also can safely check/establish
invariants.
This is horribly delicate. I hate it. A good example of how
delicate it is can be seen in Trac #7903.
Note [GADT kind self-reference]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -2671,7 +2608,8 @@ zonkPromoteMapper = TyCoMapper { tcm_smart = True
, tcm_tyvar = const zonkPromoteTcTyVar
, tcm_covar = const covar
, tcm_hole = const hole
, tcm_tybinder = const tybinder }
, tcm_tybinder = const tybinder
, tcm_tycon = return }
where
covar cv
= mkCoVarCo <$> zonkPromoteTyCoVarKind cv
......@@ -2727,11 +2665,6 @@ zonkPromoteTyCoVarBndr tv
zonkPromoteCoercion :: Coercion -> TcM Coercion
zonkPromoteCoercion = mapCoercion zonkPromoteMapper ()
zonkPromoteTypeInKnot :: TcType -> TcM TcType
zonkPromoteTypeInKnot = mapType (zonkPromoteMapper { tcm_smart = False }) ()
-- NB: Just changing smart to False will still use the smart zonker (not suitable
-- for in-the-knot) for kinds. But that's OK, because kinds aren't knot-tied.
{-
************************************************************************
* *
......
......@@ -74,7 +74,6 @@ module TcMType (
zonkTcTyCoVarBndr, zonkTcTyVarBinder,
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind, zonkTcTypeMapper,
zonkTcTypeInKnot,
zonkEvVar, zonkWC, zonkSimples,
zonkId, zonkCoVar,
......@@ -306,8 +305,7 @@ unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
-- | Check that a coercion is appropriate for filling a hole. (The hole
-- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
-- as it's used in TcHsSyn in the presence of knots.
-- itself is needed only for printing.
-- Always returns the checked coercion, but this return value is necessary
-- so that the input coercion is forced only when the output is forced.
checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
......@@ -1317,11 +1315,6 @@ tcGetGlobalTyCoVars
; writeMutVar gtv_var gbl_tvs'
; return gbl_tvs' }
-- | Zonk a type without using the smart constructors; the result type
-- is available for inspection within the type-checking knot.
zonkTcTypeInKnot :: TcType -> TcM TcType
zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
-- Zonk a type and take its free variables
-- With kind polymorphism it can be essential to zonk *first*
......@@ -1329,20 +1322,17 @@ zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
-- forall k1. forall (a:k2). a
-- where k2:=k1 is in the substitution. We don't want
-- k2 to look free in this type!
-- NB: This might be called from within the knot, so don't use
-- smart constructors. See Note [Type-checking inside the knot] in TcHsType
zonkTcTypeAndFV ty
= tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
= tyCoVarsOfTypeDSet <$> zonkTcType ty
-- | Zonk a type and call 'candidateQTyVarsOfType' on it.
-- Works within the knot.
zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
zonkTcTypeAndSplitDepVars ty
= candidateQTyVarsOfType <$> zonkTcTypeInKnot ty
= candidateQTyVarsOfType <$> zonkTcType ty
zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
zonkTcTypesAndSplitDepVars tys
= candidateQTyVarsOfTypes <$> mapM zonkTcTypeInKnot tys
= candidateQTyVarsOfTypes <$> mapM zonkTcType tys
zonkTyCoVar :: TyCoVar -> TcM TcType
-- Works on TyVars and TcTyVars
......@@ -1527,7 +1517,7 @@ zonkId id
zonkCoVar :: CoVar -> TcM CoVar
zonkCoVar = zonkId
-- | A suitable TyCoMapper for zonking a type inside the knot, and
-- | A suitable TyCoMapper for zonking a type during type-checking,
-- before all metavars are filled in.
zonkTcTypeMapper :: TyCoMapper () TcM
zonkTcTypeMapper = TyCoMapper
......@@ -1535,7 +1525,8 @@ zonkTcTypeMapper = TyCoMapper
, tcm_tyvar = const zonkTcTyVar
, tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
, tcm_hole = hole
, tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
, tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv