Commit 09bf135a authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Ben Gamari

Fix #13333 by fixing the covar's type in ctEvCoercion

The change is noted in Note [Given in ctEvCoercion]. This patch
also adds a bit more commentary to TcFlatten, documenting some
key invariants of the flattening algorithm. While in the area,
I also removed some stale commentary from TcCanonical.
parent 466803a0
......@@ -50,85 +50,23 @@ Note [Canonicalization]
~~~~~~~~~~~~~~~~~~~~~~~
Canonicalization converts a simple constraint to a canonical form. It is
unary (i.e. treats individual constraints one at a time), does not do
any zonking, but lives in TcS monad because it needs to create fresh
variables (for flattening) and consult the inerts (for efficiency).
The execution plan for canonicalization is the following:
1) Decomposition of equalities happens as necessary until we reach a
variable or type family in one side. There is no decomposition step
for other forms of constraints.
2) If, when we decompose, we discover a variable on the head then we
look at inert_eqs from the current inert for a substitution for this
variable and contine decomposing. Hence we lazily apply the inert
substitution if it is needed.
3) If no more decomposition is possible, we deeply apply the substitution
from the inert_eqs and continue with flattening.
4) During flattening, we examine whether we have already flattened some
function application by looking at all the CTyFunEqs with the same
function in the inert set. The reason for deeply applying the inert
substitution at step (3) is to maximise our chances of matching an
already flattened family application in the inert.
The net result is that a constraint coming out of the canonicalization
phase cannot be rewritten any further from the inerts (but maybe /it/ can
rewrite an inert or still interact with an inert in a further phase in the
simplifier.
Note [Caching for canonicals]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Our plan with pre-canonicalization is to be able to solve a constraint
really fast from existing bindings in TcEvBinds. So one may think that
the condition (isCNonCanonical) is not necessary. However consider
the following setup:
InertSet = { [W] d1 : Num t }
WorkList = { [W] d2 : Num t, [W] c : t ~ Int}
Now, we prioritize equalities, but in our concrete example
(should_run/mc17.hs) the first (d2) constraint is dealt with first,
because (t ~ Int) is an equality that only later appears in the
worklist since it is pulled out from a nested implication
constraint. So, let's examine what happens:
- We encounter work item (d2 : Num t)
- Nothing is yet in EvBinds, so we reach the interaction with inerts
and set:
d2 := d1
and we discard d2 from the worklist. The inert set remains unaffected.
- Now the equation ([W] c : t ~ Int) is encountered and kicks-out
(d1 : Num t) from the inerts. Then that equation gets
spontaneously solved, perhaps. We end up with:
InertSet : { [G] c : t ~ Int }
WorkList : { [W] d1 : Num t}
- Now we examine (d1), we observe that there is a binding for (Num
t) in the evidence binds and we set:
d1 := d2
and end up in a loop!
Now, the constraints that get kicked out from the inert set are always
Canonical, so by restricting the use of the pre-canonicalizer to
NonCanonical constraints we eliminate this danger. Moreover, for
canonical constraints we already have good caching mechanisms
(effectively the interaction solver) and we are interested in reducing
things like superclasses of the same non-canonical constraint being
generated hence I don't expect us to lose a lot by introducing the
(isCNonCanonical) restriction.
A similar situation can arise in TcSimplify, at the end of the
solve_wanteds function, where constraints from the inert set are
returned as new work -- our substCt ensures however that if they are
not rewritten by subst, they remain canonical and hence we will not
attempt to solve them from the EvBinds. If on the other hand they did
get rewritten and are now non-canonical they will still not match the
EvBinds, so we are again good.
unary (i.e. treats individual constraints one at a time).
Constraints originating from user-written code come into being as
CNonCanonicals (except for CHoleCans, arising from holes). We know nothing
about these constraints. So, first:
Classify CNonCanoncal constraints, depending on whether they
are equalities, class predicates, or other.
Then proceed depending on the shape of the constraint. Generally speaking,
each constraint gets flattened and then decomposed into one of several forms
(see type Ct in TcRnTypes).
When an already-canonicalized constraint gets kicked out of the inert set,
it must be recanonicalized. But we know a bit about its shape from the
last time through, so we can skip the classification step.
-}
-- Top-level canonicalization
......@@ -1739,7 +1677,7 @@ may reflect the result of unification alpha := ty, so new_pred might
not _look_ the same as old_pred, and it's vital to proceed from now on
using new_pred.
The flattener preserves type synonyms, so they should appear in new_pred
qThe flattener preserves type synonyms, so they should appear in new_pred
as well as in old_pred; that is important for good error messages.
-}
......
......@@ -751,6 +751,8 @@ flattenManyNom ev tys
flatten ty ==> (xi, co)
where
xi has no type functions, unless they appear under ForAlls
has no skolems that are mapped in the inert set
has no filled-in metavariables
co :: xi ~ ty
Note that it is flatten's job to flatten *every type function it sees*.
......@@ -761,12 +763,53 @@ Flattening also:
* applies the substitution embodied in the inert set
Because flattening zonks and the returned coercion ("co" above) is also
zonked, it's possible that (co :: xi ~ ty) isn't quite true, as ty (the
input to the flattener) might not be zonked. After zonking everything,
(co :: xi ~ ty) will be true, however. It is for this reason that we
zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
we can rely on these facts:
(F1) typeKind(xi) succeeds and returns a fully zonked kind
(F2) co :: xi ~ zonk(ty)
Note that the left-hand type of co is *always* precisely xi. The right-hand
type may or may not be ty, however: if ty has unzonked filled-in metavariables,
then the right-hand type of co will be the zonked version of ty.
It is for this reason that we
occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
even before we zonk the whole program. (In particular, this is why the
zonk in flattenTyVar is necessary.)
even before we zonk the whole program. For example, see the FTRNotFollowed
case in flattenTyVar.
Why have these invariants on flattening? Really, they're both to ensure
invariant (F1), which is a Good Thing because we sometimes use typeKind
during canonicalisation, and we want this kind to be zonked (e.g., see
TcCanonical.homogeniseRhsKind). Invariant (F2) is needed solely to support
(F1). It is relied on in one place:
- The FTRNotFollowed case in flattenTyVar. Here, we have a tyvar
that cannot be reduced any further (that is, no equality over the tyvar
is in the inert set such that the inert equality can rewrite the constraint
at hand, and it is not a filled-in metavariable).
But its kind might still not be flat,
if it mentions a type family or a variable that can be rewritten. Flattened
types have flattened kinds (see below), so we must flatten the kind. Here is
an example:
let kappa be a filled-in metavariable such that kappa := k.
[G] co :: k ~ Type
We are flattening
a :: kappa
where a is a skolem.
We end up in the FTRNotFollowed case, but we need to flatten the kind kappa.
Flattening kappa yields (Type, kind_co), where kind_co :: Type ~ k. Note that the
right-hand type of kind_co is *not* kappa, because (F1) tells us it's zonk(kappa),
which is k. Now, we return (a |> sym kind_co). If we are to uphold (F1), then
the right-hand type of (sym kind_co) had better be fully zonked. In other words,
the left-hand type of kind_co needs to be zonked... which is precisely what (F2)
guarantees.
In order to support (F2), we require that ctEvCoercion, when called on a
zonked CtEvidence, always returns a zonked coercion. See Note [Given in
ctEvCoercion]. This requirement comes into play in flatten_tyvar2. (I suppose
we could move the logic from ctEvCoercion to flatten_tyvar2, but it's much
easier to do in ctEvCoercion.)
Flattening a type also means flattening its kind. In the case of a type
variable whose kind mentions a type family, this might mean that the result
......@@ -876,7 +919,7 @@ flatten_one (AppTy ty1 ty2)
(NomEq, _) -> flatten_rhs xi1 co1 NomEq
(ReprEq, Nominal) -> flatten_rhs xi1 co1 NomEq
(ReprEq, Representational) -> flatten_rhs xi1 co1 ReprEq
(ReprEq, Phantom) ->
(ReprEq, Phantom) -> -- See Note [Phantoms in the flattener]
do { ty2 <- liftTcS $ zonkTcType ty2
; return ( mkAppTy xi1 ty2
, mkAppCo co1 (mkNomReflCo ty2)) } }
......@@ -954,8 +997,8 @@ flatten_one (CoercionTy co) = first mkCoercionTy <$> flatten_co co
-- between and then use transitivity. See Note [Flattening coercions]
flatten_co :: Coercion -> FlatM (Coercion, Coercion)
flatten_co co
= do { let (Pair ty1 ty2, role) = coercionKindRole co
; co <- liftTcS $ zonkCo co -- squeeze out any metavars from the original
= do { co <- liftTcS $ zonkCo co -- see Note [Zonking when flattening a coercion]
; let (Pair ty1 ty2, role) = coercionKindRole co
; (co1, co2) <- flattenKinds $
do { (_, co1) <- flatten_one ty1
; (_, co2) <- flatten_one ty2
......@@ -999,12 +1042,39 @@ In other words:
then
fco :: fs ~r1 ft
fs, ft are flattened types
kco :: (fs ~r1 ft) ~r2 (s ~r1 t)
kco :: fco ~r2 co
The second return value of flatten_co is always a ProofIrrelCo. As
such, it doesn't contain any information the caller doesn't have and
might not be necessary in whatever comes next.
Note that a flattened coercion might have unzonked metavariables or
type functions in it -- but its *kind* will not. Instead of just flattening
the kinds and using mkTransCo, we could actually flatten the coercion
structurally. But doing so seems harder than simply flattening the types.
Note [Zonking when flattening a coercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The first step in flatten_co (see Note [Flattening coercions]) is to
zonk the input. This is necessary because we want to ensure the following
invariants (c.f. the invariants (F1) and (F2) in Note [Flattening])
If
(co', kco) <- flatten_co co
Then
(FC1) coercionKind(co') succeeds and produces a fully zonked pair of kinds
(FC2) kco :: co' ~ zonk(co)
We must zonk to ensure (1). This is because fco is built by using mkTransCo
to build up on the input co. But if the only action that happens during
flattening ty1 and ty2 is to zonk metavariables, the coercions returned
(co1 and co2) will be reflexive. The mkTransCo calls will drop the reflexive
coercions and co' will be the same as co -- with unzonked kinds.
These invariants are necessary to uphold (F1) and (F2) in the CastTy and
CoercionTy cases.
We zonk right at the beginning to avoid duplicating work when flattening the
ty1 and ty2.
Note [Flattening synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Not expanding synonyms aggressively improves error messages, and
......
......@@ -1646,9 +1646,9 @@ of (cc_ev ct), and is fully rewritten wrt the substitution. Eg for CDictCan,
This holds by construction; look at the unique place where CDictCan is
built (in TcCanonical).
In contrast, the type of the evidence *term* (ccev_evtm or ctev_evar/dest) in
In contrast, the type of the evidence *term* (ctev_dest / ctev_evar) in
the evidence may *not* be fully zonked; we are careful not to look at it
during constraint solving. See Note [Evidence field of CtEvidence]
during constraint solving. See Note [Evidence field of CtEvidence].
-}
mkNonCanonical :: CtEvidence -> Ct
......@@ -2402,6 +2402,16 @@ For Givens we make new EvVars and bind them immediately. Two main reasons:
(see evTermCoercion), so the easy thing is to bind it to an Id.
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.
......@@ -2418,7 +2428,6 @@ data TcEvDest
data CtEvidence
= CtGiven -- Truly given, not depending on subgoals
-- NB: Spontaneous unifications belong here
{ ctev_pred :: TcPredType -- See Note [Ct/evidence invariant]
, ctev_evar :: EvVar -- See Note [Evidence field of CtEvidence]
, ctev_loc :: CtLoc }
......@@ -2459,9 +2468,11 @@ ctEvTerm :: CtEvidence -> EvTerm
ctEvTerm ev@(CtWanted { ctev_dest = HoleDest _ }) = EvCoercion $ ctEvCoercion ev
ctEvTerm ev = EvId (ctEvId 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_evar = ev_id })
= mkTcCoVarCo ev_id
ctEvCoercion (CtGiven { ctev_pred = pred_ty, ctev_evar = ev_id })
= mkTcCoVarCo (setVarType ev_id pred_ty) -- See Note [Given in ctEvCoercion]
ctEvCoercion (CtWanted { ctev_dest = dest, ctev_pred = pred })
| HoleDest hole <- dest
, Just (role, ty1, ty2) <- getEqPredTys_maybe pred
......
......@@ -1382,6 +1382,7 @@ addInertEq :: Ct -> TcS ()
addInertEq ct
= do { traceTcS "addInertEq {" $
text "Adding new inert equality:" <+> ppr ct
; ics <- getInertCans
; ct@(CTyEqCan { cc_tyvar = tv, cc_ev = ev }) <- maybeEmitShadow ics ct
......
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module T13333 where
import Data.Data
import GHC.Exts (Constraint)
data T (phantom :: k) = T
data D (p :: k -> Constraint) (x :: j) where
D :: forall (p :: k -> Constraint) (x :: k). p x => D p x
class Possibly p x where
possibly :: proxy1 p -> proxy2 x -> Maybe (D p x)
dataCast1T :: forall k c t (phantom :: k).
(Typeable k, Typeable t, Typeable phantom, Possibly Data phantom)
=> (forall d. Data d => c (t d))
-> Maybe (c (T phantom))
dataCast1T f = case possibly (Proxy :: Proxy Data) (Proxy :: Proxy phantom) of
Nothing -> Nothing
Just D -> gcast1 f
......@@ -556,3 +556,4 @@ test('T13524', normal, compile, [''])
test('T13509', normal, compile, [''])
test('T13526', normal, compile, [''])
test('T13603', normal, compile, [''])
test('T13333', normal, compile, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment