I've created this wiki page to track my learning/research as I try to improve my feature request that I made in the comments of #15009.

# 20181125 -- wanted on the RHS

- We should not float
`w :: alpha[L] ~ <RHS>`

if the RHS contains a type family application that in turn contains a metavar of a level greater than L. To float`w`

, we'd first promote all RHS metavars to level L. But since they are arguments of a type family, we should not promote them prematurely: it's possible the type family could later reduce in a way that ignores/eliminates those metavars.- (TODO I don't think the existing GHC code checks for this. Should it?)

- The
`inert_eqs`

field of the GHC internal data structure contains the`CTyEqCan`

constraints of an inert set. That's where we'd find the candidates for floating and it's also where we'd find the given equalities we'd need to check. There are other fields of that data structure that we'd require to not have any givens, before floating anything. - I'd summarize the idea as "We can float an
`CTyEqCan`

constraint from level K if:- its LHS is a metavar of level L,
- its RHS has no skolems of any level greater than L,
- its RHS has no type family applications containing metavars with level greater than L,
- the domain of the substitution induced by the givens in
`inert_eqs`

at levels greater than L does not contain a skolem with level <= L, and - that same substitution domain is immutable (e.g. no metavars, no fsks, no potential for additional equalities)."

- Note that that last conjunct depends on givens from levels less than or equal L, b/c if they were to mutate, they might interact with givens greater than L and create new such given equalities.

# 20181105 -- revises 20181104

Two things occurred after I slept on it. Both relate to Example 6 from the 20181104 entry below about CTyEqCans possibly flipping to reveal a new LHS.

- Rule 20181104 also needs to inspect the givens at level L and shallower. It's a slightly weaker predicate (implied by P[L] but not vice versa): we need to make sure none of them will flip.

- If I correctly understand what the "inert substitution" is, then I think I can summarize the (corrected) Rule 20181104 as follows. Let dis[i] be the domain of the inert substitution active in the wanteds of TcLevel i. We can safely float a wanted CTyEqCan
`w : alpha[L] ~ <t>`

from level K to level L if dis[K] can never change (which implies dis[L] can never change -- ie no CTyEqCan might flip) and if dis[K] - dis[L] does not include any metavars, any flattening skolems, or any skolems of level <= L.

# 20181104 -- first draft proposal

(I think this day's entry is self-contained.)

My core hypothesis is that levels can help us determine if a wanted equality `w`

can be floated out from under a set `gs`

of given constraints without thereby losing access to some possible solutions of `w`

(those involving at least one `g`

in `gs`

). Currently, GHC is quite conservative and does not float `w`

if it's possible that one of the givens might be an equality. With more effort, it should be possible to determine that particular givens are not relevant to a particular wanted equality, and that's what I'm exploring. I'm specifically focused on skolems with a greater `TcLevel`

, which arise from `RankNTypes`

.

Notation: single character tyvars are skolems (i.e. bound by some `forall`

), greek tyvars are metavars (i.e. unification variables or "taus"), `fsk0`

`fsk1`

and so on are flattening skolems. I haven't even begun considerings flattening meta vars, but they would be `fmv0`

`fmv1`

and so on. I write the `TcLevel`

of a metavar as a suffix in brackets on at least one of its occurrences, e.g. `alpha[2]`

. I'll only do that for skolems if I'm not showing their binding `forall`

, which is where I prefer to put the level. (This all seems pretty standard for discussions on Trac at least.)

### Example 1 - the motivator

Is `g`

relevant to `w`

?

forall[2] x. () => forall[3] (g : x ~ Int) => (w :: alpha[1] ~ Int)

GHC 8.6 conservatively concludes "Yes", just because `g`

is an equality. But `g`

is indeed not relevant to `w`

: allowing the use of `g`

does not increase the set of possible solutions of `w`

. The intuitive explanation is that `x`

does not occur in `w`

's type and cannot be introduced into it when we learn new things. As an example of "learning a new thing", consider if some other constraint somewhere else in the scope of `alpha`

causes the solver to assign `alpha := a[1]`

. Because of that assignment, GHC would replace `alpha`

by `a[1]`

thereby introducing `a`

as a new free variable of `w`

's type. The fundamental insight is that `x`

cannot be introduced that way, because `x`

is level 2 while `alpha`

is level 1, so it'd be a skolem-escape bug if `alpha`

were assigned to something with `x`

free.

Remark. The "elsewhere" constraints that assigned

`alpha := a[1]`

in that example aren't typically shown or even mentioned: we just assume that any metavar can be replaced at any time by any type whose free variables exclude the metavar and do not have a level greater than that of the metavar.

Thus, we could actually soundly float `w`

all the way to level 1, and once it's there, GHC could solve `w`

by unification, assigning `alpha := Int`

and then discharging `w`

by reflexivity. (GHC can't do that here at level 3, because a metavar is "untouchable" at any level but its own, and `alpha`

is level 1. See `jfp-outsidein.pdf`

for the motivation of that rule, which is the whole reason we need to be able to float some equalities in the first place!)

### Example 2

This example is just the previous one with the skolems' levels reduced by one.

forall[1] x. () => forall[2] (g : x ~ Int) => (w :: alpha[1] ~ Int)

This time `g`

actually might be relevant to `w`

, so we should not float. Though `x`

is not in the type of `w`

at the moment, it could be later, because now that `x`

's level is not greater than `alpha`

's, `alpha`

might be assigned to a type involving `x`

, and making that subtitution into `w`

would result in a wanted constraint that could (clearly would, in this example) require `g`

in order to be solved.

### Example 3 - metavars

The givens are not limited to skolems. What if we take Example 1 (which could safely float) and make the tyvar in `g`

a metavar instead?

forall[2] x. () => forall[3] (g : beta[2] ~ Int) => (w :: alpha[1] ~ Int)

We should not float. For example, both metavars might reduce to the same level 1 skolem variable, in which case `w := g`

might be the only possible solution.

The relation of the metavars' levels does not matter.

### Example 4 - flattening skolems

Type family applications have similar consequences as metavars.

forall[2] x. () => forall[3] (g1 : F ~ fsk, g2 : fsk ~ Int) => (w : alpha[1] ~ Int)

Again, we should not float past `g2`

. For example, we might learn `alpha := F`

.

What if the application has tyvars with greater levels?

forall[2] x. () => forall[3] (g1 : G x ~ fsk, g2 : fsk ~ Int) => (w : alpha[1] ~ Int)

It is tempting to conclude that we could safely float: `alpha[1]`

can't become `G x`

because `x`

is level 2. But! An example in `jfp-outsidein.pdf`

motivates the "open world assumption," which in this case means we should assume that we could "learn" a new top-level `G`

axiom at any time (e.g. orphan instances). And if that axiom were `G _ := F`

, we shouldn't float for exactly the same reasoning as above.

In general, the "flattening constraint" (i.e. `CFunEqCan`

) `g1`

should not itself prevent floating; the following would be safe to float.

forall[2] x. () => forall[3] (g1 : G x ~ fsk) => (w : alpha[1] ~ Int)

### Example 5 - "level inversion"

Some givens make me question my reliance on levels.

forall[1] x. () => forall[2] y. (gx : x ~ Maybe y) => forall[3]. (gy : y ~ Int) => (w : alpha[1] ~ Maybe Int

`gx`

is an interesting given equality because as a rewrite rule it replaces a level 1 variable with a type with free variable of level 2! Our reasoning in the above examples has relied on the fact that a metavar of level 1 could not become a type with a free variable whose level was greater than 1. But here, if `alpha := x`

, then next `gx`

rewrites that `x`

to `Maybe y`

, and so transitively `alpha`

has become `Maybe y`

. Disaster?

I think I have a simple answer to a tricky question: Is it safe to float `w`

out from under `gy`

? If we were to ignore `gx`

, the answer would be simple: yes, because `alpha`

is level 1 and `y`

is level 2. But with `gx`

and its "level inversion" of `x`

, we instead should not float: `gy`

might be relevant to `w`

, regardless of levels because `gx`

confuses them.

The simplifying observation is that floating `w`

is ultimately only helpful if we can float it all that way to `alpha`

's level, level 1. And to do so, we'd have to float `w`

past `gx`

itself. That'd clearly be unsound by our usual reasoning: `x`

is the same level as `alpha`

.

But what if `w`

isn't trying to float past `gx`

, only past `gy`

? That would mean either `alpha`

has a higher-level or `gx`

has a lesser level than in the example we just considered. In general, we have the following.

forall[A] x. () => ... forall[B] (gx : x ~ Maybe y) => ... forall[C]. (gy : y ~ Int) => (w : alpha[L] ~ Maybe Int

If L < B then `gx`

itself will stop `w`

. If B <= L, then `y`

is of a level <= B (else it's out of scope), hence <= L, and so `gy`

will stop `w`

regardless of `gx`

.

The lesson is that we need not work out how a level inverting constraint like `gx`

affects other givens in its scope, we can judge all givens individually. We might judge some incorrectly (`gy`

), but only if those farther out (`gx`

) will render that judgement irrelevant. Thus we should not float a constraint at all unless we can float it all the way to its final destination. (Maybe we should just perform the unification instead of floating it? Otherwise, what if we learn something "risky" after having floated only half way to our destination? This might just be a matter of error message quality.)

The way `gx`

and `gy`

interact here corresponds to the `EQDIFF`

given-given interaction rule in `jfp-outsidein.pdf`

. GHC doesn't implement that rule as written; it does not add a third constraint `gx_gy : x ~ Maybe Int`

alongside `gy`

. If it did, then `gx_gy`

would be enough to prevent floating `w`

.

### Example 6 - ignore CTyEqCan RHS unless it's a fsk

We assume the variable on the LHS is a skolem, otherwise previous examples apply.

Does the RHS of the given equality matter?

forall[M] x. ... => ... forall ... . (g : x ~ <RHS>) => (w : alpha[L] ~ Int)

GHC uses CTyEqCan constraints as left-to-right rewrite rules, so the RHS `<RHS>`

does not affect `w`

unless `x`

first becomes free in `w`

's type. If M < L, that can't happen and we float `w`

-- that's the basic reasoning from Example 1. Note that `<RHS>`

wasn't a concern. If M >= L, then `g`

prevents floating `w`

as-is, so `<RHS>`

again didn't matter.

That line of reasoning overlooks two important possibilities.

- The
`EQSAME`

given-given interaction from`jfp-outsidein.pdf`

: two CTyEqCans with the same LHS will induce a new equality between their RHSs.

- If
`<RHS>`

is a flattening skolem (i.e. a type family application), then it might reduce in such a way that causes the CTyEqCan to flip over, giving it a new LHS.

TODO Demonstrate that flipping is the only possibility (i.e. `x`

is atomic and immutable, so it will remain one side of the equality).

TODO I'm currently under the impression that fmvs cannot occur in a given CTyEqCan, so I'm not considering them.

If it weren't for the mutability issue, we could address the `EQSAME`

issue by withholding our judgement until all the givens are inert. Unlike `EQDIFF`

, GHC implements `EQSAME`

as written, by creating a new constraint. We'll wait until the givens are inert so we can simply judge any induced equalities instead of trying to anticipate the `EQSAME`

interactions and their possible cascades.

However, an inert set of CTyEqCans might not be inert after one of their LHSs changes, so the mutability issue subverts our planned reliance on inertness.

💫 😵 💫

I'm getting dizzy. Let's zoom back out. Our basic rule is: float `w`

past `g`

if `M < L`

and do not otherwise. So if we float, and then the LHS of `g`

somehow becomes a tyvar with a level >= L, we might have thus lost a possible solution to `w`

.

It seems too complicated to try to determine if `EQSAME`

interactions can or cannot lead to that happening, so I'm going to opt for a conservative heuristic and refuse to judge a float if there's a risk of losing inertness. Specifically, I will withhold judgment until we're certain that no new `EQSAME`

interactions can arise.

So I'm going to focus on the case where the RHS is a flattening skolem, because that's only way that the LHS might change, thereby invalidating a premature float judgment and/or enabling further `EQSAME`

interactions.

TODO Demonstrate that no other RHS threatens the LHS. DRAFT "A metavar of level N can only become a tyvar of level <= N, which wouldn't change the orientation of `g`

. (Even a level inverting given like `gx`

from the above example would only allow a metavar to become a type headed by a constructor -- the easy first case of this example.) So we can ignore the RHS if it's a metavar."

So how does `g : x[M] ~ fsk0`

with `x`

an inert skolem become `g' : tv[N] ~ x`

? In general, a type family application `F <t1> <t2> ...`

can reduce to a tyvar `tv`

only if that tyvar is a free variable of one of its arguments. If `fsk0`

reduces to a flattening skolem `fsk1`

, we'll end up back in this same analysis case, and so recur. If it reduces to a metavar or skolem, then GHC will flip the equality only if N >= M (skolems of the same level are resolved by their syntactic names; seems fragile to rely on that, so let's not.) -- see `TcUnify.Note [TyVar/TyVar orientation]`

.

Thus, the RHS should prevent floating only if it is a flattening skolem whose definition's free non-flattening variables (recurring on free flattening skolems) include a variable with a level N >= M. If such a free var exists, then the equality might flip, which might enable more `EQSAME`

interactions, which we do not attempt to anticipate, choosing the simpler pessimism. Even if a new `EQSAME`

interaction didn't happen, the level of the LHS has increased, and so a former decision to float might now be revealed as premature; if we some how knew `EQSAME`

interactions were not a risk, we could strengthen the predicate to `N >= L`

: let it flip as long as it still wouldn't prevent `w`

from floating.

### Rule for Consideration

After working through the above examples, I'm considering the following rule. The basic shape is informed by Example 5.

Rule 20181104. Float a (canonical) wanted

`w : alpha[L] ~ <t>`

from level K > L to level L if all the constraints given by the levels from L+1 to K (inclusive) are inert and each satifies P[L], wherenonflat_fvs t = the free variables of the type t, recurring on fsks instead of including them -- P[L] g iff g is not relevant to any wanted CTyEqCan if its LHS is a metavar whose level is <= L P[-] : TcLevel -> GivenConstraint -> Bool P[L] CDictCan g = forall sc in superclass-constraints(g). P[L] sc P[L] CFunEqCan _ ~ fsk = True P[L] CTyEqCan alpha ~ _ = False -- see Example 3 P[L] CTyEqCan fsk ~ _ = False -- see Example 4 P[L] CTyEqCan x[M] ~ fsk = L < M && forall v[N] in nonflat_fvs(fsk). N < M -- see Example 6 P[L] CTyEqCan x[M] ~ _ = L < M P[L] g = False -- it could reduce to a CTyEqCan fsk ~ _ or any fv could become the LHS, thereby unlocked EQSAME interactionsand

`nonflat_fvs(<t>)`

doesn't have any skolems with level > L.

TODO Any other restrictions on `<t>`

?

Edit: The givens shallower than L also matter; see the top-level 20181105 section above.

# 20181014 -- work in progress

Just using small examples today, no reference to earlier days -- kind of a fresh start.

### Example 1

forall[2] x. (gx : x ~ Int) => (w : alpha[tau:1] ~ Int)

`Note [Let-bound skolems]`

applies here: it is safe to float `w`

past `gx`

, regardless of skolems and givens outside the scope of `x`

.

Note that a more general `w : <W>`

can only float after being simplified by `gx`

, otherwise the skolem `x`

would escape!

### Example 2

forall[2] x. () => forall[3]. (gx : x ~ Int) => (w : alpha[tau:1] ~ Int)

In this case, I think it is also safe to float `w`

past `gx`

, even though `Note [Let-bound skolems]`

doesn't apply. This kind of example motivates my investigation here.

### Example 3

forall[2] x. () => ( (u : <U>) , forall[3]. (gx : x ~ Int) => (w : alpha[tau:2] ~ Int) )

In this case, it *NOT* safe to float `w`

past `gx`

. Simplification of `u`

might assign `alpha := x`

, in which case `gx`

may be required in order to solve `w`

. If that assignment happened after the float, we'd be stuck.

### Example 4

forall[2] x. (gx : x ~ Int) => ( (u : <U>) , (w : alpha[tau:2] ~ Int) )

`Note [Let-bound skolems]`

still applies, and it's safe to float `w`

! (GHC 8.6 does.) This is because *all* occurrences of `x`

, even those in `<U>`

, will have been eliminated by `gx`

, and so no problematic assignment can take place after the float. `x`

is a dead-binder once `gx`

has been applied within the scope that it shares with `x`

.

I will no longer explicitly write the "elsewhere" constraint `u`

; I will instead simply assume that any unification variable `alpha[tau:i]`

where `i > 0`

can rewrite to any type whose free variables' levels are all `<= i`

. (Level `0`

is reserved for flattening variables, and I anticipate I'll have to treat those somewhat differently.)

Note that Examples 3-4 with `u`

left implicit are the same as Examples 1-2 with `alpha`

's level increased from 1 to 2.

### Example 5

forall[1] x. () => forall[2] y. (gx : x ~ T y) => forall[3]. (gy : y ~ Int) => (w : alpha[tau:1] ~ T Int)

`w`

should not float past `gy`

. If we decide elsewhere that `alpha := x`

, then `w`

can only be solved via a combination of `gx`

and `gy`

.

The line of reasoning is:

- The type of
`w`

has`alpha`

free, by observation. `alpha`

can rewrite to something with`x`

free, by our heuristic regarding unification variable levels.`x`

can rewrite to something with`y`

free, by`gx`

.- The type of
`w`

can rewrite to something with`y`

free, by transitivity. - Thus, floating
`w`

out from under`gy`

could ultimately cause an avoidable type error.

Note that contrary to the given-given interaction rules in `jpf-outsidein.pdf`

, GHC does not interact `gx`

and `gy`

to create a new given `x ~ T Int`

(presumably at level 3). So we have to explicitly guard against this transitive scenario. (For example, inspect the `-ddump-tc-trace`

for `f :: (x :~: [y]) -> (y :~: Int) -> x -> c; f Refl Refl = id`

; it seems like the transitivity is actually "handled" during flattening.)

I found intermediate conclusion within that line of reasoning that `alpha[tau:1]`

can rewrite to something with `y[sk:2]`

free to be counter-intuitive because that rewriting _increases_ the maximum level of the source term's free type variables. This increase originates in the otherwise completely typical `gx : x[sk:1] ~ T y[sk:2]`

CTyEqCan.

### Refinement of Example 5

I see a much simpler argument against floating here.

`w`

would have to float past both`gy`

*and also*`gx`

for its`alpha`

to become touchable.`w`

manifestly cannot pass`gx`

.- Thus, do not float
`w`

at all.

If we consider an example with `alpha`

's level increased to `2`

so that it would not need to pass `gx`

, then it manifestly cannot pass `gy`

.

So maybe an inherited attributed along the lines of "the lowest level tyvar with a CTyEqCan in the outer givens between level 1 and here is 1" would be enough to know that `w`

cannot float all the way to its target level (`1`

, the level of its LHS `alpha`

) and so should not float at all.

### Example 6

This case is simpler than it looks at first.

forall[1] x. () => forall[2] y. () => forall[3]. (gy1 : y ~ T x) => forall[4]. (gy2 : y ~ T Int) => (w : alpha[tau:1] ~ T Int)

The subtlety is that those givens are actually not inert; GHC will interact `gy1`

and `gy2`

to create a constraint at level 4 `x ~ T Int`

, according to the `EQSAME`

rule from `jfp-outsidein.pdf`

(somewhat in contrast to Example 5, where `EQDIFF`

is apparently not directly implemented in GHC).

forall[1] x. () => forall[2] y. () => forall[3]. (gy1 : y ~ T x) => forall[4]. (gx : x ~ Int) => -- evidence binding gx from gy1 and gy2 interacting (w : alpha[tau:1] ~ T Int)

Now it's clear `w`

should not float, because of the new `gx`

--- it's quite similar to Example 5 now.

### Example 7

Similar to the previous example, this set is not yet inert.

forall[1] x. () => forall[2]. (gx : x ~ Int) => (w : alpha[tau:1] ~ x)

`gx`

can simplify `w`

, which yields Example 3, essentially.

### Example 8

Unification variables can occur in givens.

forall[1]. () => forall[2]. (gbeta : beta[tau:1] ~ Int) => -- beta must be < level 2, according to (GivenInv) of TcType.Note [TcLevel and untouchable type variables] (w : alpha[tau:1] ~ Int)

`w`

should not float past `gbeta`

, since we might elsewhere decide that `beta := alpha`

or `alpha := beta`

.

Even if `alpha`

were of a greater level

forall[2]. () => forall[3]. (gbeta : beta[tau:1] ~ Int) => (w : alpha[tau:2] ~ Int)

the assignment {{{alpha := beta}} is still possible.

### Example 9

This is my actual original motivation.

forall[2] x y. () => forall[3]. ( (g1 : x ~ alpha[tau:1]) , (g2 : y ~ beta[tau:1]) ) => ( (w1 : alpha[tau:1] ~ Int) , (w2 : beta[tau:1] ~ Int) )

I think they should both float.

The remaining examples will explore variations of this. I'll leave out `g2`

and `w2`

when possible.

forall[2] x. () => forall[3]. (g : x ~ alpha[tau:1]) => (w : alpha[tau:1] ~ Int)

### Example 10

`TcUnify.Note [TyVar/TyVar orientation]`

specifies that `x[sk:i] ~ alpha[sk:i]`

should be swapped to `alpha[sk:i] ~ x[sk:i]`

.

forall[2] x. () => forall[3]. (g : alpha[tau:2] ~ x) => (w : x ~ Int)

GHC won't consider floating that, because `w`

is not of the form `alpha[tau:_] ~ <T>`

.

I definitely don't have enough context to seriously challenge the current swap decision procedure. But, if we didn't reorient, then I don't see why `w`

shouldn't float...

forall[2] x. () => forall[3]. (g : x ~ alpha[tau:2]) => -- hypothetically ignoring current swap decision procedure (w : alpha[tau:2] ~ Int)

### Example 11

Of course, occurrences of skolems on the righthand-side of `w`

should prevent floating past their binder.

forall[2] x. () => forall[3] y. (g : x ~ alpha[tau:1]) => (w : alpha[tau:1] ~ Maybe y) -- Decide no float, since 1 < maximum (map level (fvs (Maybe y)))

### Example 12

I don't understand irreducible constraints terribly well, so I'll just treat them all conservatively for now by refining the inherited attribute.

forall[2] x. () => forall[3]. beta[tau:1] => forall[4] y. (g : x ~ alpha[tau:1]) => (w : alpha[tau:1] ~ y)

The inherited attribute is a vector, one for each parent implication, in which each vector component is the level of the lowest level tyvar on the LHS of a CTyEqCan or that occurs free in an irreducible constraint.

Maybe insoluble constraints just set the vector component to `0`

, thereby preventing floating past them?

forall[2] x. () => -- vec [Inf,Inf,Inf] (i.e. levels 2,1,0) forall[3]. beta[tau:1] => -- vec [1,1,1,1] forall[4] y. (g : x ~ alpha[tau:1]) => -- vec [2,1,1,1,1] (i.e. levels 4,3,2,1,0) (w : alpha[tau:1] ~ y) -- Decide no float, since 1 >= vec !! (4-1).

### Conclusion

TODO ... I haven't yet thought of anything clever that isn't caught by the inherited attribute test I proposed in the discussion of Example 5, even with type family applications and/or constraint kinds.

# 20181013 -- narrowing

This section distills the narrative of the 20181008 section into narrower observations and questions.

My current goal is a "simple enough", algorithm that could conservatively decide whether it is safe to float `w : alpha[tau:k] ~ <R>`

out from under `g : x[sk:i] ~ <X>`

where `k < i`

and `alpha`

might occur free in `<X>`

. Informally, it's only safe to do so if the eventual right-hand side of `w`

will definitely not (transitively) depend on `g`

.

A wanted `w : <W>`

can gain `x[_:i]`

as a free variable in two ways.

- WAY1 A uvar
`alpha[tau:j]`

that occurs in`<W>`

could be assigned a type`alpha := <T>`

where`x`

occurs free in`<T>`

, which would require`j >= i`

. - WAY2
`w`

could be simplified by a given CTyEqCan`g : y ~ <T>`

where`x`

occurs free in`<T>`

.

WAY1 cannot increase the maximum level of the free variables in `<W>`

. In contrast, WAY2 can: consider `g : y[_:2] ~ Maybe x[sk:3]`

.

Within one subtree of a binding group's entire forest of implication trees, we must assume that a uvar `alpha[tau:j]`

could be assigned a type `<T>`

in which any variable of level `<= j`

other than `alpha`

itself could occur free.

The reduction of a type family application `F <X>`

cannot introduce new free type variables beyond those already free in `<X>`

-- except for variables that arise from flattening the type family applications possibly introduced by the reduction. But it might remove some free variables.

An assignment to a uvar `alpha[tau:j]`

that occurs in the givens could directly or indirectly (via enabled given-given interactions) yield the given `g`

of WAY2.

# 20181008 -- first notes, learning a lot

I've found a useful perspective on this. Consider this implication tree.

forall[3] y. () => ( (u : <U>) , forall[4]. (g : y ~ <Y>) => (w1 : <W1>) )

The naive intuition is

We can float

`w1`

out from under`g`

if`y`

doesn't occur (free) in`<W1>`

.

In fact, according to the jfp-outsidein.pdf "Simplification Rules", `g`

will eventually simplify `w1`

into some `w2 : <W2>`

such that `y`

does not occur in `<W2>`

.

The subtlety, however, is that `y`

might occur in `<U>`

and therefore the solving of `u`

may assign a u(nification)var(iable) `alpha[tau:i]`

where `i >= 3`

to some type in which `y`

occurs; if `alpha`

occurs in `<W2>`

, then now `<W2>`

suddenly has an occurrence of `y`

again!

This example demonstrates:

forall[3] y. () => ( (u : alpha[3] ~ y) , forall[4]. (g : y ~ Int) => (w1 : alpha[3] ~ y) ) -- use g to simplify w1 --> forall[3] y. () => ( (u : alpha[3] ~ y) , forall[4]. (g : y ~ Int) => (w2 : alpha[3] ~ Int) ) -- float w2, since y does not occur in its type --> forall[3] y. () => ( (w3 : alpha[3] ~ Int) , (u : alpha[3] ~ y) , forall[4]. (g : y ~ Int) => () ) -- solve u, by alpha[3] := y --> forall[3] y. () => ( (w3 : y ~ Int) , forall[4]. (g : y ~ Int) => () ) -- Stuck because we floated!

### Comparison to status quo

Compare this to the case where `Note [Let-bound skolems]`

applies.

forall[3] y. (g : y ~ <Y>) => (w1 : <W1>)

There is no `u : <U>`

that might assign to a uvar `alpha`

shared with `<W1>`

here, so the failure mode describe above can't happen. If we add a `u`

alongside `w1`

,

forall[3] y. (g : y ~ <Y>) => ( (w1 : <W1>) , (u : <U>) )

then now it's possible solving `u`

could assign `alpha[tau:3] := ...y...`

. However, as part of floating `w1`

, we immediately promote any uvars that occur in it, so the problematic `alpha[tau:3]`

would be assigned `alpha[tau:3] := alpha[tau:2]`

, which cannot be assigned `alpha[tau:2] := ...y...`

since `y`

is `[sk:3]`

(and also `alpha[tau:2]`

is untouchable in `u[3]`

).

This silly example demonstrates:

forall[3] y. (g : y ~ Int) => (w1 : alpha[3] ~ y,u : alpha[3] ~ y) -- use g to simplify w1 --> forall[3] y. (g : y ~ Int) => (w2 : alpha[3] ~ Int,u : alpha[3] ~ y) -- float w2, since y does not occur in its type (NB the promotion of alpha 3 to 2) --> (w3 : alpha[2] ~ Int) forall[3] y. (g : y ~ Int) => (u : alpha[2] ~ y) -- Cannot solve u as in previous example, because alpha is now untouchable in u. -- solve w3, by alpha[2] := Int --> forall[3] y. (g : y ~ Int) => (u : Int ~ y) -- re-orient, reflexivity --> -- Solved!

### Refinement for Assignment

So we can refine the rule for

forall[3] y. () => ( (u : <U>) , forall[4]. (g : y ~ <Y>) => (w1 : <W1>) )

from

We can float

`w1`

out from under`g`

if`y`

does not occur in`<W1>`

.

to

We can float

`w1`

out from under`g`

if`y`

does notand can never againoccur in`<W1>`

.

How do we decide that much stronger predicate? There are a few options (e.g. there is no sibling `u`

wanted), but I currently favor checking that no uvar in `<W1>`

has a level `>= 3`

(this check should inspect the RHS of any flattening vars that occur in `<W1>`

). That prohibits the problematic reintroduction of `y`

via uvar assignment after floating.

Thus:

We can float

`w1`

out from under`g`

if`y`

does not occur in`<W1>`

and all unification variables in.`<W1>`

have level`< 3`

After I thought about this for a bit, I realized there might be another way for `y`

to be reintroduced into `<W1>`

in the more general case where that outer implication has givens.

forall[3] y. (o : <O>) => forall[4]. (g : y ~ <Y>) => (w1 : <W1>)

If it's something like `o : x[sk:2] ~ Maybe y`

, and `x`

occurs in `<W1>`

, then simplifying via `g`

and floating `w1`

and then simplifying it via `o`

might reintroduce `y`

.

### Refinement for Outer Givens (a wrong turn)

So we can generalize the rule for

forall[3] y. (o : <O>) => ( (u : <U>) , forall[4]. (g : y ~ <Y>) => (w1 : <W1>) )

by refining from

We can float

`w1`

out from under`g`

if`y`

does not occur in`<W1>`

and all unification variables in`<W1>`

have level`< 3`

.

to

We can float

`w1`

out from under`g`

ifall givens are inertand`y`

does not occur in`<W1>`

and all unification variables in`<W1>`

have level`< 3`

.

If I understand the jfp-outsidein.pdf "Interaction Rules", `o : x[sk:2] ~ Maybe y`

and `g`

ought to interact to yield something like

forall[3] y. (o : x[sk:2] ~ Maybe y) => ( (u : <U>) , forall[4]. ( (g : y ~ <Y>) , (g2 : x[sk:2] ~ Maybe <Y>) ) => (w1 : <W1>) )

Now that givens are inert, our rule will force `g`

and `g2`

to eliminate the skolems and assess uvars (level `< 2`

now) in `w1`

before floating it.

NOPE, the above is not how `g`

and `o`

"interact". I searched `TcInteract`

for something like `EQDIFF`

, but I ended up at

| isGiven ev -- See Note [Touchables and givens] = continueWith workItem

That Note hasn't existed since

commit 27310213397bb89555bb03585e057ba1b017e895 Author: simonpj@microsoft.com <unknown> Date: Wed Jan 12 14:56:04 2011 +0000 Major refactoring of the type inference engine

I don't see what touchables has to do with line 1630. /shrug

So I whipped up a test

f :: (x :~: [y]) -> (y :~: Int) -> x -> c f Refl Refl = id

which never gets further than

Implic { TcLevel = 2 Skolems = No-eqs = False Status = Unsolved Given = co_a1bQ :: [y_a1bM[sk:1]] GHC.Prim.~# x_a1bL[sk:1] Wanted = WC {wc_impl = Implic { TcLevel = 3 Skolems = No-eqs = False Status = Unsolved Given = co_a1bR :: Int GHC.Prim.~# y_a1bM[sk:1] Wanted = WC {wc_simple = [WD] hole{co_a1c2} {2}:: c_a1bN[sk:1] GHC.Prim.~# [Int] (CNonCanonical)} Binds = EvBindsVar<a1bV> a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in an equation for `f_a1bO' }} Binds = EvBindsVar<a1bW> a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in an equation for `f_a1bO' }

and even explicitly says

Inerts: {Equalities: [G] co_a1bZ {1}:: x_a1bL[sk:1] GHC.Prim.~# [y_a1bM[sk:1]] (CTyEqCan) [G] co_a1c0 {1}:: y_a1bM[sk:1] GHC.Prim.~# Int (CTyEqCan) Unsolved goals = 0}

Note that `co_a1bZ`

and `co_a1c0`

never "interacted" as `EQDIFF`

suggests they should. However, they both rewrote the wanted. (In fact, it's unflattening that seems to do this, even though there are no type families involved! See the definition of `flatten_tyvar2`

.)

### Comparison to status quo

`Note [Let-bound skolems]`

need not worry about outer givens because `y`

is not in scope outside of this implication.

### Refinement for Outer Givens with Interactions (a turn too far)

So we'll need a different refinement to ensure that `y`

cannot be reintroduced by an outer given.

In our `o : x[sk:2] ~ Maybe y`

example, `x`

has a significant relationship with `y`

: any occurrence of `x`

in the scope of `o`

will be rewritten to have an occurrence of `y`

instead. Loosely, "`x`

can become `y`

".

Similarly, any uvar `alpha[tau:i]`

where i `>= 3`

"can become `y`

" due to solving other parts of the implication tree. So the "can become" relation is a nice commonality between the two failure modes I've considered.

How might we determine if "`x`

can become `y`

" in general? Here's another failure, also based on the "`x`

can become `y`

" idea, but with more moving parts.

forall[3] y. ( (o1 : z[sk:2] ~ T x[sk:2] ) , (o2 : alpha[tau:2] ~ T (Maybe y)) ) => ( (u : <U>) , forall[4]. ( (g : y ~ <Y>) , (g2 : x[sk:2] ~ Maybe <Y>) ) => (w1 : <W1>) )

Note that the equalities `o1`

and `o2`

contain `x`

and `y`

respectively, but do not have any shared variables. However, solving another part of the implication tree might assign `alpha := z`

, in which case `o1`

and `o2`

will interact, yielding a constraint that then canonicalizes to the familiar `o : x ~ Maybe y`

. This is actually the same lesson as in the first failure mode "`alpha[tau:i]`

can become any variable at level `<= i`

", but in the givens this time and one step removed from affecting our float.

Our second refinement makes

We can float

`w1`

out from under`g`

if`y`

does not and can never again occur in`<W1>`

.

more formal as

We can float

`w1`

out from under`g`

if the transitive closure of the "can step to" relation does not relate any free variable of`<W1>`

to`y`

.

which we can shorten to

We can float

`w1`

out from under`g`

if no free variable of`<W1>`

"can become"`y`

.

by defining the following (over-estimating) properties.

- CB1 "can become" includes the transitive closure of "can step to"
- CS1
`x`

(any flavor and level) can step to itself - CS2
`alpha[tau:i]`

can step to any variable at level`<= i`

- CS3
`x`

(any flavor and level) can step to any free variable of`<X>`

, given CTyEqCan`x ~ <X>`

- CS4 Any free variable of
`<A>`

can step to any free variable of`<B>`

or vice versa, given a non-CTyEqCan equality`<A> ~ <B>`

That's enough to catch the `o : x[sk:2] ~ Maybe y`

failure. But it's not enough for the `o1`

and `o2`

failure that involved the interaction after assignment. So we must further extend "can become".

- CB2 Any free variable of
`<A>`

can become any free variable of`D`

or vice versa if a free variable of`<B>`

can become a free variable of`<C>`

or vice versa, given`<A> ~ <B>`

and`<C> ~ <D>`

(or either/both of their symmetries)

(Could there be less symmetric special cases of `CB2`

for CTyEqCans-like things?)

Let "can become" be the smallest relation satisfying all the CB* properties.

... That seems simultaneously too complicated and also too conservative. So maybe we should start with relatively simple and therefore acceptably too conservative.

### Another Refinement for Outer Givens with Interactions (a turn too far in the other direction?)

This seems reasonably balanced for starters.

forall[3] y. theta => ( (u : <U>) , forall[4]. (g : y ~ <Y>) => (w1 : <W1>) )

We can float

`w1`

out from under`g`

if no free variable of`<W1>`

"can become"`y`

.

- CB1 "can become" includes the transitive closure of "can step to"
- CS1
`x`

(any flavor and level) can step to itself - CS2
`alpha[tau:i]`

can step to any variable at level`<= i`

- CS3
`x`

(any flavor and level) can step to any free variable of`<X>`

, given CTyEqCan`x ~ <X>`

- CS4 Any free variable of
`<A>`

can step to any free variable of`<B>`

or vice versa, given a non-CTyEqCan equality`<A> ~ <B>`

- CS5 Any free variable of the possible equalities in
`theta`

can step to any other and to any variable of level`<= i`

, if there is a uvar of level`i`

in`theta`

Let "can become" be the smallest relation satisfying CB1.

### Yet Another Refinement for Outer Givens with Interactions (are we going in circles?)

TODO I'm currently thinking about about what to do if `g`

has siblings. I suspect CS5 should consider those too. Should it also consider `g`

?

My current goal is for `w : alpha[tau:1] ~ Int`

to float out from under `g : x[sk:2] ~ alpha[tau:1]`

. Thus CS5 is likely disappointingly conservative if it includes siblings:

forall[3] x y. () => ( (u : <U>) , forall[4]. ( (g1 : x ~ alpha[tau:1]) , (g1 : y ~ beta[tau:1]) ) => ( (w1 : alpha[tau:1] ~ Int) , (w2 : beta[tau:1] ~ Int) ) )

Maybe CS5 should ignore uvars on the RHS of a skolem's CTyEqCan?

## Experiments

### How do given-given interactions manifest?

f :: (x :~: [y]) -> (x :~: z) -> x -> c f Refl Refl = id

gives a trace that includes

addTcEvBind a1c0 [G] co_a1c5 = CO: co_a1bW ; co_a1c4

and

getNoGivenEqs May have given equalities Skols: [] Inerts: {Equalities: [G] co_a1c4 {1}:: x_a1bP[sk:1] GHC.Prim.~# [y_a1bQ[sk:1]] (CTyEqCan) [G] co_a1c5 {1}:: z_a1bR[sk:1] GHC.Prim.~# [y_a1bQ[sk:1]] (CTyEqCan) Unsolved goals = 0}

(The number is braces is the SubGoalDepth -- see TcRnTypes.Note [SubGoalDepth].)

and

reportImplic Implic { TcLevel = 1 Skolems = x_a1bP[sk:1] y_a1bQ[sk:1] z_a1bR[sk:1] c_a1bS[sk:1] No-eqs = True Status = Unsolved Given = Wanted = WC {wc_impl = Implic { TcLevel = 2 Skolems = No-eqs = False Status = Unsolved Given = co_a1bV :: [y_a1bQ[sk:1]] GHC.Prim.~# x_a1bP[sk:1] Wanted = WC {wc_impl = Implic { TcLevel = 3 Skolems = No-eqs = False Status = Unsolved Given = co_a1bW :: z_a1bR[sk:1] GHC.Prim.~# x_a1bP[sk:1] Wanted = WC {wc_simple = [WD] hole{co_a1c7} {2}:: c_a1bS[sk:1] GHC.Prim.~# [y_a1bQ[sk:1]] (CNonCanonical)} Binds = EvBindsVar<a1c0> a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in an equation for `f_a1bT' }} Binds = EvBindsVar<a1c1> a pattern with constructor: Refl :: forall k (a :: k). a :~: a, in an equation for `f_a1bT' }} Binds = EvBindsVar<a1c2> the type signature for: f :: forall x y z c. (x :~: [y]) -> (x :~: z) -> x -> c }