#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

#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: | -------------------------------------+------------------------------------- Comment (by goldfire): I confirm this behavior. I'd love a second opinion, but I think this sort of trickery lies at the edge of what the solver can handle. Specifically, here is my analysis: 1. We're typechecking the body of `bar`, `[((), B)] &* foo`, at type `[(((), ()), B X2)]` 2. The type of `(&*)` tells us that `[((), B)]` has type `[(a, B n)]` for some `a` and `n`. Thus, `a` is `()`. 3. Similarly, we know that `foo` must have type `[(b, B n')]`. Thus, `b` is `()` and `n'` is `X1`, where that last fact comes from the signature on `foo`. 4. We must show that `ADD n' n` is `X2` (from `bar`'s signature). Rewriting, this is {{{ [W] c1 :: ADD X1 n ~ X2 }}} where `n` is a unification variable. 5. The type of `(&*)` also gives us {{{ [W] c2 :: n ~ SUB (ADD X1 n) X1 [W] c3 :: X1 ~ SUB (ADD X1 n) n }}} Now, here I think I see why GHC 7.8 and GHC 7.10 differ. 7.8 could rewrite wanteds with wanteds. That is, it could use `c2` or `c3` to try to solve `c1`. But 7.10 doesn't do this, because rewriting wanteds with wanteds gives terrible error messages sometimes. (To be fair, I don't actually see how this works out, after some effort. But I trust it does.) Is this a use case for rewriting wanteds with wanteds? Perhaps. But it also seems to require a non-terminating rewrite system, where `n` is rewritten with something involving `n`. I'm surprised that happened in either GHC version. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11070#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11070: Type-level arithmetic of sized-types has weaker inference power than in 7.8 -------------------------------------+------------------------------------- Reporter: cactus | Owner: (none) 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: | -------------------------------------+------------------------------------- Comment (by goldfire): We're in the borderlands here, according to comment:4. I think accepting is an improvement, yes. I don't terribly want to add this as a test case, though, because I'm worried that keeping that test case working will limit our flexibility when working on the solver. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11070#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler