More of Note [Let-bound skolems]

Note [Let-bound 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 let-binding,
...

and we can float equalities past these let-bound 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):

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

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

3. bump level by bringing a_aUx[2] into scope {

4. emit co1_aUz :: gamma_aUw[1] ~ TokenType and set delta_aUy[2] := a_aUx[2]

5. bump level by bringing a_aUx[2] ~ Integer into scope as a Given {

6. bind x :: a_aUx[2]

7. infer RHS has type a_aUx[2]

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

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

10. } 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]

11. 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 let-bound 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 [Let-bound skolems]. Here is the full specification in that Note:

Note [Let-bound 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 let-binding, 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 [Let-bound 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 let-binding, 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.