title: Implementing an interface for a plain old recursive data type
body: <p>I'm fighting with Idris syntax, it seems.</p>
  
  <pre><code>module Test
  
  data Nat = Z | S Nat
  
  Eq Nat where
    Z == Z = True
    S n1 == S n2 = n1 == n2
    _ == _ = False
  </code></pre>
  
  <p>This complains with the following error (v1.1.1):</p>
  
  <pre><code>.\.\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
  </code></pre>
  
  <p>I don't understand why, I basically used the same syntax as the docs.</p>
  
  <p>When I write an <code>Eq</code> implementation for a custom, non-recursive type, such as <code>Bool</code>, it compiles just fine.</p>