aiken check coersion error

[waalge]

What Git revision are you using?

aiken v1.0.26-alpha+98bd61a

What operating system are you using, and which version?

nixos

Describe what the problem is?

Edit: Add missing context:

From here: https://github.com/aiken-lang/fuzz/tree/waalge/dict

$aiken check -m dict

      Testing ...

    ┍━ aiken/fuzz/dict ━━━━━━━━━━━━━━━━━━━━
    │ FAIL [after ? test] prop_dict_between
    │ × fuzzer failed unexpectedly
    │ | Type mismatch expected 'pair data data' got 'data'
    ┕ with --seed=149870503 → 1 tests | 0 passed | 1 failed

What should be the expected behavior?

not this

[KtorZ]

This is the minimal reproduction example I have, with no dependencies:

pub opaque type Dict<key, value> {
  inner: List<Pair<key, value>>,
}

pub fn constant(a: a) -> Fuzzer<a> {
  fn(s0) { Some((s0, a)) }
}

pub fn map(fuzz_a: Fuzzer<a>, f: fn(a) -> b) -> Fuzzer<b> {
  fn(s0) {
    when fuzz_a(s0) is {
      Some((s1, a)) -> Some((s1, f(a)))
      None -> None
    }
  }
}

// NOTE: Inlining `do_list` fixes the problem. But the indirection here causes:
//
// --> Type mismatch expected 'pair data data' got 'data'
pub fn list(fuzzer: Fuzzer<a>) -> Fuzzer<List<a>> {
  do_list(fuzzer, [])
}

fn do_list(fuzzer, xs) -> Fuzzer<List<a>> {
  let x <- map(fuzzer)
  [x, ..xs]
}

pub fn dict() -> Fuzzer<Dict<Int, Bool>> {
  list(Pair((1, True)))
    |> map(fn(inner) { Dict { inner } })
}

test prop_dict_between(_d via dict()) {
  True
}

[KtorZ]

~Interestingly, this appear to not be an issue on adding-pairs. So it seems like the cleanup on Pair / 2-tuple is solving more than expected.~

Nevermind, introducing back Pair makes it fail the same way.

[KtorZ]

Note, here's a more minimal reproduction example:

pub fn list(fuzzer: Option<a>) -> Option<List<a>> {
  inner(fuzzer, [])
}

fn inner(fuzzer, xs) -> Option<List<b>> {
  when fuzzer is {
    None -> Some(xs)
    Some(x) -> Some([x, ..xs])
  }
}

test tmp() {
  list(None) == Some([])
}

Interestingly, the issue is a combination of:

• The ambiguous nature of []
• The lack of annotation on inner for xs, which leaves the ambiguity open
• The fact that we perform inference in order, from top to bottom
• How Untyped Plutus Core is actually typed

All these combine lead to interesting behaviors. A way to fix the reproduction above for example, is by adding a type annotation to xs or, more interestingly, by declaring inner before list 🙃.

So there are two ways we can try to approach solving this:

1. (less satisfactory) We can detect the presence of still-unbound-variables after inferring a function body and throw an error to ask for more type annotation.

2. (more satisfactory) We can perform a topological sort of the definition within a module and ensure that we infer in dependency order, such that definitions that depends on other are inferred last.