You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
code:
Steps to Reproduce
Expected Behavior
no errors
Observed Behavior
Sorry if this is a known bug or already fixed.
The text was updated successfully, but these errors were encountered: