The Note [Bindings with closed types] in TcEnv describes when a binding is "closed", which in turn affects generalisation. (See the Note for details.)

But the implementation doesn't follow the Note. Instead it uses this function in TcEnv:

isClosedLetBndr :: Id -> TopLevelFlag
-- See Note [Bindings with closed types] in TcRnTypes
-- Note that we decided if a let-bound variable is closed by
-- looking at its type, which is slightly more liberal, and a whole
-- lot easier to implement, than looking at its free variables
isClosedLetBndr id
  | isEmptyVarSet (tyCoVarsOfType (idType id)) = TopLevel
  | otherwise                                  = NotTopLevel

It may be easier but it's also wrong. Consider

f x = ( let g y = x+y in ...
      , x::Int)

Is g closed (which affects how definitions in ... are generalised)? Well if we typecheck the second element of the tuple first, we may "know" that x::Int by the time we are inferring a type for g, conclude that g has no free type variables, and say that it is closed.

But if we do the x::Int part second, so while type checking the let we think that x::alpha, then we'll say that g is open.

This looks nasty. I think we should do it the way the Note says.

Thanks to Facundo for pointing this out. Not urgent, but plainly wrong.