Shadowing?

[stephen-smith]

I'm not sure if this is intentional or not, but fields can shadow each other AND you can actually access either value if they have different types. I'm not sure if this is on purpose or not:

shadowy : Record [("nil", Int), ("nil", String)]
shadowy = [ "nil" := 0, "nil" := "" ]

underneath : String
underneath = shadowy . "nil"

on_top : Int
on_top = shadowy . "nil"

That defines underneath to be the String "" and on_top to be the Int 0.

[stephen-smith]

Looks like the paper did that intentionally. Though, I'm not sure it expected that users could access a shadowed field of the same type, as long as they provide an explicit presence proof:

weird : Record [("test", Int), ("test", Int)]
weird = [ "test" := 1, "test" := 0 ]

undercover : Int
undercover = get' weird (Later First)

ready : Int
ready = weird . "test"

That defines undercover as the Int 0 and ready as the Int 1. As the paper mentioned, there's no type incorrectness, but it does seem a bit odd.