#2748: Fundep-laden code compiled and ran fine in 6.8, fails in 6.10
---------------------------------+------------------------------------------
Reporter: sedillard | Owner:
Type: bug | Status: closed
Priority: normal | Milestone:
Component: Compiler | Version: 6.10.1
Severity: normal | Resolution: invalid
Keywords: | Difficulty: Unknown
Testcase: | Os: Unknown/Multiple
Architecture: Unknown/Multiple |
---------------------------------+------------------------------------------
Changes (by simonpj):
* status: new => closed
* difficulty: => Unknown
* resolution: => invalid
Old description:
> I was kindly alerted by Ian Lynagh that some code of mine on hackage was
> causing 6.10-rc1 to fail to terminate. This code compiles and runs find
> on 6.8. Instead of diverging, 6.10.1 raises a type error. I've made a
> test case, and I'm creating this ticket to figure out what's going in. Is
> it,
>
> A) The code is incorrect and 6.8 was erroneously accepting it, and only
> by luck producing a valid program
>
> B) The code is correct and 6.10.1's typechecker is being overly
> conservative.
>
> At the core is overlapping instances. I've spent considerable effort
> removing them from the library, because I can't just look at the code and
> say for certain "this will never overlap with that" because its too
> complicated. Overlap errors become the users problem, I myself having
> been bitten by them many times as a user of my own library. The solution
> is to do without overlapping instances. The types of my instances then go
> from something nice like
>
> {{{
> instance (A t) => C t
> instance (B t) => C t --overlap
> }}}
>
> to something nasty like
>
> {{{
> instance (A (T (T x))) => C (T (T x))
> instance (B (T (T (T x)))) => C (T (T (T x))) --no overlap
> }}}
>
> It's uglier for me to read and write but ultimately better for the user
> because I've eliminated a category of errors. If the compiler will let
> me, I try to abbreviate 'T (T (T x)))' to 't' in the instance head, but
> I'm not always able to because 't' is more general than 'T (T (T x)))'.
> I'm not entirely sure how that factors into things. To see what I'm
> talking about, compile the attached file and look for the error that says
> {{{Couldn't match expected type `vmt' against inferred type `vv :. (b' :.
> v)' `vmt' is a rigid type variable...}}}. It has something to do with
> functional dependencies. The fundep involved demands that 'vmt' be of the
> type 'x :. y :. z :. etc' but in this particular case it's so verbose I
> just call it 'vmt'. 6.8 lets me do that. 6.10 doesn't. Who's right?
New description:
I was kindly alerted by Ian Lynagh that some code of mine on hackage was
causing 6.10-rc1 to fail to terminate. This code compiles and runs find on
6.8. Instead of diverging, 6.10.1 raises a type error. I've made a test
case, and I'm creating this ticket to figure out what's going in. Is it,
A) The code is incorrect and 6.8 was erroneously accepting it, and only by
luck producing a valid program
B) The code is correct and 6.10.1's typechecker is being overly
conservative.
At the core is overlapping instances. I've spent considerable effort
removing them from the library, because I can't just look at the code and
say for certain "this will never overlap with that" because its too
complicated. Overlap errors become the users problem, I myself having been
bitten by them many times as a user of my own library. The solution is to
do without overlapping instances. The types of my instances then go from
something nice like
{{{
instance (A t) => C t
instance (B t) => C t --overlap
}}}
to something nasty like
{{{
instance (A (T (T x))) => C (T (T x))
instance (B (T (T (T x)))) => C (T (T (T x))) --no overlap
}}}
It's uglier for me to read and write but ultimately better for the user
because I've eliminated a category of errors. If the compiler will let
me, I try to abbreviate 'T (T (T x)))' to 't' in the instance head, but
I'm not always able to because 't' is more general than 'T (T (T x)))'.
I'm not entirely sure how that factors into things. To see what I'm
talking about, compile the attached file and look for the error that says
{{{
Couldn't match expected type `vmt' against inferred type `vv :. (b' :. v)'
`vmt' is a rigid type variable...
}}}
It has something to do with functional dependencies. The fundep involved
demands that 'vmt' be of the type 'x :. y :. z :. etc' but in this
particular case it's so verbose I just call it 'vmt'. 6.8 lets me do that.
6.10 doesn't. Who's right?
Comment:
This is a scarily complicated piece of code. I wonder if would look
simpler with type functions?
Still I took a look. I can see this:
{{{
-- Line 147-ish
class Map a b u v | u -> a, v -> b, b u -> v, a v -> u where ...
instance Map a b (a':.u) (b':.v)
=> Map a b (a:.a':.u) (b:.b':.v) where ...
-- Line 68-ish
instance
(...
,Map (a:.a:.a:.v) vv ((a:.a:.a:.v):.(a:.a:.a:.v):.m) vmt
...) where ...
)
=>
Det' a ((a:.a:.a:.v):.(a:.a:.a:.v):.(a:.a:.a:.v):.m)
}}}
Consider this simpler version:
{{{
class C a b | a->b
instance C Int Bool
f :: C Int x => ...
}}}
GHC rejects the type ignature for 'f' because 'x' must be `Bool`. It's
the same in an instance declaration
{{{
instance C Int x => ...
}}}
And that's what you have here. The fundep `b u -> v` in class `Map`
together with the instance declaration says that in any constraint
{{{
Map ... tb (ta:ta':tu) vmt
}}}
then `vmt` must be of form `(tb:tb':tv)`. But in your example it isn't.
Changing the instance decl to
{{{
instance
(...
,Map (a:.a:.a:.v) vv ((a:.a:.a:.v):.(a:.a:.a:.v):.m)
(vv :. vmt1 :. vmt2)
...) where ...
)
=>
Det' a ((a:.a:.a:.v):.(a:.a:.a:.v):.(a:.a:.a:.v):.m)
}}}
and replacing `vmt` by `(vv:.vmt1:.vmt2)` in the code, makes the error go
away.
In short, when you use a type variable like `vmt` in a type signature, GHC
assumes you mean a type `variable` and checks that you do. This is
presumably a bug in 6.8.
I've taken the opportunity to improve the error message to say which
fundep is involved. I'll close the bug though.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2748#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
