"Use of unknown variable" ICE

[Programmerino]

This bug occurs on 0.24.3 and c304a93 (latest commit):

type option[n] = #None | #Some([n]i32)

def gen () =
    let n = 0
    in replicate n 0i32

entry test: option[] =
    if true
    then #None
    else #Some(gen ())

Error:

[  +0.000028] Reading and type-checking source program
[  +0.203442] Defunctorising
[  +0.000731] Full Normalising
[  +0.005524] Monomorphising
[  +0.052121] Lifting lambdas
[  +0.000433] Defunctionalising
[  +0.000428] Converting to core IR
[  +0.001338] Type-checking internalised program
Internal compiler error.  Please report this:
  https://github.com/diku-dk/futhark/issues
After internalisation:
In expression of statement
  {test_res_6630 : ({}, i64),
   test_res_6631 : ({}, i8),
   test_res_6632 : ({}, [test_res_6630]i32)}
in body of case {true}
In expression of statement
  {zero_6633 : ({}, [d₃_5985]i32)}
In subexp d₃_5985
Use of unknown variable d₃_5985.
types {
  type "option" = opaque {
    i8
    []i32
  }
}

let {map_6629 : ({}, unit)} =
  ()
let {test_res_6630 : ({}, i64),
     test_res_6631 : ({}, i8),
     test_res_6632 : ({}, [test_res_6630]i32)} =
  if true
  then {
    let {zero_6633 : ({}, [d₃_5985]i32)} =
      scratch(i32, d₃_5985)
    in {d₃_5985, 0i8, zero_6633}
  } else {
    let {tmp_6634 : ({}, i64),
         tmp_6635 : ({}, [tmp_6634]i32)} =
      apply gen_5980(())
      : {i64, *[?0]i32}
    let {d₃_6636 : ({}, i64)} =
      tmp_6634
    let {d₃_6637 : ({}, i64)} =
      tmp_6634
    let {tmp_6638 : ({tmp_6635}, [tmp_6634]i32)} =
      tmp_6635
    in {tmp_6634, 1i8, tmp_6638}
  }
  : {i64,
     i8,
     [?0]i32}

fun
  iota_5654 (n_6639 : i64)
  : {*[n_6639]i64} = {
  let {subtracted_step_6640 : ({}, i64)} =
    sub64(1i64, 0i64)
  let {step_zero_6641 : ({}, bool)} =
    eq_i64(0i64, 1i64)
  let {s_sign_6642 : ({}, i64)} =
    ssignum64 subtracted_step_6640
  let {bounds_invalid_downwards_6643 : ({}, bool)} =
    sle64(0i64, n_6639)
  let {bounds_invalid_upwards_6644 : ({}, bool)} =
    slt64(n_6639, 0i64)
  let {step_wrong_dir_6645 : ({}, bool)} =
    eq_i64(s_sign_6642, -1i64)
  let {distance_6646 : ({}, i64)} =
    sub64(n_6639, 0i64)
  let {step_invalid_6647 : ({}, bool)} =
    logor(step_wrong_dir_6645, step_zero_6641)
  let {range_invalid_6648 : ({}, bool)} =
    logor(step_invalid_6647, bounds_invalid_upwards_6644)
  let {valid_6649 : ({}, bool)} =
    not range_invalid_6648
  let {range_valid_c_6650 : ({}, unit)} =
    assert(valid_6649, {"Range ", 0i64 : i64, "..", 1i64 : i64, "..<", n_6639 : i64, " is invalid."}, "/prelude/array.fut:95:3-10")
  let {pos_step_6651 : ({}, i64)} =
    mul64(subtracted_step_6640, s_sign_6642)
  let {num_elems_6652 : ({}, i64)} =
    #{range_valid_c_6650}
    sdiv_up64(distance_6646, pos_step_6651)
  let {iota_res_6653 : ({}, [num_elems_6652]i64)} =
    iota64(num_elems_6652, 0i64, subtracted_step_6640)
  let {dim_match_6654 : ({}, bool)} =
    eq_i64(n_6639, num_elems_6652)
  let {empty_or_match_cert_6655 : ({}, unit)} =
    assert(dim_match_6654, {"Function return value does not match shape of declared return type."}, "/prelude/array.fut:94:1-95:10")
  let {result_proper_shape_6656 : ({iota_res_6653}, [n_6639]i64)} =
    #{empty_or_match_cert_6655}
    coerce([n_6639], iota_res_6653)
  in {result_proper_shape_6656}
}

fun
  const_6583 (x_6657 : i32,
              nameless_6658 : i64)
  : {i32} = {
  {x_6657}
}

fun
  dyn_const_6588 (x_6659 : i32)
  : {i32} = {
  {x_6659}
}

fun
  defunc_0_map_6590 (nameless_6660 : unit,
                     f_6661 : i32)
  : {i32} = {
  {f_6661}
}

fun
  defunc_0_f_6592 (x_6662 : i32,
                   nameless_6663 : i64)
  : {i32} = {
  {x_6662}
}

fun
  defunc_0_map_6593 (n_6664 : i64,
                     f_6665 : i32,
                     as_6666 : [n_6664]i64)
  : {*[n_6664]i32} = {
  let {defunc_0_map_res_6667 : ({}, [n_6664]i32)} =
    map(n_6664,
        {as_6666},
        \ {x_6668 : i64}
          : {i32} ->
          let {lam_res_6669 : ({}, i32)} =
            apply defunc_0_f_6592(f_6665, x_6668)
            : {i32}
          in {lam_res_6669})
  in {defunc_0_map_res_6667}
}

fun
  replicate_6585 (n_6670 : i64,
                  x_6671 : i32)
  : {*[n_6670]i32} = {
  let {map_arg1_6672 : ({}, [n_6670]i64)} =
    apply iota_5654(n_6670)
    : {*[n_6670]i64}
  let {map_arg1_6673 : ({map_arg1_6672}, [n_6670]i64)} =
    map_arg1_6672
  let {map_arg0_6674 : ({}, i32)} =
    apply dyn_const_6588(x_6671)
    : {i32}
  let {map_arg0_6675 : ({}, i32)} =
    map_arg0_6674
  let {defunc_0_map_arg_6676 : ({}, i32)} =
    apply defunc_0_map_6590(map_6629, map_arg0_6675)
    : {i32}
  let {replicate_res_6677 : ({}, [n_6670]i32)} =
    apply defunc_0_map_6593(n_6670, defunc_0_map_arg_6676, map_arg1_6673)
    : {*[n_6670]i32}
  in {replicate_res_6677}
}

fun
  gen_5980 (nameless_6678 : unit)
  : {i64,
     *[?0]i32} = {
  let {n_6679 : ({}, i64)} =
    0i64
  let {gen_res_6680 : ({}, [n_6679]i32)} =
    apply replicate_6585(n_6679, 0i32)
    : {*[n_6679]i32}
  let {d₂_6681 : ({}, i64)} =
    n_6679
  in {n_6679, gen_res_6680}
}

entry("test",
      {},
      {opaque "option"})
  entry_test ()
  : {i64,
     i8,
     [?0]i32} = {
  {test_res_6630, test_res_6631, test_res_6632}
}

[athas]

Interesting. Should this program be type correct? I don't think so. There is no way for the type checker to know the type of the #None branch.

[Programmerino]

I'm not sure I understand. It seems like the compiler is able to infer the type of a branch based on the type of the other branches -- why not here? For example, in:

type option 'a = #None | #Some(a)

entry test =
    if true
    then #None
    else (#Some(5): option i32)

My assumption was that the size parameter would be carried over to the other branch.

[athas]

The false branch has type Option ([n]i32) for some impossible-to-know n. The true branch has type Option ([m]i32) for any choice of m. But it cannot pick m=n because n is not in scope there. It's the same reason this program is not type correct:

def gen () : ?[n].[n]i32 =
  let n = 0
  in replicate n 0i32

def empty [n] 't (_: [n]t): [0][n]t =
  []

entry main b: [0][]i32 =
  if b
  then []
  else empty(gen ())

And the solution is the same: add a type annotation to disambiguate.

The solution I'm cooking up will actually provide a slightly misleading type error, because it will try to set m=n and then fail with a causality check. That's much easier to implement in the current structure of the type checker, which is based on fairly straightforward Hindley-Milner, followed by a pass that checks that no existential sizes ended up propagating in unfortunate places.

[athas]

Actually, one root cause of this bug is that when a constructor like #None is encountered we don't yet know its full type, only that it is "some sum type with a constructor #None [n]i32 for some n". It is difficult to track this n properly because it's not part of the syntactical type as far as the type checker is contained - the type is at this point just an unresolved type variable pointing at a constraint. The causality checker operates on fully elaborated syntactical types, so it can look precisely at what is going on.

[athas]

It's precisely this rule that the program violates, and which the type checker did not catch.

[Programmerino]

Makes sense, thank you for your detailed explanation!