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

Make a smart mkAppTyM

This patch finally delivers on Trac #15952.  Specifically

* Completely remove Note [The tcType invariant], along with
  its complicated consequences (IT1-IT6).

* Replace Note [The well-kinded type invariant] with:

      Note [The Purely Kinded Type Invariant (PKTI)]

* Instead, establish the (PKTI) in TcHsType.tcInferApps,
  by using a new function mkAppTyM when building a type
  application.  See Note [mkAppTyM].

* As a result we can remove the delicate mkNakedXX functions
  entirely.  Specifically, mkNakedCastTy retained lots of
  extremly delicate Refl coercions which just cluttered
  everything up, and(worse) were very vulnerable to being
  silently eliminated by (say) substTy. This led to a
  succession of bug reports.

The result is noticeably simpler to explain, simpler
to code, and Richard and I are much more confident that
it is correct.

It does not actually fix any bugs, but it brings us closer.
E.g. I hoped it'd fix #15918 and #15799, but it doesn't quite
do so.  However, it makes it much easier to fix.

I also did a raft of other minor refactorings:

* Use tcTypeKind consistently in the type checker

* Rename tcInstTyBinders to tcInvisibleTyBinders,
  and refactor it a bit

* Refactor tcEqType, pickyEqType, tcEqTypeVis
  Simpler, probably more efficient.

* Make zonkTcType zonk TcTyCons, at least if they have
  any free unification variables -- see zonk_tc_tycon
  in TcMType.zonkTcTypeMapper.

  Not zonking these TcTyCons was actually a bug before.

* Simplify try_to_reduce_no_cache in TcFlatten (a lot)

* Combine checkExpectedKind and checkExpectedKindX.
  And then combine the invisible-binder instantation code
  Much simpler now.

* Fix a little bug in TcMType.skolemiseQuantifiedTyVar.
  I'm not sure how I came across this originally.

* Fix a little bug in TyCoRep.isUnliftedRuntimeRep
  (the ASSERT was over-zealous).  Again I'm not certain
  how I encountered this.

* Add a missing solveLocalEqualities in
  TcHsType.tcHsPartialSigType.
  I came across this when trying to get level numbers
  right.
parent 19626218
...@@ -57,8 +57,7 @@ module HsTypes ( ...@@ -57,8 +57,7 @@ module HsTypes (
splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe, splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
splitLHsPatSynTy, splitLHsPatSynTy,
splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy, splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy,
splitHsFunType, splitHsFunType, hsTyGetAppHead_maybe,
splitHsAppTys, hsTyGetAppHead_maybe,
mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy, mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
ignoreParens, hsSigType, hsSigWcType, ignoreParens, hsSigType, hsSigWcType,
hsLTyVarBndrToType, hsLTyVarBndrsToTypes, hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
...@@ -1137,15 +1136,6 @@ The SrcSpan is the span of the original HsPar ...@@ -1137,15 +1136,6 @@ The SrcSpan is the span of the original HsPar
-} -}
splitHsAppTys :: HsType GhcRn -> (LHsType GhcRn, [LHsTypeArg GhcRn])
splitHsAppTys e = go (noLoc e) []
where
go :: LHsType GhcRn -> [LHsTypeArg GhcRn]
-> (LHsType GhcRn, [LHsTypeArg GhcRn])
go (L _ (HsAppTy _ f a)) as = go f (HsValArg a : as)
go (L _ (HsAppKindTy l ty k)) as = go ty (HsTypeArg l k : as)
go (L sp (HsParTy _ f)) as = go f (HsArgPar sp : as)
go f as = (f,as)
-------------------------------- --------------------------------
splitLHsPatSynTy :: LHsType pass splitLHsPatSynTy :: LHsType pass
-> ( [LHsTyVarBndr pass] -- universals -> ( [LHsTyVarBndr pass] -- universals
......
...@@ -667,7 +667,7 @@ typeToLHsType ty ...@@ -667,7 +667,7 @@ typeToLHsType ty
| tyConAppNeedsKindSig True tc (length args) | tyConAppNeedsKindSig True tc (length args)
-- We must produce an explicit kind signature here to make certain -- We must produce an explicit kind signature here to make certain
-- programs kind-check. See Note [Kind signatures in typeToLHsType]. -- programs kind-check. See Note [Kind signatures in typeToLHsType].
= nlHsParTy $ noLoc $ HsKindSig NoExt lhs_ty (go (typeKind ty)) = nlHsParTy $ noLoc $ HsKindSig NoExt lhs_ty (go (tcTypeKind ty))
| otherwise = lhs_ty | otherwise = lhs_ty
where where
arg_flags :: [ArgFlag] arg_flags :: [ArgFlag]
......
...@@ -313,7 +313,7 @@ import NameSet ...@@ -313,7 +313,7 @@ import NameSet
import RdrName import RdrName
import HsSyn import HsSyn
import Type hiding( typeKind ) import Type hiding( typeKind )
import TcType hiding( typeKind ) import TcType
import Id import Id
import TysPrim ( alphaTyVars ) import TysPrim ( alphaTyVars )
import TyCon import TyCon
......
...@@ -60,7 +60,7 @@ import CoreFVs ( orphNamesOfFamInst ) ...@@ -60,7 +60,7 @@ import CoreFVs ( orphNamesOfFamInst )
import TyCon import TyCon
import Type hiding( typeKind ) import Type hiding( typeKind )
import RepType import RepType
import TcType hiding( typeKind ) import TcType
import Var import Var
import Id import Id
import Name hiding ( varName ) import Name hiding ( varName )
......
...@@ -15,7 +15,7 @@ module Inst ( ...@@ -15,7 +15,7 @@ module Inst (
instCall, instDFunType, instStupidTheta, instTyVarsWith, instCall, instDFunType, instStupidTheta, instTyVarsWith,
newWanted, newWanteds, newWanted, newWanteds,
tcInstTyBinders, tcInstTyBinder, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
newOverloadedLit, mkOverLit, newOverloadedLit, mkOverLit,
...@@ -484,43 +484,34 @@ no longer cut it, but it seems fine for now. ...@@ -484,43 +484,34 @@ no longer cut it, but it seems fine for now.
-} -}
--------------------------- ---------------------------
-- | Instantantiate the TyConBinders of a forall type, -- | Instantiates up to n invisible binders
-- given its decomposed form (tvs, ty) -- Returns the instantiating types, and body kind
tcInstTyBinders :: HasDebugCallStack tcInstInvisibleTyBinders :: Int -> TcKind -> TcM ([TcType], TcKind)
=> ([TyCoBinder], TcKind) -- ^ The type (forall bs. ty)
-> TcM ([TcType], TcKind) -- ^ Instantiated bs, substituted ty tcInstInvisibleTyBinders 0 kind
-- Takes a pair because that is what splitPiTysInvisible returns = return ([], kind)
-- See also Note [Bidirectional type checking] tcInstInvisibleTyBinders n ty
tcInstTyBinders (bndrs, ty) = go n empty_subst ty
| null bndrs -- It's fine for bndrs to be empty e.g.
= return ([], ty) -- Check that (Maybe :: forall {k}. k->*),
-- and see the call to instTyBinders in checkExpectedKind
-- A user bug to be reported as such; it is not a compiler crash!
| otherwise
= do { (subst, args) <- mapAccumLM (tcInstTyBinder Nothing) empty_subst bndrs
; ty' <- zonkTcType (substTy subst ty)
-- Why zonk the result? So that tcTyVar can
-- obey (IT6) of Note [The tcType invariant] in TcHsType
-- ToDo: SLPJ: I don't think this is needed
; return (args, ty') }
where where
empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty)) empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
go n subst kind
| n > 0
, Just (bndr, body) <- tcSplitPiTy_maybe kind
, isInvisibleBinder bndr
= do { (subst', arg) <- tcInstInvisibleTyBinder subst bndr
; (args, inner_ty) <- go (n-1) subst' body
; return (arg:args, inner_ty) }
| otherwise
= return ([], substTy subst kind)
-- | Used only in *types* -- | Used only in *types*
tcInstTyBinder :: Maybe (VarEnv Kind) tcInstInvisibleTyBinder :: TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
-> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType) tcInstInvisibleTyBinder subst (Named (Bndr tv _))
tcInstTyBinder mb_kind_info subst (Named (Bndr tv _)) = do { (subst', tv') <- newMetaTyVarX subst tv
= case lookup_tv tv of ; return (subst', mkTyVarTy tv') }
Just ki -> return (extendTvSubstAndInScope subst tv ki, ki)
Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
; return (subst', mkTyVarTy tv') }
where
lookup_tv tv = do { env <- mb_kind_info -- `Maybe` monad
; lookupVarEnv env tv }
tcInstTyBinder _ subst (Anon ty) tcInstInvisibleTyBinder subst (Anon ty)
-- This is the *only* constraint currently handled in types. -- This is the *only* constraint currently handled in types.
| Just (mk, k1, k2) <- get_eq_tys_maybe substed_ty | Just (mk, k1, k2) <- get_eq_tys_maybe substed_ty
= do { co <- unifyKind Nothing k1 k2 = do { co <- unifyKind Nothing k1 k2
......
...@@ -873,9 +873,9 @@ can_eq_nc' ...@@ -873,9 +873,9 @@ can_eq_nc'
-> TcS (StopOrContinue Ct) -> TcS (StopOrContinue Ct)
-- Expand synonyms first; see Note [Type synonyms and canonicalization] -- Expand synonyms first; see Note [Type synonyms and canonicalization]
can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 can_eq_nc' flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
| Just ty1' <- tcView ty1 = can_eq_nc flat ev eq_rel ty1' ps_ty1 ty2 ps_ty2 | Just ty1' <- tcView ty1 = can_eq_nc' flat rdr_env envs ev eq_rel ty1' ps_ty1 ty2 ps_ty2
| Just ty2' <- tcView ty2 = can_eq_nc flat ev eq_rel ty1 ps_ty1 ty2' ps_ty2 | Just ty2' <- tcView ty2 = can_eq_nc' flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
-- need to check for reflexivity in the ReprEq case. -- need to check for reflexivity in the ReprEq case.
-- See Note [Eager reflexivity check] -- See Note [Eager reflexivity check]
...@@ -1048,7 +1048,7 @@ can_eq_nc_forall ev eq_rel s1 s2 ...@@ -1048,7 +1048,7 @@ can_eq_nc_forall ev eq_rel s1 s2
-- | Compare types for equality, while zonking as necessary. Gives up -- | Compare types for equality, while zonking as necessary. Gives up
-- as soon as it finds that two types are not equal. -- as soon as it finds that two types are not equal.
-- This is quite handy when some unification has made two -- This is quite handy when some unification has made two
-- types in an inert wanted to be equal. We can discover the equality without -- types in an inert Wanted to be equal. We can discover the equality without
-- flattening, which is sometimes very expensive (in the case of type functions). -- flattening, which is sometimes very expensive (in the case of type functions).
-- In particular, this function makes a ~20% improvement in test case -- In particular, this function makes a ~20% improvement in test case
-- perf/compiler/T5030. -- perf/compiler/T5030.
...@@ -1836,10 +1836,11 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 ...@@ -1836,10 +1836,11 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
| k1 `tcEqType` k2 | k1 `tcEqType` k2
= canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 = canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
-- Note [Flattening] in TcFlatten gives us (F2), which says that -- So the LHS and RHS don't have equal kinds
-- flattening is always homogeneous (doesn't change kinds). But -- Note [Flattening] in TcFlatten gives us (F2), which says that
-- perhaps by flattening the kinds of the two sides of the equality -- flattening is always homogeneous (doesn't change kinds). But
-- at hand makes them equal. So let's try that. -- perhaps by flattening the kinds of the two sides of the equality
-- at hand makes them equal. So let's try that.
| otherwise | otherwise
= do { (flat_k1, k1_co) <- flattenKind loc flav k1 -- k1_co :: flat_k1 ~N kind(xi1) = do { (flat_k1, k1_co) <- flattenKind loc flav k1 -- k1_co :: flat_k1 ~N kind(xi1)
; (flat_k2, k2_co) <- flattenKind loc flav k2 -- k2_co :: flat_k2 ~N kind(xi2) ; (flat_k2, k2_co) <- flattenKind loc flav k2 -- k2_co :: flat_k2 ~N kind(xi2)
...@@ -1852,7 +1853,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2 ...@@ -1852,7 +1853,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
, ppr flat_k2 , ppr flat_k2
, ppr k2_co ]) , ppr k2_co ])
-- we know the LHS is a tyvar. So let's dump all the coercions on the RHS -- We know the LHS is a tyvar. So let's dump all the coercions on the RHS
-- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and
-- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence -- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence
-- (as an optimization, so that we don't have to flatten the kinds again) -- (as an optimization, so that we don't have to flatten the kinds again)
...@@ -1934,7 +1935,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2 ...@@ -1934,7 +1935,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
-- See Note [Equalities with incompatible kinds] -- See Note [Equalities with incompatible kinds]
| otherwise -- Wanted and Derived | otherwise -- Wanted and Derived
-- NB: all kind equalities are Nominal -- NB: all kind equalities are Nominal
= do { emitNewDerivedEq kind_loc Nominal ki1 ki2 = do { emitNewDerivedEq kind_loc Nominal ki1 ki2
-- kind_ev :: (ki1 :: *) ~ (ki2 :: *) -- kind_ev :: (ki1 :: *) ~ (ki2 :: *)
; traceTcS "Hetero equality gives rise to derived kind equality" $ ; traceTcS "Hetero equality gives rise to derived kind equality" $
......
...@@ -1975,17 +1975,16 @@ misMatchMsg ct oriented ty1 ty2 ...@@ -1975,17 +1975,16 @@ misMatchMsg ct oriented ty1 ty2
-- themselves. -- themselves.
pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
-> SDoc -> SDoc -> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch ty1 ty2 ct = pprWithExplicitKindsWhenMismatch ty1 ty2 ct
pprWithExplicitKindsWhen mismatch = pprWithExplicitKindsWhen show_kinds
where where
(act_ty, exp_ty) = case ct of (act_ty, exp_ty) = case ct of
TypeEqOrigin { uo_actual = act TypeEqOrigin { uo_actual = act
, uo_expected = exp } -> (act, exp) , uo_expected = exp } -> (act, exp)
_ -> (ty1, ty2) _ -> (ty1, ty2)
mismatch | Just vis <- tcEqTypeVis act_ty exp_ty show_kinds = tcEqTypeVis act_ty exp_ty
= not vis -- True when the visible bit of the types look the same,
| otherwise -- so we want to show the kinds in the displayed type
= False
mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
-> (Bool, Maybe SwapFlag, SDoc) -> (Bool, Maybe SwapFlag, SDoc)
......
...@@ -1329,8 +1329,7 @@ flatten_exact_fam_app_fully tc tys ...@@ -1329,8 +1329,7 @@ flatten_exact_fam_app_fully tc tys
-- See Note [Reduce type family applications eagerly] -- See Note [Reduce type family applications eagerly]
-- the following tcTypeKind should never be evaluated, as it's just used in -- the following tcTypeKind should never be evaluated, as it's just used in
-- casting, and casts by refl are dropped -- casting, and casts by refl are dropped
= do { let reduce_co = mkNomReflCo (tcTypeKind (mkTyConApp tc tys)) = do { mOut <- try_to_reduce_nocache tc tys
; mOut <- try_to_reduce_nocache tc tys reduce_co id
; case mOut of ; case mOut of
Just out -> pure out Just out -> pure out
Nothing -> do Nothing -> do
...@@ -1452,16 +1451,8 @@ flatten_exact_fam_app_fully tc tys ...@@ -1452,16 +1451,8 @@ flatten_exact_fam_app_fully tc tys
try_to_reduce_nocache :: TyCon -- F, family tycon try_to_reduce_nocache :: TyCon -- F, family tycon
-> [Type] -- args, not necessarily flattened -> [Type] -- args, not necessarily flattened
-> CoercionN -- kind_co :: tcTypeKind(F args)
-- ~N tcTypeKind(F orig_args)
-- where
-- orig_args is what was passed to the
-- outer function
-> ( Coercion -- :: (xi |> kind_co) ~ F args
-> Coercion ) -- what to return from outer
-- function
-> FlatM (Maybe (Xi, Coercion)) -> FlatM (Maybe (Xi, Coercion))
try_to_reduce_nocache tc tys kind_co update_co try_to_reduce_nocache tc tys
= do { checkStackDepth (mkTyConApp tc tys) = do { checkStackDepth (mkTyConApp tc tys)
; mb_match <- liftTcS $ matchFam tc tys ; mb_match <- liftTcS $ matchFam tc tys
; case mb_match of ; case mb_match of
...@@ -1470,13 +1461,9 @@ flatten_exact_fam_app_fully tc tys ...@@ -1470,13 +1461,9 @@ flatten_exact_fam_app_fully tc tys
Just (norm_co, norm_ty) Just (norm_co, norm_ty)
-> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty -> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty
; eq_rel <- getEqRel ; eq_rel <- getEqRel
; let co = maybeSubCo eq_rel norm_co ; let co = mkSymCo (maybeSubCo eq_rel norm_co
`mkTransCo` mkSymCo final_co `mkTransCo` mkSymCo final_co)
role = eqRelRole eq_rel ; return $ Just (xi, co) }
xi' = xi `mkCastTy` kind_co
co' = update_co $
mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
; return $ Just (xi', co') }
Nothing -> pure Nothing } Nothing -> pure Nothing }
{- Note [Reduce type family applications eagerly] {- Note [Reduce type family applications eagerly]
......
...@@ -204,6 +204,7 @@ data ZonkEnv -- See Note [The ZonkEnv] ...@@ -204,6 +204,7 @@ data ZonkEnv -- See Note [The ZonkEnv]
, ze_tv_env :: TyCoVarEnv TyCoVar , ze_tv_env :: TyCoVarEnv TyCoVar
, ze_id_env :: IdEnv Id , ze_id_env :: IdEnv Id
, ze_meta_tv_env :: TcRef (TyVarEnv Type) } , ze_meta_tv_env :: TcRef (TyVarEnv Type) }
{- Note [The ZonkEnv] {- Note [The ZonkEnv]
~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~
* ze_flexi :: ZonkFlexi says what to do with a * ze_flexi :: ZonkFlexi says what to do with a
......
...@@ -46,7 +46,7 @@ module TcHsType ( ...@@ -46,7 +46,7 @@ module TcHsType (
typeLevelMode, kindLevelMode, typeLevelMode, kindLevelMode,
kindGeneralize, checkExpectedKind, RequireSaturation(..), kindGeneralize, checkExpectedKind_pp,
reportFloatingKvs, reportFloatingKvs,
-- Sort-checking kinds -- Sort-checking kinds
...@@ -76,9 +76,10 @@ import TcUnify ...@@ -76,9 +76,10 @@ import TcUnify
import TcIface import TcIface
import TcSimplify import TcSimplify
import TcHsSyn import TcHsSyn
import TyCoRep ( Type(..) )
import TcErrors ( reportAllUnsolved ) import TcErrors ( reportAllUnsolved )
import TcType import TcType
import Inst ( tcInstTyBinders, tcInstTyBinder ) import Inst ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
import TyCoRep( TyCoBinder(..), tyCoBinderArgFlag ) -- Used in etaExpandAlgTyCon import TyCoRep( TyCoBinder(..), tyCoBinderArgFlag ) -- Used in etaExpandAlgTyCon
import Type import Type
import TysPrim import TysPrim
...@@ -251,7 +252,7 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind ...@@ -251,7 +252,7 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
; return (mkInvForAllTys kvs ty1) } ; return (mkInvForAllTys kvs ty1) }
tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen" tc_hs_sig_type _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type"
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
-- tcTopLHsType is used for kind-checking top-level HsType where -- tcTopLHsType is used for kind-checking top-level HsType where
...@@ -291,7 +292,7 @@ tcHsDeriv hs_ty ...@@ -291,7 +292,7 @@ tcHsDeriv hs_ty
-- with "illegal deriving", below -- with "illegal deriving", below
tcTopLHsType hs_ty AnyKind tcTopLHsType hs_ty AnyKind
; let (tvs, pred) = splitForAllTys ty ; let (tvs, pred) = splitForAllTys ty
(kind_args, _) = splitFunTys (typeKind pred) (kind_args, _) = splitFunTys (tcTypeKind pred)
; case getClassPredTys_maybe pred of ; case getClassPredTys_maybe pred of
Just (cls, tys) -> return (tvs, (cls, tys, kind_args)) Just (cls, tys) -> return (tvs, (cls, tys, kind_args))
Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) } Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
...@@ -402,8 +403,6 @@ and Note [The wildcard story for types] in HsTypes.hs ...@@ -402,8 +403,6 @@ and Note [The wildcard story for types] in HsTypes.hs
The main kind checker: no validity checks here The main kind checker: no validity checks here
* * * *
************************************************************************ ************************************************************************
First a couple of simple wrappers for kcHsType
-} -}
--------------------------- ---------------------------
...@@ -431,11 +430,43 @@ tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty) ...@@ -431,11 +430,43 @@ tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty)
-- Like tcLHsType, but use it in a context where type synonyms and type families -- Like tcLHsType, but use it in a context where type synonyms and type families
-- do not need to be saturated, like in a GHCi :kind call -- do not need to be saturated, like in a GHCi :kind call
tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind) tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcLHsTypeUnsaturated ty = addTypeCtxt ty (tc_infer_lhs_type mode ty) tcLHsTypeUnsaturated hs_ty
| Just (hs_fun_ty, hs_args) <- splitHsAppTys (unLoc hs_ty)
= addTypeCtxt hs_ty $
do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
; tcInferApps_nosat mode hs_fun_ty fun_ty hs_args }
-- Notice the 'nosat'; do not instantiate trailing
-- invisible arguments of a type family.
-- See Note [Dealing with :kind]
| otherwise
= addTypeCtxt hs_ty $
tc_infer_lhs_type mode hs_ty
where where
mode = allowUnsaturated typeLevelMode mode = typeLevelMode
{- Note [Dealing with :kind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this GHCi command
ghci> type family F :: Either j k
ghci> :kind F
F :: forall {j,k}. Either j k
We will only get the 'forall' if we /refrain/ from saturating those
invisible binders. But generally we /do/ saturate those invisible
binders (see tcInferApps), and we want to do so for nested application
even in GHCi. Consider for example (Trac #16287)
ghci> type family F :: k
ghci> data T :: (forall k. k) -> Type
ghci> :kind T F
We want to reject this. It's just at the very top level that we want
to switch off saturation.
So tcLHsTypeUnsaturated does a little special case for top level
applications. Actually the common case is a bare variable, as above.
{-
************************************************************************ ************************************************************************
* * * *
Type-checking modes Type-checking modes
...@@ -450,39 +481,24 @@ concern things that the renamer can't handle. ...@@ -450,39 +481,24 @@ concern things that the renamer can't handle.
-} -}
-- | Do we require type families to be saturated?
data RequireSaturation
= YesSaturation
| NoSaturation -- e.g. during a call to GHCi's :kind
-- | Info about the context in which we're checking a type. Currently, -- | Info about the context in which we're checking a type. Currently,
-- differentiates only between types and kinds, but this will likely -- differentiates only between types and kinds, but this will likely
-- grow, at least to include the distinction between patterns and -- grow, at least to include the distinction between patterns and
-- not-patterns. -- not-patterns.
data TcTyMode --
= TcTyMode { mode_level :: TypeOrKind -- To find out where the mode is used, search for 'mode_level'
, mode_sat :: RequireSaturation data TcTyMode = TcTyMode { mode_level :: TypeOrKind }
}
-- The mode_unsat field is solely so that type families/synonyms can be unsaturated
-- in GHCi :kind calls
typeLevelMode :: TcTyMode typeLevelMode :: TcTyMode
typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_sat = YesSaturation } typeLevelMode = TcTyMode { mode_level = TypeLevel }
kindLevelMode :: TcTyMode kindLevelMode :: TcTyMode
kindLevelMode = TcTyMode { mode_level = KindLevel, mode_sat = YesSaturation } kindLevelMode = TcTyMode { mode_level = KindLevel }
allowUnsaturated :: TcTyMode -> TcTyMode
allowUnsaturated mode = mode { mode_sat = NoSaturation }
-- switch to kind level -- switch to kind level
kindLevel :: TcTyMode -> TcTyMode kindLevel :: TcTyMode -> TcTyMode
kindLevel mode = mode { mode_level = KindLevel } kindLevel mode = mode { mode_level = KindLevel }
instance Outputable RequireSaturation where
ppr YesSaturation = text "YesSaturation"
ppr NoSaturation = text "NoSaturation"
instance Outputable TcTyMode where instance Outputable TcTyMode where
ppr = ppr . mode_level ppr = ppr . mode_level
...@@ -504,7 +520,7 @@ metavariable. ...@@ -504,7 +520,7 @@ metavariable.
In types, however, we're not so lucky, because *we cannot re-generalize*! In types, however, we're not so lucky, because *we cannot re-generalize*!
There is no lambda. So, we must be careful only to instantiate at the last There is no lambda. So, we must be careful only to instantiate at the last
possible moment, when we're sure we're never going to want the lost polymorphism possible moment, when we're sure we're never going to want the lost polymorphism
again. This is done in calls to tcInstTyBinders. again. This is done in calls to tcInstInvisibleTyBinders.
To implement this behavior, we use bidirectional type checking, where we To implement this behavior, we use bidirectional type checking, where we
explicitly think about whether we know the kind of the type we're checking explicitly think about whether we know the kind of the type we're checking
...@@ -531,37 +547,6 @@ But, we want to make sure that our pattern-matches are complete. So, ...@@ -531,37 +547,6 @@ But, we want to make sure that our pattern-matches are complete. So,
we have a bunch of repetitive code just so that we get warnings if we're we have a bunch of repetitive code just so that we get warnings if we're
missing any patterns. missing any patterns.
Note [The tcType invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
(IT1) If tc_ty = tc_hs_type hs_ty exp_kind
then tcTypeKind tc_ty = exp_kind
without any zonking needed. The reason for this is that in
tcInferApps we see (F ty), and we kind-check 'ty' with an
expected-kind coming from F. Then, to make the resulting application
well kinded --- see Note [The well-kinded type invariant] in TcType ---
we need the kind-checked 'ty' to have exactly the kind that F expects,
with no funny zonking nonsense in between.
The tcType invariant also applies to checkExpectedKind:
(IT2) if
(tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
then
tcTypeKind tc_ty = exp_ki
These other invariants are all necessary, too, as these functions
are used within tc_hs_type:
(IT3) If (ty, ki) <- tc_infer_hs_type ..., then tcTypeKind ty == ki.
(IT4) If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki.
(In other words, the result kind of tc_infer_hs_type is zonked.)
(IT5) If (ty, ki) <- tcTyVar ..., then tcTypeKind ty == ki.
(IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki.
(In other words, the result kind of tcTyVar is zonked.)
-} -}
------------------------------------------ ------------------------------------------
...@@ -571,23 +556,27 @@ are used within tc_hs_type: ...@@ -571,23 +556,27 @@ are used within tc_hs_type:
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind) tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
tc_infer_lhs_type mode (L span ty) tc_infer_lhs_type mode (L span ty)
= setSrcSpan span $ = setSrcSpan span $
do { (ty', kind) <- tc_infer_hs_type mode ty tc_infer_hs_type mode ty
; return (ty', kind) }
---------------------------
-- | Call 'tc_infer_hs_type' and check its result against an expected kind.
tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
tc_infer_hs_type_ek mode hs_ty ek
= do { (ty, k) <- tc_infer_hs_type mode hs_ty
; checkExpectedKind hs_ty ty k ek }
---------------------------
-- | Infer the kind of a type and desugar. This is the "up" type-checker, -- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking] -- as described in Note [Bidirectional type checking]
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind) tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
tc_infer_hs_type mode (HsParTy _ t) = tc_infer_lhs_type mode t
tc_infer_hs_type mode (HsTyVar _ _ (L _ tv)) = tcTyVar mode tv
tc_infer_hs_type mode e@(HsAppTy {}) = tcTyApp mode e tc_infer_hs_type mode (HsParTy _ t)
tc_infer_hs_type mode e@(HsAppKindTy {}) = tcTyApp mode e = tc_infer_lhs_type mode t
tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs) tc_infer_hs_type mode ty
| not (hs_op `hasKey` funTyConKey) | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
= do { (op, op_kind) <- tcTyVar mode hs_op = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind ; tcInferApps mode hs_fun_ty fun_ty hs_args }
[HsValArg lhs, HsValArg rhs] }
tc_infer_hs_type mode (HsKindSig _ ty sig) tc_infer_hs_type mode (HsKindSig _ ty sig)
= do { sig' <- tcLHsKindSig KindSigCtxt sig = do { sig' <- tcLHsKindSig KindSigCtxt sig
...@@ -610,8 +599,7 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty))) ...@@ -610,8 +599,7 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
tc_infer_hs_type _ (XHsType (NHsCoreTy ty)) tc_infer_hs_type _ (XHsType (NHsCoreTy ty))
= do { ty <- zonkTcType ty -- (IT3) and (IT4) of Note [The tcType invariant] = return (ty, tcTypeKind ty)
; return (ty, tcTypeKind ty) }
tc_infer_hs_type _ (HsExplicitListTy _ _ tys) tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
| null tys -- this is so that we can use visible kind application with '[] | null tys -- this is so that we can use visible kind application with '[]
...@@ -630,26 +618,8 @@ tc_lhs_type mode (L span ty) exp_kind ...@@ -630,26 +618,8 @@ tc_lhs_type mode (L span ty) exp_kind
= setSrcSpan span $ = setSrcSpan span $
tc_hs_type mode ty exp_kind tc_hs_type mode ty exp_kind
------------------------------------------
tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind
-> TcM TcType
tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of
TypeLevel ->
do { arg_k <- newOpenTypeKind
; res_k <- newOpenTypeKind
; ty1' <- tc_lhs_type mode ty1 arg_k
; ty2' <- tc_lhs_type mode ty2 res_k
; checkExpectedKindMode mode (ppr $ HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
liftedTypeKind exp_kind }
KindLevel -> -- no representation polymorphism in kinds. yet.
do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
; checkExpectedKindMode mode (ppr $ HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
liftedTypeKind exp_kind }
------------------------------------------ ------------------------------------------
tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
-- See Note [The tcType invariant]
-- See Note [Bidirectional type checking] -- See Note [Bidirectional type checking]
tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
...@@ -709,29 +679,30 @@ tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_ki ...@@ -709,29 +679,30 @@ tc_hs_type mode forall@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_ki
; return (mkForAllTys bndrs ty') } ; return (mkForAllTys bndrs ty') }
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
| null (unLoc ctxt) | null (unLoc ctxt)
= tc_lhs_type mode ty exp_kind = tc_lhs_type mode rn_ty exp_kind
| otherwise -- See Note [Body kind of a HsQualTy]
| tcIsConstraintKind exp_kind
= do { ctxt' <- tc_hs_context mode ctxt = do { ctxt' <- tc_hs_context mode ctxt
; ty' <- tc_lhs_type mode rn_ty constraintKind
; return (mkPhiTy ctxt' ty') }