summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRichard Eisenberg <rae@richarde.dev>2020-01-21 17:52:48 +0000
committerMarge Bot <ben+marge-bot@smart-cactus.org>2020-03-20 20:42:56 -0400
commit73a7383ebc17f495d7acd04007c8c56b46532cb6 (patch)
treeb3c9cabb3dc8ae0e7808fda0d65fa8696ebe1570
parentcb1785d9f839e34a3a4892f354f0c51cc6553c0e (diff)
downloadhaskell-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.
-rw-r--r--compiler/GHC/Core/Coercion.hs45
-rw-r--r--compiler/GHC/Core/TyCo/Rep.hs15
-rw-r--r--compiler/GHC/Hs/Expr.hs63
-rw-r--r--compiler/GHC/Hs/Pat.hs11
-rw-r--r--compiler/GHC/HsToCore/PmCheck.hs6
-rw-r--r--compiler/typecheck/Constraint.hs86
-rw-r--r--compiler/typecheck/TcCanonical.hs351
-rw-r--r--compiler/typecheck/TcErrors.hs112
-rw-r--r--compiler/typecheck/TcFlatten.hs5
-rw-r--r--compiler/typecheck/TcHsType.hs36
-rw-r--r--compiler/typecheck/TcInteract.hs19
-rw-r--r--compiler/typecheck/TcMType.hs41
-rw-r--r--compiler/typecheck/TcOrigin.hs2
-rw-r--r--compiler/typecheck/TcPluginM.hs3
-rw-r--r--compiler/typecheck/TcSMonad.hs81
-rw-r--r--compiler/typecheck/TcSimplify.hs14
-rw-r--r--compiler/typecheck/TcUnify.hs59
-rw-r--r--testsuite/tests/dependent/should_fail/BadTelescope5.stderr2
-rw-r--r--testsuite/tests/dependent/should_fail/T14066.stderr2
-rw-r--r--testsuite/tests/dependent/should_fail/T14066e.stderr18
-rw-r--r--testsuite/tests/ghci.debugger/scripts/break012.stdout14
-rw-r--r--testsuite/tests/indexed-types/should_fail/T14887.stderr6
-rw-r--r--testsuite/tests/indexed-types/should_fail/T3330c.stderr2
-rw-r--r--testsuite/tests/partial-sigs/should_fail/T14584.stderr46
-rw-r--r--testsuite/tests/patsyn/should_fail/T15685.stderr18
-rw-r--r--testsuite/tests/polykinds/T11399.stderr2
-rw-r--r--testsuite/tests/polykinds/T14846.stderr50
-rw-r--r--testsuite/tests/polykinds/T17841.stderr15
-rw-r--r--testsuite/tests/polykinds/T7278.stderr2
-rw-r--r--testsuite/tests/polykinds/T8616.stderr10
-rw-r--r--testsuite/tests/polykinds/T9017.stderr13
-rw-r--r--testsuite/tests/typecheck/should_fail/T15629.stderr10
-rw-r--r--testsuite/tests/typecheck/should_fail/T3950.stderr2
-rw-r--r--testsuite/tests/typecheck/should_fail/T7368.stderr2
-rw-r--r--testsuite/tests/typecheck/should_fail/T7368a.stderr2
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 :: (* -> *) -> *