Alpha-equivalence for recursive let-bindings

Christiaan Baaij christiaan.baaij at gmail.com
Sun Nov 7 21:07:49 UTC 2021


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20211107/ab491b35/attachment.html>


More information about the ghc-devs mailing list