title: Pattern Match on Equality
body: <p>I'm sort of new to Idris. I've used a little agda before, and I have a heavy background in GHC Haskell. I'm trying to understand why something that works in GHC Haskell doesn't work in Idris. The following code does not compile (idris version 0.12.3, nobuiltins, noprelude):</p>
  
  <pre><code>data Nat = S Nat | Z
  
  plus : Nat -&gt; Nat -&gt; Nat
  plus Z right        = right
  plus (S left) right = S (plus left right)
  
  rightIdentityAlt : (n : Nat) -&gt; n = (plus n Z)
  rightIdentityAlt Z = Refl
  rightIdentityAlt (S y) = case rightIdentityAlt y of
    Refl =&gt; Refl
  </code></pre>
  
  <p>This fails with the following error:</p>
  
  <blockquote>
    <p>idris_binary.idr:21:3-7:When checking left hand side of IdrisBinary.case block in rightIdentityAlt at idris_binary.idr:20:31:
    Unifying y and plus y Z would lead to infinite value</p>
  </blockquote>
  
  <p>The roughly equivalent GHC haskell code does typecheck. I can get the Idris version to typecheck if I instead use:</p>
  
  <pre><code>cong : (x : Nat) -&gt; (y : Nat) -&gt; (f : Nat -&gt; Nat) -&gt; x = y -&gt; f x = f y
  cong _ _ _ Refl = Refl
  
  rightIdentity : (n : Nat) -&gt; n = (plus n Z)
  rightIdentity Z = Refl
  rightIdentity (S x) = cong x (plus x Z) S (rightIdentity x)
  </code></pre>
  
  <p>I think that the reason that <code>rightIdentityAlt</code> works in GHC Haskell but not in Idris deals with a difference in how unification work in the two language. In GHC Haskell, the unifications learned from a pattern matching on a GADT just propogate everywhere, but in Idris, it seems like you need to refine the original types with a <code>with</code> clause. Here's my attempt at doing that:</p>
  
  <pre><code>rightIdentityAlt : (n : Nat) -&gt; n = (plus n Z) 
  rightIdentityAlt Z = Refl
  rightIdentityAlt (S y) with (rightIdentityAlt y) 
    rightIdentityAlt (S y) | Refl {A = Nat} {x = y} = Refl
  </code></pre>
  
  <p>Blast. Still no good. Now we've lost the equality we were originally trying to prove:</p>
  
  <pre><code>idris_binary.idr:26:20:When checking left hand side of with block in IdrisBinary.rightIdentityAlt:
  Type mismatch between
      plus y Z (Inferred value)
  and
      y (Given value)
  Holes: IdrisBinary.rightIdentityAlt
  </code></pre>
  
  <p>I understand that the pragmatic answer is just to rewrite this using <code>cong</code> or to so something involving tactics, but I really want to understand why the way I want to write <code>rightIdentityAlt</code> doesn't work. Pattern matching on <code>=</code> isn't bringing evidence into scope the way I would expect it to. Is there a way to get it to do this, or is there something fundamentally wrong with this approach in Idris?</p>