Exitification abstracts over shadowed variables

Simon did some code review of Exitify.hs in #14152 (closed)##15110 (closed) and he was onto something; the code is wrong after all:

Consider this core term

  joinrec j (x :: Bool) (x :: Int) =
    if x == 0
    then foo x
    else jump j True (x - 1)
  in …

where the two parameters x and x are different variables, but shadow each other (i.e. have the same unique). This is legal Core!

But Exitification chooses the variables to abstract over in this line:

        -- The possible arguments of this exit join point
        -- No need for `sortQuantVars`, `captured` is already in dependency order
        abs_vars = map zap $ filter (`elemVarSet` fvs) captured

where captured = [x::Bool,x::Int] in this case, which would yield this code

  join exit (x :: Bool) (x :: Int) = foo x in
  joinrec j (x :: Bool) (x :: Int) =
    if x == 0
    then jump exit (x::Bool) (x::Int)
    else jump j True (x - 1)
  in …

which is no longer type correct (or even “scope-correct”) any more, as it passes the Int-typed x as the Bool argument to exit.

The conditions where this happens, i.e. such shadowing, is rather obscure so I did not even try to produce a lint error here. It also means that this is rather low severity, but I’ll still go and fix it.

An application of reverseNub seems to be in order – or simply switching to keeping captured in a DVarSet rather than a list (in which case sortQuantVars would be required…)

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture