Distillation crashes in some cases

[Kmeakin]

Trying to elaborate this term causes a panic:

match (0 : U32) {
    0 => 0,
    _ => 0 + 0,
}

thread 'main' panicked at 'not yet implemented: misbound local variable: Index(0)', fathom/src/surface/distillation.rs:457:25
stack backtrace:
   0: rust_begin_unwind
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/std/src/panicking.rs:575:5
   1: core::panicking::panic_fmt
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/panicking.rs:64:14
   2: fathom::surface::distillation::Context::synth_prec
             at ./fathom/src/surface/distillation.rs:457:25
   3: fathom::surface::distillation::Context::check_prec
             at ./fathom/src/surface/distillation.rs:440:18
   4: fathom::surface::distillation::Context::synth_prec::{{closure}}
             at ./fathom/src/surface/distillation.rs:634:31
   5: core::iter::adapters::map::map_try_fold::{{closure}}
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/iter/adapters/map.rs:91:28
   6: core::iter::traits::double_ended::DoubleEndedIterator::try_rfold
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/iter/traits/double_ended.rs:229:21
   7: <core::iter::adapters::rev::Rev<I> as core::iter::traits::iterator::Iterator>::try_fold
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/iter/adapters/rev.rs:56:9
   8: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::try_fold
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/iter/adapters/map.rs:117:9
   9: <core::iter::adapters::take::Take<I> as core::iter::traits::iterator::Iterator>::try_fold
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/iter/adapters/take.rs:96:13
  10: <core::iter::adapters::take::Take<I> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/iter/mod.rs:373:13
  11: scoped_arena::try_to_scope_from_iter
             at /home/karl/.local/share/cargo/registry/src/github.com-1ecc6299db9ec823/scoped-arena-0.4.1/src/lib.rs:1040:38
  12: scoped_arena::Scope<A>::try_to_scope_from_iter
             at /home/karl/.local/share/cargo/registry/src/github.com-1ecc6299db9ec823/scoped-arena-0.4.1/src/lib.rs:437:9
  13: scoped_arena::Scope<A>::to_scope_from_iter
             at /home/karl/.local/share/cargo/registry/src/github.com-1ecc6299db9ec823/scoped-arena-0.4.1/src/lib.rs:407:15
  14: fathom::surface::distillation::Context::synth_prec
             at ./fathom/src/surface/distillation.rs:631:28
  15: fathom::surface::distillation::Context::check_prec
             at ./fathom/src/surface/distillation.rs:440:18
  16: fathom::surface::distillation::Context::check
             at ./fathom/src/surface/distillation.rs:274:9
  17: fathom::surface::elaboration::Context::pretty_print_value
             at ./fathom/src/surface/elaboration.rs:458:28
  18: fathom::surface::elaboration::Context::synth_bin_op
             at ./fathom/src/surface/elaboration.rs:2028:34
  19: fathom::surface::elaboration::Context::synth
             at ./fathom/src/surface/elaboration.rs:1769:49
  20: fathom::surface::elaboration::Context::check
             at ./fathom/src/surface/elaboration.rs:1306:48
  21: fathom::surface::elaboration::Context::elab_match_const
             at ./fathom/src/surface/elaboration.rs:2335:40
  22: fathom::surface::elaboration::Context::elab_match
             at ./fathom/src/surface/elaboration.rs:2247:25
  23: fathom::surface::elaboration::Context::check_match
             at ./fathom/src/surface/elaboration.rs:2176:9
  24: fathom::surface::elaboration::Context::synth
             at ./fathom/src/surface/elaboration.rs:1466:28
  25: fathom::surface::elaboration::Context::elab_term
             at ./fathom/src/surface/elaboration.rs:730:30
  26: fathom::driver::Driver::elaborate_and_emit_term
             at ./fathom/src/driver.rs:238:30
  27: fathom::main
             at ./fathom/src/main.rs:168:21
  28: core::ops::function::FnOnce::call_once
             at /rustc/1e225413a21fa69570bd3fefea9eb05e33f8b917/library/core/src/ops/function.rs:250:5
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

bug: compiler panicked at 'not yet implemented: misbound local variable: Index(0)'
 = panicked at: fathom/src/surface/distillation.rs:457:25
 = please file a bug report at: https://github.com/yeslogic/fathom/issues/new

[Kmeakin]

The cause

• Generate a fresh meta variable for the result of the match term
• Push a local parameter for the placeholder pattern
• Check 0 + 0 against ?0
• Synth each operand of the binop, generate a fresh meta variable for each side, ?1 and ?2
• Since they are not any integer type, distill and pretty print the type of each operand and emit an error

The problem is that the type of the LHS is quoted to FunApp(Metavar(1), LocalVar(0)), and LocalVar(0) corresponds to the placeholder pattern, so its name is None.

Potential solutions

• Make synth_binop a bit smarter
• Push definitions, not parameters, when elaborating placeholder/name patterns
• Distill None names to something