semantics of Eq instance for Var.Var (was: is shadowing allowed in CoreSyn?)

[Max Bolingbroke]

On 17 February 2011 00:33, Adam Megacz <megacz at cs.berkeley.edu> wrote:
> Technically according to the code, two Vars are equal if they have the
> same Unique.  But if I understand correctly, Uniques are just supposed
> to be a way of making some other equivalence test go faster by picking a
> canonical representative (the Unique) for each equivalence class of the
> relation (from the Haddock: "[Unique is] the type of unique identifiers
> that are used in many places in GHC for fast ordering and equality tests").
>
> So, in this case, what equivalence test is being made faster?
>
> A Var is basically an OccName plus a Type, but:
>
>  - Two Vars with the same OccName may be unequal (I see why this is)
>
>  - Two Vars with different types may be equal
>
>  - Two Vars which represent variables which have different binding
>    sites may be equal (which is what I understand 'refer to the "same
>    thing"' to mean).
>
> So I guess I'm confused about what equality on Vars is supposed to mean.

Testing for equality/ordering between vars is very useful. For
example, let's say you are writing a core pass that trundles through
the tree recursively, and you want to track some information about
every variable that you may come across in the expression. In such a
case, a natural thing to do is to write a function of type:

trundle :: Map Var MyBinderData -> CoreExpr -> MyAnalysisResult

Whenever you come across a coreexpr that binds something (e.g. a
lambda) you need to extend the Map with information about the binder
before you recurse on the thing which can see that binder (e.g. the
body of the lambda). If you do this by simply inserting into the Map
then, if your binder shadows one above, the data associated with that
shadowed binding will be made inaccessible. This is almost always
exactly what you want, because it means if you look up e.g. the lambda
binder within the body you get the info associated with the binder
instead of the binder that the lambda binding shadows.

So, given that you only use the Eq/Ord instance to test Vars against
Vars originating from *visible* binding sites, everything is cool.
Where visible bindings sites are both:
 * Lexically enclosing (e.g. x is visible within e for the expression
\x -> e, but x is not visible within e for the expression (\x -> x,
e))
 * Unshadowed (e.g. the lexically first x is shadowed in the
expression \x -> \x -> e)

GHC just ensures that it never uses the Eq/Ord instance for Var in a
way that violates this property. Presumably whatever code you write
that uses equality of Vars should be careful to do the same.

> How would you write "instance Eq Var" if you didn't care about fast
> ordering and equality tests and therefore weren't using Uniques?

If you weren't using Uniques, presumably your variables would be
compared just by their OccName. This would not be substantially
different:

 * Two vars with the same occname would be equal, but
 * Two vars with different types would be equal (you could still have shadowing)
 * Two vars which represent vars with different bindings sites may be equal

I'm not sure where you are going with this line of thought.

Cheers,
Max