GitLab

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.

Trac metadata

Trac field	Value
Version	7.10.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	facundominguez@gmail.com
Operating system
Architecture