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.