Need tuple-desc-elem-implicit workaround

[ErikMcClure]

We need to either implement function variance or find a workaround for tuple-desc-elem-implicit, which was only typechecking before because the typechecker was actually broken. Currently it fails with this:

Lua error raised inside reducer collect_tuple file testfile.alc, line 983 character 60:
.\evaluator.lua:2980: both values are neutral, but they aren't equal: value.neutral(neutral_value.host_unwrap_stuck(neutral_value.tuple_element_access_stuck {
 subject = neutral_value.host_application_stuck {
  function = Lua function(_, ...): @.\terms-generators.lua:123,
  arg = neutral_value.host_tuple_stuck {
   leading = [],
   stuck_element = neutral_value.host_wrap_stuck(neutral_value.free(free.placeholder {
    index = 114,
    debug = placeholder_debug {
     name = "U",
     start_anchor = file testfile.alc, line 982 character 45,
    },
   })),
   trailing = [],
   --end neutral_value.host_tuple_stuck
  },
  --end neutral_value.host_application_stuck
 },
 index = 1,
 --end neutral_value.tuple_element_access_stuck
})) ~= value.neutral(neutral_value.host_unwrap_stuck(neutral_value.tuple_element_access_stuck {
 subject = neutral_value.host_application_stuck {
  function = Lua function(_, ...): @.\terms-generators.lua:123,
  arg = neutral_value.host_tuple_stuck {
   leading = [],
   stuck_element = neutral_value.host_wrap_stuck(neutral_value.free(free.metavariable(<table: 0x01d78eda0fa8> {
    usage = 43205,
    value = 43205,
    block_level = 3,
    trait = false,
   }))),
   trailing = [],
   --end neutral_value.host_tuple_stuck
  },
  --end neutral_value.host_application_stuck
 },
 index = 1,
 --end neutral_value.tuple_element_access_stuck
})) (printed diff)

[ErikMcClure]

This error was fixed, now we're hitting what seems like an error in substitution:

 -- Here we need to add the new arg placeholder to a map of things to substitute
-- otherwise it would be left as a free.unique in the result
mappings[unique] = typed_term.bound_variable(context_len + 1)
local val_typed = substitute_inner(val, mappings, context_len + 1)

I don't think the substitute inner unique should survive to the typechecking invocation. I suspect that indicates that the substite_inner function isn't actually finishing the substitution in that case, but I'm not sure why. I think maybe these two type expressions should actually be equal and a substitution is messing one of them up.

The stack trace:

check_concrete [./alicorn-utils.lua:30] (<table: 0x7f542a4c2e28> {
 use = value.neutral(neutral_value.tuple_element_access_stuck {
  subject = neutral_value.free(free.unique(<table: 0x7f5428ad33e0> {
   debug = "substitute_inner, val:is_closure @ @./evaluator.lua:354",
  })),
  index = 1,
 }),
 val = value.neutral(neutral_value.tuple_element_access_stuck {
  subject = neutral_value.free(free.unique(<table: 0x7f5429f17910> {
   debug = "TupleDescRelation.constrain @ @./evaluator.lua:279",
  })),
  index = 1,
 }),
 block_level = 2,
})

[ErikMcClure]

@AstroSnail managed to push this forward by fixing a missing tuple_desc_type_cons in #137, it now errors on two nuetral values with a deeply nested differing runtime context.

[AstroSnail]

currently erroring here

Alicorn0/testfile.alc

Line 1346 in fb9c2c2

let (m) = apply(c, red-param)

[ErikMcClure]

This bug is still present, but a workaround was committed to main that inlines the function.