Type function may not be injective

Question

I am attempting to prove some axioms about odd and even natural numbers. I am using three defined data types in my proof.

data Nat = Z | S Nat

data Even (a :: Nat) :: * where
  ZeroEven :: Even Z
  NextEven :: Even n -> Even (S (S n))

data Odd (a :: Nat) :: * where
  OneOdd :: Odd (S Z)
  NextOdd :: Odd n -> Odd (S (S n))

I also have the following type families defined for addition and multiplication.

type family   Add (n :: Nat) (m :: Nat) :: Nat
type instance Add Z m = m
type instance Add (S n) m = S (Add n m)

type family   Mult (n :: Nat) (m :: Nat) :: Nat
type instance Mult Z m = Z
type instance Mult (S n) m = Add (Mult n m) n

I have functions defined for proving that the sum of two evens is even and that the product of two evens is even.

evenPlusEven :: Even n -> Even m -> Even (Add n m)
evenPlusEven ZeroEven m = m
evenPlusEven (NextEven n) m = NextEven (evenPlusEven n m)

evenTimesEven :: Even n -> Even m -> Even (Mult n m)
evenTimesEven ZeroEven m = ZeroEven
evenTimesEven (NextEven n) m = evenPlusEven (EvenTimesEven n m) n

I am using the GADTs, DataKinds, TypeFamilies, and UndecidableInstances language extension and GHC version 7.10.3. Running evenPlusEven gives me the results I expect, but I get an compilation error when I include evenTimesEven. The error is:

Could not deduce (Add (Add (Mult n1 m) n1) ('S n1)
                  ~ Add (Mult n1 m) n1)
from the context (n ~ 'S ('S n1))
  bound by a pattern with constructor
             NextEven :: forall (n :: Nat). Even n -> Even ('S ('S n)),
           in an equation for `evenTimesEven'
  at OddsAndEvens.hs:71:16-25
NB: `Add' is a type function, and may not be injective
Expected type: Even (Mult n m)
  Actual type: Even (Add (Mult n1 m) n1)
Relevant bindings include
  m :: Even m
    (bound at OddsAndEvens.hs:71:28)
  n :: Even n1
    (bound at OddsAndEvens.hs:71:25)
  evenTimesEven :: Even n -> Even m -> Even (Mult n m)
    (bound at OddsAndEvens.hs:70:1)
In the expression: evenPlusEven (evenTimesEven n m) n
In an equation for `evenTimesEven':
    evenTimesEven (NextEven n) m = evenPlusEven (evenTimesEven n m) n

The type family instances for Mult compile fine and if I replace the last line of evenTimesEven with an error throw I can compile the code and the function runs fine with an input of ZeroEven which makes me think that my instance for Mult is correct and my implementation of evenTimesEven is the problem, but I'm unsure of why.

Shouldn't Even (Mult n m) and Even (Add (Mult n1 m) n1) have the same kind?

Shouldn't evenPlusEven ZeroEven m = n be evenPlusEven ZeroEven m = m? — mschmidt
Writing * for evenTimesEven, + for evenPlusEven, and 2+ for NextEven, you have written (2+n)*m = n*m + n; it should be (2+n)*m = n*m + m + m or similar instead. — Daniel Wagner

chi chi · Accepted Answer · 2017-10-11T20:48:18

Below, I'll abuse common mathematical notation.

from the context (n ~ 'S ('S n1))

From this, we get that n = 2+n1.

Expected type: Even (Mult n m)

We need to prove n*m even, i.e. (2+n1)*m even.

Actual type: Even (Add (Mult n1 m) n1)

We have proved (n1*m)+n1 even. This is not the same. The additional term should be m, not n1, and it should be added twice.

Type function may not be injective

1 Answers