Implementing an interface for a plain old recursive data type

Question

I'm fighting with Idris syntax, it seems.

module Test

data Nat = Z | S Nat

Eq Nat where
  Z == Z = True
  S n1 == S n2 = n1 == n2
  _ == _ = False

This complains with the following error (v1.1.1):

.\.\Test.idr:5:8: error: expected: "@",
    "with", argument expression,
    constraint argument,
    function right hand side,
    implicit function argument,
    with pattern
Eq Nat where
       ^
Type checking .\.\Test.idr

I don't understand why, I basically used the same syntax as the docs.

When I write an Eq implementation for a custom, non-recursive type, such as Bool, it compiles just fine.

Answer 1

You need to wrap S n patterns in parenthesis. After doing that, your will get compiler errors because Nat is already defined in Prelude. So to compile your code just replace Nat with Natural (or anything else). Though, Z and S constructors are also defined in Prelude so you either need to rename everything to be able to test in REPL easily or use %hide directive.

But at least this code compiles:

module Test

data Natural = Z | S Natural

Eq Natural where
  Z == Z = True
  (S n1) == (S n2) = n1 == n2
  _ == _ = False