summaryrefslogtreecommitdiff
path: root/compiler/GHC
diff options
context:
space:
mode:
authorRichard Eisenberg <rae@richarde.dev>2021-04-12 14:46:30 -0400
committerMarge Bot <ben+marge-bot@smart-cactus.org>2021-06-05 10:29:22 -0400
commit8c90e6c758769b068aea2891b26cc17577b6d36a (patch)
tree8915b06885c8938662f8b64f50d3dac37e174519 /compiler/GHC
parent9a28680d2e23e7b25dd7254a439aea31dfae32d5 (diff)
downloadhaskell-8c90e6c758769b068aea2891b26cc17577b6d36a.tar.gz
Fix #19682 by breaking cycles in Deriveds
This commit expands the old Note [Type variable cycles in Givens] to apply as well to Deriveds. See the Note for details and examples. This fixes a regression introduced by my earlier commit that killed off the flattener in favor of the rewriter. A few other things happened along the way: * unifyTest was renamed to touchabilityTest, because that's what it does. * isInsolubleOccursCheck was folded into checkTypeEq, which does much of the same work. To get this to work out, though, we need to keep more careful track of what errors we spot in checkTypeEq, and so CheckTyEqResult has become rather more glorious. * A redundant Note or two was eliminated. * Kill off occCheckForErrors; due to Note [Rewriting synonyms], the extra occCheckExpand here is always redundant. * Store blocked equalities separately from other inerts; less stuff to look through when kicking out. Close #19682. test case: typecheck/should_compile/T19682{,b}
Diffstat (limited to 'compiler/GHC')
-rw-r--r--compiler/GHC/Tc/Errors.hs54
-rw-r--r--compiler/GHC/Tc/Solver/Canonical.hs582
-rw-r--r--compiler/GHC/Tc/Solver/InertSet.hs29
-rw-r--r--compiler/GHC/Tc/Solver/Interact.hs22
-rw-r--r--compiler/GHC/Tc/Solver/Monad.hs243
-rw-r--r--compiler/GHC/Tc/Types/Constraint.hs205
-rw-r--r--compiler/GHC/Tc/Types/Origin.hs8
-rw-r--r--compiler/GHC/Tc/Utils/TcMType.hs8
-rw-r--r--compiler/GHC/Tc/Utils/TcType.hs51
-rw-r--r--compiler/GHC/Tc/Utils/Unify.hs191
10 files changed, 824 insertions, 569 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index 3a77998c8f..f3c8a19b04 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -19,9 +19,9 @@ import GHC.Tc.Utils.Monad
import GHC.Tc.Types.Constraint
import GHC.Core.Predicate
import GHC.Tc.Utils.TcMType
-import GHC.Tc.Utils.Unify( occCheckForErrors, CheckTyEqResult(..) )
import GHC.Tc.Utils.Env( tcInitTidyEnv )
import GHC.Tc.Utils.TcType
+import GHC.Tc.Utils.Unify ( checkTyVarEq )
import GHC.Tc.Types.Origin
import GHC.Rename.Unbound ( unknownNameSuggestions, WhatLooking(..) )
import GHC.Core.Type
@@ -600,10 +600,10 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
, ("Irreds", is_irred, False, mkGroupReporter mkIrredErr)
, ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ]
- -- also checks to make sure the constraint isn't BlockedCIS
+ -- also checks to make sure the constraint isn't HoleBlockerReason
-- See TcCanonical Note [Equalities with incompatible kinds], (4)
unblocked :: (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
- unblocked _ (CIrredCan { cc_status = BlockedCIS {}}) _ = False
+ unblocked _ (CIrredCan { cc_reason = HoleBlockerReason {}}) _ = False
unblocked checker ct pred = checker ct pred
-- rigid_nom_eq, rigid_nom_tv_eq,
@@ -1544,6 +1544,22 @@ mkTyVarEqErr ctxt report ct tv1 ty2
mkTyVarEqErr' :: DynFlags -> ReportErrCtxt -> Report -> Ct
-> TcTyVar -> TcType -> Report
mkTyVarEqErr' dflags ctxt report ct tv1 ty2
+ -- impredicativity is a simple error to understand; try it first
+ | check_eq_result `cterHasProblem` cteImpredicative
+ = let msg = vcat [ (if isSkolemTyVar tv1
+ then text "Cannot equate type variable"
+ else text "Cannot instantiate unification variable")
+ <+> quotes (ppr tv1)
+ , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ]
+ in
+ -- Unlike the other reports, this discards the old 'report_important'
+ -- instead of augmenting it. This is because the details are not likely
+ -- to be helpful since this is just an unimplemented feature.
+ mconcat [ headline_msg
+ , important msg
+ , if isSkolemTyVar tv1 then extraTyVarEqInfo ctxt tv1 ty2 else mempty
+ , report ]
+
| isSkolemTyVar tv1 -- ty2 won't be a meta-tyvar; we would have
-- swapped in Solver.Canonical.canEqTyVarHomo
|| isTyVarTyVar tv1 && not (isTyVarTy ty2)
@@ -1555,11 +1571,10 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2
, report
]
- | CTE_Occurs <- occ_check_expand
+ | cterHasOccursCheck check_eq_result
-- We report an "occurs check" even for a ~ F t a, where F is a type
-- function; it's not insoluble (because in principle F could reduce)
-- but we have certainly been unable to solve it
- -- See Note [Occurs check error] in GHC.Tc.Solver.Canonical
= let extra2 = mkEqInfoMsg ct ty1 ty2
interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
@@ -1576,16 +1591,6 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2
in
mconcat [headline_msg, extra2, extra3, report]
- | CTE_Bad <- occ_check_expand
- = let msg = vcat [ text "Cannot instantiate unification variable"
- <+> quotes (ppr tv1)
- , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ]
- in
- -- Unlike the other reports, this discards the old 'report_important'
- -- instead of augmenting it. This is because the details are not likely
- -- to be helpful since this is just an unimplemented feature.
- mconcat [ headline_msg, important msg, report ]
-
-- If the immediately-enclosing implication has 'tv' a skolem, and
-- we know by now its an InferSkol kind of skolem, then presumably
-- it started life as a TyVarTv, else it'd have been unified, given
@@ -1647,15 +1652,24 @@ mkTyVarEqErr' dflags ctxt report ct tv1 ty2
| otherwise
= reportEqErr ctxt report ct (mkTyVarTy tv1) ty2
- -- This *can* happen (#6123, and test T2627b)
+ -- This *can* happen (#6123)
-- Consider an ambiguous top-level constraint (a ~ F a)
-- Not an occurs check, because F is a type function.
where
headline_msg = misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2
ty1 = mkTyVarTy tv1
- occ_check_expand = occCheckForErrors dflags tv1 ty2
- insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
+
+ check_eq_result = case ct of
+ CIrredCan { cc_reason = NonCanonicalReason result } -> result
+ CIrredCan { cc_reason = HoleBlockerReason {} } -> cteProblem cteHoleBlocker
+ _ -> checkTyVarEq dflags tv1 ty2
+ -- in T2627b, we report an error for F (F a0) ~ a0. Note that the type
+ -- variable is on the right, so we don't get useful info for the CIrredCan,
+ -- and have to compute the result of checkTyVarEq here.
+
+
+ insoluble_occurs_check = check_eq_result `cterHasProblem` cteInsolubleOccurs
what = text $ levelString $
ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel
@@ -2073,8 +2087,6 @@ pprWithExplicitKindsWhenMismatch ty1 ty2 ct
-- True when the visible bit of the types look the same,
-- so we want to show the kinds in the displayed type
-
-
{- Note [Insoluble occurs check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider [G] a ~ [a], [W] a ~ [a] (#13674). The Given is insoluble
@@ -2085,7 +2097,7 @@ we don't solve it from the Given. It's very confusing to say
And indeed even thinking about the Givens is silly; [W] a ~ [a] is
just as insoluble as Int ~ Bool.
-Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
+Conclusion: if there's an insoluble occurs check (cteInsolubleOccurs)
then report it directly, not in the "cannot deduce X from Y" form.
This is done in misMatchOrCND (via the insoluble_occurs_check arg)
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 11606401c8..a17b7f0204 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -4,7 +4,7 @@
module GHC.Tc.Solver.Canonical(
canonicalize,
- unifyDerived, unifyTest, UnifyTestResult(..),
+ unifyDerived,
makeSuperClasses,
StopOrContinue(..), stopWith, continueWith, andWhenContinue,
solveCallStack -- For GHC.Tc.Solver
@@ -40,7 +40,6 @@ import GHC.Utils.Outputable
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Builtin.Types ( anyTypeOfKind )
-import GHC.Driver.Session( DynFlags )
import GHC.Types.Name.Set
import GHC.Types.Name.Reader
import GHC.Hs.Type( HsIPName(..) )
@@ -51,8 +50,7 @@ import GHC.Data.Bag
import GHC.Utils.Monad
import Control.Monad
import Data.Maybe ( isJust, isNothing )
-import Data.List ( zip4, partition )
-import GHC.Types.Unique.Set( nonDetEltsUniqSet )
+import Data.List ( zip4 )
import GHC.Types.Basic
import Data.Bifunctor ( bimap )
@@ -724,7 +722,7 @@ canIrred ev
do traceTcS "canEvNC:forall" (ppr pred)
canForAllNC ev tvs th p
IrredPred {} -> continueWith $
- mkIrredCt OtherCIS new_ev } }
+ mkIrredCt IrredShapeReason new_ev } }
{- *********************************************************************
* *
@@ -1094,8 +1092,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 -> continueWith (mkIrredCt OtherCIS ev)
- NomEq -> continueWith (mkIrredCt InsolubleCIS ev) }
+ ReprEq -> continueWith (mkIrredCt ReprEqReason ev)
+ NomEq -> continueWith (mkIrredCt ShapeMismatchReason ev) }
-- No need to call canEqFailure/canEqHardFailure because they
-- rewrite, and the types involved here are already rewritten
@@ -1575,10 +1573,10 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
else canEqFailure ev eq_rel ty1 ty2 }
- -- See Note [Skolem abstract data] (at tyConSkolem)
+ -- See Note [Skolem abstract data] in GHC.Core.Tycon
| tyConSkolem tc1 || tyConSkolem tc2
= do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2)
- ; continueWith (mkIrredCt OtherCIS ev) }
+ ; continueWith (mkIrredCt AbstractTyConReason ev) }
-- Fail straight away for better error messages
-- See Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1920,7 +1918,7 @@ canEqFailure ev ReprEq ty1 ty2
; traceTcS "canEqFailure with ReprEq" $
vcat [ ppr ev, ppr ty1, ppr ty2, ppr xi1, ppr xi2 ]
; new_ev <- rewriteEqEvidence ev NotSwapped xi1 xi2 co1 co2
- ; continueWith (mkIrredCt OtherCIS new_ev) }
+ ; continueWith (mkIrredCt ReprEqReason new_ev) }
-- | Call when canonicalizing an equality fails with utterly no hope.
canEqHardFailure :: CtEvidence
@@ -1931,7 +1929,7 @@ canEqHardFailure ev ty1 ty2
; (s1, co1) <- rewrite ev ty1
; (s2, co2) <- rewrite ev ty2
; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2
- ; continueWith (mkIrredCt InsolubleCIS new_ev) }
+ ; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
{-
Note [Decomposing TyConApps]
@@ -2015,22 +2013,6 @@ and the Id newtype is unwrapped. This is assured by requiring only rewritten
types in canEqCanLHS *and* having the newtype-unwrapping check above
the tyvar check in can_eq_nc.
-Note [Occurs check error]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have an occurs check error, are we necessarily hosed? Say our
-tyvar is tv1 and the type it appears in is xi2. Because xi2 is function
-free, then if we're computing w.r.t. nominal equality, then, yes, we're
-hosed. Nothing good can come from (a ~ [a]). If we're computing w.r.t.
-representational equality, this is a little subtler. Once again, (a ~R [a])
-is a bad thing, but (a ~R N a) for a newtype N might be just fine. This
-means also that (a ~ b a) might be fine, because `b` might become a newtype.
-
-So, we must check: does tv1 appear in xi2 under any type constructor
-that is generative w.r.t. representational equality? That's what
-isInsolubleOccursCheck does.
-
-See also #10715, which induced this addition.
-
Note [Put touchable variables on the left]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Ticket #10009, a very nasty example:
@@ -2254,10 +2236,10 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
-- If we have F a ~ F (F a), we want to swap.
swap_for_occurs
- | CTE_OK <- checkTyFamEq dflags fun_tc2 fun_args2
- (mkTyConApp fun_tc1 fun_args1)
- , CTE_Occurs <- checkTyFamEq dflags fun_tc1 fun_args1
- (mkTyConApp fun_tc2 fun_args2)
+ | cterHasNoProblem $ checkTyFamEq dflags fun_tc2 fun_args2
+ (mkTyConApp fun_tc1 fun_args1)
+ , cterHasOccursCheck $ checkTyFamEq dflags fun_tc1 fun_args1
+ (mkTyConApp fun_tc2 fun_args2)
= True
| otherwise
@@ -2299,10 +2281,11 @@ canEqTyVarFunEq :: CtEvidence -- :: lhs ~ (rhs |> mco)
-> MCoercion -- :: kind(rhs) ~N kind(lhs)
-> TcS (StopOrContinue Ct)
canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
- = do { can_unify <- unifyTest ev tv1 rhs
- ; dflags <- getDynFlags
- ; if | case can_unify of { NoUnify -> False; _ -> True }
- , CTE_OK <- checkTyVarEq dflags YesTypeFamilies tv1 rhs
+ = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv1 rhs
+ ; dflags <- getDynFlags
+ ; if | case is_touchable of { Untouchable -> False; _ -> True }
+ , cterHasNoProblem $
+ checkTyVarEq dflags tv1 rhs `cterRemoveProblem` cteTypeFamily
-> canEqCanLHSFinish ev eq_rel swapped (TyVarLHS tv1) rhs
| otherwise
@@ -2316,82 +2299,6 @@ canEqTyVarFunEq ev eq_rel swapped tv1 ps_xi1 fun_tc2 fun_args2 ps_xi2 mco
sym_mco = mkTcSymMCo mco
rhs = ps_xi2 `mkCastTyMCo` mco
-data UnifyTestResult
- -- See Note [Solve by unification] in GHC.Tc.Solver.Interact
- -- which points out that having UnifySameLevel is just an optimisation;
- -- we could manage with UnifyOuterLevel alone (suitably renamed)
- = UnifySameLevel
- | UnifyOuterLevel [TcTyVar] -- Promote these
- TcLevel -- ..to this level
- | NoUnify
-
-instance Outputable UnifyTestResult where
- ppr UnifySameLevel = text "UnifySameLevel"
- ppr (UnifyOuterLevel tvs lvl) = text "UnifyOuterLevel" <> parens (ppr lvl <+> ppr tvs)
- ppr NoUnify = text "NoUnify"
-
-unifyTest :: CtEvidence -> TcTyVar -> TcType -> TcS UnifyTestResult
--- This is the key test for untouchability:
--- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
--- and Note [Solve by unification] in GHC.Tc.Solver.Interact
-unifyTest ev tv1 rhs
- | not (isGiven ev) -- See Note [Do not unify Givens]
- , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1
- , canSolveByUnification info rhs
- = do { ambient_lvl <- getTcLevel
- ; given_eq_lvl <- getInnermostGivenEqLevel
-
- ; if | tv_lvl `sameDepthAs` ambient_lvl
- -> return UnifySameLevel
-
- | tv_lvl `deeperThanOrSame` given_eq_lvl -- No intervening given equalities
- , all (does_not_escape tv_lvl) free_skols -- No skolem escapes
- -> return (UnifyOuterLevel free_metas tv_lvl)
-
- | otherwise
- -> return NoUnify }
- | otherwise
- = return NoUnify
- where
- (free_metas, free_skols) = partition isPromotableMetaTyVar $
- nonDetEltsUniqSet $
- tyCoVarsOfType rhs
-
- does_not_escape tv_lvl fv
- | isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv
- | otherwise = True
- -- Coercion variables are not an escape risk
- -- If an implication binds a coercion variable, it'll have equalities,
- -- so the "intervening given equalities" test above will catch it
- -- Coercion holes get filled with coercions, so again no problem.
-
-{- Note [Do not unify Givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this GADT match
- data T a where
- T1 :: T Int
- ...
-
- f x = case x of
- T1 -> True
- ...
-
-So we get f :: T alpha[1] -> beta[1]
- x :: T alpha[1]
-and from the T1 branch we get the implication
- forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool
-
-Now, clearly we don't want to unify alpha:=Int! Yet at the moment we
-process [G] alpha[1] ~ Int, we don't have any given-equalities in the
-inert set, and hence there are no given equalities to make alpha untouchable.
-
-NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that
-never happens: invariant (GivenInv) in Note [TcLevel invariants]
-in GHC.Tc.Utils.TcType.
-
-Simple solution: never unify in Givens!
--}
-
-- The RHS here is either not CanEqLHS, or it's one that we
-- want to rewrite the LHS to (as per e.g. swapOverTyVars)
canEqCanLHSFinish :: CtEvidence
@@ -2403,52 +2310,71 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
-- RHS is fully rewritten, but with type synonyms
-- preserved as much as possible
-- guaranteed that tyVarKind lhs == typeKind rhs, for (TyEq:K)
--- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqTyVarHomo
+-- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqCanLHS2
= do { dflags <- getDynFlags
; new_ev <- rewriteEqEvidence ev swapped lhs_ty rhs rewrite_co1 rewrite_co2
+ -- by now, (TyEq:K) is already satisfied
+ ; massert (canEqLHSKind lhs `eqType` tcTypeKind rhs)
+
+ -- by now, (TyEq:N) is already satisfied (if applicable)
+ ; massert (not bad_newtype)
+
+ -- guarantees (TyEq:OC), (TyEq:F)
-- Must do the occurs check even on tyvar/tyvar
- -- equalities, in case have x ~ (y :: ..x...)
- -- #12593
- -- guarantees (TyEq:OC), (TyEq:F), and (TyEq:H)
- -- this next line checks also for coercion holes (TyEq:H); see
- -- Note [Equalities with incompatible kinds]
- ; case canEqOK dflags eq_rel lhs rhs of
- CanEqOK ->
- do { traceTcS "canEqOK" (ppr lhs $$ ppr rhs)
- ; continueWith (CEqCan { cc_ev = new_ev, cc_lhs = lhs
- , cc_rhs = rhs, cc_eq_rel = eq_rel }) }
- -- it is possible that cc_rhs mentions the LHS if the LHS is a type
- -- family. This will cause later rewriting to potentially loop, but
- -- that will be caught by the depth counter. The other option is an
- -- occurs-check for a function application, which seems awkward.
-
- CanEqNotOK status
- -- See Note [Type variable cycles in Givens]
- | OtherCIS <- status
- , Given <- ctEvFlavour ev
- , TyVarLHS lhs_tv <- lhs
- , not (isCycleBreakerTyVar lhs_tv) -- See Detail (7) of Note
- , NomEq <- eq_rel
- -> do { traceTcS "canEqCanLHSFinish breaking a cycle" (ppr lhs $$ ppr rhs)
- ; new_rhs <- breakTyVarCycle (ctEvLoc ev) rhs
- ; traceTcS "new RHS:" (ppr new_rhs)
- ; let new_pred = mkPrimEqPred (mkTyVarTy lhs_tv) new_rhs
- new_new_ev = new_ev { ctev_pred = new_pred }
- -- See Detail (6) of Note [Type variable cycles in Givens]
-
- ; if anyRewritableTyVar True NomEq (\ _ tv -> tv == lhs_tv) new_rhs
- then do { traceTcS "Note [Type variable cycles in Givens] Detail (1)"
- (ppr new_new_ev)
- ; continueWith (mkIrredCt status new_ev) }
- else continueWith (CEqCan { cc_ev = new_new_ev, cc_lhs = lhs
- , cc_rhs = new_rhs, cc_eq_rel = eq_rel }) }
-
- -- We must not use it for further rewriting!
- | otherwise
- -> do { traceTcS "canEqCanLHSFinish can't make a canonical" (ppr lhs $$ ppr rhs)
- ; continueWith (mkIrredCt status new_ev) } }
+ -- equalities, in case have x ~ (y :: ..x...); this is #12593.
+ -- This next line checks also for coercion holes (TyEq:H); see
+ -- Note [Equalities with incompatible kinds]
+ ; let result0 = checkTypeEq dflags lhs rhs `cterRemoveProblem` cteTypeFamily
+ -- type families are OK here
+ -- NB: no occCheckExpand here; see Note [Rewriting synonyms] in GHC.Tc.Solver.Rewrite
+
+
+ -- a ~R# b a is soluble if b later turns out to be Identity
+ result = case eq_rel of
+ NomEq -> result0
+ ReprEq -> cterSetOccursCheckSoluble result0
+
+ reason | result `cterHasOnlyProblem` cteHoleBlocker
+ = HoleBlockerReason (coercionHolesOfType rhs)
+ | otherwise
+ = NonCanonicalReason result
+
+ ; if cterHasNoProblem result
+ then do { traceTcS "CEqCan" (ppr lhs $$ ppr rhs)
+ ; continueWith (CEqCan { cc_ev = new_ev, cc_lhs = lhs
+ , cc_rhs = rhs, cc_eq_rel = eq_rel }) }
+
+ else do { m_stuff <- breakTyVarCycle_maybe ev result lhs rhs
+ -- See Note [Type variable cycles];
+ -- returning Nothing is the vastly common case
+ ; case m_stuff of
+ { Nothing ->
+ do { traceTcS "canEqCanLHSFinish can't make a canonical"
+ (ppr lhs $$ ppr rhs)
+ ; continueWith (mkIrredCt reason new_ev) }
+ ; Just (lhs_tv, co, new_rhs) ->
+ do { traceTcS "canEqCanLHSFinish breaking a cycle" $
+ ppr lhs $$ ppr rhs
+ ; traceTcS "new RHS:" (ppr new_rhs)
+
+ -- This check is Detail (1) in the Note
+ ; if cterHasOccursCheck (checkTyVarEq dflags lhs_tv new_rhs)
+
+ then do { traceTcS "Note [Type variable cycles] Detail (1)"
+ (ppr new_rhs)
+ ; continueWith (mkIrredCt reason new_ev) }
+
+ else do { -- See Detail (6) of Note [Type variable cycles]
+ new_new_ev <- rewriteEqEvidence new_ev NotSwapped
+ lhs_ty new_rhs
+ (mkTcNomReflCo lhs_ty) co
+
+ ; continueWith (CEqCan { cc_ev = new_new_ev
+ , cc_lhs = lhs
+ , cc_rhs = new_rhs
+ , cc_eq_rel = eq_rel }) }}}}}
where
role = eqRelRole eq_rel
@@ -2457,6 +2383,13 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
rewrite_co1 = mkTcReflCo role lhs_ty
rewrite_co2 = mkTcReflCo role rhs
+ -- This is about (TyEq:N)
+ bad_newtype | ReprEq <- eq_rel
+ , Just tc <- tyConAppTyCon_maybe rhs
+ = isNewTyCon tc
+ | otherwise
+ = False
+
-- | Solve a reflexive equality constraint
canEqReflexive :: CtEvidence -- ty ~ ty
-> EqRel
@@ -2486,77 +2419,6 @@ rewriteCastedEquality ev eq_rel swapped lhs rhs mco
sym_mco = mkTcSymMCo mco
role = eqRelRole eq_rel
----------------------------------------------
--- | Result of checking whether a RHS is suitable for pairing
--- with a CanEqLHS in a CEqCan.
-data CanEqOK
- = CanEqOK -- RHS is good
- | CanEqNotOK CtIrredStatus -- don't proceed; explains why
-
-instance Outputable CanEqOK where
- ppr CanEqOK = text "CanEqOK"
- ppr (CanEqNotOK status) = text "CanEqNotOK" <+> ppr status
-
--- | This function establishes most of the invariants needed to make
--- a CEqCan.
---
--- TyEq:OC: Checked here.
--- TyEq:F: Checked here.
--- TyEq:K: assumed; ASSERTed here (that is, kind(lhs) = kind(rhs))
--- TyEq:N: assumed; ASSERTed here (if eq_rel is R, rhs is not a newtype)
--- TyEq:TV: not checked (this is hard to check)
--- TyEq:H: Checked here.
-canEqOK :: DynFlags -> EqRel -> CanEqLHS -> Xi -> CanEqOK
-canEqOK dflags eq_rel lhs rhs
- = assert good_rhs $
- case checkTypeEq dflags YesTypeFamilies lhs rhs of
- CTE_OK -> CanEqOK
- CTE_Bad -> CanEqNotOK OtherCIS
- -- Violation of TyEq:F
-
- CTE_HoleBlocker -> CanEqNotOK (BlockedCIS holes)
- where holes = coercionHolesOfType rhs
- -- This is the case detailed in
- -- Note [Equalities with incompatible kinds]
- -- Violation of TyEq:H
-
- -- These are both a violation of TyEq:OC, but we
- -- want to differentiate for better production of
- -- error messages
- CTE_Occurs | TyVarLHS tv <- lhs
- , isInsolubleOccursCheck eq_rel tv rhs -> CanEqNotOK InsolubleCIS
- -- If we have a ~ [a], it is not canonical, and in particular
- -- we don't want to rewrite existing inerts with it, otherwise
- -- we'd risk divergence in the constraint solver
-
- -- NB: no occCheckExpand here; see Note [Rewriting synonyms]
- -- in GHC.Tc.Solver.Rewrite
-
- | otherwise -> CanEqNotOK OtherCIS
- -- A representational equality with an occurs-check problem isn't
- -- insoluble! For example:
- -- a ~R b a
- -- We might learn that b is the newtype Id.
- -- But, the occurs-check certainly prevents the equality from being
- -- canonical, and we might loop if we were to use it in rewriting.
-
- -- This case also include type family occurs-check errors, which
- -- are not generally insoluble
-
- where
- good_rhs = kinds_match && not bad_newtype
-
- lhs_kind = canEqLHSKind lhs
- rhs_kind = tcTypeKind rhs
-
- kinds_match = lhs_kind `tcEqType` rhs_kind
-
- bad_newtype | ReprEq <- eq_rel
- , Just tc <- tyConAppTyCon_maybe rhs
- = isNewTyCon tc
- | otherwise
- = False
-
{- Note [Equalities with incompatible kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
What do we do when we have an equality
@@ -2583,7 +2445,7 @@ that is, it should be put aside, and not used to rewrite any other constraint,
until the kind-equality on which it depends (namely 'co' above) is solved.
To achieve this
* The [X] constraint is a CIrredCan
-* With a cc_status of BlockedCIS bchs
+* With a cc_reason of HoleBlockerReason bchs
* Where 'bchs' is the set of "blocking coercion holes". The blocking coercion
holes are the free coercion holes of [X]'s type
* When all the blocking coercion holes in the CIrredCan are filled (solved),
@@ -2608,14 +2470,15 @@ Wrinkles:
So, we have an invariant on CEqCan (TyEq:H) that the RHS does not have
any coercion holes. This is checked in checkTypeEq. Any equalities that
- have such an RHS are turned into CIrredCans with a BlockedCIS status. We also
+ have such an RHS are turned into CIrredCans with a HoleBlockerReason. We also
must be sure to kick out any such CIrredCan constraints that mention coercion holes
when those holes get filled in, so that the unification step can now proceed.
- The kicking out is done in kickOutAfterFillingCoercionHole.
+ The kicking out is done in kickOutAfterFillingCoercionHole, and the inerts
+ are stored in the inert_blocked field of InertCans.
However, we must be careful: we kick out only when no coercion holes are
- left. The holes in the type are stored in the BlockedCIS CtIrredStatus.
+ left. The holes in the type are stored in the HoleBlockerReason CtIrredReason.
The extra check that there are no more remaining holes avoids
needless work when rewriting evidence (which fills coercion holes) and
aids efficiency.
@@ -2658,7 +2521,7 @@ Wrinkles:
cast appears opposite a tyvar. This is implemented in the cast case
of can_eq_nc'.
- (4) Reporting an error for a constraint that is blocked with status BlockedCIS
+ (4) Reporting an error for a constraint that is blocked with HoleBlockerReason
is hard: what would we say to users? And we don't
really need to report, because if a constraint is blocked, then
there is unsolved wanted blocking it; that unsolved wanted will
@@ -2668,7 +2531,7 @@ Wrinkles:
(4a) It would seem possible to do this filtering just based on the
presence of a blocking coercion hole. However, this is no good,
as it suppresses e.g. no-instance-found errors. We thus record
- a CtIrredStatus in CIrredCan and filter based on this status.
+ a CtIrredReason in CIrredCan and filter based on this status.
This happened in T14584. An alternative approach is to expressly
look for *equalities* with blocking coercion holes, but actually
recording the blockage in a status field seems nicer.
@@ -2725,53 +2588,70 @@ NOT (necessarily) expand the type synonym, since for the purpose of
good error messages we want to leave type synonyms unexpanded as much
as possible. Hence the ps_xi1, ps_xi2 argument passed to canEqCanLHS.
-Note [Type variable cycles in Givens]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Type variable cycles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider this situation (from indexed-types/should_compile/GivenLoop):
instance C (Maybe b)
- [G] a ~ Maybe (F a)
+ *[G] a ~ Maybe (F a)
[W] C a
-In order to solve the Wanted, we must use the Given to rewrite `a` to
-Maybe (F a). But note that the Given has an occurs-check failure, and
-so we can't straightforwardly add the Given to the inert set.
+or (typecheck/should_compile/T19682b):
+
+ instance C (a -> b)
+ *[WD] alpha ~ (Arg alpha -> Res alpha)
+ [W] C alpha
-The key idea is to replace the (F a) in the RHS of the Given with a
-fresh variable, which we'll call a CycleBreakerTv, or cbv. Then, emit
-a new Given to connect cbv with F a. So our situation becomes
+In order to solve the final Wanted, we must use the starred constraint
+for rewriting. But note that both starred constraints have occurs-check failures,
+and so we can't straightforwardly add these to the inert set and
+use them for rewriting. (NB: A rigid type constructor is at the
+top of both RHSs. If the type family were at the top, we'd just reorient
+in canEqTyVarFunEq.)
+
+The key idea is to replace the type family applications in the RHS of the
+starred constraints with a fresh variable, which we'll call a cycle-breaker
+variable, or cbv. Then, relate the cbv back with the original type family application
+via new equality constraints. Our situations thus become:
instance C (Maybe b)
[G] a ~ Maybe cbv
[G] F a ~ cbv
[W] C a
-Note the orientation of the second Given. The type family ends up
-on the left; see commentary on canEqTyVarFunEq, which decides how to
-orient such cases. No special treatment for CycleBreakerTvs is
-necessary. This scenario is now easily soluble, by using the first
-Given to rewrite the Wanted, which can now be solved.
+or
-(The first Given actually also rewrites the second one. This causes
-no trouble.)
+ instance C (a -> b)
+ [WD] alpha ~ (cbv1 -> cbv2)
+ [WD] Arg alpha ~ cbv1
+ [WD] Res alpha ~ cbv2
+ [W] C alpha
-More generally, we detect this scenario by the following characteristics:
- - a Given CEqCan constraint
- - with a tyvar on its LHS
- - with a soluble occurs-check failure
- - and a nominal equality
+This transformation (creating the new types and emitting new equality
+constraints) is done in breakTyVarCycle_maybe.
+
+The details depend on whether we're working with a Given or a Derived.
+(Note that the Wanteds are really WDs, above. This is because Wanteds
+are not used for rewriting.)
+
+Given
+-----
-Having identified the scenario, we wish to replace all type family
-applications on the RHS with fresh metavariables (with MetaInfo
-CycleBreakerTv). This is done in breakTyVarCycle. These metavariables are
-untouchable, but we also emit Givens relating the fresh variables to the type
-family applications they replace.
+We emit a new Given, [G] F a ~ cbv, equating the type family application to
+our new cbv. Note its orientation: The type family ends up on the left; see
+commentary on canEqTyVarFunEq, which decides how to orient such cases. No
+special treatment for CycleBreakerTvs is necessary. This scenario is now
+easily soluble, by using the first Given to rewrite the Wanted, which can now
+be solved.
+
+(The first Given actually also rewrites the second one, giving
+[G] F (Maybe cbv) ~ cbv, but this causes no trouble.)
Of course, we don't want our fresh variables leaking into e.g. error messages.
So we fill in the metavariables with their original type family applications
after we're done running the solver (in nestImplicTcS and runTcSWithEvBinds).
This is done by restoreTyVarCycles, which uses the inert_cycle_breakers field in
-InertSet, which contains the pairings invented in breakTyVarCycle.
+InertSet, which contains the pairings invented in breakTyVarCycle_maybe.
That is:
@@ -2796,27 +2676,124 @@ Note that
* The evidence for the new `F a ~ cbv` constraint is Refl, because we know this fill-in is
ultimately going to happen.
-There are drawbacks of this approach:
+Wanted/Derived
+--------------
+The fresh cycle-breaker variables here must actually be normal, touchable
+metavariables. That is, they are TauTvs. Nothing at all unusual. Repeating
+the example from above, we have
+
+ *[WD] alpha ~ (Arg alpha -> Res alpha)
+
+and we turn this into
+
+ *[WD] alpha ~ (cbv1 -> cbv2)
+ [WD] Arg alpha ~ cbv1
+ [WD] Res alpha ~ cbv2
+
+where cbv1 and cbv2 are fresh TauTvs. Why TauTvs? See [Why TauTvs] below.
+
+Critically, we emit the constraint directly instead of calling unifyWanted.
+Next, we unify alpha := cbv1 -> cbv2, having eliminated the occurs check. This
+unification happens in the course of normal behavior of top-level
+interactions, later in the solver pipeline. We know this unification will
+indeed happen, because breakTyVarCycle_maybe, which decides whether to apply
+this logic, goes to pains to make sure unification will succeed. Now, we're
+here (including further context from our original example, from the top of the
+Note):
+
+ instance C (a -> b)
+ [WD] Arg (cbv1 -> cbv2) ~ cbv1
+ [WD] Res (cbv1 -> cbv2) ~ cbv2
+ [W] C (cbv1 -> cbv2)
+
+The first two WD constraints reduce to reflexivity and are discarded,
+and the last is easily soluble.
+
+[Why TauTvs]:
+Let's look at another example (typecheck/should_compile/T19682) where we need
+to unify the cbvs:
+
+ class (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
+ instance (AllEqF xs ys, SameShapeAs xs ys) => AllEq xs ys
+
+ type family SameShapeAs xs ys :: Constraint where
+ SameShapeAs '[] ys = (ys ~ '[])
+ SameShapeAs (x : xs) ys = (ys ~ (Head ys : Tail ys))
+
+ type family AllEqF xs ys :: Constraint where
+ AllEqF '[] '[] = ()
+ AllEqF (x : xs) (y : ys) = (x ~ y, AllEq xs ys)
+
+ [WD] alpha ~ (Head alpha : Tail alpha)
+ [WD] AllEqF '[Bool] alpha
+
+Without the logic detailed in this Note, we're stuck here, as AllEqF cannot
+reduce and alpha cannot unify. Let's instead apply our cycle-breaker approach,
+just as described above. We thus invent cbv1 and cbv2 and unify
+alpha := cbv1 -> cbv2, yielding (after zonking)
+
+ [WD] Head (cbv1 : cbv2) ~ cbv1
+ [WD] Tail (cbv1 : cbv2) ~ cbv2
+ [WD] AllEqF '[Bool] (cbv1 : cbv2)
- 1. We apply this trick only for Givens, never for Wanted or Derived.
- It wouldn't make sense for Wanted, because Wanted never rewrite.
- But it's conceivable that a Derived would benefit from this all.
- I doubt it would ever happen, though, so I'm holding off.
+The first two WD constraints simplify to reflexivity and are discarded.
+But the last reduces:
- 2. We don't use this trick for representational equalities, as there
- is no concrete use case where it is helpful (unlike for nominal
- equalities). Furthermore, because function applications can be
- CanEqLHSs, but newtype applications cannot, the disparities between
- the cases are enough that it would be effortful to expand the idea
- to representational equalities. A quick attempt, with
+ [WD] Bool ~ cbv1
+ [WD] AllEq '[] cbv2
+
+The first of these is solved by unification: cbv1 := Bool. The second
+is solved by the instance for AllEq to become
+
+ [WD] AllEqF '[] cbv2
+ [WD] SameShapeAs '[] cbv2
+
+While the first of these is stuck, the second makes progress, to lead to
+
+ [WD] AllEqF '[] cbv2
+ [WD] cbv2 ~ '[]
+
+This second constraint is solved by unification: cbv2 := '[]. We now
+have
+
+ [WD] AllEqF '[] '[]
+
+which reduces to
+
+ [WD] ()
+
+which is trivially satisfiable. Hooray!
+
+Note that we need to unify the cbvs here; if we did not, there would be
+no way to solve those constraints. That's why the cycle-breakers are
+ordinary TauTvs.
+
+In all cases
+------------
+
+We detect this scenario by the following characteristics:
+ - a constraint with a tyvar on its LHS
+ - with a soluble occurs-check failure
+ - and a nominal equality
+ - and either
+ - a Given flavour (but see also Detail (7) below)
+ - a Wanted/Derived or just plain Derived flavour, with a touchable metavariable
+ on the left
+
+We don't use this trick for representational equalities, as there is no
+concrete use case where it is helpful (unlike for nominal equalities).
+Furthermore, because function applications can be CanEqLHSs, but newtype
+applications cannot, the disparities between the cases are enough that it
+would be effortful to expand the idea to representational equalities. A quick
+attempt, with
data family N a b
f :: (Coercible a (N a b), Coercible (N a b) b) => a -> b
f = coerce
- failed with "Could not match 'b' with 'b'." Further work is held off
- until when we have a concrete incentive to explore this dark corner.
+failed with "Could not match 'b' with 'b'." Further work is held off
+until when we have a concrete incentive to explore this dark corner.
Details:
@@ -2828,17 +2805,21 @@ Details:
type family, or that outer type family application would already have
been substituted away.
- However, we still must check to make sure that breakTyVarCycle actually
- succeeds in getting rid of all occurrences of the offending variable.
- If one is hidden under a forall, this won't be true. So we perform
- an additional check after performing the substitution.
+ However, we still must check to make sure that breakTyVarCycle_maybe actually
+ succeeds in getting rid of all occurrences of the offending variable. If
+ one is hidden under a forall, this won't be true. A similar problem can
+ happen if the variable appears only in a kind
+ (e.g. k ~ ... (a :: k) ...). So we perform an additional check after
+ performing the substitution. It is tiresome to re-run all of checkTyVarEq
+ here, but reimplementing just the occurs-check is even more tiresome.
- Skipping this check causes typecheck/should_fail/GivenForallLoop to loop.
+ Skipping this check causes typecheck/should_fail/GivenForallLoop and
+ polykinds/T18451 to loop.
(2) Our goal here is to avoid loops in rewriting. We can thus skip looking
- in coercions, as we don't rewrite in coercions.
- (There is no worry about unifying a meta-variable here: this Note is
- only about Givens.)
+ in coercions, as we don't rewrite in coercions. (This is another reason
+ we need to re-check that we've gotten rid of all occurrences of the
+ offending variable.)
(3) As we're substituting, we can build ill-kinded
types. For example, if we have Proxy (F a) b, where (b :: F a), then
@@ -2868,21 +2849,18 @@ Details:
Note [Flattening type-family applications when matching instances]
in GHC.Core.Unify, which
goes to this extra effort.) There may be other opportunities for
- improvement. However, this is really a very small corner case, always
- tickled by a user-written Given. The investment to craft a clever,
+ improvement. However, this is really a very small corner case.
+ The investment to craft a clever,
performant solution seems unworthwhile.
(6) We often get the predicate associated with a constraint from its
evidence. We thus must not only make sure the generated CEqCan's
fields have the updated RHS type, but we must also update the
- evidence itself. As in Detail (4), we don't need to change the
- evidence term (as in e.g. rewriteEqEvidence) because the cycle
- breaker variables are all zonked away by the time we examine the
- evidence. That is, we must set the ctev_pred of the ctEvidence.
- This is implemented in canEqCanLHSFinish, with a reference to
- this detail.
-
- (7) We don't wish to apply this magic to CycleBreakerTvs themselves.
+ evidence itself. This is done by the call to rewriteEqEvidence
+ in canEqCanLHSFinish.
+
+ (7) We don't wish to apply this magic on the equalities created
+ by this very same process.
Consider this, from typecheck/should_compile/ContextStack2:
type instance TF (a, b) = (TF a, TF b)
@@ -2913,23 +2891,19 @@ Details:
unchecked, this will end up breaking cycles again, looping ad
infinitum (and resulting in a context-stack reduction error,
not an outright loop). The solution is easy: don't break cycles
- if the var is already a CycleBreakerTv. Instead, we mark this
- final Given as a CIrredCan with an OtherCIS status (it's not
- insoluble).
-
- NB: When filling in CycleBreakerTvs, we fill them in with what
- they originally stood for (e.g. cbv1 := TF a, cbv2 := TF Int),
- not what may be in a rewritten constraint.
-
- Not breaking cycles further (which would mean changing TF cbv1 to cbv3
- and TF cbv2 to cbv4) makes sense, because we only want to break cycles
- for user-written loopy Givens, and a CycleBreakerTv certainly isn't
- user-written.
-
-NB: This same situation (an equality like b ~ Maybe (F b)) can arise with
-Wanteds, but we have no concrete case incentivising special treatment. It
-would just be a CIrredCan.
-
+ on an equality generated by breaking cycles. Instead, we mark this
+ final Given as a CIrredCan with a NonCanonicalReason with the soluble
+ occurs-check bit set (only).
+
+ We track these equalities by giving them a special CtOrigin,
+ CycleBreakerOrigin. This works for both Givens and WDs, as
+ we need the logic in the WD case for e.g. typecheck/should_fail/T17139.
+
+ (8) We really want to do this all only when there is a soluble occurs-check
+ failure, not when other problems arise (such as an impredicative
+ equality like alpha ~ forall a. a -> a). That is why breakTyVarCycle_maybe
+ uses cterHasOnlyProblem when looking at the result of checkTypeEq, which
+ checks for many of the invariants on a CEqCan.
-}
{-
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
index 4ad07a58d4..c5252fb09a 100644
--- a/compiler/GHC/Tc/Solver/InertSet.hs
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -241,7 +241,7 @@ data InertSet
, inert_cycle_breakers :: [(TcTyVar, TcType)]
-- a list of CycleBreakerTv / original family applications
-- used to undo the cycle-breaking needed to handle
- -- Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
+ -- Note [Type variable cycles] in GHC.Tc.Solver.Canonical
, inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
-- Just a hash-cons cache for use when reducing family applications
@@ -277,7 +277,8 @@ emptyInertCans
, inert_safehask = emptyDictMap
, inert_funeqs = emptyFunEqs
, inert_insts = []
- , inert_irreds = emptyCts }
+ , inert_irreds = emptyCts
+ , inert_blocked = emptyCts }
emptyInert :: InertSet
emptyInert
@@ -839,7 +840,7 @@ The idea is that
with S(fw,_).
* T3 is guaranteed by an occurs-check on the work item.
- This is done during canonicalisation, in canEqOK and checkTypeEq; invariant
+ This is done during canonicalisation, in checkTypeEq; invariant
(TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
* (K1-3) are the "kick-out" criteria. (As stated, they are really the
@@ -1101,6 +1102,14 @@ data InertCans -- See Note [Detailed InertCans Invariants] for more
-- and which don't interact with others (e.g. (c a))
-- and insoluble predicates (e.g. Int ~ Bool, or a ~ [a])
+ , inert_blocked :: Cts
+ -- Equality predicates blocked on a coercion hole.
+ -- Each Ct is a CIrredCan with cc_reason = HoleBlockerReason
+ -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+ -- wrinkle (2)
+ -- These are stored separately from inert_irreds because
+ -- they get kicked out for different reasons
+
, inert_given_eq_lvl :: TcLevel
-- The TcLevel of the innermost implication that has a Given
-- equality of the sort that make a unification variable untouchable
@@ -1119,8 +1128,11 @@ type InertEqs = DTyVarEnv EqualCtList
instance Outputable InertCans where
ppr (IC { inert_eqs = eqs
- , inert_funeqs = funeqs, inert_dicts = dicts
- , inert_safehask = safehask, inert_irreds = irreds
+ , inert_funeqs = funeqs
+ , inert_dicts = dicts
+ , inert_safehask = safehask
+ , inert_irreds = irreds
+ , inert_blocked = blocked
, inert_given_eq_lvl = ge_lvl
, inert_given_eqs = given_eqs
, inert_insts = insts })
@@ -1137,6 +1149,8 @@ instance Outputable InertCans where
text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
, ppUnless (isEmptyCts irreds) $
text "Irreds =" <+> pprCts irreds
+ , ppUnless (isEmptyCts blocked) $
+ text "Blocked =" <+> pprCts blocked
, ppUnless (null insts) $
text "Given instances =" <+> vcat (map ppr insts)
, text "Innermost given equalities =" <+> ppr ge_lvl
@@ -1210,6 +1224,11 @@ addInertItem tc_lvl
TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item }
TyVarLHS tv -> ics { inert_eqs = addTyEq eqs tv item }
+addInertItem tc_lvl ics@(IC { inert_blocked = blocked })
+ item@(CIrredCan { cc_reason = HoleBlockerReason {}})
+ = updateGivenEqs tc_lvl item $ -- this item is always an equality
+ ics { inert_blocked = blocked `snocBag` item }
+
addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {})
= updateGivenEqs tc_lvl item $ -- An Irred might turn out to be an
-- equality, so we play safe
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index 6e051c9ef6..2375fc749a 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -664,8 +664,8 @@ once had done). This problem can be tickled by typecheck/should_compile/holes.
-- mean that (ty1 ~ ty2)
interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
-interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_status = status })
- | InsolubleCIS <- status
+interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_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
@@ -1584,15 +1584,15 @@ tryToSolveByUnification :: Ct -> CtEvidence
-> TcType -- RHS
-> TcS (StopOrContinue Ct)
tryToSolveByUnification work_item ev tv rhs
- = do { can_unify <- unifyTest ev tv rhs
+ = do { is_touchable <- touchabilityTest (ctEvFlavour ev) tv rhs
; traceTcS "tryToSolveByUnification" (vcat [ ppr tv <+> char '~' <+> ppr rhs
- , ppr can_unify ])
+ , ppr is_touchable ])
- ; case can_unify of
- NoUnify -> continueWith work_item
+ ; case is_touchable of
+ Untouchable -> continueWith work_item
-- For the latter two cases see Note [Solve by unification]
- UnifySameLevel -> solveByUnification ev tv rhs
- UnifyOuterLevel free_metas tv_lvl
+ TouchableSameLevel -> solveByUnification ev tv rhs
+ TouchableOuterLevel free_metas tv_lvl
-> do { wrapTcS $ mapM_ (promoteMetaTyVarTo tv_lvl) free_metas
; setUnificationFlag tv_lvl
; solveByUnification ev tv rhs } }
@@ -1664,10 +1664,10 @@ If we solve
alpha[n] ~ ty
by unification, there are two cases to consider
-* UnifySameLevel: if the ambient level is 'n', then
+* TouchableSameLevel: if the ambient level is 'n', then
we can simply update alpha := ty, and do nothing else
-* UnifyOuterLevel free_metas n: if the ambient level is greater than
+* TouchableOuterLevel free_metas n: if the ambient level is greater than
'n' (the level of alpha), in addition to setting alpha := ty we must
do two other things:
@@ -1681,7 +1681,7 @@ by unification, there are two cases to consider
2. Set the Unification Level Flag to record that a level-n unification has
taken place. See Note [The Unification Level Flag] in GHC.Tc.Solver.Monad
-NB: UnifySameLevel is just an optimisation for UnifyOuterLevel. Promotion
+NB: TouchableSameLevel is just an optimisation for TouchableOuterLevel. Promotion
would be a no-op, and setting the unification flag unnecessarily would just
make the solver iterate more often. (We don't need to iterate when unifying
at the ambient level because of the kick-out mechanism.)
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 96228fcce5..9a4383a508 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -2,8 +2,10 @@
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
@@ -42,7 +44,7 @@ module GHC.Tc.Solver.Monad (
newWantedNC, newWantedEvVarNC,
newDerivedNC,
newBoundEvVarId,
- unifyTyVar, reportUnifications,
+ unifyTyVar, reportUnifications, touchabilityTest, TouchabilityTestResult(..),
setEvBind, setWantedEq,
setWantedEvTerm, setEvBindIfWanted,
newEvVar, newGivenEvVar, newGivenEvVars,
@@ -113,7 +115,7 @@ module GHC.Tc.Solver.Monad (
-- if the whole instance matcher simply belongs
-- here
- breakTyVarCycle, rewriterView
+ breakTyVarCycle_maybe, rewriterView
) where
import GHC.Prelude
@@ -161,6 +163,7 @@ import GHC.Types.Unique.Supply
import GHC.Tc.Types
import GHC.Tc.Types.Origin
import GHC.Tc.Types.Constraint
+import GHC.Tc.Utils.Unify
import GHC.Core.Predicate
import GHC.Types.Unique.Set
@@ -169,7 +172,7 @@ import Control.Monad
import GHC.Utils.Monad
import Data.IORef
import GHC.Exts (oneShot)
-import Data.List ( mapAccumL )
+import Data.List ( mapAccumL, partition )
import Data.List.NonEmpty ( NonEmpty(..) )
import Control.Arrow ( first )
@@ -696,27 +699,31 @@ kickOutAfterFillingCoercionHole hole filled_co
holes_of_co = coercionHolesOfCo filled_co
kick_out :: InertCans -> (WorkList, InertCans)
- kick_out ics@(IC { inert_irreds = irreds })
- = let (to_kick, to_keep) = partitionBagWith kick_ct irreds
+ kick_out ics@(IC { inert_blocked = blocked })
+ = let (to_kick, to_keep) = partitionBagWith kick_ct blocked
kicked_out = extendWorkListCts (bagToList to_kick) emptyWorkList
- ics' = ics { inert_irreds = to_keep }
+ ics' = ics { inert_blocked = to_keep }
in
(kicked_out, ics')
kick_ct :: Ct -> Either Ct Ct
-- Left: kick out; Right: keep. But even if we keep, we may need
-- to update the set of blocking holes
- kick_ct ct@(CIrredCan { cc_status = BlockedCIS holes })
+ kick_ct ct@(CIrredCan { cc_reason = HoleBlockerReason holes })
| hole `elementOfUniqSet` holes
= let new_holes = holes `delOneFromUniqSet` hole
`unionUniqSets` holes_of_co
- updated_ct = ct { cc_status = BlockedCIS new_holes }
+ updated_ct = ct { cc_reason = HoleBlockerReason new_holes }
in
if isEmptyUniqSet new_holes
then Left updated_ct
else Right updated_ct
- kick_ct other = Right other
+
+ | otherwise
+ = Right ct
+
+ kick_ct other = pprPanic "kickOutAfterFillingCoercionHole" (ppr other)
--------------
addInertSafehask :: InertCans -> Ct -> InertCans
@@ -887,17 +894,21 @@ getUnsolvedInerts :: TcS ( Bag Implication
-- (because they come from the inert set)
-- the unsolved implics may not be
getUnsolvedInerts
- = do { IC { inert_eqs = tv_eqs
- , inert_funeqs = fun_eqs
- , inert_irreds = irreds
- , inert_dicts = idicts
+ = do { IC { inert_eqs = tv_eqs
+ , inert_funeqs = fun_eqs
+ , inert_irreds = irreds
+ , inert_blocked = blocked
+ , inert_dicts = idicts
} <- getInertCans
; let unsolved_tv_eqs = foldTyEqs add_if_unsolved tv_eqs emptyCts
unsolved_fun_eqs = foldFunEqs add_if_unsolveds fun_eqs emptyCts
unsolved_irreds = Bag.filterBag is_unsolved irreds
+ unsolved_blocked = blocked -- all blocked equalities are W/D
unsolved_dicts = foldDicts add_if_unsolved idicts emptyCts
- unsolved_others = unsolved_irreds `unionBags` unsolved_dicts
+ unsolved_others = unionManyBags [ unsolved_irreds
+ , unsolved_dicts
+ , unsolved_blocked ]
; implics <- getWorkListImplics
@@ -1009,7 +1020,7 @@ This is best understood by example.
where cbv = F a
The cbv is a cycle-breaker var which stands for F a. See
- Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
+ Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
This is just like case 6, and we say "no". Saying "no" here is
essential in getting the parser to type-check, with its use of DisambECP.
@@ -1327,7 +1338,7 @@ runTcSWithEvBinds = runTcSWithEvBinds' True
runTcSWithEvBinds' :: Bool -- ^ Restore type variable cycles afterwards?
-- Don't if you want to reuse the InertSet.
- -- See also Note [Type variable cycles in Givens]
+ -- See also Note [Type variable cycles]
-- in GHC.Tc.Solver.Canonical
-> EvBindsVar
-> TcS a
@@ -1624,6 +1635,82 @@ reportUnifications (TcS thing_inside)
; TcM.updTcRef (tcs_unified env) (+ n_unifs)
; return (n_unifs, res) }
+data TouchabilityTestResult
+ -- See Note [Solve by unification] in GHC.Tc.Solver.Interact
+ -- which points out that having TouchableSameLevel is just an optimisation;
+ -- we could manage with TouchableOuterLevel alone (suitably renamed)
+ = TouchableSameLevel
+ | TouchableOuterLevel [TcTyVar] -- Promote these
+ TcLevel -- ..to this level
+ | Untouchable
+
+instance Outputable TouchabilityTestResult where
+ ppr TouchableSameLevel = text "TouchableSameLevel"
+ ppr (TouchableOuterLevel tvs lvl) = text "TouchableOuterLevel" <> parens (ppr lvl <+> ppr tvs)
+ ppr Untouchable = text "Untouchable"
+
+touchabilityTest :: CtFlavour -> TcTyVar -> TcType -> TcS TouchabilityTestResult
+-- This is the key test for untouchability:
+-- See Note [Unification preconditions] in GHC.Tc.Utils.Unify
+-- and Note [Solve by unification] in GHC.Tc.Solver.Interact
+touchabilityTest flav tv1 rhs
+ | flav /= Given -- See Note [Do not unify Givens]
+ , MetaTv { mtv_tclvl = tv_lvl, mtv_info = info } <- tcTyVarDetails tv1
+ , canSolveByUnification info rhs
+ = do { ambient_lvl <- getTcLevel
+ ; given_eq_lvl <- getInnermostGivenEqLevel
+
+ ; if | tv_lvl `sameDepthAs` ambient_lvl
+ -> return TouchableSameLevel
+
+ | tv_lvl `deeperThanOrSame` given_eq_lvl -- No intervening given equalities
+ , all (does_not_escape tv_lvl) free_skols -- No skolem escapes
+ -> return (TouchableOuterLevel free_metas tv_lvl)
+
+ | otherwise
+ -> return Untouchable }
+ | otherwise
+ = return Untouchable
+ where
+ (free_metas, free_skols) = partition isPromotableMetaTyVar $
+ nonDetEltsUniqSet $
+ tyCoVarsOfType rhs
+
+ does_not_escape tv_lvl fv
+ | isTyVar fv = tv_lvl `deeperThanOrSame` tcTyVarLevel fv
+ | otherwise = True
+ -- Coercion variables are not an escape risk
+ -- If an implication binds a coercion variable, it'll have equalities,
+ -- so the "intervening given equalities" test above will catch it
+ -- Coercion holes get filled with coercions, so again no problem.
+
+{- Note [Do not unify Givens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this GADT match
+ data T a where
+ T1 :: T Int
+ ...
+
+ f x = case x of
+ T1 -> True
+ ...
+
+So we get f :: T alpha[1] -> beta[1]
+ x :: T alpha[1]
+and from the T1 branch we get the implication
+ forall[2] (alpha[1] ~ Int) => beta[1] ~ Bool
+
+Now, clearly we don't want to unify alpha:=Int! Yet at the moment we
+process [G] alpha[1] ~ Int, we don't have any given-equalities in the
+inert set, and hence there are no given equalities to make alpha untouchable.
+
+NB: if it were alpha[2] ~ Int, this argument wouldn't hold. But that
+never happens: invariant (GivenInv) in Note [TcLevel invariants]
+in GHC.Tc.Utils.TcType.
+
+Simple solution: never unify in Givens!
+-}
+
getDefaultInfo :: TcS ([Type], (Bool, Bool))
getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
@@ -2130,51 +2217,123 @@ matchFamTcM tycon args
************************************************************************
-}
--- | Replace all type family applications in the RHS with fresh variables,
--- emitting givens that relate the type family application to the variable.
--- See Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
-breakTyVarCycle :: CtLoc
- -> TcType -- the RHS
- -> TcS TcType -- new RHS that doesn't have any type families
--- This could be considerably more efficient. See Detail (5) of Note.
-breakTyVarCycle loc = go
+-- | Conditionally replace all type family applications in the RHS with fresh
+-- variables, emitting givens that relate the type family application to the
+-- variable. See Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
+-- This only works under conditions as described in the Note; otherwise, returns
+-- Nothing.
+breakTyVarCycle_maybe :: CtEvidence
+ -> CheckTyEqResult -- result of checkTypeEq
+ -> CanEqLHS
+ -> TcType -- RHS
+ -> TcS (Maybe (TcTyVar, CoercionN, TcType))
+ -- new RHS that doesn't have any type families
+ -- co :: new type ~N old type
+ -- TcTyVar is the LHS tv; convenient for the caller
+breakTyVarCycle_maybe (ctLocOrigin . ctEvLoc -> CycleBreakerOrigin _) _ _ _
+ -- see Detail (7) of Note
+ = return Nothing
+
+breakTyVarCycle_maybe ev cte_result (TyVarLHS lhs_tv) rhs
+ | NomEq <- eq_rel
+
+ , cte_result `cterHasOnlyProblem` cteSolubleOccurs
+ -- only do this if the only problem is a soluble occurs-check
+ -- See Detail (8) of the Note.
+
+ = do { should_break <- final_check
+ ; if should_break then do { (co, new_rhs) <- go rhs
+ ; return (Just (lhs_tv, co, new_rhs)) }
+ else return Nothing }
where
+ flavour = ctEvFlavour ev
+ eq_rel = ctEvEqRel ev
+
+ final_check
+ | Given <- flavour
+ = return True
+ | ctFlavourContainsDerived flavour
+ = do { result <- touchabilityTest Derived lhs_tv rhs
+ ; return $ case result of
+ Untouchable -> False
+ _ -> True }
+ | otherwise
+ = return False
+
+ -- This could be considerably more efficient. See Detail (5) of Note.
+ go :: TcType -> TcS (CoercionN, TcType)
go ty | Just ty' <- rewriterView ty = go ty'
go (Rep.TyConApp tc tys)
- | isTypeFamilyTyCon tc
+ | isTypeFamilyTyCon tc -- worried about whether this type family is not actually
+ -- causing trouble? See Detail (5) of Note.
= do { let (fun_args, extra_args) = splitAt (tyConArity tc) tys
fun_app = mkTyConApp tc fun_args
fun_app_kind = tcTypeKind fun_app
- ; new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind)
+ ; (co, new_ty) <- emit_work fun_app_kind fun_app
+ ; (extra_args_cos, extra_args') <- mapAndUnzipM go extra_args
+ ; return (mkAppCos co extra_args_cos, mkAppTys new_ty extra_args') }
+ -- Worried that this substitution will change kinds?
+ -- See Detail (3) of Note
+
+ | otherwise
+ = do { (cos, tys) <- mapAndUnzipM go tys
+ ; return (mkTyConAppCo Nominal tc cos, mkTyConApp tc tys) }
+
+ go (Rep.AppTy ty1 ty2)
+ = do { (co1, ty1') <- go ty1
+ ; (co2, ty2') <- go ty2
+ ; return (mkAppCo co1 co2, mkAppTy ty1' ty2') }
+ go (Rep.FunTy vis w arg res)
+ = do { (co_w, w') <- go w
+ ; (co_arg, arg') <- go arg
+ ; (co_res, res') <- go res
+ ; return (mkFunCo Nominal co_w co_arg co_res, mkFunTy vis w' arg' res') }
+ go (Rep.CastTy ty cast_co)
+ = do { (co, ty') <- go ty
+ -- co :: ty' ~N ty
+ -- return_co :: (ty' |> cast_co) ~ (ty |> cast_co)
+ ; return (castCoercionKind1 co Nominal ty' ty cast_co, mkCastTy ty' cast_co) }
+
+ go ty@(Rep.TyVarTy {}) = skip ty
+ go ty@(Rep.LitTy {}) = skip ty
+ go ty@(Rep.ForAllTy {}) = skip ty -- See Detail (1) of Note
+ go ty@(Rep.CoercionTy {}) = skip ty -- See Detail (2) of Note
+
+ skip ty = return (mkNomReflCo ty, ty)
+
+ emit_work :: TcKind -- of the function application
+ -> TcType -- original function application
+ -> TcS (CoercionN, TcType) -- rewritten type (the fresh tyvar)
+ emit_work fun_app_kind fun_app = case flavour of
+ Given ->
+ do { new_tv <- wrapTcS (TcM.newCycleBreakerTyVar fun_app_kind)
; let new_ty = mkTyVarTy new_tv
given_pred = mkHeteroPrimEqPred fun_app_kind fun_app_kind
fun_app new_ty
given_term = evCoercion $ mkNomReflCo new_ty -- See Detail (4) of Note
- ; new_given <- newGivenEvVar loc (given_pred, given_term)
- ; traceTcS "breakTyVarCycle replacing type family" (ppr new_given)
+ ; new_given <- newGivenEvVar new_loc (given_pred, given_term)
+ ; traceTcS "breakTyVarCycle replacing type family in Given" (ppr new_given)
; emitWorkNC [new_given]
; updInertTcS $ \is ->
is { inert_cycle_breakers = (new_tv, fun_app) :
inert_cycle_breakers is }
- ; extra_args' <- mapM go extra_args
- ; return (mkAppTys new_ty extra_args') }
- -- Worried that this substitution will change kinds?
- -- See Detail (3) of Note
+ ; return (mkNomReflCo new_ty, new_ty) }
+ -- Why reflexive? See Detail (4) of the Note
- | otherwise
- = mkTyConApp tc <$> mapM go tys
+ _derived_or_wd ->
+ do { new_tv <- wrapTcS (TcM.newFlexiTyVar fun_app_kind)
+ ; let new_ty = mkTyVarTy new_tv
+ ; co <- emitNewWantedEq new_loc Nominal new_ty fun_app
+ ; return (co, new_ty) }
- go (Rep.AppTy ty1 ty2) = mkAppTy <$> go ty1 <*> go ty2
- go (Rep.FunTy vis w arg res) = mkFunTy vis <$> go w <*> go arg <*> go res
- go (Rep.CastTy ty co) = mkCastTy <$> go ty <*> pure co
+ -- See Detail (7) of the Note
+ new_loc = updateCtLocOrigin (ctEvLoc ev) CycleBreakerOrigin
- go ty@(Rep.TyVarTy {}) = return ty
- go ty@(Rep.LitTy {}) = return ty
- go ty@(Rep.ForAllTy {}) = return ty -- See Detail (1) of Note
- go ty@(Rep.CoercionTy {}) = return ty -- See Detail (2) of Note
+-- does not fit scenario from Note
+breakTyVarCycle_maybe _ _ _ _ = return Nothing
-- | Fill in CycleBreakerTvs with the variables they stand for.
--- See Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical.
+-- See Note [Type variable cycles] in GHC.Tc.Solver.Canonical.
restoreTyVarCycles :: InertSet -> TcM ()
restoreTyVarCycles is
= forM_ (inert_cycle_breakers is) $ \ (cycle_breaker_tv, orig_ty) ->
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index eebdd8fe2b..0422835ac0 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(..), isPendingScInst,
-- Canonical constraints
- Xi, Ct(..), Cts, CtIrredStatus(..), HoleSet,
+ Xi, Ct(..), Cts,
emptyCts, andCts, andManyCts, pprCts,
singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList,
isEmptyCts,
@@ -26,6 +26,14 @@ module GHC.Tc.Types.Constraint (
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
+ CtIrredReason(..), HoleSet, isInsolubleReason,
+
+ CheckTyEqResult, CheckTyEqProblem, cteProblem, cterClearOccursCheck,
+ cteOK, cteImpredicative, cteTypeFamily, cteHoleBlocker,
+ cteInsolubleOccurs, cteSolubleOccurs, cterSetOccursCheckSoluble,
+ cterHasNoProblem, cterHasProblem, cterHasOnlyProblem,
+ cterRemoveProblem, cterHasOccursCheck, cterFromKind,
+
CanEqLHS(..), canEqLHS_maybe, canEqLHSKind, canEqLHSType,
eqCanEqLHS,
@@ -58,7 +66,7 @@ module GHC.Tc.Types.Constraint (
wrapType,
- CtFlavour(..), ShadowInfo(..), ctEvFlavour,
+ CtFlavour(..), ShadowInfo(..), ctFlavourContainsDerived, ctEvFlavour,
CtFlavourRole, ctEvFlavourRole, ctFlavourRole,
eqCanRewrite, eqCanRewriteFR, eqMayRewriteFR,
eqCanDischargeFR,
@@ -104,6 +112,12 @@ import GHC.Utils.Panic
import Control.Monad ( msum )
import qualified Data.Semigroup ( (<>) )
+-- these are for CheckTyEqResult
+import Data.Word ( Word8 )
+import Data.List ( intersperse )
+
+
+
{-
************************************************************************
* *
@@ -178,7 +192,7 @@ data Ct
| CIrredCan { -- These stand for yet-unusable predicates
cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant]
- cc_status :: CtIrredStatus
+ 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
@@ -301,21 +315,156 @@ instance Outputable HoleSort where
------------
-- | Used to indicate extra information about why a CIrredCan is irreducible
-data CtIrredStatus
- = InsolubleCIS -- this constraint will never be solved
- | BlockedCIS HoleSet
- -- this constraint is blocked on the coercion hole(s) listed
- -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
- -- Wrinkle (4a). Why store the HoleSet? See Wrinkle (2) of that
- -- same Note.
- -- INVARIANT: A BlockedCIS is a homogeneous equality whose
- -- left hand side can fit in a CanEqLHS.
- | OtherCIS
-
-instance Outputable CtIrredStatus where
- ppr InsolubleCIS = text "(insoluble)"
- ppr (BlockedCIS holes) = parens (text "blocked on" <+> ppr holes)
- ppr OtherCIS = text "(soluble)"
+data CtIrredReason
+ = IrredShapeReason
+ -- ^ this constraint has a non-canonical shape (e.g. @c Int@, for a variable @c@)
+
+ | HoleBlockerReason HoleSet
+ -- ^ this constraint is blocked on the coercion hole(s) listed
+ -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+ -- Wrinkle (4a). Why store the HoleSet? See Wrinkle (2) of that
+ -- same Note.
+ -- INVARIANT: A HoleBlockerReason constraint is a homogeneous equality whose
+ -- left hand side can fit in a CanEqLHS.
+
+ | NonCanonicalReason CheckTyEqResult
+ -- ^ an equality where some invariant other than (TyEq:H) of 'CEqCan' is not satisfied;
+ -- the 'CheckTyEqResult' states exactly why
+ -- INVARIANT: the 'CheckTyEqResult' has some bit set other than cteHoleBlocker
+
+ | ReprEqReason
+ -- ^ an equality that cannot be decomposed because it is representational.
+ -- Example: @a b ~R# Int@.
+ -- These might still be solved later.
+ -- INVARIANT: The constraint is a representational equality constraint
+
+ | ShapeMismatchReason
+ -- ^ a nominal equality that relates two wholly different types,
+ -- like @Int ~# Bool@ or @a b ~# 3@.
+ -- INVARIANT: The constraint is a nominal equality constraint
+
+ | AbstractTyConReason
+ -- ^ an equality like @T a b c ~ Q d e@ where either @T@ or @Q@
+ -- is an abstract type constructor. See Note [Skolem abstract data]
+ -- in GHC.Core.TyCon.
+ -- INVARIANT: The constraint is an equality constraint between two TyConApps
+
+instance Outputable CtIrredReason where
+ ppr IrredShapeReason = text "(irred)"
+ ppr (HoleBlockerReason holes) = parens (text "blocked on" <+> ppr holes)
+ ppr (NonCanonicalReason cter) = ppr cter
+ ppr ReprEqReason = text "(repr)"
+ ppr ShapeMismatchReason = text "(shape)"
+ ppr AbstractTyConReason = text "(abstc)"
+
+-- | Are we sure that more solving will never solve this constraint?
+isInsolubleReason :: CtIrredReason -> Bool
+isInsolubleReason IrredShapeReason = False
+isInsolubleReason (HoleBlockerReason {}) = False
+isInsolubleReason (NonCanonicalReason cter) = cterIsInsoluble cter
+isInsolubleReason ReprEqReason = False
+isInsolubleReason ShapeMismatchReason = True
+isInsolubleReason AbstractTyConReason = True
+
+------------------------------------------------------------------------------
+--
+-- CheckTyEqResult, defined here because it is stored in a CtIrredReason
+--
+------------------------------------------------------------------------------
+
+-- | A set of problems in checking the validity of a type equality.
+-- See 'checkTypeEq'.
+newtype CheckTyEqResult = CTER Word8
+
+-- | No problems in checking the validity of a type equality.
+cteOK :: CheckTyEqResult
+cteOK = CTER zeroBits
+
+-- | Check whether a 'CheckTyEqResult' is marked successful.
+cterHasNoProblem :: CheckTyEqResult -> Bool
+cterHasNoProblem (CTER 0) = True
+cterHasNoProblem _ = False
+
+-- | An individual problem that might be logged in a 'CheckTyEqResult'
+newtype CheckTyEqProblem = CTEP Word8
+
+cteImpredicative, cteTypeFamily, cteHoleBlocker, cteInsolubleOccurs,
+ cteSolubleOccurs :: CheckTyEqProblem
+cteImpredicative = CTEP (bit 0) -- forall or (=>) encountered
+cteTypeFamily = CTEP (bit 1) -- type family encountered
+cteHoleBlocker = CTEP (bit 2) -- blocking coercion hole
+ -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
+cteInsolubleOccurs = CTEP (bit 3) -- occurs-check
+cteSolubleOccurs = CTEP (bit 4) -- occurs-check under a type function or in a coercion
+ -- must be one bit to the left of cteInsolubleOccurs
+-- See also Note [Insoluble occurs check] in GHC.Tc.Errors
+
+cteProblem :: CheckTyEqProblem -> CheckTyEqResult
+cteProblem (CTEP mask) = CTER mask
+
+occurs_mask :: Word8
+occurs_mask = insoluble_mask .|. soluble_mask
+ where
+ CTEP insoluble_mask = cteInsolubleOccurs
+ CTEP soluble_mask = cteSolubleOccurs
+
+-- | Check whether a 'CheckTyEqResult' has a 'CheckTyEqProblem'
+cterHasProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
+CTER bits `cterHasProblem` CTEP mask = (bits .&. mask) /= 0
+
+-- | Check whether a 'CheckTyEqResult' has one 'CheckTyEqProblem' and no other
+cterHasOnlyProblem :: CheckTyEqResult -> CheckTyEqProblem -> Bool
+CTER bits `cterHasOnlyProblem` CTEP mask = bits == mask
+
+cterRemoveProblem :: CheckTyEqResult -> CheckTyEqProblem -> CheckTyEqResult
+cterRemoveProblem (CTER bits) (CTEP mask) = CTER (bits .&. complement mask)
+
+cterHasOccursCheck :: CheckTyEqResult -> Bool
+cterHasOccursCheck (CTER bits) = (bits .&. occurs_mask) /= 0
+
+cterClearOccursCheck :: CheckTyEqResult -> CheckTyEqResult
+cterClearOccursCheck (CTER bits) = CTER (bits .&. complement occurs_mask)
+
+-- | Mark a 'CheckTyEqResult' as not having an insoluble occurs-check: any occurs
+-- check under a type family or in a representation equality is soluble.
+cterSetOccursCheckSoluble :: CheckTyEqResult -> CheckTyEqResult
+cterSetOccursCheckSoluble (CTER bits)
+ = CTER $ ((bits .&. insoluble_mask) `shift` 1) .|. (bits .&. complement insoluble_mask)
+ where
+ CTEP insoluble_mask = cteInsolubleOccurs
+
+-- | Retain only information about occurs-check failures, because only that
+-- matters after recurring into a kind.
+cterFromKind :: CheckTyEqResult -> CheckTyEqResult
+cterFromKind (CTER bits)
+ = CTER (bits .&. occurs_mask)
+
+cterIsInsoluble :: CheckTyEqResult -> Bool
+cterIsInsoluble (CTER bits) = (bits .&. mask) /= 0
+ where
+ mask = impredicative_mask .|. insoluble_occurs_mask
+
+ CTEP impredicative_mask = cteImpredicative
+ CTEP insoluble_occurs_mask = cteInsolubleOccurs
+
+instance Semigroup CheckTyEqResult where
+ CTER bits1 <> CTER bits2 = CTER (bits1 .|. bits2)
+instance Monoid CheckTyEqResult where
+ mempty = cteOK
+
+instance Outputable CheckTyEqResult where
+ ppr cter | cterHasNoProblem cter = text "cteOK"
+ | otherwise
+ = parens $ fcat $ intersperse vbar $ set_bits
+ where
+ all_bits = [ (cteImpredicative, "cteImpredicative")
+ , (cteTypeFamily, "cteTypeFamily")
+ , (cteHoleBlocker, "cteHoleBlocker")
+ , (cteInsolubleOccurs, "cteInsolubleOccurs")
+ , (cteSolubleOccurs, "cteSolubleOccurs") ]
+ set_bits = [ text str
+ | (bitmask, str) <- all_bits
+ , cter `cterHasProblem` bitmask ]
{- Note [CIrredCan constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -398,8 +547,8 @@ mkNonCanonical ev = CNonCanonical { cc_ev = ev }
mkNonCanonicalCt :: Ct -> Ct
mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct }
-mkIrredCt :: CtIrredStatus -> CtEvidence -> Ct
-mkIrredCt status ev = CIrredCan { cc_ev = ev, cc_status = status }
+mkIrredCt :: CtIrredReason -> CtEvidence -> Ct
+mkIrredCt reason ev = CIrredCan { cc_ev = ev, cc_reason = reason }
mkGivens :: CtLoc -> [EvId] -> [Ct]
mkGivens loc ev_ids
@@ -459,7 +608,7 @@ instance Outputable Ct where
| psc, not fds -> text "CDictCan(psc)"
| not psc, fds -> text "CDictCan(fds)"
| otherwise -> text "CDictCan"
- CIrredCan { cc_status = status } -> text "CIrredCan" <> ppr status
+ CIrredCan { cc_reason = reason } -> text "CIrredCan" <> ppr reason
CQuantCan (QCI { qci_pend_sc = pend_sc })
| pend_sc -> text "CQuantCan(psc)"
| otherwise -> text "CQuantCan"
@@ -630,8 +779,8 @@ isDroppableCt ct
keep_deriv
= case ct of
- CIrredCan { cc_status = InsolubleCIS } -> keep_eq True
- _ -> keep_eq False
+ CIrredCan { cc_reason = reason } | isInsolubleReason reason -> keep_eq True
+ _ -> keep_eq False
keep_eq definitely_insoluble
| isGivenOrigin orig -- Arising only from givens
@@ -1038,8 +1187,8 @@ 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_status = InsolubleCIS }) = True
-insolubleEqCt _ = False
+insolubleEqCt (CIrredCan { cc_reason = reason }) = isInsolubleReason reason
+insolubleEqCt _ = False
-- | Does this hole represent an "out of scope" error?
-- See Note [Insoluble holes]
@@ -1641,6 +1790,12 @@ instance Outputable CtFlavour where
ppr (Wanted WOnly) = text "[W]"
ppr Derived = text "[D]"
+-- | Does this 'CtFlavour' subsumed 'Derived'? True of @[WD]@ and @[D]@.
+ctFlavourContainsDerived :: CtFlavour -> Bool
+ctFlavourContainsDerived (Wanted WDeriv) = True
+ctFlavourContainsDerived Derived = True
+ctFlavourContainsDerived _ = False
+
ctEvFlavour :: CtEvidence -> CtFlavour
ctEvFlavour (CtWanted { ctev_nosh = nosh }) = Wanted nosh
ctEvFlavour (CtGiven {}) = Given
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index 02c5c351e7..e35f5ba385 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -462,6 +462,10 @@ data CtOrigin
| NonLinearPatternOrigin
| UsageEnvironmentOf Name
+ | CycleBreakerOrigin
+ CtOrigin -- origin of the original constraint
+ -- See Detail (7) of Note [Type variable cycles] in GHC.Tc.Solver.Canonical
+
-- An origin is visible if the place where the constraint arises is manifest
-- in user code. Currently, all origins are visible except for invisible
-- TypeEqOrigins. This is used when choosing which error of
@@ -481,6 +485,7 @@ isGivenOrigin :: CtOrigin -> Bool
isGivenOrigin (GivenOrigin {}) = True
isGivenOrigin (FunDepOrigin1 _ o1 _ _ o2 _) = isGivenOrigin o1 && isGivenOrigin o2
isGivenOrigin (FunDepOrigin2 _ o1 _ _) = isGivenOrigin o1
+isGivenOrigin (CycleBreakerOrigin o) = isGivenOrigin o
isGivenOrigin _ = False
instance Outputable CtOrigin where
@@ -627,6 +632,9 @@ pprCtOrigin (InstProvidedOrigin mod cls_inst)
, ppr cls_inst
, text "is provided by" <+> quotes (ppr mod)]
+pprCtOrigin (CycleBreakerOrigin orig)
+ = pprCtOrigin orig
+
pprCtOrigin simple_origin
= ctoHerald <+> pprCtO simple_origin
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index ccebfd6716..66a05aa30e 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -364,7 +364,7 @@ unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
-- | Check that a coercion is appropriate for filling a hole. (The hole
--- itself is needed only for printing.
+-- itself is needed only for printing.)
-- Always returns the checked coercion, but this return value is necessary
-- so that the input coercion is forced only when the output is forced.
checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
@@ -880,7 +880,7 @@ cloneAnonMetaTyVar info tv kind
; traceTc "cloneAnonMetaTyVar" (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar))
; return tyvar }
--- Make a new CycleBreakerTv. See Note [Type variable cycles in Givens]
+-- Make a new CycleBreakerTv. See Note [Type variable cycles]
-- in GHC.Tc.Solver.Canonical.
newCycleBreakerTyVar :: TcKind -> TcM TcTyVar
newCycleBreakerTyVar kind
@@ -2324,7 +2324,7 @@ zonkHole hole@(Hole { hole_ty = ty })
~~~~~~~~~~~~~~~~~~~~~~~~~~
zonkCt tries to maintain the canonical form of a Ct. For example,
- a CDictCan should stay a CDictCan;
- - a CIrredCan should stay a CIrredCan with its cc_status flag intact
+ - a CIrredCan should stay a CIrredCan with its cc_reason flag intact
Why?, for example:
- For CDictCan, the @GHC.Tc.Solver.expandSuperClasses@ step, which runs after the
@@ -2357,7 +2357,7 @@ zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args })
zonkCt (CEqCan { cc_ev = ev })
= mkNonCanonical <$> zonkCtEvidence ev
-zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_status flag
+zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_reason flag
= do { ev' <- zonkCtEvidence ev
; return (ct { cc_ev = ev' }) }
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 1a7e80bd96..9a67143892 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -82,7 +82,7 @@ module GHC.Tc.Utils.TcType (
isIntegerTy, isNaturalTy,
isBoolTy, isUnitTy, isCharTy, isCallStackTy, isCallStackPred,
isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
- isPredTy, isTyVarClassPred, isInsolubleOccursCheck,
+ isPredTy, isTyVarClassPred,
checkValidClsArgs, hasTyVarHead,
isRigidTy,
@@ -532,7 +532,7 @@ data MetaInfo
-- It /is/ allowed to unify with a polytype, unlike TauTv
| CycleBreakerTv -- Used to fix occurs-check problems in Givens
- -- See Note [Type variable cycles in Givens] in
+ -- See Note [Type variable cycles] in
-- GHC.Tc.Solver.Canonical
instance Outputable MetaDetails where
@@ -1947,40 +1947,6 @@ isImprovementPred ty
IrredPred {} -> True -- Might have equalities after reduction?
ForAllPred {} -> False
--- | Is the equality
--- a ~r ...a....
--- definitely insoluble or not?
--- a ~r Maybe a -- Definitely insoluble
--- a ~N ...(F a)... -- Not definitely insoluble
--- -- Perhaps (F a) reduces to Int
--- a ~R ...(N a)... -- Not definitely insoluble
--- -- Perhaps newtype N a = MkN Int
--- See Note [Occurs check error] in
--- "GHC.Tc.Solver.Canonical" for the motivation for this function.
-isInsolubleOccursCheck :: EqRel -> TcTyVar -> TcType -> Bool
-isInsolubleOccursCheck eq_rel tv ty
- = go ty
- where
- go ty | Just ty' <- tcView ty = go ty'
- go (TyVarTy tv') = tv == tv' || go (tyVarKind tv')
- go (LitTy {}) = False
- go (AppTy t1 t2) = case eq_rel of -- See Note [AppTy and ReprEq]
- NomEq -> go t1 || go t2
- ReprEq -> go t1
- go (FunTy _ w t1 t2) = go w || go t1 || go t2
- go (ForAllTy (Bndr tv' _) inner_ty)
- | tv' == tv = False
- | otherwise = go (varType tv') || go inner_ty
- go (CastTy ty _) = go ty -- ToDo: what about the coercion
- go (CoercionTy _) = False -- ToDo: what about the coercion
- go (TyConApp tc tys)
- | isGenerativeTyCon tc role = any go tys
- | otherwise = any go (drop (tyConArity tc) tys)
- -- (a ~ F b a), where F has arity 1,
- -- has an insoluble occurs check
-
- role = eqRelRole eq_rel
-
{- Note [Expanding superclasses]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we expand superclasses, we use the following algorithm:
@@ -2180,19 +2146,6 @@ is_tc uniq ty = case tcSplitTyConApp_maybe ty of
Just (tc, _) -> uniq == getUnique tc
Nothing -> False
-
-{- Note [AppTy and ReprEq]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider a ~R# b a
- a ~R# a b
-
-The former is /not/ a definite error; we might instantiate 'b' with Id
- newtype Id a = MkId a
-but the latter /is/ a definite error.
-
-On the other hand, with nominal equality, both are definite errors
--}
-
isRigidTy :: TcType -> Bool
isRigidTy ty
| Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 0ad43fe32e..633b1c17bf 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1,5 +1,3 @@
-
-{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
@@ -36,8 +34,7 @@ module GHC.Tc.Utils.Unify (
matchExpectedFunKind,
matchActualFunTySigma, matchActualFunTysRho,
- occCheckForErrors, CheckTyEqResult(..),
- checkTyVarEq, checkTyFamEq, checkTypeEq, AreTypeFamiliesOK(..)
+ checkTyVarEq, checkTyFamEq, checkTypeEq
) where
@@ -55,7 +52,6 @@ import GHC.Core.Coercion
import GHC.Core.Multiplicity
import GHC.Tc.Types.Evidence
import GHC.Tc.Types.Constraint
-import GHC.Core.Predicate
import GHC.Tc.Types.Origin
import GHC.Types.Name( isSystemName )
import GHC.Tc.Utils.Instantiate
@@ -76,8 +72,7 @@ import GHC.Utils.Panic.Plain
import GHC.Exts ( inline )
import Control.Monad
import Control.Arrow ( second )
-import qualified Data.Semigroup as S
-
+import qualified Data.Semigroup as S ( (<>) )
{- *********************************************************************
* *
@@ -562,7 +557,8 @@ tcSubTypePat :: CtOrigin -> UserTypeCtxt
-- If wrap = tc_sub_type_et t1 t2
-- => wrap :: t1 ~> t2
tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected
- = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected
+ = do { dflags <- getDynFlags
+ ; tc_sub_type dflags unifyTypeET inst_orig ctxt ty_actual ty_expected }
tcSubTypePat _ _ (Infer inf_res) ty_expected
= do { co <- fillInferResult ty_expected inf_res
@@ -589,8 +585,9 @@ tcSubTypeNC :: CtOrigin -- Used when instantiating
-> TcM HsWrapper
tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty
= case res_ty of
- Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt
- ty_actual ty_expected
+ Check ty_expected -> do { dflags <- getDynFlags
+ ; tc_sub_type dflags (unifyType m_thing) inst_orig ctxt
+ ty_actual ty_expected }
Infer inf_res -> do { (wrap, rho) <- topInstantiate inst_orig ty_actual
-- See Note [Instantiation of InferResult]
@@ -640,7 +637,8 @@ tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper
-- Checks that actual <= expected
-- Returns HsWrapper :: actual ~ expected
tcSubTypeSigma ctxt ty_actual ty_expected
- = tc_sub_type (unifyType Nothing) eq_orig ctxt ty_actual ty_expected
+ = do { dflags <- getDynFlags
+ ; tc_sub_type dflags (unifyType Nothing) eq_orig ctxt ty_actual ty_expected }
where
eq_orig = TypeEqOrigin { uo_actual = ty_actual
, uo_expected = ty_expected
@@ -648,7 +646,8 @@ tcSubTypeSigma ctxt ty_actual ty_expected
, uo_visible = True }
---------------
-tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
+tc_sub_type :: DynFlags
+ -> (TcType -> TcType -> TcM TcCoercionN) -- How to unify
-> CtOrigin -- Used when instantiating
-> UserTypeCtxt -- Used when skolemising
-> TcSigmaType -- Actual; a sigma-type
@@ -657,7 +656,7 @@ tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify
-- Checks that actual_ty is more polymorphic than expected_ty
-- If wrap = tc_sub_type t1 t2
-- => wrap :: t1 ~> t2
-tc_sub_type unify inst_orig ctxt ty_actual ty_expected
+tc_sub_type dflags unify inst_orig ctxt ty_actual ty_expected
| definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
, not (possibly_poly ty_actual)
= do { traceTc "tc_sub_type (drop to equality)" $
@@ -685,7 +684,7 @@ tc_sub_type unify inst_orig ctxt ty_actual ty_expected
| (tvs, theta, tau) <- tcSplitSigmaTy ty
, (tv:_) <- tvs
, null theta
- , isInsolubleOccursCheck NomEq tv tau
+ , checkTyVarEq dflags tv tau `cterHasProblem` cteInsolubleOccurs
= True
| otherwise
= False
@@ -1443,8 +1442,8 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
| isTouchableMetaTyVar cur_lvl tv1
-- See Note [Unification preconditions], (UNTOUCHABLE) wrinkles
, canSolveByUnification (metaTyVarInfo tv1) ty2
- , CTE_OK <- checkTyVarEq dflags NoTypeFamilies tv1 ty2
- -- See Note [Prevent unification with type families] about the NoTypeFamilies:
+ , cterHasNoProblem (checkTyVarEq dflags tv1 ty2)
+ -- See Note [Prevent unification with type families]
= do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2) (tyVarKind tv1)
; traceTc "uUnfilledVar2 ok" $
vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
@@ -1607,7 +1606,7 @@ Needless to say, all three have wrinkles:
isTouchableMetaTyVar.
* In the constraint solver, we track where Given equalities occur
- and use that to guard unification in GHC.Tc.Solver.Canonical.unifyTest
+ and use that to guard unification in GHC.Tc.Solver.Canonical.touchabilityTest
More details in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
Historical note: in the olden days (pre 2021) the constraint solver
@@ -1763,7 +1762,7 @@ extra, unnecessary check. But we retain it for now as it seems to work
better in practice.
Revisited in Nov '20, along with removing flattening variables. Problem
-is still present, and the solution (NoTypeFamilies) is still the same.
+is still present, and the solution is still the same.
Note [Refactoring hazard: metaTyVarUpdateOK]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1891,7 +1890,7 @@ matchExpectedFunKind hs_ty n k = go n k
{- *********************************************************************
* *
- Occurrence checking
+ Equality invariant checking
* *
********************************************************************* -}
@@ -1928,65 +1927,29 @@ with (forall k. k->*)
-}
-data CheckTyEqResult
- = CTE_OK
- | CTE_Bad -- Forall, predicate, or type family
- | CTE_HoleBlocker -- Blocking coercion hole
- -- See Note [Equalities with incompatible kinds] in "GHC.Tc.Solver.Canonical"
- | CTE_Occurs
-
-instance S.Semigroup CheckTyEqResult where
- CTE_OK <> x = x
- x <> _ = x
-
-instance Monoid CheckTyEqResult where
- mempty = CTE_OK
-
-instance Outputable CheckTyEqResult where
- ppr CTE_OK = text "CTE_OK"
- ppr CTE_Bad = text "CTE_Bad"
- ppr CTE_HoleBlocker = text "CTE_HoleBlocker"
- ppr CTE_Occurs = text "CTE_Occurs"
-
-occCheckForErrors :: DynFlags -> TcTyVar -> Type -> CheckTyEqResult
--- Just for error-message generation; so we return CheckTyEqResult
--- so the caller can report the right kind of error
--- Check whether
--- a) the given variable occurs in the given type.
--- b) there is a forall in the type (unless we have -XImpredicativeTypes)
-occCheckForErrors dflags tv ty
- = case checkTyVarEq dflags YesTypeFamilies tv ty of
- CTE_Occurs -> case occCheckExpand [tv] ty of
- Nothing -> CTE_Occurs
- Just _ -> CTE_OK
- other -> other
-
----------------
-data AreTypeFamiliesOK = YesTypeFamilies
- | NoTypeFamilies
- deriving Eq
-
-instance Outputable AreTypeFamiliesOK where
- ppr YesTypeFamilies = text "YesTypeFamilies"
- ppr NoTypeFamilies = text "NoTypeFamilies"
-
-checkTyVarEq :: DynFlags -> AreTypeFamiliesOK -> TcTyVar -> TcType -> CheckTyEqResult
-checkTyVarEq dflags ty_fam_ok tv ty
- = inline checkTypeEq dflags ty_fam_ok (TyVarLHS tv) ty
+{-# NOINLINE checkTyVarEq #-} -- checkTyVarEq becomes big after the `inline` fires
+checkTyVarEq :: DynFlags -> TcTyVar -> TcType -> CheckTyEqResult
+checkTyVarEq dflags tv ty
+ = inline checkTypeEq dflags (TyVarLHS tv) ty
-- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
+{-# NOINLINE checkTyFamEq #-} -- checkTyFamEq becomes big after the `inline` fires
checkTyFamEq :: DynFlags
-> TyCon -- type function
-> [TcType] -- args, exactly saturated
-> TcType -- RHS
- -> CheckTyEqResult
+ -> CheckTyEqResult -- always drops cteTypeFamily
checkTyFamEq dflags fun_tc fun_args ty
- = inline checkTypeEq dflags YesTypeFamilies (TyFamLHS fun_tc fun_args) ty
+ = inline checkTypeEq dflags (TyFamLHS fun_tc fun_args) ty
+ `cterRemoveProblem` cteTypeFamily
-- inline checkTypeEq so that the `case`s over the CanEqLHS get blasted away
-checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType
- -> CheckTyEqResult
--- Checks the invariants for CEqCan. In particular:
+checkTypeEq :: DynFlags -> CanEqLHS -> TcType -> CheckTyEqResult
+-- If cteHasNoProblem (checkTypeEq dflags lhs rhs), then lhs ~ rhs
+-- is a canonical CEqCan.
+--
+-- In particular, this looks for:
-- (a) a forall type (forall a. blah)
-- (b) a predicate type (c => ty)
-- (c) a type family; see Note [Prevent unification with type families]
@@ -2010,9 +1973,15 @@ checkTypeEq :: DynFlags -> AreTypeFamiliesOK -> CanEqLHS -> TcType
-- * checkTyFamEq, checkTyVarEq (which inline it to specialise away the
-- case-analysis on 'lhs')
-- * checkEqCanLHSFinish, which does not know the form of 'lhs'
-checkTypeEq dflags ty_fam_ok lhs ty
+checkTypeEq dflags lhs ty
= go ty
where
+ impredicative = cteProblem cteImpredicative
+ type_family = cteProblem cteTypeFamily
+ hole_blocker = cteProblem cteHoleBlocker
+ insoluble_occurs = cteProblem cteInsolubleOccurs
+ soluble_occurs = cteProblem cteSolubleOccurs
+
-- The GHCi runtime debugger does its type-matching with
-- unification variables that can unify with a polytype
-- or a TyCon that would usually be disallowed by bad_tc
@@ -2028,70 +1997,76 @@ checkTypeEq dflags ty_fam_ok lhs ty
go :: TcType -> CheckTyEqResult
go (TyVarTy tv') = go_tv tv'
go (TyConApp tc tys) = go_tc tc tys
- go (LitTy {}) = CTE_OK
- go (FunTy{ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
- | InvisArg <- af
- , not ghci_tv = CTE_Bad
- | otherwise = go w S.<> go a S.<> go r
+ go (LitTy {}) = cteOK
+ go (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})
+ = go w S.<> go a S.<> go r S.<>
+ if not ghci_tv && af == InvisArg
+ then impredicative
+ else cteOK
go (AppTy fun arg) = go fun S.<> go arg
go (CastTy ty co) = go ty S.<> go_co co
go (CoercionTy co) = go_co co
- go (ForAllTy (Bndr tv' _) ty)
- | not ghci_tv = CTE_Bad
- | otherwise = case lhs of
- TyVarLHS tv | tv == tv' -> CTE_OK
- | otherwise -> go_occ tv (tyVarKind tv') S.<> go ty
- _ -> go ty
+ go (ForAllTy (Bndr tv' _) ty) = (case lhs of
+ TyVarLHS tv | tv == tv' -> go_occ (tyVarKind tv') S.<> cterClearOccursCheck (go ty)
+ | otherwise -> go_occ (tyVarKind tv') S.<> go ty
+ _ -> go ty)
+ S.<>
+ if ghci_tv then cteOK else impredicative
go_tv :: TcTyVar -> CheckTyEqResult
-- this slightly peculiar way of defining this means
-- we don't have to evaluate this `case` at every variable
-- occurrence
go_tv = case lhs of
- TyVarLHS tv -> \ tv' -> if tv == tv'
- then CTE_Occurs
- else go_occ tv (tyVarKind tv')
- TyFamLHS {} -> \ _tv' -> CTE_OK
+ TyVarLHS tv -> \ tv' -> go_occ (tyVarKind tv') S.<>
+ if tv == tv' then insoluble_occurs else cteOK
+ TyFamLHS {} -> \ _tv' -> cteOK
-- See Note [Occurrence checking: look inside kinds] in GHC.Core.Type
-- For kinds, we only do an occurs check; we do not worry
-- about type families or foralls
-- See Note [Checking for foralls]
- go_occ tv k | tv `elemVarSet` tyCoVarsOfType k = CTE_Occurs
- | otherwise = CTE_OK
+ go_occ k = cterFromKind $ go k
go_tc :: TyCon -> [TcType] -> CheckTyEqResult
-- this slightly peculiar way of defining this means
-- we don't have to evaluate this `case` at every tyconapp
go_tc = case lhs of
- TyVarLHS {} -> \ tc tys ->
- if | good_tc tc -> mconcat (map go tys)
- | otherwise -> CTE_Bad
+ TyVarLHS {} -> \ tc tys -> check_tc tc S.<> go_tc_args tc tys
TyFamLHS fam_tc fam_args -> \ tc tys ->
- if | tcEqTyConApps fam_tc fam_args tc tys -> CTE_Occurs
- | good_tc tc -> mconcat (map go tys)
- | otherwise -> CTE_Bad
+ if tcEqTyConApps fam_tc fam_args tc tys
+ then insoluble_occurs
+ else check_tc tc S.<> go_tc_args tc tys
+ -- just look at arguments, not the tycon itself
+ go_tc_args :: TyCon -> [TcType] -> CheckTyEqResult
+ go_tc_args tc tys | isGenerativeTyCon tc Nominal = foldMap go tys
+ | otherwise
+ = let (tf_args, non_tf_args) = splitAt (tyConArity tc) tys in
+ cterSetOccursCheckSoluble (foldMap go tf_args) S.<> foldMap go non_tf_args
-- no bother about impredicativity in coercions, as they're
-- inferred
- go_co co | not (gopt Opt_DeferTypeErrors dflags)
- , hasCoercionHoleCo co
- = CTE_HoleBlocker -- Wrinkle (2) in GHC.Tc.Solver.Canonical
- -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
- -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for
- -- deferred type errors.
-
- | TyVarLHS tv <- lhs
+ go_co co | TyVarLHS tv <- lhs
, tv `elemVarSet` tyCoVarsOfCo co
- = CTE_Occurs
+ = soluble_occurs S.<> maybe_hole_blocker
-- Don't check coercions for type families; see commentary at top of function
| otherwise
- = CTE_OK
-
- good_tc :: TyCon -> Bool
- good_tc
- | ghci_tv = \ _tc -> True
- | otherwise = \ tc -> isTauTyCon tc &&
- (ty_fam_ok == YesTypeFamilies || isFamFreeTyCon tc)
+ = maybe_hole_blocker
+ where
+ -- See GHC.Tc.Solver.Canonical Note [Equalities with incompatible kinds]
+ -- Wrinkle (2) about this case in general, Wrinkle (4b) about the check for
+ -- deferred type errors
+ maybe_hole_blocker | not (gopt Opt_DeferTypeErrors dflags)
+ , hasCoercionHoleCo co
+ = hole_blocker
+
+ | otherwise
+ = cteOK
+
+ check_tc :: TyCon -> CheckTyEqResult
+ check_tc
+ | ghci_tv = \ _tc -> cteOK
+ | otherwise = \ tc -> (if isTauTyCon tc then cteOK else impredicative) S.<>
+ (if isFamFreeTyCon tc then cteOK else type_family)
View Lorry Controller Status