diff options
66 files changed, 1671 insertions, 1152 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 9ffcabd3a3..21d537112e 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -39,8 +39,8 @@ module GHC.Core.Coercion ( mkSymCo, mkTransCo, mkSelCo, getNthFun, getNthFromType, mkLRCo, mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, - mkFunCo1, mkFunCo2, mkFunCoNoFTF, mkFunResCo, - mkNakedFunCo1, mkNakedFunCo2, + mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo, + mkNakedFunCo, mkForAllCo, mkForAllCos, mkHomoForAllCos, mkPhantomCo, mkHoleCo, mkUnivCo, mkSubCo, @@ -51,7 +51,7 @@ module GHC.Core.Coercion ( castCoercionKind, castCoercionKind1, castCoercionKind2, mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole, - mkHeteroPrimEqPred, mkHeteroReprPrimEqPred, + mkNomPrimEqPred, -- ** Decomposition instNewTyCon_maybe, @@ -811,29 +811,20 @@ mkFunCoNoFTF r w arg_co res_co -- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@. -- This (most common) version takes a single FunTyFlag, which is used -- for both fco_afl and ftf_afr of the FunCo -mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion -mkFunCo1 r af w arg_co res_co +mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion +mkFunCo r af w arg_co res_co = mkFunCo2 r af af w arg_co res_co -mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion --- This version of mkFunCo1 does not check FunCo invariants (checkFunCo) --- It is called during typechecking on un-zonked types; --- in particular there may be un-zonked coercion variables. -mkNakedFunCo1 r af w arg_co res_co - = mkNakedFunCo2 r af af w arg_co res_co +mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion +-- This version of mkFunCo does not check FunCo invariants (checkFunCo) +-- It's a historical vestige; See Note [No assertion check on mkFunCo] +mkNakedFunCo = mkFunCo -mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag - -> CoercionN -> Coercion -> Coercion -> Coercion +mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag + -> CoercionN -> Coercion -> Coercion -> Coercion -- This is the smart constructor for FunCo; it checks invariants mkFunCo2 r afl afr w arg_co res_co - = assertPprMaybe (checkFunCo r afl afr w arg_co res_co) $ - mkNakedFunCo2 r afl afr w arg_co res_co - -mkNakedFunCo2 :: Role -> FunTyFlag -> FunTyFlag - -> CoercionN -> Coercion -> Coercion -> Coercion --- This is the smart constructor for FunCo --- "Naked"; it does not check invariants -mkNakedFunCo2 r afl afr w arg_co res_co + -- See Note [No assertion check on mkFunCo] | Just (ty1, _) <- isReflCo_maybe arg_co , Just (ty2, _) <- isReflCo_maybe res_co , Just (w, _) <- isReflCo_maybe w @@ -844,6 +835,19 @@ mkNakedFunCo2 r afl afr w arg_co res_co , fco_mult = w, fco_arg = arg_co, fco_res = res_co } +{- Note [No assertion check on mkFunCo] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We used to have a checkFunCo assertion on mkFunCo, but during typechecking +we can (legitimately) have not-full-zonked types or coercion variables, so +the assertion spuriously fails (test T11480b is a case in point). Lint +checks all these things anyway. + +We used to get around the problem by calling mkNakedFunCo from within the +typechecker, which dodged the assertion check. But then mkAppCo calls +mkTyConAppCo, which calls tyConAppFunCo_maybe, which calls mkFunCo. +Duplicating this stack of calls with "naked" versions of each seems too much. + +-- Commented out: see Note [No assertion check on mkFunCo] checkFunCo :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Maybe SDoc @@ -875,6 +879,7 @@ checkFunCo _r afl afr _w arg_co res_co ok ty = isTYPEorCONSTRAINT (typeKind ty) pp_ty str ty = text str <> colon <+> hang (ppr ty) 2 (dcolon <+> ppr (typeKind ty)) +-} -- | Apply a 'Coercion' to another 'Coercion'. -- The second coercion must be Nominal, unless the first is Phantom. @@ -2077,7 +2082,7 @@ ty_co_subst !lc role ty liftCoSubstTyVar lc r tv go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2) go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRoleListX r tc) tys) - go r (FunTy af w t1 t2) = mkFunCo1 r af (go Nominal w) (go r t1) (go r t2) + go r (FunTy af w t1 t2) = mkFunCo r af (go Nominal w) (go r t1) (go r t2) go r t@(ForAllTy (Bndr v _) ty) = let (lc', v', h) = liftCoSubstVarBndr lc v body_co = ty_co_subst lc' r ty in @@ -2606,7 +2611,8 @@ mkCoercionType Phantom = \ty1 ty2 -> in TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2] --- | Creates a primitive type equality predicate. +-- | Creates a primitive nominal type equality predicate. +-- t1 ~# t2 -- Invariant: the types are not Coercions mkPrimEqPred :: Type -> Type -> Type mkPrimEqPred ty1 ty2 @@ -2615,22 +2621,9 @@ mkPrimEqPred ty1 ty2 k1 = typeKind ty1 k2 = typeKind ty2 --- | Makes a lifted equality predicate at the given role -mkPrimEqPredRole :: Role -> Type -> Type -> PredType -mkPrimEqPredRole Nominal = mkPrimEqPred -mkPrimEqPredRole Representational = mkReprPrimEqPred -mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom" - --- | Creates a primitive type equality predicate with explicit kinds -mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type -mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2] - --- | Creates a primitive representational type equality predicate --- with explicit kinds -mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type -mkHeteroReprPrimEqPred k1 k2 ty1 ty2 - = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2] - +-- | Creates a primitive representational type equality predicate. +-- t1 ~R# t2 +-- Invariant: the types are not Coercions mkReprPrimEqPred :: Type -> Type -> Type mkReprPrimEqPred ty1 ty2 = mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2] @@ -2638,6 +2631,17 @@ mkReprPrimEqPred ty1 ty2 k1 = typeKind ty1 k2 = typeKind ty2 +-- | Makes a lifted equality predicate at the given role +mkPrimEqPredRole :: Role -> Type -> Type -> PredType +mkPrimEqPredRole Nominal = mkPrimEqPred +mkPrimEqPredRole Representational = mkReprPrimEqPred +mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom" + +-- | Creates a primitive nominal type equality predicate with an explicit +-- (but homogeneous) kind: (~#) k k ty1 ty2 +mkNomPrimEqPred :: Kind -> Type -> Type -> Type +mkNomPrimEqPred k ty1 ty2 = mkTyConApp eqPrimTyCon [k, k, ty1, ty2] + -- | Assuming that two types are the same, ignoring coercions, find -- a nominal coercion between the types. This is useful when optimizing -- transitivity over coercion applications, where splitting two @@ -2668,7 +2672,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2 go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = arg1, ft_res = res1 }) (FunTy { ft_af = af2, ft_mult = w2, ft_arg = arg2, ft_res = res2 }) = assert (af1 == af2) $ - mkFunCo1 Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2) + mkFunCo Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2) go (TyConApp tc1 args1) (TyConApp tc2 args2) = assert (tc1 == tc2) $ @@ -2749,15 +2753,17 @@ has_co_hole_co :: Coercion -> Monoid.Any folder = TyCoFolder { tcf_view = noView , tcf_tyvar = const2 (Monoid.Any False) , tcf_covar = const2 (Monoid.Any False) - , tcf_hole = const2 (Monoid.Any True) + , tcf_hole = \_ hole -> Monoid.Any (isHeteroKindCoHole hole) , tcf_tycobinder = const2 } --- | Is there a coercion hole in this type? +-- | Is there a hetero-kind coercion hole in this type? +-- (That is, a coercion hole with ch_hetero_kind=True.) +-- See wrinkle (EIK2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality hasCoercionHoleTy :: Type -> Bool hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty --- | Is there a coercion hole in this coercion? +-- | Is there a hetero-kind coercion hole in this coercion? hasCoercionHoleCo :: Coercion -> Bool hasCoercionHoleCo = Monoid.getAny . has_co_hole_co diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot index 0d56cf628c..3143414feb 100644 --- a/compiler/GHC/Core/Coercion.hs-boot +++ b/compiler/GHC/Core/Coercion.hs-boot @@ -17,9 +17,9 @@ mkReflCo :: Role -> Type -> Coercion mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion mkAppCo :: Coercion -> Coercion -> Coercion mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion -mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion -mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion -mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion +mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion +mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion +mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion mkCoVarCo :: CoVar -> Coercion mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion mkPhantomCo :: Coercion -> Type -> Type -> Coercion diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs index c8d280259a..2fc07e1be1 100644 --- a/compiler/GHC/Core/Predicate.hs +++ b/compiler/GHC/Core/Predicate.hs @@ -16,7 +16,7 @@ module GHC.Core.Predicate ( getEqPredTys, getEqPredTys_maybe, getEqPredRole, predTypeEqRel, mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole, - mkHeteroPrimEqPred, mkHeteroReprPrimEqPred, + mkNomPrimEqPred, -- Class predicates mkClassPred, isDictTy, typeDeterminesValue, diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs index 07d7a93748..a4f1df4f70 100644 --- a/compiler/GHC/Core/Reduction.hs +++ b/compiler/GHC/Core/Reduction.hs @@ -361,8 +361,8 @@ mkFunRedn r af (Reduction arg_co arg_ty) (Reduction res_co res_ty) = mkReduction - (mkFunCo1 r af w_co arg_co res_co) - (mkFunTy af w_ty arg_ty res_ty) + (mkFunCo r af w_co arg_co res_co) + (mkFunTy af w_ty arg_ty res_ty) {-# INLINE mkFunRedn #-} -- | Create a 'Reduction' associated to a Π type, diff --git a/compiler/GHC/Core/TyCo/Compare.hs b/compiler/GHC/Core/TyCo/Compare.hs index 4ef9d04eb8..9c32675d3e 100644 --- a/compiler/GHC/Core/TyCo/Compare.hs +++ b/compiler/GHC/Core/TyCo/Compare.hs @@ -379,7 +379,7 @@ We perform this optimisation in a number of places: * GHC.Core.Types.eqType * GHC.Core.Types.nonDetCmpType * GHC.Core.Unify.unify_ty - * TcCanonical.can_eq_nc' + * GHC.Tc.Solver.Equality.can_eq_nc' * TcUnify.uType This optimisation is especially helpful for the ubiquitous GHC.Types.Type, diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 8417ded123..245a1c507b 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -38,7 +38,7 @@ module GHC.Core.TyCo.Rep ( -- * Coercions Coercion(..), CoSel(..), FunSel(..), UnivCoProvenance(..), - CoercionHole(..), coHoleCoVar, setCoHoleCoVar, + CoercionHole(..), coHoleCoVar, setCoHoleCoVar, isHeteroKindCoHole, CoercionN, CoercionR, CoercionP, KindCoercion, MCoercion(..), MCoercionR, MCoercionN, @@ -1454,12 +1454,20 @@ data CoercionHole = CoercionHole { ch_co_var :: CoVar -- See Note [CoercionHoles and coercion free variables] - , ch_ref :: IORef (Maybe Coercion) + , ch_ref :: IORef (Maybe Coercion) + + , ch_hetero_kind :: Bool + -- True <=> arises from a kind-level equality + -- See Note [Equalities with incompatible kinds] + -- in GHC.Tc.Solver.Equality, wrinkle (EIK2) } coHoleCoVar :: CoercionHole -> CoVar coHoleCoVar = ch_co_var +isHeteroKindCoHole :: CoercionHole -> Bool +isHeteroKindCoHole = ch_hetero_kind + setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole setCoHoleCoVar h cv = h { ch_co_var = cv } @@ -1470,7 +1478,8 @@ instance Data.Data CoercionHole where dataTypeOf _ = mkNoRepType "CoercionHole" instance Outputable CoercionHole where - ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv) + ppr (CoercionHole { ch_co_var = cv, ch_hetero_kind = hk }) + = braces (ppr cv <> ppWhen hk (text "[hk]")) instance Uniquable CoercionHole where getUnique (CoercionHole { ch_co_var = cv }) = getUnique cv diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs index ebf87dae94..4224bd127b 100644 --- a/compiler/GHC/Core/TyCo/Subst.hs +++ b/compiler/GHC/Core/TyCo/Subst.hs @@ -387,9 +387,9 @@ extendTvSubstWithClone :: Subst -> TyVar -> TyVar -> Subst -- those variables should be in scope already extendTvSubstWithClone (Subst in_scope idenv tenv cenv) tv tv' = Subst (extendInScopeSet in_scope tv') - idenv - (extendVarEnv tenv tv (mkTyVarTy tv')) - cenv + idenv + (extendVarEnv tenv tv (mkTyVarTy tv')) + cenv -- | Add a substitution from a 'CoVar' to a 'Coercion' to the 'Subst': -- you must ensure that the in-scope set satisfies diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs index 796fb5aecd..5e4be72a34 100644 --- a/compiler/GHC/Core/Type.hs +++ b/compiler/GHC/Core/Type.hs @@ -274,7 +274,7 @@ import {-# SOURCE #-} GHC.Core.Coercion , mkTyConAppCo, mkAppCo , mkForAllCo, mkFunCo2, mkAxiomInstCo, mkUnivCo , mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo - , mkKindCo, mkSubCo, mkFunCo1 + , mkKindCo, mkSubCo, mkFunCo , decomposePiCos, coercionKind , coercionRKind, coercionType , isReflexiveCo, seqCo @@ -1332,7 +1332,7 @@ tyConAppFunCo_maybe :: HasDebugCallStack => Role -> TyCon -> [Coercion] -- ^ Return Just if this TyConAppCo should be represented as a FunCo tyConAppFunCo_maybe r tc cos | Just (af, mult, arg, res) <- ty_con_app_fun_maybe (mkReflCo r manyDataConTy) tc cos - = Just (mkFunCo1 r af mult arg res) + = Just (mkFunCo r af mult arg res) | otherwise = Nothing ty_con_app_fun_maybe :: (HasDebugCallStack, Outputable a) => a -> TyCon -> [a] diff --git a/compiler/GHC/HsToCore.hs b/compiler/GHC/HsToCore.hs index 57f1b13391..c99320e768 100644 --- a/compiler/GHC/HsToCore.hs +++ b/compiler/GHC/HsToCore.hs @@ -764,7 +764,7 @@ mkUnsafeCoercePrimPair _old_id old_expr unsafe_equality k a b = ( mkTyApps (Var unsafe_equality_proof_id) [k,b,a] , mkTyConApp unsafe_equality_tc [k,b,a] - , mkHeteroPrimEqPred k k a b + , mkNomPrimEqPred k a b ) -- NB: UnsafeRefl :: (b ~# a) -> UnsafeEquality a b, so we have to -- carefully swap the arguments above diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index ed102d9bb5..66f0cf118a 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -462,8 +462,8 @@ mkErrorItem ct ; (suppress, m_evdest) <- case ctEvidence ct of CtGiven {} -> return (False, Nothing) CtWanted { ctev_rewriters = rewriters, ctev_dest = dest } - -> do { supp <- anyUnfilledCoercionHoles rewriters - ; return (supp, Just dest) } + -> do { rewriters' <- zonkRewriterSet rewriters + ; return (not (isEmptyRewriterSet rewriters'), Just dest) } ; let m_reason = case ct of CIrredCan { cc_reason = reason } -> Just reason _ -> Nothing @@ -492,20 +492,24 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics , text "tidy_items1 =" <+> ppr tidy_items1 , text "tidy_errs =" <+> ppr tidy_errs ]) - -- Catch an awkward case in which /all/ errors are suppressed: - -- see Wrinkle at end of Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint - -- Unless we are sure that an error will be reported some other way (details - -- in the defn of tidy_items) un-suppress the lot. This makes sure we don't forget to - -- report an error at all, which is catastrophic: GHC proceeds to desguar and optimise - -- the program, even though it is full of type errors (#22702, #22793) + -- Catch an awkward (and probably rare) case in which /all/ errors are + -- suppressed: see Wrinkle (WRW2) in Note [Prioritise Wanteds with empty + -- RewriterSet] in GHC.Tc.Types.Constraint. + -- + -- Unless we are sure that an error will be reported some other way + -- (details in the defn of tidy_items) un-suppress the lot. This makes + -- sure we don't forget to report an error at all, which is + -- catastrophic: GHC proceeds to desguar and optimise the program, even + -- though it is full of type errors (#22702, #22793) ; errs_already <- ifErrsM (return True) (return False) ; let tidy_items | not errs_already -- Have not already reported an error (perhaps -- from an outer implication); see #21405 , not (any ignoreConstraint simples) -- No error is ignorable (is reported elsewhere) , all ei_suppress tidy_items1 -- All errors are suppressed - = map unsuppressErrorItem tidy_items1 - | otherwise = tidy_items1 + = map unsuppressErrorItem tidy_items1 + | otherwise + = tidy_items1 -- First, deal with any out-of-scope errors: ; let (out_of_scope, other_holes, not_conc_errs) = partition_errors tidy_errs @@ -1804,8 +1808,8 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2 return (main_msg, []) -- Incompatible kinds - -- This is wrinkle (4) in Note [Equalities with incompatible kinds] in - -- GHC.Tc.Solver.Canonical + -- This is wrinkle (EIK2) in Note [Equalities with incompatible kinds] + -- in GHC.Tc.Solver.Equality | hasCoercionHoleCo co1 || hasCoercionHoleTy ty2 = return (mkBlockedEqErr item, []) @@ -1987,8 +1991,8 @@ misMatchOrCND insoluble_occurs_check ctxt item ty1 ty2 -- Keep only UserGivens that have some equalities. -- See Note [Suppress redundant givens during error reporting] --- These are for the "blocked" equalities, as described in TcCanonical --- Note [Equalities with incompatible kinds], wrinkle (2). There should +-- These are for the "blocked" equalities, as described in GHC.Tc.Solver.Equality +-- Note [Equalities with incompatible kinds], wrinkle (EIK2). There should -- always be another unsolved wanted around, which will ordinarily suppress -- this message. But this can still be printed out with -fdefer-type-errors -- (sigh), so we must produce a message. diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs index 68c5ca2869..4c2d29a0b5 100644 --- a/compiler/GHC/Tc/Errors/Types.hs +++ b/compiler/GHC/Tc/Errors/Types.hs @@ -4755,7 +4755,7 @@ data TcSolverReportMsg | BlockedEquality ErrorItem -- These are for the "blocked" equalities, as described in -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical, - -- wrinkle (2). There should always be another unsolved wanted around, + -- wrinkle (EIK2). There should always be another unsolved wanted around, -- which will ordinarily suppress this message. But this can still be printed out -- with -fdefer-type-errors (sigh), so we must produce a message. diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 9e8375b47d..dd1b0c0eca 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -388,11 +388,11 @@ kcClassSigType :: [LocatedN Name] -> LHsSigType GhcRn -> TcM () -- meth :: forall a (x :: f a). Proxy x -> () -- When instantiating Proxy with kappa, we must unify kappa := f a. But we're -- still working out the kind of f, and thus f a will have a coercion in it. --- Coercions block unification (Note [Equalities with incompatible kinds] in --- TcCanonical) and so we fail to unify. If we try to kind-generalize, we'll --- end up promoting kappa to the top level (because kind-generalization is --- normally done right before adding a binding to the context), and then we --- can't set kappa := f a, because a is local. +-- Coercions may block unification (Note [Equalities with incompatible kinds] in +-- GHC.Tc.Solver.Equality, wrinkle (EIK2)) and so we fail to unify. If we try to +-- kind-generalize, we'll end up promoting kappa to the top level (because +-- kind-generalization is normally done right before adding a binding to the context), +-- and then we can't set kappa := f a, because a is local. kcClassSigType names sig_ty@(L _ (HsSig { sig_bndrs = hs_outer_bndrs, sig_body = hs_ty })) = addSigCtxt (funsSigCtxt names) sig_ty $ @@ -1932,7 +1932,7 @@ checkExpectedKind hs_ty ty act_kind exp_kind ; if act_kind' `tcEqType` exp_kind then return res_ty -- This is very common - else do { co_k <- uType KindLevel origin act_kind' exp_kind + else do { co_k <- unifyTypeAndEmit KindLevel origin act_kind' exp_kind ; traceTc "checkExpectedKind" (vcat [ ppr act_kind , ppr exp_kind , ppr co_k ]) diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index 121c43b987..397acd214c 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -133,7 +133,7 @@ tcRule (HsRule { rd_ext = ext , ppr lhs_wanted , ppr rhs_wanted ]) - ; (lhs_evs, residual_lhs_wanted) + ; (lhs_evs, residual_lhs_wanted, dont_default) <- simplifyRule name tc_lvl lhs_wanted rhs_wanted -- SimplifyRule Plan, step 4 @@ -153,15 +153,14 @@ tcRule (HsRule { rd_ext = ext -- See Note [Re-quantify type variables in rules] ; forall_tkvs <- candidateQTyVarsOfTypes (rule_ty : map idType tpl_ids) - ; let don't_default = nonDefaultableTyVarsOfWC residual_lhs_wanted - ; let weed_out = (`dVarSetMinusVarSet` don't_default) + ; let weed_out = (`dVarSetMinusVarSet` dont_default) quant_cands = forall_tkvs { dv_kvs = weed_out (dv_kvs forall_tkvs) , dv_tvs = weed_out (dv_tvs forall_tkvs) } ; qtkvs <- quantifyTyVars skol_info DefaultNonStandardTyVars quant_cands ; traceTc "tcRule" (vcat [ pprFullRuleName (snd ext) rname , text "forall_tkvs:" <+> ppr forall_tkvs , text "quant_cands:" <+> ppr quant_cands - , text "don't_default:" <+> ppr don't_default + , text "dont_default:" <+> ppr dont_default , text "residual_lhs_wanted:" <+> ppr residual_lhs_wanted , text "qtkvs:" <+> ppr qtkvs , text "rule_ty:" <+> ppr rule_ty @@ -401,7 +400,8 @@ simplifyRule :: RuleName -> WantedConstraints -- Constraints from LHS -> WantedConstraints -- Constraints from RHS -> TcM ( [EvVar] -- Quantify over these LHS vars - , WantedConstraints) -- Residual un-quantified LHS constraints + , WantedConstraints -- Residual un-quantified LHS constraints + , TcTyVarSet ) -- Don't default these -- See Note [The SimplifyRule Plan] -- NB: This consumes all simple constraints on the LHS, but not -- any LHS implication constraints. @@ -413,14 +413,23 @@ simplifyRule name tc_lvl lhs_wanted rhs_wanted -- Why clone? See Note [Simplify cloned constraints] ; lhs_clone <- cloneWC lhs_wanted ; rhs_clone <- cloneWC rhs_wanted - ; setTcLevel tc_lvl $ - discardResult $ - runTcS $ - do { _ <- solveWanteds lhs_clone - ; _ <- solveWanteds rhs_clone - -- Why do them separately? - -- See Note [Solve order for RULES] - ; return () } + ; (dont_default, _) + <- setTcLevel tc_lvl $ + runTcS $ + do { lhs_wc <- solveWanteds lhs_clone + ; _rhs_wc <- solveWanteds rhs_clone + -- Why do them separately? + -- See Note [Solve order for RULES] + + ; let dont_default = nonDefaultableTyVarsOfWC lhs_wc + -- If lhs_wanteds has + -- (a[sk] :: TYPE rr[sk]) ~ (b0[tau] :: TYPE r0[conc]) + -- we want r0 to be non-defaultable; + -- see nonDefaultableTyVarsOfWC. Simplest way to get + -- this is to look at the post-simplified lhs_wc, which + -- will contain (rr[sk] ~ r0[conc)]. An example is in + -- test rep-poly/RepPolyRule1 + ; return dont_default } -- Note [The SimplifyRule Plan] step 2 ; lhs_wanted <- zonkWC lhs_wanted @@ -435,9 +444,10 @@ simplifyRule name tc_lvl lhs_wanted rhs_wanted , text "rhs_wanted" <+> ppr rhs_wanted , text "quant_cts" <+> ppr quant_cts , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted + , text "dont_default" <+> ppr dont_default ] - ; return (quant_evs, residual_lhs_wanted) } + ; return (quant_evs, residual_lhs_wanted, dont_default) } where mk_quant_ev :: Ct -> TcM EvVar diff --git a/compiler/GHC/Tc/Plugin.hs b/compiler/GHC/Tc/Plugin.hs index 30f5ef7520..df532f7ac2 100644 --- a/compiler/GHC/Tc/Plugin.hs +++ b/compiler/GHC/Tc/Plugin.hs @@ -184,7 +184,7 @@ newEvVar = unsafeTcPluginTcM . TcM.newEvVar -- | Create a fresh coercion hole. -- This should only be invoked within 'tcPluginSolve'. newCoercionHole :: PredType -> TcPluginM CoercionHole -newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole +newCoercionHole = unsafeTcPluginTcM . TcM.newVanillaCoercionHole -- | Bind an evidence variable. -- diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index eaa62e44ea..9c371af463 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -3088,6 +3088,18 @@ neededEvVars implic@(Implic { ic_given = givens ------------------------------------------------- simplifyDelayedErrors :: Bag DelayedError -> TcS (Bag DelayedError) +-- Simplify any delayed errors: e.g. type and term holes +-- NB: At this point we have finished with all the simple +-- constraints; they are in wc_simple, not in the inert set. +-- So those Wanteds will not rewrite these delayed errors. +-- That's probably no bad thing. +-- +-- However if we have [W] alpha ~ Maybe a, [W] alpha ~ Int +-- and _ : alpha, then we'll /unify/ alpha with the first of +-- the Wanteds we get, and thereby report (_ : Maybe a) or +-- (_ : Int) unpredictably, depending on which we happen to see +-- first. Doesn't matter much; there is a type error anyhow. +-- T17139 is a case in point. simplifyDelayedErrors = mapBagM simpl_err where simpl_err :: DelayedError -> TcS DelayedError @@ -3104,6 +3116,7 @@ simplifyDelayedErrors = mapBagM simpl_err -- code, because we have all the givens already set up simpl_hole h@(Hole { hole_ty = ty, hole_loc = loc }) = do { ty' <- rewriteType loc ty + ; traceTcS "simpl_hole" (ppr ty $$ ppr ty') ; return (h { hole_ty = ty' }) } {- Note [Delete dead Given evidence bindings] diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 187cdc9c8b..49210cefa8 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -5,7 +5,6 @@ module GHC.Tc.Solver.Canonical( canonicalize, - unifyWanted, makeSuperClasses, StopOrContinue(..), stopWith, continueWith, andWhenContinue, solveCallStack -- For GHC.Tc.Solver @@ -144,7 +143,7 @@ canClassNC ev cls tys = do { dflags <- getDynFlags ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev [] [] cls tys -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - ; emitWork sc_cts + ; emitWork (listToBag sc_cts) ; canClass ev cls tys doNotExpand } -- doNotExpand: We have already expanded superclasses for /this/ dict -- so set the fuel to doNotExpand to avoid repeating expansion @@ -211,15 +210,13 @@ canClass ev cls tys pend_sc = -- all classes do *nominal* matching assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $ do { (redns@(Reductions _ xis), rewriters) <- rewriteArgsNom ev cls_tc tys - ; let redn@(Reduction _ xi) = mkClassPredRedn cls redns - mk_ct new_ev = CDictCan { cc_ev = new_ev - , cc_tyargs = xis - , cc_class = cls - , cc_pend_sc = pend_sc } - ; mb <- rewriteEvidence rewriters ev redn - ; traceTcS "canClass" (vcat [ ppr ev - , ppr xi, ppr mb ]) - ; return (fmap mk_ct mb) } + ; let redn = mkClassPredRedn cls redns + ; rewriteEvidence rewriters ev redn $ \new_ev -> + do { traceTcS "canClass" (vcat [ ppr new_ev, ppr (reductionReducedType redn) ]) + ; continueWith (CDictCan { cc_ev = new_ev + , cc_tyargs = xis + , cc_class = cls + , cc_pend_sc = pend_sc }) }} where cls_tc = classTyCon cls @@ -738,7 +735,7 @@ canIrred ev = do { let pred = ctEvPred ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred) ; (redn, rewriters) <- rewrite ev pred - ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev -> + ; rewriteEvidence rewriters ev redn $ \ new_ev -> do { -- Re-classify, in case rewriting has improved its shape -- Code is like the canNC, except @@ -843,7 +840,7 @@ canForAllNC ev tvs theta pred = do { dflags <- getDynFlags ; sc_cts <- mkStrictSuperClasses (givensFuel dflags) ev tvs theta cls tys -- givensFuel dflags: See Note [Expanding Recursive Superclasses and ExpansionFuel] - ; emitWork sc_cts + ; emitWork (listToBag sc_cts) ; canForAll ev doNotExpand } -- doNotExpand: as we have already (eagerly) expanded superclasses for this class @@ -863,9 +860,8 @@ canForAll :: CtEvidence -> ExpansionFuel -> TcS (StopOrContinue Ct) -- We have a constraint (forall as. blah => C tys) canForAll ev fuel = do { -- First rewrite it to apply the current substitution - let pred = ctEvPred ev - ; (redn, rewriters) <- rewrite ev pred - ; rewriteEvidence rewriters ev redn `andWhenContinue` \ new_ev -> + ; (redn, rewriters) <- rewrite ev (ctEvPred ev) + ; rewriteEvidence rewriters ev redn $ \ new_ev -> do { -- Now decompose into its pieces and solve it -- (It takes a lot less code to rewrite before decomposing.) @@ -979,32 +975,29 @@ rewriteEvidence :: RewriterSet -- ^ See Note [Wanteds rewrite Wanteds] -- in GHC.Tc.Types.Constraint -> CtEvidence -- ^ old evidence -> Reduction -- ^ new predicate + coercion, of type <type of old evidence> ~ new predicate - -> TcS (StopOrContinue CtEvidence) --- Returns Just new_ev iff either (i) 'co' is reflexivity --- or (ii) 'co' is not reflexivity, and 'new_pred' not cached --- In either case, there is nothing new to do with new_ev -{- - rewriteEvidence old_ev new_pred co -Main purpose: create new evidence for new_pred; - unless new_pred is cached already -* Returns a new_ev : new_pred, with same wanted/given flag as old_ev -* If old_ev was wanted, create a binding for old_ev, in terms of new_ev -* If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev -* Returns Nothing if new_ev is already cached - - Old evidence New predicate is Return new evidence - flavour of same flavor - ------------------------------------------------------------------- - Wanted Already solved or in inert Nothing - Not Just new_evidence - - Given Already in inert Nothing - Not Just new_evidence - -Note [Rewriting with Refl] -~~~~~~~~~~~~~~~~~~~~~~~~~~ + -> (CtEvidence -> TcS (StopOrContinue Ct)) + -> TcS (StopOrContinue Ct) +-- (rewriteEvidence old_ev new_pred co do_next) +-- Main purpose: create new evidence for new_pred; +-- unless new_pred is cached already +-- * Calls do_next with (new_ev :: new_pred), with same wanted/given flag as old_ev +-- * If old_ev was wanted, create a binding for old_ev, in terms of new_ev +-- * If old_ev was given, AND not cached, create a binding for new_ev, in terms of old_ev +-- * Stops if new_ev is already cached +-- +-- Old evidence New predicate is Return new evidence +-- flavour of same flavor +-- ------------------------------------------------------------------- +-- Wanted Already solved or in inert Stop +-- Not do_next new_evidence +-- +-- Given Already in inert Stop +-- Not do_next new_evidence + +{- Note [Rewriting with Refl] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ If the coercion is just reflexivity then you may re-use the same -variable. But be careful! Although the coercion is Refl, new_pred +evidence variable. But be careful! Although the coercion is Refl, new_pred may reflect the result of unification alpha := ty, so new_pred might not _look_ the same as old_pred, and it's vital to proceed from now on using new_pred. @@ -1017,16 +1010,16 @@ the rewriter set. We check this with an assertion. -} -rewriteEvidence rewriters old_ev (Reduction co new_pred) +rewriteEvidence rewriters old_ev (Reduction co new_pred) do_next | isReflCo co -- See Note [Rewriting with Refl] = assert (isEmptyRewriterSet rewriters) $ - continueWith (setCtEvPredType old_ev new_pred) + do_next (setCtEvPredType old_ev new_pred) rewriteEvidence rewriters ev@(CtGiven { ctev_evar = old_evar, ctev_loc = loc }) - (Reduction co new_pred) + (Reduction co new_pred) do_next = assert (isEmptyRewriterSet rewriters) $ -- this is a Given, not a wanted do { new_ev <- newGivenEvVar loc (new_pred, new_tm) - ; continueWith new_ev } + ; do_next new_ev } where -- mkEvCast optimises ReflCo new_tm = mkEvCast (evId old_evar) @@ -1036,14 +1029,14 @@ rewriteEvidence new_rewriters ev@(CtWanted { ctev_dest = dest , ctev_loc = loc , ctev_rewriters = rewriters }) - (Reduction co new_pred) + (Reduction co new_pred) do_next = do { mb_new_ev <- newWanted loc rewriters' new_pred ; massert (coercionRole co == ctEvRole ev) ; setWantedEvTerm dest IsCoherent $ mkEvCast (getEvExpr mb_new_ev) (downgradeRole Representational (ctEvRole ev) (mkSymCo co)) ; case mb_new_ev of - Fresh new_ev -> continueWith new_ev + Fresh new_ev -> do_next new_ev Cached _ -> stopWith ev "Cached wanted" } where rewriters' = rewriters S.<> new_rewriters diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs index 6893322f9a..c0f7dc7a49 100644 --- a/compiler/GHC/Tc/Solver/Dict.hs +++ b/compiler/GHC/Tc/Solver/Dict.hs @@ -16,6 +16,7 @@ import GHC.Tc.Types.Constraint import GHC.Tc.Types.Origin import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad +import GHC.Tc.Solver.Types import GHC.Builtin.Names ( coercibleTyConKey, heqTyConKey, eqTyConKey ) @@ -31,6 +32,7 @@ import GHC.Types.SrcLoc import GHC.Types.Var.Env import GHC.Types.Unique( hasKey ) +import GHC.Utils.Monad ( foldlM ) import GHC.Utils.Outputable import GHC.Utils.Panic import GHC.Utils.Misc @@ -69,22 +71,33 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls ; addSolvedDict what ev cls xis ; chooseInstance ev lkup_res } _ -> -- NoInstance or NotSure - -- We didn't solve it; so try functional dependencies with - -- the instance environment - do { doTopFundepImprovement work_item - ; tryLastResortProhibitedSuperclass inerts work_item } } + -- We didn't solve it; so try functional dependencies + tryFunDeps work_item } where dict_loc = ctEvLoc ev - doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w) --- | As a last resort, we TEMPORARILY allow a prohibited superclass solve, +tryFunDeps :: Ct -> TcS (StopOrContinue Ct) +-- Try functional dependencies +-- We do local improvement, then try top level; and we do all this last +-- See Note [Do fundeps last] +tryFunDeps work_item + = do { improved <- doLocalFunDepImprovement work_item + ; if improved then startAgainWith work_item else + + do { improved <- doTopFunDepImprovement work_item + ; if improved then startAgainWith work_item else + + do { inerts <- getTcSInerts + ; tryLastResortProhibitedSuperclass inerts work_item } } } + +tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct) +-- ^ As a last resort, we TEMPORARILY allow a prohibited superclass solve, -- emitting a loud warning when doing so: we might be creating non-terminating -- evidence (as we are in T22912 for example). -- -- See Note [Migrating away from loopy superclass solving] in GHC.Tc.TyCl.Instance. -tryLastResortProhibitedSuperclass :: InertSet -> Ct -> TcS (StopOrContinue Ct) tryLastResortProhibitedSuperclass inerts work_item@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = xis }) | let loc_w = ctEvLoc ev_w @@ -654,7 +667,7 @@ This Note describes a delicate interaction that constrains the orientation of equalities. This one is about fundeps, but the /exact/ same thing arises for type-family injectivity constraints: see Note [Improvement orientation]. -doTopFundepImprovement compares the constraint with all the instance +doTopFunDepImprovement compares the constraint with all the instance declarations, to see if we can produce any equalities. E.g class C2 a b | a -> b instance C Int Bool @@ -668,7 +681,7 @@ There is a nasty corner in #19415 which led to the typechecker looping: work_item: dwrk :: C (T @ka (a::ka)) (T @kb0 (b0::kb0)) Char where kb0, b0 are unification vars - ==> {doTopFundepImprovement: compare work_item with instance, + ==> {doTopFunDepImprovement: compare work_item with instance, generate /fresh/ unification variables kfresh0, yfresh0, emit a new Wanted, and add dwrk to inert set} @@ -694,10 +707,10 @@ We solve the problem by (#21703): carefully orienting the new Wanted so that all the freshly-generated unification variables are on the LHS. - Thus we emit - [W] T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0) + Thus we call unifyWanteds on + T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0) and /NOT/ - [W] T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0) + T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0) Now we'll unify kfresh0:=kb0, yfresh0:=b0, and all is well. The general idea is that we want to preferentially eliminate those freshly-generated @@ -784,6 +797,29 @@ wanteds. This solution was not complete, and caused a failures while trying to solve for transitive functional dependencies (test case: T21703) -- End of Historical note: Failed Alternative Plan (3) -- +Note [Do fundeps last] +~~~~~~~~~~~~~~~~~~~~~~ +Consider T4254b: + class FD a b | a -> b where { op :: a -> b } + + instance FD Int Bool + + foo :: forall a b. (a~Int,FD a b) => a -> Bool + foo = op + +From the ambiguity check on the type signature we get + [G] FD Int b + [W] FD Int beta +Interacting these gives beta:=b; then we start again and solve without +trying fundeps between the new [W] FD Int b and the top-level instance. +If we did, we'd generate [W] b ~ Bool, which fails. + +From the definition `foo = op` we get + [G] FD Int b + [W] FD Int Bool +We solve this from the top level instance before even trying fundeps. +If we did try fundeps, we'd generate [W] b ~ Bool, which fails. + Note [Weird fundeps] ~~~~~~~~~~~~~~~~~~~~ Consider class Het a b | a -> b where @@ -806,17 +842,58 @@ as the fundeps. #7875 is a case in point. -} -doTopFundepImprovement :: Ct -> TcS () +doLocalFunDepImprovement :: Ct -> TcS Bool +-- Add wanted constraints from type-class functional dependencies. +doLocalFunDepImprovement (CDictCan { cc_ev = work_ev, cc_class = cls }) + = do { inerts <- getInertCans + ; foldlM add_fds False (findDictsByClass (inert_dicts inerts) cls) } + where + work_pred = ctEvPred work_ev + work_loc = ctEvLoc work_ev + + add_fds :: Bool -> Ct -> TcS Bool + add_fds so_far inert_ct + | isGiven work_ev && isGiven inert_ev + -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps] + = return so_far + | otherwise + = do { traceTcS "doLocalFunDepImprovement" (vcat + [ ppr work_ev + , pprCtLoc work_loc, ppr (isGivenLoc work_loc) + , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc) + , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) + + ; unifs <- emitFunDepWanteds work_ev $ + improveFromAnother (derived_loc, inert_rewriters) + inert_pred work_pred + ; return (so_far || unifs) + } + where + inert_ev = ctEvidence inert_ct + inert_pred = ctEvPred inert_ev + inert_loc = ctEvLoc inert_ev + inert_rewriters = ctRewriters inert_ct + derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth` + ctl_depth inert_loc + , ctl_origin = FunDepOrigin1 work_pred + (ctLocOrigin work_loc) + (ctLocSpan work_loc) + inert_pred + (ctLocOrigin inert_loc) + (ctLocSpan inert_loc) } + +doLocalFunDepImprovement work_item = pprPanic "doLocalFunDepImprovement" (ppr work_item) + +doTopFunDepImprovement :: Ct -> TcS Bool -- Try to functional-dependency improvement between the constraint -- and the top-level instance declarations -- See Note [Fundeps with instances, and equality orientation] -- See also Note [Weird fundeps] -doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls - , cc_tyargs = xis }) +doTopFunDepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = xis }) = do { traceTcS "try_fundeps" (ppr work_item) ; instEnvs <- getInstEnvs ; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis - ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns } + ; emitFunDepWanteds ev fundep_eqns } where dict_pred = mkClassPred cls xis dict_loc = ctEvLoc ev @@ -830,5 +907,4 @@ doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls inst_pred inst_loc } , emptyRewriterSet ) -doTopFundepImprovement work_item = pprPanic "doTopFundepImprovement" (ppr work_item) - +doTopFunDepImprovement work_item = pprPanic "doTopFunDepImprovement" (ppr work_item) diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs index ed4cd500aa..6bb894b8b4 100644 --- a/compiler/GHC/Tc/Solver/Equality.hs +++ b/compiler/GHC/Tc/Solver/Equality.hs @@ -179,10 +179,10 @@ can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 -- Then, get rid of casts can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2 - | isNothing (canEqLHS_maybe ty2) -- See (3) in Note [Equalities with incompatible kinds] + | isNothing (canEqLHS_maybe ty2) -- See (EIK3) in Note [Equalities with incompatible kinds] = canEqCast rewritten ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2 can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ - | isNothing (canEqLHS_maybe ty1) -- See (3) in Note [Equalities with incompatible kinds] + | isNothing (canEqLHS_maybe ty1) -- See (EIK3) in Note [Equalities with incompatible kinds] = canEqCast rewritten ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1 ---------------------- @@ -253,10 +253,12 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2 -- See also Note [No top-level newtypes on RHS of representational equalities] can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | Just can_eq_lhs1 <- canEqLHS_maybe ty1 - = canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2 + = do { traceTcS "can_eq1" (ppr ty1 $$ ppr ty2) + ; canEqCanLHS ev eq_rel NotSwapped can_eq_lhs1 ps_ty1 ty2 ps_ty2 } | Just can_eq_lhs2 <- canEqLHS_maybe ty2 - = canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1 + = do { traceTcS "can_eq2" (ppr ty1 $$ ppr ty2) + ; canEqCanLHS ev eq_rel IsSwapped can_eq_lhs2 ps_ty2 ty1 ps_ty1 } -- If the type is TyConApp tc1 args1, then args1 really can't be less -- than tyConArity tc1. It could be *more* than tyConArity, but then we @@ -651,13 +653,18 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2 -- to an irreducible constraint; see typecheck/should_compile/T10494 -- See Note [Decomposing AppTy equalities] can_eq_app ev s1 t1 s2 t2 - | CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev - = do { co_s <- unifyWanted rewriters loc Nominal s1 s2 - ; let arg_loc - | isNextArgVisible s1 = loc - | otherwise = updateCtLocOrigin loc toInvisibleOrigin - ; co_t <- unifyWanted rewriters arg_loc Nominal t1 t2 - ; let co = mkAppCo co_s co_t + | CtWanted { ctev_dest = dest } <- ev + = do { traceTcS "can_eq_app" (vcat [ text "s1:" <+> ppr s1, text "t1:" <+> ppr t1 + , text "s2:" <+> ppr s2, text "t2:" <+> ppr t2 + , text "vis:" <+> ppr (isNextArgVisible s1) ]) + ; (co,_,_) <- wrapUnifierTcS ev Nominal $ \uenv -> + -- Unify arguments t1/t2 before function s1/s2, because + -- the former have smaller kinds, and hence simpler error messages + -- c.f. GHC.Tc.Utils.Unify.uType (go_app) + do { let arg_env = updUEnvLoc uenv (adjustCtLoc (isNextArgVisible s1) False) + ; co_t <- uType arg_env t1 t2 + ; co_s <- uType uenv s1 s2 + ; return (mkAppCo co_s co_t) } ; setWantedEq dest co ; stopWith ev "Decomposed [W] AppTy" } @@ -717,7 +724,6 @@ canTyConApp :: CtEvidence -> EqRel -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) -- See Note [Decomposing TyConApp equalities] --- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities] -- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family -- But they can be data families. canTyConApp ev eq_rel tc1 tys1 tc2 tys2 @@ -804,8 +810,8 @@ then we will just decompose s1~s2, and it might be better to do so on the spot. An important special case is where s1=s2, and we get just Refl. -So canDecomposableTyConAppOK uses unifyWanted etc to short-cut that work. -See also Note [Decomposing Dependent TyCons and Processing Wanted Equalities] +So canDecomposableTyConAppOK uses wrapUnifierTcS etc to short-cut +that work. See also Note [Work-list ordering]. Note [Decomposing TyConApp equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -908,6 +914,36 @@ that is for isInjectiveTyCon to be true: This is implemented in `can_decompose` in `canTyConApp`; it looks at injectivity, just as specified above. +Note [Work-list ordering] +~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider decomposing a TyCon equality + + (0) [W] T k_fresh (t1::k_fresh) ~ T k1 (t2::k1) + +This gives rise to 2 equalities in the solver worklist + + (1) [W] k_fresh ~ k1 + (2) [W] t1::k_fresh ~ t2::k1 + +We would like to solve (1) before looking at (2), so that we don't end +up in the complexities of canEqLHSHetero. To do this: + +* `canDecomposableTyConAppOK` calls `uType` on the arguments + /left-to-right/. See the call to zipWith4M in that function. + +* `uType` keeps the bag of emitted constraints in the same + left-to-right order. See the use of `snocBag` in `uType_defer`. + +* `wrapUnifierTcS` adds the bag of deferred constraints from + `do_unifications` to the work-list using `extendWorkListEqs`. + +* `extendWorkListEqs` and `selectWorkItem` together arrange that the + list of constraints given to `extendWorkListEqs` is processed in + left-to-right order. + +This is not a very big deal. It reduces the number of solver steps +in the test RaeJobTalk from 1830 to 1815, a 1% reduction. But still, +it doesn't cost anything either. Note [Decomposing type family applications] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1174,25 +1210,24 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 do { traceTcS "canDecomposableTyConAppOK" (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2) ; case ev of - CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } - -- new_locs and tc_roles are both infinite, so - -- we are guaranteed that cos has the same lengthm - -- as tys1 and tys2 - -- See Note [Fast path when decomposing TyConApps] - -- Caution: unifyWanteds is order sensitive - -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities] - -> do { cos <- unifyWanteds rewriters new_locs tc_roles tys1 tys2 - ; setWantedEq dest (mkTyConAppCo role tc cos) } + CtWanted { ctev_dest = dest } + -- new_locs and tc_roles are both infinite, so we are + -- guaranteed that cos has the same length as tys1 and tys2 + -- See Note [Fast path when decomposing TyConApps] + -> do { (co, _, _) <- wrapUnifierTcS ev role $ \uenv -> + do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2 + -- zipWith4M: see Note [Work-list ordering] + -- in GHC.Tc.Solved.Equality + ; return (mkTyConAppCo role tc cos) } + ; setWantedEq dest co } CtGiven { ctev_evar = evar } - -> do { let ev_co = mkCoVarCo evar - ; given_evs <- newGivenEvVars loc $ - [ ( mkPrimEqPredRole r ty1 ty2 - , evCoercion $ mkSelCo (SelTyCon i r) ev_co ) - | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] - , r /= Phantom - , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] - ; emitWorkNC given_evs } + | let ev_co = mkCoVarCo evar + -> emitNewGivens loc + [ (r, ty1, ty2, mkSelCo (SelTyCon i r) ev_co) + | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] + , r /= Phantom + , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] ; stopWith ev "Decomposed TyConApp" } @@ -1200,6 +1235,11 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 loc = ctEvLoc ev role = eqRelRole eq_rel + u_arg uenv arg_loc arg_role = uType arg_env + where + arg_env = uenv `setUEnvRole` arg_role + `updUEnvLoc` const arg_loc + -- Infinite, to allow for over-saturated TyConApps tc_roles = tyConRoleListX role tc @@ -1213,14 +1253,8 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 -- do either of these changes. (Forgetting to do so led to #16188) -- -- NB: infinite in length - new_locs = [ new_loc - | bndr <- tyConBinders tc - , let new_loc0 | isNamedTyConBinder bndr = toKindLoc loc - | otherwise = loc - new_loc | isInvisibleTyConBinder bndr - = updateCtLocOrigin new_loc0 toInvisibleOrigin - | otherwise - = new_loc0 ] + new_locs = [ adjustCtLocTyConBinder bndr loc + | bndr <- tyConBinders tc ] ++ repeat loc canDecomposableFunTy :: CtEvidence -> EqRel -> FunTyFlag @@ -1231,29 +1265,29 @@ canDecomposableFunTy ev eq_rel af f1@(m1,a1,r1) f2@(m2,a2,r2) = do { traceTcS "canDecomposableFunTy" (ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2) ; case ev of - CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } - -> do { mult <- unifyWanted rewriters mult_loc (funRole role SelMult) m1 m2 - ; arg <- unifyWanted rewriters loc (funRole role SelArg) a1 a2 - ; res <- unifyWanted rewriters loc (funRole role SelRes) r1 r2 - ; setWantedEq dest (mkNakedFunCo1 role af mult arg res) } + CtWanted { ctev_dest = dest } + -> do { (co, _, _) <- wrapUnifierTcS ev Nominal $ \ uenv -> + do { let mult_env = uenv `updUEnvLoc` toInvisibleLoc + `setUEnvRole` funRole role SelMult + ; mult <- uType mult_env m1 m2 + ; arg <- uType (uenv `setUEnvRole` funRole role SelArg) a1 a2 + ; res <- uType (uenv `setUEnvRole` funRole role SelRes) r1 r2 + ; return (mkNakedFunCo role af mult arg res) } + ; setWantedEq dest co } CtGiven { ctev_evar = evar } - -> do { let ev_co = mkCoVarCo evar - ; given_evs <- newGivenEvVars loc $ - [ ( mkPrimEqPredRole role' ty1 ty2 - , evCoercion $ mkSelCo (SelFun fs) ev_co ) - | (fs, ty1, ty2) <- [(SelMult, m1, m2) - ,(SelArg, a1, a2) - ,(SelRes, r1, r2)] - , let role' = funRole role fs ] - ; emitWorkNC given_evs } + | let ev_co = mkCoVarCo evar + -> emitNewGivens loc + [ (funRole role fs, ty1, ty2, mkSelCo (SelFun fs) ev_co) + | (fs, ty1, ty2) <- [ (SelMult, m1, m2) + , (SelArg, a1, a2) + , (SelRes, r1, r2)] ] ; stopWith ev "Decomposed TyConApp" } where - loc = ctEvLoc ev - role = eqRelRole eq_rel - mult_loc = updateCtLocOrigin loc toInvisibleOrigin + loc = ctEvLoc ev + role = eqRelRole eq_rel -- | Call when canonicalizing an equality fails, but if the equality is -- representational, there is some hope for the future. @@ -1408,7 +1442,7 @@ canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 = canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 | otherwise - = canEqCanLHSHetero ev eq_rel swapped lhs1 k1 xi2 k2 + = canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 k1 xi2 ps_xi2 k2 where k1 = canEqLHSKind lhs1 @@ -1444,64 +1478,75 @@ But this sent solver in an infinite loop (see #19415). -} canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2) + -- (or reversed if SwapFlag=IsSwapped) -> EqRel -> SwapFlag - -> CanEqLHS -- xi1 + -> CanEqLHS -> TcType -- xi1 -> TcKind -- ki1 - -> TcType -- xi2 + -> TcType -> TcType -- xi2 -> TcKind -- ki2 -> TcS (StopOrContinue Ct) -canEqCanLHSHetero ev eq_rel swapped lhs1 ki1 xi2 ki2 - -- See Note [Equalities with incompatible kinds] - -- See Note [Kind Equality Orientation] - -- NB: preserve left-to-right orientation!! - -- See Note [Fundeps with instances, and equality orientation] - -- wrinkle (W2) in GHC.Tc.Solver.Interact - = do { (kind_ev, kind_co) <- mk_kind_eq -- :: ki1 ~N ki2 - - ; let -- kind_co :: (ki1 :: *) ~N (ki2 :: *) (whether swapped or not) - lhs_redn = mkReflRedn role xi1 - rhs_redn = mkGReflRightRedn role xi2 (mkSymCo kind_co) - - -- See Note [Equalities with incompatible kinds], Wrinkle (1) - -- This will be ignored in rewriteEqEvidence if the work item is a Given - rewriters = rewriterSetFromCo kind_co +canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2 +-- See Note [Equalities with incompatible kinds] +-- See Note [Kind Equality Orientation] + +-- NB: preserve left-to-right orientation!! See wrinkle (W2) in +-- Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Interact +-- NotSwapped: +-- ev :: (lhs1:ki1) ~r# (xi2:ki2) +-- kind_co :: k11 ~# ki2 -- Same orientiation as ev +-- type_ev :: lhs1 ~r# (xi2 |> sym kind_co) +-- Swapped +-- ev :: (xi2:ki2) ~r# (lhs1:ki1) +-- kind_co :: ki2 ~# ki1 -- Same orientiation as ev +-- type_ev :: (xi2 |> kind_co) ~r# lhs1 + + = do { (kind_co, rewriters, unifs_happened) <- mk_kind_eq -- :: ki1 ~N ki2 + ; if unifs_happened + -- Unifications happened, so start again to do the zonking + -- Otherwise we might put something in the inert set that isn't inert + then startAgainWith (mkNonCanonical ev) + else + do { let lhs_redn = mkReflRedn role ps_xi1 + rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co + mb_sym_kind_co = case swapped of + NotSwapped -> mkSymCo kind_co + IsSwapped -> kind_co ; traceTcS "Hetero equality gives rise to kind equality" - (ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) + (ppr swapped $$ + ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ]) ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn - ; emitWorkNC [type_ev] -- delay the type equality until after we've finished - -- the kind equality, which may unlock things - -- See Note [Equalities with incompatible kinds] + ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co + ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }} - ; solveNonCanonicalEquality kind_ev NomEq ki1 ki2 } where - mk_kind_eq :: TcS (CtEvidence, CoercionN) + mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool) + -- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped + -- Returned Bool = True if unifications happened, so we should retry mk_kind_eq = case ev of CtGiven { ctev_evar = evar } - -> do { let kind_co = maybe_sym $ mkKindCo (mkCoVarCo evar) -- :: k1 ~ k2 - ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co) - ; return (kind_ev, ctEvCoercion kind_ev) } - - CtWanted { ctev_rewriters = rewriters } - -> newWantedEq kind_loc rewriters Nominal ki1 ki2 - - xi1 = canEqLHSType lhs1 - loc = ctev_loc ev - role = eqRelRole eq_rel - kind_loc = mkKindLoc xi1 xi2 loc - kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2 - - maybe_sym = case swapped of - IsSwapped -> mkSymCo -- if the input is swapped, then we - -- will have k2 ~ k1, so flip it to k1 ~ k2 - NotSwapped -> id + -> do { let kind_co = mkKindCo (mkCoVarCo evar) + pred_ty = unSwap swapped (mkNomPrimEqPred liftedTypeKind) ki1 ki2 + kind_loc = mkKindEqLoc xi1 xi2 (ctev_loc ev) + ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co) + ; emitWorkNC [kind_ev] + ; return (ctEvCoercion kind_ev, emptyRewriterSet, False) } + + CtWanted {} + -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv -> + let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2) + in unSwap swapped (uType uenv') ki1 ki2 + ; return (kind_co, rewriterSetFromCts cts, not (null unifs)) } + + xi1 = canEqLHSType lhs1 + role = eqRelRole eq_rel -canEqCanLHSHomo :: CtEvidence +canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs + -- or, if swapped: rhs ~ lhs -> EqRel -> SwapFlag - -> CanEqLHS -- lhs (or, if swapped, rhs) - -> TcType -- pretty lhs - -> TcType -> TcType -- rhs, pretty rhs + -> CanEqLHS -> TcType -- lhs, pretty lhs + -> TcType -> TcType -- rhs, pretty rhs -> TcS (StopOrContinue Ct) -- Guaranteed that typeKind lhs == typeKind rhs canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2 @@ -1557,46 +1602,13 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco -- See Note [Decomposing type family applications] = do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2) - -- emit wanted equalities for injective type families - ; let inj_eqns :: [TypeEqn] -- TypeEqn = Pair Type - inj_eqns - | ReprEq <- eq_rel = [] -- injectivity applies only for nom. eqs. - | fun_tc1 /= fun_tc2 = [] -- if the families don't match, stop. - - | Injective inj <- tyConInjectivityInfo fun_tc1 - = [ Pair arg1 arg2 - | (arg1, arg2, True) <- zip3 fun_args1 fun_args2 inj ] - - -- built-in synonym families don't have an entry point - -- for this use case. So, we just use sfInteractInert - -- and pass two equal RHSs. We *could* add another entry - -- point, but then there would be a burden to make - -- sure the new entry point and existing ones were - -- internally consistent. This is slightly distasteful, - -- but it works well in practice and localises the - -- problem. - | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1 - = let ki1 = canEqLHSKind lhs1 - ki2 | MRefl <- mco - = ki1 -- just a small optimisation - | otherwise - = canEqLHSKind lhs2 - - fake_rhs1 = anyTypeOfKind ki1 - fake_rhs2 = anyTypeOfKind ki2 - in - sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2 - - | otherwise -- ordinary, non-injective type family - = [] - - ; case ev of - CtWanted { ctev_rewriters = rewriters } -> - mapM_ (\ (Pair t1 t2) -> unifyWanted rewriters (ctEvLoc ev) Nominal t1 t2) inj_eqns - CtGiven {} -> return () - -- See Note [No Given/Given fundeps] in GHC.Tc.Solver.Interact - - ; tclvl <- getTcLevel + ; unifications_done <- tryFamFamInjectivity ev eq_rel + fun_tc1 fun_args1 fun_tc2 fun_args2 mco + ; if unifications_done + then -- Go round again, since the unifications affect lhs/rhs + startAgainWith (mkNonCanonical ev) + else + do { tclvl <- getTcLevel ; let tvs1 = tyCoVarsOfTypes fun_args1 tvs2 = tyCoVarsOfTypes fun_args2 @@ -1611,7 +1623,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco ; if swap_for_rewriting || swap_for_size then finish_with_swapping - else finish_without_swapping } + else finish_without_swapping } } where sym_mco = mkSymMCo mco role = eqRelRole eq_rel @@ -1762,11 +1774,11 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs | otherwise -> tryIrredInstead reason ev eq_rel swapped lhs rhs ; - PuOK rhs_redn _ -> + PuOK _ rhs_redn -> -- Success: we can solve by unification do { -- In the common case where rhs_redn is Refl, we don't need to rewrite - -- the evidence even if swapped=IsSwapped. Suppose the original was + -- the evidence, even if swapped=IsSwapped. Suppose the original was -- [W] co : Int ~ alpha -- We unify alpha := Int, and set co := <Int>. No need to -- swap to co = sym co' @@ -1778,7 +1790,6 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs ; let tv_ty = mkTyVarTy tv final_rhs = reductionReducedType rhs_redn - tv_lvl = tcTyVarLevel tv ; traceTcS "Sneaky unification:" $ vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr final_rhs, @@ -1794,14 +1805,8 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs ; setEvBindIfWanted new_ev IsCoherent $ evCoercion (mkNomReflCo final_rhs) - -- Set the unification flag if we have done outer unifications - -- that might affect an earlier implication constraint - ; ambient_lvl <- getTcLevel - ; when (ambient_lvl `strictlyDeeperThan` tv_lvl) $ - setUnificationFlag tv_lvl - -- Kick out any constraints that can now be rewritten - ; n_kicked <- kickOutAfterUnification tv + ; n_kicked <- kickOutAfterUnification [tv] ; return (Stop new_ev (text "Solved by unification" <+> pprKicked n_kicked)) }}}} @@ -1816,12 +1821,9 @@ canEqCanLHSFinish_try_unification ev eq_rel swapped lhs rhs -- and hence we /can/ use it for rewriting -- Concrete-ness: alpha[conc] ~ b[sk] -- We can use it to rewrite; we still have to solve the original - -- Coercion holes: see wrinkle (2) of - -- Note [Equalities with incompatible kinds] do_not_prevent_rewriting :: CheckTyEqResult do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<> - cteProblem cteConcrete S.<> - cteProblem cteCoercionHole + cteProblem cteConcrete --------------------------- -- Unification is off the table @@ -1848,7 +1850,7 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs -> tryIrredInstead reason ev eq_rel swapped lhs rhs - PuOK rhs_redn _ + PuOK _ rhs_redn -> do { new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped (mkReflRedn (eqRelRole eq_rel) lhs_ty) rhs_redn @@ -1921,42 +1923,59 @@ k2 and use this to cast. To wit, from [X] co :: k1 ~ k2 [X] (tv :: k1) ~ ((rhs |> sym co) :: k1) -We carry on with the *kind equality*, not the type equality, because -solving the former may unlock the latter. This choice is made in -canEqCanLHSHetero. It is important: otherwise, T13135 loops. - Wrinkles: - (1) When X is W, the new type-level wanted is effectively rewritten by the +(EIK1) When X is W, the new type-level wanted is effectively rewritten by the kind-level one. We thus include the kind-level wanted in the RewriterSet for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. This is done in canEqCanLHSHetero. - (2) If we have [W] w :: alpha ~ (rhs |> sym co_hole), should we unify alpha? No. - The problem is that the wanted w is effectively rewritten by another wanted, - and unifying alpha effectively promotes this wanted to a given. Doing so - means we lose track of the rewriter set associated with the wanted. - - Another way to say it: we must not have a co_hole in a Given, and - unification effectively makes a Given. (This is not very well motivated; - may need to dig deeper if anything goes wrong.) - - On the other hand, w is perfectly suitable for rewriting, because of the - way we carefully track rewriter sets. So we include cteCoercionHole in - `do_not_prevent_rewriting` in `canEqCanLHSFinish_try_unification`. (Side - note: I think this is an open choice. Maybe we'd get better error - messages if we did not use these equalities for rewriting.) - - We thus allow w to be a CEqCan, but we prevent unification. See - Note [Unification preconditions] in GHC.Tc.Utils.Unify. - - The only tricky part is that we must later indeed unify if/when the kind-level - wanted gets solved. This is done in kickOutAfterFillingCoercionHole, - which kicks out all equalities whose RHS mentions the filled-in coercion hole. - Note that it looks for type family equalities, too, because of the use of - unifyTest in canEqTyVarFunEq. - - (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the +(EIK2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce + [W] w : a ~ (b |> kw) + [W] kw : Type ~ (Type->Type) + + But we do /not/ want to regard `w` as canonical, and use it for rewriting + other constraints: `kw` is insoluble, and replacing something of kind + `Type` with something of kind `Type->Type` (even wrapped in an insouluble + cast) does not help, and doing so turns out to lead to much worse error + messages. (In particular, if 'a' is a unification variable, we might + unify, losing the tracking info that it depends on solving `kw`.) + + Conclusion: if a RHS contains a corecion hole arising from fixing a hetero-kinded + equality, treat the equality (`w` in this case) as non-canonical, so that + * It will not be used for unification + * It will not be used for rewriting + Instead, it lands in the inert_irreds in the inert set, awaiting solution of + that `kw`. + + (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets + solved. This is done in kickOutAfterFillingCoercionHole, which kicks out + all equalities whose RHS mentions the filled-in coercion hole. Note that + it looks for type family equalities, too, because of the use of unifyTest + in canEqTyVarFunEq. + + (EIK2b) What if the RHS mentions /other/ coercion holes? How can that happen? The + main way is like this. Assume F :: forall k. k -> Type + [W] kw : k ~ Type + [W] w : a ~ F k t + We can rewrite `w` with `kw` like this: + [W] w' : a ~ F Type (t |> kw) + The cast on the second argument of `F` is necessary to keep the appliation well-kinded. + There is nothing special here; no reason not treat w' as canonical, and use it for + rewriting. Indeed tests JuanLopez only typechecks if we do. So we'd like to treat + this kind of equality as canonical. + + Hence the ch_hetero_kind field in CoercionHole: it is True of constraints + created by `canEqCanLHSHetero` to fix up hetero-kinded equalities; and False otherwise: + + * An equality constraint is non-canonical if it mentions a hetero-kind + CoercionHole on the RHS. See the `hasCoercionHoleCo` test in GHC.Tc.Utils.checkCo. + + * Hetero-kind CoercionHoles are created when the parent's CtOrigin is + KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole and friends. We + set this origin, via `mkKindLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`. + +(EIK3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the algorithm detailed here, producing [W] co :: k1 ~ k2, and adding [W] (a :: k1) ~ ((rhs |> sym co) :: k1) to the irreducibles. Some time later, we solve co, and fill in co's coercion hole. This kicks out @@ -2146,7 +2165,7 @@ in `GHC.Tc.Solver.Monad.checkTouchableTyVarEq`. Why TauTvs? See [Why TauTvs] below. Critically, we emit the two new constraints (the last two above) -directly instead of calling unifyWanted. (Otherwise, we'd end up +directly instead of calling wrapUnifierTcS. (Otherwise, we'd end up unifying cbv1 and cbv2 immediately, achieving nothing.) Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This unification happens immediately following a successful call to @@ -2400,12 +2419,9 @@ rewriteEqEvidence new_rewriters old_ev swapped (Reduction lhs_co nlhs) (Reductio | CtWanted { ctev_dest = dest , ctev_rewriters = rewriters } <- old_ev , let rewriters' = rewriters S.<> new_rewriters - = do { (new_ev, hole_co) <- newWantedEq loc rewriters' - (ctEvRole old_ev) nlhs nrhs + = do { (new_ev, hole_co) <- newWantedEq loc rewriters' (ctEvRole old_ev) nlhs nrhs ; let co = maybeSymCo swapped $ - lhs_co - `mkTransCo` hole_co - `mkTransCo` mkSymCo rhs_co + lhs_co `mkTransCo` hole_co `mkTransCo` mkSymCo rhs_co ; setWantedEq dest co ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev , ppr nlhs @@ -2480,9 +2496,11 @@ interactEq work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) | otherwise -> case lhs of TyVarLHS {} -> finishEqCt work_item - TyFamLHS tc args -> do { improveLocalFunEqs inerts tc args work_item - ; improveTopFunEqs tc args work_item - ; finishEqCt work_item } } + TyFamLHS tc args -> do { imp1 <- improveLocalFunEqs inerts tc args work_item + ; imp2 <- improveTopFunEqs tc args work_item + ; if (imp1 || imp2) + then startAgainWith (mkNonCanonical ev) + else finishEqCt work_item } } inertsCanDischarge :: InertCans -> EqCt @@ -2746,7 +2764,7 @@ Of course, if we solve the first wanted first, the second becomes homogeneous. When looking for injectivity-inspired equalities, we work left-to-right, producing the two equalities in the order written above. However, these -equalities are then passed into unifyWanted, which will fail, adding these +equalities are then passed into wrapUnifierTcS, which will fail, adding these to the work list. However, crucially, the work list operates like a *stack*. So, because we add w1 and then w2, we process w2 first. This is silly: solving w1 would unlock w2. So we make sure to add equalities to the work @@ -2758,9 +2776,9 @@ like the right thing to do. When this was originally conceived, it was necessary to avoid a loop in T13135. That loop is now avoided by continuing with the kind equality (not the type -equality) in canEqCanLHSHetero (see Note [Equalities with incompatible kinds] -in GHC.Tc.Solver.Canonical). However, the idea of working left-to-right still -seems worthwhile, and so the calls to 'reverse' remain. +equality) in canEqCanLHSHetero (see Note [Equalities with incompatible kinds]). +However, the idea of working left-to-right still seems worthwhile, and so the calls +to 'reverse' remain. Note [Improvement orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2804,28 +2822,72 @@ equality with the template on the left. Delicate, but it works. -} +tryFamFamInjectivity :: CtEvidence -> EqRel + -> TyCon -> [TcType] -> TyCon -> [TcType] -> MCoercion + -> TcS Bool -- True <=> some unification happened +tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco + | ReprEq <- eq_rel + = return False -- Injectivity applies only for Nominal equalities + | fun_tc1 /= fun_tc2 + = return False -- If the families don't match, stop. + | isGiven ev + = return False -- See Note [No Given/Given fundeps] in GHC.Tc.Solver.Interact + + -- So this is a [W] (F tys1 ~N# F tys2) + + -- Is F an injective type family + | Injective inj <- tyConInjectivityInfo fun_tc1 + = unifyFunDeps ev Nominal $ \uenv -> + uPairsTcM uenv [ Pair ty1 ty2 + | (ty1,ty2,True) <- zip3 fun_args1 fun_args2 inj ] + + -- Built-in synonym families don't have an entry point for this + -- use case. So, we just use sfInteractInert and pass two equal + -- RHSs. We *could* add another entry point, but then there would + -- be a burden to make sure the new entry point and existing ones + -- were internally consistent. This is slightly distasteful, but + -- it works well in practice and localises the problem. Ugh. + | Just ops <- isBuiltInSynFamTyCon_maybe fun_tc1 + = let tc_kind = tyConKind fun_tc1 + ki1 = piResultTys tc_kind fun_args1 + ki2 | MRefl <- mco + = ki1 -- just a small optimisation + | otherwise + = piResultTys tc_kind fun_args2 + + fake_rhs1 = anyTypeOfKind ki1 + fake_rhs2 = anyTypeOfKind ki2 + + eqs :: [TypeEqn] + eqs = sfInteractInert ops fun_args1 fake_rhs1 fun_args2 fake_rhs2 + in + unifyFunDeps ev Nominal $ \uenv -> + uPairsTcM uenv eqs + + | otherwise -- ordinary, non-injective type family + = return False + -------------------- -improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS () +improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool -- See Note [FunDep and implicit parameter reactions] improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs }) - - | isGiven ev = return () -- See Note [No Given/Given fundeps] + | isGiven ev + = return False -- See Note [No Given/Given fundeps] | otherwise = do { fam_envs <- getFamInstEnvs ; eqns <- improve_top_fun_eqs fam_envs fam_tc args rhs ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr rhs - , ppr eqns ]) - ; mapM_ (\(Pair ty1 ty2) -> unifyWanted rewriters loc Nominal ty1 ty2) - (reverse eqns) } + , ppr eqns ]) + ; unifyFunDeps ev Nominal $ \uenv -> + uPairsTcM (bump_depth uenv) (reverse eqns) } -- Missing that `reverse` causes T13135 and T13135_simple to loop. -- See Note [Reverse order of fundep equations] where - loc = bumpCtLocDepth (ctEvLoc ev) + bump_depth env = env { u_loc = bumpCtLocDepth (u_loc env) } -- ToDo: this location is wrong; it should be FunDepOrigin2 -- See #14778 - rewriters = ctEvRewriters ev improve_top_fun_eqs :: FamInstEnvs -> TyCon -> [TcType] -> TcType @@ -2903,19 +2965,21 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] } -improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS () +improveLocalFunEqs :: InertCans -> TyCon -> [TcType] -> EqCt -> TcS Bool -- Generate improvement equalities, by comparing -- the current work item with inert CFunEqs -- E.g. x + y ~ z, x + y' ~ z => [W] y ~ y' -- -- See Note [FunDep and implicit parameter reactions] improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs }) - = unless (null improvement_eqns) $ - do { traceTcS "interactFunEq improvements: " $ + | null improvement_eqns + = return False + | otherwise + = do { traceTcS "interactFunEq improvements: " $ vcat [ text "Eqns:" <+> ppr improvement_eqns , text "Candidates:" <+> ppr funeqs_for_tc , text "Inert eqs:" <+> ppr (inert_eqs inerts) ] - ; emitFunDepWanteds (ctEvRewriters work_ev) improvement_eqns } + ; emitFunDepWanteds work_ev improvement_eqns } where funeqs = inert_funeqs inerts funeqs_for_tc :: [EqCt] diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs index ab5ee70ac1..ab3f8c9638 100644 --- a/compiler/GHC/Tc/Solver/InertSet.hs +++ b/compiler/GHC/Tc/Solver/InertSet.hs @@ -8,7 +8,8 @@ module GHC.Tc.Solver.InertSet ( -- * The work list WorkList(..), isEmptyWorkList, emptyWorkList, extendWorkListNonEq, extendWorkListCt, - extendWorkListCts, extendWorkListEq, + extendWorkListCts, extendWorkListCtList, + extendWorkListEq, extendWorkListEqs, appendWorkList, extendWorkListImplic, workListSize, selectWorkItem, @@ -31,7 +32,7 @@ module GHC.Tc.Solver.InertSet ( foldFunEqs, -- * Kick-out - kickOutRewritableLHS, + KickOutSpec(..), kickOutRewritableLHS, -- * Cycle breaker vars CycleBreakerVarStack, @@ -50,6 +51,7 @@ import GHC.Tc.Utils.TcType import GHC.Types.Var import GHC.Types.Var.Env +import GHC.Types.Var.Set import GHC.Core.Reduction import GHC.Core.Predicate @@ -60,6 +62,7 @@ import GHC.Core.TyCon import GHC.Core.Unify import GHC.Data.Bag + import GHC.Utils.Misc ( partitionWith ) import GHC.Utils.Outputable import GHC.Utils.Panic @@ -93,7 +96,7 @@ As a simple form of priority queue, our worklist separates out Note [Prioritise equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -It's very important to process equalities /first/: +It's very important to process equalities over class constraints: * (Efficiency) The general reason to do so is that if we process a class constraint first, we may end up putting it into the inert set @@ -111,14 +114,17 @@ It's very important to process equalities /first/: Solution: prioritise equalities over class constraints * (Class equalities) We need to prioritise equalities even if they - are hidden inside a class constraint; - see Note [Prioritise class equalities] + are hidden inside a class constraint; see Note [Prioritise class equalities] * (Kick-out) We want to apply this priority scheme to kicked-out - constraints too (see the call to extendWorkListCt in kick_out_rewritable + constraints too (see the call to extendWorkListCt in kick_out_rewritable) E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become homo-kinded when kicked out, and hence we want to prioritise it. +Among the equalities we prioritise ones with an empty rewriter set; +see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint, wrinkle (W1). + + Note [Prioritise class equalities] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We prioritise equalities in the solver (see selectWorkItem). But class @@ -157,6 +163,13 @@ data WorkList -- See Note [Prioritise equalities] -- See Note [Prioritise class equalities] + , wl_rw_eqs :: [Ct] -- Like wl_eqs, but ones that have a non-empty + -- rewriter set; or, more precisely, did when + -- added to the WorkList + -- We prioritise wl_eqs over wl_rw_eqs; + -- see Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint for more details. + , wl_rest :: [Ct] , wl_implics :: Bag Implication -- See Note [Residual implications] @@ -164,20 +177,41 @@ data WorkList appendWorkList :: WorkList -> WorkList -> WorkList appendWorkList - (WL { wl_eqs = eqs1, wl_rest = rest1 - , wl_implics = implics1 }) - (WL { wl_eqs = eqs2, wl_rest = rest2 - , wl_implics = implics2 }) + (WL { wl_eqs = eqs1, wl_rw_eqs = rw_eqs1 + , wl_rest = rest1, wl_implics = implics1 }) + (WL { wl_eqs = eqs2, wl_rw_eqs = rw_eqs2 + , wl_rest = rest2, wl_implics = implics2 }) = WL { wl_eqs = eqs1 ++ eqs2 + , wl_rw_eqs = rw_eqs1 ++ rw_eqs2 , wl_rest = rest1 ++ rest2 , wl_implics = implics1 `unionBags` implics2 } workListSize :: WorkList -> Int -workListSize (WL { wl_eqs = eqs, wl_rest = rest }) - = length eqs + length rest - -extendWorkListEq :: Ct -> WorkList -> WorkList -extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl } +workListSize (WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest }) + = length eqs + length rw_eqs + length rest + +extendWorkListEq :: RewriterSet -> Ct -> WorkList -> WorkList +extendWorkListEq rewriters ct wl + | isEmptyRewriterSet rewriters -- A wanted that has not been rewritten + -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint + = wl { wl_eqs = ct : wl_eqs wl } + | otherwise + = wl { wl_rw_eqs = ct : wl_rw_eqs wl } + +extendWorkListEqs :: RewriterSet -> Bag Ct -> WorkList -> WorkList +-- Add [eq1,...,eqn] to the work-list +-- They all have the same rewriter set +-- The constraints will be solved in left-to-right order: +-- see Note [Work-list ordering] in GHC.Tc.Solved.Equality +extendWorkListEqs rewriters eqs wl + | isEmptyRewriterSet rewriters + -- isEmptyRewriterSet: see Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint + = wl { wl_eqs = foldr (:) (wl_eqs wl) eqs } + -- The foldr just appends wl_eqs to the bag of eqs + | otherwise + = wl { wl_rw_eqs = foldr (:) (wl_rw_eqs wl) eqs } extendWorkListNonEq :: Ct -> WorkList -> WorkList -- Extension by non equality @@ -187,20 +221,25 @@ extendWorkListImplic :: Implication -> WorkList -> WorkList extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl } extendWorkListCt :: Ct -> WorkList -> WorkList --- Agnostic +-- Agnostic about what kind of constraint extendWorkListCt ct wl - = case classifyPredType (ctPred ct) of + = case classifyPredType (ctEvPred ev) of EqPred {} - -> extendWorkListEq ct wl + -> extendWorkListEq rewriters ct wl ClassPred cls _ -- See Note [Prioritise class equalities] | isEqPredClass cls - -> extendWorkListEq ct wl + -> extendWorkListEq rewriters ct wl _ -> extendWorkListNonEq ct wl + where + ev = ctEvidence ct + rewriters = ctEvRewriters ev -extendWorkListCts :: [Ct] -> WorkList -> WorkList --- Agnostic +extendWorkListCtList :: [Ct] -> WorkList -> WorkList +extendWorkListCtList cts wl = foldr extendWorkListCt wl cts + +extendWorkListCts :: Cts -> WorkList -> WorkList extendWorkListCts cts wl = foldr extendWorkListCt wl cts isEmptyWorkList :: WorkList -> Bool @@ -208,21 +247,24 @@ isEmptyWorkList (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics }) = null eqs && null rest && isEmptyBag implics emptyWorkList :: WorkList -emptyWorkList = WL { wl_eqs = [], wl_rest = [], wl_implics = emptyBag } +emptyWorkList = WL { wl_eqs = [], wl_rw_eqs = [], wl_rest = [], wl_implics = emptyBag } selectWorkItem :: WorkList -> Maybe (Ct, WorkList) -- See Note [Prioritise equalities] -selectWorkItem wl@(WL { wl_eqs = eqs, wl_rest = rest }) - | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts }) - | ct:cts <- rest = Just (ct, wl { wl_rest = cts }) - | otherwise = Nothing +selectWorkItem wl@(WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest }) + | ct:cts <- eqs = Just (ct, wl { wl_eqs = cts }) + | ct:cts <- rw_eqs = Just (ct, wl { wl_rw_eqs = cts }) + | ct:cts <- rest = Just (ct, wl { wl_rest = cts }) + | otherwise = Nothing -- Pretty printing instance Outputable WorkList where - ppr (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics }) + ppr (WL { wl_eqs = eqs, wl_rw_eqs = rw_eqs, wl_rest = rest, wl_implics = implics }) = text "WL" <+> (braces $ vcat [ ppUnless (null eqs) $ text "Eqs =" <+> vcat (map ppr eqs) + , ppUnless (null rw_eqs) $ + text "RwEqs =" <+> vcat (map ppr rw_eqs) , ppUnless (null rest) $ text "Non-eqs =" <+> vcat (map ppr rest) , ppUnless (isEmptyBag implics) $ @@ -1298,13 +1340,27 @@ updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl }) not_equality (CDictCan {}) = True not_equality _ = False -kickOutRewritableLHS :: CtFlavourRole -- Flavour/role of the equality that - -- is being added to the inert set - -> CanEqLHS -- The new equality is lhs ~ ty - -> InertCans - -> (WorkList, InertCans) +data KickOutSpec -- See Note [KickOutSpec] + = KOAfterUnify TcTyVarSet -- We have unified these tyvars + | KOAfterAdding CanEqLHS -- We are adding to the inert set a canonical equality + -- constraint with this LHS + +{- Note [KickOutSpec] +~~~~~~~~~~~~~~~~~~~~~~ +KickOutSpec explains why we are kicking out. + +Important property: + KOAfterAdding (TyVarLHS tv) should behave exactly like + KOAfterUnifying (unitVarSet tv) + +The main reasons for treating the two separately are +* More efficient in the single-tyvar case +* The code is far more perspicuous +-} + +kickOutRewritableLHS :: KickOutSpec -> CtFlavourRole -> InertCans -> (Cts, InertCans) -- See Note [kickOutRewritable] -kickOutRewritableLHS new_fr new_lhs +kickOutRewritableLHS ko_spec new_fr@(_, new_role) ics@(IC { inert_eqs = tv_eqs , inert_dicts = dictmap , inert_funeqs = funeqmap @@ -1319,18 +1375,11 @@ kickOutRewritableLHS new_fr new_lhs , inert_irreds = irs_in , inert_insts = insts_in } - kicked_out :: WorkList - -- NB: use extendWorkList to ensure that kicked-out equalities get priority - -- See Note [Prioritise equalities] (Kick-out). - -- The irreds may include non-canonical (hetero-kinded) equality - -- constraints, which perhaps may have become soluble after new_lhs - -- is substituted; ditto the dictionaries, which may include (a~b) - -- or (a~~b) constraints. - kicked_out = foldr extendWorkListCt - (emptyWorkList { wl_eqs = map CEqCan tv_eqs_out ++ - map CEqCan feqs_out }) - ((dicts_out `andCts` irs_out) - `extendCtsList` insts_out) + kicked_out :: Cts + kicked_out = (dicts_out `andCts` irs_out) + `extendCtsList` insts_out + `extendCtsList` map CEqCan tv_eqs_out + `extendCtsList` map CEqCan feqs_out (tv_eqs_out, tv_eqs_in) = partitionInertEqs kick_out_eq tv_eqs (feqs_out, feqs_in) = partitionFunEqs kick_out_eq funeqmap @@ -1356,14 +1405,12 @@ kickOutRewritableLHS new_fr new_lhs | otherwise = Right qci - (_, new_role) = new_fr - - fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool - fr_tv_can_rewrite_ty new_tv role ty + fr_tv_can_rewrite_ty :: (TyVar -> Bool) -> EqRel -> Type -> Bool + fr_tv_can_rewrite_ty ok_tv role ty = anyRewritableTyVar role can_rewrite ty where can_rewrite :: EqRel -> TyVar -> Bool - can_rewrite old_role tv = new_role `eqCanRewrite` old_role && tv == new_tv + can_rewrite old_role tv = new_role `eqCanRewrite` old_role && ok_tv tv fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool fr_tf_can_rewrite_ty new_tf new_tf_args role ty @@ -1376,28 +1423,23 @@ kickOutRewritableLHS new_fr new_lhs -- it's possible for old_tf_args to have too many. This is fine; -- we'll only check what we need to. - {-# INLINE fr_can_rewrite_ty #-} -- perform the check here only once + {-# INLINE fr_can_rewrite_ty #-} -- Perform case analysis on ko_spec only once fr_can_rewrite_ty :: EqRel -> Type -> Bool - fr_can_rewrite_ty = case new_lhs of - TyVarLHS new_tv -> fr_tv_can_rewrite_ty new_tv - TyFamLHS new_tf new_tf_args -> fr_tf_can_rewrite_ty new_tf new_tf_args + fr_can_rewrite_ty = case ko_spec of -- See Note [KickOutSpec] + KOAfterUnify tvs -> fr_tv_can_rewrite_ty (`elemVarSet` tvs) + KOAfterAdding (TyVarLHS tv) -> fr_tv_can_rewrite_ty (== tv) + KOAfterAdding (TyFamLHS tf tf_args) -> fr_tf_can_rewrite_ty tf tf_args fr_may_rewrite :: CtFlavourRole -> Bool fr_may_rewrite fs = new_fr `eqCanRewriteFR` fs -- Can the new item rewrite the inert item? - {-# INLINE kick_out_ct #-} -- perform case on new_lhs here only once kick_out_ct :: Ct -> Bool -- Kick it out if the new CEqCan can rewrite the inert one -- See Note [kickOutRewritable] - kick_out_ct = case new_lhs of - TyVarLHS new_tv -> \ct -> let fs@(_,role) = ctFlavourRole ct in - fr_may_rewrite fs - && fr_tv_can_rewrite_ty new_tv role (ctPred ct) - TyFamLHS new_tf new_tf_args - -> \ct -> let fs@(_, role) = ctFlavourRole ct in - fr_may_rewrite fs - && fr_tf_can_rewrite_ty new_tf new_tf_args role (ctPred ct) + kick_out_ct ct = fr_may_rewrite fs && fr_can_rewrite_ty role (ctPred ct) + where + fs@(_,role) = ctFlavourRole ct -- Implements criteria K1-K3 in Note [Extending the inert equalities] kick_out_eq :: EqCt -> Bool @@ -1430,13 +1472,31 @@ kickOutRewritableLHS new_fr new_lhs kick_out_for_completeness -- (K3) and Note [K3: completeness of solving] = case eq_rel of - NomEq -> rhs_ty `eqType` canEqLHSType new_lhs -- (K3a) - ReprEq -> is_can_eq_lhs_head new_lhs rhs_ty -- (K3b) - - - is_can_eq_lhs_head (TyVarLHS tv) = go + NomEq -> is_new_lhs rhs_ty -- (K3a) + ReprEq -> head_is_new_lhs rhs_ty -- (K3b) + + is_new_lhs :: Type -> Bool + is_new_lhs = case ko_spec of -- See Note [KickOutSpec] + KOAfterUnify tvs -> is_tyvar_ty_for tvs + KOAfterAdding lhs -> (`eqType` canEqLHSType lhs) + + is_tyvar_ty_for :: TcTyVarSet -> Type -> Bool + -- True if the type is equal to one of the tyvars + is_tyvar_ty_for tvs ty + = case getTyVar_maybe ty of + Nothing -> False + Just tv -> tv `elemVarSet` tvs + + head_is_new_lhs :: Type -> Bool + head_is_new_lhs = case ko_spec of -- See Note [KickOutSpec] + KOAfterUnify tvs -> tv_at_head (`elemVarSet` tvs) + KOAfterAdding (TyVarLHS tv) -> tv_at_head (== tv) + KOAfterAdding (TyFamLHS tf tf_args) -> fam_at_head tf tf_args + + tv_at_head :: (TyVar -> Bool) -> Type -> Bool + tv_at_head is_tv = go where - go (Rep.TyVarTy tv') = tv == tv' + go (Rep.TyVarTy tv) = is_tv tv go (Rep.AppTy fun _) = go fun go (Rep.CastTy ty _) = go ty go (Rep.TyConApp {}) = False @@ -1444,7 +1504,9 @@ kickOutRewritableLHS new_fr new_lhs go (Rep.ForAllTy {}) = False go (Rep.FunTy {}) = False go (Rep.CoercionTy {}) = False - is_can_eq_lhs_head (TyFamLHS fun_tc fun_args) = go + + fam_at_head :: TyCon -> [Type] -> Type -> Bool + fam_at_head fun_tc fun_args = go where go (Rep.TyVarTy {}) = False go (Rep.AppTy {}) = False -- no TyConApp to the left of an AppTy diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs index 809c71100b..e40478279c 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -11,7 +11,6 @@ import GHC.Tc.Solver.Canonical import GHC.Tc.Solver.Dict import GHC.Tc.Errors.Types import GHC.Tc.Utils.TcType -import GHC.Tc.Instance.FunDeps import GHC.Tc.Instance.Class ( safeOverlap ) import GHC.Tc.Types.Evidence import GHC.Tc.Types @@ -22,7 +21,6 @@ import GHC.Tc.Solver.InertSet import GHC.Tc.Solver.Monad import GHC.Core.InstEnv ( Coherence(..) ) -import GHC.Core.Class import GHC.Core.Predicate import GHC.Core.Coercion @@ -155,8 +153,7 @@ solveSimples :: Cts -> TcS () solveSimples cts = {-# SCC "solveSimples" #-} - do { updWorkListTcS (\wl -> foldr extendWorkListCt wl cts) - ; solve_loop } + do { emitWork cts; solve_loop } where solve_loop = {-# SCC "solve_loop" #-} @@ -308,7 +305,7 @@ runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline -> WorkItem -- The work item -> TcS () -- Run this item down the pipeline, leaving behind new work and inerts -runSolverPipeline pipeline workItem +runSolverPipeline full_pipeline workItem = do { wl <- getWorkList ; inerts <- getTcSInerts ; tclevel <- getTcLevel @@ -320,7 +317,7 @@ runSolverPipeline pipeline workItem , text "rest of worklist =" <+> ppr wl ] ; bumpStepCountTcS -- One step for each constraint processed - ; final_res <- run_pipeline pipeline (ContinueWith workItem) + ; final_res <- run_pipeline full_pipeline workItem ; case final_res of Stop ev s -> do { traceFireTcS ev s @@ -330,26 +327,29 @@ runSolverPipeline pipeline workItem ; traceFireTcS (ctEvidence ct) (text "Kept as inert") ; traceTcS "End solver pipeline (kept as inert) }" $ (text "final_item =" <+> ppr ct) } + StartAgain ct -> pprPanic "runSolverPipeline: StartAgain" (ppr ct) } - where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct - -> TcS (StopOrContinue Ct) - run_pipeline [] res = return res - run_pipeline _ (Stop ev s) = return (Stop ev s) - run_pipeline ((stg_name,stg):stgs) (ContinueWith ct) - = do { traceTcS ("runStage " ++ stg_name ++ " {") - (text "workitem = " <+> ppr ct) - ; res <- stg ct - ; traceTcS ("end stage " ++ stg_name ++ " }") empty - ; run_pipeline stgs res } + where + run_pipeline :: [(String,SimplifierStage)] -> Ct -> TcS (StopOrContinue Ct) + run_pipeline [] ct = return (ContinueWith ct) + run_pipeline ((stage_name,stage):stages) ct + = do { traceTcS ("runStage " ++ stage_name ++ " {") + (text "workitem = " <+> ppr ct) + ; res <- stage ct + ; traceTcS ("end stage " ++ stage_name ++ " }") (ppr res) + ; case res of + Stop {} -> return res + StartAgain ct -> run_pipeline full_pipeline ct + ContinueWith ct -> run_pipeline stages ct } {- Example 1: Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given) Reagent: a ~ [b] (given) -React with (c~d) ==> IR (ContinueWith (a~[b])) True [] -React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t] -React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True [] +React with (c~d) ==> IR (ContinueWith (a~[b])) True [] +React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t] +React with (b ~ Int) ==> IR (ContinueWith (a~[Int])) True [] Example 2: Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty} @@ -1025,8 +1025,7 @@ interactDict inerts ct_w@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = t = interactGivenIP inerts ct_w | otherwise - = do { addFunDepWork inerts ev_w cls - ; continueWith ct_w } + = continueWith ct_w interactDict _ wi = pprPanic "interactDict" (ppr wi) @@ -1131,44 +1130,6 @@ shortCutSolver dflags ev_w ev_i Nothing -> Fresh <$> newWantedNC loc (ctEvRewriters ev_w) pty | otherwise = mzero -addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS () --- Add wanted constraints from type-class functional dependencies. -addFunDepWork inerts work_ev cls - = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls) - -- No need to check flavour; fundeps work between - -- any pair of constraints, regardless of flavour - -- Importantly we don't throw workitem back in the - -- worklist because this can cause loops (see #5236) - where - work_pred = ctEvPred work_ev - work_loc = ctEvLoc work_ev - - add_fds inert_ct - = do { traceTcS "addFunDepWork" (vcat - [ ppr work_ev - , pprCtLoc work_loc, ppr (isGivenLoc work_loc) - , pprCtLoc inert_loc, ppr (isGivenLoc inert_loc) - , pprCtLoc derived_loc, ppr (isGivenLoc derived_loc) ]) - - ; unless (isGiven work_ev && isGiven inert_ev) $ - emitFunDepWanteds (ctEvRewriters work_ev) $ - improveFromAnother (derived_loc, inert_rewriters) inert_pred work_pred - -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok - -- Do not create FDs from Given/Given interactions: See Note [No Given/Given fundeps] - } - where - inert_ev = ctEvidence inert_ct - inert_pred = ctEvPred inert_ev - inert_loc = ctEvLoc inert_ev - inert_rewriters = ctRewriters inert_ct - derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth` - ctl_depth inert_loc - , ctl_origin = FunDepOrigin1 work_pred - (ctLocOrigin work_loc) - (ctLocSpan work_loc) - inert_pred - (ctLocOrigin inert_loc) - (ctLocSpan inert_loc) } {- ********************************************************************** diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs index befc9e212e..91e20becf8 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -33,6 +33,7 @@ module GHC.Tc.Solver.Monad ( -- The pipeline StopOrContinue(..), continueWith, stopWith, andWhenContinue, + startAgainWith, -- Tracing etc panicTcS, traceTcS, @@ -51,7 +52,7 @@ module GHC.Tc.Solver.Monad ( unifyTyVar, reportUnifications, touchabilityAndShapeTest, setEvBind, setWantedEq, setWantedEvTerm, setEvBindIfWanted, - newEvVar, newGivenEvVar, newGivenEvVars, + newEvVar, newGivenEvVar, emitNewGivens, checkReductionDepth, getSolvedDicts, setSolvedDicts, @@ -95,7 +96,7 @@ module GHC.Tc.Solver.Monad ( instDFunType, -- Unification - unifyWanted, unifyWanteds, + wrapUnifierTcS, unifyFunDeps, uPairsTcM, -- MetaTyVars newFlexiTcSTy, instFlexiX, @@ -159,6 +160,7 @@ import GHC.Builtin.Names ( unsatisfiableClassNameKey ) import GHC.Core.Type import GHC.Core.TyCo.Rep as Rep import GHC.Core.Coercion +import GHC.Core.Coercion.Axiom( TypeEqn ) import GHC.Core.Predicate import GHC.Core.Reduction import GHC.Core.Class @@ -171,6 +173,7 @@ import GHC.Types.Name.Reader import GHC.Types.Var import GHC.Types.Var.Set import GHC.Types.Unique.Supply +import GHC.Types.Unique.Set( elementOfUniqSet ) import GHC.Unit.Module ( HasModule, getModule, extractModule ) import qualified GHC.Rename.Env as TcM @@ -184,12 +187,11 @@ import GHC.Data.Bag as Bag import GHC.Data.Pair import GHC.Utils.Monad -import GHC.Utils.Misc( equalLength ) import GHC.Exts (oneShot) import Control.Monad import Data.IORef -import Data.List ( mapAccumL, zip4 ) +import Data.List ( mapAccumL ) import Data.Foldable import qualified Data.Semigroup as S @@ -205,7 +207,10 @@ import GHC.Data.Graph.Directed ********************************************************************* -} data StopOrContinue a - = ContinueWith a -- The constraint was not solved, although it may have + = StartAgain a -- Constraint is not solved, but some unifications + -- happened, so go back to the beginning of the pipeline + + | ContinueWith a -- The constraint was not solved, although it may have -- been rewritten | Stop CtEvidence -- The (rewritten) constraint was solved @@ -216,21 +221,25 @@ data StopOrContinue a instance Outputable a => Outputable (StopOrContinue a) where ppr (Stop ev s) = text "Stop" <> parens s <+> ppr ev ppr (ContinueWith w) = text "ContinueWith" <+> ppr w + ppr (StartAgain w) = text "StartAgain" <+> ppr w + +startAgainWith :: a -> TcS (StopOrContinue a) +startAgainWith ct = return (StartAgain ct) continueWith :: a -> TcS (StopOrContinue a) -continueWith = return . ContinueWith +continueWith ct = return (ContinueWith ct) stopWith :: CtEvidence -> String -> TcS (StopOrContinue a) stopWith ev s = return (Stop ev (text s)) andWhenContinue :: TcS (StopOrContinue a) - -> (a -> TcS (StopOrContinue b)) - -> TcS (StopOrContinue b) + -> (a -> TcS (StopOrContinue a)) + -> TcS (StopOrContinue a) andWhenContinue tcs1 tcs2 = do { r <- tcs1 ; case r of - Stop ev s -> return (Stop ev s) - ContinueWith ct -> tcs2 ct } + ContinueWith ct -> tcs2 ct + _ -> return r } infixr 0 `andWhenContinue` -- allow chaining with ($) @@ -340,8 +349,9 @@ addInertCan ct = maybeKickOut :: InertCans -> Ct -> TcS InertCans -- For a CEqCan, kick out any inert that can be rewritten by the CEqCan maybeKickOut ics ct - | CEqCan (EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel }) <- ct - = do { (_, ics') <- kickOutRewritable (ctEvFlavour ev, eq_rel) lhs ics + | CEqCan eq_ct <- ct + = do { (_, ics') <- kickOutRewritable (KOAfterAdding (eqCtLHS eq_ct)) + (eqCtFlavourRole eq_ct) ics ; return ics' } -- See [Kick out existing binding for implicit parameter] @@ -368,61 +378,73 @@ maybeKickOut ics ct = return ics ----------------------------------------- -kickOutRewritable :: CtFlavourRole -- Flavour/role of the equality that - -- is being added to the inert set - -> CanEqLHS -- The new equality is lhs ~ ty - -> InertCans - -> TcS (Int, InertCans) -kickOutRewritable new_fr new_lhs ics - = do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics - n_kicked = workListSize kicked_out +kickOutRewritable :: KickOutSpec -> CtFlavourRole + -> InertCans -> TcS (Int, InertCans) +kickOutRewritable ko_spec new_fr ics + = do { let (kicked_out, ics') = kickOutRewritableLHS ko_spec new_fr ics + n_kicked = lengthBag kicked_out - ; unless (n_kicked == 0) $ - do { updWorkListTcS (appendWorkList kicked_out) + ; unless (isEmptyBag kicked_out) $ + do { emitWork kicked_out -- The famapp-cache contains Given evidence from the inert set. -- If we're kicking out Givens, we need to remove this evidence -- from the cache, too. - ; let kicked_given_ev_vars = - [ ev_var | ct <- wl_eqs kicked_out - , CtGiven { ctev_evar = ev_var } <- [ctEvidence ct] ] + ; let kicked_given_ev_vars = foldr add_one emptyVarSet kicked_out + add_one :: Ct -> VarSet -> VarSet + add_one ct vs | CtGiven { ctev_evar = ev_var } <- ctEvidence ct + = vs `extendVarSet` ev_var + | otherwise = vs + ; when (new_fr `eqCanRewriteFR` (Given, NomEq) && -- if this isn't true, no use looking through the constraints - not (null kicked_given_ev_vars)) $ + not (isEmptyVarSet kicked_given_ev_vars)) $ do { traceTcS "Given(s) have been kicked out; drop from famapp-cache" (ppr kicked_given_ev_vars) - ; dropFromFamAppCache (mkVarSet kicked_given_ev_vars) } + ; dropFromFamAppCache kicked_given_ev_vars } ; csTraceTcS $ - hang (text "Kick out, lhs =" <+> ppr new_lhs) + hang (text "Kick out") 2 (vcat [ text "n-kicked =" <+> int n_kicked , text "kicked_out =" <+> ppr kicked_out , text "Residual inerts =" <+> ppr ics' ]) } ; return (n_kicked, ics') } -kickOutAfterUnification :: TcTyVar -> TcS Int -kickOutAfterUnification new_tv +kickOutAfterUnification :: [TcTyVar] -> TcS Int +kickOutAfterUnification tvs + | null tvs + = return 0 + | otherwise = do { ics <- getInertCans - ; (n_kicked, ics2) <- kickOutRewritable (Given,NomEq) - (TyVarLHS new_tv) ics - -- Given because the tv := xi is given; NomEq because - -- only nominal equalities are solved by unification - + ; let tv_set = mkVarSet tvs + ; (n_kicked, ics2) <- kickOutRewritable (KOAfterUnify tv_set) + (Given, NomEq) ics + -- Given because the tv := xi is given; NomEq because + -- only nominal equalities are solved by unification ; setInertCans ics2 + + -- Set the unification flag if we have done outer unifications + -- that might affect an earlier implication constraint + ; let min_tv_lvl = foldr1 minTcLevel (map tcTyVarLevel tvs) + ; ambient_lvl <- getTcLevel + ; when (ambient_lvl `strictlyDeeperThan` min_tv_lvl) $ + setUnificationFlag min_tv_lvl + + ; traceTcS "kickOutAfterUnification" (ppr tvs $$ text "n_kicked =" <+> ppr n_kicked) ; return n_kicked } --- See Wrinkle (2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical +kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () +-- See Wrinkle (EIK2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical -- It's possible that this could just go ahead and unify, but could there be occurs-check -- problems? Seems simpler just to kick out. -kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () kickOutAfterFillingCoercionHole hole = do { ics <- getInertCans ; let (kicked_out, ics') = kick_out ics - n_kicked = workListSize kicked_out + n_kicked = lengthBag kicked_out ; unless (n_kicked == 0) $ - do { updWorkListTcS (appendWorkList kicked_out) + do { updWorkListTcS (extendWorkListCts kicked_out) ; csTraceTcS $ hang (text "Kick out, hole =" <+> ppr hole) 2 (vcat [ text "n-kicked =" <+> int n_kicked @@ -431,19 +453,26 @@ kickOutAfterFillingCoercionHole hole ; setInertCans ics' } where - kick_out :: InertCans -> (WorkList, InertCans) - kick_out ics@(IC { inert_eqs = eqs, inert_funeqs = funeqs }) - = (kicked_out, ics { inert_eqs = eqs_to_keep, inert_funeqs = funeqs_to_keep }) + kick_out :: InertCans -> (Cts, InertCans) + kick_out ics@(IC { inert_irreds = irreds }) + = -- We only care about irreds here, because any constraint blocked + -- by a coercion hole is an irred. See wrinkle (EIK2a) in + -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical + (irreds_to_kick, ics { inert_irreds = irreds_to_keep }) where - (eqs_to_kick, eqs_to_keep) = partitionInertEqs kick_ct eqs - (funeqs_to_kick, funeqs_to_keep) = partitionFunEqs kick_ct funeqs - kicked_out = extendWorkListCts (map CEqCan (eqs_to_kick ++ funeqs_to_kick)) emptyWorkList + (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds - kick_ct :: EqCt -> Bool + kick_ct :: Ct -> Bool -- True: kick out; False: keep. - kick_ct (EqCt { eq_rhs = rhs, eq_ev = ctev }) - = isWanted ctev && -- optimisation: givens don't have coercion holes anyway - rhs `hasThisCoercionHoleTy` hole + kick_ct ct + | CIrredCan { cc_ev = ev, cc_reason = reason } <- ct + , CtWanted { ctev_rewriters = RewriterSet rewriters } <- ev + , NonCanonicalReason ctyeq <- reason + , ctyeq `cterHasProblem` cteCoercionHole + , hole `elementOfUniqSet` rewriters + = True + | otherwise + = False -------------- addInertSafehask :: InertCans -> Ct -> InertCans @@ -1258,12 +1287,21 @@ emitWorkNC evs | null evs = return () | otherwise - = emitWork (map mkNonCanonical evs) + = emitWork (listToBag (map mkNonCanonical evs)) -emitWork :: [Ct] -> TcS () -emitWork [] = return () -- avoid printing, among other work +emitWork :: Cts -> TcS () emitWork cts - = do { traceTcS "Emitting fresh work" (vcat (map ppr cts)) + | isEmptyBag cts -- Avoid printing, among other work + = return () + | otherwise + = do { traceTcS "Emitting fresh work" (pprBag cts) + -- Zonk the rewriter set of Wanteds, because that affects + -- the prioritisation of the work-list. Suppose a constraint + -- c1 is rewritten by another, c2. When c2 gets solved, + -- c1 has no rewriters, and can be prioritised; see + -- Note [Prioritise Wanteds with empty RewriterSet] + -- in GHC.Tc.Types.Constraint wrinkle (WRW1) + ; cts <- wrapTcS $ mapBagM TcM.zonkCtRewriterSet cts ; updWorkListTcS (extendWorkListCts cts) } emitImplication :: Implication -> TcS () @@ -1553,7 +1591,7 @@ track of - Whether any unifications at all have taken place (Nothing => no unifications) - If so, what is the outermost level that has seen a unification (Just lvl) -The iteration done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver. +The iteration is done in the simplify_loop/maybe_simplify_again loop in GHC.Tc.Solver. It helpful not to iterate unless there is a chance of progress. #8474 is an example: @@ -1627,20 +1665,22 @@ cloneMetaTyVar :: TcTyVar -> TcS TcTyVar cloneMetaTyVar tv = wrapTcS (TcM.cloneMetaTyVar tv) instFlexiX :: Subst -> [TKVar] -> TcS Subst -instFlexiX subst tvs - = wrapTcS (foldlM instFlexiHelper subst tvs) +instFlexiX subst tvs = wrapTcS (instFlexiXTcM subst tvs) -instFlexiHelper :: Subst -> TKVar -> TcM Subst +instFlexiXTcM :: Subst -> [TKVar] -> TcM Subst -- Makes fresh tyvar, extends the substitution, and the in-scope set -instFlexiHelper subst tv +-- Takes account of the case [k::Type, a::k, ...], +-- where we must substitute for k in a's kind +instFlexiXTcM subst [] + = return subst +instFlexiXTcM subst (tv:tvs) = do { uniq <- TcM.newUnique ; details <- TcM.newMetaDetails TauTv ; let name = setNameUnique (tyVarName tv) uniq kind = substTyUnchecked subst (tyVarKind tv) tv' = mkTcTyVar name kind details subst' = extendTvSubstWithClone subst tv tv' - ; TcM.traceTc "instFlexi" (ppr tv') - ; return (extendTvSubst subst' tv (mkTyVarTy tv')) } + ; instFlexiXTcM subst' tvs } matchGlobalInst :: DynFlags -> Bool -- True <=> caller is the short-cut solver @@ -1761,14 +1801,19 @@ newBoundEvVarId pred rhs ; setEvBind (mkGivenEvBind new_ev rhs) ; return new_ev } -newGivenEvVars :: CtLoc -> [(TcPredType, EvTerm)] -> TcS [CtEvidence] -newGivenEvVars loc pts = mapM (newGivenEvVar loc) pts +emitNewGivens :: CtLoc -> [(Role,TcType,TcType,TcCoercion)] -> TcS () +emitNewGivens loc pts + = do { evs <- mapM (newGivenEvVar loc) $ + [ (mkPrimEqPredRole role ty1 ty2, evCoercion co) + | (role, ty1, ty2, co) <- pts + , not (ty1 `tcEqType` ty2) ] -- Kill reflexive Givens at birth + ; emitWorkNC evs } emitNewWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS Coercion -- | Emit a new Wanted equality into the work-list emitNewWantedEq loc rewriters role ty1 ty2 = do { (ev, co) <- newWantedEq loc rewriters role ty1 ty2 - ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) + ; updWorkListTcS (extendWorkListEq rewriters (mkNonCanonical ev)) ; return co } -- | Create a new Wanted constraint holding a coercion hole @@ -1776,8 +1821,7 @@ emitNewWantedEq loc rewriters role ty1 ty2 newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) newWantedEq loc rewriters role ty1 ty2 - = do { hole <- wrapTcS $ TcM.newCoercionHole pty - ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) + = do { hole <- wrapTcS $ TcM.newCoercionHole loc pty ; return ( CtWanted { ctev_pred = pty , ctev_dest = HoleDest hole , ctev_loc = loc @@ -1906,43 +1950,47 @@ solverDepthError loc ty ************************************************************************ -} -emitFunDepWanteds :: RewriterSet -- from the work item - -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS () +emitFunDepWanteds :: CtEvidence -- The work item + -> [FunDepEqn (CtLoc, RewriterSet)] + -> TcS Bool -- True <=> some unification happened -emitFunDepWanteds _ [] = return () -- common case noop +emitFunDepWanteds _ [] = return False -- common case noop -- See Note [FunDep and implicit parameter reactions] -emitFunDepWanteds work_rewriters fd_eqns - = mapM_ do_one_FDEqn fd_eqns +emitFunDepWanteds ev fd_eqns + = unifyFunDeps ev Nominal do_fundeps where - do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) }) - | null tvs -- Common shortcut - = do { traceTcS "emitFunDepWanteds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc)) - ; mapM_ (\(Pair ty1 ty2) -> unifyWanted all_rewriters loc Nominal ty1 ty2) - (reverse eqs) } - -- See Note [Reverse order of fundep equations] - - | otherwise - = do { traceTcS "emitFunDepWanteds 2" (ppr (ctl_depth loc) $$ ppr tvs $$ ppr eqs) - ; subst <- instFlexiX emptySubst tvs -- Takes account of kind substitution - ; mapM_ (do_one_eq loc all_rewriters subst) (reverse eqs) } - -- See Note [Reverse order of fundep equations] - where - all_rewriters = work_rewriters S.<> rewriters - - do_one_eq loc rewriters subst (Pair ty1 ty2) - = unifyWanted rewriters loc Nominal (substTyUnchecked subst' ty1) ty2 - -- ty2 does not mention fd_qtvs, so no need to subst it. - -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] - -- Wrinkle (1) + do_fundeps :: UnifyEnv -> TcM () + do_fundeps env = mapM_ (do_one env) fd_eqns + + do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM () + do_one uenv (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) }) + = do { eqs' <- instantiate_eqs tvs (reverse eqs) + -- (reverse eqs): See Note [Reverse order of fundep equations] + ; uPairsTcM env_one eqs' } where - subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) - -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result - -- of matching with the [W] constraint. So we add its free - -- vars to InScopeSet, to satisfy substTy's invariants, even - -- though ty1 will never (currently) be a poytype, so this - -- InScopeSet will never be looked at. + env_one = uenv { u_rewriters = u_rewriters uenv S.<> rewriters + , u_loc = loc } + instantiate_eqs :: [TyVar] -> [TypeEqn] -> TcM [TypeEqn] + instantiate_eqs tvs eqs + | null tvs + = return eqs + | otherwise + = do { TcM.traceTc "emitFunDepWanteds 2" (ppr tvs $$ ppr eqs) + ; subst <- instFlexiXTcM emptySubst tvs -- Takes account of kind substitution + ; return [ Pair (substTyUnchecked subst' ty1) ty2 + -- ty2 does not mention fd_qtvs, so no need to subst it. + -- See GHC.Tc.Instance.Fundeps Note [Improving against instances] + -- Wrinkle (1) + | Pair ty1 ty2 <- eqs + , let subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1) ] + -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result + -- of matching with the [W] constraint. So we add its free + -- vars to InScopeSet, to satisfy substTy's invariants, even + -- though ty1 will never (currently) be a poytype, so this + -- InScopeSet will never be looked at. + } {- ************************************************************************ @@ -1951,121 +1999,86 @@ emitFunDepWanteds work_rewriters fd_eqns * * ************************************************************************ -Note [unifyWanted] -~~~~~~~~~~~~~~~~~~ +Note [wrapUnifierTcS] +~~~~~~~~~~~~~~~~~~~ When decomposing equalities we often create new wanted constraints for (s ~ t). But what if s=t? Then it'd be faster to return Refl right away. -Rather than making an equality test (which traverses the structure of the -type, perhaps fruitlessly), unifyWanted traverses the common structure, and -bales out when it finds a difference by creating a new Wanted constraint. -But where it succeeds in finding common structure, it just builds a coercion -to reflect it. +Rather than making an equality test (which traverses the structure of the type, +perhaps fruitlessly), we call uType (via wrapUnifierTcS) to traverse the common +structure, and bales out when it finds a difference by creating a new deferred +Wanted constraint. But where it succeeds in finding common structure, it just +builds a coercion to reflect it. + +This is all much faster than creating a new constraint, putting it in the +work list, picking it out, canonicalising it, etc etc. + +Note [unifyFunDeps] +~~~~~~~~~~~~~~~~~~~ +The Bool returned by `unifyFunDeps` is True if we have unified a variable +that occurs in the constraint we are trying to solve; it is not in the +inert set so `wrapUnifierTcS` won't kick it out. Instead we want to send it +back to the start of the pipeline. Hence the Bool. + +It's vital that we don't return (not (null unified)) because the fundeps +may create fresh variables; unifying them (alone) should not make us send +the constraint back to the start, or we'll get an infinite loop. See +Note [Fundeps with instances, and equality orientation] in GHC.Tc.Solver.Dict +and Note [Improvement orientation] in GHC.Tc.Solver.Equality. -} -unifyWanted :: RewriterSet -> CtLoc - -> Role -> TcType -> TcType -> TcS Coercion --- Return coercion witnessing the equality of the two types, --- emitting new work equalities where necessary to achieve that --- Very good short-cut when the two types are equal, or nearly so --- See Note [unifyWanted] --- The returned coercion's role matches the input parameter -unifyWanted rewriters loc Phantom ty1 ty2 - = do { kind_co <- unifyWanted rewriters loc Nominal (typeKind ty1) (typeKind ty2) - ; return (mkPhantomCo kind_co ty1 ty2) } - -unifyWanted rewriters loc role orig_ty1 orig_ty2 - = go orig_ty1 orig_ty2 - where - go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2 - go ty1 ty2 | Just ty2' <- coreView ty2 = go ty1 ty2' - - go (FunTy af1 w1 s1 t1) (FunTy af2 w2 s2 t2) - | af1 == af2 -- Important! See #21530 - = do { co_s <- unifyWanted rewriters loc role s1 s2 - ; co_t <- unifyWanted rewriters loc role t1 t2 - ; co_w <- unifyWanted rewriters loc Nominal w1 w2 - ; return (mkNakedFunCo1 role af1 co_w co_s co_t) } - - go (TyConApp tc1 tys1) (TyConApp tc2 tys2) - | tc1 == tc2, tys1 `equalLength` tys2 - , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality - = do { cos <- zipWith3M (unifyWanted rewriters loc) - (tyConRoleListX role tc1) tys1 tys2 - ; return (mkTyConAppCo role tc1 cos) } - - go ty1@(TyVarTy tv) ty2 - = do { mb_ty <- isFilledMetaTyVar_maybe tv - ; case mb_ty of - Just ty1' -> go ty1' ty2 - Nothing -> bale_out ty1 ty2} - go ty1 ty2@(TyVarTy tv) - = do { mb_ty <- isFilledMetaTyVar_maybe tv - ; case mb_ty of - Just ty2' -> go ty1 ty2' - Nothing -> bale_out ty1 ty2 } - - go ty1@(CoercionTy {}) (CoercionTy {}) - = return (mkReflCo role ty1) -- we just don't care about coercions! - - go ty1 ty2 = bale_out ty1 ty2 - - bale_out ty1 ty2 - | ty1 `tcEqType` ty2 = return (mkReflCo role ty1) - -- Check for equality; e.g. a ~ a, or (m a) ~ (m a) - | otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2 - - -{- -Note [Decomposing Dependent TyCons and Processing Wanted Equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When we decompose a dependent tycon we obtain a list of -mixed wanted type and kind equalities. Ideally we want -all the kind equalities to get solved first so that we avoid -generating duplicate kind equalities - -For example, consider decomposing a TyCon equality +uPairsTcM :: UnifyEnv -> [TypeEqn] -> TcM () +uPairsTcM uenv eqns = mapM_ (\(Pair ty1 ty2) -> uType uenv ty1 ty2) eqns - (0) [W] T k_fresh (t1::k_fresh) ~ T k1 (t2::k_fresh) - -This gives rise to 2 equalities in the solver worklist +unifyFunDeps :: CtEvidence -> Role + -> (UnifyEnv -> TcM ()) + -> TcS Bool +unifyFunDeps ev role do_unifications + = do { (_, _, unified) <- wrapUnifierTcS ev role do_unifications + ; return (any (`elemVarSet` fvs) unified) } + -- See Note [unifyFunDeps] + where + fvs = tyCoVarsOfType (ctEvPred ev) + +wrapUnifierTcS :: CtEvidence -> Role + -> (UnifyEnv -> TcM a) -- Some calls to uType + -> TcS (a, Bag Ct, [TcTyVar]) +-- Invokes the do_unifications argument, with a suitable UnifyEnv. +-- Emit deferred equalities and kick-out from the inert set as a +-- result of any unifications. +-- Very good short-cut when the two types are equal, or nearly so +-- See Note [wrapUnifierTcS] +-- +-- The [TcTyVar] is the list of unification variables that were +-- unified the process; the (Bag Ct) are the deferred constraints. - (1) [W] k_fresh ~ k1 - (2) [W] t1::k_fresh ~ t2::k1 +wrapUnifierTcS ev role do_unifications + = do { (cos, unified, rewriters, cts) <- wrapTcS $ + do { defer_ref <- TcM.newTcRef emptyBag + ; unified_ref <- TcM.newTcRef [] + ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev) + ; let env = UE { u_role = role + , u_rewriters = rewriters + , u_loc = ctEvLoc ev + , u_defer = defer_ref + , u_unified = Just unified_ref} -The solver worklist is processed in LIFO order: -see GHC.Tc.Solver.InertSet.selectWorkItem. -i.e. (2) is processed _before_ (1). Now, while solving (2) -we would call `canEqCanLHSHetero` and that would emit a -wanted kind equality + ; cos <- do_unifications env - (3) [W] k_fresh ~ k1 + ; cts <- TcM.readTcRef defer_ref + ; unified <- TcM.readTcRef unified_ref + ; return (cos, unified, rewriters, cts) } -But (3) is exactly the same as (1)! + -- Emit the deferred constraints + -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality + ; unless (isEmptyBag cts) $ + updWorkListTcS (extendWorkListEqs rewriters cts) -To avoid such duplicate wanted constraints from being added to the worklist, -we ensure that (2) is processed before (1). Since we are processing -the worklist in a LIFO ordering, we do it by emitting (1) before (2). -This is exactly what we do in `unifyWanteds`. + -- And kick out any inert constraint that we have unified + ; _ <- kickOutAfterUnification unified -NB: This ordering is not needed when we decompose FunTyCons as they are not dependently typed --} + ; return (cos, cts, unified) } --- NB: Length of [CtLoc] and [Roles] may be infinite --- but list of RHS [TcType] and LHS [TcType] is finite and both are of equal length -unifyWanteds :: RewriterSet -> [CtLoc] -> [Role] - -> [TcType] -- List of RHS types - -> [TcType] -- List of LHS types - -> TcS [Coercion] -unifyWanteds rewriters ctlocs roles rhss lhss = unify_wanteds rewriters $ zip4 ctlocs roles rhss lhss - where - -- Order is important here - -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities] - unify_wanteds _ [] = return [] - unify_wanteds rewriters ((new_loc, tc_role, ty1, ty2) : rest) - = do { cos <- unify_wanteds rewriters rest - ; co <- unifyWanted rewriters new_loc tc_role ty1 ty2 - ; return (co:cos) } {- ************************************************************************ @@ -2081,7 +2094,7 @@ checkTouchableTyVarEq -> TcType -- The RHS -> TcS (PuResult () Reduction) -- Used for Nominal, Wanted equalities, with a touchable meta-tyvar on LHS --- If checkTouchableTyVarEq tv ty = PuOK redn cts +-- If checkTouchableTyVarEq tv ty = PuOK cts redn -- then we can unify -- tv := ty |> redn -- with extra wanteds 'cts' @@ -2098,7 +2111,7 @@ checkTouchableTyVarEq ev lhs_tv rhs ; traceTcS "checkTouchableTyVarEq }" (ppr lhs_tv $$ ppr check_result) ; case check_result of PuFail reason -> return (PuFail reason) - PuOK redn cts -> do { emitWork (bagToList cts) + PuOK cts redn -> do { emitWork cts ; return (pure redn) } } where @@ -2147,13 +2160,13 @@ checkTouchableTyVarEq ev lhs_tv rhs _ -> TcM.newMetaTyVarTyAtLevel lhs_tv_lvl fam_app_kind ; let pty = mkPrimEqPredRole Nominal fam_app new_tv_ty - ; hole <- TcM.newCoercionHole pty + ; hole <- TcM.newVanillaCoercionHole pty ; let new_ev = CtWanted { ctev_pred = pty , ctev_dest = HoleDest hole , ctev_loc = cb_loc , ctev_rewriters = ctEvRewriters ev } - ; return (PuOK (mkReduction (HoleCo hole) new_tv_ty) - (singleCt (mkNonCanonical new_ev))) } } + ; return (PuOK (singleCt (mkNonCanonical new_ev)) + (mkReduction (HoleCo hole) new_tv_ty)) } } -- See Detail (7) of the Note cb_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin @@ -2171,8 +2184,8 @@ checkTypeEq ev eq_rel lhs rhs ; traceTcS "checkTypeEq }" (ppr check_result) ; case check_result of PuFail reason -> return (PuFail reason) - PuOK redn prs -> do { new_givens <- mapBagM mk_new_given prs - ; emitWorkNC (bagToList new_givens) + PuOK prs redn -> do { new_givens <- mapBagM mk_new_given prs + ; emitWork new_givens ; updInertTcS (addCycleBreakerBindings prs) ; return (pure redn) } } @@ -2180,9 +2193,10 @@ checkTypeEq ev eq_rel lhs rhs = do { check_result <- wrapTcS (checkTyEqRhs wanted_flags rhs) ; case check_result of PuFail reason -> return (PuFail reason) - PuOK redn cts -> do { emitWork (bagToList cts) + PuOK cts redn -> do { emitWork cts ; return (pure redn) } } where + check_given_rhs :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction) check_given_rhs rhs -- See Note [Special case for top-level of Given equality] | Just (TyFamLHS tc tys) <- canTyFamEqLHS_maybe rhs @@ -2192,6 +2206,7 @@ checkTypeEq ev eq_rel lhs rhs arg_flags = famAppArgFlags given_flags + given_flags :: TyEqFlags (TcTyVar,TcType) given_flags = TEF { tef_lhs = lhs , tef_foralls = False , tef_unifying = NotUnifying @@ -2215,14 +2230,14 @@ checkTypeEq ev eq_rel lhs rhs break_given :: TcType -> TcM (PuResult (TcTyVar,TcType) Reduction) break_given fam_app = do { new_tv <- TcM.newCycleBreakerTyVar (typeKind fam_app) - ; return (PuOK (mkReflRedn Nominal (mkTyVarTy new_tv)) - (unitBag (new_tv, fam_app))) } + ; return (PuOK (unitBag (new_tv, fam_app)) + (mkReflRedn Nominal (mkTyVarTy new_tv))) } -- Why reflexive? See Detail (4) of the Note --------------------------- - mk_new_given :: (TcTyVar, TcType) -> TcS CtEvidence + mk_new_given :: (TcTyVar, TcType) -> TcS Ct mk_new_given (new_tv, fam_app) - = newGivenEvVar cb_loc (given_pred, given_term) + = mkNonCanonical <$> newGivenEvVar cb_loc (given_pred, given_term) where new_ty = mkTyVarTy new_tv given_pred = mkPrimEqPred fam_app new_ty diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs index 6508a21420..64d590cbe9 100644 --- a/compiler/GHC/Tc/Solver/Rewrite.hs +++ b/compiler/GHC/Tc/Solver/Rewrite.hs @@ -41,6 +41,7 @@ import Control.Applicative (liftA3) import GHC.Builtin.Types (tYPETyCon) import Data.List ( find ) import GHC.Data.List.Infinite (Infinite) +import GHC.Data.Bag( listToBag ) import qualified GHC.Data.List.Infinite as Inf {- @@ -155,7 +156,7 @@ bumpDepth (RewriteM thing_inside) -- Precondition: the CtEvidence is a CtWanted of an equality recordRewriter :: CtEvidence -> RewriteM () recordRewriter (CtWanted { ctev_dest = HoleDest hole }) - = RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriterSet` hole) + = RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriter` hole) recordRewriter other = pprPanic "recordRewriter" (ppr other) {- @@ -945,7 +946,7 @@ runTcPluginRewriters rewriteEnv rewriterFunctions tys TcPluginRewriteTo { tcPluginReduction = redn , tcRewriterNewWanteds = wanteds - } -> do { emitWork wanteds; return $ Just redn } + } -> do { emitWork (listToBag wanteds); return $ Just redn } TcPluginNoRewrite {} -> runRewriters givens rewriters {- diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index d99f9067df..78c1134475 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -10,7 +10,7 @@ module GHC.Tc.Types.Constraint ( QCInst(..), pendingScInst_maybe, -- Canonical constraints - Xi, Ct(..), EqCt(..), Cts, + Xi, Ct(..), Cts, singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList, isEmptyCts, emptyCts, andCts, ctsPreds, isPendingScDict, pendingScDict_maybe, @@ -43,6 +43,8 @@ module GHC.Tc.Types.Constraint ( cterHasNoProblem, cterHasProblem, cterHasOnlyProblem, cterHasOnlyProblems, cterRemoveProblem, cterHasOccursCheck, cterFromKind, + + EqCt(..), eqCtLHS, eqCtEvidence, CanEqLHS(..), canEqLHS_maybe, canTyFamEqLHS_maybe, canEqLHSKind, canEqLHSType, eqCanEqLHS, @@ -68,11 +70,11 @@ module GHC.Tc.Types.Constraint ( ctLocTypeOrKind_maybe, ctLocDepth, bumpCtLocDepth, isGivenLoc, setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan, - pprCtLoc, + pprCtLoc, adjustCtLoc, adjustCtLocTyConBinder, -- CtEvidence CtEvidence(..), TcEvDest(..), - mkKindLoc, toKindLoc, mkGivenLoc, + mkKindEqLoc, toKindLoc, toInvisibleLoc, mkGivenLoc, isWanted, isGiven, ctEvRole, setCtEvPredType, setCtEvLoc, arisesFromGivens, tyCoVarsOfCtEvList, tyCoVarsOfCtEv, tyCoVarsOfCtEvsList, @@ -80,8 +82,7 @@ module GHC.Tc.Types.Constraint ( RewriterSet(..), emptyRewriterSet, isEmptyRewriterSet, -- exported concretely only for anyUnfilledCoercionHoles - rewriterSetFromType, rewriterSetFromTypes, rewriterSetFromCo, - addRewriterSet, + addRewriter, unitRewriterSet, unionRewriterSet, rewriterSetFromCts, wrapType, @@ -132,7 +133,6 @@ import GHC.Utils.Constants (debugIsOn) import GHC.Types.Name.Reader import Data.Coerce -import Data.Monoid ( Endo(..) ) import qualified Data.Semigroup as S import Control.Monad ( msum, when ) import Data.Maybe ( mapMaybe, isJust ) @@ -234,8 +234,8 @@ data Ct -- look like this, with the payload in an -- auxiliary type -{- Note [Invariants of EqCt] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Canonical equalities] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ An EqCt is a canonical equality constraint, one that can live in the inert set, and that can be used to rewrite other constrtaints. It satisfies these invariants: * (TyEq:OC) lhs does not occur in rhs (occurs check) @@ -249,6 +249,9 @@ and that can be used to rewrite other constrtaints. It satisfies these invariant (Applies only when constructor of newtype is in scope.) * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we will not form an EqCt (a ~ ty). + * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up + a hetero-kinded equality. See Note [Equalities with incompatible kinds] in + GHC.Tc.Solver.Equality, wrinkle (EIK2) These invariants ensure that the EqCts in inert_eqs constitute a terminating generalised substitution. See Note [inert_eqs: the inert equalities] @@ -286,7 +289,7 @@ and forms condition T3 in Note [Extending the inert equalities] in GHC.Tc.Solver.InertSet. -} -data EqCt -- An equality constraint; see Note [Invariants of EqCt] +data EqCt -- An equality constraint; see Note [Canonical equalities] = EqCt { -- CanEqLHS ~ rhs eq_ev :: CtEvidence, -- See Note [Ct/evidence invariant] eq_lhs :: CanEqLHS, @@ -294,6 +297,12 @@ data EqCt -- An equality constraint; see Note [Invariants of EqCt] eq_eq_rel :: EqRel -- INVARIANT: cc_eq_rel = ctEvEqRel cc_ev } +eqCtEvidence :: EqCt -> CtEvidence +eqCtEvidence = eq_ev + +eqCtLHS :: EqCt -> CanEqLHS +eqCtLHS = eq_lhs + ------------ -- | A 'CanEqLHS' is a type that can appear on the left of a canonical -- equality: a type variable or /exactly-saturated/ type family application. @@ -2083,41 +2092,26 @@ newtype RewriterSet = RewriterSet (UniqSet CoercionHole) emptyRewriterSet :: RewriterSet emptyRewriterSet = RewriterSet emptyUniqSet +unitRewriterSet :: CoercionHole -> RewriterSet +unitRewriterSet = coerce (unitUniqSet @CoercionHole) + +unionRewriterSet :: RewriterSet -> RewriterSet -> RewriterSet +unionRewriterSet = coerce (unionUniqSets @CoercionHole) + isEmptyRewriterSet :: RewriterSet -> Bool -isEmptyRewriterSet (RewriterSet set) = isEmptyUniqSet set - -addRewriterSet :: RewriterSet -> CoercionHole -> RewriterSet -addRewriterSet = coerce (addOneToUniqSet @CoercionHole) - --- | Makes a 'RewriterSet' from all the coercion holes that occur in the --- given coercion. -rewriterSetFromCo :: Coercion -> RewriterSet -rewriterSetFromCo co = appEndo (rewriter_set_from_co co) emptyRewriterSet - --- | Makes a 'RewriterSet' from all the coercion holes that occur in the --- given type. -rewriterSetFromType :: Type -> RewriterSet -rewriterSetFromType ty = appEndo (rewriter_set_from_ty ty) emptyRewriterSet - --- | Makes a 'RewriterSet' from all the coercion holes that occur in the --- given types. -rewriterSetFromTypes :: [Type] -> RewriterSet -rewriterSetFromTypes tys = appEndo (rewriter_set_from_tys tys) emptyRewriterSet - -rewriter_set_from_ty :: Type -> Endo RewriterSet -rewriter_set_from_tys :: [Type] -> Endo RewriterSet -rewriter_set_from_co :: Coercion -> Endo RewriterSet -(rewriter_set_from_ty, rewriter_set_from_tys, rewriter_set_from_co, _) - = foldTyCo folder () +isEmptyRewriterSet = coerce (isEmptyUniqSet @CoercionHole) + +addRewriter :: RewriterSet -> CoercionHole -> RewriterSet +addRewriter = coerce (addOneToUniqSet @CoercionHole) + +rewriterSetFromCts :: Bag Ct -> RewriterSet +-- Take a bag of Wanted equalities, and collect them as a RewriterSet +rewriterSetFromCts cts + = foldr add emptyRewriterSet cts where - folder :: TyCoFolder () (Endo RewriterSet) - folder = TyCoFolder - { tcf_view = noView - , tcf_tyvar = \ _ tv -> rewriter_set_from_ty (tyVarKind tv) - , tcf_covar = \ _ cv -> rewriter_set_from_ty (varType cv) - , tcf_hole = \ _ hole -> coerce (`addOneToUniqSet` hole) S.<> - rewriter_set_from_ty (varType (coHoleCoVar hole)) - , tcf_tycobinder = \ _ _ _ -> () } + add ct rw_set = case ctEvidence ct of + CtWanted { ctev_dest = HoleDest hole } -> rw_set `addRewriter` hole + _ -> rw_set {- ************************************************************************ @@ -2202,10 +2196,22 @@ TL;DR we want equality saturation. We thus want Wanteds to rewrite Wanteds in order to accept more programs, but we don't want Wanteds to rewrite Wanteds because doing so can create -inscrutable error messages. We choose to allow the rewriting, but -every Wanted tracks the set of Wanteds it has been rewritten by. This is -called a RewriterSet, stored in the ctev_rewriters field of the CtWanted -constructor of CtEvidence. (Only Wanteds have RewriterSets.) +inscrutable error messages. To solve this dilemma: + +* We allow Wanteds to rewrite Wanteds, but... + +* Each Wanted tracks the set of Wanteds it has been rewritten by, in its + RewriterSet, stored in the ctev_rewriters field of the CtWanted + constructor of CtEvidence. (Only Wanteds have RewriterSets.) + +* In error reporting, we simply suppress any errors that have been rewritten + by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, + which uses GHC.Tc.Utils.anyUnfilledCoercionHoles to look through any filled + coercion holes. The idea is that we wish to report the "root cause" -- the + error that rewrote all the others. + +* We prioritise Wanteds that have an empty RewriterSet: + see Note [Prioritise Wanteds with empty RewriterSet]. Let's continue our first example above: @@ -2219,25 +2225,72 @@ Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding The {w1} in the second line of output is the RewriterSet of w1. -A RewriterSet is just a set of unfilled CoercionHoles. This is -sufficient because only equalities (evidenced by coercion holes) are -used for rewriting; other (dictionary) constraints cannot ever -rewrite. The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks -and returns a RewriterSet, consisting of the evidence (a CoercionHole) -for any Wanted equalities used in rewriting. Then rewriteEvidence and -rewriteEqEvidence (in GHC.Tc.Solver.Canonical) add this RewriterSet to -the rewritten constraint's rewriter set. - -In error reporting, we simply suppress any errors that have been rewritten by -/unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem, which -uses GHC.Tc.Utils.anyUnfilledCoercionHoles to look through any filled coercion -holes. The idea is that we wish to report the "root cause" -- the error that -rewrote all the others. - -Wrinkle: In #22707, we have a case where all of the Wanteds have rewritten -each other. In order to report /some/ error in this case, we simply report -all the Wanteds. The user will get a perhaps-confusing error message, but -they've written a confusing program! +A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient +because only equalities (evidenced by coercion holes) are used for rewriting; +other (dictionary) constraints cannot ever rewrite. The rewriter (in +e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet, +consisting of the evidence (a CoercionHole) for any Wanted equalities used in +rewriting. Then rewriteEvidence and rewriteEqEvidence (in GHC.Tc.Solver.Canonical) +add this RewriterSet to the rewritten constraint's arewriter set. + +Note [Prioritise Wanteds with empty RewriterSet] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When extending the WorkList, in GHC.Tc.Solver.InertSet.extendWorkListEq, +we priorities constraints that have no rewriters. Here's why. + +Consider this, which came up in T22793: + inert: {} + work list: [W] co_ayf : awq ~ awo + work item: [W] co_ayb : awq ~ awp + + ==> {just put work item in inert set} + inert: co_ayb : awq ~ awp + work list: {} + work: [W] co_ayf : awq ~ awo + + ==> {rewrite ayf with co_ayb} + work list: {} + inert: co_ayb : awq ~ awp + co_aym{co_ayb} : awp ~ awo + ^ rewritten by ayb + + ----- start again in simplify_loop in Solver.hs ----- + inert: {} + work list: [W] co_ayb : awq ~ awp + work: co_aym{co_ayb} : awp ~ awo + + ==> {add to inert set} + inert: co_aym{co_ayb} : awp ~ awo + work list: {} + work: co_ayb : awq ~ awp + + ==> {rewrite co_ayb} + inert: co_aym{co_ayb} : awp ~ awo + co_ayp{co_aym} : awq ~ awo + work list: {} + +Now both wanteds have been rewriten by the other! This happened because +in our simplify_loop iteration, we happened to start with co_aym. All would have +been well if we'd started with the (not-rewritten) co_ayb and gotten it into the +inert set. + +With that in mind, we /prioritise/ the work-list to put constraints +with no rewriters first. This prioritisation is done in +GHC.Tc.Solver.InertSet.extendWorkListEq, and extendWorkListEqs. + +Wrinkles + +(WRW1) Before checking for an empty RewriterSet, we zonk the RewriterSet, + because some of those CoercionHoles may have been filled in since we last + looked: see GHC.Tc.Solver.Monad.emitWork. + +(WRW2) Despite the prioritisation, it is hard to be /certain/ that we can't end up + in a situation where all of the Wanteds have rewritten each other. In + order to report /some/ error in this case, we simply report all the + Wanteds. The user will get a perhaps-confusing error message, but they've + written a confusing program! (T22707 and T22793 were close, but they do + not exhibit this behaviour.) So belt and braces: see the `suppress` + stuff in GHC.Tc.Errors.mkErrorItem. Note [Avoiding rewriting cycles] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2416,10 +2469,11 @@ dictionaries don't appear in the original source code. -} -data CtLoc = CtLoc { ctl_origin :: CtOrigin - , ctl_env :: TcLclEnv - , ctl_t_or_k :: Maybe TypeOrKind -- OK if we're not sure - , ctl_depth :: !SubGoalDepth } +data CtLoc + = CtLoc { ctl_origin :: CtOrigin + , ctl_env :: TcLclEnv + , ctl_t_or_k :: Maybe TypeOrKind -- Used only to improve error messages + , ctl_depth :: !SubGoalDepth } -- The TcLclEnv includes particularly -- source location: tcl_loc :: RealSrcSpan @@ -2427,16 +2481,40 @@ data CtLoc = CtLoc { ctl_origin :: CtOrigin -- binder stack: tcl_bndrs :: TcBinderStack -- level: tcl_tclvl :: TcLevel -mkKindLoc :: TcType -> TcType -- original *types* being compared - -> CtLoc -> CtLoc -mkKindLoc s1 s2 loc = setCtLocOrigin (toKindLoc loc) - (KindEqOrigin s1 s2 (ctLocOrigin loc) - (ctLocTypeOrKind_maybe loc)) +mkKindEqLoc :: TcType -> TcType -- original *types* being compared + -> CtLoc -> CtLoc +mkKindEqLoc s1 s2 ctloc + | CtLoc { ctl_t_or_k = t_or_k, ctl_origin = origin } <- ctloc + = ctloc { ctl_origin = KindEqOrigin s1 s2 origin t_or_k + , ctl_t_or_k = Just KindLevel } + +adjustCtLocTyConBinder :: TyConBinder -> CtLoc -> CtLoc +-- Adjust the CtLoc when decomposing a type constructor +adjustCtLocTyConBinder tc_bndr loc + = adjustCtLoc is_vis is_kind loc + where + is_vis = isVisibleTyConBinder tc_bndr + is_kind = isNamedTyConBinder tc_bndr + +adjustCtLoc :: Bool -- True <=> A visible argument + -> Bool -- True <=> A kind argument + -> CtLoc -> CtLoc +-- Adjust the CtLoc when decomposing a type constructor, application, etc +adjustCtLoc is_vis is_kind loc + = loc2 + where + loc1 | is_kind = toKindLoc loc + | otherwise = loc + loc2 | is_vis = loc1 + | otherwise = toInvisibleLoc loc1 -- | Take a CtLoc and moves it to the kind level toKindLoc :: CtLoc -> CtLoc toKindLoc loc = loc { ctl_t_or_k = Just KindLevel } +toInvisibleLoc :: CtLoc -> CtLoc +toInvisibleLoc loc = updateCtLocOrigin loc toInvisibleOrigin + mkGivenLoc :: TcLevel -> SkolemInfoAnon -> TcLclEnv -> CtLoc mkGivenLoc tclvl skol_info env = CtLoc { ctl_origin = GivenOrigin skol_info diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs index 139d46fc98..4216613c4a 100644 --- a/compiler/GHC/Tc/Types/Evidence.hs +++ b/compiler/GHC/Tc/Types/Evidence.hs @@ -230,7 +230,7 @@ mkWpEta xs wrap = foldr eta_one wrap xs mk_wp_fun_co :: Mult -> TcCoercionR -> TcCoercionR -> TcCoercionR mk_wp_fun_co mult arg_co res_co - = mkNakedFunCo1 Representational FTF_T_T (multToCo mult) arg_co res_co + = mkNakedFunCo Representational FTF_T_T (multToCo mult) arg_co res_co -- FTF_T_T: WpFun is always (->) mkWpCastR :: TcCoercionR -> HsWrapper diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 41b48b6e71..794ef7986b 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -1000,6 +1000,11 @@ data FixedRuntimeRepOrigin -- ^ What context requires a fixed runtime representation? } +instance Outputable FixedRuntimeRepOrigin where + ppr (FixedRuntimeRepOrigin { frr_type = ty, frr_context = cxt }) + = text "FrOrigin" <> braces (vcat [ text "frr_type:" <+> ppr ty + , text "frr_context:" <+> ppr cxt ]) + -- | The context in which a representation-polymorphism check was performed. -- -- Does not include the type on which the check was performed; see diff --git a/compiler/GHC/Tc/Utils/Concrete.hs b/compiler/GHC/Tc/Utils/Concrete.hs index a07401ec74..85f79d81cf 100644 --- a/compiler/GHC/Tc/Utils/Concrete.hs +++ b/compiler/GHC/Tc/Utils/Concrete.hs @@ -521,7 +521,8 @@ ensureConcrete :: HasDebugCallStack -> TcType -> TcM TcType ensureConcrete frr_orig ty - = do { (ty', errs) <- makeTypeConcrete conc_orig ty + = do { traceTc "ensureConcrete {" (ppr frr_orig $$ ppr ty) + ; (ty', errs) <- makeTypeConcrete conc_orig ty ; case errs of { err:errs -> do { traceTc "ensureConcrete } failure" $ diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 873ff2979a..7db80cfccb 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -44,7 +44,8 @@ module GHC.Tc.Utils.TcMType ( newTcEvBinds, newNoTcEvBinds, addTcEvBind, emitNewExprHole, - newCoercionHole, fillCoercionHole, isFilledCoercionHole, + newCoercionHole, newCoercionHoleO, newVanillaCoercionHole, + fillCoercionHole, isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe, checkCoercionHole, @@ -103,7 +104,7 @@ module GHC.Tc.Utils.TcMType ( ------------------------------ -- Other - anyUnfilledCoercionHoles + zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet ) where import GHC.Prelude @@ -111,6 +112,7 @@ import GHC.Prelude import GHC.Driver.Session import qualified GHC.LanguageExtensions as LangExt +import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyInvisibleType ) import GHC.Tc.Types.Origin import GHC.Tc.Types.Constraint import GHC.Tc.Types.Evidence @@ -198,7 +200,7 @@ newEvVar ty = do { name <- newSysName (predTypeOccName ty) newWantedWithLoc :: CtLoc -> PredType -> TcM CtEvidence newWantedWithLoc loc pty = do dst <- case classifyPredType pty of - EqPred {} -> HoleDest <$> newCoercionHole pty + EqPred {} -> HoleDest <$> newCoercionHole loc pty _ -> EvVarDest <$> newEvVar pty return $ CtWanted { ctev_dest = dst , ctev_pred = pty @@ -223,9 +225,9 @@ newWanteds orig = mapM (newWanted orig Nothing) ---------------------------------------------- cloneWantedCtEv :: CtEvidence -> TcM CtEvidence -cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _ }) +cloneWantedCtEv ctev@(CtWanted { ctev_pred = pty, ctev_dest = HoleDest _, ctev_loc = loc }) | isEqPrimPred pty - = do { co_hole <- newCoercionHole pty + = do { co_hole <- newCoercionHole loc pty ; return (ctev { ctev_dest = HoleDest co_hole }) } | otherwise = pprPanic "cloneWantedCtEv" (ppr pty) @@ -273,13 +275,13 @@ emitWantedEqs origin pairs -- | Emits a new equality constraint emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion emitWantedEq origin t_or_k role ty1 ty2 - = do { hole <- newCoercionHole pty - ; loc <- getCtLocM origin (Just t_or_k) + = do { hole <- newCoercionHoleO origin pty + ; loc <- getCtLocM origin (Just t_or_k) ; emitSimple $ mkNonCanonical $ - CtWanted { ctev_pred = pty - , ctev_dest = HoleDest hole - , ctev_loc = loc - , ctev_rewriters = rewriterSetFromTypes [ty1, ty2] } + CtWanted { ctev_pred = pty + , ctev_dest = HoleDest hole + , ctev_loc = loc + , ctev_rewriters = emptyRewriterSet } ; return (HoleCo hole) } where pty = mkPrimEqPredRole role ty1 ty2 @@ -290,8 +292,8 @@ emitWantedEvVar :: CtOrigin -> TcPredType -> TcM EvVar emitWantedEvVar origin ty = do { new_cv <- newEvVar ty ; loc <- getCtLocM origin Nothing - ; let ctev = CtWanted { ctev_dest = EvVarDest new_cv - , ctev_pred = ty + ; let ctev = CtWanted { ctev_pred = ty + , ctev_dest = EvVarDest new_cv , ctev_loc = loc , ctev_rewriters = emptyRewriterSet } ; emitSimple $ mkNonCanonical ctev @@ -353,12 +355,23 @@ newImplication ************************************************************************ -} -newCoercionHole :: TcPredType -> TcM CoercionHole -newCoercionHole pred_ty +newVanillaCoercionHole :: TcPredType -> TcM CoercionHole +newVanillaCoercionHole = new_coercion_hole False + +newCoercionHole :: CtLoc -> TcPredType -> TcM CoercionHole +newCoercionHole loc = newCoercionHoleO (ctLocOrigin loc) + +newCoercionHoleO :: CtOrigin -> TcPredType -> TcM CoercionHole +newCoercionHoleO (KindEqOrigin {}) = new_coercion_hole True +newCoercionHoleO _ = new_coercion_hole False + +new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole +new_coercion_hole hetero_kind pred_ty = do { co_var <- newEvVar pred_ty ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty) ; ref <- newMutVar Nothing - ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } + ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref + , ch_hetero_kind = hetero_kind } } -- | Put a value in a coercion hole fillCoercionHole :: CoercionHole -> Coercion -> TcM () @@ -621,12 +634,7 @@ ensureMonoType res_ty = return () | otherwise = do { mono_ty <- newOpenFlexiTyVarTy - ; let eq_orig = TypeEqOrigin { uo_actual = res_ty - , uo_expected = mono_ty - , uo_thing = Nothing - , uo_visible = False } - - ; _co <- emitWantedEq eq_orig TypeLevel Nominal res_ty mono_ty + ; _co <- unifyInvisibleType res_ty mono_ty ; return () } promoteTcType :: TcLevel -> TcType -> TcM (TcCoercionN, TcType) @@ -652,12 +660,7 @@ promoteTcType dest_lvl ty -- where alpha and rr are fresh and from level dest_lvl = do { rr <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (mkTYPEapp rr) - ; let eq_orig = TypeEqOrigin { uo_actual = ty - , uo_expected = prom_ty - , uo_thing = Nothing - , uo_visible = False } - - ; co <- emitWantedEq eq_orig TypeLevel Nominal ty prom_ty + ; co <- unifyInvisibleType ty prom_ty ; return (co, prom_ty) } {- Note [Promoting a type] @@ -2471,8 +2474,7 @@ zonkCt ct zonkCtEvidence :: CtEvidence -> TcM CtEvidence zonkCtEvidence ctev = do { pred' <- zonkTcType (ctev_pred ctev) - ; return (setCtEvPredType ctev pred') - } + ; return (setCtEvPredType ctev pred') } zonkSkolemInfo :: SkolemInfo -> TcM SkolemInfo zonkSkolemInfo (SkolemInfo u sk) = SkolemInfo u <$> zonkSkolemInfoAnon sk @@ -2788,23 +2790,43 @@ naughtyQuantification orig_ty tv escapees ************************************************************************ -} +zonkCtRewriterSet :: Ct -> TcM Ct +zonkCtRewriterSet ct + | isGiven ev = return ct + | otherwise + = case ct of + CQuantCan {} -> return ct + CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev + ; return (CEqCan (eq { eq_ev = ev' })) } + _ -> do { ev' <- zonkCtEvRewriterSet ev + ; return (ct { cc_ev = ev' }) } + where + ev = ctEvidence ct + +zonkCtEvRewriterSet :: CtEvidence -> TcM CtEvidence +zonkCtEvRewriterSet ev@(CtGiven {}) + = return ev +zonkCtEvRewriterSet ev@(CtWanted { ctev_rewriters = rewriters }) + = do { rewriters' <- zonkRewriterSet rewriters + ; return (ev { ctev_rewriters = rewriters' }) } + -- | Check whether any coercion hole in a RewriterSet is still unsolved. -- Does this by recursively looking through filled coercion holes until -- one is found that is not yet filled in, at which point this aborts. -anyUnfilledCoercionHoles :: RewriterSet -> TcM Bool -anyUnfilledCoercionHoles (RewriterSet set) - = nonDetStrictFoldUniqSet go (return False) set +zonkRewriterSet :: RewriterSet -> TcM RewriterSet +zonkRewriterSet (RewriterSet set) + = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set -- this does not introduce non-determinism, because the only -- monadic action is to read, and the combining function is -- commutative where - go :: CoercionHole -> TcM Bool -> TcM Bool - go hole m_acc = m_acc <||> check_hole hole + go :: CoercionHole -> TcM RewriterSet -> TcM RewriterSet + go hole m_acc = unionRewriterSet <$> (check_hole hole) <*> m_acc - check_hole :: CoercionHole -> TcM Bool + check_hole :: CoercionHole -> TcM RewriterSet check_hole hole = do { m_co <- unpackCoercionHole_maybe hole ; case m_co of - Nothing -> return True -- unfilled hole + Nothing -> return (unitRewriterSet hole) Just co -> unUCHM (check_co co) } check_ty :: Type -> UnfilledCoercionHoleMonoid @@ -2818,10 +2840,10 @@ anyUnfilledCoercionHoles (RewriterSet set) , tcf_hole = \ _ -> UCHM . check_hole , tcf_tycobinder = \ _ _ _ -> () } -newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM Bool } +newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: TcM RewriterSet } instance Semigroup UnfilledCoercionHoleMonoid where - UCHM l <> UCHM r = UCHM (l <||> r) + UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r) instance Monoid UnfilledCoercionHoleMonoid where - mempty = UCHM (return False) + mempty = UCHM (return emptyRewriterSet) diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index 1a03cd1c4b..ae25678600 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -205,7 +205,7 @@ module GHC.Tc.Utils.TcType ( --------------------------------- -- argument visibility - tcTyConVisibilities, isNextTyConArgVisible, isNextArgVisible + tyConVisibilities, isNextTyConArgVisible, isNextArgVisible ) where @@ -2307,8 +2307,8 @@ Reason: the back end falls over with panic "primRepHint:VoidRep"; -- | For every arg a tycon can take, the returned list says True if the argument -- is taken visibly, and False otherwise. Ends with an infinite tail of Trues to -- allow for oversaturation. -tcTyConVisibilities :: TyCon -> [Bool] -tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True +tyConVisibilities :: TyCon -> [Bool] +tyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True where tc_binder_viss = map isVisibleTyConBinder (tyConBinders tc) tc_return_kind_viss = map isVisiblePiTyBinder (fst $ tcSplitPiTys (tyConResKind tc)) @@ -2316,13 +2316,14 @@ tcTyConVisibilities tc = tc_binder_viss ++ tc_return_kind_viss ++ repeat True -- | If the tycon is applied to the types, is the next argument visible? isNextTyConArgVisible :: TyCon -> [Type] -> Bool isNextTyConArgVisible tc tys - = tcTyConVisibilities tc `getNth` length tys + = tyConVisibilities tc `getNth` length tys -- | Should this type be applied to a visible argument? +-- E.g. (s t): is `t` a visible argument of `s`? isNextArgVisible :: TcType -> Bool isNextArgVisible ty - | Just (bndr, _) <- tcSplitPiTy_maybe ty = isVisiblePiTyBinder bndr - | otherwise = True + | Just (bndr, _) <- tcSplitPiTy_maybe (typeKind ty) = isVisiblePiTyBinder bndr + | otherwise = True -- this second case might happen if, say, we have an unzonked TauTv. -- But TauTvs can't range over types that take invisible arguments diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index fc5728cc81..428eba5d69 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -20,9 +20,11 @@ module GHC.Tc.Utils.Unify ( buildImplicationFor, buildTvImplication, emitResidualTvConstraint, -- Various unifications - unifyType, unifyKind, unifyExpectedType, - uType, promoteTcType, + unifyType, unifyKind, unifyInvisibleType, unifyExpectedType, + unifyTypeAndEmit, promoteTcType, swapOverTyVars, touchabilityAndShapeTest, + UnifyEnv(..), updUEnvLoc, setUEnvRole, + uType, -------------------------------- -- Holes @@ -1145,7 +1147,7 @@ tcEqMult origin w_actual w_expected = do { -- Note that here we do not call to `submult`, so we check -- for strict equality. - ; coercion <- uType TypeLevel origin w_actual w_expected + ; coercion <- unifyTypeAndEmit TypeLevel origin w_actual w_expected ; return $ if isReflCo coercion then WpHole else WpMultCoercion coercion } @@ -1711,18 +1713,30 @@ unifyType :: Maybe TypedThing -- ^ If present, the thing that has type ty1 -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 unifyType thing ty1 ty2 - = uType TypeLevel origin ty1 ty2 + = unifyTypeAndEmit TypeLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1 , uo_expected = ty2 , uo_thing = thing , uo_visible = True } +unifyInvisibleType :: TcTauType -> TcTauType -- ty1 (actual), ty2 (expected) + -> TcM TcCoercionN -- :: ty1 ~# ty2 +-- Actual and expected types +-- Returns a coercion : ty1 ~ ty2 +unifyInvisibleType ty1 ty2 + = unifyTypeAndEmit TypeLevel origin ty1 ty2 + where + origin = TypeEqOrigin { uo_actual = ty1 + , uo_expected = ty2 + , uo_thing = Nothing + , uo_visible = False } -- This is the "invisible" bit + unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN -- Like unifyType, but swap expected and actual in error messages -- This is used when typechecking patterns unifyTypeET ty1 ty2 - = uType TypeLevel origin ty1 ty2 + = unifyTypeAndEmit TypeLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty2 -- NB swapped , uo_expected = ty1 -- NB swapped @@ -1732,13 +1746,28 @@ unifyTypeET ty1 ty2 unifyKind :: Maybe TypedThing -> TcKind -> TcKind -> TcM CoercionN unifyKind mb_thing ty1 ty2 - = uType KindLevel origin ty1 ty2 + = unifyTypeAndEmit KindLevel origin ty1 ty2 where origin = TypeEqOrigin { uo_actual = ty1 , uo_expected = ty2 , uo_thing = mb_thing , uo_visible = True } +unifyTypeAndEmit :: TypeOrKind -> CtOrigin -> TcType -> TcType -> TcM CoercionN +-- Make a ref-cell, unify, emit the collected constraints +unifyTypeAndEmit t_or_k orig ty1 ty2 + = do { ref <- newTcRef emptyBag + ; loc <- getCtLocM orig (Just t_or_k) + ; let env = UE { u_loc = loc, u_role = Nominal + , u_rewriters = emptyRewriterSet -- ToDo: check this + , u_defer = ref, u_unified = Nothing } + + -- The hard work happens here + ; co <- uType env ty1 ty2 + + ; cts <- readTcRef ref + ; unless (null cts) (emitSimples cts) + ; return co } {- %************************************************************************ @@ -1747,45 +1776,110 @@ unifyKind mb_thing ty1 ty2 %* * %************************************************************************ -uType is the heart of the unifier. +Note [The eager unifier] +~~~~~~~~~~~~~~~~~~~~~~~~ +The eager unifier, `uType`, is called by + + * The constraint generator (e.g. in GHC.Tc.Gen.Expr), + via the wrappers `unifyType`, `unifyKind` etc + + * The constraint solver (e.g. in GHC.Tc.Solver.Equality), + via `GHC.Tc.Solver.Monad.wrapUnifierTcS`. + +`uType` runs in the TcM monad, but it carries a UnifyEnv that tells it +what to do when unifying a variable or deferring a constraint. Specifically, + * it collects deferred constraints in `u_defer`, and + * it records which unification variables it has unified in `u_unified` +Then it is up to the wrappers (one for the constraint generator, one for +the constraint solver) to deal with these collected sets. + +Although `uType` runs in the TcM monad for convenience, really it could +operate just with the ability to + * write to the accumulators of deferred constraints + and unification variables in UnifyEnv. + * read and update existing unification variables + * zonk types befire unifying (`zonkTcType` in `uUnfilledVar`, and + `zonkTyCoVarKind` in `uUnfilledVar1` + * create fresh coercion holes (`newCoercionHole`) + * emit tracing info for debugging + * look at the ambient TcLevel: `getTcLevel` +A job for the future. -} +data UnifyEnv + = UE { u_role :: Role + , u_loc :: CtLoc + , u_rewriters :: RewriterSet + + -- Deferred constraints + , u_defer :: TcRef (Bag Ct) + + -- Which variables are unified; + -- if Nothing, we don't care + , u_unified :: Maybe (TcRef [TcTyVar]) + } + +setUEnvRole :: UnifyEnv -> Role -> UnifyEnv +setUEnvRole uenv role = uenv { u_role = role } + +updUEnvLoc :: UnifyEnv -> (CtLoc -> CtLoc) -> UnifyEnv +updUEnvLoc uenv@(UE { u_loc = loc }) upd = uenv { u_loc = upd loc } + +mkKindEnv :: UnifyEnv -> TcType -> TcType -> UnifyEnv +-- Modify the UnifyEnv to be right for unifing +-- the kinds of these two types +mkKindEnv env@(UE { u_loc = ctloc }) ty1 ty2 + = env { u_role = Nominal, u_loc = mkKindEqLoc ty1 ty2 ctloc } + uType, uType_defer - :: TypeOrKind - -> CtOrigin + :: UnifyEnv -> TcType -- ty1 is the *actual* type -> TcType -- ty2 is the *expected* type -> TcM CoercionN --------------- -- It is always safe to defer unification to the main constraint solver -- See Note [Deferred unification] --- ty1 is "actual" --- ty2 is "expected" -uType_defer t_or_k origin ty1 ty2 - = do { co <- emitWantedEq origin t_or_k Nominal ty1 ty2 +uType_defer (UE { u_loc = loc, u_defer = ref + , u_role = role, u_rewriters = rewriters }) + ty1 ty2 -- ty1 is "actual", ty2 is "expected" + = do { let pred_ty = mkPrimEqPredRole role ty1 ty2 + ; hole <- newCoercionHole loc pred_ty + ; let ct = mkNonCanonical $ + CtWanted { ctev_pred = pred_ty + , ctev_dest = HoleDest hole + , ctev_loc = loc + , ctev_rewriters = rewriters } + co = HoleCo hole + ; updTcRef ref (`snocBag` ct) + -- snocBag: see Note [Work-list ordering] in GHC.Tc.Solver.Equality -- Error trace only -- NB. do *not* call mkErrInfo unless tracing is on, -- because it is hugely expensive (#5631) - ; whenDOptM Opt_D_dump_tc_trace $ do - { ctxt <- getErrCtxt - ; doc <- mkErrInfo emptyTidyEnv ctxt - ; traceTc "utype_defer" (vcat [ debugPprType ty1 + ; whenDOptM Opt_D_dump_tc_trace $ + do { ctxt <- getErrCtxt + ; doc <- mkErrInfo emptyTidyEnv ctxt + ; traceTc "utype_defer" (vcat [ ppr role + , debugPprType ty1 , debugPprType ty2 - , pprCtOrigin origin , doc]) - ; traceTc "utype_defer2" (ppr co) - } + ; traceTc "utype_defer2" (ppr co) } + ; return co } + -------------- -uType t_or_k origin orig_ty1 orig_ty2 +uType env@(UE { u_role = role }) orig_ty1 orig_ty2 + | Phantom <- role + = do { kind_co <- uType (mkKindEnv env orig_ty1 orig_ty2) + (typeKind orig_ty1) (typeKind orig_ty2) + ; return (mkPhantomCo kind_co orig_ty1 orig_ty2) } + + | otherwise = do { tclvl <- getTcLevel ; traceTc "u_tys" $ vcat [ text "tclvl" <+> ppr tclvl - , sep [ ppr orig_ty1, text "~", ppr orig_ty2] - , pprCtOrigin origin] + , sep [ ppr orig_ty1, text "~" <> ppr role, ppr orig_ty2] ] ; co <- go orig_ty1 orig_ty2 ; if isReflCo co then traceTc "u_tys yields no coercion" Outputable.empty @@ -1800,12 +1894,12 @@ uType t_or_k origin orig_ty1 orig_ty2 -- recognize (t |> co) ~ (t |> co), which is nice. Previously, we -- didn't do it this way, and then the unification above was deferred. go (CastTy t1 co1) t2 - = do { co_tys <- uType t_or_k origin t1 t2 - ; return (mkCoherenceLeftCo Nominal t1 co1 co_tys) } + = do { co_tys <- uType env t1 t2 + ; return (mkCoherenceLeftCo role t1 co1 co_tys) } go t1 (CastTy t2 co2) - = do { co_tys <- uType t_or_k origin t1 t2 - ; return (mkCoherenceRightCo Nominal t2 co2 co_tys) } + = do { co_tys <- uType env t1 t2 + ; return (mkCoherenceRightCo role t2 co2 co_tys) } -- Variables; go for uUnfilledVar -- Note that we pass in *original* (before synonym expansion), @@ -1815,19 +1909,20 @@ uType t_or_k origin orig_ty1 orig_ty2 = do { lookup_res <- isFilledMetaTyVar_maybe tv1 ; case lookup_res of Just ty1 -> do { traceTc "found filled tyvar" (ppr tv1 <+> text ":->" <+> ppr ty1) - ; go ty1 ty2 } - Nothing -> uUnfilledVar origin t_or_k NotSwapped tv1 ty2 } + ; uType env ty1 orig_ty2 } + Nothing -> uUnfilledVar env NotSwapped tv1 ty2 } + go ty1 (TyVarTy tv2) = do { lookup_res <- isFilledMetaTyVar_maybe tv2 ; case lookup_res of Just ty2 -> do { traceTc "found filled tyvar" (ppr tv2 <+> text ":->" <+> ppr ty2) - ; go ty1 ty2 } - Nothing -> uUnfilledVar origin t_or_k IsSwapped tv2 ty1 } + ; uType env orig_ty1 ty2 } + Nothing -> uUnfilledVar env IsSwapped tv2 ty1 } -- See Note [Expanding synonyms during unification] go ty1@(TyConApp tc1 []) (TyConApp tc2 []) | tc1 == tc2 - = return $ mkNomReflCo ty1 + = return $ mkReflCo role ty1 -- See Note [Expanding synonyms during unification] -- @@ -1842,14 +1937,14 @@ uType t_or_k origin orig_ty1 orig_ty2 | Just ty2' <- coreView ty2 = go ty1 ty2' -- Functions (t1 -> t2) just check the two parts - -- Do not attempt (c => t); just defer go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = arg1, ft_res = res1 }) (FunTy { ft_af = af2, ft_mult = w2, ft_arg = arg2, ft_res = res2 }) - | isVisibleFunArg af1, af1 == af2 - = do { co_l <- uType t_or_k origin arg1 arg2 - ; co_r <- uType t_or_k origin res1 res2 - ; co_w <- uType t_or_k origin w1 w2 - ; return $ mkNakedFunCo1 Nominal af1 co_w co_l co_r } + | isVisibleFunArg af1 -- Do not attempt (c => t); just defer + , af1 == af2 -- Important! See #21530 + = do { co_w <- uType (env { u_role = funRole role SelMult }) w1 w2 + ; co_l <- uType (env { u_role = funRole role SelArg }) arg1 arg2 + ; co_r <- uType (env { u_role = funRole role SelRes }) res1 res2 + ; return $ mkNakedFunCo role af1 co_w co_l co_r } -- Always defer if a type synonym family (type function) -- is involved. (Data families behave rigidly.) @@ -1861,41 +1956,40 @@ uType t_or_k origin orig_ty1 orig_ty2 go (TyConApp tc1 tys1) (TyConApp tc2 tys2) -- See Note [Mismatched type lists and application decomposition] | tc1 == tc2, equalLength tys1 tys2 - = assertPpr (isGenerativeTyCon tc1 Nominal) (ppr tc1) $ - do { cos <- zipWith3M (uType t_or_k) origins' tys1 tys2 - ; return $ mkTyConAppCo Nominal tc1 cos } - where - origins' = map (\is_vis -> if is_vis then origin else toInvisibleOrigin origin) - (tcTyConVisibilities tc1) + , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality + = assertPpr (isGenerativeTyCon tc1 role) (ppr tc1) $ + do { traceTc "go-tycon" (ppr tc1 $$ ppr tys1 $$ ppr tys2 $$ ppr (take 10 (tyConRoleListX role tc1))) + ; cos <- zipWith4M u_tc_arg (tyConVisibilities tc1) -- Infinite + (tyConRoleListX role tc1) -- Infinite + tys1 tys2 + ; return $ mkTyConAppCo role tc1 cos } go (LitTy m) ty@(LitTy n) | m == n - = return $ mkNomReflCo ty + = return $ mkReflCo role ty -- See Note [Care with type applications] -- Do not decompose FunTy against App; -- it's often a type error, so leave it for the constraint solver - go (AppTy s1 t1) (AppTy s2 t2) - = go_app (isNextArgVisible s1) s1 t1 s2 t2 + go ty1@(AppTy s1 t1) ty2@(AppTy s2 t2) + = go_app (isNextArgVisible s1) ty1 s1 t1 ty2 s2 t2 - go (AppTy s1 t1) (TyConApp tc2 ts2) + go ty1@(AppTy s1 t1) ty2@(TyConApp tc2 ts2) | Just (ts2', t2') <- snocView ts2 = assert (not (tyConMustBeSaturated tc2)) $ - go_app (isNextTyConArgVisible tc2 ts2') s1 t1 (TyConApp tc2 ts2') t2' + go_app (isNextTyConArgVisible tc2 ts2') + ty1 s1 t1 ty2 (TyConApp tc2 ts2') t2' - go (TyConApp tc1 ts1) (AppTy s2 t2) + go ty1@(TyConApp tc1 ts1) ty2@(AppTy s2 t2) | Just (ts1', t1') <- snocView ts1 = assert (not (tyConMustBeSaturated tc1)) $ - go_app (isNextTyConArgVisible tc1 ts1') (TyConApp tc1 ts1') t1' s2 t2 + go_app (isNextTyConArgVisible tc1 ts1') + ty1 (TyConApp tc1 ts1') t1' ty2 s2 t2 - go (CoercionTy co1) (CoercionTy co2) - = do { let ty1 = coercionType co1 - ty2 = coercionType co2 - ; kco <- uType KindLevel - (KindEqOrigin orig_ty1 orig_ty2 origin - (Just t_or_k)) - ty1 ty2 - ; return $ mkProofIrrelCo Nominal kco co1 co2 } + go ty1@(CoercionTy co1) ty2@(CoercionTy co2) + = do { kco <- uType (mkKindEnv env ty1 ty2) + (coercionType co1) (coercionType co2) + ; return $ mkProofIrrelCo role kco co1 co2 } -- Anything else fails -- E.g. unifying for-all types, which is relative unusual @@ -1903,17 +1997,33 @@ uType t_or_k origin orig_ty1 orig_ty2 ------------------ defer ty1 ty2 -- See Note [Check for equality before deferring] - | ty1 `tcEqType` ty2 = return (mkNomReflCo ty1) - | otherwise = uType_defer t_or_k origin ty1 ty2 + | ty1 `tcEqType` ty2 = return (mkReflCo role ty1) + | otherwise = uType_defer env orig_ty1 orig_ty2 + ------------------ - go_app vis s1 t1 s2 t2 - = do { co_s <- uType t_or_k origin s1 s2 - ; let arg_origin - | vis = origin - | otherwise = toInvisibleOrigin origin - ; co_t <- uType t_or_k arg_origin t1 t2 + u_tc_arg is_vis role ty1 ty2 + = do { traceTc "u_tc_arg" (ppr role $$ ppr ty1 $$ ppr ty2) + ; uType env_arg ty1 ty2 } + where + env_arg = env { u_loc = adjustCtLoc is_vis False (u_loc env) + , u_role = role } + + ------------------ + -- For AppTy, decompose only nominal equalities + -- See Note [Decomposing AppTy equalities] in GHC.Tc.Solver.Equality + go_app vis ty1 s1 t1 ty2 s2 t2 + | Nominal <- role + = -- Unify arguments t1/t2 before function s1/s2, because + -- the former have smaller kinds, and hence simpler error messages + -- c.f. GHC.Tc.Solver.Equality.can_eq_app + -- Example: test T8603 + do { let env_arg = env { u_loc = adjustCtLoc vis False (u_loc env) } + ; co_t <- uType env_arg t1 t2 + ; co_s <- uType env s1 s2 ; return $ mkAppCo co_s co_t } + | otherwise + = defer ty1 ty2 {- Note [Check for equality before deferring] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2009,38 +2119,35 @@ back into @uTys@ if it turns out that the variable is already bound. -} ---------- -uUnfilledVar :: CtOrigin - -> TypeOrKind - -> SwapFlag - -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar - -- definitely not a /filled/ meta-tyvar - -> TcTauType -- Type 2 - -> TcM Coercion +uUnfilledVar, uUnfilledVar1 + :: UnifyEnv + -> SwapFlag + -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar + -- definitely not a /filled/ meta-tyvar + -> TcTauType -- Type 2 + -> TcM CoercionN -- "Unfilled" means that the variable is definitely not a filled-in meta tyvar -- It might be a skolem, or untouchable, or meta - -uUnfilledVar origin t_or_k swapped tv1 ty2 - = do { ty2 <- zonkTcType ty2 - -- Zonk to expose things to the - -- occurs check, and so that if ty2 - -- looks like a type variable then it - -- /is/ a type variable - ; uUnfilledVar1 origin t_or_k swapped tv1 ty2 } - ----------- -uUnfilledVar1 :: CtOrigin - -> TypeOrKind - -> SwapFlag - -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar - -- definitely not a /filled/ meta-tyvar - -> TcTauType -- Type 2, zonked - -> TcM Coercion -uUnfilledVar1 origin t_or_k swapped tv1 ty2 +uUnfilledVar env swapped tv1 ty2 + | Nominal <- u_role env + = do { ty2 <- zonkTcType ty2 -- Zonk to expose things to the occurs check, and so + -- that if ty2 looks like a type variable then it + -- /is/ a type variable + ; uUnfilledVar1 env swapped tv1 ty2 } + + | otherwise -- See Note [Do not unify representational equalities] + -- in GHC.Tc.Solver.Equality + = unSwap swapped (uType_defer env) (mkTyVarTy tv1) ty2 + +uUnfilledVar1 env -- Precondition: u_role==Nominal + swapped + tv1 + ty2 -- ty2 is zonked | Just tv2 <- getTyVar_maybe ty2 = go tv2 | otherwise - = uUnfilledVar2 origin t_or_k swapped tv1 ty2 + = uUnfilledVar2 env swapped tv1 ty2 where -- 'go' handles the case where both are @@ -2056,21 +2163,19 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2 -- not have happened yet, and it's an invariant of -- uUnfilledTyVar2 that ty2 is fully zonked -- Omitting this caused #16902 - ; uUnfilledVar2 origin t_or_k (flipSwap swapped) - tv2 (mkTyVarTy tv1) } + ; uUnfilledVar2 env (flipSwap swapped) tv2 (mkTyVarTy tv1) } | otherwise - = uUnfilledVar2 origin t_or_k swapped tv1 ty2 + = uUnfilledVar2 env swapped tv1 ty2 ---------- -uUnfilledVar2 :: CtOrigin - -> TypeOrKind +uUnfilledVar2 :: UnifyEnv -- Precondition: u_role==Nominal -> SwapFlag -> TcTyVar -- Tyvar 1: not necessarily a meta-tyvar -- definitely not a /filled/ meta-tyvar -> TcTauType -- Type 2, zonked - -> TcM Coercion -uUnfilledVar2 origin t_or_k swapped tv1 ty2 + -> TcM CoercionN +uUnfilledVar2 env@(UE { u_defer = def_eq_ref }) swapped tv1 ty2 = do { cur_lvl <- getTcLevel -- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles -- Here we don't know about given equalities here; so we treat @@ -2079,7 +2184,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 && simpleUnifyCheck False tv1 ty2) then not_ok_so_defer else - do { co_k <- uType KindLevel kind_origin (typeKind ty2) (tyVarKind tv1) + do { def_eqs <- readTcRef def_eq_ref -- Capture current state of def_eqs + + -- Attempt to unify kinds + ; co_k <- uType (mkKindEnv env ty1 ty2) (typeKind ty2) (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) , ppr ty2 <+> dcolon <+> ppr (typeKind ty2) @@ -2090,17 +2198,22 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 -- NB: tv1 should still be unfilled, despite the kind unification -- because tv1 is not free in ty2' (or, hence, in its kind) then do { writeMetaTyVar tv1 ty2 - ; return (mkNomReflCo ty2) } - - else defer -- This cannot be solved now. See GHC.Tc.Solver.Canonical - -- Note [Equalities with incompatible kinds] for how - -- this will be dealt with in the solver + ; case u_unified env of + Nothing -> return () + Just uref -> updTcRef uref (tv1 :) + ; return (mkNomReflCo ty2) } -- Unification is always Nominal + + else -- The kinds don't match yet, so give up defer instead. + do { writeTcRef def_eq_ref def_eqs + -- Since we are discarding co_k, also discard any constraints + -- emitted by kind unification; they are just useless clutter. + -- Do this dicarding by simply restoring the previous state + -- of def_eqs; a bit imperative/yukky but works fine. + ; defer } }} where ty1 = mkTyVarTy tv1 - kind_origin = KindEqOrigin ty1 ty2 origin (Just t_or_k) - - defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 + defer = unSwap swapped (uType_defer env) ty1 ty2 not_ok_so_defer = do { traceTc "uUnfilledVar2 not ok" (ppr tv1 $$ ppr ty2) @@ -2219,18 +2332,10 @@ There are five reasons not to unify: 5. (COERCION-HOLE) Confusing coercion holes Suppose our equality is (alpha :: k) ~ (Int |> {co}) - where co :: Type ~ k is an unsolved wanted. Note that this - equality is homogeneous; both sides have kind k. Unifying here - is sensible, but it can lead to very confusing error messages. - It's very much like a Wanted rewriting a Wanted. Even worse, - unifying a variable essentially turns an equality into a Given, - and so we could not use the tracking mechanism in - Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. - We thus simply do not unify in this case. - - This is expanded as Wrinkle (2) in Note [Equalities with incompatible kinds] - in GHC.Tc.Solver.Equality - + where co :: Type ~ k is an unsolved wanted. Note that this equality + is homogeneous; both sides have kind k. We refrain from unifying here, because + of the coercion hole in the RHS -- see Wrinkle (EIK2) in + Note [Equalities with incompatible kinds] in GHC.Solver.Equality. Needless to say, all there are wrinkles: @@ -2500,7 +2605,7 @@ matchExpectedFunKind hs_ty n k = go n k go n (FunTy { ft_af = af, ft_mult = w, ft_arg = arg, ft_res = res }) | isVisibleFunArg af = do { co <- go (n-1) res - ; return (mkNakedFunCo1 Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) } + ; return (mkNakedFunCo Nominal af (mkNomReflCo w) (mkNomReflCo arg) co) } go n other = defer n other @@ -2514,7 +2619,7 @@ matchExpectedFunKind hs_ty n k = go n k , uo_thing = Just hs_ty , uo_visible = True } - ; uType KindLevel origin k new_fun } + ; unifyTypeAndEmit KindLevel origin k new_fun } {- ********************************************************************* * * @@ -2523,40 +2628,6 @@ matchExpectedFunKind hs_ty n k = go n k * * ********************************************************************* -} -{- Commented out because I think we can just use the simple, - efficient simpleUnifyCheck instead; we can always defer. - -uTypeCheckTouchableTyVarEq :: TcTyVar -> TcType -> TcM (PuResult () TcType) --- The check may expand type synonyms to avoid an occurs check, --- so we must use the return type --- --- Precondition: rhs is fully zonked -uTypeCheckTouchableTyVarEq lhs_tv rhs - | simpleUnifyCheck False lhs_tv rhs -- Do a fast-path check - -- False <=> See Note [Prevent unification with type families] - = return (pure rhs) - - | otherwise - = do { traceTc "uTypeCheckTouchableTyVarEq {" (pprTyVar lhs_tv $$ ppr rhs) - ; check_result <- checkTyEqRhs flags rhs :: TcM (PuResult () Reduction) - ; traceTc "uTypeCheckTouchableTyVarEq }" (ppr check_result) - ; case check_result of - PuFail reason -> return (PuFail reason) - PuOK redn _ -> assertPpr (isReflCo (reductionCoercion redn)) - (ppr lhs_tv $$ ppr rhs $$ ppr redn) $ - return (pure (reductionReducedType redn)) } - where - flags | MetaTv { mtv_info = tv_info, mtv_tclvl = tv_lvl } <- tcTyVarDetails lhs_tv - = TEF { tef_foralls = isRuntimeUnkSkol lhs_tv - , tef_fam_app = TEFA_Fail - , tef_unifying = Unifying tv_info tv_lvl LC_None - , tef_lhs = TyVarLHS lhs_tv - , tef_occurs = cteInsolubleOccurs } - | otherwise - = pprPanic "uTypeCheckTouchableTyVarEq" (ppr lhs_tv) - -- TEFA_Fail: See Note [Prevent unification with type families] --} - simpleUnifyCheck :: Bool -> TcTyVar -> TcType -> Bool -- A fast check: True <=> unification is OK -- If it says 'False' then unification might still be OK, but @@ -2690,22 +2761,22 @@ reductionCoercion is Refl. See `canEqCanLHSFinish_no_unification`. -} data PuResult a b = PuFail CheckTyEqResult - | PuOK b (Bag a) + | PuOK (Bag a) b instance Functor (PuResult a) where fmap _ (PuFail prob) = PuFail prob - fmap f (PuOK x cts) = PuOK (f x) cts + fmap f (PuOK cts x) = PuOK cts (f x) instance Applicative (PuResult a) where - pure x = PuOK x emptyBag + pure x = PuOK emptyBag x PuFail p1 <*> PuFail p2 = PuFail (p1 S.<> p2) PuFail p1 <*> PuOK {} = PuFail p1 PuOK {} <*> PuFail p2 = PuFail p2 - PuOK f c1 <*> PuOK x c2 = PuOK (f x) (c1 `unionBags` c2) + PuOK c1 f <*> PuOK c2 x = PuOK (c1 `unionBags` c2) (f x) instance (Outputable a, Outputable b) => Outputable (PuResult a b) where ppr (PuFail prob) = text "PuFail" <+> (ppr prob) - ppr (PuOK x cts) = text "PuOK" <> braces + ppr (PuOK cts x) = text "PuOK" <> braces (vcat [ text "redn:" <+> ppr x , text "cts:" <+> ppr cts ]) @@ -2715,7 +2786,7 @@ pprPur (PuFail prob) = text "PuFail:" <> ppr prob pprPur (PuOK {}) = text "PuOK" okCheckRefl :: TcType -> TcM (PuResult a Reduction) -okCheckRefl ty = return (PuOK (mkReflRedn Nominal ty) emptyBag) +okCheckRefl ty = return (PuOK emptyBag (mkReflRedn Nominal ty)) failCheckWith :: CheckTyEqResult -> TcM (PuResult a b) failCheckWith p = return (PuFail p) @@ -2851,15 +2922,14 @@ checkTyEqRhs flags ty checkCo :: TyEqFlags a -> Coercion -> TcM (PuResult a Coercion) -- See Note [checkCo] checkCo (TEF { tef_lhs = TyFamLHS {} }) co - = return (PuOK co emptyBag) + = return (pure co) checkCo (TEF { tef_lhs = TyVarLHS lhs_tv , tef_unifying = unifying , tef_occurs = occ_prob }) co -- Check for coercion holes, if unifying -- See (COERCION-HOLE) in Note [Unification preconditions] - | Unifying {} <- unifying - , hasCoercionHoleCo co + | hasCoercionHoleCo co = failCheckWith (cteProblem cteCoercionHole) -- Occurs check (can promote) @@ -2874,7 +2944,7 @@ checkCo (TEF { tef_lhs = TyVarLHS lhs_tv = failCheckWith (cteProblem occ_prob) | otherwise - = return (PuOK co emptyBag) + = return (pure co) {- Note [checkCo] ~~~~~~~~~~~~~~~~~ @@ -3058,7 +3128,7 @@ checkFamApp flags@(TEF { tef_unifying = unifying, tef_occurs = occ_prob TEFA_Break breaker -- Recurse; and break if there is a problem -> do { tys_res <- mapCheck (checkTyEqRhs arg_flags) tys ; case tys_res of - PuOK redns cts -> return (PuOK (mkTyConAppRedn Nominal tc redns) cts) + PuOK cts redns -> return (PuOK cts (mkTyConAppRedn Nominal tc redns)) PuFail {} -> breaker fam_app } where arg_flags = famAppArgFlags flags @@ -3228,4 +3298,3 @@ checkTopShape info xi _ -> False CycleBreakerTv -> False -- We never unify these _ -> True - diff --git a/compiler/GHC/Tc/Utils/Unify.hs-boot b/compiler/GHC/Tc/Utils/Unify.hs-boot index 0d82ea613e..9b75cea113 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs-boot +++ b/compiler/GHC/Tc/Utils/Unify.hs-boot @@ -9,8 +9,9 @@ import GHC.Tc.Types.Origin ( CtOrigin, TypedThing ) -- This boot file exists only to tie the knot between --- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate +-- GHC.Tc.Utils.Unify and GHC.Tc.Utils.Instantiate/GHC.Tc.Utils.TcMType -unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion +unifyType :: Maybe TypedThing -> TcTauType -> TcTauType -> TcM TcCoercion +unifyInvisibleType :: TcTauType -> TcTauType -> TcM TcCoercion tcSubMult :: CtOrigin -> Mult -> Mult -> TcM HsWrapper diff --git a/testsuite/tests/dependent/should_fail/T11471.hs b/testsuite/tests/dependent/should_fail/T11471.hs index ae09ae07bb..f9bc764f88 100644 --- a/testsuite/tests/dependent/should_fail/T11471.hs +++ b/testsuite/tests/dependent/should_fail/T11471.hs @@ -4,12 +4,14 @@ module T11471 where import GHC.Exts import Data.Proxy +import Data.Kind type family F a :: k type instance F Int = Int# -f :: Proxy a -> F a -> F a +f :: forall (a :: Type). Proxy a -> F a -> F a +-- NB: Those calls to F are (F @Type a) f _ x = x bad = f (undefined :: Proxy Int#) 3# diff --git a/testsuite/tests/dependent/should_fail/T11471.stderr b/testsuite/tests/dependent/should_fail/T11471.stderr index 377d1da759..8adeb4b280 100644 --- a/testsuite/tests/dependent/should_fail/T11471.stderr +++ b/testsuite/tests/dependent/should_fail/T11471.stderr @@ -1,5 +1,5 @@ -T11471.hs:15:10: error: [GHC-18872] +T11471.hs:17:10: error: [GHC-18872] • Couldn't match a lifted type with an unlifted type When matching types a :: * @@ -9,4 +9,14 @@ T11471.hs:15:10: error: [GHC-18872] • In the first argument of ‘f’, namely ‘(undefined :: Proxy Int#)’ In the expression: f (undefined :: Proxy Int#) 3# In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3# - • Relevant bindings include bad :: F a (bound at T11471.hs:15:1) + • Relevant bindings include bad :: F a (bound at T11471.hs:17:1) + +T11471.hs:17:35: error: [GHC-18872] + • Couldn't match a lifted type with an unlifted type + When matching types + F a :: * + Int# :: TYPE IntRep + • In the second argument of ‘f’, namely ‘3#’ + In the expression: f (undefined :: Proxy Int#) 3# + In an equation for ‘bad’: bad = f (undefined :: Proxy Int#) 3# + • Relevant bindings include bad :: F a (bound at T11471.hs:17:1) diff --git a/testsuite/tests/impredicative/icfp20-fail.stderr b/testsuite/tests/impredicative/icfp20-fail.stderr index a2fb0cad24..35079396f0 100644 --- a/testsuite/tests/impredicative/icfp20-fail.stderr +++ b/testsuite/tests/impredicative/icfp20-fail.stderr @@ -1,7 +1,6 @@ icfp20-fail.hs:20:10: error: [GHC-83865] - • Couldn't match type: forall a. a -> a - with: b -> b + • Couldn't match type ‘SId’ with ‘b -> b’ Expected: SId -> b -> b Actual: SId -> SId • In the expression: id diff --git a/testsuite/tests/indexed-types/should_fail/T4179.stderr b/testsuite/tests/indexed-types/should_fail/T4179.stderr index 3f88289e23..701006258a 100644 --- a/testsuite/tests/indexed-types/should_fail/T4179.stderr +++ b/testsuite/tests/indexed-types/should_fail/T4179.stderr @@ -1,13 +1,13 @@ T4179.hs:26:16: error: [GHC-83865] - • Couldn't match type: A3 (x (A2 (FCon x) -> A3 (FCon x))) - with: A3 (FCon x) + • Couldn't match type: A2 (x (A2 (FCon x) -> A3 (FCon x))) + with: A2 (FCon x) Expected: x (A2 (FCon x) -> A3 (FCon x)) -> A2 (FCon x) -> A3 (FCon x) Actual: x (A2 (FCon x) -> A3 (FCon x)) -> A2 (x (A2 (FCon x) -> A3 (FCon x))) -> A3 (x (A2 (FCon x) -> A3 (FCon x))) - NB: ‘A3’ is a non-injective type family + NB: ‘A2’ is a non-injective type family • In the first argument of ‘foldDoC’, namely ‘op’ In the expression: foldDoC op In an equation for ‘fCon’: fCon = foldDoC op diff --git a/testsuite/tests/indexed-types/should_fail/T4254b.hs b/testsuite/tests/indexed-types/should_fail/T4254b.hs index ffd117bc4c..44cdb5b602 100644 --- a/testsuite/tests/indexed-types/should_fail/T4254b.hs +++ b/testsuite/tests/indexed-types/should_fail/T4254b.hs @@ -11,3 +11,22 @@ fails :: forall a b. (a~Int,FD a b) => a -> Bool fails = op -- Could fail: no proof that b~Bool -- But can also succeed; it's not a *wanted* constraint + +{- Interestingly, the ambiguity check for the type sig succeeds: + +[G] FD Int b +[W] FD Int beta + +We get [W] beta~b; we unify immediately, and then solve. +All before we interact the [W] FD Int beta with the +top-level instances (which would give rise to [W] beta~Bool). + +One the other hand, from `fails = op` we get + +[G] FD Int b +[W] FD Int Bool + +Interacting those two gives [W] b~Bool; bu this doesn't +happen becase we now solve first. + +-}
\ No newline at end of file diff --git a/testsuite/tests/indexed-types/should_fail/T4254b.stderr b/testsuite/tests/indexed-types/should_fail/T4254b.stderr deleted file mode 100644 index 551978715c..0000000000 --- a/testsuite/tests/indexed-types/should_fail/T4254b.stderr +++ /dev/null @@ -1,20 +0,0 @@ - -T4254b.hs:10:10: error: [GHC-25897] - • Couldn't match type ‘b’ with ‘Bool’ - arising from a functional dependency between constraints: - ‘FD Int Bool’ - arising from a type ambiguity check for - the type signature for ‘fails’ at T4254b.hs:10:10-48 - ‘FD Int b’ - arising from the type signature for: - fails :: forall a b. - (a ~ Int, FD a b) => - a -> Bool at T4254b.hs:10:10-48 - ‘b’ is a rigid type variable bound by - the type signature for: - fails :: forall a b. (a ~ Int, FD a b) => a -> Bool - at T4254b.hs:10:10-48 - • In the ambiguity check for ‘fails’ - To defer the ambiguity check to use sites, enable AllowAmbiguousTypes - In the type signature: - fails :: forall a b. (a ~ Int, FD a b) => a -> Bool diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr index 43c8b26191..20e0084aa2 100644 --- a/testsuite/tests/indexed-types/should_fail/T9662.stderr +++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr @@ -1,13 +1,13 @@ T9662.hs:49:8: error: [GHC-25897] - • Couldn't match type ‘n’ with ‘Int’ + • Couldn't match type ‘k’ with ‘Int’ Expected: Exp (((sh :. k) :. m) :. n) -> Exp (((sh :. m) :. n) :. k) Actual: Exp (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int)) -> Exp (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int)) - ‘n’ is a rigid type variable bound by + ‘k’ is a rigid type variable bound by the type signature for: test :: forall sh k m n. Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k) diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index 325fbc0614..62eac96e84 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -58,7 +58,7 @@ test('T3330a', normal, compile_fail, ['']) test('T3330b', normal, compile_fail, ['']) test('T3330c', normal, compile_fail, ['']) test('T4179', normal, compile_fail, ['']) -test('T4254b', normal, compile_fail, ['']) +test('T4254b', normal, compile, ['']) test('T2239', normal, compile, ['']) test('T3440', expect_broken(19974), compile_fail, ['']) test('T4485', normal, compile_fail, ['']) diff --git a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr index fc3c1e0c8b..5614422045 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14040a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14040a.stderr @@ -1,7 +1,7 @@ T14040a.hs:26:46: error: [GHC-46956] - • Couldn't match kind ‘k0’ with ‘WeirdList z’ - Expected kind ‘WeirdList k0’, + • Couldn't match kind ‘k1’ with ‘WeirdList z’ + Expected kind ‘WeirdList k1’, but ‘xs’ has kind ‘WeirdList (WeirdList z)’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by @@ -25,8 +25,8 @@ T14040a.hs:26:46: error: [GHC-46956] -> p _ wl T14040a.hs:27:27: error: [GHC-46956] - • Couldn't match kind ‘k1’ with ‘z’ - Expected kind ‘WeirdList k1’, + • Couldn't match kind ‘k0’ with ‘z’ + Expected kind ‘WeirdList k0’, but ‘WeirdCons x xs’ has kind ‘WeirdList z’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr index fcad722d63..b9beb8c49c 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr @@ -1,7 +1,7 @@ T14584.hs:57:41: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)] • Could not deduce ‘SingI a’ arising from a use of ‘sing’ - from the context: (Action act, Monoid a, Good m1) + from the context: (Action act, Monoid a, Good m) bound by the instance declaration at T14584.hs:55:10-89 • In the second argument of ‘fromSing’, namely ‘(sing @m @a :: Sing _)’ @@ -10,23 +10,11 @@ T14584.hs:57:41: warning: [GHC-39999] [-Wdeferred-type-errors (in -Wdefault)] In the expression: act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) -T14584.hs:57:41: warning: [GHC-06200] [-Wdeferred-type-errors (in -Wdefault)] - • Cannot use equality for substitution: a0 ~ a - Doing so would be ill-kinded. - • In the second argument of ‘fromSing’, namely - ‘(sing @m @a :: Sing _)’ - In the fourth argument of ‘act’, namely - ‘(fromSing @m (sing @m @a :: Sing _))’ - In the expression: - act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) - • Relevant bindings include - monHom :: a -> a (bound at T14584.hs:57:3) - T14584.hs:57:50: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)] - • Could not deduce ‘m1 ~ *’ - from the context: (Action act, Monoid a, Good m1) + • Could not deduce ‘m ~ *’ + from the context: (Action act, Monoid a, Good m) bound by the instance declaration at T14584.hs:55:10-89 - ‘m1’ is a rigid type variable bound by + ‘m’ is a rigid type variable bound by the instance declaration at T14584.hs:55:10-89 • In the type ‘a’ @@ -36,9 +24,8 @@ T14584.hs:57:50: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)] ‘(fromSing @m (sing @m @a :: Sing _))’ T14584.hs:57:60: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘a0 :: m’ - Where: ‘a0’ is an ambiguous type variable - ‘m’ is a rigid type variable bound by + • Found type wildcard ‘_’ standing for ‘a :: m’ + Where: ‘a’, ‘m’ are rigid type variables bound by the instance declaration at T14584.hs:55:10-89 • In the first argument of ‘Sing’, namely ‘_’ diff --git a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr index aabc6130e3..ebbc115864 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14584a.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14584a.stderr @@ -1,7 +1,7 @@ T14584a.hs:12:5: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)] • Couldn't match expected type ‘()’ with actual type ‘m -> m’ - • Probable cause: ‘id’ is applied to too few arguments + • Probable cause: ‘id @m :: _’ is applied to too few arguments In the expression: id @m :: _ In an equation for ‘f’: f = id @m :: _ @@ -16,7 +16,11 @@ T14584a.hs:12:9: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)] In an equation for ‘f’: f = id @m :: _ T14584a.hs:12:14: warning: [GHC-88464] [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘()’ + • Found type wildcard ‘_’ standing for ‘m -> m’ + Where: ‘m’, ‘k’ are rigid type variables bound by + the type signature for: + f :: forall {k} (m :: k). () + at T14584a.hs:11:1-17 • In an expression type signature: _ In the expression: id @m :: _ In an equation for ‘f’: f = id @m :: _ @@ -32,3 +36,11 @@ T14584a.hs:15:17: warning: [GHC-25897] [-Wdeferred-type-errors (in -Wdefault)] In the expression: id @m In an equation for ‘h’: h = id @m • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9) + +T14584a.hs:16:8: warning: [GHC-83865] [-Wdeferred-type-errors (in -Wdefault)] + • Couldn't match expected type ‘()’ with actual type ‘m -> m’ + • Probable cause: ‘h’ is applied to too few arguments + In the expression: h + In the expression: let h = id @m in h + In an equation for ‘g’: g = let h = id @m in h + • Relevant bindings include h :: m -> m (bound at T14584a.hs:15:9) diff --git a/testsuite/tests/polykinds/T11399.hs b/testsuite/tests/polykinds/T11399.hs index 56f3c11ef7..ffa3848dc6 100644 --- a/testsuite/tests/polykinds/T11399.hs +++ b/testsuite/tests/polykinds/T11399.hs @@ -8,3 +8,7 @@ newtype UhOh (k :: * -> *) (a :: k *) = UhOh (k *) -- UhOh :: forall (k : * -> *). k * -> * instance Functor a => Functor (UhOh a) where + +{- Functor expects (* -> *) + (UhOh a) :: k * -> * +-}
\ No newline at end of file diff --git a/testsuite/tests/polykinds/T11399.stderr b/testsuite/tests/polykinds/T11399.stderr index a3baab2378..d8a6c83ecb 100644 --- a/testsuite/tests/polykinds/T11399.stderr +++ b/testsuite/tests/polykinds/T11399.stderr @@ -1,9 +1,6 @@ -T11399.hs:10:32: error: [GHC-18872] - • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’ - When matching kinds - a :: * -> * - TYPE :: GHC.Types.RuntimeRep -> * +T11399.hs:10:32: error: [GHC-83865] + • Couldn't match kind ‘*’ with ‘GHC.Types.LiftedRep’ Expected kind ‘* -> *’, but ‘UhOh a’ has kind ‘a (*) -> *’ • In the first argument of ‘Functor’, namely ‘(UhOh a)’ In the instance declaration for ‘Functor (UhOh a)’ diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr index 45ff51c259..df3868fb6c 100644 --- a/testsuite/tests/polykinds/T14172.stderr +++ b/testsuite/tests/polykinds/T14172.stderr @@ -12,9 +12,11 @@ T14172.hs:7:46: error: [GHC-88464] traverseCompose :: (a -> f b) -> g a -> f (h _) T14172.hs:8:19: error: [GHC-25897] - • Couldn't match type ‘h’ with ‘Compose f'0 g'0’ - arising from a use of ‘_Wrapping’ - ‘h’ is a rigid type variable bound by + • Couldn't match type ‘a’ with ‘g'1 a'0’ + Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a') + Actual: (Unwrapped (Compose f'0 g'1 a'0) -> f (Unwrapped (h a'))) + -> Compose f'0 g'1 a'0 -> f (h a') + ‘a’ is a rigid type variable bound by the inferred type of traverseCompose :: (a -> f b) -> g a -> f (h a') at T14172.hs:7:1-47 diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 2959f7669a..5b8ca76084 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -5,8 +5,8 @@ T14846.hs:38:8: error: [GHC-25897] Actual: Hom riki a a ‘ríki’ is a rigid type variable bound by the type signature for: - i :: forall {k4} {k5} {cls2 :: k5 -> Constraint} (xx :: k4) - (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *). + i :: forall {k4} {k5} {cls1 :: k5 -> Constraint} (xx :: k4) + (a :: Struct cls1) (ríki :: Struct cls1 -> Struct cls1 -> *). StructI xx a => ríki a a at T14846.hs:38:8-48 @@ -23,8 +23,8 @@ T14846.hs:38:8: error: [GHC-25897] In the instance declaration for ‘Category (Hom riki)’ T14846.hs:39:44: error: [GHC-25897] - • Couldn't match kind ‘k3’ with ‘Struct cls2’ - Expected kind ‘Struct cls2 -> Constraint’, + • Couldn't match kind ‘k3’ with ‘Struct cls1’ + Expected kind ‘Struct cls1 -> Constraint’, but ‘cls’ has kind ‘k3 -> Constraint’ ‘k3’ is a rigid type variable bound by the instance declaration diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr index 3ee1032c0a..f89e54a249 100644 --- a/testsuite/tests/polykinds/T9017.stderr +++ b/testsuite/tests/polykinds/T9017.stderr @@ -1,12 +1,12 @@ T9017.hs:8:7: error: [GHC-25897] - • Couldn't match kind ‘k2’ with ‘*’ + • Couldn't match kind ‘k1’ with ‘*’ When matching types - a0 :: * -> * -> * - a :: k1 -> k2 -> * + b0 :: * + b :: k1 Expected: a b (m b) Actual: a0 b0 (m0 b0) - ‘k2’ is a rigid type variable bound by + ‘k1’ is a rigid type variable bound by the type signature for: foo :: forall {k1} {k2} (a :: k1 -> k2 -> *) (b :: k1) (m :: k1 -> k2). diff --git a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr index 51a57fe27d..25a1fc1b6d 100644 --- a/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr +++ b/testsuite/tests/rep-poly/RepPolyRecordUpdate.stderr @@ -17,7 +17,7 @@ RepPolyRecordUpdate.hs:13:9: error: [GHC-55287] • The record update at field ‘fld’ does not have a fixed runtime representation. Its type is: - a0 :: TYPE rep0 + a :: TYPE rep0 Cannot unify ‘rep’ with the type variable ‘rep0’ because it is not a concrete ‘RuntimeRep’. • In a record update at field ‘fld’, diff --git a/testsuite/tests/rep-poly/T13929.stderr b/testsuite/tests/rep-poly/T13929.stderr index 837c1d4501..1789a7fdcb 100644 --- a/testsuite/tests/rep-poly/T13929.stderr +++ b/testsuite/tests/rep-poly/T13929.stderr @@ -3,7 +3,7 @@ T13929.hs:29:24: error: [GHC-55287] • The tuple argument in first position does not have a fixed runtime representation. Its type is: - a0 :: TYPE k00 + GUnboxed f rf :: TYPE k00 Cannot unify ‘rf’ with the type variable ‘k00’ because it is not a concrete ‘RuntimeRep’. • In the expression: (# gunbox x, gunbox y #) diff --git a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr index 966e19bec7..c5e44796e1 100644 --- a/testsuite/tests/typecheck/no_skolem_info/T14040.stderr +++ b/testsuite/tests/typecheck/no_skolem_info/T14040.stderr @@ -1,7 +1,7 @@ T14040.hs:27:46: error: [GHC-46956] - • Couldn't match kind ‘k0’ with ‘WeirdList z’ - Expected kind ‘WeirdList k0’, + • Couldn't match kind ‘k1’ with ‘WeirdList z’ + Expected kind ‘WeirdList k1’, but ‘xs’ has kind ‘WeirdList (WeirdList z)’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by @@ -25,8 +25,8 @@ T14040.hs:27:46: error: [GHC-46956] -> p _ wl T14040.hs:28:27: error: [GHC-46956] - • Couldn't match kind ‘k1’ with ‘z’ - Expected kind ‘WeirdList k1’, + • Couldn't match kind ‘k0’ with ‘z’ + Expected kind ‘WeirdList k0’, but ‘WeirdCons x xs’ has kind ‘WeirdList z’ because kind variable ‘z’ would escape its scope This (rigid, skolem) kind variable is bound by diff --git a/testsuite/tests/typecheck/should_compile/T13651.stderr b/testsuite/tests/typecheck/should_compile/T13651.stderr index 235d579739..a64d36e6ca 100644 --- a/testsuite/tests/typecheck/should_compile/T13651.stderr +++ b/testsuite/tests/typecheck/should_compile/T13651.stderr @@ -1,6 +1,6 @@ T13651.hs:12:8: error: [GHC-25897] - • Could not deduce ‘cs ~ Bar (Foo h) (Foo s)’ + • Could not deduce ‘cr ~ Bar h (Foo r)’ from the context: (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) bound by the type signature for: @@ -8,7 +8,7 @@ T13651.hs:12:8: error: [GHC-25897] (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) => Bar h (Bar r u) -> Bar (Foo h) (Bar u s) -> Foo (cr -> cs) at T13651.hs:(12,8)-(14,65) - ‘cs’ is a rigid type variable bound by + ‘cr’ is a rigid type variable bound by the type signature for: foo :: forall cr cu h r u cs s. (F cr cu ~ Bar h (Bar r u), F cu cs ~ Bar (Foo h) (Bar u s)) => diff --git a/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr b/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr index 9ab5b25eac..3b4968c941 100644 --- a/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr +++ b/testsuite/tests/typecheck/should_fail/AmbigFDs.stderr @@ -1,20 +1,20 @@ AmbigFDs.hs:10:8: error: [GHC-25897] - • Couldn't match type ‘b1’ with ‘b2’ + • Couldn't match type ‘b2’ with ‘b1’ arising from a functional dependency between constraints: - ‘C a b2’ + ‘C a b1’ arising from a type ambiguity check for the type signature for ‘foo’ at AmbigFDs.hs:10:8-35 - ‘C a b1’ + ‘C a b2’ arising from the type signature for: foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int at AmbigFDs.hs:10:8-35 - ‘b1’ is a rigid type variable bound by + ‘b2’ is a rigid type variable bound by the type signature for: foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int at AmbigFDs.hs:10:8-35 - ‘b2’ is a rigid type variable bound by + ‘b1’ is a rigid type variable bound by the type signature for: foo :: forall a b1 b2. (C a b1, C a b2) => a -> Int at AmbigFDs.hs:10:8-35 diff --git a/testsuite/tests/typecheck/should_fail/T16204c.stderr b/testsuite/tests/typecheck/should_fail/T16204c.stderr index df0e1675b7..c91a2cc060 100644 --- a/testsuite/tests/typecheck/should_fail/T16204c.stderr +++ b/testsuite/tests/typecheck/should_fail/T16204c.stderr @@ -2,7 +2,7 @@ T16204c.hs:16:8: error: [GHC-83865] • Couldn't match type ‘Rep’ with ‘*’ Expected: Sing @(*) a - Actual: Sing @Rep a0 + Actual: Sing @Rep a • In the first argument of ‘id’, namely ‘sTo’ In the expression: id sTo In an equation for ‘x’: x = id sTo diff --git a/testsuite/tests/typecheck/should_fail/T16512a.stderr b/testsuite/tests/typecheck/should_fail/T16512a.stderr index e89900b083..be297ee6d9 100644 --- a/testsuite/tests/typecheck/should_fail/T16512a.stderr +++ b/testsuite/tests/typecheck/should_fail/T16512a.stderr @@ -1,20 +1,18 @@ T16512a.hs:41:25: error: [GHC-25897] - • Couldn't match type ‘as’ with ‘a : as’ + • Couldn't match type ‘b’ with ‘a -> b’ Expected: AST (ListVariadic (a : as) b) Actual: AST (ListVariadic as (a -> b)) - ‘as’ is a rigid type variable bound by - a pattern with constructor: - AnApplication :: forall (as :: [*]) b. - AST (ListVariadic as b) -> ASTs as -> AnApplication b, - in a case alternative - at T16512a.hs:40:9-26 + ‘b’ is a rigid type variable bound by + the type signature for: + unapply :: forall b. AST b -> AnApplication b + at T16512a.hs:37:1-35 • In the first argument of ‘AnApplication’, namely ‘g’ In the expression: AnApplication g (a `ConsAST` as) In a case alternative: AnApplication g as -> AnApplication g (a `ConsAST` as) • Relevant bindings include - as :: ASTs as (bound at T16512a.hs:40:25) g :: AST (ListVariadic as (a -> b)) (bound at T16512a.hs:40:23) a :: AST a (bound at T16512a.hs:38:15) f :: AST (a -> b) (bound at T16512a.hs:38:10) + unapply :: AST b -> AnApplication b (bound at T16512a.hs:38:1) diff --git a/testsuite/tests/typecheck/should_fail/T16946.stderr b/testsuite/tests/typecheck/should_fail/T16946.stderr index c26e4fb339..19fe2a0b12 100644 --- a/testsuite/tests/typecheck/should_fail/T16946.stderr +++ b/testsuite/tests/typecheck/should_fail/T16946.stderr @@ -1,16 +1,15 @@ T16946.hs:11:9: error: [GHC-71451] • Cannot generalise type; skolem ‘k’ would escape its scope - if I tried to quantify (y0 :: k) in this type: + if I tried to quantify (x0 :: k) in this type: forall k (c :: k -> k -> *) (m :: forall (x :: k) (y :: k). c x y -> * -> *) a. CatMonad @k c m => - a -> m @y0 @y0 (Id @{k} @y0 c) a + a -> m @x0 @x0 (Id @{k} @x0 c) a (Indeed, I sometimes struggle even printing this correctly, due to its ill-scoped nature.) • In the type signature: boom :: forall k (c :: k -> k -> Type) (m :: forall (x :: k) (y :: k). c x y -> Type -> Type) - a. - CatMonad c m => a -> m (Id c) a + a. CatMonad c m => a -> m (Id c) a diff --git a/testsuite/tests/typecheck/should_fail/T17139.hs b/testsuite/tests/typecheck/should_fail/T17139.hs index b4025588dd..4869e9559d 100644 --- a/testsuite/tests/typecheck/should_fail/T17139.hs +++ b/testsuite/tests/typecheck/should_fail/T17139.hs @@ -13,3 +13,46 @@ type family TypeFam f fun where lift :: (a -> b) -> TypeFam f (a -> b) lift f = \x -> _ (f <*> x) + + +{- +x :: alpha +body of lambda :: beta + +[W] TypeFam f (a->b) ~ (alpha -> beta) +--> +[W] (f a -> TypeFam f b) ~ (alpha -> beta) +--> + alpha := f a + beta := TypeFam f b + +(<*>) :: Applicative g => g (p -> q) -> g p -> g q + +f <*> x + +arg1 + (a->b) ~ g0 (p0->q0) + g0 := ((->) a) + (p0 -> q0) ~ b <--------- +arg2 + alpha ~ g0 p0 + g0 ~ f <---------- + p0 := a +res + g0 q0 + +Finish with + [W] f ~ (->) a + [W] b ~ (a -> q0) + --> rewrite b + [W] (a -> q0) ~ a -> ( + +_ :: g0 q0 -> beta + :: (a -> q0) -> TypeFam f b + :: (a -> q0) -> TypeFam ((->) a) (a -> q0) + :: (a -> q0) -> (a->a) -> TypeFam (-> a) q0 + +BUT we would get different error messages if we did + g0 := f +and then encountered [W] g0 ~ ((->) a) +-}
\ No newline at end of file diff --git a/testsuite/tests/typecheck/should_fail/T17139.stderr b/testsuite/tests/typecheck/should_fail/T17139.stderr index f8ab95f5f8..1c253297d9 100644 --- a/testsuite/tests/typecheck/should_fail/T17139.stderr +++ b/testsuite/tests/typecheck/should_fail/T17139.stderr @@ -1,8 +1,8 @@ T17139.hs:15:16: error: [GHC-88464] - • Found hole: _ :: (a -> b0) -> f a -> TypeFam f b0 + • Found hole: _ :: (a -> b0) -> (a -> a) -> TypeFam ((->) a) b0 Where: ‘b0’ is an ambiguous type variable - ‘a’, ‘f’ are rigid type variables bound by + ‘a’ is a rigid type variable bound by the type signature for: lift :: forall a b (f :: * -> *). (a -> b) -> TypeFam f (a -> b) at T17139.hs:14:1-38 diff --git a/testsuite/tests/typecheck/should_fail/T18851c.stderr b/testsuite/tests/typecheck/should_fail/T18851c.stderr index 58c15d1b77..ebe5f8621d 100644 --- a/testsuite/tests/typecheck/should_fail/T18851c.stderr +++ b/testsuite/tests/typecheck/should_fail/T18851c.stderr @@ -2,13 +2,13 @@ T18851c.hs:25:27: error: [GHC-25897] • Could not deduce ‘n2 ~ n1’ arising from reasoning about an injective type family using constraints: - ‘Plus1 n2 ~ n’ - arising from a type equality - VSucc (Plus1 n2) ~ VSucc n at T18851c.hs:25:27-33 ‘Plus1 n1 ~ n’ + arising from a type equality + VSucc (Plus1 n1) ~ VSucc n at T18851c.hs:25:27-33 + ‘Plus1 n2 ~ n’ arising from a pattern with constructor: VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n), - in an equation for ‘foo’ at T18851c.hs:25:6-12 + in an equation for ‘foo’ at T18851c.hs:25:16-22 from the context: n ~ Plus1 n1 bound by a pattern with constructor: VSucc :: forall (n :: Nat). V n -> VSucc (Plus1 n), diff --git a/testsuite/tests/typecheck/should_fail/T22707.hs b/testsuite/tests/typecheck/should_fail/T22707.hs index 35b0817ec2..38606d57c0 100644 --- a/testsuite/tests/typecheck/should_fail/T22707.hs +++ b/testsuite/tests/typecheck/should_fail/T22707.hs @@ -3,11 +3,48 @@ module T22707 where newtype Cont o i a = Cont {runCont ::(a -> i) -> o } t1:: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) -t1 c = Cont $ \ati1tti2 -> (runCont c) (ati1tti2 $ \a -> evalCont (t1 c) >>== \ati1 -> return ati1 a ) +t1 c = Cont $ \ati1tti2 -> (runCont c) (ati1tti2 $ \xa -> evalCont (t1 c) >>== \ati1 -> return ati1 xa ) + + +{- This is a complicated and confused program. + We end up unifying + m0 p0 q0 b0 ~ (->) LiftedRep LiftedRep t1 t2 + which unifies q0~LiftedRep, and m0 with the (polymorphically-kinded) + (->) LiftedRep + Getting a decent error message out of this mess is a challenge! + + runCont :: Cont oo ii aa -> ((aa -> ii) -> oo) + (>>==) :: forall k (m:k->k->*->*) (p:k) (q:k) a. + PMonad m => m p q a -> (a -> m q r b) -> m p r b + + c :: Cont (i2 -> o) i1 a + Result type: Cont o i2 (a -> i1) + Arg of cont: ((a->i1) -> i2) -> o + ati1tti2 :: (a->i1) -> i2 + runCont c :: (a -> i1) -> i2 -> o + xa :: a -> i1 + t1 c :: Cont o i2 (a -> i1) + evalCont (t1 c) :: o + (>>==) @k0,m0,p0,q0,a0,r0) (evalCont (t1 c)) + [W] o ~ m0 p0 q0 a0 + ati1 :: a10 + return @m10 @a10 ati1 xa :: a11 + [W] m10 a10 ~ (a -> i1) -> a11 + => [W] m10 ~ (->) @LiftedRep @LiftedRep (a -> i1) + [W] a10 ~ a11 + Result of (\ati1 -> ..) + (>>==) @m0,p0,q0,a0) (evalCont (t1 c)) (\ati1 -> ..) :: m0 p0 r0 b0 + [W] a11 ~ m0 q0 r0 b0 + Result of (>>==) call + [W] i1 ~ m0 p0 r0 b0 +-} evalCont:: Cont o a a -> o evalCont c = (runCont c)id +instance Functor (Cont p p) where +instance Applicative (Cont p p) where + instance Monad (Cont p p) where return a = Cont ($ a) (>>=) = (>>==) diff --git a/testsuite/tests/typecheck/should_fail/T22707.stderr b/testsuite/tests/typecheck/should_fail/T22707.stderr index 0620e5996f..92ebbf6c00 100644 --- a/testsuite/tests/typecheck/should_fail/T22707.stderr +++ b/testsuite/tests/typecheck/should_fail/T22707.stderr @@ -1,16 +1,46 @@ -T22707.hs:6:37: error: [GHC-18872] - • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’ - When matching types - p0 :: * - GHC.Types.LiftedRep :: GHC.Types.RuntimeRep - Expected: Cont o i1 a - Actual: Cont (i2 -> o) i1 a - • In the first argument of ‘runCont’, namely ‘c’ - In the expression: - (runCont c) - (ati1tti2 $ \ a -> evalCont (t1 c) >>== \ ati1 -> return ati1 a) +T22707.hs:6:59: error: [GHC-25897] + • Couldn't match expected type ‘i1’ + with actual type ‘m0 GHC.Types.LiftedRep GHC.Types.LiftedRep b0’ + ‘i1’ is a rigid type variable bound by + the type signature for: + t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) + at T22707.hs:5:1-47 + • In the expression: evalCont (t1 c) >>== \ ati1 -> return ati1 xa In the second argument of ‘($)’, namely - ‘\ ati1tti2 - -> (runCont c) - (ati1tti2 $ \ a -> evalCont (t1 c) >>== \ ati1 -> ...)’ + ‘\ xa -> evalCont (t1 c) >>== \ ati1 -> return ati1 xa’ + In the second argument of ‘runCont’, namely + ‘(ati1tti2 + $ \ xa -> evalCont (t1 c) >>== \ ati1 -> return ati1 xa)’ + • Relevant bindings include + ati1tti2 :: (a -> i1) -> i2 (bound at T22707.hs:6:16) + c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4) + t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) + (bound at T22707.hs:6:1) + +T22707.hs:6:72: error: [GHC-25897] + • Couldn't match type ‘o’ + with ‘m0 + GHC.Types.LiftedRep + GHC.Types.LiftedRep + (m0 GHC.Types.LiftedRep GHC.Types.LiftedRep b0)’ + Expected: Cont + ((a -> i1) + -> m0 + GHC.Types.LiftedRep + GHC.Types.LiftedRep + (m0 GHC.Types.LiftedRep GHC.Types.LiftedRep b0)) + i1 + a + Actual: Cont (i2 -> o) i1 a + ‘o’ is a rigid type variable bound by + the type signature for: + t1 :: forall i2 o i1 a. Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) + at T22707.hs:5:1-47 + • In the first argument of ‘t1’, namely ‘c’ + In the first argument of ‘evalCont’, namely ‘(t1 c)’ + In the first argument of ‘(>>==)’, namely ‘evalCont (t1 c)’ + • Relevant bindings include + c :: Cont (i2 -> o) i1 a (bound at T22707.hs:6:4) + t1 :: Cont (i2 -> o) i1 a -> Cont o i2 (a -> i1) + (bound at T22707.hs:6:1) diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr index cba7dda734..0482cc63ba 100644 --- a/testsuite/tests/typecheck/should_fail/T3950.stderr +++ b/testsuite/tests/typecheck/should_fail/T3950.stderr @@ -1,9 +1,7 @@ -T3950.hs:16:13: error: [GHC-18872] - • Couldn't match kind ‘* -> *’ with ‘*’ - When matching types - w :: (* -> * -> *) -> * - Sealed :: (* -> *) -> * +T3950.hs:16:13: error: [GHC-83865] + • Couldn't match type: Id p0 x0 + with: Id p Expected: w (Id p) Actual: Sealed (Id p0 x0) • In the first argument of ‘Just’, namely ‘rp'’ diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr index 1485c88084..26f1c251e2 100644 --- a/testsuite/tests/typecheck/should_fail/T7368.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368.stderr @@ -1,6 +1,6 @@ T7368.hs:3:10: error: [GHC-18872] - • Couldn't match kind ‘*’ with ‘* -> *’ + • Couldn't match kind ‘* -> *’ with ‘*’ When matching types b0 :: * Maybe :: * -> * diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr index 7f9c97bce7..e60aaf8c39 100644 --- a/testsuite/tests/typecheck/should_fail/T7368a.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr @@ -1,9 +1,9 @@ T7368a.hs:8:6: error: [GHC-18872] - • Couldn't match kind ‘*’ with ‘* -> *’ + • Couldn't match kind ‘* -> *’ with ‘*’ When matching types - f :: * -> * - Bad :: (* -> *) -> * + w0 :: * -> * + Bad f :: * Expected: f (Bad f) Actual: Bad w0 • In the pattern: Bad x diff --git a/testsuite/tests/typecheck/should_fail/T7696.stderr b/testsuite/tests/typecheck/should_fail/T7696.stderr index 92f6be0211..aea284c74b 100644 --- a/testsuite/tests/typecheck/should_fail/T7696.stderr +++ b/testsuite/tests/typecheck/should_fail/T7696.stderr @@ -1,12 +1,7 @@ -T7696.hs:9:6: error: [GHC-18872] - • Couldn't match kind ‘*’ with ‘* -> *’ - When matching types - t0 :: (* -> *) -> * - w :: * -> * +T7696.hs:9:6: error: [GHC-83865] + • Couldn't match type ‘m0 a0’ with ‘()’ Expected: ((), w ()) Actual: (m0 a0, t0 m0) • In the expression: f1 In an equation for ‘f2’: f2 = f1 - • Relevant bindings include - f2 :: ((), w ()) (bound at T7696.hs:9:1) diff --git a/testsuite/tests/typecheck/should_fail/T7869.stderr b/testsuite/tests/typecheck/should_fail/T7869.stderr index d8532ea365..f6aa8d0bfc 100644 --- a/testsuite/tests/typecheck/should_fail/T7869.stderr +++ b/testsuite/tests/typecheck/should_fail/T7869.stderr @@ -1,16 +1,18 @@ T7869.hs:3:12: error: [GHC-25897] - • Couldn't match type ‘b1’ with ‘b’ + • Couldn't match type ‘a1’ with ‘a’ Expected: [a1] -> b1 Actual: [a] -> b - ‘b1’ is a rigid type variable bound by + ‘a1’ is a rigid type variable bound by an expression type signature: forall a1 b1. [a1] -> b1 at T7869.hs:3:20-27 - ‘b’ is a rigid type variable bound by + ‘a’ is a rigid type variable bound by the inferred type of f :: [a] -> b at T7869.hs:3:1-27 • In the expression: f x In the expression: (\ x -> f x) :: [a] -> b In an equation for ‘f’: f = (\ x -> f x) :: [a] -> b - • Relevant bindings include f :: [a] -> b (bound at T7869.hs:3:1) + • Relevant bindings include + x :: [a1] (bound at T7869.hs:3:7) + f :: [a] -> b (bound at T7869.hs:3:1) diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr index fcb1b8828b..3eb958919f 100644 --- a/testsuite/tests/typecheck/should_fail/T8603.stderr +++ b/testsuite/tests/typecheck/should_fail/T8603.stderr @@ -2,14 +2,28 @@ T8603.hs:33:17: error: [GHC-18872] • Couldn't match kind ‘* -> *’ with ‘*’ When matching types - m0 :: * -> * + (->) [a1] :: * -> * [a2] :: * Expected: [a2] -> StateT s RV a0 - Actual: t0 m0 (StateT s RV a0) + Actual: t0 ((->) [a1]) (StateT s RV a0) • The function ‘lift’ is applied to two value arguments, - but its type ‘m0 (StateT s RV a0) -> t0 m0 (StateT s RV a0)’ + but its type ‘([a1] -> StateT s RV a0) + -> t0 ((->) [a1]) (StateT s RV a0)’ has only one In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3] In the expression: do prize <- lift uniform [1, 2, ....] return False + +T8603.hs:33:22: error: [GHC-83865] + • Couldn't match type: RV a1 + with: StateT s RV a0 + Expected: [a1] -> StateT s RV a0 + Actual: [a1] -> RV a1 + • In the first argument of ‘lift’, namely ‘uniform’ + In a stmt of a 'do' block: prize <- lift uniform [1, 2, 3] + In the expression: + do prize <- lift uniform [1, 2, ....] + return False + • Relevant bindings include + testRVState1 :: RVState s Bool (bound at T8603.hs:32:1) diff --git a/testsuite/tests/typecheck/should_fail/tcfail122.stderr b/testsuite/tests/typecheck/should_fail/tcfail122.stderr index 58bb3d2389..84437750a1 100644 --- a/testsuite/tests/typecheck/should_fail/tcfail122.stderr +++ b/testsuite/tests/typecheck/should_fail/tcfail122.stderr @@ -1,9 +1,9 @@ tcfail122.hs:9:9: error: [GHC-18872] - • Couldn't match kind ‘*’ with ‘* -> *’ + • Couldn't match kind ‘* -> *’ with ‘*’ When matching types - c0 :: (* -> *) -> * - a :: * -> * + d0 :: * -> * + b :: * Expected: a b Actual: c0 d0 • In the expression: |