#1241: Functional dependencies not checked.
-------------------------------------+--------------------------------------
Reporter: guest | Owner:
Type: bug | Status: new
Priority: normal | Milestone: _|_
Component: Compiler (Type checker) | Version: 6.6
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Architecture: Unknown
Os: Unknown |
-------------------------------------+--------------------------------------
Changes (by simonpj):
* milestone: => _|_
Old description:
> Hello,
> GHC 6.6 (with flags {{{-fglasgow-exts -fallow-undecidable-instances}}})
> is too liberal when accepting instances. Here is an example:
> {{{
> class F a b | a -> b where f :: (a,b)
> instance F Int b
> }}}
> The instance violates the functional dependency constraint of {{{F}}}
> because (in theory) it can be used to solve both {{{F Int Bool}}} and
> {{{F Int Char}}}. In practice, it seems that some free variable gets
> bound upon the first use of {{{f}}} with a concrete type, leading to some
> rather confusing behavior. Example:
> {{{
> x :: (Int,a)
> x = f
>
> y :: (Int,Bool)
> y = f
>
> z :: (Int,Char)
> z = x -- works, but 'f' does not
> }}}
>
> -Iavor
New description:
Hello,
GHC 6.6 (with flags {{{-fglasgow-exts -fallow-undecidable-instances}}}) is
too liberal when accepting instances. Here is an example:
{{{
class F a b | a -> b where f :: (a,b)
instance F Int b
}}}
The instance violates the functional dependency constraint of {{{F}}}
because (in theory) it can be used to solve both {{{F Int Bool}}} and {{{F
Int Char}}}. In practice, it seems that some free variable gets bound
upon the first use of {{{f}}} with a concrete type, leading to some rather
confusing behavior. Example:
{{{
x :: (Int,a)
x = f
y :: (Int,Bool)
y = f
z :: (Int,Char)
z = x -- works, but 'z = f' does not
}}}
-Iavor
Comment:
This is interesting. Section 5.2 of
[http://research.microsoft.com/~simonpj/papers/fd-chr Understanding
functional dependencies via Constraint Handling Rules] explains why it is
desirable to lift the Coverage Condition, which is what `-fallow-
undecidable-instances` is doing here.
The strange behaviour you get is because the occurrece of `f` in `y` gives
rise to a top-level constraint `(F Int Bool)`. Then with the definition
`z = f` we get a second top-level constraint `(F Int Char)`, and thence
the error message
{{{
Foo12.hs:1:0:
Couldn't match expected type `Bool' against inferred type `Char'
When using functional dependencies to combine
F Int Char, arising from a use of `f' at Foo12.hs:15:4
F Int Bool, arising from a use of `f' at Foo12.hs:12:4
}}}
However, with the definition `z = x` no constraint is genreated (since `x`
does not have an overloaded type) and all is well.
This is an unexected (to me) consequence of lifting the Coverage
Condition. Yet I do not want to re-impose it because (as 5.2 explains)
it's sometimes useful to have it lifted.
I'm not sure what the Right Answer here is. It looks like another fundep
brain-bender. I'm inclined to continue working on type inference for
associated types!
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1241>
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
