Failed to reify counterexample around generic lists and tuples.

[waalge]

What Git revision are you using?

aiken v1.1.17+35e41a1

What operating system are you using, and which version?

nixos

Describe what the problem is?

Some combitation of fuzz, option, and tuple crashes the compiler.
MRE here

$aiken check
    Compiling waalge/mre-fail-option-fail 0.0.0 (.)
    Compiling aiken-lang/stdlib v2.2.0 (./build/packages/aiken-lang-stdlib)
    Compiling aiken-lang/fuzz v2.1.1 (./build/packages/aiken-lang-fuzz)
   Collecting all tests scenarios across all modules
      Testing ...

   aiken::fatal::error
   Whoops! You found a bug in the Aiken compiler.

   Please report this error at https://github.com/aiken-lang/aiken/issues/new.
   In your bug report please provide the information below and if possible the code
   that produced it.

   Operating System: linux
   Architecture:     x86_64
   Version:          v1.1.17+35e41a1

   crates/aiken-lang/src/test_framework.rs:1250:22

       failed to reify counterexample?: "invalid type annotation. expected List but got: App { public: true, contains_opaque: false, module: \"\", name: \"ByteArray\", args: [], alias: None }"

What should be the expected behavior?

[paluh]

Hello,

It seems that when refining the types there is a check which prevents insertion of a new type mapping for the parameters if a given generic is present in the map:

https://github.com/aiken-lang/aiken/blob/main/crates/aiken-lang/src/expr.rs#L1240

So in our case from the example:

(Option<ByteArray>, Option<(Int, Int)>)

(Int, Int) would never be inserted as the type for the first parameter type of the Option because the first Option traverse inserts a ByteArray which will sit there and cause a mismatch.

On the other hand it seems that just removing that check (if !generics.contains_key(&ix)) is not a solution as in the case of nested types we could just overwrite the upper binding and never restore it back. For this pair type:

type P<a> { P(a, a) }

a traverse over this value:

let x:P<P<Int>> = P(P(0, 0), P(1, 1))

could cause a problem as the outer initial binding would be p0 -> P<Int> but after diving into the first parameter/value (P(0, 0)) we would end up with a mapping of p0 -> Int and then when we move back to the second parameter (P(1, 1)) we would have a mismatch P<Int> !~ Int.

This can be tackled in multiple ways (disclaimer - I'm learning Rust ;-)):

• We can make the generic parameter map immutable and create a mutable local one out of it by cloning.
• We can use fully mutable values and try to restore overwritten values.
• We can use fully immutable data structure.

Could you please tell me if my diagnosis seem right and if that is true which version of the fix would you prefer? I'm happy to provide a PR.

[KtorZ]

@paluh is your comment meant to be related to the current issue or did you mean to open a new one?

The issue reported by @waalge comes from the test framework as it attempts to reify a UPLC value back to an Aiken value; we've probably missed a case in there (it's not trivial, and also not the first one we would have missed).

[paluh]

@KtorZ I believe that my comment was relevant to the @waalge report. The original exception in the backtrace points to: crates/aiken-lang/src/test_framework.rs:1250:22 which handles error case from reify_data.

What I'm really trying to say above is that I was able to mitigate that particular problem by dropping the check here: https://github.com/aiken-lang/aiken/blob/main/crates/aiken-lang/src/expr.rs#L1240

What I'm also trying to communicate above is that just dropping this check is probably not a good fix on its own ;-)

[paluh]

JFYI, I'm slowly working on a fix in my spare time:

• I created a test suite for reify_data: https://github.com/paluh/aiken/blob/paluh/reify-data-tests-and-fixes/crates/aiken-lang/src/expr.rs#L1610

• I think that for the bug discovered in this issue the fix could be creation of the type parameter map with local vars only (even simpler than I proposed above): https://github.com/paluh/aiken/blob/paluh/reify-data-tests-and-fixes/crates/aiken-lang/src/expr.rs#L1257

• I discovered another minor issue which I will describe separately - this test case fails: https://github.com/paluh/aiken/blob/paluh/reify-data-tests-and-fixes/crates/aiken-lang/src/expr.rs#L1654

[KtorZ]

Thanks for the digging @paluh! I haven't got time unfortunately to dive into your various links and only skimmed rapidly through them. I am a bit under the water lately on many other fronts, but I'll try to give a proper look in the upcoming days.

[paluh]

@KtorZ I'm under water as well so full understanding from my side ;-)

I'm about to open a PR but I want to fix one failing test case which I created. It is somewhat orthogonal to the main issue of reification of generics but anyway. I have a question in this context:

Could you please tell me how to approach this helper function:

aiken/crates/aiken-lang/src/expr.rs

Line 1114 in 84b0fc2

|generics, data_types, data, tipo| match data {

?

• If I understand correctly overall idea in this module then reification is a type driven process of Plutus value transformation into a synthetic untyped Aiken expression.
• This particular function sometimes ignores the type information completely and sometimes somewhat uses it.
• For example it allows me to reify an Int as ByteArray. This test case catches this case: https://github.com/paluh/aiken/blob/paluh/reify-data-tests-and-fixes/crates/aiken-lang/src/expr.rs#L1751

Should I add to this function checks which verify correct type-value correspondence (for sure I can check and cover some basic cases)?