Huh!  Dead right!

Would you like to:

• Open a ticket (you can use the text from this email)
• Submit a MR?

On the MR,

• Add a Note that again gives your killer example; and mention why we don’t need the check for NonRec
• Worth also pointing out that letrec { x = e1; y = e2 } in b is NOT considered equal to letrec { y = e1; x = e1 } in b.   Nor are let x=e1 in let y = e2 in b   considered equal to  let y = e1 in let x = e1 in b.   This is fine; but worth pointing out.

Thanks for pointing this out!

Simon

PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.com will cease to work.  Use simon.peytonjones@gmail.com instead.  (For now, it just forwards to simonpj@microsoft.com.)

From: ghc-devs <ghc-devs-bounces@haskell.org> On Behalf Of Christiaan Baaij
Sent: 07 November 2021 21:08
To: ghc-devs <ghc-devs@haskell.org>
Subject: Alpha-equivalence for recursive let-bindings

Hi list,

I was looking at the `Eq (DeBruijn CoreExpr)` instance and I noticed that the types of recursive let-bindings aren't checked for alpha-equivalence:

https://gitlab.haskell.org/ghc/ghc/-/blob/master/compiler/GHC/Core/Map/Expr.hs#L166-174

    go (Let (Rec ps1) e1) (Let (Rec ps2) e2)
      = equalLength ps1 ps2
      && D env1' rs1 == D env2' rs2
      && D env1' e1  == D env2' e2
      where
        (bs1,rs1) = unzip ps1
        (bs2,rs2) = unzip ps2
        env1' = extendCMEs env1 bs1
        env2' = extendCMEs env2 bs2

But doesn't that mean that:

let (x :: Int) = x in x

and

let (y :: Bool) = y in y

are considered alpha-equivalent?

If that is the case, then I think that's wrong. Agree?

I understand that you don't have to check types for non-recursive let-bindings: when the RHSs match, the types must be the same.

-- Christiaan