diff options
| author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-03-31 11:28:54 +0100 |
|---|---|---|
| committer | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-05-12 17:03:50 +0100 |
| commit | 3ae2fec52d0bb74fba4ed3800a4c0aed0514cb3d (patch) | |
| tree | fcd19997271f9b782039d379cd146caaa1aca25e | |
| parent | eb60ec18eff7943fb9f22b2d2ad29709b56ce02d (diff) | |
| download | haskell-wip/T23070-unify.tar.gz | |
Use the eager unifier in the constraint solverwip/T23070-unify
This patch continues the refactoring of the constraint solver
described in #23070.
The Big Deal in this patch is to call the regular, eager unifier from the
constraint solver, when we want to create new equalities. This
replaces the existing, unifyWanted which amounted to
yet-another-unifier, so it reduces duplication of a rather subtle
piece of technology. See
* Note [The eager unifier] in GHC.Tc.Utils.Unify
* GHC.Tc.Solver.Monad.wrapUnifierTcS
I did lots of other refactoring along the way
* I simplified the treatment of right hand sides that contain CoercionHoles.
Now, a constraint that contains a hetero-kind CoercionHole is non-canonical,
and cannot be used for rewriting or unification alike. This required me
to add the ch_hertero_kind flag to CoercionHole, with consequent knock-on
effects. See wrinkle (2) of `Note [Equalities with incompatible kinds]` in
GHC.Tc.Solver.Equality.
* I refactored the StopOrContinue type to add StartAgain, so that after a
fundep improvement (for example) we can simply start the pipeline again.
* I got rid of the unpleasant (and inefficient) rewriterSetFromType/Co functions.
With Richard I concluded that they are never needed.
* I discovered Wrinkle (W1) in Note [Wanteds rewrite Wanteds] in
GHC.Tc.Types.Constraint, and therefore now prioritise non-rewritten equalities.
Quite a few error messages change, I think always for the better.
Compiler runtime stays about the same, with one outlier: a 17% improvement in T17836
Metric Decrease:
T17836
T18223
66 files changed, 1671 insertions, 1152 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 6459136973..a2f4a2cecf 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. @@ -2068,7 +2073,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 @@ -2597,7 +2602,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 @@ -2606,22 +2612,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] @@ -2629,6 +2622,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 @@ -2659,7 +2663,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) $ @@ -2740,15 +2744,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: |