[Haskell-cafe] Why is type level (+) not commutative?

[Dominic Steinitz]

I have a type signature (for an extended Kalman filter as it happens thought that is not relevant)

> outer ::  forall m n p q .
>           (KnownNat m, KnownNat n, KnownNat p, KnownNat q,
>            (1 <=? n) ~ 'True, (1 <=? m) ~ 'True,
>            (1 <=? p) ~ 'True, (n + q) ~ p) =>
>           R n -> Sq n ->
>           L m n -> Sq m ->
>           (R p -> R n) -> (R n -> Sq n) -> Sq n ->
>           [R m] -> [R q] ->
>           [(R n, Sq n)]

and my function compiles. If I change (n+ q) ~ p to (q + n) ~ p then I get a type error

>     Could not deduce (p ~ (n + q))
>     from the context (KnownNat m,
>                       KnownNat n,
>                       KnownNat p,
>                       KnownNat q,
>                       (1 <=? n) ~ 'True,
>                       (1 <=? m) ~ 'True,
>                       (1 <=? p) ~ 'True,
>                       (q + n) ~ p)


Is expressing commutativity not possible?

Dominic Steinitz
dominic at steinitz.org
http://idontgetoutmuch.wordpress.com