More of Note [Letbound skolems]
Note [Letbound skolems]
in TcSMonad says
If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
and * 'a' is a skolem bound in this very implication,
then:
a) The Given is pretty much a letbinding,
...
and we can float equalities past these letbound skolems.
With that in mind, consider this, pulled from #9223 (comment 92675):
data Token t = forall a. Token (SomeToken t a)
data SomeToken t a = SomeToken (t a) a
data TokenType a where
TokLitInt :: TokenType Integer
TokLitPlus :: TokenType ()
 Without the type signature, GHC 7.8.3 can't infer the type of this function.
foo :: Token TokenType > Integer
foo (Token (SomeToken TokLitInt x)) = x + 1
foo _ = 0
Here is, roughly, what happens (uniques from actual trace left in for verisimilitude):

Guess
foo :: alpha_aUv[1] > beta_aUt[1]

Figure out
alpha_aUv[1] := Token gamma_aUw[1]

bump level by bringing
a_aUx[2]
into scope { 
emit
co1_aUz :: gamma_aUw[1] ~ TokenType
and setdelta_aUy[2] := a_aUx[2]

bump level by bringing
a_aUx[2] ~ Integer
into scope as a Given { 
bind
x :: a_aUx[2]

infer RHS has type
a_aUx[2]

emit
co2_aUR :: beta_aUt[1] ~ a_aUx[2]

} package implication:
forall[3]. a_aUx[2] ~ Integer ==> beta_aUt[1] ~ a_aUx[2]

} package implication
forall a_aUx[2]. () ==> co1_aUz :: gamma_aUw[1] ~ TokenType
forall[3] . a_aUx[2] ~ Integer ==> co2_aUR :: beta_aUt[1] ~ a_aUx[2]
 Run simplifier, yielding
gamma_aUw[1] := TokenType
(after some floating) and leading to residual
forall a_aUx[2]. () ==> forall[3] . a_aUx[2] ~ Integer ==> co2_aUR :: beta_aUt[1] ~ Integer
At this point, GHC gives up and issues an error. But actually, we can do better. If we merge the two implications (which seems allowable because there is no metavariable at level 2
that might be able to observe the difference between the original nested implication and a merged implication), then a_aUx[2]
becomes a letbound skolem and thus cannot block floating. I don't really think we should merge implications though  I don't know all the implications of doing so (pun irrelevant). Instead, we can just expand the check in Note [Letbound skolems]
. Here is the full specification in that Note:
Note [Letbound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
and * 'a' is a skolem bound in this very implication,
then:
a) The Given is pretty much a letbinding, like
f :: (a ~ b>c) => a > a
Here the equality constraint is like saying
let a = b>c in ...
It is not adding any new, local equality information,
and hence can be ignored by has_given_eqs
I propose changing to
Note [Letbound skolems]
~~~~~~~~~~~~~~~~~~~~~~~~
If * the inert set contains a canonical Given CTyEqCan (a ~ ty)
and * 'a' is a skolem bound in an implication at TcLevel N,
and * we are examining a constraint whose maximum level is M,
and * M < N
then:
a) The Given behaves as a letbinding, like
f :: (a ~ b>c) => a > a
Here the equality constraint is like saying
let a = b>c in ...
Given that the constraint in question cannot observe the difference between
the skolem's binding site and its equality constraint (because no variable
inhabits a level in between those points), it is not adding any new, local equality
information, and hence can be ignored by has_given_eqs
There is a point (b) to this Note that, I think, does not generalize in the same way, and so I have left it out here. (Obviously, some rejiggering will be required in the actual Note and the implementation of these ideas.)
What do we think? Can we float in this way? The implementation should be easy  it's the specification we must be careful about.