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 )
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
Keywords: | TypeFamilies added |
---|
comment:2 Changed 4 years ago by
Description: | modified (diff) |
---|
comment:3 Changed 4 years ago by
comment:4 Changed 4 years ago by
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:
- We're typechecking the body of
bar
,[((), B)] &* foo
, at type[(((), ()), B X2)]
- The type of
(&*)
tells us that[((), B)]
has type[(a, B n)]
for somea
andn
. Thus,a
is()
.
- Similarly, we know that
foo
must have type[(b, B n')]
. Thus,b
is()
andn'
isX1
, where that last fact comes from the signature onfoo
.
- We must show that
ADD n' n
isX2
(frombar
's signature). Rewriting, this is[W] c1 :: ADD X1 n ~ X2
where
n
is a unification variable.
- 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
Amusingly enough, this now typechecks again on GHC 8.0 and later. Is this a good thing?
comment:6 Changed 15 months ago by
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.
The same behaviour can be observed with the closed-type-family version below: