Bidirectional addition constraint

Question

A recent question on Reddit led to discussion of how one might produce a constraint function

type AddUp :: Nat -> Nat -> Nat -> Constraint

-- given
data Nat = Z | S Nat
type family m + n where
  'Z + n = n
  'S m + n = 'S (m + n)

such that

1. AddUp m n o means that m + n = o.
2. Any available type information about m, n, and/or o will flow to the others to the greatest extent possible.

The tricky part is #2, and the trickiest part of that is that if we know, for example, that m ~ 'S x and n ~ 'S ('S y), then we should infer from AddUp m n o that o ~ 'S ('S ('S z)) for some z.

It's quite easy to do this using incoherent instances, as /u/Tarmen showed:

class AddUp m n o
instance {-# INCOHERENT #-} n ~ o => AddUp 'Z n o
instance {-# INCOHERENT #-} m ~ o => AddUp m 'Z o
instance {-# INCOHERENT #-} (o ~ 'S po, AddUp m n po) => AddUp ('S m) n o
instance {-# INCOHERENT #-} (o ~ 'S po, AddUp m n po) => AddUp m ('S n) o
instance {-# INCOHERENT #-} (m ~ 'Z, n ~ 'Z) => AddUp m n 'Z

This particular use of incoherent instances is perfectly safe, but incoherent instances are a rather shady language feature in general. Is it possible to avoid them?

Answer 1

Yes, we can do it! The trick is to produce a bunch of equality constraints by matching on m and n in all the ways we can, in parallel. Here's a naive first attempt:

type AddUp m n o = (Bar m n o, Bar n m o, Baz m n o)

type family Bar m n o where
  Bar 'Z n o = n ~ o
  Bar ('S m) n o = (o ~ 'S (Pred o), AddUp m n (Pred o))

type family Baz m n o :: Constraint where
  Baz m n 'Z = (m ~ 'Z, n ~ 'Z)
  Baz _ _ _ = ()

type family Pred n where
  Pred ('S n) = n

This actually works, but it has a big problem: it takes exponential (or worse) time and space to compile! What's the problem? Consider AddUp ('S m) ('S n) o, and let's ignore Baz for now. This produces Bar ('S m) ('S n) o and Bar ('S n) ('S m) o. The first reduces to (o ~ S (Pred o), AddUp m (S n) (Pred o)) while the second reduces to (o ~ S (Pred o), AddUp n (S m) (Pred o)). Expanding AddUp, we see that one produces, among other things, Bar (S n) m (Pred o), while the other produces, among other things, Bar (S m) n (Pred o). When these, in turn, reduce, they produce (among other things), AddUp n m (Pred o) and AddUp m n (Pred o), which are equivalent.

How can we fix this? We need to break up Bar into two type families, the second of which is more restricted in what it matches on.

type AddUp m n o = (Bar m n o, Barf n m o, Baz m n o)

type family Bar m n o where
  Bar 'Z n o = n ~ o
  Bar ('S m) n o = (o ~ 'S (Pred o), AddUp m n (Pred o))
  
-- A version of Bar that refrains from matching on the second argument.
-- This is necessary to avoid exponential constraint size.
type family Barf m n o where
  Barf 'Z n o = n ~ o
  Barf ('S m) n o = (o ~ 'S (Pred o), Barf m n (Pred o), Baz m n (Pred o))

-- These are the same

type family Baz m n o :: Constraint where
  Baz m n 'Z = (m ~ 'Z, n ~ 'Z)
  Baz _ _ _ = ()

type family Pred n where
  Pred ('S n) = n

I believe this version requires only polynomial time (at least quadratic), rather than exponential. Or maybe reduces it by an exponential order from something even worse, once all the unification work and such is accounted for. In practice, it's substantially slower than the version using incoherent instances, but far, far faster than the naive version.