diff options
| author | Richard Eisenberg <rae@richarde.dev> | 2020-01-21 17:52:48 +0000 |
|---|---|---|
| committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2020-03-20 20:42:56 -0400 |
| commit | 73a7383ebc17f495d7acd04007c8c56b46532cb6 (patch) | |
| tree | b3c9cabb3dc8ae0e7808fda0d65fa8696ebe1570 | |
| parent | cb1785d9f839e34a3a4892f354f0c51cc6553c0e (diff) | |
| download | haskell-73a7383ebc17f495d7acd04007c8c56b46532cb6.tar.gz | |
Simplify treatment of heterogeneous equality
Previously, if we had a [W] (a :: k1) ~ (rhs :: k2), we would
spit out a [D] k1 ~ k2 and part the W as irreducible, hoping for
a unification. But we needn't do this. Instead, we now spit out
a [W] co :: k2 ~ k1 and then use co to cast the rhs of the original
Wanted. This means that we retain the connection between the
spat-out constraint and the original.
The problem with this new approach is that we cannot use the
casted equality for substitution; it's too like wanteds-rewriting-
wanteds. So, we forbid CTyEqCans that mention coercion holes.
All the details are in Note [Equalities with incompatible kinds]
in TcCanonical.
There are a few knock-on effects, documented where they occur.
While debugging an error in this patch, Simon and I ran into
infelicities in how patterns and matches are printed; we made
small improvements.
This patch includes mitigations for #17828, which causes spurious
pattern-match warnings. When #17828 is fixed, these lines should
be removed.
35 files changed, 631 insertions, 534 deletions
diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs index 626b1bbc78..317ca00906 100644 --- a/compiler/GHC/Core/Coercion.hs +++ b/compiler/GHC/Core/Coercion.hs @@ -12,7 +12,8 @@ module GHC.Core.Coercion ( -- * Main data type Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR, - UnivCoProvenance, CoercionHole(..), coHoleCoVar, setCoHoleCoVar, + UnivCoProvenance, CoercionHole(..), BlockSubstFlag(..), + coHoleCoVar, setCoHoleCoVar, LeftOrRight(..), Var, CoVar, TyCoVar, Role(..), ltRole, @@ -111,7 +112,9 @@ module GHC.Core.Coercion ( -- * Other promoteCoercion, buildCoercion, - simplifyArgsWorker + simplifyArgsWorker, + + badCoercionHole, badCoercionHoleCo ) where #include "HsVersions.h" @@ -148,6 +151,7 @@ import UniqFM import Control.Monad (foldM, zipWithM) import Data.Function ( on ) import Data.Char( isDigit ) +import qualified Data.Monoid as Monoid {- %************************************************************************ @@ -2904,3 +2908,40 @@ simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs ppr (take 10 orig_roles), -- often infinite! ppr orig_tys]) -} + +{- +%************************************************************************ +%* * + Coercion holes +%* * +%************************************************************************ +-} + +bad_co_hole_ty :: Type -> Monoid.Any +bad_co_hole_co :: Coercion -> Monoid.Any +(bad_co_hole_ty, _, bad_co_hole_co, _) + = foldTyCo folder () + where + folder = TyCoFolder { tcf_view = const Nothing + , tcf_tyvar = const2 (Monoid.Any False) + , tcf_covar = const2 (Monoid.Any False) + , tcf_hole = const hole + , tcf_tycobinder = const2 + } + + const2 :: a -> b -> c -> a + const2 x _ _ = x + + hole :: CoercionHole -> Monoid.Any + hole (CoercionHole { ch_blocker = YesBlockSubst }) = Monoid.Any True + hole _ = Monoid.Any False + +-- | Is there a blocking coercion hole in this type? See +-- TcCanonical Note [Equalities with incompatible kinds] +badCoercionHole :: Type -> Bool +badCoercionHole = Monoid.getAny . bad_co_hole_ty + +-- | Is there a blocking coercion hole in this coercion? See +-- TcCanonical Note [Equalities with incompatible kinds] +badCoercionHoleCo :: Coercion -> Bool +badCoercionHoleCo = Monoid.getAny . bad_co_hole_co diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs index 26c01ebcb8..c1ca32fc3c 100644 --- a/compiler/GHC/Core/TyCo/Rep.hs +++ b/compiler/GHC/Core/TyCo/Rep.hs @@ -39,7 +39,7 @@ module GHC.Core.TyCo.Rep ( -- * Coercions Coercion(..), UnivCoProvenance(..), - CoercionHole(..), coHoleCoVar, setCoHoleCoVar, + CoercionHole(..), BlockSubstFlag(..), coHoleCoVar, setCoHoleCoVar, CoercionN, CoercionR, CoercionP, KindCoercion, MCoercion(..), MCoercionR, MCoercionN, @@ -1487,12 +1487,18 @@ instance Outputable UnivCoProvenance where -- | A coercion to be filled in by the type-checker. See Note [Coercion holes] data CoercionHole - = CoercionHole { ch_co_var :: CoVar + = CoercionHole { ch_co_var :: CoVar -- See Note [CoercionHoles and coercion free variables] - , ch_ref :: IORef (Maybe Coercion) + , ch_blocker :: BlockSubstFlag -- should this hole block substitution? + -- See (2a) in TcCanonical + -- Note [Equalities with incompatible kinds] + , ch_ref :: IORef (Maybe Coercion) } +data BlockSubstFlag = YesBlockSubst + | NoBlockSubst + coHoleCoVar :: CoercionHole -> CoVar coHoleCoVar = ch_co_var @@ -1508,6 +1514,9 @@ instance Data.Data CoercionHole where instance Outputable CoercionHole where ppr (CoercionHole { ch_co_var = cv }) = braces (ppr cv) +instance Outputable BlockSubstFlag where + ppr YesBlockSubst = text "YesBlockSubst" + ppr NoBlockSubst = text "NoBlockSubst" {- Note [Phantom coercions] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs index 551401be6c..2e05270065 100644 --- a/compiler/GHC/Hs/Expr.hs +++ b/compiler/GHC/Hs/Expr.hs @@ -1089,10 +1089,9 @@ ppr_expr (XExpr x) = case ghcPass @p of GhcPs -> ppr x GhcRn -> ppr x GhcTc -> case x of - HsWrap co_fn e -> pprHsWrapper co_fn (\parens -> if parens then pprExpr e + HsWrap co_fn e -> pprHsWrapper co_fn (\parens -> if parens then pprExpr e else pprExpr e) - ppr_infix_expr :: forall p. (OutputableBndrId p) => HsExpr (GhcPass p) -> Maybe SDoc ppr_infix_expr (HsVar _ (L _ v)) = Just (pprInfixOcc v) ppr_infix_expr (HsConLikeOut _ c) = Just (pprInfixOcc (conLikeName c)) @@ -1118,7 +1117,7 @@ ppr_apps fun args = hang (ppr_expr fun) 2 (fsep (map pp args)) -- pp (Right (LHsWcTypeX (HsWC { hswc_body = L _ arg }))) -- = char '@' <> pprHsType arg pp (Right arg) - = char '@' <> ppr arg + = text "@" <> ppr arg pprExternalSrcLoc :: (StringLiteral,(Int,Int),(Int,Int)) -> SDoc pprExternalSrcLoc (StringLiteral _ src,(n1,n2),(n3,n4)) @@ -1712,41 +1711,39 @@ pprPatBind pat (grhss) pprMatch :: (OutputableBndrId idR, Outputable body) => Match (GhcPass idR) body -> SDoc -pprMatch match +pprMatch (Match { m_pats = pats, m_ctxt = ctxt, m_grhss = grhss }) = sep [ sep (herald : map (nest 2 . pprParendLPat appPrec) other_pats) - , nest 2 (pprGRHSs ctxt (m_grhss match)) ] + , nest 2 (pprGRHSs ctxt grhss) ] where - ctxt = m_ctxt match (herald, other_pats) = case ctxt of FunRhs {mc_fun=L _ fun, mc_fixity=fixity, mc_strictness=strictness} - | strictness == SrcStrict -> ASSERT(null $ m_pats match) - (char '!'<>pprPrefixOcc fun, m_pats match) - -- a strict variable binding - | fixity == Prefix -> (pprPrefixOcc fun, m_pats match) - -- f x y z = e - -- Not pprBndr; the AbsBinds will - -- have printed the signature - - | null pats2 -> (pp_infix, []) - -- x &&& y = e - - | otherwise -> (parens pp_infix, pats2) - -- (x &&& y) z = e - where - pp_infix = pprParendLPat opPrec pat1 - <+> pprInfixOcc fun - <+> pprParendLPat opPrec pat2 - - LambdaExpr -> (char '\\', m_pats match) - - _ -> if null (m_pats match) - then (empty, []) - else ASSERT2( null pats1, ppr ctxt $$ ppr pat1 $$ ppr pats1 ) - (ppr pat1, []) -- No parens around the single pat - - (pat1:pats1) = m_pats match - (pat2:pats2) = pats1 + | SrcStrict <- strictness + -> ASSERT(null pats) -- A strict variable binding + (char '!'<>pprPrefixOcc fun, pats) + + | Prefix <- fixity + -> (pprPrefixOcc fun, pats) -- f x y z = e + -- Not pprBndr; the AbsBinds will + -- have printed the signature + | otherwise + -> case pats of + (p1:p2:rest) + | null rest -> (pp_infix, []) -- x &&& y = e + | otherwise -> (parens pp_infix, rest) -- (x &&& y) z = e + where + pp_infix = pprParendLPat opPrec p1 + <+> pprInfixOcc fun + <+> pprParendLPat opPrec p2 + _ -> pprPanic "pprMatch" (ppr ctxt $$ ppr pats) + + LambdaExpr -> (char '\\', pats) + + _ -> case pats of + [] -> (empty, []) + [pat] -> (ppr pat, []) -- No parens around the single pat in a case + _ -> pprPanic "pprMatch" (ppr ctxt $$ ppr pats) +pprMatch (XMatch nec) = noExtCon nec pprGRHSs :: (OutputableBndrId idR, Outputable body) => HsMatchContext passL -> GRHSs (GhcPass idR) body -> SDoc diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs index c427d977ed..1bddfa2c71 100644 --- a/compiler/GHC/Hs/Pat.hs +++ b/compiler/GHC/Hs/Pat.hs @@ -1,3 +1,4 @@ + {- (c) The University of Glasgow 2006 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 @@ -58,6 +59,7 @@ import TcEvidence import BasicTypes -- others: import GHC.Core.Ppr ( {- instance OutputableBndr TyVar -} ) +import GHC.Driver.Session ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) ) import TysWiredIn import Var import RdrName ( RdrName ) @@ -526,10 +528,11 @@ pprPat (NPat _ l (Just _) _) = char '-' <> ppr l pprPat (NPlusKPat _ n k _ _ _) = hcat [ppr n, char '+', ppr k] pprPat (SplicePat _ splice) = pprSplice splice pprPat (CoPat _ co pat _) = pprIfTc @p $ - pprHsWrapper co $ \parens - -> if parens - then pprParendPat appPrec pat - else pprPat pat + sdocWithDynFlags $ \ dflags -> + if gopt Opt_PrintTypecheckerElaboration dflags + then hang (text "CoPat" <+> parens (ppr co)) + 2 (pprParendPat appPrec pat) + else pprPat pat pprPat (SigPat _ pat ty) = ppr pat <+> dcolon <+> ppr_ty where ppr_ty = case ghcPass @p of GhcPs -> ppr ty diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs index 3891be649d..61278391d0 100644 --- a/compiler/GHC/HsToCore/PmCheck.hs +++ b/compiler/GHC/HsToCore/PmCheck.hs @@ -32,7 +32,7 @@ import GHC.Core (CoreExpr, Expr(Var,App)) import FastString (unpackFS, lengthFS) import GHC.Driver.Session import GHC.Hs -import TcHsSyn +import TcHsSyn ( shortCutLit ) import Id import GHC.Core.ConLike import Name @@ -45,7 +45,7 @@ import GHC.Core.DataCon import GHC.Core.TyCon import Var (EvVar) import GHC.Core.Coercion -import TcEvidence +import TcEvidence ( HsWrapper(..), isIdHsWrapper ) import TcType (evVarPred) import {-# SOURCE #-} GHC.HsToCore.Expr (dsExpr, dsLExpr, dsSyntaxExpr) import {-# SOURCE #-} GHC.HsToCore.Binds (dsHsWrapper) @@ -999,7 +999,7 @@ checkGrdTree guards deltas = do tracePm "checkGrdTree {" $ vcat [ ppr guards , ppr deltas ] res <- checkGrdTree' guards deltas - tracePm "}:" (ppr res) -- braces are easier to match by tooling + tracePm "checkGrdTree }:" (ppr res) -- braces are easier to match by tooling return res -- ---------------------------------------------------------------------------- diff --git a/compiler/typecheck/Constraint.hs b/compiler/typecheck/Constraint.hs index 4855b5c57c..20a1a7d774 100644 --- a/compiler/typecheck/Constraint.hs +++ b/compiler/typecheck/Constraint.hs @@ -14,7 +14,7 @@ module Constraint ( QCInst(..), isPendingScInst, -- Canonical constraints - Xi, Ct(..), Cts, emptyCts, andCts, andManyCts, pprCts, + Xi, Ct(..), Cts, CtIrredStatus(..), emptyCts, andCts, andManyCts, pprCts, singleCt, listToCts, ctsElts, consCts, snocCts, extendCtsList, isEmptyCts, isCTyEqCan, isCFunEqCan, isPendingScDict, superClassesMightHelp, getPendingWantedScs, @@ -25,7 +25,7 @@ module Constraint ( ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin, ctEvId, mkTcEqPredLikeEv, mkNonCanonical, mkNonCanonicalCt, mkGivens, - mkIrredCt, mkInsolubleCt, + mkIrredCt, ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel, ctEvExpr, ctEvTerm, ctEvCoercion, ctEvEvId, tyCoVarsOfCt, tyCoVarsOfCts, @@ -145,13 +145,12 @@ data Ct } | CIrredCan { -- These stand for yet-unusable predicates - cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] - cc_insol :: Bool -- True <=> definitely an error, can never be solved - -- False <=> might be soluble + cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] + cc_status :: CtIrredStatus -- 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 (tv1 ~ ty2) where the CTyEqCan kind invariant fails + -- or (tv1 ~ ty2) where the CTyEqCan kind invariant (TyEq:K) fails -- or (F tys ~ ty) where the CFunEqCan kind invariant fails -- See Note [CIrredCan constraints] @@ -163,19 +162,21 @@ data Ct | CTyEqCan { -- tv ~ rhs -- Invariants: -- * See Note [inert_eqs: the inert equalities] in TcSMonad - -- * tv not in tvs(rhs) (occurs check) - -- * If tv is a TauTv, then rhs has no foralls + -- * (TyEq:OC) tv not in deep tvs(rhs) (occurs check) + -- * (TyEq:F) If tv is a TauTv, then rhs has no foralls -- (this avoids substituting a forall for the tyvar in other types) - -- * tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant] - -- * rhs may have at most one top-level cast - -- * rhs (perhaps under the one cast) is *almost function-free*, + -- * (TyEq:K) tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant] + -- * (TyEq:AFF) rhs (perhaps under the one cast) is *almost function-free*, -- See Note [Almost function-free] - -- * If the equality is representational, rhs has no top-level newtype + -- * (TyEq:N) If the equality is representational, rhs has no top-level newtype -- See Note [No top-level newtypes on RHS of representational -- equalities] in TcCanonical - -- * If rhs (perhaps under the cast) is also a tv, then it is oriented + -- * (TyEq:TV) If rhs (perhaps under the cast) is also a tv, then it is oriented -- to give best chance of -- unification happening; eg if rhs is touchable then lhs is too + -- See TcCanonical Note [Canonical orientation for tyvar/tyvar equality constraints] + -- * (TyEq:H) The RHS has no blocking coercion holes. See TcCanonical + -- Note [Equalities with incompatible kinds], wrinkle (2) cc_ev :: CtEvidence, -- See Note [Ct/evidence invariant] cc_tyvar :: TcTyVar, cc_rhs :: TcType, -- Not necessarily function-free (hence not Xi) @@ -241,6 +242,21 @@ data HoleSort = ExprHole | TypeHole -- ^ A hole in a type (PartialTypeSignatures) +------------ +-- | Used to indicate extra information about why a CIrredCan is irreducible +data CtIrredStatus + = InsolubleCIS -- this constraint will never be solved + | BlockedCIS -- this constraint is blocked on a coercion hole + -- The hole will appear in the ctEvPred of the constraint with this status + -- See Note [Equalities with incompatible kinds] in TcCanonical + -- Wrinkle (4a) + | OtherCIS + +instance Outputable CtIrredStatus where + ppr InsolubleCIS = text "(insoluble)" + ppr BlockedCIS = text "(blocked)" + ppr OtherCIS = text "(soluble)" + {- Note [Hole constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~ CHoleCan constraints are used for two kinds of holes, @@ -296,7 +312,8 @@ responds True to isTypeFamilyTyCon), except (possibly) * under a forall, or * in a coercion (either in a CastTy or a CercionTy) -The RHS of a CTyEqCan must be almost function-free. This is for two reasons: +The RHS of a CTyEqCan must be almost function-free, invariant (TyEq:AFF). +This is for two reasons: 1. There cannot be a top-level function. If there were, the equality should really be a CFunEqCan, not a CTyEqCan. @@ -346,11 +363,8 @@ mkNonCanonical ev = CNonCanonical { cc_ev = ev } mkNonCanonicalCt :: Ct -> Ct mkNonCanonicalCt ct = CNonCanonical { cc_ev = cc_ev ct } -mkIrredCt :: CtEvidence -> Ct -mkIrredCt ev = CIrredCan { cc_ev = ev, cc_insol = False } - -mkInsolubleCt :: CtEvidence -> Ct -mkInsolubleCt ev = CIrredCan { cc_ev = ev, cc_insol = True } +mkIrredCt :: CtIrredStatus -> CtEvidence -> Ct +mkIrredCt status ev = CIrredCan { cc_ev = ev, cc_status = status } mkGivens :: CtLoc -> [EvId] -> [Ct] mkGivens loc ev_ids @@ -409,9 +423,7 @@ instance Outputable Ct where CDictCan { cc_pend_sc = pend_sc } | pend_sc -> text "CDictCan(psc)" | otherwise -> text "CDictCan" - CIrredCan { cc_insol = insol } - | insol -> text "CIrredCan(insol)" - | otherwise -> text "CIrredCan(sol)" + CIrredCan { cc_status = status } -> text "CIrredCan" <> ppr status CHoleCan { cc_occ = occ } -> text "CHoleCan:" <+> ppr occ CQuantCan (QCI { qci_pend_sc = pend_sc }) | pend_sc -> text "CQuantCan(psc)" @@ -439,14 +451,10 @@ tyCoVarsOfCtList = fvVarList . tyCoFVsOfCt -- | Returns free variables of constraints as a composable FV computation. -- See Note [Deterministic FV] in FV. tyCoFVsOfCt :: Ct -> FV -tyCoFVsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi }) - = tyCoFVsOfType xi `unionFV` FV.unitFV tv - `unionFV` tyCoFVsOfType (tyVarKind tv) -tyCoFVsOfCt (CFunEqCan { cc_tyargs = tys, cc_fsk = fsk }) - = tyCoFVsOfTypes tys `unionFV` FV.unitFV fsk - `unionFV` tyCoFVsOfType (tyVarKind fsk) -tyCoFVsOfCt (CDictCan { cc_tyargs = tys }) = tyCoFVsOfTypes tys tyCoFVsOfCt ct = tyCoFVsOfType (ctPred ct) + -- This must consult only the ctPred, so that it gets *tidied* fvs if the + -- constraint has been tidied. Tidying a constraint does not tidy the + -- fields of the Ct, only the predicate in the CtEvidence. -- | Returns free variables of a bag of constraints as a non-deterministic -- set. See Note [Deterministic FV] in FV. @@ -549,18 +557,15 @@ isDroppableCt ct keep_deriv = case ct of - CHoleCan {} -> True - CIrredCan { cc_insol = insoluble } - -> keep_eq insoluble - _ -> keep_eq False + CHoleCan {} -> True + CIrredCan { cc_status = InsolubleCIS } -> keep_eq True + _ -> keep_eq False keep_eq definitely_insoluble | isGivenOrigin orig -- Arising only from givens = definitely_insoluble -- Keep only definitely insoluble | otherwise = case orig of - KindEqOrigin {} -> True -- See Note [Dropping derived constraints] - -- See Note [Dropping derived constraints] -- For fundeps, drop wanted/wanted interactions FunDepOrigin2 {} -> True -- Top-level/Wanted @@ -610,12 +615,6 @@ But (tiresomely) we do keep *some* Derived constraints: * Type holes are derived constraints, because they have no evidence and we want to keep them, so we get the error report - * Insoluble kind equalities (e.g. [D] * ~ (* -> *)), with - KindEqOrigin, may arise from a type equality a ~ Int#, say. See - Note [Equalities with incompatible kinds] in TcCanonical. - Keeping these around produces better error messages, in practice. - E.g., test case dependent/should_fail/T11471 - * We keep most derived equalities arising from functional dependencies - Given/Given interactions (subset of FunDepOrigin1): The definitely-insoluble ones reflect unreachable code. @@ -664,7 +663,6 @@ isDerivedCt = isDerived . ctEvidence isCTyEqCan :: Ct -> Bool isCTyEqCan (CTyEqCan {}) = True -isCTyEqCan (CFunEqCan {}) = False isCTyEqCan _ = False isCDictCan_Maybe :: Ct -> Maybe Class @@ -990,8 +988,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_insol = insol }) = insol -insolubleEqCt _ = False +insolubleEqCt (CIrredCan { cc_status = InsolubleCIS }) = True +insolubleEqCt _ = False instance Outputable WantedConstraints where ppr (WC {wc_simple = s, wc_impl = i}) diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs index 33b15aa292..7dbe32d9c0 100644 --- a/compiler/typecheck/TcCanonical.hs +++ b/compiler/typecheck/TcCanonical.hs @@ -16,7 +16,7 @@ import GhcPrelude import Constraint import GHC.Core.Predicate import TcOrigin -import TcUnify( swapOverTyVars, metaTyVarUpdateOK ) +import TcUnify( swapOverTyVars, metaTyVarUpdateOK, MetaTyVarUpdateResult(..) ) import TcType import GHC.Core.Type import TcFlatten @@ -95,7 +95,7 @@ canonicalize (CNonCanonical { cc_ev = ev }) EqPred eq_rel ty1 ty2 -> do traceTcS "canEvNC:eq" (ppr ty1 $$ ppr ty2) canEqNC ev eq_rel ty1 ty2 IrredPred {} -> do traceTcS "canEvNC:irred" (ppr pred) - canIrred ev + canIrred OtherCIS ev ForAllPred tvs theta p -> do traceTcS "canEvNC:forall" (ppr pred) canForAllNC ev tvs theta p where @@ -104,7 +104,7 @@ canonicalize (CNonCanonical { cc_ev = ev }) canonicalize (CQuantCan (QCI { qci_ev = ev, qci_pend_sc = pend_sc })) = canForAll ev pend_sc -canonicalize (CIrredCan { cc_ev = ev }) +canonicalize (CIrredCan { cc_ev = ev, cc_status = status }) | EqPred eq_rel ty1 ty2 <- classifyPredType (ctEvPred ev) = -- For insolubles (all of which are equalities, do /not/ flatten the arguments -- In #14350 doing so led entire-unnecessary and ridiculously large @@ -114,7 +114,7 @@ canonicalize (CIrredCan { cc_ev = ev }) canEqNC ev eq_rel ty1 ty2 | otherwise - = canIrred ev + = canIrred status ev canonicalize (CDictCan { cc_ev = ev, cc_class = cls , cc_tyargs = xis, cc_pend_sc = pend_sc }) @@ -704,9 +704,9 @@ See also Note [Evidence for quantified constraints] in GHC.Core.Predicate. ************************************************************************ -} -canIrred :: CtEvidence -> TcS (StopOrContinue Ct) +canIrred :: CtIrredStatus -> CtEvidence -> TcS (StopOrContinue Ct) -- Precondition: ty not a tuple and no other evidence form -canIrred ev +canIrred status ev = do { let pred = ctEvPred ev ; traceTcS "can_pred" (text "IrredPred = " <+> ppr pred) ; (xi,co) <- flatten FM_FlattenAll ev pred -- co :: xi ~ pred @@ -716,7 +716,7 @@ canIrred ev ClassPred cls tys -> canClassNC new_ev cls tys EqPred eq_rel ty1 ty2 -> canEqNC new_ev eq_rel ty1 ty2 _ -> continueWith $ - mkIrredCt new_ev } } + mkIrredCt status new_ev } } canHole :: CtEvidence -> OccName -> HoleSort -> TcS (StopOrContinue Ct) canHole ev occ hole_sort @@ -984,6 +984,7 @@ can_eq_nc' True _rdr_env _envs ev ReprEq ty1 _ ty2 _ -- When working with ReprEq, unwrap newtypes. -- See Note [Unwrap newtypes first] +-- This must be above the TyVarTy case, in order to guarantee (TyEq:N) can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 | ReprEq <- eq_rel , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1 @@ -995,8 +996,10 @@ can_eq_nc' _flat rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2 -- Then, get rid of casts can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2 + | not (isTyVarTy ty2) -- See (3) in Note [Equalities with incompatible kinds] = canEqCast flat ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2 can_eq_nc' flat _rdr_env _envs ev eq_rel ty1 ps_ty1 (CastTy ty2 co2) _ + | not (isTyVarTy ty1) -- See (3) in Note [Equalities with incompatible kinds] = canEqCast flat ev eq_rel IsSwapped ty2 co2 ty1 ps_ty1 -- NB: pattern match on True: we want only flat types sent to canEqTyVar. @@ -1051,8 +1054,8 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ 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 ev) - NomEq -> continueWith (mkInsolubleCt ev) } + ReprEq -> continueWith (mkIrredCt OtherCIS ev) + NomEq -> continueWith (mkIrredCt InsolubleCIS ev) } -- No need to call canEqFailure/canEqHardFailure because they -- flatten, and the types involved here are already flat @@ -1478,7 +1481,7 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2 -- See Note [Skolem abstract data] (at tyConSkolem) | tyConSkolem tc1 || tyConSkolem tc2 = do { traceTcS "canTyConApp: skolem abstract" (ppr tc1 $$ ppr tc2) - ; continueWith (mkIrredCt ev) } + ; continueWith (mkIrredCt OtherCIS ev) } -- Fail straight away for better error messages -- See Note [Use canEqFailure in canDecomposableTyConApp] @@ -1752,7 +1755,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 new_ev) } + ; continueWith (mkIrredCt OtherCIS new_ev) } -- | Call when canonicalizing an equality fails with utterly no hope. canEqHardFailure :: CtEvidence @@ -1762,7 +1765,7 @@ canEqHardFailure ev ty1 ty2 = do { (s1, co1) <- flatten FM_SubstOnly ev ty1 ; (s2, co2) <- flatten FM_SubstOnly ev ty2 ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 - ; continueWith (mkInsolubleCt new_ev) } + ; continueWith (mkIrredCt InsolubleCIS new_ev) } {- Note [Decomposing TyConApps] @@ -1948,118 +1951,61 @@ canEqTyVar ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2 | k1 `tcEqType` k2 = canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 ps_xi2 - -- So the LHS and RHS don't have equal kinds - -- Note [Flattening] in TcFlatten gives us (F2), which says that - -- flattening is always homogeneous (doesn't change kinds). But - -- perhaps by flattening the kinds of the two sides of the equality - -- at hand makes them equal. So let's try that. | otherwise - = do { (flat_k1, k1_co) <- flattenKind loc flav k1 -- k1_co :: flat_k1 ~N kind(xi1) - ; (flat_k2, k2_co) <- flattenKind loc flav k2 -- k2_co :: flat_k2 ~N kind(xi2) - ; traceTcS "canEqTyVar tried flattening kinds" - (vcat [ sep [ parens (ppr tv1 <+> dcolon <+> ppr k1) - , text "~" - , parens (ppr xi2 <+> dcolon <+> ppr k2) ] - , ppr flat_k1 - , ppr k1_co - , ppr flat_k2 - , ppr k2_co ]) - - -- We know the LHS is a tyvar. So let's dump all the coercions on the RHS - -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and - -- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence - -- (as an optimization, so that we don't have to flatten the kinds again) - -- and then emit a kind equality in canEqTyVarHetero. - -- See Note [Equalities with incompatible kinds] - - ; let role = eqRelRole eq_rel - ; if flat_k1 `tcEqType` flat_k2 - then do { let rhs_kind_co = mkTcSymCo k2_co `mkTcTransCo` k1_co - -- :: kind(xi2) ~N kind(xi1) - - new_rhs = xi2 `mkCastTy` rhs_kind_co - ps_rhs = ps_xi2 `mkCastTy` rhs_kind_co - rhs_co = mkTcGReflLeftCo role xi2 rhs_kind_co - - ; new_ev <- rewriteEqEvidence ev swapped xi1 new_rhs - (mkTcReflCo role xi1) rhs_co - -- NB: rewriteEqEvidence executes a swap, if any, so we're - -- NotSwapped now. - ; canEqTyVarHomo new_ev eq_rel NotSwapped tv1 ps_xi1 new_rhs ps_rhs } - else - do { let sym_k1_co = mkTcSymCo k1_co -- :: kind(xi1) ~N flat_k1 - sym_k2_co = mkTcSymCo k2_co -- :: kind(xi2) ~N flat_k2 - - new_lhs = xi1 `mkCastTy` sym_k1_co -- :: flat_k1 - new_rhs = xi2 `mkCastTy` sym_k2_co -- :: flat_k2 - ps_rhs = ps_xi2 `mkCastTy` sym_k2_co - - lhs_co = mkTcGReflLeftCo role xi1 sym_k1_co - rhs_co = mkTcGReflLeftCo role xi2 sym_k2_co - -- lhs_co :: (xi1 |> sym k1_co) ~ xi1 - -- rhs_co :: (xi2 |> sym k2_co) ~ xi2 + = canEqTyVarHetero ev eq_rel swapped tv1 ps_xi1 k1 xi2 ps_xi2 k2 - ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co - -- no longer swapped, due to rewriteEqEvidence - ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_xi1 - new_rhs flat_k2 ps_rhs } } where - xi1 = mkTyVarTy tv1 - k1 = tyVarKind tv1 k2 = tcTypeKind xi2 - loc = ctEvLoc ev - flav = ctEvFlavour ev - -canEqTyVarHetero :: CtEvidence -- :: (tv1 |> co1 :: ki1) ~ (xi2 :: ki2) - -> EqRel - -> TcTyVar -> TcCoercionN -> TcKind -- tv1 |> co1 :: ki1 - -> TcType -- pretty tv1 (*without* the coercion) - -> TcType -> TcKind -- xi2 :: ki2 - -> TcType -- pretty xi2 +canEqTyVarHetero :: CtEvidence -- :: (tv1 :: ki1) ~ (xi2 :: ki2) + -> EqRel -> SwapFlag + -> TcTyVar -> TcType -- tv1, pretty tv1 + -> TcKind -- ki1 + -> TcType -> TcType -- xi2, pretty xi2 :: ki2 + -> TcKind -- ki2 -> TcS (StopOrContinue Ct) -canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2 +canEqTyVarHetero ev eq_rel swapped tv1 ps_tv1 ki1 xi2 ps_xi2 ki2 -- See Note [Equalities with incompatible kinds] - | CtGiven { ctev_evar = evar } <- ev - -- unswapped: tm :: (lhs :: ki1) ~ (rhs :: ki2) - -- swapped : tm :: (rhs :: ki2) ~ (lhs :: ki1) - = do { let kind_co = mkTcKindCo (mkTcCoVarCo evar) - ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co) - ; let -- kind_ev :: (ki1 :: *) ~ (ki2 :: *) (whether swapped or not) + = do { kind_co <- emit_kind_co -- :: ki2 ~N ki1 + + ; let -- kind_co :: (ki2 :: *) ~N (ki1 :: *) (whether swapped or not) -- co1 :: kind(tv1) ~N ki1 - -- homo_co :: ki2 ~N kind(tv1) - homo_co = mkTcSymCo (ctEvCoercion kind_ev) `mkTcTransCo` mkTcSymCo co1 - rhs' = mkCastTy xi2 homo_co -- :: kind(tv1) - ps_rhs' = mkCastTy ps_xi2 homo_co -- :: kind(tv1) - rhs_co = mkTcGReflLeftCo role xi2 homo_co - -- rhs_co :: (xi2 |> homo_co :: kind(tv1)) ~ xi2 - - lhs' = mkTyVarTy tv1 -- :: kind(tv1) - lhs_co = mkTcGReflRightCo role lhs' co1 - -- lhs_co :: (tv1 :: kind(tv1)) ~ (tv1 |> co1 :: ki1) - - ; traceTcS "Hetero equality gives rise to given kind equality" - (ppr kind_ev <+> dcolon <+> ppr kind_pty) - ; emitWorkNC [kind_ev] - ; type_ev <- rewriteEqEvidence ev NotSwapped lhs' rhs' lhs_co rhs_co - ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' } + rhs' = xi2 `mkCastTy` kind_co -- :: ki1 + ps_rhs' = ps_xi2 `mkCastTy` kind_co -- :: ki1 + rhs_co = mkTcGReflLeftCo role xi2 kind_co + -- rhs_co :: (xi2 |> kind_co) ~ xi2 - -- See Note [Equalities with incompatible kinds] - | otherwise -- Wanted and Derived - -- NB: all kind equalities are Nominal - = do { emitNewDerivedEq kind_loc Nominal ki1 ki2 - -- kind_ev :: (ki1 :: *) ~ (ki2 :: *) - ; traceTcS "Hetero equality gives rise to derived kind equality" $ - ppr ev - ; continueWith (mkIrredCt ev) } + lhs' = mkTyVarTy tv1 -- same as old lhs + lhs_co = mkTcReflCo role lhs' + + ; traceTcS "Hetero equality gives rise to kind equality" + (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ]) + ; type_ev <- rewriteEqEvidence ev swapped lhs' rhs' lhs_co rhs_co + -- rewriteEqEvidence carries out the swap, so we're NotSwapped any more + ; canEqTyVarHomo type_ev eq_rel NotSwapped tv1 ps_tv1 rhs' ps_rhs' } where - kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2 - kind_loc = mkKindLoc (mkTyVarTy tv1 `mkCastTy` co1) xi2 loc + emit_kind_co :: TcS CoercionN + emit_kind_co + | CtGiven { ctev_evar = evar } <- ev + = do { let kind_co = maybe_sym $ mkTcKindCo (mkTcCoVarCo evar) -- :: k2 ~ k1 + ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co) + ; emitWorkNC [kind_ev] + ; return (ctEvCoercion kind_ev) } - loc = ctev_loc ev - role = eqRelRole eq_rel + | otherwise + = unifyWanted kind_loc Nominal ki2 ki1 + + loc = ctev_loc ev + role = eqRelRole eq_rel + kind_loc = mkKindLoc (mkTyVarTy tv1) xi2 loc + kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki2 ki1 + + maybe_sym = case swapped of + IsSwapped -> id -- if the input is swapped, then we already + -- will have k2 ~ k1 + NotSwapped -> mkTcSymCo -- guaranteed that tcTypeKind lhs == tcTypeKind rhs canEqTyVarHomo :: CtEvidence @@ -2074,14 +2020,10 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _ = canEqReflexive ev eq_rel (mkTyVarTy tv1) -- we don't need to check co because it must be reflexive + -- this guarantees (TyEq:TV) | Just (tv2, co2) <- tcGetCastedTyVar_maybe xi2 , swapOverTyVars tv1 tv2 = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped) - -- FM_Avoid commented out: see Note [Lazy flattening] in TcFlatten - -- let fmode = FE { fe_ev = ev, fe_mode = FM_Avoid tv1' True } - -- Flatten the RHS less vigorously, to avoid gratuitous flattening - -- True <=> xi2 should not itself be a type-function application - ; let role = eqRelRole eq_rel sym_co2 = mkTcSymCo co2 ty1 = mkTyVarTy tv1 @@ -2112,11 +2054,17 @@ canEqTyVar2 :: DynFlags -- LHS is an inert type variable, -- and RHS is fully rewritten, but with type synonyms -- preserved as much as possible +-- guaranteed that tyVarKind lhs == typeKind rhs, for (TyEq:K) +-- the "flat" requirement guarantees (TyEq:AFF) +-- (TyEq:N) is checked in can_eq_nc', and (TyEq:TV) is handled in canEqTyVarHomo canEqTyVar2 dflags ev eq_rel swapped tv1 rhs - | Just rhs' <- metaTyVarUpdateOK dflags tv1 rhs -- No occurs check + -- this next line checks also for coercion holes; see + -- Note [Equalities with incompatible kinds] + | MTVU_OK rhs' <- mtvu -- No occurs check -- 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) = do { new_ev <- rewriteEqEvidence ev swapped lhs rhs' rewrite_co1 rewrite_co2 ; continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1 , cc_rhs = rhs', cc_eq_rel = eq_rel }) } @@ -2125,20 +2073,30 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 rhs -- We must not use it for further rewriting! = do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr rhs) ; new_ev <- rewriteEqEvidence ev swapped lhs rhs rewrite_co1 rewrite_co2 - ; if isInsolubleOccursCheck eq_rel tv1 rhs - then continueWith (mkInsolubleCt new_ev) + ; let status | isInsolubleOccursCheck eq_rel tv1 rhs + = 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 - else continueWith (mkIrredCt new_ev) } + | MTVU_HoleBlocker <- mtvu + = BlockedCIS + -- This is the case detailed in + -- Note [Equalities with incompatible kinds] + + | otherwise + = 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. + + ; continueWith (mkIrredCt status new_ev) } where + mtvu = metaTyVarUpdateOK dflags tv1 rhs + role = eqRelRole eq_rel lhs = mkTyVarTy tv1 @@ -2162,57 +2120,92 @@ What do we do when we have an equality (tv :: k1) ~ (rhs :: k2) -where k1 and k2 differ? This Note explores this treacherous area. - -We must proceed differently here depending on whether we have a Wanted -or a Given. Consider this: - - [W] w :: (alpha :: k) ~ (Int :: Type) - -where k is a skolem. One possible way forward is this: - - [W] co :: k ~ Type - [W] w :: (alpha :: k) ~ (Int |> sym co :: k) - -The next step will be to unify - - alpha := Int |> sym co +where k1 and k2 differ? Easy: we create a coercion that relates k1 and +k2 and use this to cast. To wit, from -Now, consider what error we'll report if we can't solve the "co" -wanted. Its CtOrigin is the w wanted... which now reads (after zonking) -Int ~ Int. The user thus sees that GHC can't solve Int ~ Int, which -is embarrassing. See #11198 for more tales of destruction. + [X] (tv :: k1) ~ (rhs :: k2) -The reason for this odd behavior is much the same as -Note [Wanteds do not rewrite Wanteds] in Constraint: note that the -new `co` is a Wanted. +we go to -The solution is then not to use `co` to "rewrite" -- that is, cast -- `w`, but -instead to keep `w` heterogeneous and irreducible. Given that we're not using -`co`, there is no reason to collect evidence for it, so `co` is born a -Derived, with a CtOrigin of KindEqOrigin. When the Derived is solved (by -unification), the original wanted (`w`) will get kicked out. We thus get + [noDerived X] co :: k2 ~ k1 + [X] (tv :: k1) ~ ((rhs |> co) :: k1) -[D] _ :: k ~ Type -[W] w :: (alpha :: k) ~ (Int :: Type) - -Note that the Wanted is unchanged and will be irreducible. This all happens -in canEqTyVarHetero. - -Note that, if we had [G] co1 :: k ~ Type available, then we never get -to canEqTyVarHetero: canEqTyVar tries flattening the kinds first. If -we have [G] co1 :: k ~ Type, then flattening the kind of alpha would -rewrite k to Type, and we would end up in canEqTyVarHomo. - -Successive canonicalizations of the same Wanted may produce -duplicate Deriveds. Similar duplications can happen with fundeps, and there -seems to be no easy way to avoid. I expect this case to be rare. +where -For Givens, this problem (the Wanteds-rewriting-Wanteds action of -a kind coercion) doesn't bite, so a heterogeneous Given gives -rise to a Given kind equality. No Deriveds here. We thus homogenise -the Given (see the "homo_co" in the Given case in canEqTyVarHetero) and -carry on with a homogeneous equality constraint. + noDerived G = G + noDerived _ = W + +Wrinkles: + + (1) The noDerived step is because Derived equalities have no evidence. + And yet we absolutely need evidence to be able to proceed here. + Given evidence will use the KindCo coercion; Wanted evidence will + be a coercion hole. Even a Derived hetero equality begets a Wanted + kind equality. + + (2) Though it would be sound to do so, we must not mark the rewritten Wanted + [W] (tv :: k1) ~ ((rhs |> co) :: k1) + as canonical in the inert set. In particular, we must not unify tv. + If we did, the Wanted becomes a Given (effectively), and then can + rewrite other Wanteds. But that's bad: See Note [Wanteds to not rewrite Wanteds] + in Constraint. The problem is about poor error messages. See #11198 for + tales of destruction. + + So, we have an invariant on CTyEqCan (TyEq:H) that the RHS does not have + any coercion holes. This is checked in metaTyVarUpdateOK. We also + must be sure to kick out any constraints that mention coercion holes + when those holes get filled in. + + (2a) We don't want to do this for CoercionHoles that witness + CFunEqCans (that are produced by the flattener), as these will disappear + once we unflatten. So we remember in the CoercionHole structure + whether the presence of the hole should block substitution or not. + A bit gross, this. + + (2b) We must now absolutely make sure to kick out any constraints that + mention a newly-filled-in coercion hole. This is done in + kickOutAfterFillingCoercionHole. + + (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the + algorithm detailed here, producing [W] co :: k2 ~ k1, and adding + [W] (a :: k1) ~ ((rhs |> co) :: k1) to the irreducibles. Some time + later, we solve co, and fill in co's coercion hole. This kicks out + the irreducible as described in (2b). + But now, during canonicalization, we see the cast + and remove it, in canEqCast. By the time we get into canEqTyVar, the equality + is heterogeneous again, and the process repeats. + + To avoid this, we don't strip casts off a type if the other type + in the equality is a tyvar. And this is an improvement regardless: + because tyvars can, generally, unify with casted types, there's no + reason to go through the work of stripping off the cast when the + 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 only because + of wrinkle (2) 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 + be reported. We thus push such errors to the bottom of the queue + in the error-reporting code; they should never be printed. + + (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. + 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. + + (4b) The error message might be printed with -fdefer-type-errors, + so it still must exist. This is the only reason why there is + a message at all. Otherwise, we could simply do nothing. + +Historical note: + +We used to do this via emitting a Derived kind equality and then parking +the heterogeneous equality as irreducible. But this new approach is much +more direct. And it doesn't produce duplicate Deriveds (as the old one did). Note [Type synonyms and canonicalization] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2376,7 +2369,6 @@ rewriteEqEvidence :: CtEvidence -- Old evidence :: olhs ~ orhs (not swap -- or orhs ~ olhs (swapped) -> SwapFlag -> TcType -> TcType -- New predicate nlhs ~ nrhs - -- Should be zonked, because we use tcTypeKind on nlhs/nrhs -> TcCoercion -- lhs_co, of type :: nlhs ~ olhs -> TcCoercion -- rhs_co, of type :: nrhs ~ orhs -> TcS CtEvidence -- Of type nlhs ~ nrhs @@ -2411,16 +2403,21 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co ; newGivenEvVar loc' (new_pred, new_tm) } | CtWanted { ctev_dest = dest, ctev_nosh = si } <- old_ev - = do { (new_ev, hole_co) <- newWantedEq_SI si loc' (ctEvRole old_ev) nlhs nrhs - -- The "_SI" variant ensures that we make a new Wanted - -- with the same shadow-info as the existing one (#16735) - ; let co = maybeSym swapped $ - mkSymCo lhs_co - `mkTransCo` hole_co - `mkTransCo` rhs_co - ; setWantedEq dest co - ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co]) - ; return new_ev } + = case dest of + HoleDest hole -> + do { (new_ev, hole_co) <- newWantedEq_SI (ch_blocker hole) si loc' + (ctEvRole old_ev) nlhs nrhs + -- The "_SI" variant ensures that we make a new Wanted + -- with the same shadow-info as the existing one (#16735) + ; let co = maybeSym swapped $ + mkSymCo lhs_co + `mkTransCo` hole_co + `mkTransCo` rhs_co + ; setWantedEq dest co + ; traceTcS "rewriteEqEvidence" (vcat [ppr old_ev, ppr nlhs, ppr nrhs, ppr co]) + ; return new_ev } + + _ -> panic "rewriteEqEvidence" #if __GLASGOW_HASKELL__ <= 810 | otherwise diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index ea859bf3a8..e889940893 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -28,6 +28,7 @@ import TcType import TcOrigin import GHC.Rename.Unbound ( unknownNameSuggestions ) import GHC.Core.Type +import GHC.Core.Coercion import GHC.Core.TyCo.Rep import GHC.Core.TyCo.Ppr ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon, pprWithTYPE ) import GHC.Core.Unify ( tcMatchTys ) @@ -61,7 +62,6 @@ import SrcLoc import GHC.Driver.Session import ListSetOps ( equivClasses ) import Maybes -import Pair import qualified GHC.LanguageExtensions as LangExt import FV ( fvVarList, unionFV ) @@ -549,7 +549,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics }) -- See Note [Do not report derived but soluble errors] ; mapBagM_ (reportImplic ctxt2) implics } - -- NB ctxt1: don't suppress inner insolubles if there's only a + -- NB ctxt2: don't suppress inner insolubles if there's only a -- wanted insoluble here; but do suppress inner insolubles -- if there's a *given* insoluble here (= inaccessible code) where @@ -562,29 +562,36 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics }) -- (see TcRnTypes.insolubleCt) is caught here, otherwise -- we might suppress its error message, and proceed on past -- type checking to get a Lint error later - report1 = [ ("Out of scope", is_out_of_scope, True, mkHoleReporter tidy_cts) - , ("Holes", is_hole, False, mkHoleReporter tidy_cts) - , ("custom_error", is_user_type_error, True, mkUserTypeErrorReporter) + report1 = [ ("Out of scope", unblocked is_out_of_scope, True, mkHoleReporter tidy_cts) + , ("Holes", unblocked is_hole, False, mkHoleReporter tidy_cts) + , ("custom_error", unblocked is_user_type_error, True, mkUserTypeErrorReporter) , given_eq_spec - , ("insoluble2", utterly_wrong, True, mkGroupReporter mkEqErr) - , ("skolem eq1", very_wrong, True, mkSkolReporter) - , ("skolem eq2", skolem_eq, True, mkSkolReporter) - , ("non-tv eq", non_tv_eq, True, mkSkolReporter) + , ("insoluble2", unblocked utterly_wrong, True, mkGroupReporter mkEqErr) + , ("skolem eq1", unblocked very_wrong, True, mkSkolReporter) + , ("skolem eq2", unblocked skolem_eq, True, mkSkolReporter) + , ("non-tv eq", unblocked non_tv_eq, True, mkSkolReporter) -- The only remaining equalities are alpha ~ ty, -- where alpha is untouchable; and representational equalities -- Prefer homogeneous equalities over hetero, because the -- former might be holding up the latter. -- See Note [Equalities with incompatible kinds] in TcCanonical - , ("Homo eqs", is_homo_equality, True, mkGroupReporter mkEqErr) - , ("Other eqs", is_equality, False, mkGroupReporter mkEqErr) ] + , ("Homo eqs", unblocked is_homo_equality, True, mkGroupReporter mkEqErr) + , ("Other eqs", unblocked is_equality, True, mkGroupReporter mkEqErr) + , ("Blocked eqs", is_equality, False, mkSuppressReporter mkBlockedEqErr)] -- report2: we suppress these if there are insolubles elsewhere in the tree report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr) , ("Irreds", is_irred, False, mkGroupReporter mkIrredErr) , ("Dicts", is_dict, False, mkGroupReporter mkDictErr) ] + -- also checks to make sure the constraint isn't BlockedCIS + -- See TcCanonical Note [Equalities with incompatible kinds], (4) + unblocked :: (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool + unblocked _ (CIrredCan { cc_status = BlockedCIS }) _ = False + unblocked checker ct pred = checker ct pred + -- rigid_nom_eq, rigid_nom_tv_eq, is_hole, is_dict, is_equality, is_ip, is_irred :: Ct -> Pred -> Bool @@ -796,6 +803,11 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) mkGroupReporter mk_err ctxt cts = mapM_ (reportGroup mk_err ctxt . toList) (equivClasses cmp_loc cts) +-- Like mkGroupReporter, but doesn't actually print error messages +mkSuppressReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter +mkSuppressReporter mk_err ctxt cts + = mapM_ (suppressGroup mk_err ctxt . toList) (equivClasses cmp_loc cts) + eq_lhs_type :: Ct -> Ct -> Bool eq_lhs_type ct1 ct2 = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of @@ -806,8 +818,7 @@ eq_lhs_type ct1 ct2 cmp_loc :: Ct -> Ct -> Ordering cmp_loc ct1 ct2 = ctLocSpan (ctLoc ct1) `compare` ctLocSpan (ctLoc ct2) -reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt - -> [Ct] -> TcM () +reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter reportGroup mk_err ctxt cts = ASSERT( not (null cts)) do { err <- mk_err ctxt cts @@ -824,6 +835,14 @@ reportGroup mk_err ctxt cts = -- but that's hard to know for sure, and if we don't -- abort, we need bindings for all (e.g. #12156) +-- like reportGroup, but does not actually report messages. It still adds +-- -fdefer-type-errors bindings, though. +suppressGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> Reporter +suppressGroup mk_err ctxt cts + = do { err <- mk_err ctxt cts + ; traceTc "Suppressing errors for" (ppr cts) + ; mapM_ (addDeferredBinding ctxt err) cts } + maybeReportHoleError :: ReportErrCtxt -> Ct -> ErrMsg -> TcM () -- Unlike maybeReportError, these "hole" errors are -- /not/ suppressed by cec_suppress. We want to see them! @@ -1439,10 +1458,10 @@ mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report -> Maybe SwapFlag -- Nothing <=> not sure -> TcType -> TcType -> TcM ErrMsg mkEqErr_help dflags ctxt report ct oriented ty1 ty2 - | Just (tv1, co1) <- tcGetCastedTyVar_maybe ty1 - = mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2 - | Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2 - = mkTyVarEqErr dflags ctxt report ct swapped tv2 co2 ty1 + | Just (tv1, _) <- tcGetCastedTyVar_maybe ty1 + = mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 + | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2 + = mkTyVarEqErr dflags ctxt report ct swapped tv2 ty1 | otherwise = reportEqErr ctxt report ct oriented ty1 ty2 where @@ -1459,13 +1478,13 @@ reportEqErr ctxt report ct oriented ty1 ty2 mkTyVarEqErr, mkTyVarEqErr' :: DynFlags -> ReportErrCtxt -> Report -> Ct - -> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg + -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg -- tv1 and ty2 are already tidied -mkTyVarEqErr dflags ctxt report ct oriented tv1 co1 ty2 - = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr co1 $$ ppr ty2) - ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 } +mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 + = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2) + ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 } -mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 +mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 | not insoluble_occurs_check -- See Note [Occurs check wins] , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would -- be oriented the other way round; @@ -1514,23 +1533,6 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 -- to be helpful since this is just an unimplemented feature. ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } } - -- check for heterogeneous equality next; see Note [Equalities with incompatible kinds] - -- in TcCanonical - | not (k1 `tcEqType` k2) - = do { let main_msg = addArising (ctOrigin ct) $ - vcat [ hang (text "Kind mismatch: cannot unify" <+> - parens (ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)) <+> - text "with:") - 2 (sep [ppr ty2, dcolon, ppr k2]) - , text "Their kinds differ." ] - cast_msg - | isTcReflexiveCo co1 = empty - | otherwise = text "NB:" <+> ppr tv1 <+> - text "was casted to have kind" <+> - quotes (ppr k1) - - ; mkErrorMsgFromCt ctxt ct (mconcat [important main_msg, important cast_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 @@ -1596,9 +1598,6 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2 -- Consider an ambiguous top-level constraint (a ~ F a) -- Not an occurs check, because F is a type function. where - Pair _ k1 = tcCoercionKind co1 - k2 = tcTypeKind ty2 - ty1 = mkTyVarTy tv1 occ_check_expand = occCheckForErrors dflags tv1 ty2 insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2 @@ -1681,6 +1680,24 @@ pp_givens givens 2 (sep [ text "bound by" <+> ppr skol_info , text "at" <+> ppr (tcl_loc (ic_env implic)) ]) +-- These are for the "blocked" equalities, as described in TcCanonical +-- Note [Equalities with incompatible kinds], wrinkle (2). There should +-- always be another unsolved wanted around, which will ordinarily suppress +-- this message. But this can still be printed out with -fdefer-type-errors +-- (sigh), so we must produce a message. +mkBlockedEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg +mkBlockedEqErr ctxt (ct:_) = mkErrorMsgFromCt ctxt ct report + where + report = important msg + msg = vcat [ hang (text "Cannot use equality for substitution:") + 2 (ppr (ctPred ct)) + , text "Doing so would be ill-kinded." ] + -- This is a terrible message. Perhaps worse, if the user + -- has -fprint-explicit-kinds on, they will see that the two + -- sides have the same kind, as there is an invisible cast. + -- I really don't know how to do better. +mkBlockedEqErr _ [] = panic "mkBlockedEqErr no constraints" + {- Note [Suppress redundant givens during error reporting] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1724,9 +1741,9 @@ extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc extraTyVarEqInfo ctxt tv1 ty2 = extraTyVarInfo ctxt tv1 $$ ty_extra ty2 where - ty_extra ty = case tcGetTyVar_maybe ty of - Just tv -> extraTyVarInfo ctxt tv - Nothing -> empty + ty_extra ty = case tcGetCastedTyVar_maybe ty of + Just (tv, _) -> extraTyVarInfo ctxt tv + Nothing -> empty extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc extraTyVarInfo ctxt tv @@ -2734,10 +2751,7 @@ mkAmbigMsg prepend_msg ct | otherwise -- "The type variable 't0' is ambiguous" = text "The" <+> what <+> text "variable" <> plural tkvs - <+> pprQuotedList tkvs <+> is_or_are tkvs <+> text "ambiguous" - - is_or_are [_] = text "is" - is_or_are _ = text "are" + <+> pprQuotedList tkvs <+> isOrAre tkvs <+> text "ambiguous" pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc pprSkols ctxt tvs diff --git a/compiler/typecheck/TcFlatten.hs b/compiler/typecheck/TcFlatten.hs index f467df06ce..ecad0361d3 100644 --- a/compiler/typecheck/TcFlatten.hs +++ b/compiler/typecheck/TcFlatten.hs @@ -104,9 +104,6 @@ Note [The flattening story] then xis1 /= xis2 i.e. at most one CFunEqCan with a particular LHS -* Function applications can occur in the RHS of a CTyEqCan. No reason - not allow this, and it reduces the amount of flattening that must occur. - * Flattening a type (F xis): - If we are flattening in a Wanted/Derived constraint then create new [W] x : F xis ~ fmv @@ -1801,7 +1798,7 @@ unflattenWanteds tv_eqs funeqs -- bump the unification count; it is "improvement" -- Note [Unflattening can force the solver to iterate] = ASSERT2( tyVarKind tv `eqType` tcTypeKind rhs, ppr ct ) - -- CTyEqCan invariant should ensure this is true + -- CTyEqCan invariant (TyEq:K) should ensure this is true do { is_filled <- isFilledMetaTyVar tv ; elim <- case is_filled of False -> do { traceTcS "unflatten_eq 2" (ppr ct) diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 8d47f4b329..9c578949f8 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -195,18 +195,30 @@ tcHsSigWcType :: UserTypeCtxt -> LHsSigWcType GhcRn -> TcM Type tcHsSigWcType ctxt sig_ty = tcHsSigType ctxt (dropWildCards sig_ty) kcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM () -kcClassSigType skol_info names sig_ty - = discardResult $ - tcClassSigType skol_info names sig_ty - -- tcClassSigType does a fair amount of extra work that we don't need, - -- such as ordering quantified variables. But we absolutely do need - -- to push the level when checking method types and solve local equalities, - -- and so it seems easier just to call tcClassSigType than selectively - -- extract the lines of code from tc_hs_sig_type that we really need. - -- If we don't push the level, we get #16517, where GHC accepts - -- class C a where - -- meth :: forall k. Proxy (a :: k) -> () - -- Note that k is local to meth -- this is hogwash. +-- This is a special form of tcClassSigType that is used during the +-- kind-checking phase to infer the kind of class variables. Cf. tc_hs_sig_type. +-- Importantly, this does *not* kind-generalize. Consider +-- class SC f where +-- meth :: forall a (x :: f a). Proxy x -> () +-- When instantiating Proxy with kappa, we must unify kappa := f a. But we're +-- still working out the kind of f, and thus f a will have a coercion in it. +-- Coercions block unification (Note [Equalities with incompatible kinds] in +-- TcCanonical) and so we fail to unify. If we try to kind-generalize, we'll +-- end up promoting kappa to the top level (because kind-generalization is +-- normally done right before adding a binding to the context), and then we +-- can't set kappa := f a, because a is local. +kcClassSigType skol_info names (HsIB { hsib_ext = sig_vars + , hsib_body = hs_ty }) + = addSigCtxt (funsSigCtxt names) hs_ty $ + do { (tc_lvl, (wanted, (spec_tkvs, _))) + <- pushTcLevelM $ + solveLocalEqualitiesX "kcClassSigType" $ + bindImplicitTKBndrs_Skol sig_vars $ + tc_lhs_type typeLevelMode hs_ty liftedTypeKind + + ; emitResidualTvConstraint skol_info Nothing spec_tkvs + tc_lvl wanted } +kcClassSigType _ _ (XHsImplicitBndrs nec) = noExtCon nec tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type -- Does not do validity checking diff --git a/compiler/typecheck/TcInteract.hs b/compiler/typecheck/TcInteract.hs index ab98e650ed..4401bb7142 100644 --- a/compiler/typecheck/TcInteract.hs +++ b/compiler/typecheck/TcInteract.hs @@ -18,8 +18,9 @@ import TcFlatten import TcUnify( canSolveByUnification ) import VarSet import GHC.Core.Type as Type -import GHC.Core.InstEnv ( DFunInstType ) -import GHC.Core.Coercion.Axiom ( sfInteractTop, sfInteractInert ) +import GHC.Core.Coercion ( BlockSubstFlag(..) ) +import GHC.Core.InstEnv ( DFunInstType ) +import GHC.Core.Coercion.Axiom ( sfInteractTop, sfInteractInert ) import Var import TcType @@ -687,8 +688,9 @@ 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_insol = insoluble }) - | insoluble -- For insolubles, don't allow the constraint to be dropped +interactIrred inerts workItem@(CIrredCan { cc_ev = ev_w, cc_status = status }) + | InsolubleCIS <- status + -- 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 -- See Note [Do not add duplicate derived insolubles] @@ -1639,9 +1641,9 @@ solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS () -- workItem = the new Given constraint -- -- NB: No need for an occurs check here, because solveByUnification always --- arises from a CTyEqCan, a *canonical* constraint. Its invariants --- say that in (a ~ xi), the type variable a does not appear in xi. --- See TcRnTypes.Ct invariants. +-- arises from a CTyEqCan, a *canonical* constraint. Its invariant (TyEq:OC) +-- says that in (a ~ xi), the type variable a does not appear in xi. +-- See Constraint.Ct invariants. -- -- Post: tv is unified (by side effect) with xi; -- we often write tv := xi @@ -2102,7 +2104,8 @@ shortCutReduction old_ev fsk ax_co fam_tc tc_args `mkTcTransCo` ctEvCoercion old_ev) ) Wanted {} -> - do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal + -- See TcCanonical Note [Equalities with incompatible kinds] about NoBlockSubst + do { (new_ev, new_co) <- newWantedEq_SI NoBlockSubst WDeriv deeper_loc Nominal (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk) ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co ; return new_ev } diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 702641a227..945f42c81d 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -184,7 +184,7 @@ newWanted :: CtOrigin -> Maybe TypeOrKind -> PredType -> TcM CtEvidence -- Deals with both equality and non-equality predicates newWanted orig t_or_k pty = do loc <- getCtLocM orig t_or_k - d <- if isEqPrimPred pty then HoleDest <$> newCoercionHole pty + d <- if isEqPrimPred pty then HoleDest <$> newCoercionHole YesBlockSubst pty else EvVarDest <$> newEvVar pty return $ CtWanted { ctev_dest = d , ctev_pred = pty @@ -211,8 +211,8 @@ newHoleCt hole ev ty = do cloneWanted :: Ct -> TcM Ct cloneWanted ct - | ev@(CtWanted { ctev_dest = HoleDest {}, ctev_pred = pty }) <- ctEvidence ct - = do { co_hole <- newCoercionHole pty + | ev@(CtWanted { ctev_dest = HoleDest old_hole, ctev_pred = pty }) <- ctEvidence ct + = do { co_hole <- newCoercionHole (ch_blocker old_hole) pty ; return (mkNonCanonical (ev { ctev_dest = HoleDest co_hole })) } | otherwise = return ct @@ -262,7 +262,7 @@ emitDerivedEqs origin pairs -- | Emits a new equality constraint emitWantedEq :: CtOrigin -> TypeOrKind -> Role -> TcType -> TcType -> TcM Coercion emitWantedEq origin t_or_k role ty1 ty2 - = do { hole <- newCoercionHole pty + = do { hole <- newCoercionHole YesBlockSubst pty ; loc <- getCtLocM origin (Just t_or_k) ; emitSimple $ mkNonCanonical $ CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole @@ -323,12 +323,16 @@ newImplication ************************************************************************ -} -newCoercionHole :: TcPredType -> TcM CoercionHole -newCoercionHole pred_ty +newCoercionHole :: BlockSubstFlag -- should the presence of this hole block substitution? + -- See sub-wrinkle in TcCanonical + -- Note [Equalities with incompatible kinds] + -> TcPredType -> TcM CoercionHole +newCoercionHole blocker pred_ty = do { co_var <- newEvVar pred_ty - ; traceTc "New coercion hole:" (ppr co_var) + ; traceTc "New coercion hole:" (ppr co_var <+> ppr blocker) ; ref <- newMutVar Nothing - ; return $ CoercionHole { ch_co_var = co_var, ch_ref = ref } } + ; return $ CoercionHole { ch_co_var = co_var, ch_blocker = blocker + , ch_ref = ref } } -- | Put a value in a coercion hole fillCoercionHole :: CoercionHole -> Coercion -> TcM () @@ -2020,9 +2024,8 @@ zonkSimples cts = do { cts' <- mapBagM zonkCt cts ~~~~~~~~~~~~~~~~~~~~~~~~~~ zonkCt tries to maintain the canonical form of a Ct. For example, - a CDictCan should stay a CDictCan; - - a CTyEqCan should stay a CTyEqCan (if the LHS stays as a variable.). - a CHoleCan should stay a CHoleCan - - a CIrredCan should stay a CIrredCan with its cc_insol flag intact + - a CIrredCan should stay a CIrredCan with its cc_status flag intact Why?, for example: - For CDictCan, the @TcSimplify.expandSuperClasses@ step, which runs after the @@ -2035,6 +2038,11 @@ Why?, for example: - For CIrredCan we want to see if a constraint is insoluble with insolubleWC +On the other hand, we change CTyEqCan to CNonCanonical, because of all of +CTyEqCan's invariants, which can break during zonking. Besides, the constraint +will be canonicalised again, so there is little benefit in keeping the +CTyEqCan structure. + NB: we do not expect to see any CFunEqCans, because zonkCt is only called on unflattened constraints. @@ -2045,6 +2053,7 @@ creates e.g. a CDictCan where the cc_tyars are /not/ function free. -} zonkCt :: Ct -> TcM Ct +-- See Note [zonkCt behaviour] zonkCt ct@(CHoleCan { cc_ev = ev }) = do { ev' <- zonkCtEvidence ev ; return $ ct { cc_ev = ev' } } @@ -2056,12 +2065,8 @@ zonkCt ct@(CDictCan { cc_ev = ev, cc_tyargs = args }) zonkCt (CTyEqCan { cc_ev = ev }) = mkNonCanonical <$> zonkCtEvidence ev - -- CTyEqCan has some delicate invariants that may be violated by - -- zonking (documented with the Ct type) , so we don't want to create - -- a CTyEqCan here. Besides, this will be canonicalized again anyway, - -- so there is very little benefit in keeping the CTyEqCan constructor. -zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_insol flag +zonkCt ct@(CIrredCan { cc_ev = ev }) -- Preserve the cc_status flag = do { ev' <- zonkCtEvidence ev ; return (ct { cc_ev = ev' }) } @@ -2264,12 +2269,8 @@ zonkTidyOrigin env orig = return (env, orig) ---------------- tidyCt :: TidyEnv -> Ct -> Ct -- Used only in error reporting --- Also converts it to non-canonical tidyCt env ct - = case ct of - CHoleCan { cc_ev = ev } - -> ct { cc_ev = tidy_ev env ev } - _ -> mkNonCanonical (tidy_ev env (ctEvidence ct)) + = ct { cc_ev = tidy_ev env (ctEvidence ct) } where tidy_ev :: TidyEnv -> CtEvidence -> CtEvidence -- NB: we do not tidy the ctev_evar field because we don't diff --git a/compiler/typecheck/TcOrigin.hs b/compiler/typecheck/TcOrigin.hs index 37b4d9a8d9..9dc137f7d9 100644 --- a/compiler/typecheck/TcOrigin.hs +++ b/compiler/typecheck/TcOrigin.hs @@ -363,7 +363,7 @@ data CtOrigin -- visible.) Only used for prioritizing error messages. } - | KindEqOrigin -- See Note [Equalities with incompatible kinds] in TcCanonical. + | KindEqOrigin TcType (Maybe TcType) -- A kind equality arising from unifying these two types CtOrigin -- originally arising from this (Maybe TypeOrKind) -- the level of the eq this arises from diff --git a/compiler/typecheck/TcPluginM.hs b/compiler/typecheck/TcPluginM.hs index 36d35e049a..c85f72c157 100644 --- a/compiler/typecheck/TcPluginM.hs +++ b/compiler/typecheck/TcPluginM.hs @@ -79,6 +79,7 @@ import GHC.Core.Class import GHC.Driver.Types import Outputable import GHC.Core.Type +import GHC.Core.Coercion ( BlockSubstFlag(..) ) import Id import GHC.Core.InstEnv import FastString @@ -179,7 +180,7 @@ newEvVar = unsafeTcPluginTcM . TcM.newEvVar -- | Create a fresh coercion hole. newCoercionHole :: PredType -> TcPluginM CoercionHole -newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole +newCoercionHole = unsafeTcPluginTcM . TcM.newCoercionHole YesBlockSubst -- | Bind an evidence variable. This must not be invoked from -- 'tcPluginInit' or 'tcPluginStop', or it will panic. diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs index 3fd956f87a..fe74720796 100644 --- a/compiler/typecheck/TcSMonad.hs +++ b/compiler/typecheck/TcSMonad.hs @@ -300,8 +300,8 @@ workListWantedCount (WL { wl_eqs = eqs, wl_rest = rest }) = count isWantedCt eqs + count is_wanted rest where is_wanted ct - | CIrredCan { cc_ev = ev, cc_insol = insol } <- ct - = not insol && isWanted ev + | CIrredCan { cc_status = InsolubleCIS } <- ct + = False | otherwise = isWantedCt ct @@ -767,6 +767,7 @@ The InertCans represents a collection of constraints with the following properti eg a wanted cannot rewrite a given) * CTyEqCan equalities: see Note [inert_eqs: the inert equalities] + Also see documentation in Constraint.Ct for a list of invariants Note [EqualCtList invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -919,8 +920,8 @@ The idea is that with S(fw,_). * T3 is guaranteed by a simple occurs-check on the work item. - This is done during canonicalisation, in canEqTyVar; - (invariant: a CTyEqCan never has an occurs check). + This is done during canonicalisation, in canEqTyVar; invariant + (TyEq:OC) of CTyEqCan. * (K1-3) are the "kick-out" criteria. (As stated, they are really the "keep" criteria.) If the current inert S contains a triple that does @@ -1639,11 +1640,13 @@ add_item ics item@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) , inert_count = bumpUnsolvedCount ev (inert_count ics) } add_item ics@(IC { inert_irreds = irreds, inert_count = count }) - item@(CIrredCan { cc_ev = ev, cc_insol = insoluble }) + item@(CIrredCan { cc_ev = ev, cc_status = status }) = ics { inert_irreds = irreds `Bag.snocBag` item - , inert_count = if insoluble - then count -- inert_count does not include insolubles - else bumpUnsolvedCount ev count } + , inert_count = case status of + InsolubleCIS -> count + _ -> bumpUnsolvedCount ev count } + -- inert_count does not include insolubles + add_item ics item@(CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys }) = ics { inert_dicts = addDict (inert_dicts ics) cls tys item @@ -1821,6 +1824,42 @@ kickOutAfterUnification new_tv ; setInertCans ics2 ; return n_kicked } +-- See Wrinkle (2b) in Note [Equalities with incompatible kinds] in TcCanonical +kickOutAfterFillingCoercionHole :: CoercionHole -> TcS () +kickOutAfterFillingCoercionHole hole + = do { ics <- getInertCans + ; let (kicked_out, ics') = kick_out ics + n_kicked = workListSize kicked_out + + ; unless (n_kicked == 0) $ + do { updWorkListTcS (appendWorkList kicked_out) + ; csTraceTcS $ + hang (text "Kick out, hole =" <+> ppr hole) + 2 (vcat [ text "n-kicked =" <+> int n_kicked + , text "kicked_out =" <+> ppr kicked_out + , text "Residual inerts =" <+> ppr ics' ]) } + + ; setInertCans ics' } + where + kick_out :: InertCans -> (WorkList, InertCans) + kick_out ics@(IC { inert_irreds = irreds }) + = let (to_kick, to_keep) = partitionBag kick_ct irreds + + kicked_out = extendWorkListCts (bagToList to_kick) emptyWorkList + ics' = ics { inert_irreds = to_keep } + in + (kicked_out, ics') + + kick_ct :: Ct -> Bool + -- This is not particularly efficient. Ways to do better: + -- 1) Have a custom function that looks for a coercion hole and returns a Bool + -- 2) Keep co-hole-blocked constraints in a separate part of the inert set, + -- keyed by their co-hole. (Is it possible for more than one co-hole to be + -- in a constraint? I doubt it.) + kick_ct (CIrredCan { cc_ev = ev, cc_status = BlockedCIS }) + = coHoleCoVar hole `elemVarSet` tyCoVarsOfType (ctEvPred ev) + kick_ct _other = False + {- Note [kickOutRewritable] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ See also Note [inert_eqs: the inert equalities]. @@ -3200,7 +3239,10 @@ newFlattenSkolem flav loc tc xis | otherwise -- Generate a [WD] for both Wanted and Derived -- See Note [No Derived CFunEqCans] = do { fmv <- wrapTcS (TcM.newFmvTyVar fam_ty) - ; (ev, hole_co) <- newWantedEq loc Nominal fam_ty (mkTyVarTy fmv) + -- See (2a) in TcCanonical + -- Note [Equalities with incompatible kinds] + ; (ev, hole_co) <- newWantedEq_SI NoBlockSubst WDeriv loc Nominal + fam_ty (mkTyVarTy fmv) ; return (ev, hole_co, fmv) } ---------------------------- @@ -3386,7 +3428,7 @@ useVars co_vars setWantedEq :: TcEvDest -> Coercion -> TcS () setWantedEq (HoleDest hole) co = do { useVars (coVarsOfCo co) - ; wrapTcS $ TcM.fillCoercionHole hole co } + ; fillCoercionHole hole co } setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq" (ppr ev) -- | Good for both equalities and non-equalities @@ -3394,12 +3436,12 @@ setWantedEvTerm :: TcEvDest -> EvTerm -> TcS () setWantedEvTerm (HoleDest hole) tm | Just co <- evTermCoercion_maybe tm = do { useVars (coVarsOfCo co) - ; wrapTcS $ TcM.fillCoercionHole hole co } + ; fillCoercionHole hole co } | otherwise = -- See Note [Yukky eq_sel for a HoleDest] do { let co_var = coHoleCoVar hole ; setEvBind (mkWantedEvBind co_var tm) - ; wrapTcS $ TcM.fillCoercionHole hole (mkTcCoVarCo co_var) } + ; fillCoercionHole hole (mkTcCoVarCo co_var) } setWantedEvTerm (EvVarDest ev_id) tm = setEvBind (mkWantedEvBind ev_id tm) @@ -3423,6 +3465,11 @@ We even re-use the CoHole's Id for this binding! Yuk! -} +fillCoercionHole :: CoercionHole -> Coercion -> TcS () +fillCoercionHole hole co + = do { wrapTcS $ TcM.fillCoercionHole hole co + ; kickOutAfterFillingCoercionHole hole } + setEvBindIfWanted :: CtEvidence -> EvTerm -> TcS () setEvBindIfWanted ev tm = case ev of @@ -3468,13 +3515,13 @@ emitNewWantedEq loc role ty1 ty2 -- | Make a new equality CtEvidence newWantedEq :: CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) -newWantedEq = newWantedEq_SI WDeriv +newWantedEq = newWantedEq_SI YesBlockSubst WDeriv -newWantedEq_SI :: ShadowInfo -> CtLoc -> Role +newWantedEq_SI :: BlockSubstFlag -> ShadowInfo -> CtLoc -> Role -> TcType -> TcType -> TcS (CtEvidence, Coercion) -newWantedEq_SI si loc role ty1 ty2 - = do { hole <- wrapTcS $ TcM.newCoercionHole pty +newWantedEq_SI blocker si loc role ty1 ty2 + = do { hole <- wrapTcS $ TcM.newCoercionHole blocker pty ; traceTcS "Emitting new coercion hole" (ppr hole <+> dcolon <+> ppr pty) ; return ( CtWanted { ctev_pred = pty, ctev_dest = HoleDest hole , ctev_nosh = si @@ -3520,7 +3567,7 @@ newWanted = newWanted_SI WDeriv newWanted_SI :: ShadowInfo -> CtLoc -> PredType -> TcS MaybeNew newWanted_SI si loc pty | Just (role, ty1, ty2) <- getEqPredTys_maybe pty - = Fresh . fst <$> newWantedEq_SI si loc role ty1 ty2 + = Fresh . fst <$> newWantedEq_SI YesBlockSubst si loc role ty1 ty2 | otherwise = newWantedEvVar_SI si loc pty diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index ea95a0b4ad..868be78c68 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -2432,7 +2432,6 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs is_float_eq_candidate ct | pred <- ctPred ct , EqPred NomEq ty1 ty2 <- classifyPredType pred - , tcTypeKind ty1 `tcEqType` tcTypeKind ty2 = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of (Just tv1, _) -> float_tv_eq_candidate tv1 ty2 (_, Just tv2) -> float_tv_eq_candidate tv2 ty1 @@ -2479,19 +2478,6 @@ happen. In particular, float out equalities that are: case, floating out won't help either, and it may affect grouping of error messages. -* Homogeneous (both sides have the same kind). Why only homogeneous? - Because heterogeneous equalities have derived kind equalities. - See Note [Equalities with incompatible kinds] in TcCanonical. - If we float out a hetero equality, then it will spit out the same - derived kind equality again, which might create duplicate error - messages. - - Instead, we do float out the kind equality (if it's worth floating - out, as above). If/when we solve it, we'll be able to rewrite the - original hetero equality to be homogeneous, and then perhaps make - progress / float it out. The duplicate error message was spotted in - typecheck/should_fail/T7368. - * Nominal. No point in floating (alpha ~R# ty), because we do not unify representational equalities even if alpha is touchable. See Note [Do not unify representational equalities] in TcInteract. diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index cb3865122b..6914851144 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -1693,7 +1693,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 where go dflags cur_lvl | canSolveByUnification cur_lvl tv1 ty2 - , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2 + , MTVU_OK ty2' <- metaTyVarUpdateOK dflags tv1 ty2 = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1) ; traceTc "uUnfilledVar2 ok" $ vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1) @@ -1762,7 +1762,7 @@ lhsPriority tv {- Note [TyVar/TyVar orientation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Given (a ~ b), should we orient the CTyEqCan as (a~b) or (b~a)? -This is a surprisingly tricky question! +This is a surprisingly tricky question! This is invariant (TyEq:TV). The question is answered by swapOverTyVars, which is use - in the eager unifier, in TcUnify.uUnfilledVar1 @@ -2178,7 +2178,9 @@ with (forall k. k->*) data MetaTyVarUpdateResult a = MTVU_OK a - | MTVU_Bad -- Forall, predicate, or type family + | MTVU_Bad -- Forall, predicate, or type family + | MTVU_HoleBlocker -- Blocking coercion hole + -- See Note [Equalities with incompatible kinds] in TcCanonical | MTVU_Occurs deriving (Functor) @@ -2187,9 +2189,16 @@ instance Applicative MetaTyVarUpdateResult where (<*>) = ap instance Monad MetaTyVarUpdateResult where - MTVU_OK x >>= k = k x - MTVU_Bad >>= _ = MTVU_Bad - MTVU_Occurs >>= _ = MTVU_Occurs + MTVU_OK x >>= k = k x + MTVU_Bad >>= _ = MTVU_Bad + MTVU_HoleBlocker >>= _ = MTVU_HoleBlocker + MTVU_Occurs >>= _ = MTVU_Occurs + +instance Outputable a => Outputable (MetaTyVarUpdateResult a) where + ppr (MTVU_OK a) = text "MTVU_OK" <+> ppr a + ppr MTVU_Bad = text "MTVU_Bad" + ppr MTVU_HoleBlocker = text "MTVU_HoleBlocker" + ppr MTVU_Occurs = text "MTVU_Occurs" occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult () -- Just for error-message generation; so we return MetaTyVarUpdateResult @@ -2199,22 +2208,25 @@ occCheckForErrors :: DynFlags -> TcTyVar -> Type -> MetaTyVarUpdateResult () -- b) there is a forall in the type (unless we have -XImpredicativeTypes) occCheckForErrors dflags tv ty = case preCheck dflags True tv ty of - MTVU_OK _ -> MTVU_OK () - MTVU_Bad -> MTVU_Bad - MTVU_Occurs -> case occCheckExpand [tv] ty of - Nothing -> MTVU_Occurs - Just _ -> MTVU_OK () + MTVU_OK _ -> MTVU_OK () + MTVU_Bad -> MTVU_Bad + MTVU_HoleBlocker -> MTVU_HoleBlocker + MTVU_Occurs -> case occCheckExpand [tv] ty of + Nothing -> MTVU_Occurs + Just _ -> MTVU_OK () ---------------- metaTyVarUpdateOK :: DynFlags -> TcTyVar -- tv :: k1 -> TcType -- ty :: k2 - -> Maybe TcType -- possibly-expanded ty + -> MetaTyVarUpdateResult TcType -- possibly-expanded ty -- (metaTyVarUpdateOK tv ty) -- We are about to update the meta-tyvar tv with ty -- Check (a) that tv doesn't occur in ty (occurs check) -- (b) that ty does not have any foralls -- (in the impredicative case), or type functions +-- (c) that ty does not have any blocking coercion holes +-- See Note [Equalities with incompatible kinds] in TcCanonical -- -- We have two possible outcomes: -- (1) Return the type to update the type variable with, @@ -2237,20 +2249,24 @@ metaTyVarUpdateOK dflags tv ty = case preCheck dflags False tv ty of -- False <=> type families not ok -- See Note [Prevent unification with type families] - MTVU_OK _ -> Just ty - MTVU_Bad -> Nothing -- forall, predicate, or type function - MTVU_Occurs -> occCheckExpand [tv] ty + MTVU_OK _ -> MTVU_OK ty + MTVU_Bad -> MTVU_Bad -- forall, predicate, type function + MTVU_HoleBlocker -> MTVU_HoleBlocker -- coercion hole + MTVU_Occurs -> case occCheckExpand [tv] ty of + Just expanded_ty -> MTVU_OK expanded_ty + Nothing -> MTVU_Occurs preCheck :: DynFlags -> Bool -> TcTyVar -> TcType -> MetaTyVarUpdateResult () -- A quick check for -- (a) a forall type (unless -XImpredicativeTypes) -- (b) a predicate type (unless -XImpredicativeTypes) -- (c) a type family --- (d) an occurrence of the type variable (occurs check) +-- (d) a blocking coercion hole +-- (e) an occurrence of the type variable (occurs check) -- -- For (a), (b), and (c) we check only the top level of the type, NOT --- inside the kinds of variables it mentions. But for (c) we do --- look in the kinds of course. +-- inside the kinds of variables it mentions. For (d) we look deeply +-- in coercions, and for (e) we do look in the kinds of course. preCheck dflags ty_fam_ok tv ty = fast_check ty @@ -2292,10 +2308,13 @@ preCheck dflags ty_fam_ok tv ty fast_check_occ k | tv `elemVarSet` tyCoVarsOfType k = MTVU_Occurs | otherwise = ok - -- For coercions, we are only doing an occurs check here; -- no bother about impredicativity in coercions, as they're -- inferred - fast_check_co co | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs + fast_check_co co | not (gopt Opt_DeferTypeErrors dflags) + , badCoercionHoleCo co = MTVU_HoleBlocker + -- Wrinkle (4b) in TcCanonical Note [Equalities with incompatible kinds] + + | tv `elemVarSet` tyCoVarsOfCo co = MTVU_Occurs | otherwise = ok bad_tc :: TyCon -> Bool diff --git a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr index da79678d5b..57b2ee7876 100644 --- a/testsuite/tests/dependent/should_fail/BadTelescope5.stderr +++ b/testsuite/tests/dependent/should_fail/BadTelescope5.stderr @@ -1,6 +1,6 @@ BadTelescope5.hs:10:81: error: - • Expected kind ‘k’, but ‘d’ has kind ‘Proxy a’ + • Expected kind ‘k1’, but ‘d’ has kind ‘Proxy a1’ • In the second argument of ‘SameKind’, namely ‘d’ In the type signature: bar :: forall a k (b :: k) (c :: Proxy b) (d :: Proxy a). diff --git a/testsuite/tests/dependent/should_fail/T14066.stderr b/testsuite/tests/dependent/should_fail/T14066.stderr index e5179e510b..a6780ff75f 100644 --- a/testsuite/tests/dependent/should_fail/T14066.stderr +++ b/testsuite/tests/dependent/should_fail/T14066.stderr @@ -1,6 +1,6 @@ T14066.hs:15:59: error: - • Expected kind ‘k’, but ‘b’ has kind ‘k1’ + • Expected kind ‘k2’, but ‘b’ has kind ‘k3’ • In the second argument of ‘SameKind’, namely ‘b’ In the type signature: g :: forall k (b :: k). SameKind a b In the expression: diff --git a/testsuite/tests/dependent/should_fail/T14066e.stderr b/testsuite/tests/dependent/should_fail/T14066e.stderr index 03a2b9255d..ee903d6b4c 100644 --- a/testsuite/tests/dependent/should_fail/T14066e.stderr +++ b/testsuite/tests/dependent/should_fail/T14066e.stderr @@ -1,20 +1,10 @@ -T14066e.hs:13:59: error: - • Couldn't match kind ‘k’ with ‘*’ - ‘k’ is a rigid type variable bound by - the type signature for: - j :: forall {k} {k1} (c :: k) (b :: k1). - Proxy a -> Proxy b -> Proxy c -> Proxy b - at T14066e.hs:12:5-61 - When matching kinds - k1 :: * - c :: k - Expected kind ‘c’, but ‘b'’ has kind ‘k1’ - • In the first argument of ‘Proxy’, namely ‘(b' :: c')’ +T14066e.hs:13:65: error: + • Expected a type, but ‘c'’ has kind ‘k1’ + • In the kind ‘c'’ + In the first argument of ‘Proxy’, namely ‘(b' :: c')’ In an expression type signature: Proxy (b' :: c') - In the expression: p1 :: Proxy (b' :: c') • Relevant bindings include p2 :: Proxy c (bound at T14066e.hs:13:27) - p1 :: Proxy b (bound at T14066e.hs:13:10) j :: Proxy a -> Proxy b -> Proxy c -> Proxy b (bound at T14066e.hs:13:5) diff --git a/testsuite/tests/ghci.debugger/scripts/break012.stdout b/testsuite/tests/ghci.debugger/scripts/break012.stdout index 5d478ae04e..2e86b42713 100644 --- a/testsuite/tests/ghci.debugger/scripts/break012.stdout +++ b/testsuite/tests/ghci.debugger/scripts/break012.stdout @@ -1,14 +1,14 @@ Stopped in Main.g, break012.hs:5:10-18 -_result :: (a1, a2 -> a2, (), a -> a -> a) = _ -a :: a1 = _ -b :: a3 -> a3 = _ +_result :: (p, a1 -> a1, (), a -> a -> a) = _ +a :: p = _ +b :: a2 -> a2 = _ c :: () = _ d :: a -> a -> a = _ -a :: a1 -b :: a3 -> a3 +a :: p +b :: a2 -> a2 c :: () d :: a -> a -> a -a = (_t1::a1) -b = (_t2::a3 -> a3) +a = (_t1::p) +b = (_t2::a2 -> a2) c = (_t3::()) d = (_t4::a -> a -> a) diff --git a/testsuite/tests/indexed-types/should_fail/T14887.stderr b/testsuite/tests/indexed-types/should_fail/T14887.stderr index 56875a7628..ff7e14b464 100644 --- a/testsuite/tests/indexed-types/should_fail/T14887.stderr +++ b/testsuite/tests/indexed-types/should_fail/T14887.stderr @@ -7,6 +7,10 @@ T14887.hs:13:1: error: • In the type family declaration for ‘Foo2’ T14887.hs:14:11: error: - • Expected kind ‘a0 :~: a0’, but ‘e :: a :~: a’ has kind ‘a :~: a’ + • Couldn't match kind ‘k1’ with ‘k’ + When matching kinds + a0 :: k + a :: k1 + Expected kind ‘a0 :~: a0’, but ‘e :: a :~: a’ has kind ‘a :~: a’ • In the second argument of ‘Foo2’, namely ‘(e :: a :~: a)’ In the type family declaration for ‘Foo2’ diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr index 4ef5ae66a8..943dbb148b 100644 --- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr +++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr @@ -1,6 +1,6 @@ T3330c.hs:25:43: error: - • Couldn't match kind ‘* -> *’ with ‘*’ + • Couldn't match kind ‘*’ with ‘* -> *’ When matching types f1 :: * -> * f1 x :: * diff --git a/testsuite/tests/partial-sigs/should_fail/T14584.stderr b/testsuite/tests/partial-sigs/should_fail/T14584.stderr index 80c8ce2683..372ca3fba2 100644 --- a/testsuite/tests/partial-sigs/should_fail/T14584.stderr +++ b/testsuite/tests/partial-sigs/should_fail/T14584.stderr @@ -1,58 +1,26 @@ T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Could not deduce: m1 ~ * - from the context: (Action act, Monoid a, Good m1) - bound by the instance declaration at T14584.hs:54:10-89 - ‘m1’ is a rigid type variable bound by - the instance declaration - at T14584.hs:54:10-89 - When matching types - a :: * - a0 :: m - Expected type: Sing a0 - Actual type: Sing a - • In the second argument of ‘fromSing’, namely - ‘(sing @m @a :: Sing _)’ - In the fourth argument of ‘act’, namely - ‘(fromSing @m (sing @m @a :: Sing _))’ - In the expression: - act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) - • Relevant bindings include - monHom :: a -> a (bound at T14584.hs:56:3) - -T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Could not deduce: a ~~ a0 + • Could not deduce (SingI a) arising from a use of ‘sing’ from the context: (Action act, Monoid a, Good m1) bound by the instance declaration at T14584.hs:54:10-89 - ‘a’ is a rigid type variable bound by - the instance declaration - at T14584.hs:54:10-89 - Expected type: Sing a0 - Actual type: Sing a • In the second argument of ‘fromSing’, namely ‘(sing @m @a :: Sing _)’ In the fourth argument of ‘act’, namely ‘(fromSing @m (sing @m @a :: Sing _))’ In the expression: act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) - • Relevant bindings include - monHom :: a -> a (bound at T14584.hs:56:3) -T14584.hs:56:41: warning: [-Wdeferred-type-errors (in -Wdefault)] - • Could not deduce (SingI a) arising from a use of ‘sing’ - from the context: (Action act, Monoid a, Good m1) - bound by the instance declaration at T14584.hs:54:10-89 - • In the second argument of ‘fromSing’, namely +T14584.hs:56:50: warning: [-Wdeferred-type-errors (in -Wdefault)] + • Expected kind ‘m1’, but ‘a’ has kind ‘*’ + • In the type ‘a’ + In the second argument of ‘fromSing’, namely ‘(sing @m @a :: Sing _)’ In the fourth argument of ‘act’, namely ‘(fromSing @m (sing @m @a :: Sing _))’ - In the expression: - act @_ @_ @act (fromSing @m (sing @m @a :: Sing _)) T14584.hs:56:60: warning: [-Wpartial-type-signatures (in -Wdefault)] - • Found type wildcard ‘_’ standing for ‘a0 :: m’ - Where: ‘a0’ is an ambiguous type variable - ‘m’ is a rigid type variable bound by + • Found type wildcard ‘_’ standing for ‘a :: m’ + Where: ‘a’, ‘m’ are rigid type variables bound by the instance declaration at T14584.hs:54:10-89 • In the first argument of ‘Sing’, namely ‘_’ diff --git a/testsuite/tests/patsyn/should_fail/T15685.stderr b/testsuite/tests/patsyn/should_fail/T15685.stderr index 13fc5a81ec..7f01ebc479 100644 --- a/testsuite/tests/patsyn/should_fail/T15685.stderr +++ b/testsuite/tests/patsyn/should_fail/T15685.stderr @@ -1,9 +1,21 @@ T15685.hs:13:24: error: - • Kind mismatch: cannot unify (f :: a -> *) with: + • Couldn't match kind ‘a1’ with ‘[k0]’ + ‘a1’ is untouchable + inside the constraints: as ~ (a2 : as1) + bound by a pattern with constructor: + Here :: forall {a1} (f :: a1 -> *) (a2 :: a1) (as :: [a1]). + f a2 -> NS f (a2 : as), + in a pattern synonym declaration + at T15685.hs:13:19-26 + ‘a1’ is a rigid type variable bound by + the inferred type of HereNil :: NS f as + at T15685.hs:13:9-15 + Possible fix: add a type signature for ‘HereNil’ + When matching types + f :: a1 -> * NP a0 :: [k0] -> * - Their kinds differ. - Expected type: f a1 + Expected type: f a2 Actual type: NP a0 b0 • In the pattern: Nil In the pattern: Here Nil diff --git a/testsuite/tests/polykinds/T11399.stderr b/testsuite/tests/polykinds/T11399.stderr index e5c9e0e37c..9174cd0b7d 100644 --- a/testsuite/tests/polykinds/T11399.stderr +++ b/testsuite/tests/polykinds/T11399.stderr @@ -1,6 +1,6 @@ T11399.hs:10:32: error: - • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’ + • Couldn't match kind ‘GHC.Types.RuntimeRep’ with ‘*’ When matching kinds a :: * -> * TYPE :: GHC.Types.RuntimeRep -> * diff --git a/testsuite/tests/polykinds/T14846.stderr b/testsuite/tests/polykinds/T14846.stderr index 83e32f7a21..edb19408b2 100644 --- a/testsuite/tests/polykinds/T14846.stderr +++ b/testsuite/tests/polykinds/T14846.stderr @@ -3,8 +3,8 @@ T14846.hs:38:8: error: • Couldn't match type ‘ríki’ with ‘Hom riki’ ‘ríki’ is a rigid type variable bound by the type signature for: - i :: forall {k5} {k6} {cls2 :: k6 -> Constraint} (xx :: k5) - (a :: Struct cls2) (ríki :: Struct cls2 -> Struct cls2 -> *). + i :: forall {k5} {k6} {cls3 :: k6 -> Constraint} (xx :: k5) + (a :: Struct cls3) (ríki :: Struct cls3 -> Struct cls3 -> *). StructI xx a => ríki a a at T14846.hs:38:8-48 @@ -23,32 +23,36 @@ T14846.hs:38:8: error: In the instance declaration for ‘Category (Hom riki)’ T14846.hs:39:12: error: - • Couldn't match kind ‘k4’ with ‘Struct cls2’ - ‘k4’ is a rigid type variable bound by - the instance declaration - at T14846.hs:37:10-65 - When matching kinds - cls0 :: Struct cls -> Constraint - cls1 :: k4 -> Constraint + • Could not deduce (StructI xx1 structured0) + arising from a use of ‘struct’ + from the context: Category riki + bound by the instance declaration at T14846.hs:37:10-65 + or from: StructI xx a + bound by the type signature for: + i :: forall {k5} {k6} {cls3 :: k6 -> Constraint} (xx :: k5) + (a :: Struct cls3). + StructI xx a => + Hom riki a a + at T14846.hs:38:8-48 + The type variables ‘xx1’, ‘structured0’ are ambiguous + Relevant bindings include + i :: Hom riki a a (bound at T14846.hs:39:3) + These potential instance exist: + instance forall k (xx :: k) (cls :: k -> Constraint) + (structured :: Struct cls). + (Structured xx cls ~ structured, cls xx) => + StructI xx structured + -- Defined at T14846.hs:28:10 • In the expression: struct :: AStruct (Structured a cls) In the expression: case struct :: AStruct (Structured a cls) of In an equation for ‘i’: i = case struct :: AStruct (Structured a cls) of - • Relevant bindings include - i :: Hom riki a a (bound at T14846.hs:39:3) -T14846.hs:39:31: error: - • Couldn't match kind ‘k4’ with ‘Struct cls2’ - ‘k4’ is a rigid type variable bound by - the instance declaration - at T14846.hs:37:10-65 - When matching kinds - cls1 :: k4 -> Constraint - cls0 :: Struct cls -> Constraint - Expected kind ‘Struct cls0’, - but ‘Structured a cls’ has kind ‘Struct cls1’ - • In the first argument of ‘AStruct’, namely ‘(Structured a cls)’ +T14846.hs:39:44: error: + • Expected kind ‘Struct cls3 -> Constraint’, + but ‘cls’ has kind ‘k4 -> Constraint’ + • In the second argument of ‘Structured’, namely ‘cls’ + In the first argument of ‘AStruct’, namely ‘(Structured a cls)’ In an expression type signature: AStruct (Structured a cls) - In the expression: struct :: AStruct (Structured a cls) • Relevant bindings include i :: Hom riki a a (bound at T14846.hs:39:3) diff --git a/testsuite/tests/polykinds/T17841.stderr b/testsuite/tests/polykinds/T17841.stderr index 975f5a11d0..6157f55399 100644 --- a/testsuite/tests/polykinds/T17841.stderr +++ b/testsuite/tests/polykinds/T17841.stderr @@ -1,13 +1,6 @@ -T17841.hs:7:40: error: - • Couldn't match kind ‘k’ with ‘*’ - ‘k’ is a rigid type variable bound by - the class declaration for ‘Foo’ - at T17841.hs:7:17 - When matching kinds - k0 :: * - t :: k - Expected kind ‘t’, but ‘a’ has kind ‘k0’ - • In the first argument of ‘Proxy’, namely ‘(a :: t)’ +T17841.hs:7:45: error: + • Expected a type, but ‘t’ has kind ‘k2’ + • In the kind ‘t’ + In the first argument of ‘Proxy’, namely ‘(a :: t)’ In the type signature: foo :: Proxy (a :: t) - In the class declaration for ‘Foo’ diff --git a/testsuite/tests/polykinds/T7278.stderr b/testsuite/tests/polykinds/T7278.stderr index 265e27892b..37b00a7a70 100644 --- a/testsuite/tests/polykinds/T7278.stderr +++ b/testsuite/tests/polykinds/T7278.stderr @@ -1,5 +1,5 @@ T7278.hs:9:43: error: - • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k’ + • Expected kind ‘* -> * -> *’, but ‘t’ has kind ‘k1’ • In the type signature: f :: (C (t :: k) (TF t)) => TF t p1 p0 -> t p1 p0 diff --git a/testsuite/tests/polykinds/T8616.stderr b/testsuite/tests/polykinds/T8616.stderr index 4341b3051a..2a8b6482aa 100644 --- a/testsuite/tests/polykinds/T8616.stderr +++ b/testsuite/tests/polykinds/T8616.stderr @@ -1,13 +1,13 @@ T8616.hs:8:16: error: - • Couldn't match kind ‘k’ with ‘*’ - ‘k’ is a rigid type variable bound by + • Couldn't match kind ‘k1’ with ‘*’ + ‘k1’ is a rigid type variable bound by the type signature for: - withSomeSing :: forall k (kproxy :: k). Proxy kproxy + withSomeSing :: forall k1 (kproxy :: k1). Proxy kproxy at T8616.hs:7:1-52 When matching types a0 :: * - Any :: k + Any :: k1 • In the expression: undefined :: (Any :: k) In an equation for ‘withSomeSing’: withSomeSing = undefined :: (Any :: k) @@ -15,7 +15,7 @@ T8616.hs:8:16: error: withSomeSing :: Proxy kproxy (bound at T8616.hs:8:1) T8616.hs:8:30: error: - • Expected a type, but ‘Any :: k’ has kind ‘k’ + • Expected a type, but ‘Any :: k’ has kind ‘k1’ • In an expression type signature: (Any :: k) In the expression: undefined :: (Any :: k) In an equation for ‘withSomeSing’: diff --git a/testsuite/tests/polykinds/T9017.stderr b/testsuite/tests/polykinds/T9017.stderr index b1d336646a..8acf58c9b5 100644 --- a/testsuite/tests/polykinds/T9017.stderr +++ b/testsuite/tests/polykinds/T9017.stderr @@ -1,16 +1,17 @@ T9017.hs:8:7: error: - • Couldn't match kind ‘k1’ with ‘*’ - ‘k1’ is a rigid type variable bound by + • Couldn't match kind ‘k2’ with ‘*’ + ‘k2’ is a rigid type variable bound by the type signature for: - foo :: forall {k} {k1} (a :: k -> k1 -> *) (b :: k) (m :: k -> k1). + foo :: forall {k2} {k3} (a :: k2 -> k3 -> *) (b :: k2) + (m :: k2 -> k3). a b (m b) at T9017.hs:7:1-16 When matching types - a1 :: * -> * -> * - a :: k -> k1 -> * + a0 :: * -> * -> * + a :: k2 -> k3 -> * Expected type: a b (m b) - Actual type: a1 a0 (m0 a0) + Actual type: a0 a1 (m0 a1) • In the expression: arr return In an equation for ‘foo’: foo = arr return • Relevant bindings include diff --git a/testsuite/tests/typecheck/should_fail/T15629.stderr b/testsuite/tests/typecheck/should_fail/T15629.stderr index a0e0f42286..ac307ed9d5 100644 --- a/testsuite/tests/typecheck/should_fail/T15629.stderr +++ b/testsuite/tests/typecheck/should_fail/T15629.stderr @@ -1,7 +1,7 @@ T15629.hs:26:37: error: • Expected kind ‘x1 ~> F x1 ab1’, - but ‘F1Sym :: x ~> F x z’ has kind ‘x1 ~> F x1 z’ + but ‘F1Sym :: x ~> F x z’ has kind ‘x1 ~> F x1 z1’ • In the first argument of ‘Comp’, namely ‘(F1Sym :: x ~> F x z)’ In the first argument of ‘Proxy’, namely ‘((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab)’ @@ -10,18 +10,18 @@ T15629.hs:26:37: error: Proxy ((Comp (F1Sym :: x ~> F x z) F2Sym) :: F x ab ~> F x ab) T15629.hs:27:9: error: - • Couldn't match kind ‘ab1’ with ‘z’ - ‘ab1’ is a rigid type variable bound by + • Couldn't match kind ‘z1’ with ‘ab1’ + ‘z1’ is a rigid type variable bound by the type signature for: g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym) at T15629.hs:26:5-84 - ‘z’ is a rigid type variable bound by + ‘ab1’ is a rigid type variable bound by the type signature for: g :: forall z1 ab1. Proxy (Comp F1Sym F2Sym) at T15629.hs:26:5-84 When matching types f0 :: x ~> F x ab - F1Sym :: TyFun x1 (F x1 z) -> * + F1Sym :: TyFun x1 (F x1 z1) -> * Expected type: Proxy (Comp F1Sym F2Sym) Actual type: Proxy (Comp f0 F2Sym) • In the expression: sg Proxy Proxy diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr index 60da6c09ae..e0a3526000 100644 --- a/testsuite/tests/typecheck/should_fail/T3950.stderr +++ b/testsuite/tests/typecheck/should_fail/T3950.stderr @@ -1,6 +1,6 @@ T3950.hs:15:8: error: - • Couldn't match kind ‘* -> *’ with ‘*’ + • Couldn't match kind ‘*’ with ‘* -> *’ When matching types w :: (* -> * -> *) -> * Sealed :: (* -> *) -> * diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr index 660ef98f26..54c12f76f7 100644 --- a/testsuite/tests/typecheck/should_fail/T7368.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368.stderr @@ -1,6 +1,6 @@ T7368.hs:3:10: error: - • Couldn't match kind ‘*’ with ‘* -> *’ + • Couldn't match kind ‘* -> *’ with ‘*’ When matching types b0 :: * Maybe :: * -> * diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr index 16c8326afe..93b8b04378 100644 --- a/testsuite/tests/typecheck/should_fail/T7368a.stderr +++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr @@ -1,6 +1,6 @@ T7368a.hs:8:6: error: - • Couldn't match kind ‘*’ with ‘* -> *’ + • Couldn't match kind ‘* -> *’ with ‘*’ When matching types f :: * -> * Bad :: (* -> *) -> * |