Pattern Match on Equality

Question

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):

data Nat = S Nat | Z

plus : Nat -> Nat -> Nat
plus Z right        = right
plus (S left) right = S (plus left right)

rightIdentityAlt : (n : Nat) -> n = (plus n Z)
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) = case rightIdentityAlt y of
  Refl => Refl

This fails with the following error:

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

The roughly equivalent GHC haskell code does typecheck. I can get the Idris version to typecheck if I instead use:

cong : (x : Nat) -> (y : Nat) -> (f : Nat -> Nat) -> x = y -> f x = f y
cong _ _ _ Refl = Refl

rightIdentity : (n : Nat) -> n = (plus n Z)
rightIdentity Z = Refl
rightIdentity (S x) = cong x (plus x Z) S (rightIdentity x)

I think that the reason that rightIdentityAlt 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 with clause. Here's my attempt at doing that:

rightIdentityAlt : (n : Nat) -> n = (plus n Z) 
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) with (rightIdentityAlt y) 
  rightIdentityAlt (S y) | Refl {A = Nat} {x = y} = Refl

Blast. Still no good. Now we've lost the equality we were originally trying to prove:

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

I understand that the pragmatic answer is just to rewrite this using cong or to so something involving tactics, but I really want to understand why the way I want to write rightIdentityAlt doesn't work. Pattern matching on = 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?

Answer 1

I think this can be related to Hasochism.

The word Hasochism was used by Lindley and McBride to descibe the pain and pleasure of using (pseudo-) dependent types like GADTs in Haskell. In Haskell, as soon as we match on Refl, GHC invokes a theorem prover which will propagate that equality for us. This is the "pleasure" part.

The "pain" part lies in not having full dependent types. We do not really have f : (x : T) -> ... in Haskell. If x is universally quantified, it has to be a type in Haskell, and it will be erased at runtime, so we can't pattern match on it directly. We have to use singletons, and other techniques. Also, in Haskell we can't write g : (h : *->*) (x : *) -> h x -> ... and pass the first two arguments to make h x = Int. For that, h would need to be a type-level function, e.g. g (\t:* -> t) Int 42, but we haven't those. The lack of this feature greatly simplifies the "pleasure" part, though, and the type erasure makes the language more efficient (even though we should have the option of avoiding the erasure, with pi types), so it's not that bad.

Anyway, in Agda/Coq/Idris, unless you want to use some automagic stuff (like tactics), you have to write your own dependent elimination, and bring your equality proofs around where you need them, e.g. using your cong.

As an alternative, this also compiles:

rightIdentityAlt : (n : Nat) -> n = (plus n Z)
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) = aux y (rightIdentityAlt y) 
  where
  aux : (m : Nat) -> m = plus n Z -> S m = plus (S n) Z
  aux _ Refl = Refl

Note the innermost function aux, which involves two variables m and n. This is done so, when matching against Refl, this results in substituting m with plus n Z without affecting the n. To play this "trick" we need two distinct variables.

The issue with the original code is that m and n, there, are multiple occurrences of the same variable n. This makes the dependent matching to replace both with S y, and check the resulting type, which triggers the error.

Personally, I can understand better the dependent pattern matching in Coq, where you can use match .. return ... to express the resulting type of each match. Further, that is an expression which can be nested, without requiring separate definitions. Here it is, annotated with some comments showing how each match affects the required type.

Fixpoint rightIdentityAlt (n: nat): n = plus n O :=
   match n return n = plus n O with
   | O => (* required: n = plus n O with n := O
             hence   : O = plus O O *)
      eq_refl
   | S y =>  (* required: n = plus n O with n := S y
                hence   : S y = plus (S y) O *)
      match rightIdentityAlt y in _ = o return S y = S o with
      | eq_refl => (* required: S y = S o with o := y
                      hence   : S y = S y *)
         eq_refl
      end
   end
.