Separate name resolution from elaboration

[Kmeakin]

Pushing and popping names during elaboration/unification/semantics is an annoyance (#488). It would be nice if we can separate name resolution to a separate pass performed before elaboration.

A potential hurdle is that some aspects of name resolution are type-sensitive, and so AFAIK cannot be purely syntax-directed. Namely, elaboration of surface::Term::Tuple depends on the type being checked against: if it elaborated to a RecordLiteral, no new bindings are inserted. But if it is elaborated to a RecordType or RecordFormat, a new binding is inserted for each element of the tuple. We may be able to find a workaround for this.

[Kmeakin]

Prior art

• rustc and rust-analyzer perform name resolution as a separate phase before type checking. IIUC name resolution in Rust is purely syntax directed, at least for locals (though not for globals, methods, associated types etc)
• GHC has a "renamer" pass between parsing and type checking (GHC commentary, GHC wiki)

[brendanzab]

Not really sure this would buy us, but I could be missing something. Doesn’t this still require us to push and pop parameters and definitions during elaboration? The issue in elaboration is more that we are mutating the state of the context in-place - that includes both the name environment and the type environment.

[Kmeakin]

I think it would allow us to simply mutate the environment, rather than pushing/popping.

eg currently when elaborating a let-expression:

let name = pattern.name();
let (expr, r#type_value) = self.synth(def_expr);
let expr_value = self.eval_env().eval(&expr);
self.local_env.push_def(name, expr_value, r#type_value);
let body_expr = self.synth(body_expr);
self.local_env.pop();

instead it would simply be:

let name = pattern.name();
let (expr, r#type_value) = self.synth(def_expr);
let expr_value = self.eval_env().eval(&expr);
self.local_env.set(pattern, expr_value, r#type_value);
let body_expr = self.synth(body_expr);

where self.local_env is a FxHashMap<ByAddr<&'arena Pattern<ByteRange>, (ArcValue<'arena>, ArcValue<'arena>)

[brendanzab]

Oh, so would we be switching to unique names in the syntax, as opposed to de Bruijn indices?

[Kmeakin]

No, I think we still want de Bruijn indices so that alpha equivalence is trivial