summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simon.peytonjones@gmail.com>2023-05-06 18:48:31 +0100
committerSimon Peyton Jones <simon.peytonjones@gmail.com>2023-05-06 18:48:31 +0100
commit375dde8784f3dc36cdf5eff212b856134863fa1e (patch)
treed2f51d4db1eaf4af0cdda1d56045769ef5e519c5
parent514ed18884cf6d52ebc06a91e7c4729e6f91db7a (diff)
downloadhaskell-375dde8784f3dc36cdf5eff212b856134863fa1e.tar.gz
Add the SolverStage monad
This refactoring makes a substantial improvement in the structure of GHC.Tc.Solver.Equality. I also added the new type IrredCt (akin to EqCt). Still to come: DictCt.
Diffstat
-rw-r--r--compiler/GHC/Tc/Errors.hs5
-rw-r--r--compiler/GHC/Tc/Solver/Canonical.hs31
-rw-r--r--compiler/GHC/Tc/Solver/Dict.hs2
-rw-r--r--compiler/GHC/Tc/Solver/Equality.hs511
-rw-r--r--compiler/GHC/Tc/Solver/InertSet.hs94
-rw-r--r--compiler/GHC/Tc/Solver/Interact.hs107
-rw-r--r--compiler/GHC/Tc/Solver/Monad.hs85
-rw-r--r--compiler/GHC/Tc/Solver/Rewrite.hs6
-rw-r--r--compiler/GHC/Tc/Types/Constraint.hs110
-rw-r--r--compiler/GHC/Tc/Utils/Monad.hs8
-rw-r--r--compiler/GHC/Tc/Utils/TcMType.hs24
11 files changed, 536 insertions, 447 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 8998b621e6..8e839e5824 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -465,8 +465,9 @@ mkErrorItem ct
-> do { rewriters' <- zonkRewriterSet rewriters
; return (not (isEmptyRewriterSet rewriters'), Just dest) }
- ; let m_reason = case ct of CIrredCan { cc_reason = reason } -> Just reason
- _ -> Nothing
+ ; let m_reason = case ct of
+ CIrredCan (IrredCt { ir_reason = reason }) -> Just reason
+ _ -> Nothing
; return $ Just $ EI { ei_pred = ctPred ct
, ei_evdest = m_evdest
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 49210cefa8..e8419de4ca 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -86,17 +86,17 @@ last time through, so we can skip the classification step.
-- Top-level canonicalization
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-canonicalize :: Ct -> TcS (StopOrContinue Ct)
-canonicalize (CNonCanonical { cc_ev = ev })
- = {-# SCC "canNC" #-}
- canNC ev
+canonicalize :: Ct -> SolverStage Ct
+canonicalize (CNonCanonical ev)
+ = canNC ev
-canonicalize (CEqCan can_eq_ct) = solveCanonicalEquality can_eq_ct
+canonicalize (CEqCan can_eq_ct)
+ = solveCanonicalEquality can_eq_ct
canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc }))
- = canForAll ev pend_sc
+ = Stage $ canForAll ev pend_sc
-canonicalize (CIrredCan { cc_ev = ev })
+canonicalize (CIrredCan (IrredCt { ir_ev = ev }))
= canNC ev
-- Instead of rewriting the evidence before classifying, it's possible we
-- can make progress without the rewrite. Try this first.
@@ -109,20 +109,15 @@ canonicalize (CIrredCan { cc_ev = ev })
canonicalize (CDictCan { cc_ev = ev, cc_class = cls
, cc_tyargs = xis, cc_pend_sc = pend_sc })
= {-# SCC "canClass" #-}
- canClass ev cls xis pend_sc
+ Stage $ canClass ev cls xis pend_sc
-canNC :: CtEvidence -> TcS (StopOrContinue Ct)
+canNC :: CtEvidence -> SolverStage Ct
canNC ev =
case classifyPredType pred of
- ClassPred cls tys -> do traceTcS "canEvNC:cls" (ppr cls <+> ppr tys)
- canClassNC ev cls tys
- EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2)
- solveNonCanonicalEquality ev eq_rel ty1 ty2
- IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred)
- canIrred ev
- ForAllPred tvs th p -> do traceTcS "canEvNC:forall" (ppr pred)
- canForAllNC ev tvs th p
-
+ ClassPred cls tys -> Stage $ canClassNC ev cls tys
+ EqPred eq_rel ty1 ty2 -> solveNonCanonicalEquality ev eq_rel ty1 ty2
+ IrredPred {} -> Stage $ canIrred ev
+ ForAllPred tvs th p -> Stage $ canForAllNC ev tvs th p
where
pred = ctEvPred ev
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index c0f7dc7a49..f815bbfd86 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -113,7 +113,7 @@ tryLastResortProhibitedSuperclass inerts
tryLastResortProhibitedSuperclass _ work_item
= continueWith work_item
-chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
+chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue a)
chooseInstance work_item
(OneInst { cir_new_theta = theta
, cir_what = what
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index bb2a9aa6d5..965927d6b7 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/compiler/GHC/Tc/Solver/Equality.hs
@@ -100,42 +100,201 @@ It's as if we treat (->) and (=>) as different type constructors, which
indeed they are!
-}
-solveCanonicalEquality :: EqCt -> TcS (StopOrContinue Ct)
+solveCanonicalEquality :: EqCt -> SolverStage Ct
solveCanonicalEquality (EqCt { eq_ev = ev, eq_eq_rel = eq_rel
, eq_lhs = lhs, eq_rhs = rhs })
= solveNonCanonicalEquality ev eq_rel (canEqLHSType lhs) rhs
-solveNonCanonicalEquality :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
+solveNonCanonicalEquality :: CtEvidence -> EqRel -> Type -> Type
+ -> SolverStage Ct
solveNonCanonicalEquality ev eq_rel ty1 ty2
- = do { result <- zonk_eq_types ty1 ty2
- ; case result of
- Right ty -> canEqReflexive ev eq_rel ty
- Left (Pair ty1' ty2') -> can_eq_nc False ev' eq_rel ty1' ty1' ty2' ty2'
- where
- ev' | debugIsOn = setCtEvPredType ev $
- mkPrimEqPredRole (eqRelRole eq_rel) ty1' ty2'
- | otherwise = ev
+ = do { Pair ty1' ty2' <- zonkEqTypes ev eq_rel ty1 ty2
+ ; let ev' | debugIsOn = setCtEvPredType ev $
+ mkPrimEqPredRole (eqRelRole eq_rel) ty1' ty2'
+ | otherwise = ev
-- ev': satisfy the precondition of can_eq_nc
- }
-can_eq_nc
- :: Bool -- True => both types are rewritten
- -> CtEvidence
- -> EqRel
- -> Type -> Type -- LHS, after and before type-synonym expansion, resp
- -> Type -> Type -- RHS, after and before type-synonym expansion, resp
- -> TcS (StopOrContinue Ct)
+ ; mb_canon <- canonicaliseEquality ev' eq_rel ty1' ty2'
+
+ ; case mb_canon of {
+
+ Left irred_ct -> do { solveIrredEquality irred_ct
+ ; return (CIrredCan irred_ct) } ;
+
+ Right eq_ct -> do { interactEq eq_ct
+ ; tryFunDeps eq_ct
+ ; tryQuantifiedConstraints eq_ct
+ ; return (CEqCan eq_ct) } } }
+
+
+
+{- *********************************************************************
+* *
+* zonkEqTypes
+* *
+********************************************************************* -}
+
+---------------------------------
+-- | Compare types for equality, while zonking as necessary. Gives up
+-- as soon as it finds that two types are not equal.
+-- This is quite handy when some unification has made two
+-- types in an inert Wanted to be equal. We can discover the equality without
+-- rewriting, which is sometimes very expensive (in the case of type functions).
+-- In particular, this function makes a ~20% improvement in test case
+-- perf/compiler/T5030.
+--
+-- Returns either the (partially zonked) types in the case of
+-- inequality, or the one type in the case of equality. canEqReflexive is
+-- a good next step in the 'Right' case. Returning 'Left' is always safe.
+--
+-- NB: This does *not* look through type synonyms. In fact, it treats type
+-- synonyms as rigid constructors. In the future, it might be convenient
+-- to look at only those arguments of type synonyms that actually appear
+-- in the synonym RHS. But we're not there yet.
+zonkEqTypes :: CtEvidence -> EqRel -> TcType -> TcType -> SolverStage (Pair TcType)
+zonkEqTypes ev eq_rel ty1 ty2
+ = Stage $ do { res <- go ty1 ty2
+ ; case res of
+ Left pair -> continueWith pair
+ Right ty -> canEqReflexive ev eq_rel ty }
+ where
+ go :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
+ go (TyVarTy tv1) (TyVarTy tv2) = tyvar_tyvar tv1 tv2
+ go (TyVarTy tv1) ty2 = tyvar NotSwapped tv1 ty2
+ go ty1 (TyVarTy tv2) = tyvar IsSwapped tv2 ty1
+
+ -- We handle FunTys explicitly here despite the fact that they could also be
+ -- treated as an application. Why? Well, for one it's cheaper to just look
+ -- at two types (the argument and result types) than four (the argument,
+ -- result, and their RuntimeReps). Also, we haven't completely zonked yet,
+ -- so we may run into an unzonked type variable while trying to compute the
+ -- RuntimeReps of the argument and result types. This can be observed in
+ -- testcase tc269.
+ go (FunTy af1 w1 arg1 res1) (FunTy af2 w2 arg2 res2)
+ | af1 == af2
+ , eqType w1 w2
+ = do { res_a <- go arg1 arg2
+ ; res_b <- go res1 res2
+ ; return $ combine_rev (FunTy af1 w1) res_b res_a }
+
+ go ty1@(FunTy {}) ty2 = bale_out ty1 ty2
+ go ty1 ty2@(FunTy {}) = bale_out ty1 ty2
+
+ go ty1 ty2
+ | Just (tc1, tys1) <- splitTyConAppNoView_maybe ty1
+ , Just (tc2, tys2) <- splitTyConAppNoView_maybe ty2
+ = if tc1 == tc2 && tys1 `equalLength` tys2
+ -- Crucial to check for equal-length args, because
+ -- we cannot assume that the two args to 'go' have
+ -- the same kind. E.g go (Proxy * (Maybe Int))
+ -- (Proxy (*->*) Maybe)
+ -- We'll call (go (Maybe Int) Maybe)
+ -- See #13083
+ then tycon tc1 tys1 tys2
+ else bale_out ty1 ty2
+
+ go ty1 ty2
+ | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
+ , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
+ = do { res_a <- go ty1a ty2a
+ ; res_b <- go ty1b ty2b
+ ; return $ combine_rev mkAppTy res_b res_a }
+
+ go ty1@(LitTy lit1) (LitTy lit2)
+ | lit1 == lit2
+ = return (Right ty1)
+
+ go ty1 ty2 = bale_out ty1 ty2
+ -- We don't handle more complex forms here
+
+ bale_out ty1 ty2 = return $ Left (Pair ty1 ty2)
+
+ tyvar :: SwapFlag -> TcTyVar -> TcType
+ -> TcS (Either (Pair TcType) TcType)
+ -- Try to do as little as possible, as anything we do here is redundant
+ -- with rewriting. In particular, no need to zonk kinds. That's why
+ -- we don't use the already-defined zonking functions
+ tyvar swapped tv ty
+ = case tcTyVarDetails tv of
+ MetaTv { mtv_ref = ref }
+ -> do { cts <- readTcRef ref
+ ; case cts of
+ Flexi -> give_up
+ Indirect ty' -> do { trace_indirect tv ty'
+ ; unSwap swapped go ty' ty } }
+ _ -> give_up
+ where
+ give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
+
+ tyvar_tyvar tv1 tv2
+ | tv1 == tv2 = return (Right (mkTyVarTy tv1))
+ | otherwise = do { (ty1', progress1) <- quick_zonk tv1
+ ; (ty2', progress2) <- quick_zonk tv2
+ ; if progress1 || progress2
+ then go ty1' ty2'
+ else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
+
+ trace_indirect tv ty
+ = traceTcS "Following filled tyvar (zonk_eq_types)"
+ (ppr tv <+> equals <+> ppr ty)
+
+ quick_zonk tv = case tcTyVarDetails tv of
+ MetaTv { mtv_ref = ref }
+ -> do { cts <- readTcRef ref
+ ; case cts of
+ Flexi -> return (TyVarTy tv, False)
+ Indirect ty' -> do { trace_indirect tv ty'
+ ; return (ty', True) } }
+ _ -> return (TyVarTy tv, False)
+
+ -- This happens for type families, too. But recall that failure
+ -- here just means to try harder, so it's OK if the type function
+ -- isn't injective.
+ tycon :: TyCon -> [TcType] -> [TcType]
+ -> TcS (Either (Pair TcType) TcType)
+ tycon tc tys1 tys2
+ = do { results <- zipWithM go tys1 tys2
+ ; return $ case combine_results results of
+ Left tys -> Left (mkTyConApp tc <$> tys)
+ Right tys -> Right (mkTyConApp tc tys) }
+
+ combine_results :: [Either (Pair TcType) TcType]
+ -> Either (Pair [TcType]) [TcType]
+ combine_results = bimap (fmap reverse) reverse .
+ foldl' (combine_rev (:)) (Right [])
+
+ -- combine (in reverse) a new result onto an already-combined result
+ combine_rev :: (a -> b -> c)
+ -> Either (Pair b) b
+ -> Either (Pair a) a
+ -> Either (Pair c) c
+ combine_rev f (Left list) (Left elt) = Left (f <$> elt <*> list)
+ combine_rev f (Left list) (Right ty) = Left (f <$> pure ty <*> list)
+ combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys)
+ combine_rev f (Right tys) (Right ty) = Right (f ty tys)
+
+
+{- *********************************************************************
+* *
+* canonicaliseEquality
+* *
+********************************************************************* -}
+
+canonicaliseEquality
+ :: CtEvidence -> EqRel
+ -> Type -> Type -- LHS and RHS
+ -> SolverStage (Either IrredCt EqCt)
-- Precondition: in DEBUG mode, the `ctev_pred` of `ev` is (ps_ty1 ~# ps_ty2),
-- without zonking
-- This precondition is needed (only in DEBUG) to satisfy the assertions
-- in mkSelCo, called in canDecomposableTyConAppOK and canDecomposableFunTy
-can_eq_nc rewritten ev eq_rel ty1 ps_ty1 ty2 ps_ty2
- = do { traceTcS "can_eq_nc" $
- vcat [ ppr rewritten, ppr ev, ppr eq_rel, ppr ty1, ppr ps_ty1, ppr ty2, ppr ps_ty2 ]
- ; rdr_env <- getGlobalRdrEnvTcS
- ; fam_insts <- getFamInstEnvs
- ; can_eq_nc' rewritten rdr_env fam_insts ev eq_rel ty1 ps_ty1 ty2 ps_ty2 }
+canonicaliseEquality ev eq_rel ty1 ty2
+ = Stage $ do { traceTcS "canonicaliseEquality" $
+ vcat [ ppr ev, ppr eq_rel, ppr ty1, ppr ty2 ]
+ ; rdr_env <- getGlobalRdrEnvTcS
+ ; fam_insts <- getFamInstEnvs
+ ; can_eq_nc' False rdr_env fam_insts ev eq_rel ty1 ty1 ty2 ty2 }
can_eq_nc'
:: Bool -- True => both input types are rewritten
@@ -145,7 +304,7 @@ can_eq_nc'
-> EqRel
-> Type -> Type -- LHS, after and before type-synonym expansion, resp
-> Type -> Type -- RHS, after and before type-synonym expansion, resp
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
-- See Note [Comparing nullary type synonyms] in GHC.Core.Type.
can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(TyConApp tc1 []) _ps_ty1 (TyConApp tc2 []) _ps_ty2
@@ -171,19 +330,19 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _
can_eq_nc' _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
| ReprEq <- eq_rel
, Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1
- = can_eq_newtype_nc ev NotSwapped ty1 stuff1 ty2 ps_ty2
+ = can_eq_newtype_nc rdr_env envs ev NotSwapped ty1 stuff1 ty2 ps_ty2
| ReprEq <- eq_rel
, Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
- = can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1
+ = can_eq_newtype_nc rdr_env envs ev IsSwapped ty2 stuff2 ty1 ps_ty1
-- Then, get rid of casts
-can_eq_nc' rewritten _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
+can_eq_nc' rewritten rdr_env envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
| isNothing (canEqLHS_maybe ty2) -- See (W3) 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) _
+ = canEqCast rewritten rdr_env envs 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 (W3) in Note [Equalities with incompatible kinds]
- = canEqCast rewritten ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
+ = canEqCast rewritten rdr_env envs ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1
----------------------
-- Otherwise try to decompose
@@ -276,8 +435,8 @@ can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
= do { traceTcS "can_eq_nc' catch-all case" (ppr ps_ty1 $$ ppr ps_ty2)
; case eq_rel of -- See Note [Unsolved equalities]
- ReprEq -> solveIrredEquality ReprEqReason ev
- NomEq -> solveIrredEquality ShapeMismatchReason ev }
+ ReprEq -> finishCanWithIrred ReprEqReason ev
+ NomEq -> finishCanWithIrred ShapeMismatchReason ev }
-- No need to call canEqFailure/canEqHardFailure because they
-- rewrite, and the types involved here are already rewritten
@@ -294,7 +453,7 @@ Missing this point is what caused #15431
---------------------------------
can_eq_nc_forall :: CtEvidence -> EqRel
-> Type -> Type -- LHS and RHS
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
-- (forall as. phi1) ~ (forall bs. phi2)
-- Check for length match of as, bs
-- Then build an implication constraint: forall as. phi1 ~ phi2[as/bs]
@@ -370,139 +529,6 @@ can_eq_nc_forall ev eq_rel s1 s2
= do { (wanted, co) <- newWantedEq loc rewriters role ty1 ty2
; return (co, unitBag (mkNonCanonical wanted)) }
----------------------------------
--- | Compare types for equality, while zonking as necessary. Gives up
--- as soon as it finds that two types are not equal.
--- This is quite handy when some unification has made two
--- types in an inert Wanted to be equal. We can discover the equality without
--- rewriting, which is sometimes very expensive (in the case of type functions).
--- In particular, this function makes a ~20% improvement in test case
--- perf/compiler/T5030.
---
--- Returns either the (partially zonked) types in the case of
--- inequality, or the one type in the case of equality. canEqReflexive is
--- a good next step in the 'Right' case. Returning 'Left' is always safe.
---
--- NB: This does *not* look through type synonyms. In fact, it treats type
--- synonyms as rigid constructors. In the future, it might be convenient
--- to look at only those arguments of type synonyms that actually appear
--- in the synonym RHS. But we're not there yet.
-zonk_eq_types :: TcType -> TcType -> TcS (Either (Pair TcType) TcType)
-zonk_eq_types = go
- where
- go (TyVarTy tv1) (TyVarTy tv2) = tyvar_tyvar tv1 tv2
- go (TyVarTy tv1) ty2 = tyvar NotSwapped tv1 ty2
- go ty1 (TyVarTy tv2) = tyvar IsSwapped tv2 ty1
-
- -- We handle FunTys explicitly here despite the fact that they could also be
- -- treated as an application. Why? Well, for one it's cheaper to just look
- -- at two types (the argument and result types) than four (the argument,
- -- result, and their RuntimeReps). Also, we haven't completely zonked yet,
- -- so we may run into an unzonked type variable while trying to compute the
- -- RuntimeReps of the argument and result types. This can be observed in
- -- testcase tc269.
- go (FunTy af1 w1 arg1 res1) (FunTy af2 w2 arg2 res2)
- | af1 == af2
- , eqType w1 w2
- = do { res_a <- go arg1 arg2
- ; res_b <- go res1 res2
- ; return $ combine_rev (FunTy af1 w1) res_b res_a }
-
- go ty1@(FunTy {}) ty2 = bale_out ty1 ty2
- go ty1 ty2@(FunTy {}) = bale_out ty1 ty2
-
- go ty1 ty2
- | Just (tc1, tys1) <- splitTyConAppNoView_maybe ty1
- , Just (tc2, tys2) <- splitTyConAppNoView_maybe ty2
- = if tc1 == tc2 && tys1 `equalLength` tys2
- -- Crucial to check for equal-length args, because
- -- we cannot assume that the two args to 'go' have
- -- the same kind. E.g go (Proxy * (Maybe Int))
- -- (Proxy (*->*) Maybe)
- -- We'll call (go (Maybe Int) Maybe)
- -- See #13083
- then tycon tc1 tys1 tys2
- else bale_out ty1 ty2
-
- go ty1 ty2
- | Just (ty1a, ty1b) <- tcSplitAppTyNoView_maybe ty1
- , Just (ty2a, ty2b) <- tcSplitAppTyNoView_maybe ty2
- = do { res_a <- go ty1a ty2a
- ; res_b <- go ty1b ty2b
- ; return $ combine_rev mkAppTy res_b res_a }
-
- go ty1@(LitTy lit1) (LitTy lit2)
- | lit1 == lit2
- = return (Right ty1)
-
- go ty1 ty2 = bale_out ty1 ty2
- -- We don't handle more complex forms here
-
- bale_out ty1 ty2 = return $ Left (Pair ty1 ty2)
-
- tyvar :: SwapFlag -> TcTyVar -> TcType
- -> TcS (Either (Pair TcType) TcType)
- -- Try to do as little as possible, as anything we do here is redundant
- -- with rewriting. In particular, no need to zonk kinds. That's why
- -- we don't use the already-defined zonking functions
- tyvar swapped tv ty
- = case tcTyVarDetails tv of
- MetaTv { mtv_ref = ref }
- -> do { cts <- readTcRef ref
- ; case cts of
- Flexi -> give_up
- Indirect ty' -> do { trace_indirect tv ty'
- ; unSwap swapped go ty' ty } }
- _ -> give_up
- where
- give_up = return $ Left $ unSwap swapped Pair (mkTyVarTy tv) ty
-
- tyvar_tyvar tv1 tv2
- | tv1 == tv2 = return (Right (mkTyVarTy tv1))
- | otherwise = do { (ty1', progress1) <- quick_zonk tv1
- ; (ty2', progress2) <- quick_zonk tv2
- ; if progress1 || progress2
- then go ty1' ty2'
- else return $ Left (Pair (TyVarTy tv1) (TyVarTy tv2)) }
-
- trace_indirect tv ty
- = traceTcS "Following filled tyvar (zonk_eq_types)"
- (ppr tv <+> equals <+> ppr ty)
-
- quick_zonk tv = case tcTyVarDetails tv of
- MetaTv { mtv_ref = ref }
- -> do { cts <- readTcRef ref
- ; case cts of
- Flexi -> return (TyVarTy tv, False)
- Indirect ty' -> do { trace_indirect tv ty'
- ; return (ty', True) } }
- _ -> return (TyVarTy tv, False)
-
- -- This happens for type families, too. But recall that failure
- -- here just means to try harder, so it's OK if the type function
- -- isn't injective.
- tycon :: TyCon -> [TcType] -> [TcType]
- -> TcS (Either (Pair TcType) TcType)
- tycon tc tys1 tys2
- = do { results <- zipWithM go tys1 tys2
- ; return $ case combine_results results of
- Left tys -> Left (mkTyConApp tc <$> tys)
- Right tys -> Right (mkTyConApp tc tys) }
-
- combine_results :: [Either (Pair TcType) TcType]
- -> Either (Pair [TcType]) [TcType]
- combine_results = bimap (fmap reverse) reverse .
- foldl' (combine_rev (:)) (Right [])
-
- -- combine (in reverse) a new result onto an already-combined result
- combine_rev :: (a -> b -> c)
- -> Either (Pair b) b
- -> Either (Pair a) a
- -> Either (Pair c) c
- combine_rev f (Left list) (Left elt) = Left (f <$> elt <*> list)
- combine_rev f (Left list) (Right ty) = Left (f <$> pure ty <*> list)
- combine_rev f (Right tys) (Left elt) = Left (f <$> elt <*> pure tys)
- combine_rev f (Right tys) (Right ty) = Right (f ty tys)
{- Note [Unwrap newtypes first]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -612,14 +638,15 @@ though, because we check our depth in `can_eq_newtype_nc`.
------------------------
-- | We're able to unwrap a newtype. Update the bits accordingly.
-can_eq_newtype_nc :: CtEvidence -- ^ :: ty1 ~ ty2
+can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs
+ -> CtEvidence -- ^ :: ty1 ~ ty2
-> SwapFlag
-> TcType -- ^ ty1
-> ((Bag GlobalRdrElt, TcCoercion), TcType) -- ^ :: ty1 ~ ty1'
-> TcType -- ^ ty2
-> TcType -- ^ ty2, with type synonyms
- -> TcS (StopOrContinue Ct)
-can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
+can_eq_newtype_nc rdr_env envs ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
= do { traceTcS "can_eq_newtype_nc" $
vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ]
@@ -638,7 +665,7 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
; new_ev <- rewriteEqEvidence emptyRewriterSet ev' swapped
redn1 (mkReflRedn Representational ps_ty2)
- ; can_eq_nc False new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
+ ; can_eq_nc' False rdr_env envs new_ev ReprEq ty1' ty1' ty2 ps_ty2 }
---------
-- ^ Decompose a type application.
@@ -647,7 +674,7 @@ can_eq_newtype_nc ev swapped ty1 ((gres, co1), ty1') ty2 ps_ty2
can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-> Xi -> Xi -- s1 t1
-> Xi -> Xi -- s2 t2
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
-- AppTys only decompose for nominal equality, so this case just leads
-- to an irreducible constraint; see typecheck/should_compile/T10494
@@ -685,7 +712,7 @@ can_eq_app ev s1 t1 s2 t2
; evar_t <- newGivenEvVar loc ( mkTcEqPredLikeEv ev t1 t2
, evCoercion co_t )
; emitWorkNC [evar_t]
- ; solveNonCanonicalEquality evar_s NomEq s1 s2 }
+ ; startAgainWith (mkNonCanonical evar_s) }
where
loc = ctEvLoc ev
@@ -701,20 +728,21 @@ can_eq_app ev s1 t1 s2 t2
-- | Break apart an equality over a casted type
-- looking like (ty1 |> co1) ~ ty2 (modulo a swap-flag)
canEqCast :: Bool -- are both types rewritten?
+ -> GlobalRdrEnv -> FamInstEnvs
-> CtEvidence
-> EqRel
-> SwapFlag
-> TcType -> Coercion -- LHS (res. RHS), ty1 |> co1
-> TcType -> TcType -- RHS (res. LHS), ty2 both normal and pretty
- -> TcS (StopOrContinue Ct)
-canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
+canEqCast rewritten rdr_env envs ev eq_rel swapped ty1 co1 ty2 ps_ty2
= do { traceTcS "Decomposing cast" (vcat [ ppr ev
, ppr ty1 <+> text "|>" <+> ppr co1
, ppr ps_ty2 ])
; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
(mkGReflLeftRedn role ty1 co1)
(mkReflRedn role ps_ty2)
- ; can_eq_nc rewritten new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
+ ; can_eq_nc' rewritten rdr_env envs new_ev eq_rel ty1 ty1 ty2 ps_ty2 }
where
role = eqRelRole eq_rel
@@ -722,7 +750,7 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
canTyConApp :: CtEvidence -> EqRel
-> TyCon -> [TcType]
-> TyCon -> [TcType]
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
-- See Note [Decomposing TyConApp equalities]
-- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family
-- But they can be data families.
@@ -737,7 +765,7 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
-- See Note [Skolem abstract data] in GHC.Core.Tycon
| tyConSkolem tc1 || tyConSkolem tc2
= do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
- ; solveIrredEquality AbstractTyConReason ev }
+ ; finishCanWithIrred AbstractTyConReason ev }
-- Fail straight away for better error messages
-- See Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1203,7 +1231,7 @@ Extra points
canDecomposableTyConAppOK :: CtEvidence -> EqRel
-> TyCon -> [TcType] -> [TcType]
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue a)
-- Precondition: tys1 and tys2 are the same finite length, hence "OK"
canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
= assert (tys1 `equalLength` tys2) $
@@ -1260,7 +1288,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
canDecomposableFunTy :: CtEvidence -> EqRel -> FunTyFlag
-> (Type,Type,Type) -- (multiplicity,arg,res)
-> (Type,Type,Type) -- (multiplicity,arg,res)
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue a)
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)
@@ -1293,7 +1321,7 @@ canDecomposableFunTy ev eq_rel af f1@(m1,a1,r1) f2@(m2,a2,r2)
-- representational, there is some hope for the future.
-- Examples in Note [Use canEqFailure in canDecomposableTyConApp]
canEqFailure :: CtEvidence -> EqRel
- -> TcType -> TcType -> TcS (StopOrContinue Ct)
+ -> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
canEqFailure ev NomEq ty1 ty2
= canEqHardFailure ev ty1 ty2
canEqFailure ev ReprEq ty1 ty2
@@ -1305,18 +1333,18 @@ canEqFailure ev ReprEq ty1 ty2
; traceTcS "canEqFailure with ReprEq" $
vcat [ ppr ev, ppr redn1, ppr redn2 ]
; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
- ; continueWith (mkIrredCt ReprEqReason new_ev) }
+ ; finishCanWithIrred ReprEqReason new_ev }
-- | Call when canonicalizing an equality fails with utterly no hope.
canEqHardFailure :: CtEvidence
- -> TcType -> TcType -> TcS (StopOrContinue Ct)
+ -> TcType -> TcType -> TcS (StopOrContinue (Either IrredCt a))
-- See Note [Make sure that insolubles are fully rewritten]
canEqHardFailure ev ty1 ty2
= do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2)
; (redn1, rewriters1) <- rewriteForErrors ev ty1
; (redn2, rewriters2) <- rewriteForErrors ev ty2
; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
- ; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
+ ; finishCanWithIrred ShapeMismatchReason new_ev }
{-
Note [Canonicalising type applications]
@@ -1436,7 +1464,7 @@ canEqCanLHS :: CtEvidence -- ev :: lhs ~ rhs
-> CanEqLHS -- lhs (or, if swapped, rhs)
-> TcType -- lhs: pretty lhs, already rewritten
-> TcType -> TcType -- rhs: already rewritten
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
| k1 `tcEqType` k2
= canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
@@ -1484,7 +1512,7 @@ canEqCanLHSHetero :: CtEvidence -- :: (xi1 :: ki1) ~ (xi2 :: ki2)
-> TcKind -- ki1
-> TcType -> TcType -- xi2
-> TcKind -- ki2
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
-- See Note [Equalities with incompatible kinds]
-- See Note [Kind Equality Orientation]
@@ -1547,7 +1575,7 @@ canEqCanLHSHomo :: CtEvidence -- lhs ~ rhs
-> EqRel -> SwapFlag
-> CanEqLHS -> TcType -- lhs, pretty lhs
-> TcType -> TcType -- rhs, pretty rhs
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
-- Guaranteed that typeKind lhs == typeKind rhs
canEqCanLHSHomo ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
| (xi2', mco) <- split_cast_ty xi2
@@ -1571,7 +1599,7 @@ canEqCanLHS2 :: CtEvidence -- lhs ~ (rhs |> mco)
-> CanEqLHS -- rhs
-> TcType -- pretty rhs
-> MCoercion -- :: kind(rhs) ~N kind(lhs)
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
| lhs1 `eqCanEqLHS` lhs2
-- It must be the case that mco is reflexive
@@ -1696,11 +1724,11 @@ If we have a TyFamLHS on both sides, we choose how to orient it.
-- want to rewrite the LHS to (as per e.g. swapOverTyVars)
canEqCanLHSFinish, canEqCanLHSFinish_try_unification,
canEqCanLHSFinish_no_unification
- :: CtEvidence
+ :: CtEvidence -- (lhs ~ rhs) or if swapped (rhs ~ lhs)
-> EqRel -> SwapFlag
- -> CanEqLHS -- lhs (or, if swapped, rhs)
- -> TcType -- rhs (or, if swapped, lhs)
- -> TcS (StopOrContinue Ct)
+ -> CanEqLHS -- lhs
+ -> TcType -- rhs
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
-- RHS is fully rewritten, but with type synonyms
-- preserved as much as possible
-- Guaranteed preconditions that
@@ -1866,49 +1894,54 @@ canEqCanLHSFinish_no_unification ev eq_rel swapped lhs rhs
-- * new_ev has reductionReducedType on the RHS
-- * eq_rhs is set to reductionReducedType
-- See Note [Forgetful synonyms in checkTyConApp] in GHC.Tc.Utils.Unify
- ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = lhs
- , eq_rhs = reductionReducedType rhs_redn }) } }
+ ; continueWith $ Right $
+ EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
+ , eq_lhs = lhs
+ , eq_rhs = reductionReducedType rhs_redn } } }
----------------------
swapAndFinish :: CtEvidence -> EqRel -> SwapFlag
-> TcType -> CanEqLHS -- ty ~ F tys
- -> TcS (StopOrContinue Ct)
+ -> TcS (StopOrContinue (Either IrredCt EqCt))
-- We have an equality alpha ~ F tys, that we can't unify e.g because 'tys'
-- mentions alpha, it would not be a canonical constraint as-is.
-- We want to flip it to (F tys ~ a), whereupon it is canonical
swapAndFinish ev eq_rel swapped lhs_ty can_rhs
- = do { new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
+ = do { let role = eqRelRole eq_rel
+ ; new_ev <- rewriteEqEvidence emptyRewriterSet ev (flipSwap swapped)
(mkReflRedn role (canEqLHSType can_rhs))
(mkReflRedn role lhs_ty)
- ; interactEq (EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
- , eq_lhs = can_rhs, eq_rhs = lhs_ty }) }
- where
- role = eqRelRole eq_rel
+ ; continueWith $ Right $
+ EqCt { eq_ev = new_ev, eq_eq_rel = eq_rel
+ , eq_lhs = can_rhs, eq_rhs = lhs_ty } }
----------------------
tryIrredInstead :: CheckTyEqResult -> CtEvidence -> EqRel -> SwapFlag
- -> CanEqLHS -> TcType -> TcS (StopOrContinue Ct)
+ -> CanEqLHS -> TcType -> TcS (StopOrContinue (Either IrredCt a))
-- We have a non-canonical equality
-- We still swap it if 'swapped' says so, so that it is oriented
--- in the direction that the error message reporting machinery
+-- in the direction that the error-reporting machinery
-- expects it; e.g. (m ~ t m) rather than (t m ~ m)
-- This is not very important, and only affects error reporting.
tryIrredInstead reason ev eq_rel swapped lhs rhs
= do { traceTcS "cantMakeCanonical" (ppr reason $$ ppr lhs $$ ppr rhs)
+ ; let role = eqRelRole eq_rel
; new_ev <- rewriteEqEvidence emptyRewriterSet ev swapped
(mkReflRedn role (canEqLHSType lhs))
(mkReflRedn role rhs)
- ; solveIrredEquality (NonCanonicalReason reason) new_ev }
- where
- role = eqRelRole eq_rel
+ ; finishCanWithIrred (NonCanonicalReason reason) new_ev }
+
+finishCanWithIrred :: CtIrredReason -> CtEvidence
+ -> TcS (StopOrContinue (Either IrredCt a))
+finishCanWithIrred reason ev
+ = continueWith $ Left $ IrredCt { ir_ev = ev, ir_reason = reason }
-----------------------
-- | Solve a reflexive equality constraint
canEqReflexive :: CtEvidence -- ty ~ ty
-> EqRel
-> TcType -- ty
- -> TcS (StopOrContinue Ct) -- always Stop
+ -> TcS (StopOrContinue a) -- always Stop
canEqReflexive ev eq_rel ty
= do { setEvBindIfWanted ev IsCoherent $
evCoercion (mkReflCo (eqRelRole eq_rel) ty)
@@ -2488,10 +2521,10 @@ But it's not so simple:
call to strictly_more_visible.
-}
-interactEq :: EqCt -> TcS (StopOrContinue Ct)
-interactEq work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
-
- = do { inerts <- getInertCans
+interactEq :: EqCt -> SolverStage ()
+interactEq work_item@(EqCt { eq_ev = ev, eq_eq_rel = eq_rel })
+ = Stage $
+ do { inerts <- getInertCans
; if | Just (ev_i, swapped) <- inertsCanDischarge inerts work_item
-> do { setEvBindIfWanted ev IsCoherent $
evCoercion (maybeSymCo swapped $
@@ -2501,14 +2534,7 @@ interactEq work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })
; stopWith ev "Solved from inert" }
| otherwise
- -> case lhs of
- TyVarLHS {} -> 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 } }
-
+ -> continueWith () }
inertsCanDischarge :: InertCans -> EqCt
-> Maybe ( CtEvidence -- The evidence for the inert
@@ -2628,6 +2654,7 @@ make the solver iterate more often. (We don't need to iterate when unifying
at the ambient level because of the kick-out mechanism.)
-}
+
{-********************************************************************
* *
Final wrap-up for equalities
@@ -2647,10 +2674,10 @@ See
-}
--------------------
-solveIrredEquality :: CtIrredReason -> CtEvidence -> TcS (StopOrContinue Ct)
-solveIrredEquality reason ev
+solveIrredEquality :: IrredCt -> SolverStage ()
+solveIrredEquality irred@(IrredCt { ir_ev = ev })
| EqPred eq_rel t1 t2 <- classifyPredType (ctEvPred ev)
- = final_qci_check (mkIrredCt reason ev) eq_rel t1 t2
+ = lookup_eq_in_qcis (CIrredCan irred) eq_rel t1 t2
-- If the final_qci_check fails, we'll do continueWith on an IrredCt
-- That in turn will go down the Irred pipeline, so which deals with
-- the case where we have [G] Coercible (m a) (m b), and [W] m a ~R# m b
@@ -2664,24 +2691,25 @@ solveIrredEquality reason ev
= pprPanic "solveIrredEquality" (ppr ev)
--------------------
-finishEqCt :: EqCt -> TcS (StopOrContinue Ct)
-finishEqCt work_item@(EqCt { eq_lhs = lhs, eq_rhs = rhs, eq_eq_rel = eq_rel })
- = final_qci_check (CEqCan work_item) eq_rel (canEqLHSType lhs) rhs
+tryQuantifiedConstraints :: EqCt -> SolverStage ()
+tryQuantifiedConstraints work_item@(EqCt { eq_lhs = lhs, eq_rhs = rhs, eq_eq_rel = eq_rel })
+ = lookup_eq_in_qcis (CEqCan work_item) eq_rel (canEqLHSType lhs) rhs
--------------------
-final_qci_check :: Ct -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct)
+lookup_eq_in_qcis :: Ct -> EqRel -> TcType -> TcType -> SolverStage ()
-- The "final QCI check" checks to see if we have
-- [W] t1 ~# t2
-- and a Given quantified contraint like (forall a b. blah => a ~ b)
-- Why? See Note [Looking up primitive equalities in quantified constraints]
-final_qci_check work_ct eq_rel lhs rhs
- = do { ev_binds_var <- getTcEvBindsVar
+lookup_eq_in_qcis work_ct eq_rel lhs rhs
+ = Stage $
+ do { ev_binds_var <- getTcEvBindsVar
; ics <- getInertCans
; if isWanted ev -- Never look up Givens in quantified constraints
&& not (null (inert_insts ics)) -- Shortcut common case
&& not (isCoEvBindsVar ev_binds_var) -- See Note [Instances in no-evidence implications]
then try_for_qci
- else continueWith work_ct }
+ else continueWith () }
where
ev = ctEvidence work_ct
loc = ctEvLoc ev
@@ -2690,27 +2718,27 @@ final_qci_check work_ct eq_rel lhs rhs
try_for_qci -- First try looking for (lhs ~ rhs)
| Just (cls, tys) <- boxEqPred eq_rel lhs rhs
= do { res <- matchLocalInst (mkClassPred cls tys) loc
- ; traceTcS "final_qci_check:1" (ppr (mkClassPred cls tys))
+ ; traceTcS "lookup_irred_in_qcis:1" (ppr (mkClassPred cls tys))
; case res of
OneInst { cir_mk_ev = mk_ev }
-> chooseInstance ev (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
_ -> try_swapping }
| otherwise
- = continueWith work_ct
+ = continueWith ()
try_swapping -- Now try looking for (rhs ~ lhs) (see #23333)
| Just (cls, tys) <- boxEqPred eq_rel rhs lhs
= do { res <- matchLocalInst (mkClassPred cls tys) loc
- ; traceTcS "final_qci_check:2" (ppr (mkClassPred cls tys))
+ ; traceTcS "lookup_irred_in_qcis:2" (ppr (mkClassPred cls tys))
; case res of
OneInst { cir_mk_ev = mk_ev }
-> do { ev' <- rewriteEqEvidence emptyRewriterSet ev IsSwapped
(mkReflRedn role rhs) (mkReflRedn role lhs)
; chooseInstance ev' (res { cir_mk_ev = mk_eq_ev cls tys mk_ev }) }
- _ -> do { traceTcS "final_qci_check:3" (ppr work_ct)
- ; continueWith work_ct }}
+ _ -> do { traceTcS "lookup_irred_in_qcis:3" (ppr work_ct)
+ ; continueWith () }}
| otherwise
- = continueWith work_ct
+ = continueWith ()
mk_eq_ev cls tys mk_ev evs
| sc_id : rest <- classSCSelIds cls -- Just one superclass for this
@@ -2875,6 +2903,19 @@ tryFamFamInjectivity ev eq_rel fun_tc1 fun_args1 fun_tc2 fun_args2 mco
= return False
--------------------
+tryFunDeps :: EqCt -> SolverStage ()
+tryFunDeps work_item@(EqCt { eq_lhs = lhs, eq_ev = ev })
+ = Stage $
+ case lhs of
+ TyFamLHS tc args -> do { inerts <- getInertCans
+ ; imp1 <- improveLocalFunEqs inerts tc args work_item
+ ; imp2 <- improveTopFunEqs tc args work_item
+ ; if (imp1 || imp2)
+ then startAgainWith (mkNonCanonical ev)
+ else continueWith () }
+ TyVarLHS {} -> continueWith ()
+
+--------------------
improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool
-- See Note [FunDep and implicit parameter reactions]
improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs })
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index 042e3ff9e3..af812fe6e1 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -31,6 +31,10 @@ module GHC.Tc.Solver.InertSet (
partitionInertEqs, partitionFunEqs,
foldFunEqs,
+ -- * Inert Irreds
+ InertIrreds, delIrred, extendIrreds, foldIrreds,
+ findMatchingIrreds,
+
-- * Kick-out
kickOutRewritableLHS,
@@ -51,6 +55,7 @@ import GHC.Tc.Utils.TcType
import GHC.Types.Var
import GHC.Types.Var.Env
+import GHC.Types.Basic( SwapFlag(..) )
import GHC.Core.Reduction
import GHC.Core.Predicate
@@ -319,7 +324,7 @@ emptyInertCans
, inert_dicts = emptyDictMap
, inert_safehask = emptyDictMap
, inert_insts = []
- , inert_irreds = emptyCts }
+ , inert_irreds = emptyBag }
emptyInert :: InertSet
emptyInert
@@ -1131,7 +1136,7 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
-- ^ See Note [Safe Haskell Overlapping Instances Implementation]
-- in GHC.Tc.Solver
- , inert_irreds :: Cts
+ , inert_irreds :: InertIrreds
-- Irreducible predicates that cannot be made canonical,
-- and which don't interact with others (e.g. (c a))
-- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a])
@@ -1152,6 +1157,7 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
type InertEqs = DTyVarEnv EqualCtList
type InertFunEqs = FunEqMap EqualCtList
+type InertIrreds = Bag IrredCt
instance Outputable InertCans where
ppr (IC { inert_eqs = eqs
@@ -1174,7 +1180,7 @@ instance Outputable InertCans where
text "Dictionaries =" <+> pprBag (dictsToBag dicts)
, ppUnless (isEmptyTcAppMap safehask) $
text "Safe Haskell unsafe overlap =" <+> pprBag (dictsToBag safehask)
- , ppUnless (isEmptyCts irreds) $
+ , ppUnless (isEmptyBag irreds) $
text "Irreds =" <+> pprBag irreds
, ppUnless (null insts) $
text "Given instances =" <+> vcat (map ppr insts)
@@ -1274,6 +1280,74 @@ extendFunEqs fun_eqs eq_ct@(EqCt { eq_lhs = TyFamLHS tc args })
= addCanFunEq fun_eqs tc args eq_ct
extendFunEqs _ other = pprPanic "extendFunEqs" (ppr other)
+
+{- *********************************************************************
+* *
+ Inert Irreds
+* *
+********************************************************************* -}
+
+extendIrreds :: [IrredCt] -> InertIrreds -> InertIrreds
+extendIrreds extras irreds
+ | null extras = irreds
+ | otherwise = irreds `unionBags` listToBag extras
+
+delIrred :: InertCans -> IrredCt -> InertCans
+-- Remove a particular (Given) Irred, on the instructions of a plugin
+-- For some reason this is done vis the evidence Id, not the type
+-- Compare delEq. I have not idea why
+delIrred ics (IrredCt { ir_ev = ev })
+ = ics { inert_irreds = filterBag keep (inert_irreds ics) }
+ where
+ ev_id = ctEvEvId ev
+ keep (IrredCt { ir_ev = ev' }) = ev_id == ctEvEvId ev'
+
+foldIrreds :: (IrredCt -> b -> b) -> InertIrreds -> b -> b
+foldIrreds k irreds z = foldr k z irreds
+
+findMatchingIrreds :: InertIrreds -> CtEvidence
+ -> (Bag (IrredCt, SwapFlag), InertIrreds)
+findMatchingIrreds irreds ev
+ | EqPred eq_rel1 lty1 rty1 <- classifyPredType pred
+ -- See Note [Solving irreducible equalities]
+ = partitionBagWith (match_eq eq_rel1 lty1 rty1) irreds
+ | otherwise
+ = partitionBagWith match_non_eq irreds
+ where
+ pred = ctEvPred ev
+ match_non_eq irred
+ | irredCtPred irred `tcEqTypeNoKindCheck` pred = Left (irred, NotSwapped)
+ | otherwise = Right irred
+
+ match_eq eq_rel1 lty1 rty1 irred
+ | EqPred eq_rel2 lty2 rty2 <- classifyPredType (irredCtPred irred)
+ , eq_rel1 == eq_rel2
+ , Just swap <- match_eq_help lty1 rty1 lty2 rty2
+ = Left (irred, swap)
+ | otherwise
+ = Right irred
+
+ match_eq_help lty1 rty1 lty2 rty2
+ | lty1 `tcEqTypeNoKindCheck` lty2, rty1 `tcEqTypeNoKindCheck` rty2
+ = Just NotSwapped
+ | lty1 `tcEqTypeNoKindCheck` rty2, rty1 `tcEqTypeNoKindCheck` lty2
+ = Just IsSwapped
+ | otherwise
+ = Nothing
+
+{- Note [Solving irreducible equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#14333)
+ [G] a b ~R# c d
+ [W] c d ~R# a b
+Clearly we should be able to solve this! Even though the constraints are
+not decomposable. We solve this when looking up the work-item in the
+irreducible constraints to look for an identical one. When doing this
+lookup, findMatchingIrreds spots the equality case, and matches either
+way around. It has to return a swap-flag so we can generate evidence
+that is the right way round too.
+-}
+
{- *********************************************************************
* *
Adding to and removing from the inert set
@@ -1290,10 +1364,10 @@ addInertItem tc_lvl
TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys eq_ct }
TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv eq_ct }
-addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {})
- = updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an
+addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) ct@(CIrredCan irred)
+ = updateGivenEqs tc_lvl ct $ -- An Irred might turn out to be an
-- equality, so we play safe
- ics { inert_irreds = irreds `snocBag` item }
+ ics { inert_irreds = irreds `snocBag` irred }
addInertItem _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
= ics { inert_dicts = addDict (inert_dicts ics) cls tys item }
@@ -1358,7 +1432,7 @@ kickOutRewritableLHS new_fr new_lhs
-- 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 = (dicts_out `andCts` irs_out)
+ kicked_out = (dicts_out `andCts` fmap CIrredCan irs_out)
`extendCtsList` insts_out
`extendCtsList` map CEqCan tv_eqs_out
`extendCtsList` map CEqCan feqs_out
@@ -1366,7 +1440,7 @@ kickOutRewritableLHS new_fr new_lhs
(tv_eqs_out, tv_eqs_in) = partitionInertEqs kick_out_eq tv_eqs
(feqs_out, feqs_in) = partitionFunEqs kick_out_eq funeqmap
(dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
- (irs_out, irs_in) = partitionBag kick_out_ct irreds
+ (irs_out, irs_in) = partitionBag (kick_out_ct . CIrredCan) irreds
-- Kick out even insolubles: See Note [Rewrite insolubles]
-- Of course we must kick out irreducibles like (c a), in case
-- we can rewrite 'c' to something more useful
@@ -1577,8 +1651,8 @@ noGivenNewtypeReprEqs :: TyCon -> InertSet -> Bool
noGivenNewtypeReprEqs tc inerts
= not (anyBag might_help (inert_irreds (inert_cans inerts)))
where
- might_help ct
- = case classifyPredType (ctPred ct) of
+ might_help irred
+ = case classifyPredType (ctEvPred (irredCtEvidence irred)) of
EqPred ReprEq t1 t2
| Just (tc1,_) <- tcSplitTyConApp_maybe t1
, tc == tc1
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index e40478279c..94ab1f6379 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -175,9 +175,9 @@ runTcPluginsGiven
; if null givens then return [] else
do { p <- runTcPluginSolvers solvers (givens,[])
; let (solved_givens, _) = pluginSolvedCts p
- insols = pluginBadCts p
- ; updInertCans (removeInertCts solved_givens)
- ; updInertIrreds (\irreds -> extendCtsList irreds insols)
+ insols = map (ctIrredCt PluginReason) (pluginBadCts p)
+ ; updInertCans (removeInertCts solved_givens)
+ ; updInertIrreds (extendIrreds insols)
; return (pluginNewCts p) } } }
-- | Given a bag of (rewritten, zonked) wanteds, invoke the plugins on
@@ -283,11 +283,11 @@ runTcPluginSolvers solvers all_cts
(xs `without` cts, ys `without` cts)
without :: [Ct] -> [Ct] -> [Ct]
- without = deleteFirstsBy eqCt
+ without = deleteFirstsBy eq_ct
- eqCt :: Ct -> Ct -> Bool
- eqCt c c' = ctFlavour c == ctFlavour c'
- && ctPred c `tcEqType` ctPred c'
+ eq_ct :: Ct -> Ct -> Bool
+ eq_ct c c' = ctFlavour c == ctFlavour c'
+ && ctPred c `tcEqType` ctPred c'
add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
add xs scs = foldl' addOne scs xs
@@ -298,11 +298,8 @@ runTcPluginSolvers solvers all_cts
CtWanted {} -> (givens, (ev,ct):wanteds)
-type WorkItem = Ct
-type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
-
-runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
- -> WorkItem -- The work item
+runSolverPipeline :: [(String, Ct -> SolverStage Ct)] -- The pipeline
+ -> Ct -- The work item
-> TcS ()
-- Run this item down the pipeline, leaving behind new work and inerts
runSolverPipeline full_pipeline workItem
@@ -330,12 +327,12 @@ runSolverPipeline full_pipeline workItem
StartAgain ct -> pprPanic "runSolverPipeline: StartAgain" (ppr ct)
}
where
- run_pipeline :: [(String,SimplifierStage)] -> Ct -> TcS (StopOrContinue Ct)
+ run_pipeline :: [(String, Ct -> SolverStage Ct)] -> 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
+ ; res <- runSolverStage (stage ct)
; traceTcS ("end stage " ++ stage_name ++ " }") (ppr res)
; case res of
Stop {} -> return res
@@ -367,10 +364,10 @@ React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
-}
-thePipeline :: [(String,SimplifierStage)]
-thePipeline = [ ("canonicalization", GHC.Tc.Solver.Canonical.canonicalize)
- , ("interact with inerts", interactWithInertsStage)
- , ("top-level reactions", topReactionsStage) ]
+thePipeline :: [(String, Ct -> SolverStage Ct)]
+thePipeline = [ ("canonicalization", GHC.Tc.Solver.Canonical.canonicalize)
+ , ("interact with inerts", interactWithInertsStage)
+ , ("top-level reactions", topReactionsStage) ]
{-
*********************************************************************************
@@ -407,16 +404,17 @@ or, equivalently,
-- Interaction result of WorkItem <~> Ct
-interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
+interactWithInertsStage :: Ct -> SolverStage Ct
-- Precondition: if the workitem is a CEqCan then it will not be able to
-- react with anything at this stage (except, maybe, via a type family
-- dependency)
interactWithInertsStage wi
- = do { inerts <- getTcSInerts
+ = Stage $
+ do { inerts <- getTcSInerts
; let ics = inert_cans inerts
; case wi of
- CIrredCan {} -> interactIrred ics wi
+ CIrredCan ir_ct -> interactIrred ics ir_ct
CDictCan {} -> interactDict ics wi
CEqCan {} -> continueWith wi -- "Canonicalisation" stage is
-- full solver for equalities
@@ -633,19 +631,20 @@ once had done). This problem can be tickled by typecheck/should_compile/holes.
-- we can rewrite them. We can never improve using this:
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
-- mean that (ty1 ~ ty2)
-interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
+interactIrred :: InertCans -> IrredCt -> TcS (StopOrContinue Ct)
-interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
+interactIrred inerts irred_w@(IrredCt { ir_ev = ev_w, ir_reason = reason })
| isInsolubleReason reason
-- For insolubles, don't allow the constraint to be dropped
-- which can happen with solveOneFromTheOther, so that
-- we get distinct error messages with -fdefer-type-errors
- = continueWith ct_w
+ = carry_on
| let (matching_irreds, others) = findMatchingIrreds (inert_irreds inerts) ev_w
- , ((ct_i, swap) : _rest) <- bagToList matching_irreds
+ , ((irred_i, swap) : _rest) <- bagToList matching_irreds
-- See Note [Multiple matching irreds]
- , let ev_i = ctEvidence ct_i
+ , let ev_i = irredCtEvidence irred_i
+ ct_i = CIrredCan irred_i
= do { traceTcS "iteractIrred" $
vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))
, text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]
@@ -654,62 +653,21 @@ interactIrred inerts ct_w@(CIrredCan { cc_ev = ev_w, cc_reason = reason })
; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }
KeepWork -> do { setEvBindIfWanted ev_i IsCoherent (swap_me swap ev_w)
; updInertIrreds (\_ -> others)
- ; continueWith ct_w } }
+ ; carry_on } }
| otherwise
- = continueWith ct_w
+ = carry_on
where
+ ct_w = CIrredCan irred_w
+ carry_on = continueWith ct_w
+
swap_me :: SwapFlag -> CtEvidence -> EvTerm
swap_me swap ev
= case swap of
NotSwapped -> ctEvTerm ev
IsSwapped -> evCoercion (mkSymCo (evTermCoercion (ctEvTerm ev)))
-interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
-
-findMatchingIrreds :: Cts -> CtEvidence -> (Bag (Ct, SwapFlag), Bag Ct)
-findMatchingIrreds irreds ev
- | EqPred eq_rel1 lty1 rty1 <- classifyPredType pred
- -- See Note [Solving irreducible equalities]
- = partitionBagWith (match_eq eq_rel1 lty1 rty1) irreds
- | otherwise
- = partitionBagWith match_non_eq irreds
- where
- pred = ctEvPred ev
- match_non_eq ct
- | ctPred ct `tcEqTypeNoKindCheck` pred = Left (ct, NotSwapped)
- | otherwise = Right ct
-
- match_eq eq_rel1 lty1 rty1 ct
- | EqPred eq_rel2 lty2 rty2 <- classifyPredType (ctPred ct)
- , eq_rel1 == eq_rel2
- , Just swap <- match_eq_help lty1 rty1 lty2 rty2
- = Left (ct, swap)
- | otherwise
- = Right ct
-
- match_eq_help lty1 rty1 lty2 rty2
- | lty1 `tcEqTypeNoKindCheck` lty2, rty1 `tcEqTypeNoKindCheck` rty2
- = Just NotSwapped
- | lty1 `tcEqTypeNoKindCheck` rty2, rty1 `tcEqTypeNoKindCheck` lty2
- = Just IsSwapped
- | otherwise
- = Nothing
-
-{- Note [Solving irreducible equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (#14333)
- [G] a b ~R# c d
- [W] c d ~R# a b
-Clearly we should be able to solve this! Even though the constraints are
-not decomposable. We solve this when looking up the work-item in the
-irreducible constraints to look for an identical one. When doing this
-lookup, findMatchingIrreds spots the equality case, and matches either
-way around. It has to return a swap-flag so we can generate evidence
-that is the right way round too.
--}
-
{-
*********************************************************************************
* *
@@ -1229,11 +1187,12 @@ I can think of two ways to fix this:
**********************************************************************
-}
-topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
+topReactionsStage :: Ct -> SolverStage Ct
-- The work item does not react with the inert set,
-- so try interaction with top-level instances.
topReactionsStage work_item
- = do { traceTcS "doTopReact" (ppr work_item)
+ = Stage $
+ do { traceTcS "doTopReact" (ppr work_item)
; case work_item of
CDictCan {} ->
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index bfbba18a11..1dce35b00b 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -33,7 +33,7 @@ module GHC.Tc.Solver.Monad (
-- The pipeline
StopOrContinue(..), continueWith, stopWith, andWhenContinue,
- startAgainWith,
+ startAgainWith, SolverStage(Stage, runSolverStage),
-- Tracing etc
panicTcS, traceTcS,
@@ -207,7 +207,7 @@ import GHC.Data.Graph.Directed
********************************************************************* -}
data StopOrContinue a
- = StartAgain a -- Constraint is not solved, but some unifications
+ = StartAgain Ct -- 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
@@ -223,7 +223,23 @@ instance Outputable a => Outputable (StopOrContinue a) where
ppr (ContinueWith w) = text "ContinueWith" <+> ppr w
ppr (StartAgain w) = text "StartAgain" <+> ppr w
-startAgainWith :: a -> TcS (StopOrContinue a)
+newtype SolverStage a = Stage { runSolverStage :: TcS (StopOrContinue a) }
+ deriving( Functor )
+
+instance Applicative SolverStage where
+ pure x = Stage (return (ContinueWith x))
+ (<*>) = ap
+
+instance Monad SolverStage where
+ return = pure
+ (Stage m) >>= k = Stage $
+ do { soc <- m
+ ; case soc of
+ StartAgain x -> return (StartAgain x)
+ Stop ev d -> return (Stop ev d)
+ ContinueWith x -> runSolverStage (k x) }
+
+startAgainWith :: Ct -> TcS (StopOrContinue a)
startAgainWith ct = return (StartAgain ct)
continueWith :: a -> TcS (StopOrContinue a)
@@ -434,7 +450,7 @@ kickOutAfterFillingCoercionHole hole
n_kicked = lengthBag kicked_out
; unless (n_kicked == 0) $
- do { updWorkListTcS (extendWorkListCts kicked_out)
+ do { updWorkListTcS (extendWorkListCts (fmap CIrredCan kicked_out))
; csTraceTcS $
hang (text "Kick out, hole =" <+> ppr hole)
2 (vcat [ text "n-kicked =" <+> int n_kicked
@@ -443,16 +459,16 @@ kickOutAfterFillingCoercionHole hole
; setInertCans ics' }
where
- kick_out :: InertCans -> (Cts, InertCans)
+ kick_out :: InertCans -> (Bag IrredCt, InertCans)
kick_out ics@(IC { inert_irreds = irreds })
= (irreds_to_kick, ics { inert_irreds = irreds_to_keep })
where
(irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds
- kick_ct :: Ct -> Bool
+ kick_ct :: IrredCt -> Bool
-- True: kick out; False: keep.
kick_ct ct
- | CIrredCan { cc_ev = ev, cc_reason = reason } <- ct
+ | IrredCt { ir_ev = ev, ir_reason = reason } <- ct
, CtWanted { ctev_rewriters = RewriterSet rewriters } <- ev
, NonCanonicalReason ctyeq <- reason
, ctyeq `cterHasProblem` cteCoercionHole
@@ -545,7 +561,7 @@ updInertSafehask :: (DictMap Ct -> DictMap Ct) -> TcS ()
updInertSafehask upd_fn
= updInertCans $ \ ics -> ics { inert_safehask = upd_fn (inert_safehask ics) }
-updInertIrreds :: (Cts -> Cts) -> TcS ()
+updInertIrreds :: (Bag IrredCt -> Bag IrredCt) -> TcS ()
-- Modify the inert set with the supplied function
updInertIrreds upd_fn
= updInertCans $ \ ics -> ics { inert_irreds = upd_fn (inert_irreds ics) }
@@ -572,19 +588,20 @@ getInnermostGivenEqLevel = do { inert <- getInertCans
-- want to consider a pattern match that introduces insoluble Givens to be
-- redundant (see Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver).
getInertInsols :: TcS Cts
-getInertInsols = do { inert <- getInertCans
- ; let irreds = inert_irreds inert
- unsats = findDictsByTyConKey (inert_dicts inert) unsatisfiableClassNameKey
- ; return $ unsats `unionBags` filterBag insolubleCt irreds }
+getInertInsols
+ = do { inert <- getInertCans
+ ; let insols = filterBag insolubleIrredCt (inert_irreds inert)
+ unsats = findDictsByTyConKey (inert_dicts inert) unsatisfiableClassNameKey
+ ; return $ unsats `unionBags` fmap CIrredCan insols }
getInertGivens :: TcS [Ct]
-- Returns the Given constraints in the inert set
getInertGivens
= do { inerts <- getInertCans
- ; let all_cts = foldIrreds (:) (inert_irreds inerts)
- $ foldDicts (:) (inert_dicts inerts)
- $ foldFunEqs ((:) . CEqCan) (inert_funeqs inerts)
- $ foldTyEqs ((:) . CEqCan) (inert_eqs inerts)
+ ; let all_cts = foldIrreds ((:) . CIrredCan) (inert_irreds inerts)
+ $ foldDicts (:) (inert_dicts inerts)
+ $ foldFunEqs ((:) . CEqCan) (inert_funeqs inerts)
+ $ foldTyEqs ((:) . CEqCan) (inert_eqs inerts)
$ []
; return (filter isGivenCt all_cts) }
@@ -659,10 +676,10 @@ getUnsolvedInerts
; let unsolved_tv_eqs = foldTyEqs add_if_unsolved_eq tv_eqs emptyCts
unsolved_fun_eqs = foldFunEqs add_if_unsolved_eq fun_eqs emptyCts
- unsolved_irreds = Bag.filterBag isWantedCt irreds
+ unsolved_irreds = Bag.filterBag (isWanted . irredCtEvidence) irreds
unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
- unsolved_others = unionManyBags [ unsolved_irreds
- , unsolved_dicts ]
+ unsolved_others = fmap CIrredCan unsolved_irreds `unionBags`
+ unsolved_dicts
; implics <- getWorkListImplics
@@ -684,9 +701,9 @@ getUnsolvedInerts
add_if_unsolved_eq eq_ct cts | isWanted (eq_ev eq_ct) = CEqCan eq_ct `consCts` cts
| otherwise = cts
-getHasGivenEqs :: TcLevel -- TcLevel of this implication
- -> TcS ( HasGivenEqs -- are there Given equalities?
- , Cts ) -- Insoluble equalities arising from givens
+getHasGivenEqs :: TcLevel -- TcLevel of this implication
+ -> TcS ( HasGivenEqs -- are there Given equalities?
+ , InertIrreds ) -- Insoluble equalities arising from givens
-- See Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
getHasGivenEqs tclvl
= do { inerts@(IC { inert_irreds = irreds
@@ -712,8 +729,9 @@ getHasGivenEqs tclvl
, text "Insols:" <+> ppr given_insols]
; return (has_ge, given_insols) }
where
- insoluble_given_equality ct
- = insolubleEqCt ct && isGivenCt ct
+ insoluble_given_equality :: IrredCt -> Bool
+ insoluble_given_equality irred
+ = insolubleIrredCt irred && isGiven (irredCtEvidence irred)
removeInertCts :: [Ct] -> InertCans -> InertCans
-- ^ Remove inert constraints from the 'InertCans', for use when a
@@ -727,17 +745,11 @@ removeInertCt is ct =
CDictCan { cc_class = cl, cc_tyargs = tys } ->
is { inert_dicts = delDict (inert_dicts is) cl tys }
- CEqCan eq_ct -> delEq is eq_ct
-
- CIrredCan {} -> is { inert_irreds = filterBag (not . eqCt ct) $ inert_irreds is }
-
+ CEqCan eq_ct -> delEq is eq_ct
+ CIrredCan ir_ct -> delIrred is ir_ct
CQuantCan {} -> panic "removeInertCt: CQuantCan"
CNonCanonical {} -> panic "removeInertCt: CNonCanonical"
-eqCt :: Ct -> Ct -> Bool
--- Equality via ctEvId
-eqCt c c' = ctEvId c == ctEvId c'
-
-- | Looks up a family application in the inerts.
lookupFamAppInert :: (CtFlavourRole -> Bool) -- can it rewrite the target?
-> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
@@ -820,15 +832,6 @@ dropFromFamAppCache varset
check redn
= not (anyFreeVarsOfCo (`elemVarSet` varset) $ reductionCoercion redn)
-{- *********************************************************************
-* *
- Irreds
-* *
-********************************************************************* -}
-
-foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
-foldIrreds k irreds z = foldr k z irreds
-
{-
************************************************************************
* *
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 64d590cbe9..0a30379303 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -92,9 +92,9 @@ runRewriteCtEv ev
runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, RewriterSet)
runRewrite loc flav eq_rel thing_inside
= do { rewriters_ref <- newTcRef emptyRewriterSet
- ; let fmode = RE { re_loc = loc
- , re_flavour = flav
- , re_eq_rel = eq_rel
+ ; let fmode = RE { re_loc = loc
+ , re_flavour = flav
+ , re_eq_rel = eq_rel
, re_rewriters = rewriters_ref }
; res <- runRewriteM thing_inside fmode
; rewriters <- readTcRef rewriters_ref
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 9ab842df98..e43b3b16a8 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -18,17 +18,19 @@ module GHC.Tc.Types.Constraint (
isWantedCt, isGivenCt,
isTopLevelUserTypeError, containsUserTypeError, getUserTypeErrorMsg,
isUnsatisfiableCt_maybe,
- ctEvidence, ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
+ ctEvidence, updCtEvidence,
+ ctLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
ctRewriters,
ctEvId, wantedEvId_maybe, mkTcEqPredLikeEv,
- mkNonCanonical, mkNonCanonicalCt, mkGivens,
- mkIrredCt,
+ mkNonCanonical, mkGivens,
ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId,
ctEvRewriters,
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
+ IrredCt(..), mkIrredCt, ctIrredCt, irredCtEvidence, irredCtPred,
+
ExpansionFuel, doNotExpand, consumeFuel, pendingFuel,
assertFuelPrecondition, assertFuelPreconditionStrict,
@@ -54,8 +56,8 @@ module GHC.Tc.Types.Constraint (
isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
addInsols, dropMisleading, addSimples, addImplics, addHoles,
addNotConcreteError, addDelayedErrors,
- tyCoVarsOfWC,
- tyCoVarsOfWCList, insolubleWantedCt, insolubleEqCt, insolubleCt,
+ tyCoVarsOfWC, tyCoVarsOfWCList,
+ insolubleWantedCt, insolubleEqCt, insolubleCt, insolubleIrredCt,
insolubleImplic, nonDefaultableTyVarsOfWC,
Implication(..), implicationPrototype, checkTelescopeSkol,
@@ -207,30 +209,10 @@ data Ct
-- (b) those superclasses are not yet explored
}
- | CIrredCan { -- These stand for yet-unusable predicates
- cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
- cc_reason :: CtIrredReason
-
- -- For the might-be-soluble case, the ctev_pred of the evidence is
- -- of form (tv xi1 xi2 ... xin) with a tyvar at the head
- -- or (lhs1 ~ ty2) where the CEqCan kind invariant (TyEq:K) fails
- -- See Note [CIrredCan constraints]
-
- -- The definitely-insoluble case is for things like
- -- Int ~ Bool tycons don't match
- -- a ~ [a] occurs check
- }
-
- | CNonCanonical { -- See Note [NonCanonical Semantics] in GHC.Tc.Solver.Monad
- cc_ev :: CtEvidence
- }
-
- | CEqCan EqCt -- A canonical equality constraint
-
- | CQuantCan QCInst -- A quantified constraint
- -- NB: I expect to make more of the cases in Ct
- -- look like this, with the payload in an
- -- auxiliary type
+ | CNonCanonical CtEvidence -- See Note [NonCanonical Semantics] in GHC.Tc.Solver.Monad
+ | CIrredCan IrredCt -- A "irreducible" constraint (non-canonical)
+ | CEqCan EqCt -- A canonical equality constraint
+ | CQuantCan QCInst -- A quantified constraint
{- Note [Canonical equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -308,6 +290,29 @@ instance Outputable CanEqLHS where
ppr (TyFamLHS fam_tc fam_args) = ppr (mkTyConApp fam_tc fam_args)
------------
+data IrredCt -- These stand for yet-unusable predicates
+ -- See Note [CIrredCan constraints]
+ = IrredCt { ir_ev :: CtEvidence -- See Note [Ct/evidence invariant]
+ , ir_reason :: CtIrredReason }
+
+mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
+mkIrredCt reason ev = CIrredCan (IrredCt { ir_ev = ev, ir_reason = reason })
+
+irredCtEvidence :: IrredCt -> CtEvidence
+irredCtEvidence = ir_ev
+
+irredCtPred :: IrredCt -> PredType
+irredCtPred = ctEvPred . irredCtEvidence
+
+ctIrredCt :: CtIrredReason -> Ct -> IrredCt
+ctIrredCt _ (CIrredCan ir) = ir
+ctIrredCt reason ct = IrredCt { ir_ev = ctEvidence ct
+ , ir_reason = reason }
+
+instance Outputable IrredCt where
+ ppr irred = ppr (CIrredCan irred)
+
+------------
data QCInst -- A much simplified version of ClsInst
-- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical
= QCI { qci_ev :: CtEvidence -- Always of type forall tvs. context => ty
@@ -461,12 +466,17 @@ data CtIrredReason
-- in GHC.Core.TyCon.
-- INVARIANT: The constraint is an equality constraint between two TyConApps
+ | PluginReason
+ -- ^ a typechecker plugin returned this in the pluginBagCts field
+ -- of TcPluginProgress
+
instance Outputable CtIrredReason where
ppr IrredShapeReason = text "(irred)"
ppr (NonCanonicalReason cter) = ppr cter
ppr ReprEqReason = text "(repr)"
ppr ShapeMismatchReason = text "(shape)"
ppr AbstractTyConReason = text "(abstc)"
+ ppr PluginReason = text "(plugin)"
-- | Are we sure that more solving will never solve this constraint?
isInsolubleReason :: CtIrredReason -> Bool
@@ -475,6 +485,7 @@ isInsolubleReason (NonCanonicalReason cter) = cterIsInsoluble cter
isInsolubleReason ReprEqReason = False
isInsolubleReason ShapeMismatchReason = True
isInsolubleReason AbstractTyConReason = True
+isInsolubleReason PluginReason = True
------------------------------------------------------------------------------
--
@@ -675,13 +686,7 @@ Type-level holes have no evidence at all.
-}
mkNonCanonical :: CtEvidence -> Ct
-mkNonCanonical ev = CNonCanonical { cc_ev = ev }
-
-mkNonCanonicalCt :: Ct -> Ct
-mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
-
-mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
-mkIrredCt reason ev = CIrredCan { cc_ev = ev, cc_reason = reason }
+mkNonCanonical ev = CNonCanonical ev
mkGivens :: CtLoc -> [EvId] -> [Ct]
mkGivens loc ev_ids
@@ -692,9 +697,20 @@ mkGivens loc ev_ids
, ctev_loc = loc })
ctEvidence :: Ct -> CtEvidence
-ctEvidence (CQuantCan (QCI { qci_ev = ev })) = ev
-ctEvidence (CEqCan (EqCt { eq_ev = ev })) = ev
-ctEvidence ct = cc_ev ct
+ctEvidence (CQuantCan (QCI { qci_ev = ev })) = ev
+ctEvidence (CEqCan (EqCt { eq_ev = ev })) = ev
+ctEvidence (CIrredCan (IrredCt { ir_ev = ev })) = ev
+ctEvidence (CNonCanonical ev) = ev
+ctEvidence (CDictCan { cc_ev = ev }) = ev
+
+updCtEvidence :: (CtEvidence -> CtEvidence) -> Ct -> Ct
+updCtEvidence upd ct
+ = case ct of
+ CQuantCan qci@(QCI { qci_ev = ev }) -> CQuantCan (qci { qci_ev = upd ev })
+ CEqCan eq@(EqCt { eq_ev = ev }) -> CEqCan (eq { eq_ev = upd ev })
+ CIrredCan ir@(IrredCt { ir_ev = ev }) -> CIrredCan (ir { ir_ev = upd ev })
+ CNonCanonical ev -> CNonCanonical (upd ev)
+ CDictCan { cc_ev = ev } -> ct { cc_ev = upd ev }
ctLoc :: Ct -> CtLoc
ctLoc = ctEvLoc . ctEvidence
@@ -753,7 +769,7 @@ instance Outputable Ct where
CDictCan { cc_pend_sc = psc }
| psc > 0 -> text "CDictCan" <> parens (text "psc" <+> ppr psc)
| otherwise -> text "CDictCan"
- CIrredCan { cc_reason = reason } -> text "CIrredCan" <> ppr reason
+ CIrredCan (IrredCt { ir_reason = reason }) -> text "CIrredCan" <> ppr reason
CQuantCan (QCI { qci_pend_sc = psc })
| psc > 0 -> text "CQuantCan" <> parens (text "psc" <+> ppr psc)
| otherwise -> text "CQuantCan"
@@ -1168,9 +1184,9 @@ addSimples wc cts
addImplics :: WantedConstraints -> Bag Implication -> WantedConstraints
addImplics wc implic = wc { wc_impl = wc_impl wc `unionBags` implic }
-addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints
-addInsols wc cts
- = wc { wc_simple = wc_simple wc `unionBags` cts }
+addInsols :: WantedConstraints -> Bag IrredCt -> WantedConstraints
+addInsols wc insols
+ = wc { wc_simple = wc_simple wc `unionBags` fmap CIrredCan insols }
addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints
addHoles wc holes
@@ -1305,8 +1321,12 @@ insolubleEqCt :: Ct -> Bool
-- True for Int ~ F a Int
-- but False for Maybe Int ~ F a Int Int
-- (where F is an arity-1 type function)
-insolubleEqCt (CIrredCan { cc_reason = reason }) = isInsolubleReason reason
-insolubleEqCt _ = False
+insolubleEqCt (CIrredCan ir_ct) = insolubleIrredCt ir_ct
+insolubleEqCt _ = False
+
+insolubleIrredCt :: IrredCt -> Bool
+insolubleIrredCt (IrredCt { ir_reason = reason })
+ = isInsolubleReason reason
-- | Returns True of equality constraints that are definitely insoluble,
-- as well as TypeError constraints.
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index 75b74cbb35..12a898ec93 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -105,7 +105,7 @@ module GHC.Tc.Utils.Monad(
chooseUniqueOccTc,
getConstraintVar, setConstraintVar,
emitConstraints, emitStaticConstraints, emitSimple, emitSimples,
- emitImplication, emitImplications, emitInsoluble,
+ emitImplication, emitImplications,
emitDelayedErrors, emitHole, emitHoles, emitNotConcreteError,
discardConstraints, captureConstraints, tryCaptureConstraints,
pushLevelAndCaptureConstraints,
@@ -1825,12 +1825,6 @@ emitImplications ct
do { lie_var <- getConstraintVar ;
updTcRef lie_var (`addImplics` ct) }
-emitInsoluble :: Ct -> TcM ()
-emitInsoluble ct
- = do { traceTc "emitInsoluble" (ppr ct)
- ; lie_var <- getConstraintVar
- ; updTcRef lie_var (`addInsols` unitBag ct) }
-
emitDelayedErrors :: Bag DelayedError -> TcM ()
emitDelayedErrors errs
= do { traceTc "emitDelayedErrors" (ppr errs)
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 7db80cfccb..4d2dcdcba8 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -2463,9 +2463,9 @@ zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
zonkCt (CEqCan (EqCt { eq_ev = ev }))
= mkNonCanonical <$> zonkCtEvidence ev
-zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_reason flag
+zonkCt (CIrredCan ir@(IrredCt { ir_ev = ev })) -- Preserve the cc_reason flag
= do { ev' <- zonkCtEvidence ev
- ; return (ct { cc_ev = ev' }) }
+ ; return (CIrredCan (ir { ir_ev = ev' })) }
zonkCt ct
= do { fl' <- zonkCtEvidence (ctEvidence ct)
@@ -2694,7 +2694,7 @@ zonkTidyFRRInfos = go []
----------------
tidyCt :: TidyEnv -> Ct -> Ct
-- Used only in error reporting
-tidyCt env ct = ct { cc_ev = tidyCtEvidence env (ctEvidence ct) }
+tidyCt env ct = updCtEvidence (tidyCtEvidence env) ct
tidyCtEvidence :: TidyEnv -> CtEvidence -> CtEvidence
-- NB: we do not tidy the ctev_evar field because we don't
@@ -2792,16 +2792,18 @@ naughtyQuantification orig_ty tv escapees
zonkCtRewriterSet :: Ct -> TcM Ct
zonkCtRewriterSet ct
- | isGiven ev = return ct
+ | isGivenCt ct = 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
+ CEqCan eq@(EqCt { eq_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev
+ ; return (CEqCan (eq { eq_ev = ev' })) }
+ CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev
+ ; return (CIrredCan (ir { ir_ev = ev' })) }
+ CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev
+ ; return (CNonCanonical ev') }
+ CDictCan { cc_ev = ev } -> do { ev' <- zonkCtEvRewriterSet ev
+ ; return (ct { cc_ev = ev' }) }
+ CQuantCan {} -> return ct
zonkCtEvRewriterSet :: CtEvidence -> TcM CtEvidence
zonkCtEvRewriterSet ev@(CtGiven {})
View Lorry Controller Status