[Bug] partially implicit ternary in index leads to `Unsatisfiable`

[0rphon]

🐛 Bug Report

this only throws an error when using a mutable/input variable, if you use a const variable then it runs fine

Code snippet to reproduce

function main () {
    const a = [1u8; 2];
    let x = 2u8;
    const y = a[1u8 > x? 0 : 1u16];
}

Stack trace & error message

D:\Work\leo-playground>D:\Work\leo_repos\leo\target\release\leo clean && D:\Work\leo_repos\leo\target\release\leo run
      Done Finished in 0 milliseconds 
     Build Starting...
     Build Compiling main program... ("D:\\Work\\leo-playground\\src/main.leo")
      Done Finished in 4 milliseconds 
Error:     --> D:\Work\leo-playground\src/main.leo:4:17
     |
   4 |     const y = a[1u8 > x? 0 : 1u16];
     |                 ^^^^^^^^^^^^^^^^^
     |
     = the gadget operation `conditional select` failed due to synthesis error `Unsatisfiable`

Your Environment

• leo commit c16dad0
• rustc version 1.53.0
• Windows 10.0.19042 (Windows 10 Pro) [64-bit]

[0rphon]

a message copied from the fuzzer slack channel that i think could be of use here:

i think it being intended behavior or not really comes down to if its intended for all ternary branches to need to be explicit. because this code causes a similar error

function main (x: u8) {
    const y = x > 2u8? 1u8 : 2;
}

D:\Work\leo-playground>D:\Work\leo_repos\leo\target\release\leo clean && D:\Work\leo_repos\leo\target\release\leo run
      Done Finished in 0 milliseconds 

     Build Starting...
     Build Compiling main program... ("D:\\Work\\leo-playground\\src/main.leo")
      Done Finished in 2 milliseconds

Error:     --> D:\Work\leo-playground\src/main.leo:2:30
     |
   2 |     const y = x > 2u8? 1u8 : 2;
     |                              ^
     |
     = failed to resolve type for variable definition 'unknown'

ive known about it for a while but it never really occurred to me that it might not be intended until i saw it in the context of the index example

[collinc97]

@0rphon can you check if this was resolved by #1019 ?

[0rphon]

This is still an issue as of commit 59510107c6e9936ca32aeb31b9275d3c4c6b7c2b

[damirka]

At 55f110b6b6ec0d774166d02fc549fa866e5db7e1 error has changed. It's no longer a SnarkVM issue, type inference fails to define type.

      Done Finished in 14 milliseconds 

Error:     --> /leo/tmp/snark/src/main.leo:4:17
     |
   4 |     const y = a[1u8 > x? 0 : 1u16];
     |                 ^^^^^^^^^^^^^^^^^
     |
     = ternary sides had different types: left u32, right u16

[gluax]

We can close this, that new issue @damirka is getting is an already open issue #905.

[0rphon]

@gluax why was this closed? still an issue as of commit 1667447, and as i stated here isn't actually required to be in an index so i dont think its fully related to #905

function main() {
    let x = true? 1u8 : 2;
}

     Build Starting...
     Build Compiling main program... ("/home/orphon/Work/leo-playground/src/main.leo")
      Done Finished in 0 milliseconds 

Error:     --> /home/orphon/Work/leo-playground/src/main.leo:2:25
     |
   2 |     let x = true? 1u8 : 2;
     |                         ^
     |
     = failed to resolve type for variable definition 'unknown'

[gluax]

@0rphon oh whoops! I missed that comment saying it wasn't required to be an index. We were talking about this bug in the prioritization meeting, and I learned the original error no longer applies. I thought it was because it was an index. We can re-open and remove the snarkVM tag then.

[0rphon]

as of commit 7a5979660b7c4200fc3c8feb3263dbadd04daf0a: no longer occurs if the second value is implicit, still occurs if the first value is implicit

function main () {
    let x = true? 1 : 2u8;
}

D:\Work\leo-playground>D:\Work\leo_repos\leo\target\release\leo clean && D:\Work\leo_repos\leo\target\release\leo run
      Done Finished in 1 milliseconds 

     Build Starting...
     Build Compiling main program... ("D:\\Work\\leo-playground\\src/main.leo")
      Done Finished in 3 milliseconds

Error [EASG0373025]: failed to resolve type for variable definition 'unknown'
    --> D:\Work\leo-playground\src/main.leo:2:19
     |
   2 |     let x = true? 1 : 2u8;

[0rphon]

keeping the snarkvm tag since this may still occur at the snarkvm level and simply be blocked by the error at the asg level

[collinc97]

Implicit types are currently not supported in Leo v1.6.2.