Shadowing in a lambda list gives an unexpected result

[david-christiansen]

Moved from:
GaloisInc/saw-script#367

This is unexpected:

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.6.1

Loading module Cryptol
Cryptol> :t \x x -> x : [8]
[warning] at <interactive>:1:4--1:5
    This binding for x shadows the existing binding from
    (at <interactive>:1:2--1:3, x)
(\x x -> x : [8]) : {a} [8] -> a -> [8]

[robdockins]

Note also:

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 2.6.1 (d8b1a7a)

Loading module Cryptol
Cryptol> :t \x -> \x -> x:[8]
[warning] at <interactive>:1:8--1:9
    This binding for x shadows the existing binding from
    (at <interactive>:1:2--1:3, x)
(\x -> \x -> x : [8]) : {a} a -> [8] -> [8]

So it seems specifically to be a problem with the translation of multi-argument lambdas.

[brianhuffman]

Note something strange about the warning from the original post:

Cryptol> :t \x x -> x : [8]
[warning] at <interactive>:1:4--1:5
    This binding for x shadows the existing binding from
    (at <interactive>:1:2--1:3, x)
(\x x -> x : [8]) : {a} [8] -> a -> [8]

The warning says that the second occurrence of x (at 1:4--1:5) shadows the first one (at 1:2--1:3). Yet the type shows that the first one is actually the one in scope in the body of the function.

Things seem to get even weirder when more complex patterns (e.g. tuple patterns) are involved. With \(x, y) x -> x, the warning now says that the first x shadows the second, and the type shows that the first x is the one used in the body.

Cryptol> :t \(x, y) x -> x
[warning] at <interactive>:1:3--1:4
    This binding for x shadows the existing binding from
    (at <interactive>:1:9--1:10, x)
(\(x, y) x -> x) : {a, b, c} (b, c) -> a -> b

But if we put a tuple pattern in the second argument, now the second x shadows the first (the inferred type also agrees with this).

Cryptol> :t \x (x, y) -> x
[warning] at <interactive>:1:5--1:6
    This binding for x shadows the existing binding from
    (at <interactive>:1:2--1:3, x)
(\x (x, y) -> x) : {a, b, c} a -> (b, c) -> b

If we put a tuple pattern in both arguments, then we get not just a shadowing warning, as I'd expect, but instead we get an "overlapping symbols" error!

Cryptol> :t \(x, y) (x, y) -> x
[error]
    Overlapping symbols defined:
    (at <interactive>:1:3--1:4, x)
    (at <interactive>:1:10--1:11, x)
[error]
    Overlapping symbols defined:
    (at <interactive>:1:6--1:7, y)
    (at <interactive>:1:13--1:14, y)

[brianhuffman]

Another weird one:

Cryptol> :t \x [x] x -> x
[warning] at <interactive>:1:8--1:9
    This binding for x shadows the existing binding from
    (at <interactive>:1:2--1:3, x)
[warning] at <interactive>:1:5--1:6
    This binding for x shadows the existing binding from
    (at <interactive>:1:2--1:3, x)
(\x [x] x -> x) : {a, b, c} a -> [1]c -> b -> c

The x in scope in the body is the middle one. Whichever x has the square brackets around it gets priority, apparently.

[yav]

Yeah, I think that all of these should be errors saying "multiple definitions for 'thing'".

[brianhuffman]

I think that in all cases, \pat1 pat2 -> body should mean exactly the same thing as \pat1 -> \pat2 -> body.

[robdockins]

Agreed... I'm a bit surprised this isn't literally how the desuguaring works...

[yav]

OK, we can leave them as just shadowing warnings, if you prefer that, although I can't really think about why might we want to allow people to write \x x -> x.

I suspect the actual bug is that some list is reversed somewhere, so I'll have a go at fixing it.

[brianhuffman]

Well, I see that ghc actually gives an error if you write \x x -> x, so I'd be OK with matching what Haskell does.

I got as far as identifying this line in the function renamePats as (part of) the problem:
https://github.com/GaloisInc/cryptol/blob/master/src/Cryptol/ModuleSystem/Renamer.hs#L875

I think it should read return (env' `shadowing` pe, p':rest') instead.

I couldn't figure out what was causing the inconsistent behavior with \x [x] x -> x, though.

[yav]

That might be due to an interaction with NoPat. If I recall correctly, we desugar patterns really early, in retrospect probably not the best of ideas. As a result we probably end up with something like this:

\x (ys : [1]_) x -> x
   where x = ys[0] 

I guess this has the effect of x becoming more local, which is wrong.

EDIT: correct the words.

[brianhuffman]

I see... Yes, we are doing NoPat before renaming. This would explain why we get an "overlapping symbols" error with \[x] [x] -> x: It gets turned into \p1 p2 -> x where x = p1@0; x = p2@0 before the renamer runs.

Is there any reason why we couldn't run the renamer before the NoPat pass? It doesn't seem like this would be hard to change.

[yav]

This is probably the right thing to do, although it probably would require some refactoring. Originally we just had NoPat and no renamer and I can't think of a reason for the renamer to run after.

The main reason to do NoPat was to make all variable binding sites completely explicit, as this makes it easy to associate type signatures with them (I think NoPat moves the signatures into the bindings).

It seems that this should still work, but we'd have to change the type names NoPat works with. I don't think that should be a problem though.

Since you are already looking into it, I'll un-assign myself :)

[robdockins]

Just to confirm, this bug still exists as of current master (2338302)

[robdockins]

I'm looking into this a bit, and I thought I'd jot down some things I learned.

The NoPat pass actually does quite a bit more than just desugaring patterns. It also relocates informations about names to their bindings sites. This includes fixity information, type signatures and pragmas (mostly the "property" attribute). It then removes the associated declarations from the module syntax.

The renamer then assumes all this work has been done. In particular, it expects to find type signatures (if they exist) for names when it does renaming in the bodies of definitions. This may bring type variables into scope, which then may be mentioned in type applications and numeric demotions.

Ultimately, I think this work probably all needs to be done in one unified pass instead.