Success of typechecking depends on order of independent cases.

[SeanRBurton]

I have defined the following datatype:

data Inty = Pos Nat | Neg Nat | Zero                                            

representing the integers, where Pos n represents n and Neg n represents -n.

If I then define addition like so:

addInt : Inty -> Inty -> Inty                                                   
addInt (Pos n) (Neg m) = if n >= m then Pos (minus n m) else Neg (minus m n)
addInt (Neg n) (Pos m) = if m >= n then Pos (minus m n) else Neg (minus n m)
addInt Zero m = m                                                               
addInt n Zero = n                                                               
addInt (Pos n) (Pos m) = Pos (add n m)                                          
addInt (Neg n) (Neg m) = Neg (add n m)     

then

addIntAssoc : addInt n (addInt m o) = addInt (addInt n m) o                     
addIntAssoc {n=Zero} = Refl  

refuses to typecheck.

However, if I move the case

addInt Zero m = m                                                               

to the top, this typechecks fine.

Is this expected behaviour?

[ahmadsalim]

I do not think that the order of clauses should matter for typechecking purposes, so I think this is a true bug.

[edwinb]

The order of clauses does matter, because it affects the way the case tree is built - they're not definitional equalities.

I'd have to look more closely at the case trees to see what is really going on here, but if you have an argument position where some arguments are variables and some arguments are constructors, this sort of thing could happen.

Is anyone else able to take a look at what's going on here? The case trees are built in Idris/Core/CaseTree.hs and you can look at them with :di at the REPL or --dumpcases (the output of both is ugly, sorry).

[ahmadsalim]

@edwinb I should have been more clear I think, I meant when the patterns where disjoint as in this case.

[ahmadsalim]

So I have looked into this and the issue it seems is that the case-trees now impose an order of which variables are matched against instead of treating the above simultaneously. In particular in your case it pattern matches on the second argument before the first argument and so it never reaches the right case.

The case tree output is:

[{e0},{e1}] case {e1} of
    Main.Neg({e6}) => case {e0} of
        Main.Pos({e7}) => Prelude.Bool.ifThenElse Main.Inty (Prelude.Interfaces.>= Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Ord {e7} {e6}) (Delay LazyValue Main.Inty (Main.Pos (Prelude.Nat.minus {e7} {e6}))) (Delay LazyValue Main.Inty (Main.Neg (Prelude.Nat.minus {e6} {e7})))
        _ => case {e0} of
            Main.Zero() => {e1}
            _ => case {e1} of
                Main.Neg({e4}) => case {e0} of
                    Main.Neg({e5}) => Main.Neg (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num {e5} {e4})
                Main.Pos({e2}) => case {e0} of
                    Main.Pos({e3}) => Main.Pos (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num {e3} {e2})
                Main.Zero() => {e0}
    Main.Pos({e8}) => case {e0} of
        Main.Neg({e9}) => Prelude.Bool.ifThenElse Main.Inty (Prelude.Interfaces.>= Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Ord {e8} {e9}) (Delay LazyValue Main.Inty (Main.Pos (Prelude.Nat.minus {e8} {e9}))) (Delay LazyValue Main.Inty (Main.Neg (Prelude.Nat.minus {e9} {e8})))
        _ => case {e0} of
            Main.Zero() => {e1}
            _ => case {e1} of
                Main.Neg({e4}) => case {e0} of
                    Main.Neg({e5}) => Main.Neg (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num {e5} {e4})
                Main.Pos({e2}) => case {e0} of
                    Main.Pos({e3}) => Main.Pos (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num {e3} {e2})
                Main.Zero() => {e0}
    _ => case {e0} of
        Main.Zero() => {e1}
        _ => case {e1} of
            Main.Neg({e4}) => case {e0} of
                Main.Neg({e5}) => Main.Neg (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num {e5} {e4})
            Main.Pos({e2}) => case {e0} of
                Main.Pos({e3}) => Main.Pos (Prelude.Interfaces.+ Prelude.Nat.Nat Prelude.Nat.Nat implementation of Prelude.Interfaces.Num {e3} {e2})
            Main.Zero() => {e0}

[ahmadsalim]

Now that I see it, it does make sense that an ordering must be enforced in your case. However, the order should probably prioritise the first argument over the second argument; I am unsure on how to come up with a good heurestic to enforce that.

[edwinb]

The problem here, in the end, is that the order in which the case tree compiler works across the arguments is important. It tries to prioritise things which have more distinct constructors, at the moment, works right to left by default because heuristically that tends to generate smaller case trees.

I don't think this is the right thing to do, though, because the order matters. I would like to change it so that it works left to right for compile time case trees, and make sure that any optimisations preserve the meaning, but there are some slightly tricky issues in some existing code if we do that. The proof002 test fails, in particular, and in fact it only works because of the way the case trees happen to be built...

I can fix the case tree compiler for this specific case, but I'll leave this issue open for the moment until I've worked out how to solve the related problems... (I should really open a new issue, if only I can work out exactly what the problem is...)