if statement doesn't unify when condition has multiple cases

[johannes-riecken]

Given an equality of an if statement with multiple cases in the condition and something else, I can't rewrite. I encountered this while trying to write a proof where I check if a Fin 10 is greater than 0, so I'd be happy to know a workaround. I tried to use logging to figure out where things go wrong, but didn't notice anything peculiar.

Steps to Reproduce

Try to type-check this code either with the Idris2 at HEAD or with Idris2 0.7.0.

import Syntax.PreorderReasoning
import Data.Nat

%default total
public export
foo : (x : Nat) -> (if (case x of {Z => True; (S n) => False}) then x else x) = x
foo 0 = Refl
foo (S x) = Refl

public export
bar : Nat -> Nat
bar x = (if (case x of {Z => True; (S n) => False}) then x else x)

public export
barIsId : (x : Nat) -> bar x = x
barIsId x = Calc $
    |~ (if (case x of {Z => True; (S n) => False}) then x else x)
    ~~ x ...(foo x)

public export
barIsId2 : (x : Nat) -> bar x = x
barIsId2 x = rewrite foo x in Refl

Expected Behavior

The file type-checks (which is would if I were to replace {Z => True; (S n) => False} with {n => True}).

Observed Behavior

Error: While processing right hand side of barIsId. Can't solve constraint between: if case x of { 0 => True ; S n => False } then x else x and if case x of { 0 => True ; S n => False } then x else x.

sandbox.foo:18:8--18:20
 14 | public export
 15 | barIsId : (x : Nat) -> bar x = x
 16 | barIsId x = Calc $
 17 |     |~ (if (case x of {Z => True; (S n) => False}) then x else x)
 18 |     ~~ x ...(foo x)
             ^^^^^^^^^^^^

Error: While processing right hand side of barIsId2. Rewriting by (if case x of { 0 => True ; S n => False } then x else x) = x did not change type bar x = x.

sandbox.foo:22:14--22:35
 18 |     ~~ x ...(foo x)
 19 |
 20 | public export
 21 | barIsId2 : (x : Nat) -> bar x = x
 22 | barIsId2 x = rewrite foo x in Refl
                   ^^^^^^^^^^^^^^^^^^^^^

[dunhamsteve]

Idris stumbles when trying to unify if statements. This is because the if gets turned into a case statement and then lifted to a top level function. Each instance is a separate function, and they're not definitionally equal. Since x is a variable, evaluation is stuck at applying that function. We probably should document this better. (I know because I've hit the same issue.)

If it's not a dependent if, then you can use ifThenElse and have something like: ifThenElse (isSucc x) x x instead of if (case x of {Z => True; (S n) => False}) then x else x. You might also consider making that whole expression into a single top level helper function. Then unification can match the head and the spine, because the values involved are variables. That essentially is what ifThenElse does.

[johannes-riecken]

Thanks for the fast reply. Maybe I should have looked at the generated core code to figure it out. Sounds also like Prelude.EqOrd.max might be better defined with ifThenElse then, though I guess that would break old proofs that rely on the definition with the if keyword. If you don't see any way to change this behavior so that the if statements stay definitionally equal, then feel free to close this issue.

[johannes-riecken]

I don't know much about how the compiler works, so sorry if this idea is stupid, but maybe the solution would be to not only generate the top-level functions with the case statements, but also a top-level proof of their definitional equality, and then to automatically insert a rewrite expression with that proof when both top-level functions have to be unified? Congratulations on the new release by the way!

[buzden]

maybe the solution would be to not only generate the top-level functions with the case statements, but also a top-level proof of their definitional equality, and then to automatically insert a rewrite expression with that proof when both top-level functions have to be unified?

Your solution is not stupid, but definitely looks hacky over a particular design decision of the compiler.

There is a better way, just not to treat cases at top-level functions, and there is also an alternative core called Yaffle that implements this idea, but it is not as usable as status quo and it's development paused in favour if even better alternative core, which development is slow too.