Commit 73a7383e authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

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.
parent cb1785d9
Pipeline #16959 passed with stages
in 559 minutes and 52 seconds
......@@ -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
......@@ -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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -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
......
{-
(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
......
......@@ -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
-- ----------------------------------------------------------------------------
......
......@@ -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})
......
This diff is collapsed.
This diff is collapsed.
......@@ -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)
......
......@@ -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
......
......@@ -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 }
......
......@@ -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
......
......@@ -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
......
......@@ -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.
......
......@@ -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,_).