-- https://lean-lang.org/functional_programming_in_lean/type-classes/out-params.html
data Nat = Zero | Succ Nat
  deriving (Show)

class HPlus a b c where
  (<+>) :: a -> b -> c

instance HPlus Nat Nat Nat where
  Zero <+> m = m
  (Succ n) <+> m = Succ (n <+> m)

instance HPlus Nat Integer Integer where
  Zero <+> b = b
  (Succ n) <+> b = 1 + (n <+> b)

instance HPlus Integer Nat Integer where
  a <+> Zero = a
  a <+> (Succ b) = 1 + (a <+> b)

-- a more general instance, which of course overlaps with the preceding two
instance {-# OVERLAPS #-} (Num n) => HPlus Nat n n where
  Zero <+> b = b
  (Succ n) <+> b = 1 + (n <+> b)