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

8 Nov 2015

      #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
           Keywords:                 |  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:
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11070
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler