unification failure between if then else statements when using isYes (decEq n a) as the condition about idris2

[dunhamsteve]

Another workaround is to use the ifThenElse function.

I believe this issue stems from the if ... then ... else essentially being a case statement, which gets lifted to a new top level function in Idris. So It's trying two unify two different generated functions (one for each if ... then ... else ...) and getting stuck because it doesn't know which way the argument idYes (decEq n a) goes.

When ifThenElse is used, they're calling the same function and they can be compared as terms, despite the first argument being stuck. And with your workaround, each branch of the with unsticks the reduction of the generated functions.

I think the new core being developed for Idris will help with this by including case in the core language.

[astaugaard]

Thank you for this explanation. I'll keep this in mind.