From d36ae5d6a448178e3db4736f6a4364e48ac7041b Mon Sep 17 00:00:00 2001 From: Simon Peyton Jones Date: Thu, 25 Jan 2018 09:57:01 +0000 Subject: [PATCH] Comments about CoercionHoles Richard was confused; I hope these comments help. --- compiler/typecheck/TcSimplify.hs | 11 +++---- compiler/types/TyCoRep.hs | 51 ++++++++++++++++++++++++-------- 2 files changed, 44 insertions(+), 18 deletions(-) diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs index 62a4800373..e0588ea914 100644 --- a/compiler/typecheck/TcSimplify.hs +++ b/compiler/typecheck/TcSimplify.hs @@ -2346,13 +2346,14 @@ The "bound variables of the implication" are 3. The binders of all evidence bindings in `ic_binds`. Example forall a. (d :: t1 ~ t2) EvBinds { (co :: t1 ~# t2) = superclass-sel d } - => [W] co : (a ~# b |> co) - Here `co` is gotten by superclass selection from `d`. + => [W] co2 : (a ~# b |> co) + Here `co` is gotten by superclass selection from `d`, and the + wanted constraint co2 must not float. - 4. And the evidence variable of any equality constraint whose type - mentions a bound variable. Example: + 4. And the evidence variable of any equality constraint (incl + Wanted ones) whose type mentions a bound variable. Example: forall k. [W] co1 :: t1 ~# t2 |> co2 - [W] co2 :: k ~# * + [W] co2 :: k ~# * Here, since `k` is bound, so is `co2` and hence so is `co1`. Here (1,2,3) are handled by the "seed_skols" calculation, and diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index d9cc42b6f2..588963d012 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -1214,6 +1214,8 @@ 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 + -- See Note [CoercionHoles and coercion free variables] + , ch_ref :: IORef (Maybe Coercion) } @@ -1254,7 +1256,7 @@ During typechecking, constraint solving for type classes works by For equality constraints we use a different strategy. See Note [The equality types story] in TysPrim for background on equality constraints. - - For boxed equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just + - For /boxed/ equality constraints, (t1 ~N t2) and (t1 ~R t2), it's just like type classes above. (Indeed, boxed equality constraints *are* classes.) - But for /unboxed/ equality constraints (t1 ~R# t2) and (t1 ~N# t2) we use a different plan @@ -1270,15 +1272,24 @@ For unboxed equalities: The main reason for all this is that there may be no good place to let-bind the evidence for unboxed equalities: - - We emit constraints for kind coercions, to be used - to cast a type's kind. These coercions then must be used in types. Because - they might appear in a top-level type, there is no place to bind these - (unlifted) coercions in the usual way. + + - We emit constraints for kind coercions, to be used to cast a + type's kind. These coercions then must be used in types. Because + they might appear in a top-level type, there is no place to bind + these (unlifted) coercions in the usual way. - A coercion for (forall a. t1) ~ (forall a. t2) will look like forall a. (coercion for t1~t2) - But the coercion for (t1~t2) may mention 'a', and we don't have let-bindings - within coercions. We could add them, but coercion holes are easier. + But the coercion for (t1~t2) may mention 'a', and we don't have + let-bindings within coercions. We could add them, but coercion + holes are easier. + + - Moreover, nothing is lost from the lack of let-bindings. For + dicionaries want to achieve sharing to avoid recomoputing the + dictionary. But coercions are entirely erased, so there's little + benefit to sharing. Indeed, even if we had a let-binding, we + always inline types and coercions at every use site and drop the + binding. Other notes about HoleCo: @@ -1289,14 +1300,26 @@ Other notes about HoleCo: type-checking vs forms that can appear in core proper, holes in Core will be ruled out. - * The Unique carried with a coercion hole is used solely for debugging. + * See Note [CoercionHoles and coercion free variables] + + * Coercion holes can be compared for equality like other coercions: + by looking at the types coerced. + + +Note [CoercionHoles and coercion free variables] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Why does a CoercionHole contain a CoVar, as well as reference to +fill in? Because we want to treat that CoVar as a free variable of +the coercion. See Trac #14584, and Note [What prevents a +constraint from floating] in TcSimplify, item (4): + + forall k. [W] co1 :: t1 ~# t2 |> co2 + [W] co2 :: k ~# * - * Coercion holes can be compared for equality only like other coercions: - only by looking at the types coerced. +Here co2 is a CoercionHole. But we /must/ know that it is free in +co1, because that's all that stops it floating outside the +implication. - * We don't use holes for other evidence because other evidence wants to - be /shared/. But coercions are entirely erased, so there's little - benefit to sharing. Note [ProofIrrelProv] ~~~~~~~~~~~~~~~~~~~~~ @@ -1461,6 +1484,7 @@ tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc = tyCoFVsOfCoVar v fv_cand in_scope acc tyCoFVsOfCo (HoleCo h) fv_cand in_scope acc = tyCoFVsOfCoVar (coHoleCoVar h) fv_cand in_scope acc + -- See Note [CoercionHoles and coercion free variables] tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc = (tyCoFVsOfProv p `unionFV` tyCoFVsOfType t1 @@ -1525,6 +1549,7 @@ coVarsOfCo (ForAllCo tv kind_co co) coVarsOfCo (FunCo _ co1 co2) = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2 coVarsOfCo (CoVarCo v) = coVarsOfCoVar v coVarsOfCo (HoleCo h) = coVarsOfCoVar (coHoleCoVar h) + -- See Note [CoercionHoles and coercion free variables] coVarsOfCo (AxiomInstCo _ _ as) = coVarsOfCos as coVarsOfCo (UnivCo p _ t1 t2) = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2] coVarsOfCo (SymCo co) = coVarsOfCo co -- GitLab