[GHC] #8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition)

#8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) ------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- == Abstract == Hi! I'm writing a compiler, which produces Haskell code. I've discovered it is impossible to keep currently used features / logic using GHC 7.7 instead of 7.6 Below is more detailed description of the problem: == The idea == I'm writing a [DSL][1], which compiles to Haskell. Users of this language can define own immutable data structures and associated functions. By associated function I mean a function, which belongs to a data structure. For example, user can write (in "pythonic" pseudocode): {{{#!python data Vector a: x,y,z :: a def method1(self, x): return x }}} (which is equivalent to the following code, but shows also, that associated functions beheva like type classes with open world assumption): {{{#!python data Vector a: x,y,z :: a def Vector.method1(self, x): return x }}} In this example, `method1` is a function associated with `Vector` data type, and can be used like `v.testid(5)` (where `v` is instance of `Vector` data type). I'm translating such code to Haskell code, but I'm facing a problem, which I'm trying to solve for a long time. == The problem == I'm trying to move the code from GHC 7.6 over GHC 7.7. The code works perfectly under GHC 7.6, but does not under GHC 7.7. I want to ask you how can I fix it to make it working in the new version of the compiler? == Example code == Lets see a simplified version of generated (by my compiler) Haskell code: {{{#!haskell {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FunctionalDependencies #-} import Data.Tuple.OneTuple ------------------------------ -- data types ------------------------------ data Vector a = Vector {x :: a, y :: a, z :: a} deriving (Show) -- the Vector_testid is used as wrapper over a function "testid". newtype Vector_testid a = Vector_testid a ------------------------------ -- sample function, which is associated to data type Vector ------------------------------ testid (v :: Vector a) x = x ------------------------------ -- problematic function (described later) ------------------------------ testx x = call (method1 x) $ OneTuple "test" ------------------------------ -- type classes ------------------------------ -- type class used to access "method1" associated function class Method1 cls m func | cls -> m, cls -> func where method1 :: cls -> m func -- simplified version of type class used to "evaluate" functions based on -- their input. For example: passing empty tuple as first argument of `call` -- indicates evaluating function with default arguments (in this example -- the mechanism of getting default arguments is not available) class Call a b where call :: a -> b ------------------------------ -- type classes instances ------------------------------ instance (out ~ (t1->t1)) => Method1 (Vector a) Vector_testid out where method1 = (Vector_testid . testid) instance (base ~ (OneTuple t1 -> t2)) => Call (Vector_testid base) (OneTuple t1 -> t2) where call (Vector_testid val) = val ------------------------------ -- example usage ------------------------------ main = do let v = Vector (1::Int) (2::Int) (3::Int) -- following lines equals to a pseudocode of ` v.method1 "test" ` -- OneTuple is used to indicate, that we are passing single element. -- In case of more or less elements, ordinary tuples would be used. print $ call (method1 v) $ OneTuple "test" print $ testx v }}} The code compiles and works fine with GHC 7.6. When I'm trying to compile it with GHC 7.7, I'm getting following error: {{{ debug.hs:61:10: Illegal instance declaration for ‛Method1 (Vector a) Vector_testid out’ The liberal coverage condition fails in class ‛Method1’ for functional dependency: ‛cls -> func’ Reason: lhs type ‛Vector a’ does not determine rhs type ‛out’ In the instance declaration for ‛Method1 (Vector a) Vector_testid out’ }}} The error is caused by new rules of checking what functional dependencies can do, namely `liberal coverage condition` (as far as I know, this is `coverage condition` relaxed by using `-XUndecidableInstances`) == Some attemps to fix the problem == I was trying to overcome this problem by changing the definition of `Method1` to: {{{#!haskell class Method1 cls m func | cls -> m where method1 :: cls -> m func }}} Which resolves the problem with functional dependencies, but then the line: {{{#!haskell testx x = call (method1 x) $ OneTuple "test" }}} is not allowed anymore, causing a compile error (in both 7.6 and 7.7 versions): {{{ Could not deduce (Method1 cls m func0) arising from the ambiguity check for ‛testx’ from the context (Method1 cls m func, Call (m func) (OneTuple [Char] -> s)) bound by the inferred type for ‛testx’: (Method1 cls m func, Call (m func) (OneTuple [Char] -> s)) => cls -> s at debug.hs:50:1-44 The type variable ‛func0’ is ambiguous When checking that ‛testx’ has the inferred type ‛forall cls (m :: * -> *) func s. (Method1 cls m func, Call (m func) (OneTuple [Char] -> s)) => cls -> s’ Probable cause: the inferred type is ambiguous }}} It is also impossible to solve this issue using type families (as far as I know). If we replace `Method1` type class and instances with following code (or simmilar): {{{#!haskell class Method1 cls m | cls -> m where type Func cls method1 :: cls -> m (Func cls) instance Method1 (Vector a) Vector_testid where type Func (Vector a) = (t1->t1) method1 = (Vector_testid . testid) }}} We would get obvious error `Not in scope: type variable ‛t1’`, because type families does not allow to use types, which does not appear on LHS of type expression. == The final question == How can I make this idea work under GHC 7.7? I know the new `liberal coverage condition` allows GHC devs make some progress with type checking, but it should somehow be doable to port idea working in GHC 7.6 over never compiler version. (without forcing user of my DSL to introduce any further types - everything so far, like type class instances, I'm genarating using Template Haskell) Maybe is there a way to indroduce an extension, which will disable liberal coverage condition in such situations? There is also a StackOverflow discussion available, here: http://stackoverflow.com/questions/20778588/liberal-coverage-condition- introduced-in-ghc-7-7-breaks-code-valid-in-ghc-7-6 [1]: http://en.wikipedia.org/wiki/Domain-specific_language -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: #1241, #2247, #8356 Blocking: | -----------------------------------+--------------------------------------- Changes (by rwbarton): * related: => #1241, #2247, #8356 Comment: {{{#!haskell class Method1 cls m func | cls -> m, cls -> func where ... }}} This means "for any type `cls`, there must be at most one type `func` for which there is an instance `Method1 cls m func`". (And the same for `m`.) {{{#!haskell instance (out ~ (t1->t1)) => Method1 (Vector a) Vector_testid out where ... }}} This defines instances like `Method1 (Vector Bool) Vector_testid (Int -> Int)`, `Method1 (Vector Bool) Vector_testid (Char -> Char)`, etc., so it violates the functional dependency. So, it was a (long-standing) bug that GHC 7.6 allowed this instance declaration. See the related tickets for further discussion. As for how to fix your program: it's hard to see what's going on with the `Call` type class, but can you try dropping both functional dependencies and writing {{{#!haskell instance (m ~ Vector_testid, out ~ (t1->t1)) => Method1 (Vector a) m out where ... }}} I'll leave this ticket open as several people have asked for an option to relax this functional dependency sanity condition, but I don't think it's a very good idea myself; the condition seems to usually catch real bugs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: #1241, #2247, #8356 Blocking: | -----------------------------------+--------------------------------------- Comment (by rwbarton): Perhaps the option to emulate the GHC 7.6 behavior could be called `-XDysfunctionalDependencies`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: #1241, #2247, #8356 Blocking: | -----------------------------------+--------------------------------------- Comment (by danilo2): Replying to [comment:1 rwbarton]: First of all, thank you for your response and your comments :)
This means "for any type `cls`, there must be at most one type `func` for which there is an instance `Method1 cls m func`". (And the same for `m`.) Exactly - with one data type `cls` there could be "associated" only one function `func` with the name `method1`.
{{{#!haskell instance (out ~ (t1->t1)) => Method1 (Vector a) Vector_testid out where
...
}}}
This defines instances like `Method1 (Vector Bool) Vector_testid (Int -> Int)`, `Method1 (Vector Bool) Vector_testid (Char -> Char)`, etc., so it violates the functional dependency. So, it was a (long-standing) bug that GHC 7.6 allowed this instance declaration.
Hm, but if we assume, that there is only one such function `(a->a)` for a given `cls`, this should not be a problem? In such case, we are sure, that for `Vector a` and `Vector_testid` there is 0 or 1 functions with such signature (of course without such assumption this could be dangerous, but if a "power user" is writing lets say a DSL or is generating Haskell code and knows what he is doing, I see no point in preventing it.
See the related tickets for further discussion.
As for how to fix your program: it's hard to see what's going on with
I'll read them, thank you. the `Call` type class (...) I'm really sorry for this - my example was probalby too simplified. Please take a look at this code (this is the same as above, but slighty modified and extended): {{{#!haskell {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FunctionalDependencies #-} import Data.Tuple.OneTuple ------------------------------ data Vector a = Vector {x :: a, y :: a, z :: a} deriving (Show) newtype Vector_method1 a = Vector_method1 a newtype Vector_method2 a = Vector_method2 a ------------------------------ testid (v :: Vector a) x = x testf2 (v :: Vector a) x = (x,x) ------------------------------ testx x = call (method1 x) "test" ------------------------------ class Method1 cls m func | cls -> m, cls -> func where method1 :: cls -> m func class Method2 cls m func | cls -> m, cls -> func where method2 :: cls -> m func class Call ptr args result | ptr args -> result where call :: ptr -> args -> result ------------------------------ instance (out ~ (t1->t1)) => Method1 (Vector a) Vector_method1 out where method1 = (Vector_method1 . testid) instance (base ~ (t1 -> t2), out ~ t2) => Call (Vector_method1 base) (OneTuple t1) out where call (Vector_method1 val) (OneTuple arg) = val arg instance (base ~ (String -> t2), out ~ t2) => Call (Vector_method1 base) () out where call (Vector_method1 val) _ = val "default string" ------------------------------ instance (out ~ (t1->(t1,t1))) => Method2 (Vector a) Vector_method2 out where method2 = (Vector_method2 . testf2) instance (base ~ (t1 -> t2), out ~ t2) => Call (Vector_method2 base) (OneTuple t1) out where call (Vector_method2 val) (OneTuple arg) = val arg ------------------------------ main = do let v = Vector (1::Int) (2::Int) (3::Int) print $ call (method1 v) (OneTuple "test") print $ call (method1 v) () print $ call (method2 v) (OneTuple "test") }}} output: {{{#!haskell "test" "default string" ("test","test") }}} Here you can see, that we can call "method1" giving it `(OneTuple "test")` or `()`. The former passes simply one argument, while the later passes 0 arguments and the default value of "default string" is choosen instead.
(...) but can you try dropping both functional dependencies and writing {{{#!haskell instance (m ~ Vector_testid, out ~ (t1->t1)) => Method1 (Vector a) m out where ... }}}
Unfortunatelly I can not :( Look, `Vector_testid` indicates, that it holds "testid" method (it should be named `Vector_method1` instead - sorry for that typo. If we get more associated functions, we would have `Vector_method2`, `Vector_method3` etc, so we need to distinguish them - see the sample code in this comment.
I'll leave this ticket open as several people have asked for an option to relax this functional dependency sanity condition, but I don't think it's a very good idea myself; the condition seems to usually catch real bugs.
I do not think to allow some "power users" to relax this condition, if such people know what they are doing. I completely agree, such condition usually catches a lot of bugs - so it should be enabled by default, but If you know, what you are doing, you've ben warned and you should make it off :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Unfortunatelly I can not :( Look, Vector_testid indicates, that it holds "testid" method (it should be named Vector_method1 instead - sorry for
#8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: #1241, #2247, #8356 Blocking: | -----------------------------------+--------------------------------------- Comment (by rwbarton): that typo.
If we get more associated functions, we would have Vector_method2, Vector_method3 etc, so we need to distinguish them - see the sample code in this comment.
That doesn't seem to be a problem, as those will be instances of different classes `Method2`, `Method3`. {{{#!haskell instance (m ~ Vector_method1, out ~ (t1->t1)) => Method1 (Vector a) m out where method1 = (Vector_method1 . testid) instance (m ~ Vector_method2, out ~ (t1->(t1,t1))) => Method2 (Vector a) m out where method2 = (Vector_method2 . testf2) }}} With these changes your second program runs for me with GHC HEAD as long as I comment out `testx`--which is not used in the program. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: #1241, #2247, #8356 Blocking: | -----------------------------------+--------------------------------------- Comment (by danilo2): Replying to [comment:4 rwbarton]:
That doesn't seem to be a problem, as those will be instances of different classes `Method2`, `Method3`. Ouch, of course, you are right. I wanted to tell about the problem you've discovered later:
(...) With these changes your second program runs for me with GHC HEAD as long as I comment out `testx`--which is not used in the program.
And this is the problem I was talking about on StackOverflow and my original question - I marked it as "the problematic function" in GHC 7.7. It is now impossible, to make this function an "Vectora associated method" `method3`. We are generating all type class instances with template Haskell reifying needed functions to get their type signatures. If such function does not compile, reify would also fail. Even writing type class instances manually, it is impossible to make instances of `Method3` and `Call` for it, because it does not compile. By the way, this function will make more sense if it will be written as: {{{#!haskell testx v x = call (method1 x) (OneTuple "test") }}} , which means, calling associated "method1" of "x" with one argument of "test". It is still working in GHC 7.6. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: bug | Status: new Priority: high | Milestone: Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: None/Unknown | Blocked By: Test Case: | Related Tickets: #1241, #2247, #8356 Blocking: | -----------------------------------+--------------------------------------- Comment (by danilo2): Replying to [comment:4 rwbarton]: According to my previous comment, here is sample code, which uses the function `testx` as associated metthod `method2` to datatype `Vector` (it works under GHC 7.6 and is, as you've noted, impossible to convert to 7.7): {{{#!haskell {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE FunctionalDependencies #-} import Data.Tuple.OneTuple ------------------------------ data Vector a = Vector {x :: a, y :: a, z :: a} deriving (Show) newtype Vector_method1 a = Vector_method1 a newtype Vector_method2 a = Vector_method2 a ------------------------------ testid v x = x testf2 v x = (x,x) ------------------------------ -- problematic function: testx v x = call (method1 x) (OneTuple "test") ------------------------------ class Method1 cls m func | cls -> m, cls -> func where method1 :: cls -> m func class Method2 cls m func | cls -> m, cls -> func where method2 :: cls -> m func class Call ptr args result | ptr args -> result where call :: ptr -> args -> result ------------------------------ instance (out ~ (t1->t1)) => Method1 (Vector a) Vector_method1 out where method1 = (Vector_method1 . testid) instance (base ~ (t1 -> t2), out ~ t2) => Call (Vector_method1 base) (OneTuple t1) out where call (Vector_method1 val) (OneTuple arg) = val arg instance (base ~ (String -> t2), out ~ t2) => Call (Vector_method1 base) () out where call (Vector_method1 val) _ = val "default string" ------------------------------ instance ( Call (m func0) (OneTuple String) b , Method1 a m func0 , out ~ (a -> b) ) => Method2 (Vector v) Vector_method2 out where method2 = (Vector_method2 . testx) instance (base ~ (t1 -> t2), out ~ t2) => Call (Vector_method2 base) (OneTuple t1) out where call (Vector_method2 val) (OneTuple arg) = val arg ------------------------------ main = do let v = Vector (1::Int) (2::Int) (3::Int) print $ call (method1 v) (OneTuple "test") print $ call (method1 v) () print $ call (method2 v) (OneTuple v) }}} Output: {{{#!haskell "test" "default string" "test" }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: feature | Status: new request | Milestone: Priority: high | Version: 7.7 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: None/Unknown | Related Tickets: #1241, #2247, #8356 Test Case: | Blocking: | -----------------------------------+--------------------------------------- Changes (by goldfire): * type: bug => feature request Comment: I have to say I like the idea of `-XDysfunctionalDependencies`. An error in functional dependencies can never make a program "go wrong". Why do I claim this? Because the type safety of GHC Haskell is based on the type safety of Core, GHC's internal, typed language.... and functional dependencies don't exist, at all, in Core. So, perhaps functional dependencies can change exactly what Core is produced, but they can only go from one type-safe Core program to another type-safe Core program. I see something like `-XDysfunctionalDependencies` as quite like `-XIncoherentInstances`. These threaten coherence (the notion that the same instance of a class will be used for the same type(s) in different places) but not type safety. The a power user wants to ignore coherence, maybe that's OK. `-XDysfunctionalDependencies` has another nice benefit: it gives users a quick and dirty way to arbitrarily nudge the type inference engine. Currently, one of the tenets of type inference is that it makes no guesses and performs no search. But with `-XDysfunctionalDependencies` users could provide (perhaps incoherent) hints to the type inference engine, which would allow more programs to type check. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -----------------------------------+--------------------------------------- Reporter: danilo2 | Owner: Type: feature | Status: new request | Milestone: Priority: high | Version: 7.7 Component: Compiler | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: None/Unknown | Related Tickets: #1241, #2247, #8356 Test Case: | Blocking: | -----------------------------------+--------------------------------------- Comment (by danilo2): Hello! Is there any progress regarding this issue? It was planned for ghc-7.7 and I feel it is not very hard to implement (because it only lifts checking for liberage coverage condition) - but of course I might be wrong :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: None/Unknown | Related Tickets: #1241, #2247, #8356 Test Case: | Blocking: | -----------------------------------+--------------------------------------- Changes (by thoughtpolice): * milestone: => 7.10.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: None/Unknown | Related Tickets: #1241, #2247, #8356 Test Case: | Blocking: | -----------------------------------+--------------------------------------- Comment (by goldfire): See https://phabricator.haskell.org/D69 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: None/Unknown | Related Tickets: #1241, #2247, #8356 Test Case: | Blocking: | -----------------------------------+--------------------------------------- Comment (by goldfire): I take back my claim that `-XDysfunctionalDependencies` cannot cause type errors. While it's true that fundeps do not exist in Core, it's conceivable that dysfundeps could cause invalid Core to be produced, leading to errors caught by `-dcore-lint`. I have not thought this out in great detail, but I think I was too quick to judgment in comment:7. To summarize: it's possible that dysfundeps are type-safe, and it's possible that they are not. I have not thought hard enough about the problem to stake a claim on one answer or another: my reasoning in comment:7 is bogus, though perhaps my conclusion is correct. In any case, I don't wish to be cited as the person who thinks that these are safe! :) I still ''do'' think that, if someone discovers these ''are'' safe, they might become an interesting tool. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Keywords: Compiler | Architecture: Unknown/Multiple Resolution: | Difficulty: Unknown Operating System: | Blocked By: Unknown/Multiple | Related Tickets: #1241, #2247, #8356, #9103 Type of failure: | None/Unknown | Test Case: | Blocking: | ----------------------------+---------------------------------------------- Changes (by simonpj): * related: #1241, #2247, #8356 => #1241, #2247, #8356, #9103 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 | -------------------------------------+------------------------------------- Changes (by thoughtpolice): * differential: => Phab:D69 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 | -------------------------------------+------------------------------------- Comment (by simonpj): Provoked by this ticket, and other recent ones (#9227, #9103) I’ve taken another look. Here are my preliminary conclusions. * #1241 has the best overall discussion, and the paper “[http://research.microsoft.com/en-us/um/people/simonpj/papers/fd-chr/ Understanding functional dependencies using constraint handling rules]” * The [http://www.haskell.org/ghc/docs/latest/html/users_guide/type- class-extensions.html#instance-rules user manual section] that claims “Both the Paterson Conditions and the Coverage Condition are lifted if you give the `-XUndecidableInstances` flag” is plain wrong. * What actually happens is that `-XUndecideableInstances` weakens the Coverage Condition to the Liberal Coverage condition. See `Note [Coverage conditions]` in `FunDeps.lhs`. (Actually, looking at the paper, what is called “Liberal Coverage Condition” here and in the code is the “Refined Weak Coverage Condition” in the paper, Definition 15. * Even this looks bogus. Looking at #1241 comment 15, we see that to get good behaviour (termination, confluence) we need “full fundeps” and “S(tvsright) are all type variables”, neither of which are checked by GHC. * I disagree with Richard's comment above (comment 11). There is no way that fundeps can cause a program to pass the type checker but fail Core Lint. All that fundeps do is cause extra “derived” type equalities to be added to the constraint solver’s pile. That can cause type errors, and perhaps confusing ones, but it cannot cause unsoundness. * The worst that can happen is 1. Non-termination of the type inference engine. This can definitely happen, but is acceptable; c.f. `-XUndecideableInstances`. 2. Non-confluence of type inference. The paper goes on about this at length. I think it amounts to incompleteness. Maybe type inference will succeed one day, but fail the next because of some random variation in the order in which the constraint solver tackles its constraints. I do not have an example that shows this behaviour, but it would be a Bad Thing. I see no good reason to stop programmers getting perhaps-strange behaviour if they ask for it. So I would be OK with doing this (which is exactly what https://phabricator.haskell.org/D69 proposes this behaviour for the Coverage Condition (see [http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class- extensions.html#instance-rules user manual]) * No flags: Coverage Condition enforced * `-XUndecidableInstances`: changes Coverage Condition to Liberal Coverage Condition. This risks non-termination. I’m still uneasy about the consequences of not checking for “full” fundeps (see comment 15 of #1241) but it’s what happens right now. * `-XDysFunctionalDependencies`: removes the Coverage Condition altogether, with somewhat unknown consequences. So this is a long-winded way of saying I’m ok with the D69 proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 | -------------------------------------+------------------------------------- Changes (by simonpj): * related: #1241, #2247, #8356, #9103 => #1241, #2247, #8356, #9103, #9227 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): Incidentally, on the Phab comment stream, danilo2 says: I'm very attracted to the idea to be able to throw away liberage coverage condition - in some places it could give interesting effects (like IncoherentInstances). But in opposite to IncoherentInstances, I've got a real-life code, which is right now working using DysfunctionalDependencies and is working great. I and some people from the company I'm working in were thinking for a long time if we can replace a very special type class instance with other mechanisms and we came to a conclusion, that using this extension would be life saver for us - and this is the reason I started looking into ghc and implementing it. I would be very happy If you agree with me and would allow this extension to exist within GHC. I'm adding the comment in here by way of further motivation. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:16 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 | -------------------------------------+------------------------------------- Changes (by simonpj): * cc: diatchki, martin.sulzmann@… (added) Comment: Martin, Iavor, I'd welcome feedback about the proposed course of action in comment:14 above. Thanks! Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:17 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 diatchki): I think that rwbarton's comments above explain quite well why danilo2's program is incorrect, and GHC correctly rejects it. No matter which rule we use to ''implement'' the consistency check for the functional- dependency, it is crucial that the rule is ''sound''. No sound rule will accept that program, because it violates the ''specification'' for functional dependencies. As for `DysfunctoinalDependencies`: I have no idea what that means, or how it is supposed to work. Is there a write-up or a spec that explains the extension? I'll refrain from commenting further until I understand the concept, but I do think that if it gets implemented, it should use a different syntax from FDs. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): @diatchki please do not base your opinion on the examples above - they are a little old and of course, they do not obey some basic principles. The idea with `-XDysfunctionalDependencies` is just to lift both the Paterson Conditions and the Coverage Condition - something `-XDysfunctionalDependencies` claims to do (according to documentation), but does not (as simonpj noticed above). When using this extension you can just give hints to typechecker and compile programs like the one I've posted on https://phabricator.haskell.org/D69 : {{{#!haskell {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DysfunctionalDependencies #-} class CTest a b | a -> b where ctest :: a -> b data X = X instance Monad m => CTest X (m Int) where ctest _ = return 5 main = print (ctest X :: [Int]) -- [5] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

No matter which rule we use to ''implement'' the consistency check for
#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): Replying to [comment:18 diatchki]: the functional-dependency, it is crucial that the rule is ''sound''. Why? As Simon notes above, if FDs are unsound, the programs that we get are still type-correct. There may be class coherence issues and/or fragile compilation (that is, changes in behavior that stem from seemingly- insignificant changes in code), but not outright failure. (By outright failure, I mean "seg fault" or `unsafeCoerce`.) And, in comment:19, I believe danilo2 meant to say that the documentation claims that `-XUndecidableInstances` lifts the Paterson and coverage conditions, but that the documentation is wrong. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:20 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): I think we are all agreed that type inference must be sound. But, as mentioned above, "sound" for GHC means that * If the program passes the type checker, the elaborated Core program satisfies Core Lint. * If a program satisfies Core Lint, it enjoys preservation and progress (of the Core program); it cannot seg-fault. In operational terms I think the change proposed is well specified: look at comment:14, especially the user manual section and the three bullets at the end of the comment. The question at issue is not soundness, but rather * Precisely which programs satisfy the type inference engine? * Is type inference complete? I.e. does it find a type for every program specified by the first bullet? * Is type inference robust? I.e. can a small change in the program (e.g. swapping the order of arguments to a function) make the difference between type inference succeeding and failing? * Is the elaborated program coherent? I.e. is it well specified what the result of running that program will be? The effect of `-XDysFunctionalDependencies` on these aspects of type inference is not well understood. But it seems a much more benign form of allowing the programmer saying "trust me please" than `unsafeCoerce`, for example, because the soundness guarantee is not threatened. The `-XUndecideableInstances` flag is somewhat similar, in that it continues to guarantee soundness, but allows type inference to diverge. This could perfectly well be a per-instance pragma, rather than a module- wide language extensions. Something like {{{ instance {-# DYSFUNCTIONAL#-} Monad m => CTest X (m Int) where ... }}} That might be better, actually; it's more precisely targeted. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:21 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): See also #9267 for an interesting example. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:22 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): @goldfire, you are right - I fixed my comment, thank you :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:23 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 sulzmann): Some brief comments regarding the various conditions/flags. * Paterson Conditions and the Coverage Condition (plus the FD Consistency Condition) The above guarantee sound and decidable type inference. In CHR speak, termination and confluence. Confluence effectively means that we find unique answers. Hence, confluence implies consistency. Hence, we also obtain type safety. * Dropping the Coverage Condition There are numerous examples which violate this condition. Naively dropping this condition potentially threatens decidable type inference (due to non-termination) and type safety (due to non-confluence). * Weak (aka refined) Coverage Condition Guarantees local confluence (critical pairs are joinable). Assuming that instances are terminating we obtain confluence (by Newman's Lemma). The bad news is that typical examples which violate the coverage but satisfy the weak coverage condition are non-terminating. Consider the classic example class F a b | a -> b instance F a b => F [a] [b] where for constraint F [a] a the type inferencer will not terminate The good news is that in "On Termination, Confluence and Consistent CHR-based Type Inference", ICLP'14, we show that (under some modest extra conditions) for terminating type inference goals we find unique answers. In essence, we're happy to achieve local confluence under the assumption that we have local termination. * XUndecidableInstances Enforces the weak coverage condition but gives up on (global) termination. Assuming that the GHC type inference terminates nothing bad will happen though (cause we find unique answers, see above) * DysfunctionalDependencies I can only guess what this means as I couldn't find any concrete definition. My impression is to drop the weak coverage condition? Bad idea! We no longer have local confluence. We might be lucky enough that GHC always applies type inference rules (FD improvement, instances) in a fixed order and thus 'unique' answers are guarantees. Sounds rather brittle to me. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): Martin, thanks. Yes, as comment:14 specifies (fairly precisely I thought), `DysFunctionalDependencies` means relaxing the coverage condition altogether. Let me stress once more that, apparently contrary to your second bullet, dropping coverage does not threaten type soundness. I'm not quite sure what you mean by "type safety". I did actually go back to our JFP paper "Understanding functional dependencies using constraint handling rules" to see if I could find a concrete example of the problems that might arise, but all I could find I was the unsupported claim that "all is lost" if we don't have confluence. I ''believe'' (but I have no example that demonstrates) that dropping the Coverage Condition might mean that a small change in the program makes a large difference in whether the type inference algorithm succeeds. But it would be good to have some concrete cases. One way to gather some might be to allow it, and see whether our users start complaining about unpredicatable inference. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:25 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 sulzmann): Correct. I'm too pessimistic in my comment. For type safety (well-typed programs cannot go wrong) it suffices to have consistency. Simon, surely the Consistency Condition must hold at least, right? I agree then that the Coverage Condition (or variants) can be dropped. See Theorem 1 in the above mentioned paper. I still find it strange that you want to drop the Coverage Condition (or variants of it). This clearly leads to non-confluence, hence, unpredictable type inference. Consider class F a b | a -> b where f :: a -> b -> a instance F b a => F [a] [b] -- Order of 'a' and 'b' swapped! -- Hence, (weak) coverage is violated. g as bs c = (f as bs, f as c) The above gives (roughly) rise to the constraints F [a] [b], F[a] c Depending on the order type inference rules are applied, the following two final constraints may arise (1) c = [b], F b a (2) c = [b'], F b a, F b' a Say we use (1) for some type annotation but the type checker only comes up with (2). Urgh! To conclude: - For type safety we require at least consistency - For predictable type inference we require (local) termination and (weak) coverage. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:26 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): I've got a single question related to this topic - lets assume I've got a simple code: {{{#!haskell {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DysfunctionalDependencies #-} class CTest a b | a -> b where ctest :: a -> b data X = X instance Monad m => CTest X (m Int) where ctest _ = return 5 main = do let f = ctest X -- ... some code here print "end" }}} Is it possible in such example, that anything would break using the `-XDysfunctionalDependencies` (assuming, that all instances mention concrete types for `a`, like the one on the example, which mentions `X` in place of `a`)? This is the exact case we need to use it right now (of course very simplified). For now it works very well even for large examples. When such code "could" break and give us unpredictable results? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:27 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 sulzmann): You should be fine in the situation you describe above. The type inferencer is faced with a single constraint CText X t for some t which is then reduced to t = m Int, Monad m In my example I assume two occurrences of method f which result in F [a] [b], F[a] c This leads then to a conflict between the FD and the instance rule. Hence, we find two distinct final constraint stores (1) and (2). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): @sulzmann - great, so `-XDysfunctionalDependencies` are safe for our purposes - we never define instances described by your example :) Its very good to hear that, because we've got such instance in core system of our product, which works great now and we do not imagine how could we handle it other way around :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:29 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): OK, Martin, that's a good example (in comment:26). Let's see a bit more detail. We start with {{{ F [a] [b], F [a] c }}} Now there are two sorts of "improvement" rules which might fire: A. '''Between two constraints'''. Since we have `F [a] [b]` and `F [a] c`, we may derive `[b] ~ c`. After all the class fundep for `F` claims that `a -> b`. B. '''Between a constraint and an instance declaration'''. Here we have * `instance forall p q. F q p => F [p] [q]` (I have alpha-renamed.) * `F [a] c` Since the `[a]` matches the `[p]` we may conclude that `c ~ [q']`, where `q'` is a fresh unification variable, reflecting the fact that the instance declaration says the second parameter must be a list but doesn't tell you what the element type is. So Martin's point is that there are two possible solution paths: {{{ F [a] [b], F [a] c ===> Use (A) to combine the two F [a] [b], F [a] c, c ~ [b] ===> Use the instance declaration to simplify F b a, c ~ [b] }}} Here is the other path: {{{ F [a] [b], F [a] c ===> use the instance declaration F b a, F [a] c ===> use (B) to combine the second constraint with the instance F b a, F [a] c, c ~ [q'] ===> use the instance declaration again F b a, F q' a, c ~ [q'] (stuck) }}} This is helpful: it's a concrete example that demonstrates how minor variations in the way the inference engine works may lead to unpredictable failures in type inference. One possible reaction is that if you are going to lift the Coverage Condition, then (A) yields too many equalities, and you shouldn't use it. But (B) is still useful, and is actually what is wanted here. So maybe we want {{{ class C a b | a ~> b }}} notice `a ~> b` rather than `a -> b`, meaning "`a` specifies the ''shape'' of `b`", which would make use improvement rule (B) but not (A) for this fundep. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:30 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

@diatchki please do not base your opinion on the examples above - they are a little old and of course, they do not obey some basic principles. The idea with `-XDysfunctionalDependencies` is just to lift both the Paterson Conditions and the Coverage Condition - something `-XUndecidableInstances` claims to do (according to documentation), but does not (as simonpj noticed above). When using this extension you can just give some interesting hints to typechecker and compile programs like
#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 diatchki): This program has the exact same problem as the one in the ticket above: it violates the functional dependency. Having a "functional dependency" simply means that you are telling GHC that you want to work with a "functional relation (in the specified parameters)", and it should give you an error if you made a mistake. Here is how you can rewrite your program without `Dysfunctional Dependencies`: {{{ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} data X = X class C a b where ctest :: a -> b class D a f b | a -> b where dtest :: a -> f b instance Monad m => D X m Int where dtest _ = return 5 instance (Monad m) => C X (m Int) where ctest = dtest main = print (ctest X :: [Int]) -- [5] }}} Replying to [comment:19 danilo2]: the one I've posted on https://phabricator.haskell.org/D69 :
{{{#!haskell {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DysfunctionalDependencies #-}
class CTest a b | a -> b where ctest :: a -> b
data X = X
instance Monad m => CTest X (m Int) where
ctest _ = return 5
main = print (ctest X :: [Int]) -- [5] }}}
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Martin, thanks. Yes, as comment:14 specifies (fairly precisely I
#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 diatchki): comment:14 specifies what GHC is NOT going to do, but it does not specify what it will do! As a programmer, when I see a class-declaration: {{{ class C a b | a -> b }}} I think: ''Aha, there is a functional relation between the parameters of this class. This means that whenever the first parameters of instances are the same, so will be the second ones''. I don't know what this declaration means in the context of `Dysfunctional Dependencies`. I am also unclear about why `DysfunctionalDependencies` removes some of the consistency checks but not ``all``? I believe that due to the current GHC implementation, "nothing will go wrong" even if we allowed instances such as `C Int Char` and `C Int Bool`, or am I missing something? All of this will change, however, if we were to complete the implementation of FDs and added support for using the FDs on given constraints: then type-safety actually depends on the consistency of the instances, and we better not have any `Dysfunctoinal Dependencies` around. Replying to [comment:25 simonpj]: thought), `DysFunctionalDependencies` means relaxing the coverage condition altogether.
Let me stress once more that, apparently contrary to your second bullet,
dropping coverage does not threaten type soundness. I'm not quite sure what you mean by "type safety". I did actually go back to our JFP paper "Understanding functional dependencies using constraint handling rules" to see if I could find a concrete example of the problems that might arise, but all I could find I was the unsupported claim that "all is lost" if we don't have confluence.
I ''believe'' (but I have no example that demonstrates) that dropping
the Coverage Condition might mean that a small change in the program makes a large difference in whether the type inference algorithm succeeds. But it would be good to have some concrete cases. One way to gather some might be to allow it, and see whether our users start complaining about unpredicatable inference.
Simon
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:32 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 sulzmann): Here's a brief summary of my current understanding: At all times we demand (the) Consistency (Condition). For instance, the following example violates the Consistency Condition. class C a b | a -> b instance C Int Bool instance C Int Char The Consistency Condition is the minimal requirement to guarantee type safety. (1) The Coverage Condition guarantees termination and confluence for all programs. Recall confluence means that we find unique answers. (2) The Weak Coverage Condition guarantees (local) confluence assuming that we can establish (local) termination. That is, if the type inferencer terminates for some constraint arising from some program text (aka goal constraint) then we know the answer is unique. (3) So what happens if we drop coverage (but of course still demand consistency)? Then we can neither guarantee termination nor confluence (which is obviously bad for predictable type inference). The example I gave still enjoys termination but in general we encounter non-confluence. danilo2 mentions some specific application scenario where for the specific constraints arising out of the program text we seem to find unique answers. I agree that the naming of GHC flags (UndecidableInstances, DysfunctionalDependencies) connected to (2) and (3) is not very helpful and rather confusing. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:33 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): @diatchki - you are right - in this simple example your solution would work and will fulfill the LCC (Liberal Coverage Condition). Again - trying to simplify examples, they got oversimplified sometimes. I will try to put here another one, a little more complex: {{{#!haskell {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DysfunctionalDependencies #-} class Property a b | a -> b where property :: a -> b data X = X data Y = Y instance Monad m => Property X Y where prperty _ = Y instance Monad m => Property Y (m Int) where property _ = return 5 main = do let f = property $ property X -- ... some code here print "end" }}} Let assume the above code is generated an **rarely** there is situation that the LCC condition is not met (as with the second instance). Property is just an associated object with current one. We want to create chains of associated objects, like `property $ property $ property Z`. To do so, we have to use functional dependencies. Additional there is no way of checking if such chain violates or not the LCC. This is the users responsibility (I can explain this further if needed). Sometimes it could happen, that LCC would be not met, as I showed above, but it still (!) tells: "Aha, there is a functional relation between the parameters of this class. This means that whenever the first parameters of instances are the same, so will be the second ones." and this is still true for `-XDysfunctionalDependencies`! The difference is, as shown by @sulzmann, that the Coverage Condition is completely lifted. The above example is still very, very simplified and does not show the complex of the problem, but as I mentioned above - we have moved succesfully our code from GHC 7.6 into GHC 7.10(head) with the extension of `-XDysfunctionalDependencies` and it just works (even with large "connection chains" (mentioned above). I think it just works in this scenario and still, the fundeps are talking to as, that whenever the first parameters are the same, so will be the second ones. One thing that is not so beautifull is the name - I do not know if `-XDysfunctionalDependencies` or `-XUndecidableInstances` are proper names for their behaviours. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:34 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 emertens): Instead of using "dysfunctional" dependencies, the above programs can be written in GHC today as shown below. This pattern actually happens in the wild regularly and takes advantage of the way GHC resolves instances. {{{ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} class Property a b where property :: a -> b data X = X data Y = Y deriving Show instance (y ~ Y) => Property X y where property _ = Y instance (Monad m, m Int ~ y) => Property Y y where property _ = return 5 main = do print =<< property Y print (property Y :: [Int]) print (property X) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:35 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): @emertens: I know it really well, it would not work - look at this example: {{{#!haskell {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} class Property a b where property :: a -> b data X = X data Y = Y deriving Show data Z = Z deriving Show instance (y ~ Y) => Property X y where property _ = Y instance (z ~ Z) => Property Y z where property _ = Z tst a = property $ property a main = do print (property $ property X) }}} Error: {{{#!haskell Could not deduce (Property s0 b) arising from the ambiguity check for ‘tst’ from the context (Property a s, Property s b) bound by the inferred type for ‘tst’: (Property a s, Property s b) => a -> b at Tmp.hs:21:1-29 The type variable ‘s0’ is ambiguous When checking that ‘tst’ has the inferred type tst :: forall b s a. (Property a s, Property s b) => a -> b Probable cause: the inferred type is ambiguous }}} It will work for simple examples but will fail for functions like `tst` - it's caused by open world assumption - you never knows if there will be another instance defined, which will be more precise than already defined (with `-XOverlappingInstances` enabled). The only way around is to use fundeps here :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:36 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 rwbarton): You can write your program with `AllowAmbiguousTypes`: add `{-# LANGUAGE AllowAmbiguousTypes, ScopedTypeVariables #-}` and change `tst` to {{{ tst :: forall a s b. (Property a s, Property s b) => a -> b tst a = property (property a :: s) }}} Your program could be equally ambiguous if it used GHC 7.6-style/dys- functional dependencies. The difference is that GHC 7.6 assumes that in `Property a s`, `a` determines `s` if and only if there is a fundep `a -> s`, though neither implication is necessarily true. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:37 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): Replying to [comment:37 rwbarton]: It still would not work: 1) the following script does not compile 2) I DO want to determine the output type based on the input types - I really want to introduce there fundep. I mean - I want to be able to write `tst a = property (property a)` and use it as `tst X` and get `Z` as the result. Additional - this is only one of the exampels we are using the extension. There are some other places where it works quite well. I do not know if here is the best place to discuss possible workarounds (but I'm very happy and thankfull to hear suggestions)? Anyway, I post the code I mentioned above: {{{#!haskell {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE AllowAmbiguousTypes #-} class Property a b where property :: a -> b data X = X data Y = Y deriving Show data Z = Z deriving Show instance (y ~ Y) => Property X y where property _ = Y instance (z ~ Z) => Property Y z where property _ = Z tst :: forall a s b. (Property a s, Property s b) => a -> b tst a = property (property a :: s) main = do print (property $ property X) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:38 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 simonpj): Several points * Your script in comment:37 typechecks just fine if you use `-XScopedTypeVariables`. You need the 's' in the body of `tst` to be the same as the one in the type signature. * Interestingly in this example, unlike earlier ones, the instances for `Property` really do morally satisfy the (liberal) Coverage condition: the first parameter determines the second. And GHC knows this. For example, this is accepted right now (with `UndecidableInstances` so that we get the liberal coverage condition): {{{ class Property a b | a -> b where -- Note the fundep property :: a -> b instance (y ~ Y) => Property X y where -- Suppose this was accepted property _ = Y }}} And now you don't need the `:: s` signature in the body of `tst` * It's also worth remembering that ALL fundeps do in GHC is guide the type inference engine. And you can offer the same guidance via type signatures. So you should be alle to fix your 600-module system by adding some type signatures. * Martin's excellent example, explained in detail in comment:30, is a pretty convincing reason for not rushing ahead with lifting the coverage condition altogether, especially given that there is another workaround (type signatures). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:39 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 danilo2): Replying to [comment:39 simonpj]: 1) Of course - you are right - with `-XScopedTypeVariables` it does compile and works well - please forgot me, I overlooked the flag. 2) Yes this example satisfies the Coverage Condition, but as I described before it is just another simplification of some problem and in general we got instances which satisfy and which does not the condition. 3) There is other problem with providing such types by hand - we are generating the code and it would be very hard to generate such annotations in general. @rwbarton: Thank you again for your example - of course it works as you described. Still, while it needs some type signatures, they are hard for us to generate (while we are generating the Haskell's code). I think introducing optional `-XDysfunctionalDependencies` flag even as a local flag or using `~>` symbol, as Simon suggested above, would be a great thing - allowing to play with type system and creating easier some "hackish" things if user wishesh to. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:40 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 danilo2): Replying to [comment:41 goldfire]: It deos not, but from simple reason. Your instance for PolyMonad does not specify what is the `m3` in any sense. I mean - you are using `(morph ma)` and `(morph . fmb)`. According to open world assumption, anybody can create any instance for `Morph` class, which is NOT injective, so we get here disambigous types: {{{#!haskell Could not deduce (Monad m20) arising from the ambiguity check for ‘f’ from the context (Monad m3, Monad m2, Morph m5 m2, Morph m4 m2, Morph m2 m3, Morph m1 m3) bound by the inferred type for ‘f’: (Monad m3, Monad m2, Morph m5 m2, Morph m4 m2, Morph m2 m3, Morph m1 m3) => m1 t -> (t -> m4 t1) -> (t1 -> m5 b) -> m3 b at Tmp.hs:(44,1)-(46,16) The type variable ‘m20’ is ambiguous When checking that ‘f’ has the inferred type f :: forall t (m1 :: * -> *) (m2 :: * -> *) (m3 :: * -> *) b t1 (m4 :: * -> *) (m5 :: * -> *). (Monad m3, Monad m2, Morph m5 m2, Morph m4 m2, Morph m2 m3, Morph m1 m3) => m1 t -> (t -> m4 t1) -> (t1 -> m5 b) -> m3 b Probable cause: the inferred type is ambiguous }}} But your example can be easly fixed by defining any hints and NOT using `-XDysfunctionalDependencies` like this: {{{#!haskell {-# LANGUAGE RebindableSyntax, MultiParamTypeClasses, FlexibleInstances, AllowAmbiguousTypes, FunctionalDependencies, NoMonomorphismRestriction, ScopedTypeVariables, UndecidableInstances #-} 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: class (Monad m1, Monad m2, Monad m3) => MatchMonad m1 m2 m3 | m1 m2 -> m3 instance (Morph m1 m3, Morph m2 m3, Monad m3, MatchMonad m1 m2 m3) => PolyMonad m1 m2 m3 where ma >>= fmb = bind (morph ma) (morph . fmb) -- ma >>= fmb = bind (matchMonad (morph ma) (undefined:: )) (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 a }}} Still, I completely agree with all the things you stated in your post. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:42 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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'm not sure I understand comment:42, danilo2. The error you have toward the beginning of the comment is what I see when I leave out the fun-dep on `PolyMonad`. It doesn't seem related to my commented-out instance. Or, does un-commenting out the instance really produce that error? That's something strange. And, the `MatchMonad` idea just seems to kick the can down the road a bit: how could we have my desired instance for `MatchMonad` without `DysfunctionalDependencies`? Yes, `f` will type-check, but it won't be able to be called. Or am I deeply confused? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:43 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 sulzmann): Regarding dropping the Consistency Condition (comment:41) Well, that's the minimal requirement I demand to call something Functional Dependencies. Oh, I see we are in the DysfunctionalDependencies world :) I'm also more than curious how to establish type safety without this requirement. What I'm describing in comment:33 are various forms of (type safe) Functional Dependencies where 'predictability' of type inference decreases the more we relax the coverage criteria. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:44 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by danilo2): @goldfire: I'm out of the office right now - I've got to do something urgent today - in the evening I'll reply you with examples and my understanding of the things. I'm sorry for the delay - I 'll edit this comment. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:45 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by neo): Hi! I'm not sure if I face the same problem as the issue author or if my code is just "wrong" but when testing my code with GHC 7.8 I get the [https://travis-ci.org/adp-multi/adp-multi/jobs/34132805#L437 same error] while it worked with 7.6. My library ([https://hackage.haskell.org/package /adp-multi adp-multi]) is a parsing library for running dynamic programming algorithms with sequences as input (used in bioinformatics to fold RNA secondary structures). The grammar is defined as a DSL where some syntax sugar is defined using type class instances. One of the two problematic instances is the following (simplified): {{{ {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DeriveDataTypeable #-} -- | To support higher dimensions, a subword is a list -- of indices. Valid list lengths are 2n with n>0. type Subword = [Int] type Parser a b = Array Int a -- ^ The input sequence -> Subword -- ^ Subword of the input sequence to be parsed -> [b] -- ^ Parsing results class Parseable p a b | p -> a b where toParser :: p -> Parser a b data EPS = EPS deriving (Eq, Show, Data, Typeable) empty1 :: Parser a EPS empty1 _ [i,j] = [ EPS | i == j ] instance Parseable EPS a EPS where toParser _ = empty1 }}} See [https://github.com/adp-multi/adp- multi/blob/0.2.3/src/ADP/Multi/ElementaryParsers.hs#L152 here] and [https://github.com/adp-multi/adp-multi/blob/0.2.3/src/ADP/Multi/Parser.hs here] for the full code. The error with 7.8 is: {{{ Illegal instance declaration for ‘Parseable EPS a EPS’ The liberal coverage condition fails in class ‘Parseable’ for functional dependency: ‘p -> a b’ Reason: lhs type ‘EPS’ does not determine rhs types ‘a’, ‘EPS’ In the instance declaration for ‘Parseable EPS a EPS’ }}} The other problematic instance is basically the same but for 2D inputs. In essence I want the empty word parser empty1 to work for any input type, e.g. for a char but also a number (which would then be a list of chars or numbers as the input sequence). Am I doing something terribly wrong or does this ticket also apply to me? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:46 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by syallop): Replying to [comment:46 neo]:
Hi! I'm not sure if I face the same problem as the issue author or if my code is just "wrong" but when testing my code with GHC 7.8 I get the [https://travis-ci.org/adp-multi/adp-multi/jobs/34132805#L437 same error] while it worked with 7.6. I believe you do. I can confirm that your code compiles with -XDysfunctionalDependencies.
-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:47 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by emertens): Replying to [comment:46 neo]: Your instance `instance Parseable EPS a EPS` fails to satisfy the function dependency `p -> a b` because the `a` can not be determined from `EPS`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:48 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by goldfire): What's the status on this ticket? I'm still eager to see this merged, and other than regression tests, the patch seems to be in decent shape. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:49 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by simonpj): Situation is this. In comment:30 I show (using Martin's example) that lifting the liberal coverage condition (which is what `-XDysFunctionalDependencies` proposes to do) means that type inference becomes unpredicatable. On Monday it might succeed, but after a minor change to the order in which constraints are examined, on Tuesday it might fail. This is not a happy situation. I did not realise this when I wrote comment:14. On the other hand, danilo2 (I wish I knew your real name) is saying strongly that `=XDysFunctionalDependencies` would really help him. It is possible that his problem could be solved in some other way, but that would take a serious investment of time to find out, and danilo2 believes not. So what to do? We could treat it like `unsafeCoerce`: you can use it, but then you are on your own. (Maybe it should have an even more discouraging name e.g. `-XUnpredicatbleFunctionalDependencies`.) I worry, though, that people will bump into problems, and submit bug reports, ... Any other opinions? danilo2, are you still arguing for this despite the difficulties? Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:50 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by danilo2): Hello Simon, Goldfire! Answering your question Simon - my name is Wojciech Daniło :) The situation you describe is really dangerous. Still - I and some people I'm working with belive that `-XDysfunctionalDependencies` would help us. Even more - this is crutial for the project to work and we are using this flag in very specific situations. But there is one more thing to note about our situation. Right now we are using Haskell as a backend to our language. Some specific features are very hard to reach in Haskell so we are slowly moving over our own type checker and compilation directly to Haskell core. If we succeed, we would not need this extension anymore. But this will not happen in very near future and for now this is crutial for the project we are working on. I would vote for treating `-XDysfunctionalDependencies` as `unsafeCoerce` for now and writing in the documentation that it is very dangerous. This way we can limit incorrect bug reports etc. Do you think it makes sense? Wojciech -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:51 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by goldfire): About unpredictability: I think this is quite similar to `IncoherentInstances`, where, I believe, similar unpredictability exists. A notable difference here is that `DysfunctionalDependencies` would introduce compile-time unpredictability. I would say, though, that it is up to the user to make sure that their dysfunctional dependencies are confluent w.r.t. the equivalence relation that is relevant to them -- which might not be `(~)`. So, I think there's support for this feature. What needs to be done to merge? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:52 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by simonpj): OK, fine, let's do it. Perhaps Wojciech can address my comments in Prabricator. And add a couple of regression tests, culled from this ticket. Most important, I think the user manual needs a sub-section explaining the consequences of `DysFunctionalDependencies`, with pointers to further details (e.g. this ticket). Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:53 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by danilo2): Simon, I would love to and I would do it. I just need some help - if anybody could give me some informations - where are these regression tests and what exactly should I add, I would do it with pleasure :) I was looking for it for a limited time (because of huge amount of work) but with some tips I will add them as fast as possible :) Help with writing this documentation section would also be needed - especially when talking about consequences according to how GHC works internally. Wojciech -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:54 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by goldfire): This [wiki:Building/RunningTests/Adding wiki page] tells you how to add test cases. As for documentation, you should edit `docs/users_guide/glasgow_exts.xml`. The format there is that for DocBooks, but it's easy enough just to parrot the code that's in there. Is this enough guidance? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:55 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by danilo2): Goldfire - I would do it as fast as possible. But first I have to solve an issue I've got here at the company I'm working at. It is connected to injective type families (if I'm not wrong). Anyway it shows, that we cannot do something in Haskell, which should be doable in my opinion. I would be very thankful if you Goldfire or Simon just look at it and give maybe any hints how can we solve it: http://stackoverflow.com/questions/25854072/injective-type-families-in- haskell After solving it I will start working on the tests asap. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:56 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: | Related Tickets: #1241, #2247, None/Unknown | #8356, #9103, #9227 Test Case: | Blocking: | Differential Revisions: Phab:D69 | -------------------------------------+------------------------------------- Comment (by goldfire): I've responded to that !StackOverflow post. (By the way, my name is Richard Eisenberg -- I have no intent on hiding my identity behind the name "goldfire".) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:57 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #1241, #2247, | Blocking: #8356, #9103, #9227 | Differential Revisions: Phab:D69 -------------------------------------+------------------------------------- Changes (by dfeuer): * milestone: 7.10.1 => 7.12.1 Comment: This is fairly obviously not going to happen in a feature freeze. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:58 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #1241, #2247, | Blocking: #8356, #9103, #9227 | Differential Revisions: Phab:D69 -------------------------------------+------------------------------------- Comment (by atnnn): What is the status of this feature? I ran into another case where it might be useful: {{{#!hs {-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances, ConstraintKinds, GADTs #-} class F a | -> a instance (eq ~ (a ~ ()), eq) => F a }}} GHC considers this illegal, but in practice it satisfies the functional dependency. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:59 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #1241, #2247, | Blocking: #8356, #9103, #9227 | Differential Revisions: Phab:D69 -------------------------------------+------------------------------------- Comment (by simonpj): It looks stalled to me. Wojciech was going to work on some aspects (notably making the pragma work per-instance rather than globally) but nothing has happened. I'm happy to advise anyone who wants to take up the cudgels here. It's not too hard, despite this very long thread. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:60 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #1241, #2247, | Blocking: #8356, #9103, #9227 | Differential Revisions: Phab:D69 -------------------------------------+------------------------------------- Comment (by rwbarton): Replying to [comment:59 atnnn]:
What is the status of this feature?
I ran into another case where it might be useful:
{{{#!hs {-# LANGUAGE FunctionalDependencies, FlexibleInstances, UndecidableInstances, ConstraintKinds, GADTs #-}
class F a | -> a instance (eq ~ (a ~ ()), eq) => F a }}}
I guess this is a reduction of some more non-trivial instance declaration? Otherwise one could just write `instance (a ~ ()) => F a`, and this is accepted by GHC.
GHC considers this illegal, but in practice it satisfies the functional dependency.
In principle it looks to be a bug that GHC does not accept your program already, and it would continue to be a bug even if `DysfunctionalDependencies` was added; but in practice obscure fundep- related bugs are not always fixed quickly. Still, I think you should probably file this as a separate ticket. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:61 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #1241, #2247, | Blocking: #8356, #9103, #9227 | Differential Revisions: Phab:D69 -------------------------------------+------------------------------------- Comment (by rwbarton): Some thoughts upon returning to this ticket after a long time. * Is there a wiki page or similar describing the meaning of functional dependencies under `DysfunctionalDependencies`? I think I understand the meaning in the case of `class C a b | a -> b`: I think the condition is that for any type `a0`, there is at most one ''instance declaration'' `instance C a[vs] b[vs]` for which `a[vs]` unifies with `a0`, but this unification may not fully determine `b[vs]`. But I don't know what it means to write a dysfunctional dependency like `class C a b c | a -> b`. How does that differ from the dependency `a c -> b`? * Would adding `DysfunctionalDependencies` get in the way of some day desugaring functional dependencies into type families, and removing the fundep solver code? (Is this likely to ever happen anyways?) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:62 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

* Is there a wiki page or similar describing the meaning of functional dependencies under `DysfunctionalDependencies`? I think I understand the meaning in the case of `class C a b | a -> b`: I think the condition is
#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #1241, #2247, | Blocking: #8356, #9103, #9227 | Differential Revisions: Phab:D69 -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:62 rwbarton]: that for any type `a0`, there is at most one ''instance declaration'' `instance C a[vs] b[vs]` for which `a[vs]` unifies with `a0`, but this unification may not fully determine `b[vs]`. But I don't know what it means to write a dysfunctional dependency like `class C a b c | a -> b`. How does that differ from the dependency `a c -> b`? My understanding of `DysfunctionalDependencies` is much, much simpler: just omit the check that takes place at instance declarations. For example, the following would be accepted: {{{ class Terrible a b | a -> b instance Terrible Int Bool instance Terrible Int Char }}} Now, suppose we have {{{ foo :: Terrible a b => a -> b foo = undefined }}} and we call `show (foo (5 :: Int))`. GHC has to figure out what type the argument to `show` has so it can supply the right `Show` instance. In this case, the type inferred for `foo (5 :: Int)` will either be `Bool` or `Char`, depending on the whims of GHC at the moment. They're called dysfunctional for a reason! Nevertheless, they can be useful if the user is careful to construct a set of instances that isn't terrible, but still doesn't meet the liberal coverage condition. Much like with `IncoherentInstances`, it's up to the user not to shoot themselves in the foot.
* Would adding `DysfunctionalDependencies` get in the way of some day
desugaring functional dependencies into type families, and removing the fundep solver code? (Is this likely to ever happen anyways?) This is a good point. The only reason I'm not against `DysfunctionalDependencies` is that I know functional dependencies don't make it into Core, and so you can't use this feature to write `unsafeCoerce`. But if we did desugar functional dependencies into something that does exist in Core, `DysfunctionalDependencies` would be in deep water. Is this a reason to avoid writing the feature? Perhaps. It certainly gives me pause when thinking about it. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:63 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: high | Milestone: 7.12.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: #1241, #2247, | Blocking: #8356, #9103, #9227 | Differential Revisions: Phab:D69 -------------------------------------+------------------------------------- Comment (by simonpj):
Is there a wiki page or similar describing the meaning of functional dependencies under `DysfunctionalDependencies`?
See the end of comment:14. This stuff needs to end up in the user manual though. It's a simple, easily-specified change. I don't think we should hold it up because of a vague aspiration to implement fundeps in terms of type families; I'm sure there will be lots of ''other'' wrinkles to that. I would much prefer it done as a '''per-instance''' pragma, since we now have the technology to do that, rather than as a module-wide pragma. All it needs is for someone to do it. I'm happy to advise. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:64 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler | Version: 7.7 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by bgamari): * priority: high => normal * milestone: 8.0.1 => 8.2.1 Comment: This won't be happening in 8.0. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:66 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: Type: feature request | Status: new Priority: normal | Milestone: 8.2.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by dfeuer): I think Simon's suggestion in [comment:30 comment 30] of a different notation for not-really-functional suggestions is much better than the per-instance pragma. Thus {{{#!hs class Foo a b c | a b -> c, a c ~> b }}} would clearly indicate that `a` and `b` must solidly determine `c`, but that the type checker is free to guess `b` based on `a` and `c` when it thinks it needs to. One thing to note is that, as shown in [http://stackoverflow.com/a/35413064/1477667 this answer] to a related question I asked recently, functional dependencies are ''already'' dysfunctional. In particular, module import diamonds can lead to undetected fundep violations. I'd personally like to see the following: 1. Add a "soft dependency" `~>` as described. 2. Plug the module diamond loophole. 3. Translate fundeps into type families in core, so that `class Bar a b | a -> b` will let me write `funBar :: (Bar a b, Bar a b') => b :~: b'`. The translation could even be ''exposed'' by an extension, I imagine, so that `__Bar_1_DETERMINES_2` (or whatever) would be a usable type family. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:68 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Changes (by rwbarton): * milestone: 8.2.1 => 8.4.1 -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:69 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:63 goldfire]: Hi Richard, I think we're already (at GHC 7.10/8.0) pretty close to being able to write your `class Terrible`.
{{{ class Terrible a b | a -> b instance Terrible Int Bool instance Terrible Int Char }}}
See Iavor's example comment:12:ticket:10675. Or this https://mail.haskell.org/pipermail/glasgow-haskell- users/2017-April/026507.html . Both examples rely on `UndecidableInstances` and overlaps. Not necessrily `OverlappingInstances`: in Iavor's example, the FunDeps are non-full.
{{{ foo :: Terrible a b => a -> b foo = undefined }}}
and we call `show (foo (5 :: Int))`. GHC has to figure out what type the
argument to `show` has so it can supply the right `Show` instance. In this case, the type inferred for `foo (5 :: Int)` will either be `Bool` or `Char`, depending on the whims of GHC at the moment. In those examples I cited, GHC does make a predictable choice (so not entirely on a whim). But it's inconsistent between the FunDeps, so very sensitive to subtle changes in (apparently) unrelated parts of the program/some distant module. For example, merely adding a type signature could trigger selecting a different instance.
... Much like with `IncoherentInstances`, it's up to the user not to shoot themselves in the foot.
With a great deal of hindsight, what `Undecidable` means in these cases is: * The type specified in the instance head isn't mechanically derivable from the other type parameters. So the programmer is saying "trust me, at any use site, you'll be able to figure out the right type". * GHC can't follow the trail of instance constraints/instantiation -- especially because it might need looking at other modules and/or a very long chain. * So `Undecidable` means GHC can't/won't decide whether any given FunDep is instantiated consistently across all the instances. I'm not sure that's abundantly well explained in the docos. OTOH, there's some type-level programming that deliberately exploits that inconsistency -- such as anything that despatches on a type-level type-equality condition (the whole of the HList library, as originally developed). Closed type families is nowadays a much more hygienic mechanism. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:70 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:34 danilo2]: Hi Wojciech/all, this ticket seems to have been stalled for some time. Is it still causing anybody pain? Did something get better in a later release? I've tried to wade through the comments, but I'm left very unsure what the proposal is, or what are the use cases. To look at your proposed test code. (https://phabricator.haskell.org/D69 has a smaller example.) Either the code is not actually testing for how D69 is to change behaviour, or there's already a (simpler?) way to achieve it.
... I will try to put here another one, a little more complex: {{{#!haskell {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DysfunctionalDependencies #-}
class Property a b | a -> b where property :: a -> b
data X = X data Y = Y
instance Monad m => Property X Y where property _ = Y
instance Monad m => Property Y (m Int) where property _ = return 5
main = do let f = property $ property X }}}
Your O.P. included a Monad as one of the params to the class, and it was determined from the first param. Here the Monad seems to materialise out of thin air. In your first `instance` it's not even used. In the second instance it seems that could be any Monad at all(?) If your class is usually non-monadic, but you happen to use method `property` inside monadic code, you could just wrap the call in `return`. If your class is usually monadic, but you happen to need `property` in a non-monadic context, you could wrap it in the the `Identity` monad and extract the result(?) See my comment:70 above/examples. With `UndecidableInstances` there seems to be plenty of ways to evade the Consistency Condition. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:71 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:63 goldfire]:
My understanding of `DysfunctionalDependencies` is much, much simpler:
just omit the check that takes place at instance declarations. For example, the following would be accepted: Hereby confirming we can write Richard’s class `Terrible` today [GHC 8.0.1]. Of course not directly like this:
{{{ class Terrible a b | a -> b instance Terrible Int Bool instance Terrible Int Char }}}
“Instances inconsistent with Functional Dependency”. But we can abuse GHC’s "bogus consistency check" ticket:10675#comment:15. {{{ {-# LANGUAGE UndecidableInstances, … #-} class Terrible2 a b | a -> b instance {-# OVERLAPS #-} Terrible2 Int Bool instance {-# OVERLAPS #-} (b ~ Char) => Terrible2 Int b }}} If the usage site gives you wanted `b ~ Bool`, this uses the first instance. Otherwise it selects the second instance and improves to `b ~ Char`.
{{{ foo :: Terrible a b => a -> b foo = undefined }}}
and we call `show (foo (5 :: Int))`. GHC has to figure out what type the
argument to `show` has so it can supply the right `Show` instance. In this case, the type inferred for `foo (5 :: Int)` will either be `Bool` or `Char`, depending on the whims of GHC at the moment. They're called dysfunctional for a reason!
Want to choose one of those instances arbitrarily, in the absence of any wanted for `b`? Then just change the pragmas to `{-# INCOHERENT #-}`. You have more possible instances? Then repeat the trick. Instead of that second instance: {{{ instance {-# INCOHERENT #-} (Terrible3 Int b) => Terrible2 Int b class Terrible3 a b | a -> b instance {-# INCOHERENT #-} Terrible3 Int Char instance {-# INCOHERENT #-} (Terrible4 Int b) => Terrible3 Int b -- context gives you the constructor only? Then you can improve the content: class Terrible4 a b | a -> b instance {-# INCOHERENT #-} (b’ ~ String) => Terrible4 Int (Maybe b’) instance {-# INCOHERENT #-} (Terrible5 Int b) => Terrible4 Int b }}} This is a (verbose) way to achieve a Closed Class. The thing we can’t get is per @Danilo’s O.P. with a free type var: {{{ class Terrible5 a b | a -> b instance {-# INCOHERENT #-} (out ~ (t1 -> t1)) => Terrible5 Int out }}} Too liberal even for the Liberal Coverage Conditions. Perhaps if there’s a known set of choices for `t1` we could write out a class/instance for each? (With a default improvement at the end of the chain.) It's difficult to see this is any genuine variety of `FunDep`. It just evades the error you'd get in `show ( foo (5 :: Int) )` about an ambiguous type. I suppose we're lucky GHC has never applied the rule (from the original FunDeps paper) that if we have `Terrible Int b1` and `Terrible Int b2` then `b1 = b2` (that's identical types, not merely unifiable -- not that they're even unifiable for `Terrible`). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:72 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#8634: Relax functional dependency coherence check ("liberal coverage condition") -------------------------------------+------------------------------------- Reporter: danilo2 | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: 8.8.1 Component: Compiler (Type | Version: 7.7 checker) | Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #1241, #2247, | Differential Rev(s): Phab:D69 #8356, #9103, #9227 | Wiki Page: | -------------------------------------+------------------------------------- Comment (by ByteEater): Is it possible to separate the parts requiring 7.6 behaviour and the newest Accelerate which requires at least 7.8 and compile them separately with different versions of GHC, then link? If so, would it be a viable solution for you, Wojciech (@danilo2)? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8634#comment:75 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC