LLVM backend reports "undefined value"

[b-studios]

type EMPTY {}

def main() = {
  def loop(): EMPTY = { println("!"); loop() }
  def foo(): EMPTY = loop();
  val x: Int = foo() match {}
  x + 1
}

gives

opt: ./out/strings.ll:777:20: error: use of undefined value '%x_2210'
        store %Int %x_2210, ptr %x_2210p_24
                   ^

but should compile and print ! in a loop.

[b-studios]

This is a blocker for #449

[b-studios]

The machine IR looks fine to me

def main_4200 = {
  def loop_4204 = {
    let utf8_string_literal_6221 = "\21";
    let x_6220 = println_310(utf8_string_literal_6221);
    subst [__4284 !-> x_6220];
    subst [ev6212_6212 !-> ev6212_6212];
    jump loop_4204
  };
  push { (x_6217 : Nothing) =>
    subst [x_4206 !-> x_6217];
    let x_6216 = 1;
    let x_6215 = infixAdd_4(x_4206, x_6216);
    return x_6215
  };
  push { (x_6218 : EMPTY) =>
    subst [tmp4218_4285 !-> x_6218];
    <>
  };
  let evidence_zero_6219 = Here;
  subst [ev6212_6212 !-> evidence_zero_6219];
  jump loop_4204
};
jump main_4200

[phischu]

The problem is that the following invariant is broken by this program: every variable has a single type. Specifically, the variable x_6217 is bound at type Nothing, but used at type Int. This confuses the free variable analysis, which uses the name and the type to compare for equality.

There are three possible solutions:

1. Drop the invariant and compare variables just by their name.
2. Add an explicit upcast instruction.
3. Bind variables at the type they are used with.

Not sure which of these is best.

As an unrelated side note, why do we transform empty matches to holes and not to empty matches?

[marzipankaiser]

We seem to make that assumption in lifted, too (commented assert): https://github.com/effekt-lang/effekt/blob/3099bd098962a580ed973261f9345c368345cdbb/effekt/shared/src/main/scala/effekt/lifted/Tree.scala#L197

[b-studios]

Would it be an option to take subtyping into account, when checking this? Or would this be the same as option 2?