Matching Unapplied Data Constructors in Idris?

August 30, 2017

I got a weird bug today while working on an Idris program. I wrote something structurally similar to this:

blah : Maybe Bool -> Nat
blah Just = 2
blah Nothing = 3

This looks like it shouldn’t even compile, but it did. Furthermore, blah Nothing evaluated to 2 instead of 3, but worked correctly if I switched the order of the cases in the declaration. I figured there had to be some kind of weird problem with the type checker.

It turned out not to be a bug at all. Unlike Haskell, in which constructors must be capitalized and normal functions must not, Idris doesn’t care about capitalization. Since Idris can’t pattern match on functions, including unapplied constructors, it was creating a local variable called Just. I might as well have written this:

blah : Maybe Bool -> Nat
blah x = 2
blah Nothing = 3

The function was sensitive to the order of its patterns because the first pattern was an inadvertent catch-all.