Commit 8e15e3d3 authored by Richard Eisenberg's avatar Richard Eisenberg

Improve error messages around kind mismatches.

Previously, when canonicalizing (or unifying, in uType) a
heterogeneous equality, we emitted a kind equality and used the
resulting coercion to cast one side of the heterogeneous equality.

While sound, this led to terrible error messages. (See the bugs
listed below.) The problem is that using the coercion built from
the emitted kind equality is a bit like a wanted rewriting a wanted.
The solution is to keep heterogeneous equalities as irreducible.

See Note [Equalities with incompatible kinds] in TcCanonical.

This commit also removes a highly suspicious switch to FM_SubstOnly
when flattening in the kinds of a type variable. I have no idea
why this was there, other than as a holdover from pre-TypeInType.
I've not left a Note because there is simply no reason I can conceive
of that the FM_SubstOnly should be there.

One challenge with this patch is that the emitted derived equalities
might get emitted several times: when a heterogeneous equality is
in an implication and then gets floated out from the implication,
the Derived is present both in and out of the implication. This
causes a duplicate error message. (Test case:
typecheck/should_fail/T7368) Solution: track the provenance of
Derived constraints and refuse to float out a constraint that has
an insoluble Derived.

Lastly, this labels one test (dependent/should_fail/RAE_T32a)
as expect_broken, because the problem is really #12919. The
different handling of constraints in this patch exposes the error.

This fixes bugs #11198, #12373, #13530, and #13610.

test cases:
typecheck/should_fail/{T8262,T8603,tcail122,T12373,T13530,T13610}
parent 4a264157
......@@ -563,6 +563,22 @@ can_eq_nc' _flat rdr_env envs ev ReprEq ty1 ps_ty1 ty2 _
| Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2
= can_eq_newtype_nc ev IsSwapped ty2 stuff2 ty1 ps_ty1
-- Now, check for tyvars. This must happen before CastTy because we need
-- to catch casted tyvars, as the flattener might produce these,
-- due to the fact that flattened types have flattened kinds.
-- See Note [Flattening].
-- Note that there can be only one cast on the tyvar because this will
-- run after the "get rid of casts" case of can_eq_nc' function on the
-- not-yet-flattened types.
-- NB: pattern match on True: we want only flat types sent to canEqTyVar.
-- See also Note [No top-level newtypes on RHS of representational equalities]
can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
| Just (tv1, co1) <- getCastedTyVar_maybe ty1
= canEqTyVar ev eq_rel NotSwapped tv1 co1 ps_ty1 ty2 ps_ty2
can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2
| Just (tv2, co2) <- getCastedTyVar_maybe ty2
= canEqTyVar ev eq_rel IsSwapped tv2 co2 ps_ty2 ty1 ps_ty1
-- Then, get rid of casts
can_eq_nc' flat _rdr_env _envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2
= canEqCast flat ev eq_rel NotSwapped ty1 co1 ty2 ps_ty2
......@@ -609,14 +625,6 @@ can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
`andWhenContinue` \ new_ev ->
can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
-- Type variable on LHS or RHS are last.
-- NB: pattern match on True: we want only flat types sent to canEqTyVar.
-- See also Note [No top-level newtypes on RHS of representational equalities]
can_eq_nc' True _rdr_env _envs ev eq_rel (TyVarTy tv1) ps_ty1 ty2 ps_ty2
= canEqTyVar ev eq_rel NotSwapped tv1 ps_ty1 ty2 ps_ty2
can_eq_nc' True _rdr_env _envs ev eq_rel ty1 ps_ty1 (TyVarTy tv2) ps_ty2
= canEqTyVar ev eq_rel IsSwapped tv2 ps_ty2 ty1 ps_ty1
-- We've flattened and the types don't match. Give up.
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)
......@@ -1356,19 +1364,6 @@ isInsolubleOccursCheck does.
See also #10715, which induced this addition.
Note [No derived kind equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we're working with a heterogeneous derived equality
[D] (t1 :: k1) ~ (t2 :: k2)
we want to homogenise to establish the kind invariant on CTyEqCans.
But we can't emit [D] k1 ~ k2 because we wouldn't then be able to
use the evidence in the homogenised types. So we emit a wanted
constraint, because we do really need the evidence here.
Thus: no derived kind equalities.
-}
canCFunEqCan :: CtEvidence
......@@ -1396,54 +1391,120 @@ canCFunEqCan ev fn tys fsk
---------------------
canEqTyVar :: CtEvidence -- ev :: lhs ~ rhs
-> EqRel -> SwapFlag
-> TcTyVar -> TcType -- lhs: already flat, not a cast
-> TcType -> TcType -- rhs: already flat, not a cast
-> TcTyVar -> CoercionN -- tv1 |> co1
-> TcType -- lhs: pretty lhs, already flat
-> TcType -> TcType -- rhs: already flat
-> TcS (StopOrContinue Ct)
canEqTyVar ev eq_rel swapped tv1 ps_ty1 (TyVarTy tv2) _
| tv1 == tv2
= canEqReflexive ev eq_rel ps_ty1
canEqTyVar ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
| k1 `eqType` k2
= canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 xi2 ps_xi2
-- See Note [Equalities with incompatible kinds]
| CtGiven { ctev_evar = evar } <- ev
-- unswapped: tm :: (lhs :: k1) ~ (rhs :: k2)
-- swapped : tm :: (rhs :: k2) ~ (lhs :: k1)
= do { kind_ev_id <- newBoundEvVarId kind_pty
(EvCoercion $
if isSwapped swapped
then mkTcSymCo $ mkTcKindCo $ mkTcCoVarCo evar
else mkTcKindCo $ mkTcCoVarCo evar)
-- kind_ev_id :: (k1 :: *) ~ (k2 :: *) (whether swapped or not)
; let kind_ev = CtGiven { ctev_pred = kind_pty
, ctev_evar = kind_ev_id
, ctev_loc = kind_loc }
homo_co = mkSymCo $ mkCoVarCo kind_ev_id
rhs' = mkCastTy xi2 homo_co
ps_rhs' = mkCastTy ps_xi2 homo_co
; traceTcS "Hetero equality gives rise to given kind equality"
(ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
; emitWorkNC [kind_ev]
; type_ev <- newGivenEvVar loc $
if isSwapped swapped
then ( mkTcEqPredLikeEv ev rhs' lhs
, EvCoercion $
mkTcCoherenceLeftCo (mkTcCoVarCo evar) homo_co )
else ( mkTcEqPredLikeEv ev lhs rhs'
, EvCoercion $
mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
-- unswapped: type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
-- swapped : type_ev :: ((rhs |> sym kind_ev_id) :: k1) ~ (lhs :: k1)
; canEqTyVarHomo type_ev eq_rel swapped tv1 co1 ps_ty1 rhs' ps_rhs' }
-- See Note [Equalities with incompatible kinds]
| otherwise -- Wanted and Derived
-- NB: all kind equalities are Nominal
= do { emitNewDerivedEq kind_loc Nominal k1 k2
-- kind_ev :: (k1 :: *) ~ (k2 :: *)
; traceTcS "Hetero equality gives rise to derived kind equality" $
ppr ev
; continueWith (CIrredEvCan { cc_ev = ev }) }
where
lhs = mkTyVarTy tv1 `mkCastTy` co1
Pair _ k1 = coercionKind co1
k2 = typeKind xi2
| swapOverTyVars tv1 tv2
kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
kind_loc = mkKindLoc lhs xi2 loc
loc = ctev_loc ev
-- guaranteed that typeKind lhs == typeKind rhs
canEqTyVarHomo :: CtEvidence
-> EqRel -> SwapFlag
-> TcTyVar -> CoercionN -- lhs: tv1 |> co1
-> TcType -- pretty lhs
-> TcType -> TcType -- rhs (might not be flat)
-> TcS (StopOrContinue Ct)
canEqTyVarHomo ev eq_rel swapped tv1 co1 ps_ty1 ty2 _
| Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
, tv1 == tv2
= canEqReflexive ev eq_rel (mkTyVarTy tv1 `mkCastTy` co1)
-- we don't need to check co2 because its type must match co1
| Just (tv2, co2) <- tcGetCastedTyVar_maybe ty2
, swapOverTyVars tv1 tv2
= do { traceTcS "canEqTyVar" (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
; dflags <- getDynFlags
; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 ps_ty1 }
; canEqTyVar2 dflags ev eq_rel (flipSwap swapped) tv2 co2 ps_ty1 }
canEqTyVar ev eq_rel swapped tv1 _ _ ps_ty2
canEqTyVarHomo ev eq_rel swapped tv1 co1 _ _ ps_ty2
= do { dflags <- getDynFlags
; canEqTyVar2 dflags ev eq_rel swapped tv1 ps_ty2 }
; canEqTyVar2 dflags ev eq_rel swapped tv1 co1 ps_ty2 }
-- The RHS here is either not a casted tyvar, or it's a tyvar but we want
-- to rewrite the LHS to the RHS (as per swapOverTyVars)
canEqTyVar2 :: DynFlags
-> CtEvidence -- lhs ~ rhs (or, if swapped, orhs ~ olhs)
-> EqRel
-> SwapFlag
-> TcTyVar -- lhs, flat
-> TcType -- rhs, flat
-> TcTyVar -> CoercionN -- lhs = tv |> co, flat
-> TcType -- rhs
-> TcS (StopOrContinue Ct)
-- LHS is an inert type variable,
-- and RHS is fully rewritten, but with type synonyms
-- preserved as much as possible
canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
| Just xi2' <- metaTyVarUpdateOK dflags tv1 xi2 -- No occurs check
canEqTyVar2 dflags ev eq_rel swapped tv1 co1 orhs
| Just nrhs' <- metaTyVarUpdateOK dflags tv1 nrhs -- No occurs check
-- Must do the occurs check even on tyvar/tyvar
-- equalities, in case have x ~ (y :: ..x...)
-- Trac #12593
= rewriteEqEvidence ev swapped xi1 xi2' co1 co2
= rewriteEqEvidence ev swapped nlhs nrhs' rewrite_co1 rewrite_co2
`andWhenContinue` \ new_ev ->
homogeniseRhsKind new_ev eq_rel xi1 xi2' $ \new_new_ev xi2'' ->
CTyEqCan { cc_ev = new_new_ev, cc_tyvar = tv1
, cc_rhs = xi2'', cc_eq_rel = eq_rel }
continueWith (CTyEqCan { cc_ev = new_ev, cc_tyvar = tv1
, cc_rhs = nrhs', cc_eq_rel = eq_rel })
| otherwise -- For some reason (occurs check, or forall) we can't unify
-- We must not use it for further rewriting!
= do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr xi2)
; rewriteEqEvidence ev swapped xi1 xi2 co1 co2
= do { traceTcS "canEqTyVar2 can't unify" (ppr tv1 $$ ppr nrhs)
; rewriteEqEvidence ev swapped nlhs nrhs rewrite_co1 rewrite_co2
`andWhenContinue` \ new_ev ->
if isInsolubleOccursCheck eq_rel tv1 xi2
if isInsolubleOccursCheck eq_rel tv1 nrhs
then do { emitInsoluble (mkNonCanonical new_ev)
-- If we have a ~ [a], it is not canonical, and in particular
-- we don't want to rewrite existing inerts with it, otherwise
......@@ -1457,13 +1518,18 @@ canEqTyVar2 dflags ev eq_rel swapped tv1 xi2
-- But, the occurs-check certainly prevents the equality from being
-- canonical, and we might loop if we were to use it in rewriting.
else do { traceTcS "Possibly-soluble occurs check"
(ppr xi1 $$ ppr xi2)
(ppr nlhs $$ ppr nrhs)
; continueWith (CIrredEvCan { cc_ev = new_ev }) } }
where
role = eqRelRole eq_rel
xi1 = mkTyVarTy tv1
co1 = mkTcReflCo role xi1
co2 = mkTcReflCo role xi2
nlhs = mkTyVarTy tv1
nrhs = orhs `mkCastTy` mkTcSymCo co1
-- rewrite_co1 :: tv1 ~ (tv1 |> co1)
-- rewrite_co2 :: (rhs |> sym co1) ~ rhs
rewrite_co1 = mkTcReflCo role nlhs `mkTcCoherenceRightCo` co1
rewrite_co2 = mkTcReflCo role orhs `mkTcCoherenceLeftCo` mkTcSymCo co1
-- | Solve a reflexive equality constraint
canEqReflexive :: CtEvidence -- ty ~ ty
......@@ -1475,75 +1541,6 @@ canEqReflexive ev eq_rel ty
mkTcReflCo (eqRelRole eq_rel) ty)
; stopWith ev "Solved by reflexivity" }
-- See Note [Equalities with incompatible kinds]
homogeniseRhsKind :: CtEvidence -- ^ the evidence to homogenise
-> EqRel
-> TcType -- ^ original LHS
-> Xi -- ^ original RHS
-> (CtEvidence -> Xi -> Ct)
-- ^ how to build the homogenised constraint;
-- the 'Xi' is the new RHS
-> TcS (StopOrContinue Ct)
homogeniseRhsKind ev eq_rel lhs rhs build_ct
| k1 `tcEqType` k2
= continueWith (build_ct ev rhs)
| CtGiven { ctev_evar = evar } <- ev
-- tm :: (lhs :: k1) ~ (rhs :: k2)
= do { kind_ev_id <- newBoundEvVarId kind_pty
(EvCoercion $
mkTcKindCo $ mkTcCoVarCo evar)
-- kind_ev_id :: (k1 :: *) ~# (k2 :: *)
; let kind_ev = CtGiven { ctev_pred = kind_pty
, ctev_evar = kind_ev_id
, ctev_loc = kind_loc }
homo_co = mkSymCo $ mkCoVarCo kind_ev_id
rhs' = mkCastTy rhs homo_co
; traceTcS "Hetero equality gives rise to given kind equality"
(ppr kind_ev_id <+> dcolon <+> ppr kind_pty)
; emitWorkNC [kind_ev]
; type_ev <- newGivenEvVar loc
( mkTcEqPredLikeEv ev lhs rhs'
, EvCoercion $
mkTcCoherenceRightCo (mkTcCoVarCo evar) homo_co )
-- type_ev :: (lhs :: k1) ~ ((rhs |> sym kind_ev_id) :: k1)
; continueWith (build_ct type_ev rhs') }
| otherwise -- Wanted and Derived. See Note [No derived kind equalities]
-- evar :: (lhs :: k1) ~ (rhs :: k2)
= do { kind_co <- emitNewWantedEq kind_loc Nominal k1 k2
-- kind_ev :: (k1 :: *) ~ (k2 :: *)
; traceTcS "Hetero equality gives rise to wanted kind equality" $
ppr (kind_co)
; let homo_co = mkSymCo kind_co
-- homo_co :: k2 ~ k1
rhs' = mkCastTy rhs homo_co
; case ev of
CtGiven {} -> panic "homogeniseRhsKind"
CtDerived {} -> continueWith (build_ct (ev { ctev_pred = homo_pred })
rhs')
where homo_pred = mkTcEqPredLikeEv ev lhs rhs'
CtWanted { ctev_dest = dest } -> do
{ (type_ev, hole_co) <- newWantedEq loc role lhs rhs'
-- type_ev :: (lhs :: k1) ~ (rhs |> sym kind_co :: k1)
; setWantedEq dest
(hole_co `mkTransCo`
(mkReflCo role rhs
`mkCoherenceLeftCo` homo_co))
-- dest := hole ; <rhs> |> homo_co :: (lhs :: k1) ~ (rhs :: k2)
; continueWith (build_ct type_ev rhs') }}
where
k1 = typeKind lhs
k2 = typeKind rhs
kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind k1 k2
kind_loc = mkKindLoc lhs rhs loc
loc = ctev_loc ev
role = eqRelRole eq_rel
{-
Note [Canonical orientation for tyvar/tyvar equality constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -1605,21 +1602,66 @@ the fsk.
Note [Equalities with incompatible kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
canEqLeaf is about to make a CTyEqCan or CFunEqCan; but both have the
invariant that LHS and RHS satisfy the kind invariants for CTyEqCan,
CFunEqCan. What if we try to unify two things with incompatible
kinds?
What do we do when we have an equality
(tv :: k1) ~ (rhs :: k2)
where k1 and k2 differ? This Note explores this treacherous area.
First off, the question above is slightly the wrong question. Flattening
a tyvar will flatten its kind (Note [Flattening] in TcFlatten); flattening
the kind might introduce a cast. So we might have a casted tyvar on the
left. We thus revise our test case to
(tv |> co :: k1) ~ (rhs :: k2)
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
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.
The reason for this odd behavior is much the same as
Note [Wanteds do not rewrite Wanteds] in TcRnTypes: note that the
new `co` is a Wanted. 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. When the Derived is solved (by unification),
the original wanted (`w`) will get kicked out.
Note that, if we had [G] co1 :: k ~ Type available, then none of this code would
trigger, because flattening would have rewritten k to Type. That is,
`w` would look like [W] (alpha |> co1 :: Type) ~ (Int :: Type), and the tyvar
case will trigger, correctly rewriting alpha to (Int |> sym co1).
eg a ~ b where a::*, b::*->*
or a ~ b where a::*, b::k, k is a kind variable
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.
The CTyEqCan compatKind invariant is important. If we make a CTyEqCan
for a~b, then we might well *substitute* 'b' for 'a', and that might make
a well-kinded type ill-kinded; and that is bad (eg typeKind can crash, see
Trac #7696).
For Givens, this problem 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 canEqTyVar) and
carry on with a homogeneous equality constraint.
So instead for these ill-kinded equalities we homogenise the RHS of the
equality, emitting new constraints as necessary.
Separately, I (Richard E) spent some time pondering what to do in the case
that we have [W] (tv |> co1 :: k1) ~ (tv |> co2 :: k2) where k1 and k2
differ. Note that the tv is the same. (This case is handled as the first
case in canEqTyVarHomo.) At one point, I thought we could solve this limited
form of heterogeneous Wanted, but I then reconsidered and now treat this case
just like any other heterogeneous Wanted.
Note [Type synonyms and canonicalization]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -53,6 +53,7 @@ import SrcLoc
import DynFlags
import ListSetOps ( equivClasses )
import Maybes
import Pair
import qualified GHC.LanguageExtensions as LangExt
import FV ( fvVarList, unionFV )
......@@ -478,19 +479,23 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
-- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
-- we might suppress its error message, and proceed on past
-- type checking to get a Lint error later
report1 = [ ("custom_error", is_user_type_error,
True, mkUserTypeErrorReporter)
report1 = [ ("custom_error", 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)
, ("Out of scope", is_out_of_scope, True, mkHoleReporter)
, ("Holes", is_hole, False, mkHoleReporter)
, ("insoluble2 ty", utterly_wrong_ty, True, mkGroupReporter mkEqErr)
, ("insoluble2_ki", 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)
, ("Out of scope", is_out_of_scope, True, mkHoleReporter)
, ("Holes", is_hole, False, mkHoleReporter)
-- The only remaining equalities are alpha ~ ty,
-- where alpha is untouchable; and representational equalities
, ("Other eqs", is_equality, False, mkGroupReporter mkEqErr) ]
-- 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) ]
-- report2: we suppress these if there are insolubles elsewhere in the tree
report2 = [ ("Implicit params", is_ip, False, mkGroupReporter mkIPErr)
......@@ -510,6 +515,12 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
utterly_wrong _ _ = False
-- Like utterly_wrong, but suppress derived kind equalities
utterly_wrong_ty ct pred
= utterly_wrong ct pred && case ctOrigin ct of
KindEqOrigin {} -> False
_ -> True
-- Things like (a ~N Int)
very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
very_wrong _ _ = False
......@@ -527,6 +538,9 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
is_user_type_error ct _ = isUserTypeErrorCt ct
is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2
is_homo_equality _ _ = False
is_equality _ (EqPred {}) = True
is_equality _ _ = False
......@@ -1447,9 +1461,9 @@ the unsolved (t ~ Bool), t won't look like an untouchable meta-var
any more. So we don't assert that it is.
-}
mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
-- Don't have multiple equality errors from the same location
-- E.g. (Int,Bool) ~ (Bool,Int) one error will do!
mkEqErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
mkEqErr _ [] = panic "mkEqErr"
......@@ -1589,9 +1603,12 @@ 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 <- tcGetTyVar_maybe ty1 = mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
| Just tv2 <- tcGetTyVar_maybe ty2 = mkTyVarEqErr dflags ctxt report ct swapped tv2 ty1
| otherwise = reportEqErr 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
| otherwise
= reportEqErr ctxt report ct oriented ty1 ty2
where
swapped = fmap flipSwap oriented
......@@ -1606,13 +1623,13 @@ reportEqErr ctxt report ct oriented ty1 ty2
mkTyVarEqErr, mkTyVarEqErr'
:: DynFlags -> ReportErrCtxt -> Report -> Ct
-> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
-> Maybe SwapFlag -> TcTyVar -> TcCoercionN -> TcType -> TcM ErrMsg
-- tv1 and ty2 are already tidied
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
= 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
mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 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;
......@@ -1661,6 +1678,23 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 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 SigTv, else it'd have been unified, given
......@@ -1706,7 +1740,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
, Implic { ic_env = env, ic_given = given
, ic_tclvl = lvl, ic_info = skol_info } <- implic
= ASSERT2( not (isTouchableMetaTyVar lvl tv1)
, ppr tv1 ) -- See Note [Error messages for untouchables]
, ppr tv1 $$ ppr lvl ) -- See Note [Error messages for untouchables]
do { let msg = important $ misMatchMsg ct oriented ty1 ty2
tclvl_extra = important $
nest 2 $
......@@ -1725,6 +1759,9 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 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 = typeKind ty2
ty1 = mkTyVarTy tv1
occ_check_expand = occCheckForErrors dflags tv1 ty2
insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
......
......@@ -33,7 +33,7 @@ module TcEvidence (
mkTcKindCo,
tcCoercionKind, coVarsOfTcCo,
mkTcCoVarCo,
isTcReflCo,
isTcReflCo, isTcReflexiveCo,
tcCoercionRole,
unwrapIP, wrapIP
) where
......@@ -115,6 +115,10 @@ tcCoercionRole :: TcCoercion -> Role
coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet
isTcReflCo :: TcCoercion -> Bool
-- | This version does a slow check, calculating the related types and seeing
-- if they are equal.
isTcReflexiveCo :: TcCoercion -> Bool
mkTcReflCo = mkReflCo
mkTcSymCo = mkSymCo
mkTcTransCo = mkTransCo
......@@ -143,7 +147,7 @@ tcCoercionKind = coercionKind
tcCoercionRole = coercionRole
coVarsOfTcCo = coVarsOfCo
isTcReflCo = isReflCo
isTcReflexiveCo = isReflexiveCo
{-
%************************************************************************
......
......@@ -584,7 +584,7 @@ setMode new_mode thing_inside
else runFlatM thing_inside (env { fe_mode = new_mode })
-- | Use when flattening kinds/kind coercions. See
-- Note [No derived kind equalities] in TcCanonical
-- Note [No derived kind equalities]
flattenKinds :: FlatM a -> FlatM a
flattenKinds thing_inside
= FlatM $ \env ->
......@@ -717,6 +717,18 @@ soon throw out the phantoms when decomposing a TyConApp. (Or, the
canonicaliser will emit an insoluble, in which case the unflattened version
yields a better error message anyway.)
Note [No derived kind equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We call flattenKinds in two places: in flatten_co (Note [Flattening coercions])
and in flattenTyVar. The latter case is easier to understand; flattenKinds is
used to flatten the kind of a flat (i.e. inert) tyvar. Flattening a kind
naturally produces a coercion. This coercion is then used in the flattened type.
However, danger lurks if the flattening flavour (that is, the fe_flavour of the
FlattenEnv) is Derived: the coercion might be bottom. (This can happen when
looks up a kindvar in the inert set only to find a Derived equality, with
no coercion.) The solution is simple: ensure that the fe_flavour is not derived
when flattening a kind. This is what flattenKinds does.
-}
{- *********************************************************************
......@@ -1326,10 +1338,9 @@ flattenTyVar tv
FTRNotFollowed -- Done
-> do { let orig_kind = tyVarKind tv
; (_new_kind, kind_co) <- setMode FM_SubstOnly $
flattenKinds $
; (_new_kind, kind_co) <- flattenKinds $
flatten_one orig_kind
; let Pair _ zonked_kind = coercionKind kind_co
; let Pair _ zonked_kind = coercionKind kind_co
-- NB: kind_co :: _new_kind ~ zonked_kind
-- But zonked_kind is not necessarily the same as orig_kind
-- because that may have filled-in metavars.
......@@ -1339,13 +1350,13 @@ flattenTyVar tv
-- See also Note [Flattening]
-- An alternative would to use (zonkTcType orig_kind),
-- but some simple measurements suggest that's a little slower
; let tv' = setTyVarKind tv zonked_kind
tv_ty' = mkTyVarTy tv'
ty' = tv_ty' `mkCastTy` mkSymCo kind_co
; let tv' = setTyVarKind tv zonked_kind
tv_ty' = mkTyVarTy tv'
ty' = tv_ty' `mkCastTy` mkSymCo kind_co
; role <- getRole
; return (ty', mkReflCo role tv_ty'
`mkCoherenceLeftCo` mkSymCo kind_co) } }
; role <- getRole
; return (ty', mkReflCo role tv_ty'
`mkCoherenceLeftCo` mkSymCo kind_co) } }
flatten_tyvar1 :: TcTyVar -> FlatM FlattenTvResult
-- "Flattening" a type variable means to apply the substitution to it
...