#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature | Status: new request | Milestone: 7.10.1 Priority: high | Version: 7.7 Component: Compiler | Keywords: Resolution: | Operating System: Unknown/Multiple Differential Revisions: Phab:D69 | Type of failure: None/Unknown Architecture: | Test Case: Unknown/Multiple | Blocking: Difficulty: Unknown | Blocked By: | Related Tickets: #1241, | #2247, #8356, #9103, #9227 | -------------------------------------+------------------------------------- Comment (by goldfire): I have another use case for dysfunctional dependencies. While I agree that the problem could be solved "just with type annotations", the burden would be quite high: {{{#!haskell {-# LANGUAGE RebindableSyntax, MultiParamTypeClasses, FlexibleInstances, AllowAmbiguousTypes, FunctionalDependencies #-} module PolyMonad where import Prelude hiding (Monad(..)) -- normal, "monomorphic" monads class Monad m where return :: a -> m a bind :: m a -> (a -> m b) -> m b fail :: String -> m a -- Morph m1 m2 means that we can lift results in m1 to results in m2 class Morph m1 m2 where morph :: m1 a -> m2 a -- Three monads form a polymonad when we can define this kind of -- bind operation. The functional dependency is very much meant to -- be *dys*functional, in that GHC should use it only when it has -- no other means to determine m3. class PolyMonad m1 m2 m3 | m1 m2 -> m3 where (>>=) :: m1 a -> (a -> m2 b) -> m3 b -- This is my desired instance, rejected (quite rightly) by the coverage -- condition: -- instance (Morph m1 m3, Morph m2 m3, Monad m3) => PolyMonad m1 m2 m3 where -- ma >>= fmb = bind (morph ma) (morph . fmb) -- an example of this in action: newtype Id a = Id a instance Monad Id where return = Id bind (Id x) f = f x fail = error instance Morph m m where morph = id -- Without the fundep on PolyMonad, `f` cannot type-check, -- even with a top-level type signature, because of inherent -- ambiguity. f x y z = do a <- x b <- y a z b }}} Instead of using fancy rebindable syntax, I could write out my definition for `f`, put in lots of type annotations with lots of scoped type variables, and get away with it all. But that's quite a dissatisfying answer here. One of the key reasons why I'm OK with dysfunctionality here is that there is an (unenforced) expectation of coherence among `Morph` instances. That is, if we have `Morph m1 m2` and `Morph m2 m3`, I expect also to have `Morph m1 m3` such that `morph == morph . morph`, if you follow my meaning. Without this coherence, the dysfunctionality is indeed disastrous... but, I believe that `Morph` coherence would allow the code above to work nicely. This is why I've always seen dysfunctional dependencies to be quite like incoherent instances. We're asking GHC to care less about consistency so that we, the programmer, can care more. Following this further, I disagree with Martin in comment:33 saying that we insist on consistency. He gives the following example: {{{#!haskell class C a b | a -> b instance C Int Bool instance C Int Char }}} In a dysfunctional world, what's wrong with this? It absolutely does mean that if GHC has to satisfy `C Int x`, an arbitrary and fragile choice will be made. But it also means that GHC can satisfy both `C Int Bool` and `C Int Char` if it needs to. It's up to the programmer to ensure that the implementations of the instances obey some set of properties so that the program's behavior is not fragile. This seems like a reasonable burden to me. danilo2, does my example above work with your `DysfunctionalDependencies`, with the instance put in? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:41 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler