Type-level arithmetic of sized-types has weaker inference power than in 7.8

Given the following definitions (just a copy of the relevant bits from sized-types 0.3.5.1, to keep this example self-contained):

-- Copied from sized-types 0.3.5.1
data X0 = X0
data N1 = N1

data X0_ a = X0_ Integer
data X1_ a = X1_ Integer
type X1 = X1_ X0
type X2 = X0_ (X1_ X0)

type family APP0 a
type instance APP0 X0 = X0
type instance APP0 N1 = X0_ N1
type instance APP0 (X1_ a) = X0_ (X1_ a)
type instance APP0 (X0_ a) = X0_ (X0_ a)

type family APP1 a
type instance APP1 X0 = X1_ X0
type instance APP1 N1 = N1
type instance APP1 (X1_ a) = X1_ (X1_ a)
type instance APP1 (X0_ a) = X1_ (X0_ a)

type family SUCC a
type instance SUCC X0 = X1_ X0
type instance SUCC N1 = X0
type instance SUCC (X1_ a) = APP0 (SUCC a)
type instance SUCC (X0_ a) = APP1 a

type family ADD a b
type instance ADD a X0 = a
type instance ADD X0 a = a
type instance ADD X0 N1 = N1
type instance ADD N1 N1 = APP0 N1
type instance ADD N1 (X1_ b) = APP0 b
type instance ADD N1 (X0_ b) = APP1 (ADD N1 b)
type instance ADD (X1_ a) N1 = APP0 a
type instance ADD (X0_ a) N1 = APP1 (ADD a N1)
type instance ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b))
type instance ADD (X1_ a) (X0_ b) = APP1 (ADD a b)
type instance ADD (X0_ a) (X1_ b) = APP1 (ADD a b)
type instance ADD (X0_ a) (X0_ b) = APP0 (ADD a b)

type family NOT a
type instance NOT X0 = N1
type instance NOT N1 = X0
type instance NOT (X1_ a) = APP0 (NOT a)
type instance NOT (X0_ a) = APP1 (NOT a)

type SUB a b = ADD a (SUCC (NOT b))

The following module typechecks with GHC 7.8.3:

data B w = B

(&*) :: (n ~ SUB (ADD n' n) n', n' ~ SUB (ADD n' n) n)
     => [(a, B n)] -> [(b, B n')] -> [((a, b), B (ADD n' n))]
mks &* args = undefined

foo :: [((), B X1)]
foo =  [((), B)]

bar :: [(((), ()), B X2)]
bar = [((), B)] &* foo

However, it fails with GHC 7.10.2, with

/tmp/GHCBug.hs:70:7:
    Couldn't match type ‘ADD X1 n0’ with ‘X0_ (X1_ X0)’
    The type variable ‘n0’ is ambiguous
    Expected type: [(((), ()), B X2)]
      Actual type: [(((), ()), B (ADD X1 n0))]
    In the expression: [((), B)] &* foo
    In an equation for ‘bar’: bar = [((), B)] &* foo

/tmp/GHCBug.hs:70:17:
    Occurs check: cannot construct the infinite type:
      n0 ~ ADD (ADD X1 n0) N1
    The type variable ‘n0’ is ambiguous
    Expected type: SUB (ADD X1 n0) X1
      Actual type: n0
    In the expression: [((), B)] &* foo
    In an equation for ‘bar’: bar = [((), B)] &* foo
Failed, modules loaded: none.

The workaround/solution is to change the definition of bar:

bar :: [(((), ()), B X2)]
bar = [((), B :: B X1)] &* foo

This second version typechecks with GHC 7.10.2.