Can I implement Eq for a type which can contain a list of itself?

Question

This code doesn't compile:

data Foo = A String | B (List Foo)

Eq Foo where
  (==) (A x) (A y) = x == y
  (==) (B xs) (B ys) = xs == ys
  (==) _ _ = False

It yields the following error:

Type checking ./eq.idr eq.idr:11:3-27: | 11 | (==) (A x) (A y) = x == y | ~~~~~~~~~~~~~~~~~~~~~~~~~ Prelude.Interfaces.Main.Foo implementation of Prelude.Interfaces.Eq, method == is possibly not total due to recursive path Prelude.Interfaces.Main.Foo implementation of Prelude.Interfaces.Eq, method == --> Prelude.Interfaces.Main.Foo implementation of Prelude.Interfaces.Eq, method ==

So is the problem here that we're relying on Eq Foo in its implementation, hence the recursive path? That doesn't seem to explain it, because this compiles:

data Bar = C String | D Bar

Eq Bar where
  (==) (C x) (C y) = x == y
  (==) (D x) (D y) = x == y
  (==) _ _ = False

So - I can have recursive calls to == on whatever I'm defining the implementation on, but I can't to lists of it? Am I missing a trick to make this work, or am I trying to do something that's fundamentally broken somewhere?

Answer 1

The function that decides equality needs to be implemented in terms of mutual recursion, just as Foo itself is defined by mutual recursion.

Eq Foo where
  (==) = eq
    where mutual -- massive indentation necessary
            eq : Foo -> Foo -> Bool
            eq (A l) (A r) = l == r
            eq (B l) (B r) = eq1 l r
            eq _ _ = False 
            eq1 : List Foo -> List Foo -> Bool
            eq1 (l :: ls) (r :: rs) = eq l r && eq1 ls rs
            eq1 [] [] = True
            eq1 _ _ = False

You can't reuse List's own (==), but it is possible to factor out a pattern.

zipWithFoldrElem : (ls : List a) -> (rs : List a) -> ((l : a) -> (r : a) -> Elem (l, r) (zip ls rs) -> b) -> (b -> Lazy b -> b) -> b -> b -> b -> b
zipWithFoldrElem [] [] _ _ e _ _ = e
zipWithFoldrElem [] (_ :: _) _ _ _ el _ = el
zipWithFoldrElem (_ :: _) [] _ _ _ _ er = er
zipWithFoldrElem (l :: ls) (r :: rs) f g e el er = f l r Here `g` zipWithFoldLazyElem ls rs (\l, r, e => f l r (There e)) g e el er

Eq Foo where
  (A l) == (A r) = l == r
  (B l) == (B r) = zipWithFoldrElem l r (f l r) (&&) True False False
   where f : (ls : List Foo) -> (rs : List Foo) -> (l : Foo) -> (r : Foo) -> Elem (l, r) (zip ls rs) -> Bool
         f (l :: _) (r :: _) l r Here = l == r
         f (_ :: ls) (_ :: rs) l r (There e) = f ls rs l r e
         f [] [] _ _ _ impossible
  _ == _ = False

And, for show, here's a lexicographic Ord:

Ord Foo where
  compare (A l) (A r) = l `compare` r
  compare (B l) (B r) = zipWithFoldrElem l r (f l r) thenCompare EQ LT GT
    where f : (ls : List Foo) -> (rs : List Foo) -> (l : Foo) -> (r : Foo) -> Elem (l, r) (zip ls rs) -> Ordering
          f (l :: _) (r :: _) l r Here = l `compare` r
          f (_ :: ls) (_ :: rs) l r (There e) = f ls rs l r e
          f [] [] _ _ _ impossible
  compare (A _) (B _) = LT
  compare (B _) (A _) = GT