#9210: "overlapping instances" through FunctionalDependencies -------------------------------------+------------------------------------- Reporter: rwbarton | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Resolution: | Keywords: FunDeps Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:9 diatchki]:
I mean that the example I gave should be rejected, but the program is accepted.
Sorry, Iavor, I'm not following. GHC as at 8.0.1 seems to be behaving as documented here http://downloads.haskell.org/~ghc/8.0.2/docs/html/users_guide/glasgow_exts.h... #instance-resolution * It is fine for there to be a ''potential'' of overlap (...); an error is only reported if a particular constraint matches more than one [instance]. .
The check for FD consistency is done when multiple instances come
together, not when you use them. Are you saying this is what you'd like to see happening? What GHC is actually doing is checking FD consistency when it sees the instance decls, and only rejecting if the instances are outright contradictory. If there's only a ''potential'' inconsistency (due to overlap), GHC only rejects at the use site if it can't resolve to a particular instance. .
This is necessary, because it ensures that the FD invariant on the class
holds, and then we can use the invariant in whatever context we want. For the same reason, you can't have instances be consistent only in some cases.
Again, I think you're saying you'd like to be able to "use the invariant"/rely on them being consistent(?) .
Currently GHC is very conservative in its use of FDs---it uses them only
for type inference. Yes GHC is conservative. Whereas in the FDs-via-CHRs paper, it is expected that under an FD `C a b | a -> b` if we have `C a b` and `C a b'` we can conclude `b = b'` (that's type equality, not just unifiability); GHC does not arrive at any such conclusion. .
This is why having inconsistent instances like the example I showed is
not the end of the world: it may result in odd behavior where GHC sometimes infers the one type and sometimes the other, but the final result is still a sound Haskell program.
For example, if GHC encountered a constraint `Foo (Int,Int) Int a`,
where `a` is a unification variable, it might instantiate `a` as either `((),Int)` or `(Int,())` depending on in what order it happened to consult the instances. This is essentially the problem that was reported in the ticket.
Yes that is the problem reported on the ticket. AFAICT is was still a problem at 7.10. I see no evidence it is still happening at 8.0. (I've tried the same code at both versions.) I agree with @Reid it's rather discomforting this change of behaviour can't be nailed down to a specific mod. What you can still do in 8.0 is put a type signature, to get inconsistent behaviour: {{{ f4 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: ((), Int) -- results in ((), 7) f5 = foo (5 :: Int, 7 :: Int) (9 :: Int) :: (Int, ()) -- results in (5, ()) }}} .
However, if GHC was to start using the FDs fully as they were intended, having inconsistent instances would lead to unsound type-checking. For example, in this case, GHC should be able to prove that `((),Int) ~ (Int,())`, which is obviously bogus.
Hmm. "as they were intended" is rather debatable. For each of the examples you're bringing forward, you're using several extensions of Haskell beyond Haskell 2010: `UndecidableInstances` or non-full dependencies (in a way that breaks the FDs-via-CHRs rules) or overlap -- either `OverlappingInstances` or overlap of the types in a non-full dependency. In this case we're now discussing you need `FlexibleInstances`, again not envisaged in the paper. I think each of those extensions is justifiable. Furthermore for GHC to be using FD inference as per the FDs-via-CHRs rules would block separate compilation. (The CHRs assume you can see all instance decls.) So I think it's prudent GHC does not try to go that far, and therefore avoids the risk of unsound type-checking. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9210#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler