Opened 4 years ago

Last modified 15 months ago

#11070 new bug

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

Reported by: cactus Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.10.2
Keywords: TypeFamilies Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by cactus)

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.

Change History (6)

comment:1 Changed 4 years ago by cactus

Keywords: TypeFamilies added

comment:2 Changed 4 years ago by cactus

Description: modified (diff)

comment:3 Changed 4 years ago by cactus

The same behaviour can be observed with the closed-type-family version below:

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 where
    APP0 X0 = X0
    APP0 N1 = X0_ N1
    APP0 (X1_ a) = X0_ (X1_ a)
    APP0 (X0_ a) = X0_ (X0_ a)

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

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

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

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

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

comment:4 Changed 4 years ago 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)]
  1. The type of (&*) tells us that [((), B)] has type [(a, B n)] for some a and n. Thus, a is ().
  1. 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.
  1. 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.

  1. 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.

comment:5 Changed 15 months ago by RyanGlScott

Amusingly enough, this now typechecks again on GHC 8.0 and later. Is this a good thing?

comment:6 Changed 15 months ago 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.

Note: See TracTickets for help on using tickets.