[GHC] #11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8

[GHC]

#11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8
-------------------------------------+-------------------------------------
        Reporter:  cactus            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  7.10.2
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by cactus:

Old description:

> 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)
>
> class Size ix
> instance Size X0
> instance Size a => Size (X1_ a)
> instance Size a => Size (X0_ a)
>
> 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
>
> (&*) :: (Size n, Size n', Size (ADD n' n), 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.

New description:

 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.

--

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11070#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler