Fix bug in DR when choosing local variable names

[davidweichiang]

If the alpha-renaming at Main.hs:112 is commented out, it now passes all tests. I'm not aware of any places other than Compile where term variables need to be renamed apart. Can we delete line 112?

Helps #119.

[colin-mcd]

I think the reason we need to alpha-rename everything before type checking is to avoid a situation like:

data Nat = Zero | Succ Nat;
define pred =
  \ Nat. case Nat of
    | Zero -> Zero
    | Succ n -> n;

Which won't type check because the type definition of Nat would get overwritten by the local term variable, so it would no longer be able to lookup the constructors of Nat

Another related situation is:

define iszero = \ n. case n of Zero -> True | Succ _ -> False;
define iszero' = \ n. let Nat = () in iszero n;

[davidweichiang]

OK, so we can not delete line 112 for now, but if #118 ends up introducing different namespaces for terms and types, I wonder if the above examples would not be problems anymore.

Will this be okay to merge (without deleting line 112)?

[colin-mcd]

Also note that even if we separated the term/type namespaces, I'd be hesitant because of potential issues with constructor name clashes, as in

data Nat = Zero | Succ Nat;
define iszero = \ Succ. case Succ of
  | Zero -> True
  | Succ n -> False;

It's possible this would be fine if we always get the ctor info from the datatype definition for type-checking, I'd just be nervous about making that a requirement

[davidweichiang]

OK, but then my question is, is the renaming at line 112 good enough to guarantee that there are no conflicts throughout the pipeline?

[davidweichiang]

I guess that's also an argument for #85.