summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2018-12-24 14:55:41 +0000
committerSimon Peyton Jones <simonpj@microsoft.com>2018-12-24 14:55:41 +0000
commitf4449232e43784abff325bd3bf90f3cb5857b28b (patch)
tree5babde190babb2af2385d3dc5f97d20e1cac5343
parent79d031326d614f6ca637b67a11949dab64afe728 (diff)
downloadhaskell-f4449232e43784abff325bd3bf90f3cb5857b28b.tar.gz
Make tcTypeKind monadic
This patch is work in progress on Trac #15952. IT DOES NOT COMPILE. The main payload is progress towards making tcTypeKind monadic. However I have not yet made a monadic version of tcEqType, nor changed all those tcEqType calls to a monadic context. Hence, it won't compile as-is. I'm just parking the work I've done, on a branch, until I've had a chance to agree the path with Richard. (The previous patches on this branch /do/ compile and almost-completely validate.)
Diffstat
-rw-r--r--compiler/typecheck/FamInst.hs12
-rw-r--r--compiler/typecheck/Inst.hs29
-rw-r--r--compiler/typecheck/TcCanonical.hs94
-rw-r--r--compiler/typecheck/TcDeriv.hs49
-rw-r--r--compiler/typecheck/TcDerivInfer.hs25
-rw-r--r--compiler/typecheck/TcErrors.hs21
-rw-r--r--compiler/typecheck/TcExpr.hs8
-rw-r--r--compiler/typecheck/TcFlatten.hs35
-rw-r--r--compiler/typecheck/TcHsSyn.hs10
-rw-r--r--compiler/typecheck/TcHsType.hs31
-rw-r--r--compiler/typecheck/TcInstDcls.hs2
-rw-r--r--compiler/typecheck/TcInteract.hs6
-rw-r--r--compiler/typecheck/TcMType.hs249
-rw-r--r--compiler/typecheck/TcPat.hs3
-rw-r--r--compiler/typecheck/TcPatSyn.hs42
-rw-r--r--compiler/typecheck/TcRnDriver.hs9
-rw-r--r--compiler/typecheck/TcSMonad.hs13
-rw-r--r--compiler/typecheck/TcSplice.hs6
-rw-r--r--compiler/typecheck/TcTyClsDecls.hs17
-rw-r--r--compiler/typecheck/TcType.hs166
-rw-r--r--compiler/typecheck/TcUnify.hs32
-rw-r--r--compiler/types/Type.hs37
22 files changed, 551 insertions, 345 deletions
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index 144b315bed..4f32065d37 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -155,8 +155,14 @@ newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcM FamInst
newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
= ASSERT2( tyCoVarsOfTypes lhs `subVarSet` tcv_set, text "lhs" <+> pp_ax )
ASSERT2( tyCoVarsOfType rhs `subVarSet` tcv_set, text "rhs" <+> pp_ax )
- ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
- do { (subst, tvs') <- freshenTyVarBndrs tvs
+ do { when debugIsOn $
+ do { lhs_kind <- tcTypeKindM (mkTyConApp fam_tc lhs)
+ ; rhs_kind <- tcTypeKindM rhs
+ ; ASSERT2( lhs_kind `eqType` rhs_kind,
+ text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind )
+ return () }
+
+ ; (subst, tvs') <- freshenTyVarBndrs tvs
; (subst, cvs') <- freshenCoVarBndrsX subst cvs
; dflags <- getDynFlags
; let lhs' = substTys subst lhs
@@ -187,8 +193,6 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
, fi_rhs = rhs'
, fi_axiom = axiom }) }
where
- lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs)
- rhs_kind = tcTypeKind rhs
tcv_set = mkVarSet (tvs ++ cvs)
pp_ax = pprCoAxiom axiom
CoAxBranch { cab_tvs = tvs
diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index dd8f8ba03c..cb49073a57 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -298,14 +298,13 @@ instTyVarsWith orig tvs tys
go subst [] []
= return subst
go subst (tv:tvs) (ty:tys)
- | tv_kind `tcEqType` ty_kind
- = go (extendTCvSubst subst tv ty) tvs tys
- | otherwise
- = do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind
- ; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys }
- where
- tv_kind = substTy subst (tyVarKind tv)
- ty_kind = tcTypeKind ty
+ = do { let tv_kind = substTy subst (tyVarKind tv)
+ ; ty_kind <- tcTypeKindM ty
+ ; eq_kind <- tv_kind `tcEqTypeM` ty_kind
+ ; ty' <- if eq_kind then return ty
+ else do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind
+ ; return (ty `mkCastTy` co) }
+ ; go (extendTCvSubst subst tv ty') tvs tys }
go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
@@ -580,17 +579,17 @@ tcInstTyBinder _ subst (Anon ty)
mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
-- monadic just for convenience with mkEqBoxTy
mkHEqBoxTy co ty1 ty2
- = return $
- mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
- where k1 = tcTypeKind ty1
- k2 = tcTypeKind ty2
+ = do { k1 <- tcTypeKindM ty1
+ ; k2 <- tcTypeKindM ty2
+ ; return $ mkTyConApp (promoteDataCon heqDataCon)
+ [k1, k2, ty1, ty2, mkCoercionTy co] }
-- | This takes @a ~# b@ and returns @a ~ b@.
mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
mkEqBoxTy co ty1 ty2
- = return $
- mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
- where k = tcTypeKind ty1
+ = do { k <- tcTypeKindM ty1
+ ; return $ mkTyConApp (promoteDataCon eqDataCon)
+ [k, ty1, ty2, mkCoercionTy co] }
{-
************************************************************************
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index dce9a10aff..5d9aabeaf0 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -873,16 +873,17 @@ 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]
-- Check only when flat because the zonk_eq_types check in canEqNC takes
-- care of the non-flat case.
can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
- | ty1 `tcEqType` ty2
+ | ty1 `tcEqType` ty2 -- In the flat case ty1 and ty2 are zonked,
+ -- so it's ok to use the non-monadic tcEqType
= canEqReflexive ev ReprEq ty1
-- When working with ReprEq, unwrap newtypes.
@@ -1038,17 +1039,16 @@ can_eq_nc_forall ev eq_rel s1 s2
-- This version returns the wanted constraint rather
-- than putting it in the work list
unify loc role ty1 ty2
- | ty1 `tcEqType` ty2
- = return (mkTcReflCo role ty1, emptyBag)
- | otherwise
- = do { (wanted, co) <- newWantedEq loc role ty1 ty2
- ; return (co, unitBag (mkNonCanonical wanted)) }
+ = do { already_eq <- ty1 `tcEqTypeM` ty2
+ ; if already_eq then return (mkTcReflCo role ty1, emptyBag)
+ else do { (wanted, co) <- newWantedEq loc role ty1 ty2
+ ; return (co, unitBag (mkNonCanonical wanted)) } }
---------------------------------
-- | 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.
@@ -1304,11 +1304,13 @@ can_eq_app ev s1 t1 s2 t2
-- Test case: typecheck/should_run/Typeable1
-- We could also include this mismatch check above (for W and D), but it's slow
-- and we'll get a better error message not doing it
- | s1k `mismatches` s2k
- = canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
-
| CtGiven { ctev_evar = evar, ctev_loc = loc } <- ev
- = do { let co = mkTcCoVarCo evar
+ = do { s1k <- tcTypeKindM s1
+ ; s2k <- tcTypeKindM s2
+ ; if isForAllTy s1k /= isForAllTy s2k
+ then canEqHardFailure ev (s1 `mkAppTy` t1) (s2 `mkAppTy` t2)
+ else
+ do { let co = mkTcCoVarCo evar
co_s = mkTcLRCo CLeft co
co_t = mkTcLRCo CRight co
; evar_s <- newGivenEvVar loc ( mkTcEqPredLikeEv ev s1 s2
@@ -1316,15 +1318,7 @@ can_eq_app ev s1 t1 s2 t2
; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
, evCoercion co_t )
; emitWorkNC [evar_t]
- ; canEqNC evar_s NomEq s1 s2 }
-
- where
- s1k = tcTypeKind s1
- s2k = tcTypeKind s2
-
- k1 `mismatches` k2
- = isForAllTy k1 && not (isForAllTy k2)
- || not (isForAllTy k1) && isForAllTy k2
+ ; canEqNC evar_s NomEq s1 s2 }}
-----------------------
-- | Break apart an equality over a casted type
@@ -1789,10 +1783,8 @@ canCFunEqCan ev fn tys fsk
else do { traceTcS "canCFunEqCan: non-refl" $
vcat [ text "Kind co:" <+> ppr kind_co
, text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk)
- , text "LHS:" <+> hang (ppr (mkTyConApp fn tys))
- 2 (dcolon <+> ppr (tcTypeKind (mkTyConApp fn tys)))
- , text "New LHS" <+> hang (ppr new_lhs)
- 2 (dcolon <+> ppr (tcTypeKind new_lhs)) ]
+ , text "LHS:" <+> ppr (mkTyConApp fn tys)
+ , text "New LHS" <+> ppr new_lhs ]
; (ev', new_co, new_fsk)
<- newFlattenSkolem flav (ctEvLoc ev) fn tys'
; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
@@ -1821,15 +1813,25 @@ canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs
-> TcType -> TcType -- rhs: already flat
-> TcS (StopOrContinue Ct)
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
+ = do { let k1 = tyVarKind tv1
+ ; k2 <- tcTypeKindM xi2
+ ; homo_kind <- tcEqTypeM k1 k2
+ ; if homo_kind
+ then canEqTyVarHomo ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
+ else canEqTyVarTake2 ev eq_rel swapped tv1 ps_ty1 k1 xi2 ps_xi2 k2 }
+
+canEqTyVarTake2 :: CtEvidence -- ev :: lhs ~ rhs
+ -> EqRel -> SwapFlag
+ -> TcTyVar -> TcType -> TcKind -- tv1, its pretty form, and its kind
+ -> TcType -> TcType -> TcKind -- rhs, its pretty form, and its kind
+ -- Both tv1 and rhs are already flat
+ -> TcS (StopOrContinue Ct)
+canEqTyVarTake2 ev eq_rel swapped tv1 ps_ty1 k1 xi2 ps_xi2 k2
+ = do { -- 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_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)
; traceTcS "canEqTyVar tried flattening kinds"
(vcat [ sep [ parens (ppr tv1 <+> dcolon <+> ppr k1)
@@ -1848,7 +1850,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
-- See Note [Equalities with incompatible kinds]
; let role = eqRelRole eq_rel
- ; if flat_k1 `tcEqType` flat_k2
+ ; if flat_k1 `tcEqType` flat_k2 -- Fully zonked, so tcEqType is ok
then do { let rhs_kind_co = mkTcSymCo k2_co `mkTcTransCo` k1_co
-- :: kind(xi2) ~N kind(xi1)
@@ -1880,10 +1882,6 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
new_rhs flat_k2 ps_rhs } }
where
xi1 = mkTyVarTy tv1
-
- k1 = tyVarKind tv1
- k2 = tcTypeKind xi2
-
loc = ctEvLoc ev
flav = ctEvFlavour ev
@@ -1922,7 +1920,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" $
@@ -2364,7 +2362,9 @@ unifyWanted :: CtLoc -> Role
-- See Note [unifyWanted and unifyDerived]
-- The returned coercion's role matches the input parameter
unifyWanted loc Phantom ty1 ty2
- = do { kind_co <- unifyWanted loc Nominal (tcTypeKind ty1) (tcTypeKind ty2)
+ = do { k1 <- tcTypeKindM ty1
+ ; k2 <- tcTypeKindM ty2
+ ; kind_co <- unifyWanted loc Nominal k1 k2
; return (mkPhantomCo kind_co ty1 ty2) }
unifyWanted loc role orig_ty1 orig_ty2
@@ -2401,9 +2401,10 @@ unifyWanted loc role orig_ty1 orig_ty2
go ty1 ty2 = bale_out ty1 ty2
bale_out ty1 ty2
- | ty1 `tcEqType` ty2 = return (mkTcReflCo role ty1)
- -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
- | otherwise = emitNewWantedEq loc role orig_ty1 orig_ty2
+ = do { -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
+ already_eq <- ty1 `tcEqTypeM` ty2
+ ; if already_eq then return (mkTcReflCo role ty1)
+ else emitNewWantedEq loc role orig_ty1 orig_ty2 }
unifyDeriveds :: CtLoc -> [Role] -> [TcType] -> [TcType] -> TcS ()
-- See Note [unifyWanted and unifyDerived]
@@ -2444,9 +2445,10 @@ unify_derived loc role orig_ty1 orig_ty2
go ty1 ty2 = bale_out ty1 ty2
bale_out ty1 ty2
- | ty1 `tcEqType` ty2 = return ()
- -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
- | otherwise = emitNewDerivedEq loc role orig_ty1 orig_ty2
+ = do { -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
+ already_eq <- ty1 `tcEqTypeM` ty2
+ ; if already_eq then return ()
+ else emitNewDerivedEq loc role orig_ty1 orig_ty2 }
maybeSym :: SwapFlag -> TcCoercion -> TcCoercion
maybeSym IsSwapped co = mkTcSymCo co
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index 4bbb42d4b3..fde558100b 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -27,6 +27,7 @@ import TcClassDcl( instDeclCtxt3, tcATDefault, tcMkDeclCtxt )
import TcEnv
import TcGenDeriv -- Deriv stuff
import TcValidity( checkValidInstHead )
+import TcMType( tcTypeKindM )
import InstEnv
import Inst
import FamInstEnv
@@ -629,9 +630,9 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mbl_deriv_strat overlap_mode))
-- Perform an additional unification with the kind of the `via`
-- type and the result of the previous kind unification.
Just (ViaStrategy via_ty) -> do
- let via_kind = tcTypeKind via_ty
- inst_ty_kind = tcTypeKind inst_ty'
- mb_match = tcUnifyTy inst_ty_kind via_kind
+ via_kind <- tcTypeKindM via_ty
+ inst_ty_kind <- tcTypeKindM inst_ty'
+ let mb_match = tcUnifyTy inst_ty_kind via_kind
checkTc (isJust mb_match)
(derivingViaKindErr cls inst_ty_kind
@@ -788,13 +789,14 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
-- See Note [tc_args and tycon arity]
(tc_args_to_keep, args_to_drop)
= splitAt n_args_to_keep tc_args
- inst_ty_kind = tcTypeKind (mkTyConApp tc tc_args_to_keep)
+ enough_args = n_args_to_keep >= 0
+
+ ; inst_ty_kind <- tcTypeKindM (mkTyConApp tc tc_args_to_keep)
- -- Match up the kinds, and apply the resulting kind substitution
+ ; let -- Match up the kinds, and apply the resulting kind substitution
-- to the types. See Note [Unify kinds in deriving]
-- We are assuming the tycon tyvars and the class tyvars are distinct
- mb_match = tcUnifyTy inst_ty_kind cls_arg_kind
- enough_args = n_args_to_keep >= 0
+ mb_match = tcUnifyTy inst_ty_kind cls_arg_kind
-- Check that the result really is well-kinded
; checkTc (enough_args && isJust mb_match)
@@ -826,24 +828,21 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
case mb_deriv_strat' of
-- Perform an additional unification with the kind of the `via`
-- type and the result of the previous kind unification.
- Just (ViaStrategy via_ty) -> do
- let final_via_ty = via_ty
- final_via_kind = tcTypeKind final_via_ty
- final_inst_ty_kind
- = tcTypeKind (mkTyConApp tc final_tc_args')
- via_match = tcUnifyTy final_inst_ty_kind final_via_kind
-
- checkTc (isJust via_match)
- (derivingViaKindErr cls final_inst_ty_kind
- final_via_ty final_via_kind)
-
- let Just via_subst = via_match
- (final_tkvs, final_cls_tys, final_tc_args)
- = propagate_subst via_subst tkvs'
- final_cls_tys' final_tc_args'
- pure ( final_tkvs, final_cls_tys, final_tc_args
- , Just $ ViaStrategy $ substTy via_subst via_ty
- )
+ Just (ViaStrategy via_ty) ->
+ do { final_via_kind <- tcTypeKindM via_ty
+ ; final_inst_ty_kind <- tcTypeKindM (mkTyConApp tc final_tc_args')
+ ; let via_match = tcUnifyTy final_inst_ty_kind final_via_kind
+
+ ; checkTc (isJust via_match) $
+ derivingViaKindErr cls final_inst_ty_kind
+ via_ty final_via_kind
+
+ ; let Just via_subst = via_match
+ (final_tkvs, final_cls_tys, final_tc_args)
+ = propagate_subst via_subst tkvs'
+ final_cls_tys' final_tc_args'
+ ; pure ( final_tkvs, final_cls_tys, final_tc_args
+ , Just $ ViaStrategy $ substTy via_subst via_ty ) }
_ -> pure ( tkvs', final_cls_tys', final_tc_args'
, mb_deriv_strat' )
diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs
index ba45e09dc5..df1a3a51fc 100644
--- a/compiler/typecheck/TcDerivInfer.hs
+++ b/compiler/typecheck/TcDerivInfer.hs
@@ -111,6 +111,8 @@ inferConstraintsDataConArgs inst_ty inst_tys
, denv_cls_tys = cls_tys } <- ask
wildcard <- isStandaloneWildcardDeriv
+ inst_ty_kind <- lift $ tcTypeKindM inst_ty
+
let tc_binders = tyConBinders rep_tc
choose_level bndr
| isNamedTyConBinder bndr = KindLevel
@@ -157,7 +159,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
is_generic = main_cls `hasKey` genClassKey
is_generic1 = main_cls `hasKey` gen1ClassKey
-- is_functor_like: see Note [Inferring the instance context]
- is_functor_like = tcTypeKind inst_ty `tcEqKind` typeToTypeKind
+ is_functor_like = inst_ty_kind `tcEqKind` typeToTypeKind
|| is_generic1
get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
@@ -192,6 +194,8 @@ inferConstraintsDataConArgs inst_ty inst_tys
-- See Note [Inferring the instance context]
mk_functor_like_constraints orig t_or_k cls
= map $ \ty -> let ki = tcTypeKind ty in
+ -- OK to use typeKind because 'ty' is a fully
+ -- zonked constructor argument type
( [ mk_cls_pred orig t_or_k cls ty
, mkPredOrigin orig KindLevel
(mkPrimEqPred ki typeToTypeKind) ]
@@ -228,15 +232,17 @@ inferConstraintsDataConArgs inst_ty inst_tys
-- Reason: when the IF holds, we generate a method
-- dataCast2 f = gcast2 f
-- and we need the Data constraints to typecheck the method
- extra_constraints = [mkThetaOriginFromPreds constrs]
+ mk_extra_constraints
+ | main_cls `hasKey` dataClassKey
+ = do { rep_tc_arg_kinds <- lift $ mapM tcTypeKindM rep_tc_args
+ ; if all isLiftedTypeKind rep_tc_arg_kinds
+ then return [mkThetaOriginFromPreds constrs]
+ else return [] }
+ | otherwise
+ = return []
where
- constrs
- | main_cls `hasKey` dataClassKey
- , all (isLiftedTypeKind . tcTypeKind) rep_tc_args
- = [ mk_cls_pred deriv_origin t_or_k main_cls ty
- | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
- | otherwise
- = []
+ constrs = [ mk_cls_pred deriv_origin t_or_k main_cls ty
+ | (t_or_k, ty) <- zip t_or_ks rep_tc_args ]
mk_cls_pred orig t_or_k cls ty
-- Don't forget to apply to cls_tys' too
@@ -276,6 +282,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
[ ppr main_cls <+> ppr inst_tys'
, ppr arg_constraints
]
+ ; extra_constraints <- mk_extra_constraints
; return ( stupid_constraints ++ extra_constraints
++ arg_constraints
, tvs', inst_tys') }
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index df307f240c..0c283382c1 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -603,7 +603,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
is_user_type_error ct _ = isUserTypeErrorCt ct
- is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTypeKind ty2
+ is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2
is_homo_equality _ _ = False
is_equality _ (EqPred {}) = True
@@ -1177,7 +1177,7 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
where
occ = holeOcc hole
hole_ty = ctEvPred (ctEvidence ct)
- hole_kind = tcTypeKind hole_ty
+ hole_kind = typeKind hole_ty
tyvars = tyCoVarsOfTypeList hole_ty
hole_msg = case hole of
@@ -1500,9 +1500,9 @@ mkEqErr1 ctxt ct -- Wanted or derived;
|| not (cty1 `pickyEqType` cty2)
-> hang (text "When matching" <+> sub_what)
2 (vcat [ ppr cty1 <+> dcolon <+>
- ppr (tcTypeKind cty1)
+ ppr (typeKind cty1)
, ppr cty2 <+> dcolon <+>
- ppr (tcTypeKind cty2) ])
+ ppr (typeKind cty2) ])
_ -> text "When matching the kind of" <+> quotes (ppr cty1)
msg2 = case sub_o of
TypeEqOrigin {}
@@ -1750,7 +1750,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
-- Not an occurs check, because F is a type function.
where
Pair _ k1 = tcCoercionKind co1
- k2 = tcTypeKind ty2
+ k2 = typeKind ty2
ty1 = mkTyVarTy tv1
occ_check_expand = occCheckForErrors dflags tv1 ty2
@@ -1976,16 +1976,15 @@ misMatchMsg ct oriented ty1 ty2
pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
-> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch ty1 ty2 ct =
- pprWithExplicitKindsWhen mismatch
+ 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)
@@ -2517,7 +2516,7 @@ mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_over
, not (isTypeFamilyTyCon tc)
= hang (text "GHC can't yet do polykinded")
2 (text "Typeable" <+>
- parens (ppr ty <+> dcolon <+> ppr (tcTypeKind ty)))
+ parens (ppr ty <+> dcolon <+> ppr (typeKind ty)))
| otherwise
= empty
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 8afcc8b666..35412f5bdb 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -387,8 +387,9 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
--
-- The *result* type can have any kind (Trac #8739),
-- so we don't need to check anything for that
+ ; arg2_kind <- tcTypeKindM arg2_sigma
; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma))
- (tcTypeKind arg2_sigma) liftedTypeKind
+ arg2_kind liftedTypeKind
-- ignore the evidence. arg2_sigma must have type * or #,
-- because we know arg2_sigma -> or_res_ty is well-kinded
-- (because otherwise matchActualFunTys would fail)
@@ -1345,9 +1346,10 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
insted_ty = substTyWithInScope in_scope [tv] [ty_arg] inner_ty
-- NB: tv and ty_arg have the same kind, so this
-- substitution is kind-respecting
+ ; arg_kind <- tcTypeKindM ty_arg
; traceTc "VTA" (vcat [ppr tv, debugPprType kind
- , debugPprType ty_arg
- , debugPprType (tcTypeKind ty_arg)
+ , debugPprType ty_arg <+> dcolon
+ <+> debugPprType arg_kind
, debugPprType inner_ty
, debugPprType insted_ty ])
diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs
index b3c41a5711..a1de5a8779 100644
--- a/compiler/typecheck/TcFlatten.hs
+++ b/compiler/typecheck/TcFlatten.hs
@@ -1470,12 +1470,13 @@ flatten_app_ty_args fun_xi fun_co []
-- this will be a common case when called from flatten_fam_app, so shortcut
= return (fun_xi, fun_co)
flatten_app_ty_args fun_xi fun_co arg_tys
- = do { (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
+ = do { let fun_kind = tcTypeKind fun_xi -- fun_xi is flat, to tcTypeKind is fine
+ ; (xi, co, kind_co) <- case tcSplitTyConApp_maybe fun_xi of
Just (tc, xis) ->
do { let tc_roles = tyConRolesRepresentational tc
arg_roles = dropList xis tc_roles
; (arg_xis, arg_cos, kind_co)
- <- flatten_vector (tcTypeKind fun_xi) arg_roles arg_tys
+ <- flatten_vector fun_kind arg_roles arg_tys
-- Here, we have fun_co :: T xi1 xi2 ~ ty
-- and we need to apply fun_co to the arg_cos. The problem is
@@ -1494,7 +1495,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys
; return (app_xi, app_co, kind_co) }
Nothing ->
do { (arg_xis, arg_cos, kind_co)
- <- flatten_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
+ <- flatten_vector fun_kind (repeat Nominal) arg_tys
; let arg_xi = mkAppTys fun_xi arg_xis
arg_co = mkAppCos fun_co arg_cos
; return (arg_xi, arg_co, kind_co) }
@@ -1626,8 +1627,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
@@ -1749,16 +1749,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
@@ -1769,11 +1761,8 @@ flatten_exact_fam_app_fully tc tys
; 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') }
+ co' = mkSymCo co
+ ; return $ Just (xi, co') }
Nothing -> pure Nothing }
{- Note [Reduce type family applications eagerly]
@@ -2062,6 +2051,7 @@ unflattenWanteds tv_eqs funeqs
-- Note [Unflattening can force the solver to iterate]
= ASSERT2( tyVarKind tv `eqType` tcTypeKind rhs, ppr ct )
-- CTyEqCan invariant should ensure this is true
+ -- We can do tcTypeKind because the constraint is inert
do { is_filled <- isFilledMetaTyVar tv
; elim <- case is_filled of
False -> do { traceTcS "unflatten_eq 2" (ppr ct)
@@ -2102,10 +2092,9 @@ unflattenWanteds tv_eqs funeqs
finalise_eq (CTyEqCan { cc_ev = ev, cc_tyvar = tv
, cc_rhs = rhs, cc_eq_rel = eq_rel }) rest
| isFmvTyVar tv
- = do { ty1 <- zonkTcTyVar tv
- ; rhs' <- zonkTcType rhs
- ; if ty1 `tcEqType` rhs'
- then do { setReflEvidence ev eq_rel rhs'
+ = do { already_eq <- mkTyVarTy tv `tcEqTypeM` rhs
+ ; if already_eq
+ then do { setReflEvidence ev eq_rel rhs
; return rest }
else return (mkNonCanonical ev `consCts` rest) }
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index 6834af9f41..ec434ad415 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -1039,10 +1039,12 @@ zonk_cmd_top env (HsCmdTop (CmdTopTc stack_tys ty ids) cmd)
new_ty <- zonkTcTypeToTypeX env ty
new_ids <- mapSndM (zonkExpr env) ids
- MASSERT( isLiftedTypeKind (tcTypeKind new_stack_tys) )
- -- desugarer assumes that this is not levity polymorphic...
- -- but indeed it should always be lifted due to the typing
- -- rules for arrows
+ when debugIsOn $
+ do { new_stack_kind <- tcTypeKindM new_stack_tys
+ ; MASSERT( isLiftedTypeKind new_stack_kind) }
+ -- desugarer assumes that this is not levity polymorphic...
+ -- but indeed it should always be lifted due to the typing
+ -- rules for arrows
return (HsCmdTop (CmdTopTc new_stack_tys new_ty new_ids) new_cmd)
zonk_cmd_top _ (XCmdTop {}) = panic "zonk_cmd_top"
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 182facc3fd..ca93199819 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -249,7 +249,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
@@ -812,14 +812,10 @@ tc_hs_tuple_type mode rn_ty HsBoxedOrConstraintTuple hs_tys exp_kind
-- (Either Int, Int), we do not want to get an error saying
-- "the second argument of a tuple should have kind *->*"
- ; tys <- zonkTcTypes tys -- Expose as much kind information as poss
-
- ; traceTc "tc_hs_tuple 3" $
- vcat [ ppr ty <+> dcolon <+> ppr (tcTypeKind ty) | ty <- tys ]
+ ; kinds <- mapM tcTypeKindM tys -- Expose as much kind information as poss
; let (arg_kind, tup_sort)
- = case [ (k,s) | ty <- tys
- , let k = typeKind ty
+ = case [ (k,s) | k <- kinds
, Just s <- [tupKindSort_maybe k] ] of
((k,s) : _) -> (k,s)
[] -> (liftedTypeKind, BoxedTuple)
@@ -898,22 +894,15 @@ tcInferApps :: TcTyMode
-> TcType -- ^ Function
-> [LHsType GhcRn] -- ^ Args
-> TcM TcType -- ^ (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 orig_fun_ty orig_hs_args
- = do { fun_ty <- zonkTcType orig_fun_ty
- ; let fun_ki = tcTypeKind fun_ty
- empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
+tcInferApps mode orig_hs_ty fun_ty orig_hs_args
+ = do { fun_ki <- tcTypeKindM fun_ty
+ ; let empty_subst = mkEmptyTCvSubst $ mkInScopeSet $
tyCoVarsOfType fun_ki
(orig_ki_binders, orig_inner_ki) = tcSplitPiTys fun_ki
; traceTc "tcInferApps {" $
vcat [ text "orig_hs_ty:" <+> ppr orig_hs_ty
, text "orig_hs_args:" <+> ppr orig_hs_args
- , text "caller_fun_ty:" <+> ppr orig_fun_ty
, text "fun_ty:" <+> ppr fun_ty
, text "fun_ki:" <+> ppr fun_ki ]
; (f_args, _res_k) <- go 1 empty_subst fun_ty orig_ki_binders orig_inner_ki orig_hs_args
@@ -1021,8 +1010,8 @@ checkExpectedKindX pp_hs_ty ty exp_kind
-- 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 act_kind = tcTypeKind ty
- n_exp_invis_bndrs = invisibleTyBndrCount exp_kind
+ act_kind <- tcTypeKindM ty
+ ; 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)
@@ -1037,8 +1026,8 @@ checkExpectedKindX pp_hs_ty ty exp_kind
, text "act_kind':" <+> ppr act_kind'
, text "exp_kind:" <+> ppr exp_kind ]
- ; if act_kind' `tcEqType` exp_kind
- then return ty' -- This is very common
+ ; eq_kinds <- act_kind' `tcEqTypeM` exp_kind
+ ; if eq_kinds then return ty' -- This is very common
else
do { let origin = TypeEqOrigin { uo_actual = act_kind'
, uo_expected = exp_kind
diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs
index 3b82d59b60..7f655724e9 100644
--- a/compiler/typecheck/TcInstDcls.hs
+++ b/compiler/typecheck/TcInstDcls.hs
@@ -793,7 +793,7 @@ tcDataFamHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksi
bindImplicitTKBndrs_Q_Skol imp_vars $
bindExplicitTKBndrs_Q_Skol AnyKind exp_bndrs $
do { stupid_theta <- tcHsContext hs_ctxt
- ; (lhs_ty, _) <- tcFamTyPats fam_tc mb_clsinfo hs_pats
+ ; lhs_ty <- tcFamTyPats fam_tc mb_clsinfo hs_pats
; mapM_ (wrapLocM_ kcConDecl) hs_cons
; res_kind <- tc_kind_sig m_ksig
; lhs_ty <- checkExpectedKindX pp_lhs lhs_ty res_kind
diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs
index 277e3249d4..527ca31833 100644
--- a/compiler/typecheck/TcInteract.hs
+++ b/compiler/typecheck/TcInteract.hs
@@ -1205,6 +1205,7 @@ interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
filtered_dicts = addDictsByClass dicts cls other_ip_dicts
-- Pick out any Given constraints for the same implicit parameter
+ -- Everything is inert (zonked) to ok to use tcEqType
is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
= isGiven ev && ip_str `tcEqType` ip_str'
is_this_ip _ = False
@@ -1631,11 +1632,12 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
-- we often write tv := xi
solveByUnification wd tv xi
= do { let tv_ty = mkTyVarTy tv
+ ; xi_kind <- tcTypeKindM xi
; traceTcS "Sneaky unification:" $
vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
text "Coercion:" <+> pprEq tv_ty xi,
- text "Left Kind is:" <+> ppr (tcTypeKind tv_ty),
- text "Right Kind is:" <+> ppr (tcTypeKind xi) ]
+ text "Left Kind is:" <+> ppr (tyVarKind tv),
+ text "Right Kind is:" <+> ppr xi_kind ]
; unifyTyVar tv xi
; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 0ca27f57d0..1486d656f4 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -37,6 +37,10 @@ module TcMType (
tauifyExpType, inferResultToType,
--------------------------------
+ -- Getting the kind of a type
+ tcEqTypeM, tcTypeKindM, piResultTysM,
+
+ --------------------------------
-- Creating new evidence variables
newEvVar, newEvVars, newDict,
newWanted, newWanteds, newHoleCt, cloneWanted, cloneWC,
@@ -60,18 +64,21 @@ module TcMType (
freshenTyVarBndrs, freshenCoVarBndrsX,
--------------------------------
+ -- Quantification
+ candidateQTyVarsOfType, candidateQTyVarsOfKind,
+ candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
+ CandidatesQTvs(..), delCandidates, candidateKindVars,
+ skolemiseQuantifiedTyVar, defaultTyVar,
+ quantifyTyVars,
+
+ --------------------------------
-- Zonking and tidying
zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin,
tidyEvVar, tidyCt, tidySkolemInfo,
- zonkTcTyVar, zonkTcTyVars,
+ zonkTcTyVar, zonkTcTyVars,
zonkTcTyVarToTyVar, zonkTyVarTyVarPairs,
zonkTyCoVarsAndFV, zonkTcTypeAndFV,
zonkTyCoVarsAndFVList,
- candidateQTyVarsOfType, candidateQTyVarsOfKind,
- candidateQTyVarsOfTypes, candidateQTyVarsOfKinds,
- CandidatesQTvs(..), delCandidates, candidateKindVars,
- skolemiseQuantifiedTyVar, defaultTyVar,
- quantifyTyVars,
zonkTcTyCoVarBndr, zonkTyConBinders,
zonkTcType, zonkTcTypes, zonkCo,
zonkTyCoVarKind,
@@ -128,6 +135,221 @@ import qualified Data.Semigroup as Semi
{-
************************************************************************
* *
+ tcTypeKind
+* *
+************************************************************************
+-}
+
+tcTypeKindM :: HasDebugCallStack => TcType -> TcM TcKind
+tcTypeKindM (TyConApp tc tys) = return (piResultTys (tyConKind tc) tys)
+tcTypeKindM (LitTy l) = return (typeLiteralKind l)
+tcTypeKindM (CastTy _ty co) = return (pSnd $ coercionKind co)
+tcTypeKindM (CoercionTy co) = return (coercionType co)
+
+tcTypeKindM (FunTy arg res)
+ = do { arg_k <- tcTypeKindM arg
+ ; if tcIsConstraintKind arg_k
+ then do { res_k <- tcTypeKindM res
+ ; if tcIsConstraintKind res_k
+ then return constraintKind
+ else return liftedTypeKind }
+ else return liftedTypeKind }
+
+tcTypeKindM (AppTy fun arg)
+ = go fun [arg]
+ where
+ -- Accumulate the type arugments, so we can call piResultTys,
+ -- rather than a succession of calls to piResultTy (which is
+ -- asymptotically costly as the number of arguments increases)
+ go (AppTy fun arg) args = go fun (arg:args)
+ go fun args = do { fun_k <- tcTypeKindM fun
+ ; piResultTysM fun_k args }
+
+tcTypeKindM ty@(ForAllTy {})
+ = do { body_k <- tcTypeKindM body
+ ; if tcIsConstraintKind body_k
+ then return constraintKind
+ else case occCheckExpand tvs body_k of -- We must make sure tv does
+ Just k' -> return k' -- not occur in kind
+ Nothing -> pprPanic "tcTypeKindM"
+ (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_k) }
+ where
+ (tvs, body) = splitTyVarForAllTys ty
+
+tcTypeKindM (TyVarTy tv)
+ | isMetaTyVar tv
+ = do { maybe_ty <- readMetaTyVar tv
+ ; case maybe_ty of
+ Indirect ty -> tcTypeKindM ty
+ Flexi -> return (tyVarKind tv) }
+ | otherwise
+ = return (tyVarKind tv)
+
+piResultTysM :: HasDebugCallStack => TcType -> [TcType] -> TcM TcType
+piResultTysM ty orig_args = go init_subst ty orig_args
+ where
+ init_subst = mkEmptyTCvSubst $ mkInScopeSet (tyCoVarsOfTypes (ty:orig_args))
+
+ go :: TCvSubst -> TcType -> [TcType] -> TcM TcType
+ go subst ty []
+ = return (substTy subst ty) -- substTy has a fast-path for empty substitutions
+
+ go subst ty all_args@(arg:args)
+ | Just ty' <- tcView ty
+ = go subst ty' all_args
+
+ | FunTy _ res <- ty
+ = go subst res args
+
+ | ForAllTy (Bndr tv _) res <- ty
+ = go (extendTCvSubst subst tv arg) res args
+
+ | TyVarTy tv <- ty
+ , isMetaTyVar tv
+ = do { maybe_ty <- readMetaTyVar tv
+ ; case maybe_ty of
+ Indirect ty -> go subst ty all_args
+ Flexi -> try_subst subst ty all_args }
+
+ | otherwise
+ = try_subst subst ty all_args
+
+ try_subst subst ty args
+ | not (isEmptyTCvSubst subst) -- See Note [Care with kind instantiation]
+ = go init_subst (substTy subst ty) args
+
+ | otherwise
+ = -- We have not run out of arguments, but the function doesn't
+ -- have the right kind to apply to them; so panic.
+ -- Without the explicit isEmptyVarEnv test, an ill-kinded type
+ -- would give an infniite loop, which is very unhelpful
+ -- c.f. Trac #15473
+ pprPanic "piResultTysM" (ppr ty $$ ppr orig_args $$ ppr args)
+
+
+-- | A monadic version of tcEqType
+-- If it returns True, the two types are definitely equal
+-- If not, they might still be equal, after zonking
+-- Reason for this one-sided conservative-ness: tcEqTypeM is used only
+-- for fast-path checks, and we don't want the full glory of RnEnv2,
+-- which requires us to find the free vars to find the in-scope set,
+-- which requires zonking... and is almost never necessary
+tcEqTypeM :: TcType -> TcType -> TcM Bool
+tcEqTypeM t1 t2
+ = do { k1 <- tcTypeKindM t1
+ ; k2 <- tcTypeKindM t2
+ ; tc_eq_type_m k1 k2 `scAndM` tc_eq_type_m t1 t2 }
+
+tc_eq_type_m :: TcType -> TcType -> TcM Bool
+tc_eq_type_m orig_ty1 orig_ty2
+ = go orig_ty1 orig_ty2
+ where
+ go :: TcType -> TcType -> TcM Bool
+ go t1 t2 | Just t1' <- tcView t1 = go t1' t2
+ go t1 t2 | Just t2' <- tcView t2 = go t1 t2'
+
+ go (TyVarTy tv1) t2 = go_tv tv1 t2
+ go t1 (TyVarTy tv2) = go_tv tv2 t1
+
+ go (LitTy lit1) (LitTy lit2)
+ = return (lit1 == lit2)
+
+ go t1@(ForAllTy {}) t2 = return (tcEqTypeNoKindCheck t1 t2)
+ go t1 t2@(ForAllTy {}) = return (tcEqTypeNoKindCheck t1 t2)
+
+ -- 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 (FunTy arg1 res1) (FunTy arg2 res2)
+ = go arg1 arg2 `scAndM` go res1 res2
+ go ty (FunTy arg res) = eqFunTy arg res ty
+ go (FunTy arg res) ty = eqFunTy arg res ty
+
+ -- See Note [Equality on AppTys] in Type
+ go (AppTy s1 t1) ty2
+ | Just (s2, t2) <- repSplitAppTy_maybe ty2
+ = go s1 s2 `scAndM` go t1 t2
+ go ty1 (AppTy s2 t2)
+ | Just (s1, t1) <- repSplitAppTy_maybe ty1
+ = go s1 s2 `scAndM` go t1 t2
+
+ go (TyConApp tc1 ts1) (TyConApp tc2 ts2)
+ | tc1 == tc2 = gos ts1 ts2
+ | otherwise = return False
+
+ go (CastTy t1 _) t2 = go t1 t2
+ go t1 (CastTy t2 _) = go t1 t2
+ go (CoercionTy {}) (CoercionTy {}) = return True
+
+ go _ _ = return False
+
+ --------
+ gos [] [] = return True
+ gos (t1:ts1) (t2:ts2) = go t1 t2 `scAndM` gos ts1 ts2
+ gos _ _ = return False
+
+ --------
+ go_tv :: TcTyVar -> TcType -> TcM Bool
+ go_tv tv1 t2
+ | isMetaTyVar tv1
+ = do { mb_t1 <- readMetaTyVar tv1
+ ; case mb_t1 of
+ Indirect t1 -> go t1 t2
+ Flexi -> go_tv1 tv1 t2 }
+ | otherwise
+ = go_tv1 tv1 t2
+
+ --------
+ go_tv1 :: TcTyVar -> TcType -> TcM Bool
+ -- tv1 is not a filled-in meta-tyvar
+ go_tv1 tv1 (TyVarTy tv2)
+ | isMetaTyVar tv2
+ = do { mb_t2 <- readMetaTyVar tv2
+ ; case mb_t2 of
+ Indirect t2 -> go_tv1 tv1 t2
+ Flexi -> go_tv2 tv1 tv2 }
+ | otherwise
+ = go_tv2 tv1 tv2
+
+ go_tv1 _ _ = return False -- TyVar vs non-TyVar
+
+ --------
+ go_tv2 :: TcTyVar -> TcTyVar -> TcM Bool
+ -- Neither is a filled-in meta-tyvar
+ go_tv2 tv1 tv2 = return (tv1 == tv2)
+
+ --------
+ -- @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is
+ -- sometimes hard to know directly because @ty@ might have some casts
+ -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't
+ -- 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 :: Type -> Type -> Type -> TcM Bool
+ -- Last arg is /not/ FunTy
+ eqFunTy arg res ty@(AppTy{}) = get_args ty []
+ where
+ get_args :: Type -> [Type] -> TcM 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
+ | tc == funTyCon
+ , [_, _, arg', res'] <- tys ++ args
+ = go arg arg' <&&> go res res'
+ get_args _ _ = return False
+ eqFunTy _ _ _ = return False
+
+scAndM :: TcM Bool -> TcM Bool -> TcM Bool
+-- A short-circuiting 'and' for monadic computations
+-- If the first returns False, it does not do the second at all
+-- (Whereas <&&> does the seecond regardless.)
+scAndM mb1 mb2 = do { b1 <- mb1
+ ; if b1 then mb2
+ else return False }
+
+{-
+************************************************************************
+* *
Kind variables
* *
************************************************************************
@@ -684,7 +906,8 @@ newFskTyVar fam_ty
, mtv_ref = ref
, mtv_tclvl = tclvl }
name = mkMetaTyVarName uniq (fsLit "fsk")
- ; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
+ ; fam_ty_kind <- tcTypeKindM fam_ty
+ ; return (mkTcTyVar name fam_ty_kind details) }
newFmvTyVar :: TcType -> TcM TcTyVar
-- Very like newMetaTyVar, except sets mtv_tclvl to one less
@@ -697,7 +920,8 @@ newFmvTyVar fam_ty
, mtv_ref = ref
, mtv_tclvl = tclvl }
name = mkMetaTyVarName uniq (fsLit "s")
- ; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
+ ; fam_ty_kind <- tcTypeKindM fam_ty
+ ; return (mkTcTyVar name fam_ty_kind details) }
newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
newMetaDetails info
@@ -784,10 +1008,9 @@ 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
+ ; ty_kind <- tcTypeKindM ty
+ ; 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]
@@ -2199,4 +2422,4 @@ formatLevPolyErr ty
, text "Kind:" <+> pprWithTYPE tidy_ki ])
where
(tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
- tidy_ki = tidyType tidy_env (tcTypeKind ty)
+ tidy_ki = tidyType tidy_env (typeKind ty)
diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs
index ba3603fb42..38236afbdf 100644
--- a/compiler/typecheck/TcPat.hs
+++ b/compiler/typecheck/TcPat.hs
@@ -351,7 +351,8 @@ tc_pat penv (LazyPat x pat) pat_ty thing_inside
-- Check that the expected pattern type is itself lifted
; pat_ty <- readExpType pat_ty
- ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind
+ ; pat_kind <- tcTypeKindM pat_ty
+ ; _ <- unifyType Nothing pat_kind liftedTypeKind
; return (LazyPat x pat', res) }
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index ea1f483268..370e62f998 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -53,7 +53,6 @@ import FieldLabel
import Bag
import Util
import ErrUtils
-import Data.Maybe( mapMaybe )
import Control.Monad ( zipWithM )
import Data.List( partition )
@@ -166,8 +165,8 @@ tcInferPatSynDecl (PSB { psb_id = lname@(dL->L _ name), psb_args = details
do { prov_dicts <- mapM zonkId prov_dicts
; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts
-- Filtering: see Note [Remove redundant provided dicts]
- (prov_theta, prov_evs)
- = unzip (mapMaybe mkProvEvidence filtered_prov_dicts)
+ ; pairs <- mapMaybeM mkProvEvidence filtered_prov_dicts
+ ; let (prov_theta, prov_evs) = unzip pairs
req_theta = map evVarPred req_dicts
-- Report coercions that esacpe
@@ -189,29 +188,30 @@ tcInferPatSynDecl (PSB { psb_id = lname@(dL->L _ name), psb_args = details
pat_ty rec_fields } }
tcInferPatSynDecl (XPatSynBind _) = panic "tcInferPatSynDecl"
-mkProvEvidence :: EvId -> Maybe (PredType, EvTerm)
+mkProvEvidence :: EvId -> TcM (Maybe (PredType, EvTerm))
-- See Note [Equality evidence in pattern synonyms]
mkProvEvidence ev_id
| EqPred r ty1 ty2 <- classifyPredType pred
- , let k1 = tcTypeKind ty1
- k2 = tcTypeKind ty2
- is_homo = k1 `tcEqType` k2
- homo_tys = [k1, ty1, ty2]
- hetero_tys = [k1, k2, ty1, ty2]
- = case r of
- ReprEq | is_homo
- -> Just ( mkClassPred coercibleClass homo_tys
- , evDataConApp coercibleDataCon homo_tys eq_con_args )
- | otherwise -> Nothing
- NomEq | is_homo
- -> Just ( mkClassPred eqClass homo_tys
- , evDataConApp eqDataCon homo_tys eq_con_args )
- | otherwise
- -> Just ( mkClassPred heqClass hetero_tys
- , evDataConApp heqDataCon hetero_tys eq_con_args )
+ = do { k1 <- tcTypeKindM ty1
+ ; k2 <- tcTypeKindM ty2
+ ; is_homo <- k1 `tcEqTypeM` k2
+ ; let homo_tys = [k1, ty1, ty2]
+ hetero_tys = [k1, k2, ty1, ty2]
+ ; return $
+ case r of
+ ReprEq | is_homo
+ -> Just ( mkClassPred coercibleClass homo_tys
+ , evDataConApp coercibleDataCon homo_tys eq_con_args )
+ | otherwise -> Nothing
+ NomEq | is_homo
+ -> Just ( mkClassPred eqClass homo_tys
+ , evDataConApp eqDataCon homo_tys eq_con_args )
+ | otherwise
+ -> Just ( mkClassPred heqClass hetero_tys
+ , evDataConApp heqDataCon hetero_tys eq_con_args ) }
| otherwise
- = Just (pred, EvExpr (evId ev_id))
+ = return (Just (pred, EvExpr (evId ev_id)))
where
pred = evVarPred ev_id
eq_con_args = [evId ev_id]
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 5e6f6308e0..8ed21f2d81 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2400,7 +2400,8 @@ tcRnType hsc_env normalise rdr_type
; _ <- checkNoErrs (simplifyInteractive lie)
-- Do kind generalisation; see Note [Kind-generalise in tcRnType]
- ; kvs <- kindGeneralize (tcTypeKind ty)
+ ; kind <- tcTypeKindM ty
+ ; kvs <- kindGeneralize kind
; ty <- zonkTcTypeToType ty
-- Do validity checking on type
@@ -2408,12 +2409,12 @@ tcRnType hsc_env normalise rdr_type
; ty' <- if normalise
then do { fam_envs <- tcGetFamInstEnvs
- ; let (_, ty')
- = normaliseType fam_envs Nominal ty
+ ; let (_, ty') = normaliseType fam_envs Nominal ty
; return ty' }
else return ty ;
- ; return (ty', mkInvForAllTys kvs (tcTypeKind ty')) }
+ ; kind' <- tcTypeKindM ty'
+ ; return (ty', mkInvForAllTys kvs kind') }
{- Note [TcRnExprMode]
~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 69f58b9002..587a26fd0a 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -105,7 +105,7 @@ module TcSMonad (
zonkTyCoVarsAndFV, zonkTcType, zonkTcTypes, zonkTcTyVar, zonkCo,
zonkTyCoVarsAndFVList,
zonkSimples, zonkWC,
- zonkTyCoVarKind,
+ zonkTyCoVarKind, tcEqTypeM, tcTypeKindM,
-- References
newTcRef, readTcRef, writeTcRef, updTcRef,
@@ -3126,6 +3126,13 @@ zonkWC wc = wrapTcS (TcM.zonkWC wc)
zonkTyCoVarKind :: TcTyCoVar -> TcS TcTyCoVar
zonkTyCoVarKind tv = wrapTcS (TcM.zonkTyCoVarKind tv)
+tcEqTypeM :: TcType -> TcType -> TcS Bool
+tcEqTypeM ty1 ty2 = wrapTcS (TcM.tcEqTypeM ty1 ty2)
+
+tcTypeKindM :: TcType -> TcS TcKind
+tcTypeKindM ty = wrapTcS (TcM.tcTypeKindM ty)
+
+
{- *********************************************************************
* *
* Flatten skolems *
@@ -3399,10 +3406,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/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index c51771d225..08b2992809 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1199,7 +1199,7 @@ reifyInstances th_nm th_tys
-- In particular, the type might have kind
-- variables inside it (Trac #7477)
- ; traceTc "reifyInstances" (ppr ty $$ ppr (tcTypeKind ty))
+ ; traceTc "reifyInstances" (ppr ty $$ ppr (typeKind ty))
; case splitTyConApp_maybe ty of -- This expands any type synonyms
Just (tc, tys) -- See Trac #7910
| Just cls <- tyConClass_maybe tc
@@ -1639,7 +1639,7 @@ annotThType :: Bool -- True <=> annotate
annotThType _ _ th_ty@(TH.SigT {}) = return th_ty
annotThType True ty th_ty
| not $ isEmptyVarSet $ filterVarSet isTyVar $ tyCoVarsOfType ty
- = do { let ki = tcTypeKind ty
+ = do { ki <- tcTypeKindM ty
; th_ki <- reifyKind ki
; return (TH.SigT th_ty th_ki) }
annotThType _ _ th_ty = return th_ty
@@ -1944,7 +1944,7 @@ reify_tc_app tc tys
-- See Note [Kind annotations on TyConApps]
maybe_sig_t th_type
| needs_kind_sig
- = do { let full_kind = tcTypeKind (mkTyConApp tc tys)
+ = do { full_kind <- tcTypeKindM (mkTyConApp tc tys)
; th_full_kind <- reifyKind full_kind
; return (TH.SigT th_type th_full_kind) }
| otherwise
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 9b399281ff..8615347c50 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -1742,7 +1742,8 @@ 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 NotAssociated hs_pats
+ do { fam_app <- tcFamTyPats tc_fam_tc NotAssociated hs_pats
+ ; res_kind <- tcTypeKindM fam_app
; tcCheckLHsType hs_rhs_ty res_kind }
-- Why "_Tv" here? Consider (Trac #14066
-- type family Bar x y where
@@ -1893,7 +1894,9 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty
(tyConKind fam_tc)
; return (mkTyConApp fam_tc args, rhs_kind) }
| otherwise
- = tcFamTyPats fam_tc mb_clsinfo hs_pats
+ = do { fam_app <- tcFamTyPats fam_tc mb_clsinfo hs_pats
+ ; res_kind <- tcTypeKindM fam_app
+ ; return (fam_app, res_kind) }
{- Note [Apparently-nullary families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1941,7 +1944,7 @@ tcFamTyPats fam_tc mb_clsinfo hs_pats
-- Ensure that the instance is consistent its parent class
; addConsistencyConstraints mb_clsinfo fam_app
- ; return (fam_app, tcTypeKind fam_app) }
+ ; return fam_app }
where
fam_name = tyConName fam_tc
fam_arity = tyConArity fam_tc
@@ -2438,8 +2441,8 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
-- So we return ( [a,b,z], [x,y]
-- , [], [x,y,z]
-- , [a~(x,y),b~z], <arg-subst> )
- | Just subst <- ASSERT( isLiftedTypeKind (tcTypeKind res_ty) )
- ASSERT( isLiftedTypeKind (tcTypeKind res_tmpl) )
+ | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
+ ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
tcMatchTy res_tmpl res_ty
= let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
raw_ex_tvs = dc_tvs `minusList` univ_tvs
@@ -2959,8 +2962,8 @@ checkValidDataCon dflags existential_ok tc con
orig_res_ty = dataConOrigResTy con
; traceTc "checkValidDataCon" (vcat
[ ppr con, ppr tc, ppr tc_tvs
- , ppr res_ty_tmpl <+> dcolon <+> ppr (tcTypeKind res_ty_tmpl)
- , ppr orig_res_ty <+> dcolon <+> ppr (tcTypeKind orig_res_ty)])
+ , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
+ , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
; checkTc (isJust (tcMatchTy res_ty_tmpl
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 8b91ed04f7..80883e4e48 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -1711,8 +1711,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
@@ -1721,93 +1721,83 @@ 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 True True ty1 ty2
- -- convert Just True to Just False
- invis :: Maybe Bool -> Maybe Bool
- invis = fmap (const False)
+-- | 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 True False ty1 ty2
-(<!>) :: 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 <!>
+-- | 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 True ty1 ty2
-- | 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 vis env (TyVarTy tv1) (TyVarTy tv2)
- = check vis $ rnOccL env tv1 == rnOccR env tv2
+ go env (TyVarTy tv1) (TyVarTy tv2)
+ = rnOccL env tv1 == rnOccR env tv2
- go vis _ (LitTy lit1) (LitTy lit2)
- = check vis $ lit1 == lit2
+ go _ (LitTy lit1) (LitTy lit2)
+ = 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]
@@ -1817,30 +1807,20 @@ 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
+ 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
--- | 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
{- *********************************************************************
* *
@@ -1972,7 +1952,7 @@ boxEqPred eq_rel ty1 ty2
where
k1 = tcTypeKind ty1
k2 = tcTypeKind ty2
- homo_kind = k1 `tcEqType` k2
+ homo_kind = k1 `tcEqType` k2 -- Constraints here are inert, so tcEqType is fine
pickCapturedPreds
:: TyVarSet -- Quantifying over these
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index f51c7241a8..6840a14ef5 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -435,16 +435,15 @@ matchExpectedAppTy orig_ty
-- Defer splitting by generating an equality constraint
defer
- = do { ty1 <- newFlexiTyVarTy kind1
+ = do { orig_kind <- tcTypeKindM orig_ty
+ ; let kind1 = mkFunTy liftedTypeKind orig_kind
+ kind2 = liftedTypeKind -- m :: * -> k
+ -- arg type :: *
+ ; ty1 <- newFlexiTyVarTy kind1
; ty2 <- newFlexiTyVarTy kind2
; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
; return (co, (ty1, ty2)) }
- orig_kind = tcTypeKind orig_ty
- kind1 = mkFunTy liftedTypeKind orig_kind
- kind2 = liftedTypeKind -- m :: * -> k
- -- arg type :: *
-
{-
************************************************************************
* *
@@ -790,7 +789,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
@@ -909,9 +908,11 @@ fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
where
check_hole ty -- Debug check only
= do { let ty_lvl = tcTypeLevel ty
- ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
- ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
- ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
+ ; when debugIsOn $
+ do { kind <- tcTypeKindM ty
+ ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl)
+ , ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
+ ppr ty <+> dcolon <+> ppr kind $$ ppr orig_ty ) }
; cts <- readTcRef ref
; case cts of
Just already_there -> pprPanic "writeExpType"
@@ -993,12 +994,12 @@ promoteTcType dest_lvl ty
dont_promote_it :: TcM (TcCoercion, TcType)
dont_promote_it -- Check that ty :: TYPE rr, for some (fresh) rr
= do { res_kind <- newOpenTypeKind
- ; let ty_kind = tcTypeKind ty
- kind_orig = TypeEqOrigin { uo_actual = ty_kind
+ ; ty_kind <- tcTypeKindM ty
+ ; let kind_orig = TypeEqOrigin { uo_actual = ty_kind
, uo_expected = res_kind
, uo_thing = Nothing
, uo_visible = False }
- ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind
+ ; ki_co <- uType KindLevel kind_orig ty_kind res_kind
; let co = mkTcGReflRightCo Nominal ty ki_co
; return (co, ty `mkCastTy` ki_co) }
@@ -1639,10 +1640,11 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
go dflags cur_lvl
| canSolveByUnification cur_lvl tv1 ty2
, Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
- = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
+ = do { k2' <- tcTypeKindM ty2'
+ ; co_k <- uType KindLevel kind_origin k2' (tyVarKind tv1)
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
- , ppr ty2 <+> dcolon <+> ppr (tcTypeKind ty2)
+ , ppr ty2 <+> dcolon <+> ppr k2'
, ppr (isTcReflCo co_k), ppr co_k ]
; if isTcReflCo co_k -- only proceed if the kinds matched.
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 0fff81c2ab..2321bf4f32 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -39,7 +39,7 @@ module Type (
mkForAllTy, mkForAllTys, mkTyCoInvForAllTys, mkSpecForAllTys,
mkVisForAllTys, mkTyCoInvForAllTy,
mkInvForAllTy, mkInvForAllTys,
- splitForAllTys, splitForAllVarBndrs,
+ splitForAllTys, splitTyVarForAllTys, splitForAllVarBndrs,
splitForAllTy_maybe, splitForAllTy,
splitForAllTy_ty_maybe, splitForAllTy_co_maybe,
splitPiTy_maybe, splitPiTy, splitPiTys,
@@ -132,7 +132,7 @@ module Type (
Kind,
-- ** Finding the kind of a type
- typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly,
+ typeKind, tcTypeKind, typeLiteralKind, isTypeLevPoly, resultIsLevPoly,
tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
-- ** Common Kind
@@ -1820,6 +1820,10 @@ isEvVarType :: Type -> Bool
-- See Note [Evidence for quantified constraints]
isEvVarType ty = isCoVarType ty || isPredTy ty
+isPredTy :: Type -> Bool
+-- See Note [Types for coercions, predicates, and evidence]
+isPredTy ty = tcIsConstraintKind (typeKind ty)
+
-- | Does this type classify a core (unlifted) Coercion?
-- At either role nominal or representational
-- (t1 ~# t2) or (t1 ~R# t2)
@@ -2701,6 +2705,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
@@ -2726,17 +2731,17 @@ typeKind ty@(ForAllTy {})
(tvs, body) = splitTyVarForAllTys ty
body_kind = typeKind body
------------------------------
+----------------------------
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
-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 (TyVarTy tyvar) = tyVarKind tyvar
+tcTypeKind (CastTy _ty co) = pSnd $ coercionKind co
+tcTypeKind (CoercionTy co) = coercionType co
tcTypeKind (AppTy fun arg)
= go fun [arg]
@@ -2750,7 +2755,6 @@ tcTypeKind (AppTy fun arg)
tcTypeKind ty@(ForAllTy {})
| tcIsConstraintKind body_kind
= constraintKind
-
| otherwise
= case occCheckExpand tvs body_kind of -- We must make sure tv does not occur in kind
Just k' -> k' -- As it is already out of scope!
@@ -2758,19 +2762,12 @@ tcTypeKind ty@(ForAllTy {})
(ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
where
(tvs, body) = splitTyVarForAllTys ty
- body_kind = tcTypeKind body
-
-
-isPredTy :: Type -> Bool
--- See Note [Types for coercions, predicates, and evidence]
-isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
+ body_kind = tcTypeKind body
--------------------------
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.
View Lorry Controller Status