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

[astaugaard]

$ idris2 --version
Idris 2, version 0.7.0

code:

import Data.Vect
import Decidable.Equality
import Decidable.Decidable

count : Nat -> Vect n Nat -> Nat
count t [] = 0
count t (a :: as) = 
  if isYes (decEq t a) then 
    S (count t as)
  else count t as

-- all three sub-parts of the if then else statement all work with Refl
test1 : (a : Nat) -> (n : Nat) -> (as : Vect len Nat) -> isYes (decEq n a) = isYes (decEq n a)
test1 a n as = Refl

test2 : (a : Nat) -> (n : Nat) -> (as : Vect len Nat) ->  S (count {n = len} n as) = S (count {n = len} n as)
test2 a n as = Refl

test3 : (a : Nat) -> (n : Nat) -> (as : Vect len Nat) -> (count {n = len} n as) = (count {n = len} n as)
test3 a n as = Refl
-- end of that stuff

-- work around that does type check
aeqb : (a : Nat) -> (n : Nat) -> (as : Vect len Nat) -> Equal {a = Nat} {b = Nat} 
    (if isYes (decEq n a) then S (count {n = len} n as) else count {n = len} n as) 
    (if isYes (decEq n a) then S (count {n = len} n as) else count {n = len} n as)
aeqb a n as with (decEq n a)
    _ | (Yes p) = Refl
    _ | (No p) = Refl

-- does not type check
aeqb2 : (a : Nat) -> (n : Nat) -> (as : Vect len Nat) -> Equal {a = Nat} {b = Nat} 
    (if isYes (decEq n a) then S (count {n = len} n as) else count {n = len} n as) 
    (if isYes (decEq n a) then S (count {n = len} n as) else count {n = len} n as)
aeqb2 a n as = Refl

Steps to Reproduce

idris2 example.idr

Expected Behavior

no errors

Observed Behavior

Error: While processing right hand side of aeqb2. Can't solve constraint between: if isYes (decEq n a) then S (count n as) else count n as and if isYes (decEq n a) then S (count n as) else count n as.

example:38:16--38:20
 34 | -- does not type check
 35 | aeqb2 : (a : Nat) -> (n : Nat) -> (as : Vect len Nat) -> Equal {a = Nat} {b = Nat} 
 36 |     (if isYes (decEq n a) then S (count {n = len} n as) else count {n = len} n as) 
 37 |     (if isYes (decEq n a) then S (count {n = len} n as) else count {n = len} n as)
 38 | aeqb2 a n as = Refl

Sorry if this is a known bug or already fixed.

[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.