summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2019-01-24 11:53:03 +0000
committerSimon Peyton Jones <simonpj@microsoft.com>2019-02-14 08:40:03 +0000
commit682783828275cca5fd8bf5be5b52054c75e0e22c (patch)
tree2cdde211f8e816b174edce813a7d05c7a054228d
parent19626218566ea709b5f6f287d3c296b0c4021de2 (diff)
downloadhaskell-682783828275cca5fd8bf5be5b52054c75e0e22c.tar.gz
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.
Diffstat
-rw-r--r--compiler/hsSyn/HsTypes.hs12
-rw-r--r--compiler/hsSyn/HsUtils.hs2
-rw-r--r--compiler/main/GHC.hs2
-rw-r--r--compiler/main/InteractiveEval.hs2
-rw-r--r--compiler/typecheck/Inst.hs59
-rw-r--r--compiler/typecheck/TcCanonical.hs21
-rw-r--r--compiler/typecheck/TcErrors.hs11
-rw-r--r--compiler/typecheck/TcFlatten.hs23
-rw-r--r--compiler/typecheck/TcHsSyn.hs1
-rw-r--r--compiler/typecheck/TcHsType.hs853
-rw-r--r--compiler/typecheck/TcInstDcls.hs13
-rw-r--r--compiler/typecheck/TcMType.hs41
-rw-r--r--compiler/typecheck/TcSMonad.hs4
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs53
-rw-r--r--compiler/typecheck/TcType.hs297
-rw-r--r--compiler/typecheck/TcUnify.hs50
-rw-r--r--compiler/types/Coercion.hs2
-rw-r--r--compiler/types/OptCoercion.hs2
-rw-r--r--compiler/types/TyCoRep.hs7
-rw-r--r--compiler/types/TyCon.hs47
-rw-r--r--compiler/types/Type.hs73
-rw-r--r--compiler/types/Type.hs-boot2
-rw-r--r--compiler/utils/Outputable.hs6
-rw-r--r--compiler/utils/Outputable.hs-boot3
-rw-r--r--testsuite/tests/ghci/should_fail/T16287.stderr13
25 files changed, 839 insertions, 760 deletions
diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index 5eeca6eac2..fa87613416 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -57,8 +57,7 @@ module HsTypes (
splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
splitLHsPatSynTy,
splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy,
- splitHsFunType,
- splitHsAppTys, hsTyGetAppHead_maybe,
+ splitHsFunType, hsTyGetAppHead_maybe,
mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
ignoreParens, hsSigType, hsSigWcType,
hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
@@ -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
-> ( [LHsTyVarBndr pass] -- universals
diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index 9cd3a207ad..72c70a83ab 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -667,7 +667,7 @@ typeToLHsType ty
| tyConAppNeedsKindSig True tc (length args)
-- We must produce an explicit kind signature here to make certain
-- 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
where
arg_flags :: [ArgFlag]
diff --git a/compiler/main/GHC.hs b/compiler/main/GHC.hs
index 471a558cc6..a1cc4a7cb6 100644
--- a/compiler/main/GHC.hs
+++ b/compiler/main/GHC.hs
@@ -313,7 +313,7 @@ import NameSet
import RdrName
import HsSyn
import Type hiding( typeKind )
-import TcType hiding( typeKind )
+import TcType
import Id
import TysPrim ( alphaTyVars )
import TyCon
diff --git a/compiler/main/InteractiveEval.hs b/compiler/main/InteractiveEval.hs
index 79e64b3ad9..4e6d26b1d6 100644
--- a/compiler/main/InteractiveEval.hs
+++ b/compiler/main/InteractiveEval.hs
@@ -60,7 +60,7 @@ import CoreFVs ( orphNamesOfFamInst )
import TyCon
import Type hiding( typeKind )
import RepType
-import TcType hiding( typeKind )
+import TcType
import Var
import Id
import Name hiding ( varName )
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index 284d6a95d3..d4348ec29c 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -15,7 +15,7 @@ module Inst (
instCall, instDFunType, instStupidTheta, instTyVarsWith,
newWanted, newWanteds,
- tcInstTyBinders, tcInstTyBinder,
+ tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
newOverloadedLit, mkOverLit,
@@ -484,43 +484,34 @@ no longer cut it, but it seems fine for now.
-}
---------------------------
--- | Instantantiate the TyConBinders of a forall type,
--- given its decomposed form (tvs, ty)
-tcInstTyBinders :: HasDebugCallStack
- => ([TyCoBinder], TcKind) -- ^ The type (forall bs. ty)
- -> TcM ([TcType], TcKind) -- ^ Instantiated bs, substituted ty
--- Takes a pair because that is what splitPiTysInvisible returns
--- See also Note [Bidirectional type checking]
-tcInstTyBinders (bndrs, 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') }
+-- | Instantiates up to n invisible binders
+-- Returns the instantiating types, and body kind
+tcInstInvisibleTyBinders :: Int -> TcKind -> TcM ([TcType], TcKind)
+
+tcInstInvisibleTyBinders 0 kind
+ = return ([], kind)
+tcInstInvisibleTyBinders n ty
+ = go n empty_subst ty
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*
-tcInstTyBinder :: Maybe (VarEnv Kind)
- -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
-tcInstTyBinder mb_kind_info subst (Named (Bndr tv _))
- = case lookup_tv tv of
- 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 }
-
+tcInstInvisibleTyBinder :: TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
+tcInstInvisibleTyBinder subst (Named (Bndr tv _))
+ = do { (subst', tv') <- newMetaTyVarX subst tv
+ ; return (subst', mkTyVarTy tv') }
-tcInstTyBinder _ subst (Anon ty)
+tcInstInvisibleTyBinder subst (Anon ty)
-- This is the *only* constraint currently handled in types.
| Just (mk, k1, k2) <- get_eq_tys_maybe substed_ty
= do { co <- unifyKind Nothing k1 k2
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index d643925127..09ef93a6db 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -873,9 +873,9 @@ can_eq_nc'
-> TcS (StopOrContinue Ct)
-- 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
- | Just ty1' <- tcView ty1 = can_eq_nc flat 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
+can_eq_nc' flat rdr_env envs 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 rdr_env envs ev eq_rel ty1 ps_ty1 ty2' ps_ty2
-- need to check for reflexivity in the ReprEq case.
-- See Note [Eager reflexivity check]
@@ -1048,7 +1048,7 @@ can_eq_nc_forall ev eq_rel s1 s2
-- | Compare types for equality, while zonking as necessary. Gives up
-- as soon as it finds that two types are not equal.
-- 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).
-- In particular, this function makes a ~20% improvement in test case
-- perf/compiler/T5030.
@@ -1836,10 +1836,11 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
| k1 `tcEqType` k2
= canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
- -- Note [Flattening] in TcFlatten gives us (F2), which says that
- -- flattening is always homogeneous (doesn't change kinds). But
- -- perhaps by flattening the kinds of the two sides of the equality
- -- at hand makes them equal. So let's try that.
+ -- So the LHS and RHS don't have equal kinds
+ -- Note [Flattening] in TcFlatten gives us (F2), which says that
+ -- flattening is always homogeneous (doesn't change kinds). But
+ -- perhaps by flattening the kinds of the two sides of the equality
+ -- at hand makes them equal. So let's try that.
| otherwise
= 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)
@@ -1852,7 +1853,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
, ppr flat_k2
, 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
-- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence
-- (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
-- See Note [Equalities with incompatible kinds]
| otherwise -- Wanted and Derived
- -- NB: all kind equalities are Nominal
+ -- NB: all kind equalities are Nominal
= do { emitNewDerivedEq kind_loc Nominal ki1 ki2
-- kind_ev :: (ki1 :: *) ~ (ki2 :: *)
; traceTcS "Hetero equality gives rise to derived kind equality" $
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index df307f240c..ab48326398 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -1975,17 +1975,16 @@ misMatchMsg ct oriented ty1 ty2
-- themselves.
pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
-> SDoc -> SDoc
-pprWithExplicitKindsWhenMismatch ty1 ty2 ct =
- pprWithExplicitKindsWhen mismatch
+pprWithExplicitKindsWhenMismatch ty1 ty2 ct
+ = pprWithExplicitKindsWhen show_kinds
where
(act_ty, exp_ty) = case ct of
TypeEqOrigin { uo_actual = act
, uo_expected = exp } -> (act, exp)
_ -> (ty1, ty2)
- mismatch | Just vis <- tcEqTypeVis act_ty exp_ty
- = not vis
- | otherwise
- = False
+ show_kinds = tcEqTypeVis act_ty exp_ty
+ -- True when the visible bit of the types look the same,
+ -- so we want to show the kinds in the displayed type
mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
-> (Bool, Maybe SwapFlag, SDoc)
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index 2a0fc7a33a..aa2c0202fb 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1329,8 +1329,7 @@ flatten_exact_fam_app_fully tc tys
-- See Note [Reduce type family applications eagerly]
-- the following tcTypeKind should never be evaluated, as it's just used in
-- casting, and casts by refl are dropped
- = do { let reduce_co = mkNomReflCo (tcTypeKind (mkTyConApp tc tys))
- ; mOut <- try_to_reduce_nocache tc tys reduce_co id
+ = do { mOut <- try_to_reduce_nocache tc tys
; case mOut of
Just out -> pure out
Nothing -> do
@@ -1452,16 +1451,8 @@ flatten_exact_fam_app_fully tc tys
try_to_reduce_nocache :: TyCon -- F, family tycon
-> [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))
- try_to_reduce_nocache tc tys kind_co update_co
+ try_to_reduce_nocache tc tys
= do { checkStackDepth (mkTyConApp tc tys)
; mb_match <- liftTcS $ matchFam tc tys
; case mb_match of
@@ -1470,13 +1461,9 @@ flatten_exact_fam_app_fully tc tys
Just (norm_co, norm_ty)
-> do { (xi, final_co) <- bumpDepth $ flatten_one norm_ty
; eq_rel <- getEqRel
- ; let co = maybeSubCo eq_rel norm_co
- `mkTransCo` mkSymCo final_co
- role = eqRelRole eq_rel
- xi' = xi `mkCastTy` kind_co
- co' = update_co $
- mkTcCoherenceLeftCo role xi kind_co (mkSymCo co)
- ; return $ Just (xi', co') }
+ ; let co = mkSymCo (maybeSubCo eq_rel norm_co
+ `mkTransCo` mkSymCo final_co)
+ ; return $ Just (xi, co) }
Nothing -> pure Nothing }
{- Note [Reduce type family applications eagerly]
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 462b9245e5..3f7a32565d 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -204,6 +204,7 @@ data ZonkEnv -- See Note [The ZonkEnv]
, ze_tv_env :: TyCoVarEnv TyCoVar
, ze_id_env :: IdEnv Id
, ze_meta_tv_env :: TcRef (TyVarEnv Type) }
+
{- Note [The ZonkEnv]
~~~~~~~~~~~~~~~~~~~~~
* ze_flexi :: ZonkFlexi says what to do with a
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 7a63202f96..a6cdd09849 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -46,7 +46,7 @@ module TcHsType (
typeLevelMode, kindLevelMode,
- kindGeneralize, checkExpectedKind, RequireSaturation(..),
+ kindGeneralize, checkExpectedKind_pp,
reportFloatingKvs,
-- Sort-checking kinds
@@ -76,9 +76,10 @@ import TcUnify
import TcIface
import TcSimplify
import TcHsSyn
+import TyCoRep ( Type(..) )
import TcErrors ( reportAllUnsolved )
import TcType
-import Inst ( tcInstTyBinders, tcInstTyBinder )
+import Inst ( tcInstInvisibleTyBinders, tcInstInvisibleTyBinder )
import TyCoRep( TyCoBinder(..), tyCoBinderArgFlag ) -- Used in etaExpandAlgTyCon
import Type
import TysPrim
@@ -251,7 +252,7 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind
; 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 is used for kind-checking top-level HsType where
@@ -291,7 +292,7 @@ tcHsDeriv hs_ty
-- with "illegal deriving", below
tcTopLHsType hs_ty AnyKind
; let (tvs, pred) = splitForAllTys ty
- (kind_args, _) = splitFunTys (typeKind pred)
+ (kind_args, _) = splitFunTys (tcTypeKind pred)
; case getClassPredTys_maybe pred of
Just (cls, tys) -> return (tvs, (cls, tys, kind_args))
Nothing -> failWithTc (text "Illegal deriving item" <+> quotes (ppr hs_ty)) }
@@ -402,8 +403,6 @@ and Note [The wildcard story for types] in HsTypes.hs
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)
-- 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
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
- 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
@@ -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,
-- differentiates only between types and kinds, but this will likely
-- grow, at least to include the distinction between patterns and
-- not-patterns.
-data TcTyMode
- = TcTyMode { mode_level :: TypeOrKind
- , mode_sat :: RequireSaturation
- }
- -- The mode_unsat field is solely so that type families/synonyms can be unsaturated
- -- in GHCi :kind calls
+--
+-- To find out where the mode is used, search for 'mode_level'
+data TcTyMode = TcTyMode { mode_level :: TypeOrKind }
typeLevelMode :: TcTyMode
-typeLevelMode = TcTyMode { mode_level = TypeLevel, mode_sat = YesSaturation }
+typeLevelMode = TcTyMode { mode_level = TypeLevel }
kindLevelMode :: TcTyMode
-kindLevelMode = TcTyMode { mode_level = KindLevel, mode_sat = YesSaturation }
-
-allowUnsaturated :: TcTyMode -> TcTyMode
-allowUnsaturated mode = mode { mode_sat = NoSaturation }
+kindLevelMode = TcTyMode { mode_level = KindLevel }
-- switch to kind level
kindLevel :: TcTyMode -> TcTyMode
kindLevel mode = mode { mode_level = KindLevel }
-instance Outputable RequireSaturation where
- ppr YesSaturation = text "YesSaturation"
- ppr NoSaturation = text "NoSaturation"
-
instance Outputable TcTyMode where
ppr = ppr . mode_level
@@ -504,7 +520,7 @@ metavariable.
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
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
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,
we have a bunch of repetitive code just so that we get warnings if we're
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:
tc_infer_lhs_type :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
tc_infer_lhs_type mode (L span ty)
= setSrcSpan span $
- do { (ty', kind) <- tc_infer_hs_type mode ty
- ; return (ty', kind) }
+ tc_infer_hs_type mode ty
+---------------------------
+-- | 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,
-- as described in Note [Bidirectional type checking]
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 e@(HsAppKindTy {}) = tcTyApp mode e
+tc_infer_hs_type mode (HsParTy _ t)
+ = tc_infer_lhs_type mode t
-tc_infer_hs_type mode (HsOpTy _ lhs lhs_op@(L _ hs_op) rhs)
- | not (hs_op `hasKey` funTyConKey)
- = do { (op, op_kind) <- tcTyVar mode hs_op
- ; tcTyApps mode (noLoc $ HsTyVar noExt NotPromoted lhs_op) op op_kind
- [HsValArg lhs, HsValArg rhs] }
+tc_infer_hs_type mode ty
+ | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
+ = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
+ ; tcInferApps mode hs_fun_ty fun_ty hs_args }
tc_infer_hs_type mode (HsKindSig _ ty sig)
= do { sig' <- tcLHsKindSig KindSigCtxt sig
@@ -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 _ (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)
| null tys -- this is so that we can use visible kind application with '[]
@@ -631,25 +619,7 @@ tc_lhs_type mode (L span 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
--- See Note [The tcType invariant]
-- See Note [Bidirectional type checking]
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
; 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)
- = 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
+ ; ty' <- tc_lhs_type mode rn_ty constraintKind
+ ; return (mkPhiTy ctxt' ty') }
- -- See Note [Body kind of a HsQualTy]
- ; ty' <- if tcIsConstraintKind exp_kind
- then tc_lhs_type mode ty constraintKind
- else do { ek <- newOpenTypeKind
- -- The body kind (result of the function)
- -- can be TYPE r, for any r, hence newOpenTypeKind
- ; ty' <- tc_lhs_type mode ty ek
- ; checkExpectedKindMode mode (ppr ty) ty' liftedTypeKind exp_kind }
+ | otherwise
+ = do { ctxt' <- tc_hs_context mode ctxt
- ; return (mkPhiTy ctxt' ty') }
+ ; ek <- newOpenTypeKind -- The body kind (result of the function) can
+ -- be TYPE r, for any r, hence newOpenTypeKind
+ ; ty' <- tc_lhs_type mode rn_ty ek
+ ; checkExpectedKind (unLoc rn_ty) (mkPhiTy ctxt' ty')
+ liftedTypeKind exp_kind }
--------- Lists, arrays, and tuples
tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
= do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
; checkWiredInTyCon listTyCon
- ; checkExpectedKindMode mode (ppr rn_ty) (mkListTy tau_ty) liftedTypeKind exp_kind }
+ ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
-- See Note [Distinguishing tuple kinds] in HsTypes
-- See Note [Inferring tuple kinds]
@@ -757,10 +728,10 @@ tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
-- In the [] case, it's not clear what the kind is, so guess *
; tys' <- sequence [ setSrcSpan loc $
- checkExpectedKindMode mode (ppr hs_ty) ty kind arg_kind
+ checkExpectedKind hs_ty ty kind arg_kind
| ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
- ; finish_tuple rn_ty mode tup_sort tys' (map (const arg_kind) tys') exp_kind }
+ ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
tc_hs_type mode rn_ty@(HsTupleTy _ hs_tup_sort tys) exp_kind
@@ -778,10 +749,9 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
; let arg_reps = map kindRep arg_kinds
arg_tys = arg_reps ++ tau_tys
- ; checkExpectedKindMode mode (ppr rn_ty)
- (mkTyConApp (sumTyCon arity) arg_tys)
- (unboxedSumKind arg_reps)
- exp_kind
+ sum_ty = mkTyConApp (sumTyCon arity) arg_tys
+ sum_kind = unboxedSumKind arg_reps
+ ; checkExpectedKind rn_ty sum_ty sum_kind exp_kind
}
--------- Promoted lists and tuples
@@ -789,7 +759,7 @@ tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
= do { tks <- mapM (tc_infer_lhs_type mode) tys
; (taus', kind) <- unifyKinds tys tks
; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
- ; checkExpectedKindMode mode (ppr rn_ty) ty (mkListTy kind) exp_kind }
+ ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
where
mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
@@ -802,7 +772,7 @@ tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
; let kind_con = tupleTyCon Boxed arity
ty_con = promotedTupleDataCon Boxed arity
tup_k = mkTyConApp kind_con ks
- ; checkExpectedKindMode mode (ppr rn_ty) (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
+ ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
where
arity = length tys
@@ -812,41 +782,53 @@ tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
; ty' <- tc_lhs_type mode ty liftedTypeKind
; let n' = mkStrLitTy $ hsIPNameFS n
; ipClass <- tcLookupClass ipClassName
- ; checkExpectedKindMode mode (ppr rn_ty) (mkClassPred ipClass [n',ty'])
- constraintKind exp_kind }
+ ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
+ constraintKind exp_kind }
-tc_hs_type mode rn_ty@(HsStarTy _ _) exp_kind
+tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
-- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't have to
-- handle it in 'coreView' and 'tcView'.
- = checkExpectedKindMode mode (ppr rn_ty) liftedTypeKind liftedTypeKind exp_kind
+ = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind
--------- Literals
-tc_hs_type mode rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
+tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
= do { checkWiredInTyCon typeNatKindCon
- ; checkExpectedKindMode mode (ppr rn_ty) (mkNumLitTy n) typeNatKind exp_kind }
+ ; checkExpectedKind rn_ty (mkNumLitTy n) typeNatKind exp_kind }
-tc_hs_type mode rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
+tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
= do { checkWiredInTyCon typeSymbolKindCon
- ; checkExpectedKindMode mode (ppr rn_ty) (mkStrLitTy s) typeSymbolKind exp_kind }
+ ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
--------- Potentially kind-polymorphic types: call the "up" checker
-- See Note [Future-proofing the type checker]
-tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
+tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
+tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
+tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
+tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
+tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek
+tc_hs_type _ wc@(HsWildCardTy _) ek = tcWildCardOcc wc ek
-tc_hs_type mode wc@(HsWildCardTy _) exp_kind
- = do { wc_ty <- tcWildCardOcc mode wc exp_kind
- ; return (mkNakedCastTy wc_ty (mkTcNomReflCo exp_kind))
- -- Take care here! Even though the coercion is Refl,
- -- we still need it to establish Note [The tcType invariant]
- }
+------------------------------------------
+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
+ ; checkExpectedKind (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
+ ; checkExpectedKind (HsFunTy noExt ty1 ty2) (mkFunTy ty1' ty2')
+ liftedTypeKind exp_kind }
-tcWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
-tcWildCardOcc mode wc exp_kind
+---------------------------
+tcWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType
+tcWildCardOcc wc exp_kind
= do { wc_tv <- newWildTyVar
-- The wildcard's kind should be an un-filled-in meta tyvar
; loc <- getSrcSpanM
@@ -857,7 +839,7 @@ tcWildCardOcc mode wc exp_kind
-- See Note [Wildcards in visible kind application]
; unless (part_tysig && not warning)
(emitWildCardHoleConstraints [(name,wc_tv)])
- ; checkExpectedKindMode mode (ppr wc) (mkTyVarTy wc_tv)
+ ; checkExpectedKind wc (mkTyVarTy wc_tv)
(tyVarKind wc_tv) exp_kind }
{- Note [Wildcards in visible kind application]
@@ -883,12 +865,12 @@ See related Note [Wildcards in visible type application] here and
Note [The wildcard story for types] in HsTypes.hs
-}
----------------------------
--- | 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
- ; checkExpectedKindMode mode (ppr hs_ty) ty k ek }
+
+{- *********************************************************************
+* *
+ Tuples
+* *
+********************************************************************* -}
---------------------------
tupKindSort_maybe :: TcKind -> Maybe TupleSort
@@ -906,18 +888,17 @@ tc_tuple rn_ty mode tup_sort tys exp_kind
UnboxedTuple -> mapM (\_ -> newOpenTypeKind) tys
ConstraintTuple -> return (nOfThem arity constraintKind)
; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
- ; finish_tuple rn_ty mode tup_sort tau_tys arg_kinds exp_kind }
+ ; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
where
arity = length tys
finish_tuple :: HsType GhcRn
- -> TcTyMode
-> TupleSort
-> [TcType] -- ^ argument types
-> [TcKind] -- ^ of these kinds
-> TcKind -- ^ expected kind of the whole tuple
-> TcM TcType
-finish_tuple rn_ty mode tup_sort tau_tys tau_kinds exp_kind
+finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
= do { traceTc "finish_tuple" (ppr res_kind $$ ppr tau_kinds $$ ppr exp_kind)
; let arg_tys = case tup_sort of
-- See also Note [Unboxed tuple RuntimeRep vars] in TyCon
@@ -933,7 +914,7 @@ finish_tuple rn_ty mode tup_sort tau_tys tau_kinds exp_kind
; checkWiredInTyCon tc
; return tc }
UnboxedTuple -> return (tupleTyCon Unboxed arity)
- ; checkExpectedKindMode mode (ppr rn_ty) (mkTyConApp tycon arg_tys) res_kind exp_kind }
+ ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
where
arity = length tau_tys
tau_reps = map kindRep tau_kinds
@@ -948,6 +929,49 @@ bigConstraintTuple arity
<+> parens (text "max arity =" <+> int mAX_CTUPLE_SIZE))
2 (text "Instead, use a nested tuple")
+
+{- *********************************************************************
+* *
+ Type applications
+* *
+********************************************************************* -}
+
+splitHsAppTys :: HsType GhcRn -> Maybe (LHsType GhcRn, [LHsTypeArg GhcRn])
+splitHsAppTys hs_ty
+ | is_app hs_ty = Just (go (noLoc hs_ty) [])
+ | otherwise = Nothing
+ where
+ is_app :: HsType GhcRn -> Bool
+ is_app (HsAppKindTy {}) = True
+ is_app (HsAppTy {}) = True
+ is_app (HsOpTy _ _ (L _ op) _) = not (op `hasKey` funTyConKey)
+ -- I'm not sure why this funTyConKey test is necessary
+ -- Can it even happen? Perhaps for t1 `(->)` t2
+ -- but then maybe it's ok to treat that like a normal
+ -- application rather than using the special rule for HsFunTy
+ is_app (HsTyVar {}) = True
+ is_app (HsParTy _ (L _ ty)) = is_app ty
+ is_app _ = False
+
+ 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 (L _ (HsOpTy _ l op@(L sp _) r)) as
+ = ( L sp (HsTyVar noExt NotPromoted op)
+ , HsValArg l : HsValArg r : as )
+ go f as = (f, as)
+
+---------------------------
+tcInferAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
+-- Version of tc_infer_lhs_type specialised for the head of an
+-- application. In particular, for a HsTyVar (which includes type
+-- constructors, it does not zoom off into tcInferApps and family
+-- saturation
+tcInferAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
+ = tcTyVar mode tv
+tcInferAppHead mode ty
+ = tc_infer_lhs_type mode ty
+
---------------------------
-- | Apply a type of a given kind to a list of arguments. This instantiates
-- invisible parameters as necessary. Always consumes all the arguments,
@@ -955,84 +979,116 @@ bigConstraintTuple arity
-- This takes an optional @VarEnv Kind@ which maps kind variables to kinds.-
-- These kinds should be used to instantiate invisible kind variables;
-- they come from an enclosing class for an associated type/data family.
-tcInferApps :: TcTyMode
- -> LHsType GhcRn -- ^ Function (for printing only)
- -> TcType -- ^ Function
- -> TcKind -- ^ Function kind (zonked)
- -> [LHsTypeArg GhcRn] -- ^ Args
- -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
--- Precondition: tcTypeKind fun_ty = fun_ki
--- Reason: we will return a type application like (fun_ty arg1 ... argn),
--- and that type must be well-kinded
--- See Note [The tcType invariant]
--- Postcondition: Result kind is zonked.
-tcInferApps mode orig_hs_ty fun_ty orig_fun_ki orig_hs_args
- = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args $$ ppr orig_fun_ki)
- ; (f_args, res_k) <- go 1 empty_subst fun_ty orig_fun_ki orig_hs_args
- ; traceTc "tcInferApps }" empty
- ; res_k <- zonkTcType res_k -- Uphold (IT4) of Note [The tcType invariant]
+--
+-- tcInferApps also arranges to saturate any trailing invisible arguments
+-- of a type-family application, which is usually the right thing to do
+-- tcInferApps_nosat does not do this saturation; it is used only
+-- by ":kind" in GHCi
+tcInferApps, tcInferApps_nosat
+ :: TcTyMode
+ -> LHsType GhcRn -- ^ Function (for printing only)
+ -> TcType -- ^ Function
+ -> [LHsTypeArg GhcRn] -- ^ Args
+ -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
+tcInferApps mode hs_ty fun hs_args
+ = do { (f_args, res_k) <- tcInferApps_nosat mode hs_ty fun hs_args
+ ; saturateFamApp f_args res_k }
+
+tcInferApps_nosat mode orig_hs_ty fun orig_hs_args
+ = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args)
+ ; (f_args, res_k) <- go_init 1 fun orig_hs_args
+ ; traceTc "tcInferApps }" (ppr f_args <+> dcolon <+> ppr res_k)
; return (f_args, res_k) }
where
- empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
- tyCoVarsOfType orig_fun_ki
-
- go :: Int -- the # of the next argument
- -> TCvSubst -- instantiating substitution
- -> TcType -- function applied to some args
- -> TcKind -- function kind
- -> [LHsTypeArg GhcRn] -- un-type-checked args
- -> TcM (TcType, TcKind) -- same as overall return type
-
- -- case on all_args first, for performance reasons
- go n subst fun fun_ki all_args = case (all_args, tcSplitPiTy_maybe fun_ki) of
- -- no user-written args left. We're done!
- ([], _) -> return (fun, nakedSubstTy subst fun_ki)
- -- nakedSubstTy: see Note [The well-kinded type invariant]
-
- -- We don't care about parens here
- (HsArgPar _ : args, _) -> go n subst fun fun_ki args
-
- -- Next argument is a kind application (fun @ki)
- (HsTypeArg _ ki_arg : args, Just (ki_binder, inner_ki)) ->
+
+ -- go_init just initialises the auxiliary
+ -- arguments of the 'go' loop
+ go_init n fun all_args
+ = go n fun empty_subst fun_ki all_args
+ where
+ fun_ki = tcTypeKind fun
+ -- We do (tcTypeKind fun) here, even though the caller
+ -- knows the function kind, to absolutely guarantee
+ -- INVARIANT for 'go'
+ -- Note that in a typical application (F t1 t2 t3),
+ -- the 'fun' is just a TyCon, so tcTypeKind is fast
+
+ empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
+ tyCoVarsOfType fun_ki
+
+ go :: Int -- The # of the next argument
+ -> TcType -- Function applied to some args
+ -> TCvSubst -- Applies to function kind
+ -> TcKind -- Function kind
+ -> [LHsTypeArg GhcRn] -- Un-type-checked args
+ -> TcM (TcType, TcKind) -- Result type and its kind
+ -- INVARIANT: in any call (go n fun subst fun_ki args)
+ -- tcTypeKind fun = subst(fun_ki)
+ -- So the 'subst' and 'fun_ki' arguments are simply
+ -- there to avoid repeatedly calling tcTypeKind.
+ --
+ -- Reason for INVARIANT: to support the Purely Kinded Type Invariant
+ -- it's important that if fun_ki has a forall, then so does
+ -- (tcTypeKind fun), because the next thing we are going to do
+ -- is apply 'fun' to an argument type.
+
+ -- Dispatch on all_args first, for performance reasons
+ go n fun subst fun_ki all_args = case (all_args, tcSplitPiTy_maybe fun_ki) of
+
+ ---------------- No user-written args left. We're done!
+ ([], _) -> return (fun, substTy subst fun_ki)
+
+ ---------------- HsArgPar: We don't care about parens here
+ (HsArgPar _ : args, _) -> go n fun subst fun_ki args
+
+ ---------------- HsTypeArg: a kind application (fun @ki)
+ (HsTypeArg _ hs_ki_arg : hs_args, Just (ki_binder, inner_ki)) ->
case tyCoBinderArgFlag ki_binder of
- Inferred -> instantiate ki_binder inner_ki
+
+ -- FunTy with PredTy on LHS, or ForAllTy with Inferred
+ Inferred -> instantiate ki_binder inner_ki
+
+ -- Specified (invisible) binder with visible kind argument
Specified ->
- -- Invisible and specified binder with visible kind argument
do { traceTc "tcInferApps (vis kind app)"
- (vcat [ ppr ki_binder, ppr ki_arg
+ (vcat [ ppr ki_binder, ppr hs_ki_arg
, ppr (tyBinderType ki_binder)
, ppr subst, ppr (tyCoBinderArgFlag ki_binder) ])
- ; let exp_kind = nakedSubstTy subst $ tyBinderType ki_binder
- -- nakedSubstTy: see Note [The well-kinded type invariant]
- ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty ki_arg n) $
- unsetWOptM Opt_WarnPartialTypeSignatures $
- setXOptM LangExt.PartialTypeSignatures $
- -- see Note [Wildcards in visible kind application]
- tc_lhs_type (kindLevel mode) ki_arg exp_kind
+
+ ; let exp_kind = substTy subst $ tyBinderType ki_binder
+
+ ; ki_arg <- addErrCtxt (funAppCtxt orig_hs_ty hs_ki_arg n) $
+ unsetWOptM Opt_WarnPartialTypeSignatures $
+ setXOptM LangExt.PartialTypeSignatures $
+ -- Urgh! see Note [Wildcards in visible kind application]
+ -- ToDo: must kill this ridiculous messing with DynFlags
+ tc_lhs_type (kindLevel mode) hs_ki_arg exp_kind
+
; traceTc "tcInferApps (vis kind app)" (ppr exp_kind)
- ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
- ; go (n+1) subst'
- (mkNakedAppTy fun arg')
- inner_ki args }
-
- -- visible kind application, but we need a normal type application; error.
- -- this is when we have (fun @ki) but (fun :: k1 -> k2), that is, without a forall
- Required -> do { traceTc "tcInferApps (error)"
- (vcat [ ppr ki_binder
- , ppr ki_arg
- , ppr (tyBinderType ki_binder)
- , ppr subst
- , ppr (isInvisibleBinder ki_binder) ])
- ; ty_app_err ki_arg $ nakedSubstTy subst fun_ki }
-
- -- no binder; try applying the substitution, or fail if that's not possible
+ ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
+ ; go (n+1) fun' subst' inner_ki hs_args }
+
+ -- Visible kind application, but we need a normal type application; error.
+ -- This happens when we have (fun @ki) but (fun :: k1 -> k2),
+ -- that is, without a forall
+ Required ->
+ do { traceTc "tcInferApps (error)"
+ (vcat [ ppr ki_binder
+ , ppr hs_ki_arg
+ , ppr (tyBinderType ki_binder)
+ , ppr subst
+ , ppr (isInvisibleBinder ki_binder) ])
+ ; ty_app_err hs_ki_arg $ substTy subst fun_ki }
+
+ -- No binder; try applying the substitution, or fail if that's not possible
(HsTypeArg _ ki_arg : _, Nothing) -> try_again_after_substing_or $
ty_app_err ki_arg substed_fun_ki
- -- normal argument (fun ty)
+ ---------------- HsValArg: a nomal argument (fun ty)
(HsValArg arg : args, Just (ki_binder, inner_ki))
-- next binder is invisible; need to instantiate it
- | isInvisibleBinder ki_binder
+ | isInvisibleBinder ki_binder -- FunTy with PredTy on LHS;
+ -- or ForAllTy with Inferred or Specified
-> instantiate ki_binder inner_ki
-- "normal" case
@@ -1042,138 +1098,266 @@ tcInferApps mode orig_hs_ty fun_ty orig_fun_ki orig_hs_args
, ppr arg
, ppr (tyBinderType ki_binder)
, ppr subst ])
- ; let exp_kind = nakedSubstTy subst $ tyBinderType ki_binder
- -- nakedSubstTy: see Note [The well-kinded type invariant]
+ ; let exp_kind = substTy subst $ tyBinderType ki_binder
; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
tc_lhs_type mode arg exp_kind
; traceTc "tcInferApps (vis normal app) 2" (ppr exp_kind)
- ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
- ; go (n+1) subst' (mkNakedAppTy fun arg') inner_ki args }
+ ; (subst', fun') <- mkAppTyM subst fun ki_binder arg'
+ ; go (n+1) fun' subst' inner_ki args }
-- no binder; try applying the substitution, or infer another arrow in fun kind
(HsValArg _ : _, Nothing)
-> try_again_after_substing_or $
- do { traceTc "tcInferApps (no binder)" empty
- ; (co, arg_k, res_k) <- matchExpectedFunKind hs_ty substed_fun_ki
- ; let new_in_scope = tyCoVarsOfTypes [arg_k, res_k]
- subst' = zapped_subst `extendTCvInScopeSet` new_in_scope
- ; go n subst'
- (fun `mkNakedCastTy` co) -- See Note [The well-kinded type invariant]
- (mkFunTy arg_k res_k) all_args }
-
+ do { let arrows_needed = n_initial_val_args all_args
+ ; co <- matchExpectedFunKind hs_ty arrows_needed substed_fun_ki
+
+ ; fun' <- zonkTcType (fun `mkTcCastTy` co)
+ -- This zonk is essential, to expose the fruits
+ -- of matchExpectedFunKind to the 'go' loop
+
+ ; traceTc "tcInferApps (no binder)" $
+ vcat [ ppr fun <+> dcolon <+> ppr fun_ki
+ , ppr arrows_needed
+ , ppr co
+ , ppr fun' <+> dcolon <+> ppr (tcTypeKind fun')]
+ ; go_init n fun' all_args }
+ -- Use go_init to establish go's INVARIANT
where
instantiate ki_binder inner_ki
= do { traceTc "tcInferApps (need to instantiate)"
(vcat [ ppr ki_binder
, ppr subst
, ppr (tyCoBinderArgFlag ki_binder)])
- ; (subst', arg') <- tcInstTyBinder Nothing subst ki_binder
- ; go n subst' (mkNakedAppTy fun arg') inner_ki all_args }
+ ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder
+ ; go n (mkAppTy fun arg') subst' inner_ki all_args }
+ -- Because tcInvisibleTyBinder instantiate ki_binder,
+ -- the kind of arg' will have the same shape as the kind
+ -- of ki_binder. So we don't need mkAppTyM here.
try_again_after_substing_or fallthrough
| not (isEmptyTCvSubst subst)
- = go n zapped_subst fun substed_fun_ki all_args
+ = go n fun zapped_subst substed_fun_ki all_args
| otherwise
= fallthrough
- substed_fun_ki = substTy subst fun_ki
- zapped_subst = zapTCvSubst subst
- hs_ty = appTypeToArg orig_hs_ty (take (n-1) orig_hs_args)
+ zapped_subst = zapTCvSubst subst
+ substed_fun_ki = substTy subst fun_ki
+ hs_ty = appTypeToArg orig_hs_ty (take (n-1) orig_hs_args)
+
+ n_initial_val_args :: [HsArg tm ty] -> Arity
+ -- Count how many leading HsValArgs we have
+ n_initial_val_args (HsValArg {} : args) = 1 + n_initial_val_args args
+ n_initial_val_args (HsArgPar {} : args) = n_initial_val_args args
+ n_initial_val_args _ = 0
+
+ ty_app_err arg ty
+ = failWith $ text "Cannot apply function of kind" <+> quotes (ppr ty)
+ $$ text "to visible kind argument" <+> quotes (ppr arg)
+
+
+mkAppTyM :: TCvSubst
+ -> TcType -> TyCoBinder -- fun, plus its top-level binder
+ -> TcType -- arg
+ -> TcM (TCvSubst, TcType) -- Extended subst, plus (fun arg)
+-- Precondition: the application (fun arg) is well-kinded after zonking
+-- That is, the application makes sense
+--
+-- Precondition: for (mkAppTyM subst fun bndr arg)
+-- tcTypeKind fun = Pi bndr. body
+-- That is, fun always has a ForAllTy or FunTy at the top
+-- and 'bndr' is fun's pi-binder
+--
+-- Postcondition: if fun and arg satisfy (PKTI), the purely-kinded type
+-- invariant, then so does the result type (fun arg)
+--
+-- We do not require that
+-- tcTypeKind arg = tyVarKind (binderVar bndr)
+-- This must be true after zonking (precondition 1), but it's not
+-- required for the (PKTI).
+mkAppTyM subst fun ki_binder arg
+ | -- See Note [mkAppTyM]: Nasty case 2
+ TyConApp tc args <- fun
+ , isTypeSynonymTyCon tc
+ , args `lengthIs` (tyConArity tc - 1)
+ , any isTrickyTvBinder (tyConTyVars tc) -- We could cache this in the synonym
+ = do { arg' <- zonkTcType arg
+ ; args' <- zonkTcTypes args
+ ; let subst' = case ki_binder of
+ Anon {} -> subst
+ Named (Bndr tv _) -> extendTvSubstAndInScope subst tv arg'
+ ; return (subst', mkTyConApp tc (args' ++ [arg'])) }
+
+
+mkAppTyM subst fun (Anon {}) arg
+ = return (subst, mk_app_ty fun arg)
+
+mkAppTyM subst fun (Named (Bndr tv _)) arg
+ = do { arg' <- if isTrickyTvBinder tv
+ then -- See Note [mkAppTyM]: Nasty case 1
+ zonkTcType arg
+ else return arg
+ ; return ( extendTvSubstAndInScope subst tv arg'
+ , mk_app_ty fun arg' ) }
+
+mk_app_ty :: TcType -> TcType -> TcType
+-- This function just adds an ASSERT for mkAppTyM's precondition
+mk_app_ty fun arg
+ = ASSERT2( isPiTy fun_kind
+ , ppr fun <+> dcolon <+> ppr fun_kind $$ ppr arg )
+ mkAppTy fun arg
+ where
+ fun_kind = tcTypeKind fun
+
+isTrickyTvBinder :: TcTyVar -> Bool
+-- NB: isTrickyTvBinder is just an optimisation
+-- It would be absolutely sound to return True always
+isTrickyTvBinder tv = isPiTy (tyVarKind tv)
+
+{- Note [The Purely Kinded Type Invariant (PKTI)]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+During type inference, we maintain this invariant
+
+ (PKTI) It is legal to call 'tcTypeKind' on any Type ty,
+ on any sub-term of ty, /without/ zonking ty
+
+ Moreover, any such returned kind
+ will itself satisfy (PKTI)
+
+By "legal to call tcTypeKind" we mean "tcTypeKind will not crash".
+The way in which tcTypeKind can crash is in applications
+ (a t1 t2 .. tn)
+if 'a' is a type variable whose kind doesn't have enough arrows
+or foralls. (The crash is in piResultTys.)
+
+The loop in tcInferApps has to be very careful to maintain the (PKTI).
+For example, suppose
+ kappa is a unification variable
+ We have already unified kappa := Type
+ yielding co :: Refl (Type -> Type)
+ a :: kappa
+then consider the type
+ (a Int)
+If we call tcTypeKind on that, we'll crash, because the (un-zonked)
+kind of 'a' is just kappa, not an arrow kind. So we must zonk first.
+
+So the type inference engine is very careful when building applications.
+This happens in tcInferApps. Suppose we are kind-checking the type (a Int),
+where (a :: kappa). Then in tcInferApps we'll run out of binders on
+a's kind, so we'll call matchExpectedFunKind, and unify
+ kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
+At this point we must zonk the function type to expose the arrrow, so
+that (a Int) will satisfy (PKTI).
+
+The absence of this caused Trac #14174 and #14520.
+
+The calls to mkAppTyM is the other place we are very careful.
+
+Note [mkAppTyM]
+~~~~~~~~~~~~~~~
+mkAppTyM is trying to guaranteed the Purely Kinded Type Invariant
+(PKTI) for its result type (fun arg). There are two ways it can go wrong:
+
+* Nasty case 1: forall types (polykinds/T14174a)
+ T :: forall (p :: *->*). p Int -> p Bool
+ Now kind-check (T x), where x::kappa.
+ Well, T and x both satisfy the PKTI, but
+ T x :: x Int -> x Bool
+ and (x Int) does /not/ satisfy the PKTI.
+
+* Nasty case 2: type synonyms
+ type S f a = f a
+ Even though (S ff aa) would satisfy the (PKTI) if S was a data type
+ (i.e. nasty case 1 is dealt with), it might still not satisfy (PKTI)
+ if S is a type synonym, because the /expansion/ of (S ff aa) is
+ (ff aa), and /that/ does not satisfy (PKTI). E.g. perhaps
+ (ff :: kappa), where 'kappa' has already been unified with (*->*).
+
+ We check for nasty case 2 on the final argument of a type synonym.
+
+Notice that in both cases the trickiness only happens if the
+bound variable has a pi-type. Hence isTrickyTvBinder.
+-}
+
+
+saturateFamApp :: TcType -> TcKind -> TcM (TcType, TcKind)
+-- Precondition for (saturateFamApp ty kind):
+-- tcTypeKind ty = kind
+--
+-- If 'ty' is an unsaturated family application wtih trailing
+-- invisible arguments, instanttiate them.
+-- See Note [saturateFamApp]
+
+saturateFamApp ty kind
+ | Just (tc, args) <- tcSplitTyConApp_maybe ty
+ , mustBeSaturated tc
+ , let n_to_inst = tyConArity tc - length args
+ = do { (extra_args, ki') <- tcInstInvisibleTyBinders n_to_inst kind
+ ; return (ty `mkTcAppTys` extra_args, ki') }
+ | otherwise
+ = return (ty, kind)
+
+{- Note [saturateFamApp]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+ type family F :: Either j k
+ type instance F @Type = Right Maybe
+ type instance F @Type = Right Either```
+
+Then F :: forall {j,k}. Either j k
+
+The two type instances do a visible kind application that instantiates
+'j' but not 'k'. But we want to end up with instances that look like
+ type instance F @Type @(*->*) = Right @Type @(*->*) Maybe
+
+so that F has arity 2. We must instantiate that trailing invisible
+binder. In general, Invisible binders precede Specified and Required,
+so this is only going to bite for apparently-nullary families.
- ty_app_err arg ty = failWith $ text "Cannot apply function of kind" <+> quotes (ppr ty)
- $$ text "to visible kind argument" <+> quotes (ppr arg)
+Note that
+ type family F2 :: forall k. k -> *
+is quite different and really does have arity 0.
+
+It's not just type instances where we need to saturate those
+unsaturated arguments: see #11246. Hence doing this in tcInferApps.
+-}
appTypeToArg :: LHsType GhcRn -> [LHsTypeArg GhcRn] -> LHsType GhcRn
-appTypeToArg f [] = f
-appTypeToArg f (HsValArg arg : args) = appTypeToArg (mkHsAppTy f arg) args
+appTypeToArg f [] = f
+appTypeToArg f (HsValArg arg : args) = appTypeToArg (mkHsAppTy f arg) args
+appTypeToArg f (HsArgPar _ : args) = appTypeToArg f args
appTypeToArg f (HsTypeArg l arg : args)
= appTypeToArg (mkHsAppKindTy l f arg) args
-appTypeToArg f (HsArgPar _ : arg) = appTypeToArg f arg
-
--- | 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
--- your function.
--- Used for type-checking types only.
-tcTyApps :: TcTyMode
- -> LHsType GhcRn -- ^ Function (for printing only)
- -> TcType -- ^ Function
- -> TcKind -- ^ Function kind (zonked)
- -> [LHsTypeArg 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', ki') <- tcInferApps mode orig_hs_ty fun_ty fun_ki args
- ; return (ty' `mkNakedCastTy` mkNomReflCo ki', ki') }
- -- The mkNakedCastTy is for (IT3) of Note [The tcType invariant]
-
-tcTyApp :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind) -- only HsAppTy or HsAppKindTy
-tcTyApp mode e
- = do { let (hs_fun_ty, hs_args) = splitHsAppTys e
- ; (fun_ty, fun_kind) <- tc_infer_lhs_type mode hs_fun_ty
- -- NB: (IT4) of Note [The tcType invariant] ensures that fun_kind is zonked
- ; tcTyApps mode hs_fun_ty fun_ty fun_kind hs_args }
---------------------------
--- Internally-callable version of checkExpectedKind
-checkExpectedKindMode :: HasDebugCallStack
- => TcTyMode
- -> SDoc -- type we're checking
- -> TcType -- type we're checking
- -> TcKind -- kind of that type
- -> TcKind -- expected kind
- -> TcM TcType
-checkExpectedKindMode mode = checkExpectedKind (mode_sat mode)
+
+
+{- *********************************************************************
+* *
+ checkExpectedKind
+* *
+********************************************************************* -}
-- | This instantiates invisible arguments for the type being checked if it must
-- be saturated and is not yet saturated. It then calls and uses the result
-- from checkExpectedKindX to build the final type
--- Obeys Note [The tcType invariant]
checkExpectedKind :: HasDebugCallStack
- => RequireSaturation -- ^ Do we require all type families to be saturated?
- -> SDoc -- ^ type we're checking (for printing)
- -> TcType -- ^ type we're checking
- -> TcKind -- ^ the known kind of that type
- -> TcKind -- ^ the expected kind
+ => HsType GhcRn -- ^ type we're checking (for printing)
+ -> TcType -- ^ type we're checking
+ -> TcKind -- ^ the known kind of that type
+ -> TcKind -- ^ the expected kind
-> TcM TcType
-checkExpectedKind sat hs_ty ty act exp
- = do { (new_ty, new_act) <- case splitTyConApp_maybe ty of
- Just (tc, args)
- -- if the family tycon must be saturated and is not yet satured
- -- If we don't do this, we get #11246
- | YesSaturation <- sat
- , not (mightBeUnsaturatedTyCon tc) && length args < tyConArity tc
- -> do {
- -- we need to instantiate all invisible arguments up until saturation
- (tc_args, kind) <- tcInstTyBinders (splitPiTysInvisibleN
- (tyConArity tc - length args)
- act)
- ; let tc_ty = mkTyConApp tc $ args ++ tc_args
- ; traceTc "checkExpectedKind:satTyFam" (vcat [ ppr tc <+> dcolon <+> ppr act
- , ppr kind ])
- ; return (tc_ty, kind) }
- _ -> return (ty, act)
- ; (new_args, co_k) <- checkExpectedKindX hs_ty new_act exp
- ; return (new_ty `mkNakedAppTys` new_args `mkNakedCastTy` co_k) }
-
-checkExpectedKindX :: HasDebugCallStack
- => SDoc -- HsType whose kind we're checking
- -> TcKind -- the known kind of that type, k
- -> TcKind -- the expected kind, exp_kind
- -> TcM ([TcType], TcCoercionN)
- -- (the new args, the coercion)
--- Instantiate a kind (if necessary) and then call unifyType
--- (checkExpectedKind ty act_kind exp_kind)
--- checks that the actual kind act_kind is compatible
--- with the expected kind exp_kind
-checkExpectedKindX pp_hs_ty act_kind exp_kind
- = do { -- We need to make sure that both kinds have the same number of implicit
- -- foralls out front. If the actual kind has more, instantiate accordingly.
- -- Otherwise, just pass the type & kind through: the errors are caught
- -- in unifyType.
- let n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
- n_act_invis_bndrs = invisibleTyBndrCount act_kind
- n_to_inst = n_act_invis_bndrs - n_exp_invis_bndrs
- ; (new_args, act_kind') <- tcInstTyBinders (splitPiTysInvisibleN n_to_inst act_kind)
+-- Just a convenience wrapper to save calls to 'ppr'
+checkExpectedKind hs_ty ty act exp
+ = checkExpectedKind_pp (ppr hs_ty) ty act exp
+
+checkExpectedKind_pp :: HasDebugCallStack
+ => SDoc -- ^ The thing we are checking
+ -> TcType -- ^ type we're checking
+ -> TcKind -- ^ the known kind of that type
+ -> TcKind -- ^ the expected kind
+ -> TcM TcType
+checkExpectedKind_pp pp_hs_ty ty act_kind exp_kind
+ = do { traceTc "checkExpectedKind" (ppr ty $$ ppr act_kind)
+
+ ; (new_args, act_kind') <- tcInstInvisibleTyBinders n_to_inst act_kind
; let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = exp_kind
@@ -1182,18 +1366,27 @@ checkExpectedKindX pp_hs_ty act_kind exp_kind
; traceTc "checkExpectedKindX" $
vcat [ pp_hs_ty
- , text "act_kind:" <+> ppr act_kind
, text "act_kind':" <+> ppr act_kind'
, text "exp_kind:" <+> ppr exp_kind ]
+ ; let res_ty = ty `mkTcAppTys` new_args
+
; if act_kind' `tcEqType` exp_kind
- then return (new_args, mkTcNomReflCo exp_kind) -- This is very common
+ then return res_ty -- This is very common
else do { co_k <- uType KindLevel origin act_kind' exp_kind
; traceTc "checkExpectedKind" (vcat [ ppr act_kind
, ppr exp_kind
, ppr co_k ])
- -- See Note [The tcType invariant]
- ; return (new_args, co_k) } }
+ ; return (res_ty `mkTcCastTy` co_k) } }
+ where
+ -- We need to make sure that both kinds have the same number of implicit
+ -- foralls out front. If the actual kind has more, instantiate accordingly.
+ -- Otherwise, just pass the type & kind through: the errors are caught
+ -- in unifyType.
+ n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
+ n_act_invis_bndrs = invisibleTyBndrCount act_kind
+ n_to_inst = n_act_invis_bndrs - n_exp_invis_bndrs
+
---------------------------
tcHsMbContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
@@ -1220,26 +1413,14 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon
= do { traceTc "lk1" (ppr name)
; thing <- tcLookup name
; case thing of
- ATyVar _ tv -> -- Important: zonk before returning
- -- We may have the application ((a::kappa) b)
- -- where kappa is already unified to (k1 -> k2)
- -- Then we want to see that arrow. Best done
- -- here because we are also maintaining
- -- Note [The tcType invariant], so we don't just
- -- want to zonk the kind, leaving the TyVar
- -- un-zonked (Trac #14873)
- do { ty <- zonkTcTyVar tv
- ; return (ty, tcTypeKind ty) }
+ ATyVar _ tv -> return (mkTyVarTy tv, tyVarKind tv)
ATcTyCon tc_tc
-> do { -- See Note [GADT kind self-reference]
unless (isTypeLevel (mode_level mode))
(promotionErr name TyConPE)
; check_tc tc_tc
- ; tc_kind <- zonkTcType (tyConKind tc_tc)
- -- (IT6) of Note [The tcType invariant]
- ; return (mkTyConTy tc_tc `mkNakedCastTy` mkNomReflCo tc_kind, tc_kind) }
- -- the mkNakedCastTy ensures (IT5) of Note [The tcType invariant]
+ ; return (mkTyConTy tc_tc, tyConKind tc_tc) }
AGlobal (ATyCon tc)
-> do { check_tc tc
@@ -1362,8 +1543,8 @@ we try to figure out whether it's a tuple of kind * or Constraint.
If after Step 2 it's not clear from the arguments that it's
Constraint, then it must be *. Once having decided that we re-check
-the Check the arguments again to give good error messages
-in eg. `(Maybe, Maybe)`
+the arguments to give good error messages in
+ e.g. (Maybe, Maybe)
Note that we will still fail to infer the correct kind in this case:
@@ -2320,7 +2501,8 @@ tcHsPartialSigType ctxt sig_ty
, (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTy hs_ty
= addSigCtxt ctxt hs_ty $
do { (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
- <- tcWildCardBinders sig_wcs $ \ wcs ->
+ <- solveLocalEqualities "tcHsPatSigTypes" $
+ tcWildCardBinders sig_wcs $ \ wcs ->
bindImplicitTKBndrs_Tv implicit_hs_tvs $
bindExplicitTKBndrs_Tv explicit_hs_tvs $
do { -- Instantiate the type-class context; but if there
@@ -2371,7 +2553,7 @@ tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType)
tcPartialContext hs_theta
| Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta
, L _ wc@(HsWildCardTy _) <- ignoreParens hs_ctxt_last
- = do { wc_tv_ty <- tcWildCardOcc typeLevelMode wc constraintKind
+ = do { wc_tv_ty <- tcWildCardOcc wc constraintKind
; theta <- mapM tcLHsPredType hs_theta1
; return (theta, Just wc_tv_ty) }
| otherwise
@@ -2600,7 +2782,8 @@ together. Hence the new_tv function in tcHsPatSigType.
unifyKinds :: [LHsType GhcRn] -> [(TcType, TcKind)] -> TcM ([TcType], TcKind)
unifyKinds rn_tys act_kinds
= do { kind <- newMetaKindVar
- ; let check rn_ty (ty, act_kind) = checkExpectedKind YesSaturation (ppr $ unLoc rn_ty) ty act_kind kind
+ ; let check rn_ty (ty, act_kind)
+ = checkExpectedKind (unLoc rn_ty) ty act_kind kind
; tys' <- zipWithM check rn_tys act_kinds
; return (tys', kind) }
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index fccf8b7917..c1fd0da4c6 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -794,12 +794,17 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi
bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
do { stupid_theta <- tcHsContext hs_ctxt
; (lhs_ty, lhs_kind) <- tcFamTyPats fam_tc hs_pats
- -- Ensure that the instance is consistent with its
- -- parent class
+
+ -- Ensure that the instance is consistent
+ -- with its parent class
; addConsistencyConstraints mb_clsinfo lhs_ty
+
+ -- Add constraints from the data constructors
; mapM_ (wrapLocM_ kcConDecl) hs_cons
+
+ -- Add constraints from the result signature
; res_kind <- tc_kind_sig m_ksig
- ; lhs_ty <- checkExpectedKind YesSaturation pp_lhs lhs_ty lhs_kind res_kind
+ ; lhs_ty <- checkExpectedKind_pp pp_lhs lhs_ty lhs_kind res_kind
; return (stupid_theta, lhs_ty, res_kind) }
-- See TcTyClsDecls Note [Generalising in tcFamTyPatsGuts]
@@ -894,7 +899,7 @@ There are several fiddly subtleties lurking here
'k1' and 'k2', as well as 'b'.
The skolemise bit is done in tc_kind_sig, while the instantiate bit
- is done by the checkExpectedKind that immediately follows.
+ is done by tcFamTyPats.
* Very fiddly point. When we eta-reduce to
axiom AxDrep forall a b. D [(a,b]] = Drep a b
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index ffeb602382..c12c2f6e88 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -6,7 +6,7 @@
Monadic type operations
This module contains monadic operations over types that contain
-mutable type variables
+mutable type variables.
-}
{-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
@@ -784,10 +784,8 @@ writeMetaTyVarRef tyvar ref ty
= do { meta_details <- readMutVar ref;
-- Zonk kinds to allow the error check to work
; zonked_tv_kind <- zonkTcType tv_kind
- ; zonked_ty <- zonkTcType ty
- ; let zonked_ty_kind = tcTypeKind zonked_ty -- Need to zonk even before typeKind;
- -- otherwise, we can panic in piResultTy
- kind_check_ok = tcIsConstraintKind zonked_tv_kind
+ ; zonked_ty_kind <- zonkTcType ty_kind
+ ; let kind_check_ok = tcIsConstraintKind zonked_tv_kind
|| tcEqKind zonked_ty_kind zonked_tv_kind
-- Hack alert! tcIsConstraintKind: see TcHsType
-- Note [Extra-constraint holes in partial type signatures]
@@ -813,6 +811,7 @@ writeMetaTyVarRef tyvar ref ty
; writeMutVar ref (Indirect ty) }
where
tv_kind = tyVarKind tyvar
+ ty_kind = tcTypeKind ty
tv_lvl = tcTyVarLevel tyvar
ty_lvl = tcTypeLevel ty
@@ -1518,15 +1517,14 @@ defaultTyVar default_kind tv
; writeMetaTyVar tv liftedRepTy
; return True }
- | default_kind -- -XNoPolyKinds and this is a kind var
- = do { default_kind_var tv -- so default it to * if possible
- ; return True }
+ | default_kind -- -XNoPolyKinds and this is a kind var
+ = default_kind_var tv -- so default it to * if possible
| otherwise
= return False
where
- default_kind_var :: TyVar -> TcM ()
+ default_kind_var :: TyVar -> TcM Bool
-- defaultKindVar is used exclusively with -XNoPolyKinds
-- See Note [Defaulting with -XNoPolyKinds]
-- It takes an (unconstrained) meta tyvar and defaults it.
@@ -1534,11 +1532,20 @@ defaultTyVar default_kind tv
default_kind_var kv
| isLiftedTypeKind (tyVarKind kv)
= do { traceTc "Defaulting a kind var to *" (ppr kv)
- ; writeMetaTyVar kv liftedTypeKind }
+ ; writeMetaTyVar kv liftedTypeKind
+ ; return True }
| otherwise
- = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
- , text "of kind:" <+> ppr (tyVarKind kv')
- , text "Perhaps enable PolyKinds or add a kind signature" ])
+ = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
+ , text "of kind:" <+> ppr (tyVarKind kv')
+ , text "Perhaps enable PolyKinds or add a kind signature" ])
+ -- We failed to default it, so return False to say so.
+ -- Hence, it'll get skolemised. That might seem odd, but we must either
+ -- promote, skolemise, or zap-to-Any, to satisfy TcHsType
+ -- Note [Recipe for checking a signature]
+ -- Otherwise we get level-number assertion failures. It doesn't matter much
+ -- because we are in an error siutation anyway.
+ ; return False
+ }
where
(_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
@@ -1937,7 +1944,7 @@ zonkTcTypeMapper = TyCoMapper
, tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
, tcm_hole = hole
, tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv
- , tcm_tycon = return }
+ , tcm_tycon = zonk_tc_tycon }
where
hole :: () -> CoercionHole -> TcM Coercion
hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
@@ -1948,6 +1955,12 @@ zonkTcTypeMapper = TyCoMapper
Nothing -> do { cv' <- zonkCoVar cv
; return $ HoleCo (hole { ch_co_var = cv' }) } }
+ zonk_tc_tycon tc -- A non-poly TcTyCon may have unification
+ -- variables that need zonking, but poly ones cannot
+ | tcTyConIsPoly tc = return tc
+ | otherwise = do { tck' <- zonkTcType (tyConKind tc)
+ ; return (setTcTyConKind tc tck') }
+
-- For unbound, mutable tyvars, zonkType uses the function given to it
-- For tyvars bound at a for-all, zonkType zonks them to an immutable
-- type variable and zonks the kind too
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index a845623aaa..c5ffb054f2 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -3401,10 +3401,8 @@ newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts
emitNewWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS Coercion
-- | Emit a new Wanted equality into the work-list
emitNewWantedEq loc role ty1 ty2
- | otherwise
= do { (ev, co) <- newWantedEq loc role ty1 ty2
- ; updWorkListTcS $
- extendWorkListEq (mkNonCanonical ev)
+ ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
; return co }
-- | Make a new equality CtEvidence
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 1333489ad8..55c06fce8f 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -39,7 +39,6 @@ import {-# SOURCE #-} TcInstDcls( tcInstDecls1 )
import TcDeriv (DerivInfo)
import TcHsType
import ClsInst( AssocInstInfo(..) )
-import Inst( tcInstTyBinders )
import TcMType
import TysWiredIn ( unitTy )
import TcType
@@ -1742,7 +1741,7 @@ kcTyFamInstEqn tc_fam_tc
; discardResult $
bindImplicitTKBndrs_Q_Tv imp_vars $
bindExplicitTKBndrs_Q_Tv AnyKind (mb_expl_bndrs `orElse` []) $
- do { (_, res_kind) <- tcFamTyPats tc_fam_tc hs_pats
+ do { (_fam_app, res_kind) <- tcFamTyPats tc_fam_tc hs_pats
; tcCheckLHsType hs_rhs_ty res_kind }
-- Why "_Tv" here? Consider (Trac #14066
-- type family Bar x y where
@@ -1870,7 +1869,7 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
solveEqualities $
bindImplicitTKBndrs_Q_Skol imp_vars $
bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
- do { (lhs_ty, rhs_kind) <- tc_lhs
+ do { (lhs_ty, rhs_kind) <- tcFamTyPats fam_tc hs_pats
-- Ensure that the instance is consistent with its
-- parent class (#16008)
; addConsistencyConstraints mb_clsinfo lhs_ty
@@ -1897,43 +1896,6 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
-- have been solved before we attempt to unravel it
; traceTc "tcTyFamInstEqnGuts }" (ppr fam_tc <+> pprTyVars qtvs)
; return (qtvs, pats, rhs_ty) }
- where
- tc_lhs | null hs_pats -- See Note [Apparently-nullary families]
- = do { (args, rhs_kind) <- tcInstTyBinders $
- splitPiTysInvisibleN (tyConArity fam_tc)
- (tyConKind fam_tc)
- ; return (mkTyConApp fam_tc args, rhs_kind) }
- | otherwise
- = tcFamTyPats fam_tc hs_pats
-
-{- Note [Apparently-nullary families]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
- type family F :: k -> *
-
-This really means
- type family F @k :: k -> *
-
-That is, the family has arity 1, and can match on the kind. So it's
-not really a nullary family. NB that
- type famly F2 :: forall k. k -> *
-is quite different and really does have arity 0.
-
-Returning to F we might have
- type instannce F = Maybe
-which instantaite 'k' to '*' and really means
- type instannce F @* = Maybe
-
-Conclusion: in this odd case where there are no LHS patterns, we
-should instantiate any invisible foralls in F's kind, to saturate
-its arity (but no more). This is what happens in tc_lhs in
-tcTyFamInstEqnGuts.
-
-If there are any visible patterns, then the first will force
-instantiation of any Inferred quantifiers for F -- remember,
-Inferred quantifiers always come first.
--}
-
-----------------
tcFamTyPats :: TyCon
@@ -1942,9 +1904,7 @@ tcFamTyPats :: TyCon
-- Used for both type and data families
tcFamTyPats fam_tc hs_pats
= do { traceTc "tcFamTyPats {" $
- vcat [ ppr fam_tc <+> dcolon <+> ppr fam_kind
- , text "arity:" <+> ppr fam_arity
- , text "kind:" <+> ppr fam_kind ]
+ vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]
; let fun_ty = mkTyConApp fam_tc []
@@ -1952,18 +1912,15 @@ tcFamTyPats fam_tc hs_pats
setXOptM LangExt.PartialTypeSignatures $
-- See Note [Wildcards in family instances] in
-- RnSource.hs
- tcInferApps typeLevelMode lhs_fun fun_ty
- fam_kind hs_pats
+ tcInferApps typeLevelMode lhs_fun fun_ty hs_pats
; traceTc "End tcFamTyPats }" $
- vcat [ ppr fam_tc <+> dcolon <+> ppr fam_kind
- , text "res_kind:" <+> ppr res_kind ]
+ vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ]
; return (fam_app, res_kind) }
where
fam_name = tyConName fam_tc
fam_arity = tyConArity fam_tc
- fam_kind = tyConKind fam_tc
lhs_fun = noLoc (HsTyVar noExt NotPromoted (noLoc fam_name))
unravelFamInstPats :: TcType -> [TcType]
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index a7ba6b7966..7fcf30a538 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -52,7 +52,7 @@ module TcType (
--------------------------------
-- Builders
mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy,
- mkNakedAppTy, mkNakedAppTys, mkNakedCastTy, nakedSubstTy,
+ mkTcAppTy, mkTcAppTys, mkTcCastTy,
--------------------------------
-- Splitters
@@ -122,7 +122,7 @@ module TcType (
--------------------------------
-- Rexported from Kind
- Kind, typeKind, tcTypeKind,
+ Kind, tcTypeKind,
liftedTypeKind,
constraintKind,
isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
@@ -225,7 +225,7 @@ import ErrUtils( Validity(..), MsgDoc, isValid )
import qualified GHC.LanguageExtensions as LangExt
import Data.List ( mapAccumL )
-import Data.Functor.Identity( Identity(..) )
+-- import Data.Functor.Identity( Identity(..) )
import Data.IORef
import Data.List.NonEmpty( NonEmpty(..) )
@@ -1295,103 +1295,23 @@ getDFunTyLitKey (StrTyLit n) = mkOccName Name.varName (show n) -- hm
{- *********************************************************************
* *
- Maintaining the well-kinded type invariant
+ Building types
* *
********************************************************************* -}
-{- Note [The well-kinded type invariant]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [The tcType invariant] in TcHsType.
-
-During type inference, we maintain this invariant
-
- (INV-TK): it is legal to call 'tcTypeKind' on any Type ty,
- /without/ zonking ty
-
-For example, suppose
- kappa is a unification variable
- We have already unified kappa := Type
- yielding co :: Refl (Type -> Type)
- a :: kappa
-then consider the type
- (a Int)
-If we call tcTypeKind on that, we'll crash, because the (un-zonked)
-kind of 'a' is just kappa, not an arrow kind. If we zonk first
-we'd be fine, but that is too tiresome, so instead we maintain
-(INV-TK). So we do not form (a Int); instead we form
- (a |> co) Int
-and tcTypeKind has no problem with that.
-
-Bottom line: we want to keep that 'co' /even though it is Refl/.
-
-Immediate consequence: during type inference we cannot use the "smart
-contructors" for types, particularly
- mkAppTy, mkCastTy
-because they all eliminate Refl casts. Solution: during type
-inference use the mkNakedX type formers, which do no Refl-elimination.
-E.g. mkNakedCastTy uses an actual CastTy, without optimising for
-Refl. (NB: mkNakedCastTy is only called in two places: in tcInferApps
-and in checkExpectedResultKind.)
-
-Where does this show up in practice: apparently mainly in
-TcHsType.tcInferApps. Suppose we are kind-checking the type (a Int),
-where (a :: kappa). Then in tcInferApps we'll run out of binders on
-a's kind, so we'll call matchExpectedFunKind, and unify
- kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2)
-That evidence is actually Refl, but we must not discard the cast to
-form the result type
- ((a::kappa) (Int::*))
-because that does not satisfy the invariant, and crashes TypeKind. This
-caused Trac #14174 and #14520.
-
-Notes:
-
-* The Refls will be removed later, when we zonk the type.
-
-* This /also/ applies to substitution. We must use nakedSubstTy,
- not substTy, because the latter uses smart constructors that do
- Refl-elimination.
+-- ToDo: I think we need Tc versions of these
+-- Reason: mkCastTy checks isReflexiveCastTy, which checks
+-- for equality; and that has a different answer
+-- depending on whether or not Type = Constraint
--}
+mkTcAppTys :: Type -> [Type] -> Type
+mkTcAppTys = mkAppTys
----------------
-mkNakedAppTys :: Type -> [Type] -> Type
--- See Note [The well-kinded type invariant]
-mkNakedAppTys ty1 [] = ty1
-mkNakedAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
-mkNakedAppTys ty1 tys2 = foldl' AppTy ty1 tys2
-
-mkNakedAppTy :: Type -> Type -> Type
--- See Note [The well-kinded type invariant]
-mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
-
-mkNakedCastTy :: Type -> Coercion -> Type
--- Do /not/ attempt to get rid of the cast altogether,
--- even if it is Refl: see Note [The well-kinded type invariant]
--- Even doing (t |> co1) |> co2 ---> t |> (co1;co2)
--- does not seem worth the bother
---
--- NB: zonking will get rid of these casts, because it uses mkCastTy
---
--- In fact the calls to mkNakedCastTy ar pretty few and far between.
-mkNakedCastTy ty co = CastTy ty co
-
-nakedSubstTy :: HasCallStack => TCvSubst -> TcType -> TcType
-nakedSubstTy subst ty
- | isEmptyTCvSubst subst = ty
- | otherwise = runIdentity $
- checkValidSubst subst [ty] [] $
- mapType nakedSubstMapper subst ty
- -- Interesting idea: use StrictIdentity to avoid space leaks
-
-nakedSubstMapper :: TyCoMapper TCvSubst Identity
-nakedSubstMapper
- = TyCoMapper { tcm_smart = False
- , tcm_tyvar = \subst tv -> return (substTyVar subst tv)
- , tcm_covar = \subst cv -> return (substCoVar subst cv)
- , tcm_hole = \_ hole -> return (HoleCo hole)
- , tcm_tycobinder = \subst tv _ -> return (substVarBndr subst tv)
- , tcm_tycon = return }
+mkTcAppTy :: Type -> Type -> Type
+mkTcAppTy = mkAppTy
+
+mkTcCastTy :: Type -> Coercion -> Type
+mkTcCastTy = mkCastTy -- Do we need a tc version of mkCastTy?
{-
************************************************************************
@@ -1410,25 +1330,29 @@ variables. It's up to you to make sure this doesn't matter.
-- | Splits a forall type into a list of 'TyBinder's and the inner type.
-- Always succeeds, even if it returns an empty list.
tcSplitPiTys :: Type -> ([TyBinder], Type)
-tcSplitPiTys ty = ASSERT( all isTyBinder (fst sty) ) sty
+tcSplitPiTys ty
+ = ASSERT( all isTyBinder (fst sty) ) sty
where sty = splitPiTys ty
-- | Splits a type into a TyBinder and a body, if possible. Panics otherwise
tcSplitPiTy_maybe :: Type -> Maybe (TyBinder, Type)
-tcSplitPiTy_maybe ty = ASSERT( isMaybeTyBinder sty ) sty
- where sty = splitPiTy_maybe ty
- isMaybeTyBinder (Just (t,_)) = isTyBinder t
- isMaybeTyBinder _ = True
+tcSplitPiTy_maybe ty
+ = ASSERT( isMaybeTyBinder sty ) sty
+ where
+ sty = splitPiTy_maybe ty
+ isMaybeTyBinder (Just (t,_)) = isTyBinder t
+ isMaybeTyBinder _ = True
tcSplitForAllTy_maybe :: Type -> Maybe (TyVarBinder, Type)
tcSplitForAllTy_maybe ty | Just ty' <- tcView ty = tcSplitForAllTy_maybe ty'
tcSplitForAllTy_maybe (ForAllTy tv ty) = ASSERT( isTyVarBinder tv ) Just (tv, ty)
tcSplitForAllTy_maybe _ = Nothing
--- | Like 'tcSplitPiTys', but splits off only named binders, returning
--- just the tycovars.
+-- | Like 'tcSplitPiTys', but splits off only named binders,
+-- returning just the tycovars.
tcSplitForAllTys :: Type -> ([TyVar], Type)
-tcSplitForAllTys ty = ASSERT( all isTyVar (fst sty) ) sty
+tcSplitForAllTys ty
+ = ASSERT( all isTyVar (fst sty) ) sty
where sty = splitForAllTys ty
-- | Like 'tcSplitForAllTys', but splits off only named binders.
@@ -1720,8 +1644,8 @@ tcEqType :: HasDebugCallStack => TcType -> TcType -> Bool
-- equality] (in TyCoRep) as `eqType`, but Type.eqType believes (* ==
-- Constraint), and that is NOT what we want in the type checker!
tcEqType ty1 ty2
- = isNothing (tc_eq_type tcView ki1 ki2) &&
- isNothing (tc_eq_type tcView ty1 ty2)
+ = tc_eq_type False False ki1 ki2
+ && tc_eq_type False False ty1 ty2
where
ki1 = tcTypeKind ty1
ki2 = tcTypeKind ty2
@@ -1730,93 +1654,85 @@ tcEqType ty1 ty2
-- as long as their non-coercion structure is identical.
tcEqTypeNoKindCheck :: TcType -> TcType -> Bool
tcEqTypeNoKindCheck ty1 ty2
- = isNothing $ tc_eq_type tcView ty1 ty2
-
--- | Like 'tcEqType', but returns information about whether the difference
--- is visible in the case of a mismatch.
--- @Nothing@ : the types are equal
--- @Just True@ : the types differ, and the point of difference is visible
--- @Just False@ : the types differ, and the point of difference is invisible
-tcEqTypeVis :: TcType -> TcType -> Maybe Bool
-tcEqTypeVis ty1 ty2
- = tc_eq_type tcView ty1 ty2 <!> invis (tc_eq_type tcView ki1 ki2)
- where
- ki1 = tcTypeKind ty1
- ki2 = tcTypeKind ty2
+ = tc_eq_type False False ty1 ty2
+
+-- | Like 'tcEqType', but returns True if the /visible/ part of the types
+-- are equal, even if they are really unequal (in the invisible bits)
+tcEqTypeVis :: TcType -> TcType -> Bool
+tcEqTypeVis ty1 ty2 = tc_eq_type False True ty1 ty2
+
+-- | Like 'pickyEqTypeVis', but returns a Bool for convenience
+pickyEqType :: TcType -> TcType -> Bool
+-- Check when two types _look_ the same, _including_ synonyms.
+-- So (pickyEqType String [Char]) returns False
+-- This ignores kinds and coercions, because this is used only for printing.
+pickyEqType ty1 ty2 = tc_eq_type True False ty1 ty2
- -- convert Just True to Just False
- invis :: Maybe Bool -> Maybe Bool
- invis = fmap (const False)
-(<!>) :: Maybe Bool -> Maybe Bool -> Maybe Bool
-Nothing <!> x = x
-Just True <!> _ = Just True
-Just _vis <!> Just True = Just True
-Just vis <!> _ = Just vis
-infixr 3 <!>
-- | Real worker for 'tcEqType'. No kind check!
-tc_eq_type :: (TcType -> Maybe TcType) -- ^ @tcView@, if you want unwrapping
- -> Type -> Type -> Maybe Bool
-tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
+tc_eq_type :: Bool -- ^ True <=> do not expand type synonyms
+ -> Bool -- ^ True <=> compare visible args only
+ -> Type -> Type
+ -> Bool
+-- Flags False, False is the usual setting for tc_eq_type
+tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
+ = go orig_env orig_ty1 orig_ty2
where
- go :: Bool -> RnEnv2 -> Type -> Type -> Maybe Bool
- go vis env t1 t2 | Just t1' <- view_fun t1 = go vis env t1' t2
- go vis env t1 t2 | Just t2' <- view_fun t2 = go vis env t1 t2'
+ go :: RnEnv2 -> Type -> Type -> Bool
+ go env t1 t2 | not keep_syns, Just t1' <- tcView t1 = go env t1' t2
+ go env t1 t2 | not keep_syns, Just t2' <- tcView t2 = go env t1 t2'
+
+ go env (TyVarTy tv1) (TyVarTy tv2)
+ = rnOccL env tv1 == rnOccR env tv2
- go vis env (TyVarTy tv1) (TyVarTy tv2)
- = check vis $ rnOccL env tv1 == rnOccR env tv2
+ go _ (LitTy lit1) (LitTy lit2)
+ = lit1 == lit2
- go vis _ (LitTy lit1) (LitTy lit2)
- = check vis $ lit1 == lit2
+ go env (ForAllTy (Bndr tv1 vis1) ty1)
+ (ForAllTy (Bndr tv2 vis2) ty2)
+ = vis1 == vis2
+ && (vis_only || go env (varType tv1) (varType tv2))
+ && go (rnBndr2 env tv1 tv2) ty1 ty2
- go vis env (ForAllTy (Bndr tv1 vis1) ty1)
- (ForAllTy (Bndr tv2 vis2) ty2)
- = go (isVisibleArgFlag vis1) env (varType tv1) (varType tv2)
- <!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
- <!> check vis (vis1 == vis2)
-- Make sure we handle all FunTy cases since falling through to the
-- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
-- kind variable, which causes things to blow up.
- go vis env (FunTy arg1 res1) (FunTy arg2 res2)
- = go vis env arg1 arg2 <!> go vis env res1 res2
- go vis env ty (FunTy arg res)
- = eqFunTy vis env arg res ty
- go vis env (FunTy arg res) ty
- = eqFunTy vis env arg res ty
+ go env (FunTy arg1 res1) (FunTy arg2 res2)
+ = go env arg1 arg2 && go env res1 res2
+ go env ty (FunTy arg res) = eqFunTy env arg res ty
+ go env (FunTy arg res) ty = eqFunTy env arg res ty
-- See Note [Equality on AppTys] in Type
- go vis env (AppTy s1 t1) ty2
+ go env (AppTy s1 t1) ty2
| Just (s2, t2) <- tcRepSplitAppTy_maybe ty2
- = go vis env s1 s2 <!> go vis env t1 t2
- go vis env ty1 (AppTy s2 t2)
+ = go env s1 s2 && go env t1 t2
+ go env ty1 (AppTy s2 t2)
| Just (s1, t1) <- tcRepSplitAppTy_maybe ty1
- = go vis env s1 s2 <!> go vis env t1 t2
- go vis env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
- = check vis (tc1 == tc2) <!> gos (tc_vis vis tc1) env ts1 ts2
- go vis env (CastTy t1 _) t2 = go vis env t1 t2
- go vis env t1 (CastTy t2 _) = go vis env t1 t2
- go _ _ (CoercionTy {}) (CoercionTy {}) = Nothing
- go vis _ _ _ = Just vis
-
- gos _ _ [] [] = Nothing
- gos (v:vs) env (t1:ts1) (t2:ts2) = go v env t1 t2 <!> gos vs env ts1 ts2
- gos (v:_) _ _ _ = Just v
- gos _ _ _ _ = panic "tc_eq_type"
-
- tc_vis :: Bool -> TyCon -> [Bool]
- tc_vis True tc = viss ++ repeat True
- -- the repeat True is necessary because tycons can legitimately
- -- be oversaturated
+ = go env s1 s2 && go env t1 t2
+
+ go env (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ = tc1 == tc2 && gos env (tc_vis tc1) ts1 ts2
+
+ go env (CastTy t1 _) t2 = go env t1 t2
+ go env t1 (CastTy t2 _) = go env t1 t2
+ go _ (CoercionTy {}) (CoercionTy {}) = True
+
+ go _ _ _ = False
+
+ gos _ _ [] [] = True
+ gos env (ig:igs) (t1:ts1) (t2:ts2) = (ig || go env t1 t2)
+ && gos env igs ts1 ts2
+ gos _ _ _ _ = False
+
+ tc_vis :: TyCon -> [Bool] -- True for the fields we should ignore
+ tc_vis tc | vis_only = inviss ++ repeat False -- Ignore invisibles
+ | otherwise = repeat False -- Ignore nothing
+ -- The repeat False is necessary because tycons
+ -- can legitimately be oversaturated
where
bndrs = tyConBinders tc
- viss = map isVisibleTyConBinder bndrs
- tc_vis False _ = repeat False -- if we're not in a visible context, our args
- -- aren't either
-
- check :: Bool -> Bool -> Maybe Bool
- check _ True = Nothing
- check vis False = Just vis
+ inviss = map isInvisibleTyConBinder bndrs
orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
@@ -1826,30 +1742,19 @@ tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
-- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
-- res is unzonked/unflattened. Thus this function, which handles this
-- corner case.
- eqFunTy :: Bool -> RnEnv2 -> Type -> Type -> Type -> Maybe Bool
- eqFunTy vis env arg res (FunTy arg' res')
- = go vis env arg arg' <!> go vis env res res'
- eqFunTy vis env arg res ty@(AppTy{})
- | Just (tc, [_, _, arg', res']) <- get_args ty []
- , tc == funTyCon
- = go vis env arg arg' <!> go vis env res res'
+ eqFunTy :: RnEnv2 -> Type -> Type -> Type -> Bool
+ -- Last arg is /not/ FunTy
+ eqFunTy env arg res ty@(AppTy{}) = get_args ty []
where
- get_args :: Type -> [Type] -> Maybe (TyCon, [Type])
+ get_args :: Type -> [Type] -> Bool
get_args (AppTy f x) args = get_args f (x:args)
get_args (CastTy t _) args = get_args t args
- get_args (TyConApp tc tys) args = Just (tc, tys ++ args)
- get_args _ _ = Nothing
- eqFunTy vis _ _ _ _
- = Just vis
-
--- | Like 'pickyEqTypeVis', but returns a Bool for convenience
-pickyEqType :: TcType -> TcType -> Bool
--- Check when two types _look_ the same, _including_ synonyms.
--- So (pickyEqType String [Char]) returns False
--- This ignores kinds and coercions, because this is used only for printing.
-pickyEqType ty1 ty2
- = isNothing $
- tc_eq_type (const Nothing) ty1 ty2
+ get_args (TyConApp tc tys) args
+ | tc == funTyCon
+ , [_, _, arg', res'] <- tys ++ args
+ = go env arg arg' && go env res res'
+ get_args _ _ = False
+ eqFunTy _ _ _ _ = False
{- *********************************************************************
* *
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index f51c7241a8..6af873e036 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -790,7 +790,7 @@ tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected
inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual
- -- if we haven't recurred through an arrow, then
+ -- If we haven't recurred through an arrow, then
-- the eq_orig will list ty_actual. In this case,
-- we want to update the origin to reflect the
-- instantiation. If we *have* recurred through
@@ -1450,12 +1450,12 @@ uType t_or_k origin orig_ty1 orig_ty2
go (AppTy s1 t1) (TyConApp tc2 ts2)
| Just (ts2', t2') <- snocView ts2
- = ASSERT( mightBeUnsaturatedTyCon tc2 )
+ = ASSERT( not (mustBeSaturated tc2) )
go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2'
go (TyConApp tc1 ts1) (AppTy s2 t2)
| Just (ts1', t1') <- snocView ts1
- = ASSERT( mightBeUnsaturatedTyCon tc1 )
+ = ASSERT( not (mustBeSaturated tc1) )
go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2
go (CoercionTy co1) (CoercionTy co2)
@@ -2019,37 +2019,43 @@ we return a made-up TcTyVarDetails, but I think it works smoothly.
-}
-- | Breaks apart a function kind into its pieces.
-matchExpectedFunKind :: Outputable fun
- => fun -- ^ type, only for errors
- -> TcKind -- ^ function kind
- -> TcM (Coercion, TcKind, TcKind)
- -- ^ co :: old_kind ~ arg -> res
-matchExpectedFunKind hs_ty = go
+matchExpectedFunKind
+ :: Outputable fun
+ => fun -- ^ type, only for errors
+ -> Arity -- ^ n: number of desired arrows
+ -> TcKind -- ^ fun_ kind
+ -> TcM Coercion -- ^ co :: fun_kind ~ (arg1 -> ... -> argn -> res)
+
+matchExpectedFunKind hs_ty n k = go n k
where
- go k | Just k' <- tcView k = go k'
+ go 0 k = return (mkNomReflCo k)
- go k@(TyVarTy kvar)
+ go n k | Just k' <- tcView k = go n k'
+
+ go n k@(TyVarTy kvar)
| isMetaTyVar kvar
= do { maybe_kind <- readMetaTyVar kvar
; case maybe_kind of
- Indirect fun_kind -> go fun_kind
- Flexi -> defer k }
+ Indirect fun_kind -> go n fun_kind
+ Flexi -> defer n k }
+
+ go n (FunTy arg res)
+ = do { co <- go (n-1) res
+ ; return (mkTcFunCo Nominal (mkTcNomReflCo arg) co) }
- go k@(FunTy arg res) = return (mkNomReflCo k, arg, res)
- go other = defer other
+ go n other
+ = defer n other
- defer k
- = do { arg_kind <- newMetaKindVar
- ; res_kind <- newMetaKindVar
- ; let new_fun = mkFunTy arg_kind res_kind
+ defer n k
+ = do { arg_kinds <- newMetaKindVars n
+ ; res_kind <- newMetaKindVar
+ ; let new_fun = mkFunTys arg_kinds res_kind
origin = TypeEqOrigin { uo_actual = k
, uo_expected = new_fun
, uo_thing = Just (ppr hs_ty)
, uo_visible = True
}
- ; co <- uType KindLevel origin k new_fun
- ; return (co, arg_kind, res_kind) }
-
+ ; uType KindLevel origin k new_fun }
{- *********************************************************************
* *
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 7bb85740ac..733c11977e 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -430,7 +430,7 @@ splitAppCo_maybe (TyConAppCo r tc args)
, Just (args', arg') <- snocView args
= Just ( mkTyConAppCo r tc args', arg' )
- | mightBeUnsaturatedTyCon tc
+ | not (mustBeSaturated tc)
-- Never create unsaturated type family apps!
, Just (args', arg') <- snocView args
, Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 1d48ed05b5..0e9a599573 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -1159,7 +1159,7 @@ etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
= ASSERT( tc == tc2 ) Just cos2
etaTyConAppCo_maybe tc co
- | mightBeUnsaturatedTyCon tc
+ | not (mustBeSaturated tc)
, (Pair ty1 ty2, r) <- coercionKindRole co
, Just (tc1, tys1) <- splitTyConApp_maybe ty1
, Just (tc2, tys2) <- splitTyConApp_maybe ty2
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index f7c21b7626..8dead3042d 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -917,8 +917,9 @@ isLiftedRuntimeRep rep
isUnliftedRuntimeRep rep
| Just rep' <- coreView rep = isUnliftedRuntimeRep rep'
- | TyConApp rr_tc args <- rep
- , isUnliftedRuntimeRepTyCon rr_tc = ASSERT( null args ) True
+ | TyConApp rr_tc _ <- rep -- NB: args might be non-empty
+ -- e.g. TupleRep
+ , isUnliftedRuntimeRepTyCon rr_tc = True
| otherwise = False
isUnliftedRuntimeRepTyCon :: TyCon -> Bool
@@ -3448,6 +3449,8 @@ pprPrecTypeX env prec ty
if debugStyle sty -- Use debugPprType when in
then debug_ppr_ty prec ty -- when in debug-style
else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty)
+ -- NB: debug-style is used for -dppr-debug
+ -- dump-style is used for -ddump-tc-trace etc
pprTyLit :: TyLit -> SDoc
pprTyLit = pprIfaceTyLit . toIfaceTyLit
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index eb0b84d47e..058f090f59 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -50,7 +50,7 @@ module TyCon(
isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
isUnboxedSumTyCon, isPromotedTupleTyCon,
isTypeSynonymTyCon,
- mightBeUnsaturatedTyCon,
+ mustBeSaturated,
isPromotedDataCon, isPromotedDataCon_maybe,
isKindTyCon, isLiftedTypeKindTyConName,
isTauTyCon, isFamFreeTyCon,
@@ -69,7 +69,8 @@ module TyCon(
isTyConAssoc, tyConAssoc_maybe, tyConFlavourAssoc_maybe,
isImplicitTyCon,
isTyConWithSrcDataCons,
- isTcTyCon, isTcLevPoly,
+ isTcTyCon, setTcTyConKind,
+ isTcLevPoly,
-- ** Extracting information out of TyCons
tyConName,
@@ -108,7 +109,7 @@ module TyCon(
pprPromotionQuote, mkTyConKind,
-- ** Predicated on TyConFlavours
- tcFlavourCanBeUnsaturated, tcFlavourIsOpen,
+ tcFlavourIsOpen,
-- * Runtime type representation
TyConRepName, tyConRepName_maybe,
@@ -1930,11 +1931,11 @@ isFamFreeTyCon _ = True
-- (T ~N d), (a ~N e) and (b ~N f)?
-- Specifically NOT true of synonyms (open and otherwise)
--
--- It'd be unusual to call mightBeUnsaturatedTyCon on a regular H98
+-- It'd be unusual to call mustBeSaturated on a regular H98
-- type synonym, because you should probably have expanded it first
-- But regardless, it's not decomposable
-mightBeUnsaturatedTyCon :: TyCon -> Bool
-mightBeUnsaturatedTyCon = tcFlavourCanBeUnsaturated . tyConFlavour
+mustBeSaturated :: TyCon -> Bool
+mustBeSaturated = tcFlavourMustBeSaturated . tyConFlavour
-- | Is this an algebraic 'TyCon' declared with the GADT syntax?
isGadtSyntaxTyCon :: TyCon -> Bool
@@ -2131,6 +2132,14 @@ isTcTyCon :: TyCon -> Bool
isTcTyCon (TcTyCon {}) = True
isTcTyCon _ = False
+setTcTyConKind :: TyCon -> Kind -> TyCon
+-- Update the Kind of a TcTyCon
+-- The new kind is always a zonked version of its previous
+-- kind, so we don't need to update any other fields.
+-- See Note [The Purely Kinded Invariant] in TcHsType
+setTcTyConKind tc@(TcTyCon {}) kind = tc { tyConKind = kind }
+setTcTyConKind tc _ = pprPanic "setTcTyConKind" (ppr tc)
+
-- | Could this TyCon ever be levity-polymorphic when fully applied?
-- True is safe. False means we're sure. Does only a quick check
-- based on the TyCon's category.
@@ -2504,19 +2513,19 @@ tyConFlavour (PromotedDataCon {}) = PromotedDataConFlavour
tyConFlavour (TcTyCon { tcTyConFlavour = flav }) = flav
-- | Can this flavour of 'TyCon' appear unsaturated?
-tcFlavourCanBeUnsaturated :: TyConFlavour -> Bool
-tcFlavourCanBeUnsaturated ClassFlavour = True
-tcFlavourCanBeUnsaturated DataTypeFlavour = True
-tcFlavourCanBeUnsaturated NewtypeFlavour = True
-tcFlavourCanBeUnsaturated DataFamilyFlavour{} = True
-tcFlavourCanBeUnsaturated TupleFlavour{} = True
-tcFlavourCanBeUnsaturated SumFlavour = True
-tcFlavourCanBeUnsaturated AbstractTypeFlavour = True
-tcFlavourCanBeUnsaturated BuiltInTypeFlavour = True
-tcFlavourCanBeUnsaturated PromotedDataConFlavour = True
-tcFlavourCanBeUnsaturated TypeSynonymFlavour = False
-tcFlavourCanBeUnsaturated OpenTypeFamilyFlavour{} = False
-tcFlavourCanBeUnsaturated ClosedTypeFamilyFlavour = False
+tcFlavourMustBeSaturated :: TyConFlavour -> Bool
+tcFlavourMustBeSaturated ClassFlavour = False
+tcFlavourMustBeSaturated DataTypeFlavour = False
+tcFlavourMustBeSaturated NewtypeFlavour = False
+tcFlavourMustBeSaturated DataFamilyFlavour{} = False
+tcFlavourMustBeSaturated TupleFlavour{} = False
+tcFlavourMustBeSaturated SumFlavour = False
+tcFlavourMustBeSaturated AbstractTypeFlavour = False
+tcFlavourMustBeSaturated BuiltInTypeFlavour = False
+tcFlavourMustBeSaturated PromotedDataConFlavour = False
+tcFlavourMustBeSaturated TypeSynonymFlavour = True
+tcFlavourMustBeSaturated OpenTypeFamilyFlavour{} = True
+tcFlavourMustBeSaturated ClosedTypeFamilyFlavour = True
-- | Is this flavour of 'TyCon' an open type family or a data family?
tcFlavourIsOpen :: TyConFlavour -> Bool
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 142da4c79c..6590489b01 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -539,9 +539,11 @@ data TyCoMapper env m
-- ^ The returned env is used in the extended scope
, tcm_tycon :: TyCon -> m TyCon
- -- ^ This is used only to turn 'TcTyCon's into 'TyCon's.
- -- See Note [Type checking recursive type and class declarations]
- -- in TcTyClsDecls
+ -- ^ This is used only for TcTyCons
+ -- a) To zonk TcTyCons
+ -- b) To turn TcTyCons into TyCons.
+ -- See Note [Type checking recursive type and class declarations]
+ -- in TcTyClsDecls
}
{-# INLINABLE mapType #-} -- See Note [Specialising mappers]
@@ -553,12 +555,18 @@ mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
where
go (TyVarTy tv) = tyvar env tv
go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
- go t@(TyConApp tc []) | not (isTcTyCon tc)
- = return t -- avoid allocation in this exceedingly
- -- common case (mostly, for *)
- go (TyConApp tc tys)
+ go ty@(TyConApp tc tys)
+ | isTcTyCon tc
= do { tc' <- tycon tc
; mktyconapp tc' <$> mapM go tys }
+
+ -- Not a TcTyCon
+ | null tys -- Avoid allocation in this very
+ = return ty -- common case (E.g. Int, LiftedRep etc)
+
+ | otherwise
+ = mktyconapp tc <$> mapM go tys
+
go (FunTy arg res) = FunTy <$> go arg <*> go res
go (ForAllTy (Bndr tv vis) inner)
= do { (env', tv') <- tycobinder env tv vis
@@ -587,7 +595,9 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
go (Refl ty) = Refl <$> mapType mapper env ty
go (GRefl r ty mco) = mkgreflco r <$> mapType mapper env ty <*> (go_mco mco)
go (TyConAppCo r tc args)
- = do { tc' <- tycon tc
+ = do { tc' <- if isTcTyCon tc
+ then tycon tc
+ else return tc
; mktyconappco r tc' <$> mapM go args }
go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
go (ForAllCo tv kind_co co)
@@ -720,6 +730,10 @@ mkAppTy ty1 ty2 = AppTy ty1 ty2
--
-- Here Id is partially applied in the type sig for Foo,
-- but once the type synonyms are expanded all is well
+ --
+ -- Moreover in TcHsTypes.tcInferApps we build up a type
+ -- (T t1 t2 t3) one argument at a type, thus forming
+ -- (T t1), (T t1 t2), etc
mkAppTys :: Type -> [Type] -> Type
mkAppTys ty1 [] = ty1
@@ -758,7 +772,7 @@ repSplitAppTy_maybe (AppTy ty1 ty2)
= Just (ty1, ty2)
repSplitAppTy_maybe (TyConApp tc tys)
- | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
+ | not (mustBeSaturated tc) || tys `lengthExceeds` tyConArity tc
, Just (tys', ty') <- snocView tys
= Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
@@ -770,6 +784,8 @@ repSplitAppTy_maybe _other = Nothing
tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
-- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
-- any coreView stuff is already done. Refuses to look through (c => t)
+-- The "Rep" means that we assumes that any tcView stuff is already done.
+-- Refuses to look through (c => t)
tcRepSplitAppTy_maybe (FunTy ty1 ty2)
| isPredTy ty1
= Nothing -- See Note [Decomposing fat arrow c=>t]
@@ -782,13 +798,14 @@ tcRepSplitAppTy_maybe (FunTy ty1 ty2)
tcRepSplitAppTy_maybe (AppTy ty1 ty2) = Just (ty1, ty2)
tcRepSplitAppTy_maybe (TyConApp tc tys)
- | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
+ | not (mustBeSaturated tc) || tys `lengthExceeds` tyConArity tc
, Just (tys', ty') <- snocView tys
= Just (TyConApp tc tys', ty') -- Never create unsaturated type family apps!
tcRepSplitAppTy_maybe _other = Nothing
-- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+-- The "Rep" means that we assumes that any tcView stuff is already done.
-- Defined here to avoid module loops between Unify and TcType.
tcRepSplitTyConApp_maybe (TyConApp tc tys)
= Just (tc, tys)
@@ -804,6 +821,7 @@ tcRepSplitTyConApp_maybe _
-- | Like 'tcSplitTyConApp' but doesn't look through type synonyms.
tcRepSplitTyConApp :: HasCallStack => Type -> (TyCon, [Type])
+-- The "Rep" means that we assumes that any tcView stuff is already done.
-- Defined here to avoid module loops between Unify and TcType.
tcRepSplitTyConApp ty =
case tcRepSplitTyConApp_maybe ty of
@@ -829,8 +847,8 @@ splitAppTys ty = split ty ty []
split _ (AppTy ty arg) args = split ty ty (arg:args)
split _ (TyConApp tc tc_args) args
= let -- keep type families saturated
- n | mightBeUnsaturatedTyCon tc = 0
- | otherwise = tyConArity tc
+ n | mustBeSaturated tc = tyConArity tc
+ | otherwise = 0
(tc_args1, tc_args2) = splitAt n tc_args
in
(TyConApp tc tc_args1, tc_args2 ++ args)
@@ -849,8 +867,8 @@ repSplitAppTys ty = split ty []
where
split (AppTy ty arg) args = split ty (arg:args)
split (TyConApp tc tc_args) args
- = let n | mightBeUnsaturatedTyCon tc = 0
- | otherwise = tyConArity tc
+ = let n | mustBeSaturated tc = tyConArity tc
+ | otherwise = 0
(tc_args1, tc_args2) = splitAt n tc_args
in
(TyConApp tc tc_args1, tc_args2 ++ args)
@@ -967,9 +985,6 @@ In the compiler we maintain the invariant that all saturated applications of
See #11714.
-}
-isFunTy :: Type -> Bool
-isFunTy ty = isJust (splitFunTy_maybe ty)
-
splitFunTy :: Type -> (Type, Type)
-- ^ Attempts to extract the argument and result types from a type, and
-- panics if that is not possible. See also 'splitFunTy_maybe'
@@ -1011,6 +1026,8 @@ piResultTy ty arg = case piResultTy_maybe ty arg of
Nothing -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
piResultTy_maybe :: Type -> Type -> Maybe Type
+-- We don't need a 'tc' version, because
+-- this function behaves the same for Type and Constraint
piResultTy_maybe ty arg
| Just ty' <- coreView ty = piResultTy_maybe ty' arg
@@ -1460,11 +1477,17 @@ isForAllTy_co _ = False
-- | Is this a function or forall?
isPiTy :: Type -> Bool
-isPiTy ty | Just ty' <- coreView ty = isForAllTy ty'
+isPiTy ty | Just ty' <- coreView ty = isPiTy ty'
isPiTy (ForAllTy {}) = True
isPiTy (FunTy {}) = True
isPiTy _ = False
+-- | Is this a function?
+isFunTy :: Type -> Bool
+isFunTy ty | Just ty' <- coreView ty = isFunTy ty'
+isFunTy (FunTy {}) = True
+isFunTy _ = False
+
-- | Take a forall type apart, or panics if that is not possible.
splitForAllTy :: Type -> (TyCoVar, Type)
splitForAllTy ty
@@ -2705,6 +2728,7 @@ Note that:
-----------------------------
typeKind :: HasDebugCallStack => Type -> Kind
+-- No need to expand synonyms
typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
typeKind (LitTy l) = typeLiteralKind l
typeKind (FunTy {}) = liftedTypeKind
@@ -2732,6 +2756,7 @@ typeKind ty@(ForAllTy {})
-----------------------------
tcTypeKind :: HasDebugCallStack => Type -> Kind
+-- No need to expand synonyms
tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
tcTypeKind (LitTy l) = typeLiteralKind l
tcTypeKind (TyVarTy tyvar) = tyVarKind tyvar
@@ -2739,8 +2764,8 @@ tcTypeKind (CastTy _ty co) = pSnd $ coercionKind co
tcTypeKind (CoercionTy co) = coercionType co
tcTypeKind (FunTy arg res)
- | isPredTy arg && isPredTy res = constraintKind
- | otherwise = liftedTypeKind
+ | isPredTy arg, isPredTy res = constraintKind
+ | otherwise = liftedTypeKind
tcTypeKind (AppTy fun arg)
= go fun [arg]
@@ -2765,16 +2790,14 @@ tcTypeKind ty@(ForAllTy {})
body_kind = tcTypeKind body
-isPredTy :: Type -> Bool
+isPredTy :: HasDebugCallStack => Type -> Bool
-- See Note [Types for coercions, predicates, and evidence]
isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
--------------------------
typeLiteralKind :: TyLit -> Kind
-typeLiteralKind l =
- case l of
- NumTyLit _ -> typeNatKind
- StrTyLit _ -> typeSymbolKind
+typeLiteralKind (NumTyLit {}) = typeNatKind
+typeLiteralKind (StrTyLit {}) = typeSymbolKind
-- | Returns True if a type is levity polymorphic. Should be the same
-- as (isKindLevPoly . typeKind) but much faster.
diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot
index 84fbaca6f7..d9ea519a08 100644
--- a/compiler/types/Type.hs-boot
+++ b/compiler/types/Type.hs-boot
@@ -8,7 +8,7 @@ import Var ( TyCoVar )
import {-# SOURCE #-} TyCoRep( Type, Coercion )
import Util
-isPredTy :: Type -> Bool
+isPredTy :: HasDebugCallStack => Type -> Bool
isCoercionTy :: Type -> Bool
mkAppTy :: Type -> Type -> Type
diff --git a/compiler/utils/Outputable.hs b/compiler/utils/Outputable.hs
index b3d77aa843..768d247bf0 100644
--- a/compiler/utils/Outputable.hs
+++ b/compiler/utils/Outputable.hs
@@ -1199,7 +1199,7 @@ pprTraceException heading doc =
pprSTrace :: HasCallStack => SDoc -> a -> a
pprSTrace doc = pprTrace "" (doc $$ callStackDoc)
-warnPprTrace :: Bool -> String -> Int -> SDoc -> a -> a
+warnPprTrace :: HasCallStack => Bool -> String -> Int -> SDoc -> a -> a
-- ^ Just warn about an assertion failure, recording the given file and line number.
-- Should typically be accessed with the WARN macros
warnPprTrace _ _ _ _ x | not debugIsOn = x
@@ -1207,7 +1207,9 @@ warnPprTrace _ _file _line _msg x
| hasNoDebugOutput unsafeGlobalDynFlags = x
warnPprTrace False _file _line _msg x = x
warnPprTrace True file line msg x
- = pprDebugAndThen unsafeGlobalDynFlags trace heading msg x
+ = pprDebugAndThen unsafeGlobalDynFlags trace heading
+ (msg $$ callStackDoc )
+ x
where
heading = hsep [text "WARNING: file", text file <> comma, text "line", int line]
diff --git a/compiler/utils/Outputable.hs-boot b/compiler/utils/Outputable.hs-boot
index ad7d091833..fb3c173a33 100644
--- a/compiler/utils/Outputable.hs-boot
+++ b/compiler/utils/Outputable.hs-boot
@@ -1,11 +1,12 @@
module Outputable where
import GhcPrelude
+import GHC.Stack( HasCallStack )
data SDoc
showSDocUnsafe :: SDoc -> String
-warnPprTrace :: Bool -> String -> Int -> SDoc -> a -> a
+warnPprTrace :: HasCallStack => Bool -> String -> Int -> SDoc -> a -> a
text :: String -> SDoc
diff --git a/testsuite/tests/ghci/should_fail/T16287.stderr b/testsuite/tests/ghci/should_fail/T16287.stderr
index 13f0852144..8b0f882ab7 100644
--- a/testsuite/tests/ghci/should_fail/T16287.stderr
+++ b/testsuite/tests/ghci/should_fail/T16287.stderr
@@ -2,11 +2,16 @@
<interactive>:1:1: error:
The type synonym ‘F1’ should have 1 argument, but has been given none
-<interactive>:1:1: error:
- The type family ‘F2’ should have no arguments, but has been given none
+<interactive>:1:4: error:
+ • Expected kind ‘forall k. k’, but ‘F2’ has kind ‘k0’
+ • In the first argument of ‘T2’, namely ‘F2’
+ In the type ‘T2 F2’
<interactive>:1:1: error:
The type synonym ‘F1’ should have 1 argument, but has been given none
-<interactive>:1:1: error:
- The type family ‘F2’ should have no arguments, but has been given none
+<interactive>:1:11: error:
+ • Expected kind ‘forall k. k’, but ‘F2’ has kind ‘k0’
+ • In the first argument of ‘T2’, namely ‘F2’
+ In the first argument of ‘Maybe’, namely ‘(T2 F2)’
+ In the type ‘Maybe (T2 F2)’
View Lorry Controller Status