Commit e3dbb44f authored by Richard Eisenberg's avatar Richard Eisenberg

Fix #12919 by making the flattener homegeneous.

This changes a key invariant of the flattener. Previously,
flattening a type meant flattening its kind as well. But now,
flattening is always homogeneous -- that is, the kind of the
flattened type is the same as the kind of the input type.
This is achieved by various wizardry in the TcFlatten.flatten_many
function, as described in Note [flatten_many].

There are several knock-on effects, including some refactoring
in the canonicalizer to take proper advantage of the flattener's
changed behavior. In particular, the tyvar case of can_eq_nc' no
longer needs to take casts into account.

Another effect is that flattening a tyconapp might change it
into a casted tyconapp. This might happen if the result kind
of the tycon contains a variable, and that variable changes
during flattening. Because the flattener is homogeneous, it tacks
on a cast to keep the tyconapp kind the same. However, this
is problematic when flattening CFunEqCans, which need to have
an uncasted tyconapp on the LHS and must remain homogeneous.
The solution is a more involved canCFunEqCan, described in
Note [canCFunEqCan].

This patch fixes #13643 (as tested in typecheck/should_compile/T13643)
and the panic in typecheck/should_compile/T13822 (as reported in #14024).
Actually, there were two bugs in T13822: the first was just some
incorrect logic in tryFill (part of the unflattener) -- also fixed
in this patch -- and the other was the main bug fixed in this ticket.

The changes in this patch exposed a long-standing flaw in OptCoercion,
in that breaking apart an AppCo sometimes has unexpected effects on
kinds. See new Note [EtaAppCo] in OptCoercion, which explains the
problem and fix.

Also here is a reversion of the major change in
09bf135a, affecting ctEvCoercion.
It turns out that making the flattener homogeneous changes the
invariants on the algorithm, making the change in that patch
no longer necessary.

This patch also fixes:
  #14038 (dependent/should_compile/T14038)
  #13910 (dependent/should_compile/T13910)
  #13938 (dependent/should_compile/T13938)
  #14441 (typecheck/should_compile/T14441)
  #14556 (dependent/should_compile/T14556)
  #14720 (dependent/should_compile/T14720)
  #14749 (typecheck/should_compile/T14749)

Sadly, this patch negatively affects performance of type-family-
heavy code. The following patch fixes these performance degradations.
However, the performance fixes are somewhat invasive and so I've
kept them as a separate patch, labeling this one as [skip ci] so
that validation doesn't fail on the performance cases.
parent 97e1f300
This diff is collapsed.
This diff is collapsed.
......@@ -1597,7 +1597,7 @@ interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
; if canSolveByUnification tclvl tv rhs
then do { solveByUnification ev tv rhs
; n_kicked <- kickOutAfterUnification tv
; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
else unsolved_inert }
......@@ -1640,10 +1640,6 @@ solveByUnification wd tv xi
; unifyTyVar tv xi
; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
ppr_kicked :: Int -> SDoc
ppr_kicked 0 = empty
ppr_kicked n = parens (int n <+> text "kicked out")
{- Note [Avoid double unifications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The spontaneous solver has to return a given which mentions the unified unification
......@@ -1961,59 +1957,34 @@ improve_top_fun_eqs fam_envs fam_tc args rhs_ty
shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
-> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
-- See Note [Top-level reductions for type functions]
-- Previously, we flattened the tc_args here, but there's no need to do so.
-- And, if we did, this function would have all the complication of
-- TcCanonical.canCFunEqCan. See Note [canCFunEqCan]
shortCutReduction old_ev fsk ax_co fam_tc tc_args
= ASSERT( ctEvEqRel old_ev == NomEq)
do { (xis, cos) <- flattenManyNom old_ev tc_args
-- ax_co :: F args ~ G tc_args
-- cos :: xis ~ tc_args
-- old_ev :: F args ~ fsk
-- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
; new_ev <- case ctEvFlavour old_ev of
do { new_ev <- case ctEvFlavour old_ev of
Given -> newGivenEvVar deeper_loc
( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
, evCoercion (mkTcTyConAppCo Nominal fam_tc cos
`mkTcTransCo` mkTcSymCo ax_co
`mkTcTransCo` ctEvCoercion old_ev) )
( mkPrimEqPred (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
, evCoercion (mkTcSymCo ax_co
`mkTcTransCo` ctEvCoercion old_ev) )
Wanted {} ->
do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
(mkTyConApp fam_tc xis) (mkTyVarTy fsk)
; setWantedEq (ctev_dest old_ev) $
ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal
fam_tc cos)
`mkTcTransCo` new_co
(mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
; return new_ev }
Derived -> pprPanic "shortCutReduction" (ppr old_ev)
; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
, cc_tyargs = xis, cc_fsk = fsk }
, cc_tyargs = tc_args, cc_fsk = fsk }
; updWorkListTcS (extendWorkListFunEq new_ct)
; stopWith old_ev "Fun/Top (shortcut)" }
where
deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
-- (dischargeFmv x fmv co ty)
-- [W] ev :: F tys ~ fmv
-- co :: F tys ~ xi
-- Precondition: fmv is not filled, and fmv `notElem` xi
-- ev is Wanted
--
-- Then set fmv := xi,
-- set ev := co
-- kick out any inert things that are now rewritable
--
-- Does not evaluate 'co' if 'ev' is Derived
dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
= ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
do { setWantedEvTerm dest (EvExpr (evCoercion co))
; unflattenFmv fmv xi
; n_kicked <- kickOutAfterUnification fmv
; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
{- Note [Top-level reductions for type functions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
c.f. Note [The flattening story] in TcFlatten
......
......@@ -697,9 +697,11 @@ writeMetaTyVarRef tyvar ref ty
= do { meta_details <- readMutVar ref;
-- Zonk kinds to allow the error check to work
; zonked_tv_kind <- zonkTcType tv_kind
; zonked_ty_kind <- zonkTcType ty_kind
; let kind_check_ok = isPredTy tv_kind -- Don't check kinds for updates
-- to coercion variables. Why not??
; zonked_ty <- zonkTcType ty
; let zonked_ty_kind = typeKind zonked_ty -- need to zonk even before typeKind;
-- otherwise, we can panic in piResultTy
kind_check_ok = isPredTy tv_kind -- Don't check kinds for updates
-- to coercion variables. TODO (RAE): Why not?
|| isConstraintKind zonked_tv_kind
|| tcEqKind zonked_ty_kind zonked_tv_kind
-- Hack alert! isConstraintKind: see TcHsType
......@@ -708,7 +710,7 @@ writeMetaTyVarRef tyvar ref ty
kind_msg = hang (text "Ill-kinded update to meta tyvar")
2 ( ppr tyvar <+> text "::" <+> (ppr tv_kind $$ ppr zonked_tv_kind)
<+> text ":="
<+> ppr ty <+> text "::" <+> (ppr ty_kind $$ ppr zonked_ty_kind) )
<+> ppr ty <+> text "::" <+> (ppr zonked_ty_kind) )
; traceTc "writeMetaTyVar" (ppr tyvar <+> text ":=" <+> ppr ty)
......@@ -726,7 +728,6 @@ writeMetaTyVarRef tyvar ref ty
; writeMutVar ref (Indirect ty) }
where
tv_kind = tyVarKind tyvar
ty_kind = typeKind ty
tv_lvl = tcTyVarLevel tyvar
ty_lvl = tcTypeLevel ty
......
......@@ -2648,15 +2648,6 @@ For Givens we make new EvVars and bind them immediately. Two main reasons:
So a Given has EvVar inside it rather than (as previously) an EvTerm.
Note [Given in ctEvCoercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When retrieving the evidence from a Given equality, we update the type of the EvVar
from the ctev_pred field. In Note [Evidence field of CtEvidence], we claim that
the type of the evidence is never looked at -- but this isn't true in the case of
a coercion that is used in a type. (See the comments in Note [Flattening] in TcFlatten
about the FTRNotFollowed case of flattenTyVar.) So, right here where we are retrieving
the coercion from a Given, we update the type to make sure it's zonked.
-}
-- | A place for type-checking evidence to go after it is generated.
......@@ -2713,11 +2704,9 @@ ctEvExpr :: CtEvidence -> EvExpr
ctEvExpr ev@(CtWanted { ctev_dest = HoleDest _ }) = evCoercion $ ctEvCoercion ev
ctEvExpr ev = evId (ctEvEvId ev)
-- Always returns a coercion whose type is precisely ctev_pred of the CtEvidence.
-- See also Note [Given in ctEvCoercion]
ctEvCoercion :: CtEvidence -> Coercion
ctEvCoercion (CtGiven { ctev_pred = pred_ty, ctev_evar = ev_id })
= mkTcCoVarCo (setVarType ev_id pred_ty) -- See Note [Given in ctEvCoercion]
ctEvCoercion (CtGiven { ctev_evar = ev_id })
= mkTcCoVarCo ev_id
ctEvCoercion (CtWanted { ctev_dest = dest })
| HoleDest hole <- dest
= -- ctEvCoercion is only called on type equalities
......
......@@ -82,6 +82,7 @@ module TcSMonad (
-- The flattening cache
lookupFlatCache, extendFlatCache, newFlattenSkolem, -- Flatten skolems
dischargeFmv, pprKicked,
-- Inert CFunEqCans
updInertFunEqs, findFunEq,
......@@ -1134,8 +1135,78 @@ work?
because even tyvars in the casts and coercions could give
an infinite loop if we don't expose it
* CIrredCan: Yes if the inert set can rewrite the constraint.
We used to think splitting irreds was unnecessary, but
see Note [Splitting Irred WD constraints]
* Others: nothing is gained by splitting.
Note [Splitting Irred WD constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Splitting Irred constraints can make a difference. Here is the
scenario:
a[sk] :: F v -- F is a type family
beta :: alpha
work item: [WD] a ~ beta
This is heterogeneous, so we try flattening the kinds.
co :: F v ~ fmv
[WD] (a |> co) ~ beta
This is still hetero, so we emit a kind equality and make the work item an
inert Irred.
work item: [D] fmv ~ alpha
inert: [WD] (a |> co) ~ beta (CIrredCan)
Can't make progress on the work item. Add to inert set. This kicks out the
old inert, because a [D] can rewrite a [WD].
work item: [WD] (a |> co) ~ beta
inert: [D] fmv ~ alpha (CTyEqCan)
Can't make progress on this work item either (although GHC tries by
decomposing the cast and reflattening... but that doesn't make a difference),
which is still hetero. Emit a new kind equality and add to inert set. But,
critically, we split the Irred.
work list:
[D] fmv ~ alpha (CTyEqCan)
[D] (a |> co) ~ beta (CIrred) -- this one was split off
inert:
[W] (a |> co) ~ beta
[D] fmv ~ alpha
We quickly solve the first work item, as it's the same as an inert.
work item: [D] (a |> co) ~ beta
inert:
[W] (a |> co) ~ beta
[D] fmv ~ alpha
We decompose the cast, yielding
[D] a ~ beta
We then flatten the kinds. The lhs kind is F v, which flattens to fmv which
then rewrites to alpha.
co' :: F v ~ alpha
[D] (a |> co') ~ beta
Now this equality is homo-kinded. So we swizzle it around to
[D] beta ~ (a |> co')
and set beta := a |> co', and go home happy.
If we don't split the Irreds, we loop. This is all dangerously subtle.
This is triggered by test case typecheck/should_compile/SplitWD.
Note [Examples of how Derived shadows helps completeness]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Trac #10009, a very nasty example:
......@@ -1298,7 +1369,9 @@ shouldSplitWD inert_eqs (CTyEqCan { cc_tyvar = tv, cc_rhs = ty
|| anyRewritableTyVar False eq_rel (canRewriteTv inert_eqs) ty
-- NB False: do not ignore casts and coercions
-- See Note [Splitting WD constraints]
where
shouldSplitWD inert_eqs (CIrredCan { cc_ev = ev })
= anyRewritableTyVar False (ctEvEqRel ev) (canRewriteTv inert_eqs) (ctEvPred ev)
shouldSplitWD _ _ = False -- No point in splitting otherwise
......@@ -2954,6 +3027,30 @@ demoteUnfilledFmv fmv
do { tv_ty <- TcM.newFlexiTyVarTy (tyVarKind fmv)
; TcM.writeMetaTyVar fmv tv_ty } }
-----------------------------
dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
-- (dischargeFmv x fmv co ty)
-- [W] ev :: F tys ~ fmv
-- co :: F tys ~ xi
-- Precondition: fmv is not filled, and fmv `notElem` xi
-- ev is Wanted
--
-- Then set fmv := xi,
-- set ev := co
-- kick out any inert things that are now rewritable
--
-- Does not evaluate 'co' if 'ev' is Derived
dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
= ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
do { setWantedEvTerm dest (EvExpr (evCoercion co))
; unflattenFmv fmv xi
; n_kicked <- kickOutAfterUnification fmv
; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ pprKicked n_kicked) }
dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
pprKicked :: Int -> SDoc
pprKicked 0 = empty
pprKicked n = parens (int n <+> text "kicked out")
{- *********************************************************************
* *
......@@ -3212,4 +3309,3 @@ from which we get the implication
(forall a. t1 ~ t2)
See TcSMonad.deferTcSForAllEq
-}
......@@ -68,7 +68,7 @@ module TcType (
tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
tcRepGetNumAppTys,
tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, nextRole,
tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar,
tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
---------------------------------
......
This diff is collapsed.
......@@ -37,6 +37,7 @@ mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
isReflCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
decomposePiCos :: Kind -> [Type] -> Coercion -> ([Coercion], Coercion)
coVarKindsTypesRole :: CoVar -> (Kind, Kind, Type, Type, Role)
coVarRole :: CoVar -> Role
......
......@@ -93,8 +93,8 @@ optCoercion env co
(Pair in_ty1 in_ty2, in_role) = coercionKindRole co
(Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
in
ASSERT2( substTyUnchecked env in_ty1 `eqType` out_ty1 &&
substTyUnchecked env in_ty2 `eqType` out_ty2 &&
ASSERT2( substTy env in_ty1 `eqType` out_ty1 &&
substTy env in_ty2 `eqType` out_ty2 &&
in_role == out_role
, text "optCoercion changed types!"
$$ hang (text "in_co:") 2 (ppr co)
......@@ -596,15 +596,11 @@ opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
opt_trans_rule is co1@(AppCo co1a co1b) co2
| Just (co2a,co2b) <- etaAppCo_maybe co2
= fireTransRule "EtaAppL" co1 co2 $
mkAppCo (opt_trans is co1a co2a)
(opt_trans is co1b co2b)
= opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
opt_trans_rule is co1 co2@(AppCo co2a co2b)
| Just (co1a,co1b) <- etaAppCo_maybe co1
= fireTransRule "EtaAppR" co1 co2 $
mkAppCo (opt_trans is co1a co2a)
(opt_trans is co1b co2b)
= opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
-- Push transitivity inside forall
opt_trans_rule is co1 co2
......@@ -698,10 +694,45 @@ opt_trans_rule _ co1 co2 -- Identity rule
opt_trans_rule _ _ _ = Nothing
-- See Note [EtaAppCo]
opt_trans_rule_app :: InScopeSet
-> Coercion -- original left-hand coercion (printing only)
-> Coercion -- original right-hand coercion (printing only)
-> Coercion -- left-hand coercion "function"
-> [Coercion] -- left-hand coercion "args"
-> Coercion -- right-hand coercion "function"
-> [Coercion] -- right-hand coercion "args"
-> Maybe Coercion
opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
| AppCo co1aa co1ab <- co1a
, Just (co2aa, co2ab) <- etaAppCo_maybe co2a
= opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
| AppCo co2aa co2ab <- co2a
, Just (co1aa, co1ab) <- etaAppCo_maybe co1a
= opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
| otherwise
= ASSERT( co1bs `equalLength` co2bs )
fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
let Pair _ rt1a = coercionKind co1a
Pair lt2a _ = coercionKind co2a
Pair _ rt1bs = traverse coercionKind co1bs
Pair lt2bs _ = traverse coercionKind co2bs
kcoa = mkKindCo $ buildCoercion lt2a rt1a
kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
co2a' = mkCoherenceLeftCo co2a kcoa
co2bs' = zipWith mkCoherenceLeftCo co2bs kcobs
in
mkAppCos (opt_trans is co1a co2a')
(zipWith (opt_trans is) co1bs co2bs')
fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule _rule _co1 _co2 res
= -- pprTrace ("Trans rule fired: " ++ _rule) (vcat [ppr _co1, ppr _co2, ppr res]) $
Just res
= Just res
{-
Note [Conflict checking with AxiomInstCo]
......@@ -758,6 +789,65 @@ that (Id Int) and (Id Bool) are Surely Apart, as they're headed by type
families. At the time of writing, I (Richard Eisenberg) couldn't think of
a way of detecting this any more efficient than just building the optimised
coercion and checking.
Note [EtaAppCo]
~~~~~~~~~~~~~~~
Suppose we're trying to optimize (co1a co1b ; co2a co2b). Ideally, we'd
like to rewrite this to (co1a ; co2a) (co1b ; co2b). The problem is that
the resultant coercions might not be well kinded. Here is an example (things
labeled with x don't matter in this example):
k1 :: Type
k2 :: Type
a :: k1 -> Type
b :: k1
h :: k1 ~ k2
co1a :: x1 ~ (a |> (h -> <Type>)
co1b :: x2 ~ (b |> h)
co2a :: a ~ x3
co2b :: b ~ x4
First, convince yourself of the following:
co1a co1b :: x1 x2 ~ (a |> (h -> <Type>)) (b |> h)
co2a co2b :: a b ~ x3 x4
(a |> (h -> <Type>)) (b |> h) `eqType` a b
That last fact is due to Note [Non-trivial definitional equality] in TyCoRep,
where we ignore coercions in types as long as two types' kinds are the same.
In our case, we meet this last condition, because
(a |> (h -> <Type>)) (b |> h) :: Type
and
a b :: Type
So the input coercion (co1a co1b ; co2a co2b) is well-formed. But the
suggested output coercions (co1a ; co2a) and (co1b ; co2b) are not -- the
kinds don't match up.
The solution here is to twiddle the kinds in the output coercions. First, we
need to find coercions
ak :: kind(a |> (h -> <Type>)) ~ kind(a)
bk :: kind(b |> h) ~ kind(b)
This can be done with mkKindCo and buildCoercion. The latter assumes two
types are identical modulo casts and builds a coercion between them.
Then, we build (co1a ; co2a |> sym ak) and (co1b ; co2b |> sym bk) as the
output coercions. These are well-kinded. (We cast the right-hand coercion
because mkCoherenceLeftCo is smaller than mkCoherenceRightCo.)
Also, note that all of this is done after accumulated any nested AppCo
parameters. This step is to avoid quadratic behavior in calling coercionKind.
The problem described here was first found in dependent/should_compile/dynamic-paper.
-}
-- | Check to make sure that an AxInstCo is internally consistent.
......
......@@ -265,8 +265,10 @@ data Type
Type
Type -- ^ Type application to something other than a 'TyCon'. Parameters:
--
-- 1) Function: must /not/ be a 'TyConApp',
-- 1) Function: must /not/ be a 'TyConApp' or 'CastTy',
-- must be another 'AppTy', or 'TyVarTy'
-- See Note [Respecting definitional equality] (EQ1) about the
-- no 'CastTy' requirement
--
-- 2) Argument type
......@@ -299,8 +301,8 @@ data Type
Type
KindCoercion -- ^ A kind cast. The coercion is always nominal.
-- INVARIANT: The cast is never refl.
-- INVARIANT: The cast is "pushed down" as far as it
-- can go. See Note [Pushing down casts]
-- INVARIANT: The Type is not a CastTy (use TransCo instead)
-- See Note [Respecting definitional equality] (EQ2) and (EQ3)
| CoercionTy
Coercion -- ^ Injection of a Coercion into a type
......@@ -340,19 +342,12 @@ kinds or types.
This kind instantiation only happens in TyConApp currently.
Note [Pushing down casts]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have (a :: k1 -> *), (b :: k1), and (co :: * ~ q).
The type (a b |> co) is `eqType` to ((a |> co') b), where
co' = (->) <k1> co. Thus, to make this visible to functions
that inspect types, we always push down coercions, preferring
the second form. Note that this also applies to TyConApps!
Note [Non-trivial definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Is Int |> <*> the same as Int? YES! In order to reduce headaches,
we decide that any reflexive casts in types are just ignored. More
generally, the `eqType` function, which defines Core's type equality
we decide that any reflexive casts in types are just ignored.
(Indeed they must be. See Note [Respecting definitional equality].)
More generally, the `eqType` function, which defines Core's type equality
relation, ignores casts and coercion arguments, as long as the
two types have the same kind. This allows us to be a little sloppier
in keeping track of coercions, which is a good thing. It also means
......@@ -385,6 +380,9 @@ The effect of this all is that eqType, the implementation of the implicit
equality check, can use any homogeneous relation that is smaller than ~, as
those rules must also be admissible.
A more drawn out argument around all of this is presented in Section 7.2 of
Richard E's thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf).
What would go wrong if we insisted on the casts matching? See the beginning of
Section 8 in the unpublished paper above. Theoretically, nothing at all goes
wrong. But in practical terms, getting the coercions right proved to be
......@@ -405,10 +403,67 @@ constructors and destructors in Type respect whatever relation is chosen.
Another helpful principle with eqType is this:
** If (t1 eqType t2) then I can replace t1 by t2 anywhere. **
(EQ) If (t1 `eqType` t2) then I can replace t1 by t2 anywhere.
This principle also tells us that eqType must relate only types with the
same kinds.
Note [Respecting definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Non-trivial definitional equality] introduces the property (EQ).
How is this upheld?
Any function that pattern matches on all the constructors will have to
consider the possibility of CastTy. Presumably, those functions will handle
CastTy appropriately and we'll be OK.
More dangerous are the splitXXX functions. Let's focus on splitTyConApp.
We don't want it to fail on (T a b c |> co). Happily, if we have
(T a b c |> co) `eqType` (T d e f)
then co must be reflexive. Why? eqType checks that the kinds are equal, as
well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f).
By the kind check, we know that (T a b c |> co) and (T d e f) have the same
kind. So the only way that co could be non-reflexive is for (T a b c) to have
a different kind than (T d e f). But because T's kind is closed (all tycon kinds
are closed), the only way for this to happen is that one of the arguments has
to differ, leading to a contradiction. Thus, co is reflexive.
Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
about outermost casts to uphold (EQ). Eliminating reflexive casts is done
in mkCastTy.
Unforunately, that's not the end of the story. Consider comparing
(T a b c) =? (T a b |> (co -> <Type>)) (c |> co)
These two types have the same kind (Type), but the left type is a TyConApp
while the right type is not. To handle this case, we say that the right-hand
type is ill-formed, requiring an AppTy never to have a casted TyConApp
on its left. It is easy enough to pull around the coercions to maintain
this invariant, as done in Type.mkAppTy. In the example above, trying to
form the right-hand type will instead yield (T a b (c |> co |> sym co) |> <Type>).
Both the casts there are reflexive and will be dropped. Huzzah.
This idea of pulling coercions to the right works for splitAppTy as well.
However, there is one hiccup: it's possible that a coercion doesn't relate two
Pi-types. For example, if we have @type family Fun a b where Fun a b = a -> b@,
then we might have (T :: Fun Type Type) and (T |> axFun) Int. That axFun can't
be pulled to the right. But we don't need to pull it: (T |> axFun) Int is not
`eqType` to any proper TyConApp -- thus, leaving it where it is doesn't violate
our (EQ) property.
Lastly, in order to detect reflexive casts reliably, we must make sure not
to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
In sum, in order to uphold (EQ), we need the following three invariants:
(EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
cast is one that relates either a FunTy to a FunTy or a
ForAllTy to a ForAllTy.
(EQ2) No reflexive casts in CastTy.
(EQ3) No nested CastTys.
These invariants are all documented above, in the declaration for Type.
-}
{- **********************************************************************
......
......@@ -30,7 +30,7 @@ module Type (
mkTyConApp, mkTyConTy,
tyConAppTyCon_maybe, tyConAppTyConPicky_maybe,
tyConAppArgs_maybe, tyConAppTyCon, tyConAppArgs,
splitTyConApp_maybe, splitTyConApp, tyConAppArgN, nextRole,
splitTyConApp_maybe, splitTyConApp, tyConAppArgN,
tcRepSplitTyConApp_maybe, tcSplitTyConApp_maybe,
splitListTyConApp_maybe,
repSplitTyConApp_maybe,
......@@ -92,7 +92,7 @@ module Type (
mkAnonBinder,
isAnonTyBinder, isNamedTyBinder,
binderVar, binderVars, binderKind, binderArgFlag,
tyBinderType,
tyBinderType, tyBinderVar_maybe,
binderRelevantType_maybe, caseBinder,
isVisibleArgFlag, isInvisibleArgFlag, isVisibleBinder, isInvisibleBinder,
tyConBindersTyBinders,
......@@ -659,6 +659,11 @@ the type checker (e.g. when matching type-function equations).
-- | Applies a type to another, as in e.g. @k a@
mkAppTy :: Type -> Type -> Type
-- See Note [Respecting definitional equality], invariant (EQ1).
mkAppTy (CastTy fun_ty co) arg_ty
| ([arg_co], res_co) <- decomposePiCos (typeKind fun_ty) [arg_ty] co
= (fun_ty `mkAppTy` (arg_ty `mkCastTy` arg_co)) `mkCastTy` res_co
mkAppTy (TyConApp tc tys) ty2 = mkTyConApp tc (tys ++ [ty2])
mkAppTy ty1 ty2 = AppTy ty1 ty2
-- Note that the TyConApp could be an
......@@ -672,6 +677,15 @@ mkAppTy ty1 ty2 = AppTy ty1 ty2
mkAppTys :: Type -> [Type] -> Type
mkAppTys ty1 [] = ty1
mkAppTys (CastTy fun_ty co) arg_tys -- much more efficient then nested mkAppTy
-- Why do this? See (EQ1) of
-- Note [Respecting definitional equality]
-- in TyCoRep
= foldl AppTy ((mkAppTys fun_ty casted_arg_tys) `mkCastTy` res_co) leftovers
where
(arg_cos, res_co) = decomposePiCos (typeKind fun_ty) arg_tys co
(args_to_cast, leftovers) = splitAtList arg_cos arg_tys
casted_arg_tys = zipWith mkCastTy args_to_cast arg_cos
mkAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
mkAppTys ty1 tys2 = foldl AppTy ty1 tys2
......@@ -1126,20 +1140,6 @@ splitListTyConApp_maybe ty = case splitTyConApp_maybe ty of
Just (tc,[e]) | tc == listTyCon -> Just e
_other -> Nothing
-- | What is the role assigned to the next parameter of this type? Usually,
-- this will be 'Nominal', but if the type is a 'TyConApp', we may be able to
-- do better. The type does *not* have to be well-kinded when applied for this
-- to work!
nextRole :: Type -> Role
nextRole ty
| Just (tc, tys) <- splitTyConApp_maybe ty
, let num_tys = length tys
, num_tys < tyConArity tc
= tyConRoles tc `getNth` num_tys
| otherwise
= Nominal
newTyConInstRhs :: TyCon -> [Type] -> Type
-- ^ Unwrap one 'layer' of newtype on a type constructor and its
-- arguments, using an eta-reduced version of the @newtype@ if possible.
......@@ -1156,47 +1156,6 @@ newTyConInstRhs tycon tys
~~~~~~
A casted type has its *kind* casted into something new.
Note [No reflexive casts in types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As far as possible, we would like to maintain the following property:
(*) If (t1 `eqType` t2), then t1 and t2 are treated identically within GHC.
The (*) property is very useful, because we have a tendency to compare two
types to see if they're equal, and then arbitrarily choose one. We don't
want this arbitrary choice to then matter later on. Maintaining (*) means
that every function that looks at a structure of a type must think about
casts. In places where we directly pattern-match, this consideration is
forced by consideration of the CastTy constructor.
But, when we call a splitXXX function, it's easy to ignore the possibility
of casts. In particular, splitTyConApp is used extensively, and we don't
want it to fail on (T a b c |> co). Happily, if we have
(T a b c |> co) `eqType` (T d e f)
then co must be reflexive. Why? eqType checks that the kinds are equal, as
well as checking that (a `eqType` d), (b `eqType` e), and (c `eqType` f).
By the kind check, we know that (T a b c |> co) and (T d e f) have the same
kind. So the only way that co could be non-reflexive is for (T a b c) to have
a different kind than (T d e f). But because T's kind is closed (all tycon kinds
are closed), the only way for this to happen is that one of the arguments has
to differ, leading to a contradiction. Thus, co is reflexive.
Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
about outermost casts to uphold (*).
Unfortunately, that's not the end of the story. Consider comparing
(T a b c) =? (T a b |> (co -> <Type>)) (c |> sym co)
These two types have the same kind (Type), but the left type is a TyConApp
while the right type is not. To handle this case, we will have to implement
some variant of the dreaded KPush algorithm (c.f. CoreOpt.pushCoDataCon).
This stone is left unturned for now, meaning that we don't yet uphold (*).
The other place where (*) will be hard to guarantee is in splitAppTy, because
I (Richard E) can't think of a way to push coercions into AppTys. The good
news here is that splitAppTy is not used all that much, and so all clients of
that function can simply be told to use splitCastTy as well, in order to
uphold (*). This, too, is left undone, for now.
-}
splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
......@@ -1206,16 +1165,17 @@ splitCastTy_maybe _ = Nothing
-- | Make a 'CastTy'. The Coercion must be nominal. Checks the
-- Coercion for reflexivity, dropping it if it's reflexive.
-- See Note [No reflexive casts in types]
-- See Note [Respecting definitional equality] in TyCoRep
mkCastTy :: Type -> Coercion -> Type
mkCastTy ty co | isReflexiveCo co = ty
mkCastTy ty co | isReflexiveCo co = ty -- (EQ2) from the Note
-- NB: Do the slow check here. This is important to keep the splitXXX
-- functions working properly. Otherwise, we may end up with something
-- like (((->) |> something_reflexive_but_not_obviously_so) biz baz)
-- fails under splitFunTy_maybe. This happened with the cheaper check
-- in test dependent/should_compile/dynamic-paper.
mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2)
mkCastTy (CastTy ty co1) co2 = mkCastTy ty (co1 `mkTransCo` co2) -- (EQ3) from the Note
-- call mkCastTy again for the reflexivity check
mkCastTy ty co = CastTy ty co
tyConBindersTyBinders :: [TyConBinder] -> [TyBinder]
......@@ -1495,6 +1455,10 @@ isNamedTyBinder :: TyBinder -> Bool
isNamedTyBinder (Named {}) = True
isNamedTyBinder (Anon {}) = False
tyBinderVar_maybe :: TyBinder -> Maybe TyVar
tyBinderVar_maybe (Named tv) = Just $ binderVar tv