Opened 6 years ago

Last modified 10 months ago

#8634 new feature request

Relax functional dependency coherence check ("liberal coverage condition")

Reported by: danilo2 Owned by:
Priority: normal Milestone: 8.10.1
Component: Compiler (Type checker) Version: 7.7
Keywords: Cc: diatchki, martin.sulzmann@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #1241, #2247, #8356, #9103, #9227 Differential Rev(s): Phab:D69
Wiki Page:

Description

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):

  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):

    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:

    {-# 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:

    class Method1 cls m func | cls -> m where 
        method1 :: cls -> m func

Which resolves the problem with functional dependencies, but then the line:

    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):

    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

Change History (76)

comment:1 Changed 6 years ago by rwbarton

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.)

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

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.

comment:2 Changed 6 years ago by rwbarton

Perhaps the option to emulate the GHC 7.6 behavior could be called -XDysfunctionalDependencies.

comment:3 in reply to:  1 Changed 6 years ago by danilo2

Replying to 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.

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.

I'll read them, thank you.

As for how to fix your program: it's hard to see what's going on with 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):

{-# 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:

"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

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 making it off is your responsibility :)

Last edited 6 years ago by danilo2 (previous) (diff)

comment:4 Changed 6 years ago by rwbarton

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.

That doesn't seem to be a problem, as those will be instances of different classes Method2, Method3.

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.

comment:5 in reply to:  4 Changed 6 years ago by danilo2

Replying to 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 "Vector 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:

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.

Last edited 6 years ago by danilo2 (previous) (diff)

comment:6 in reply to:  4 Changed 6 years ago by danilo2

Replying to 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):

{-# 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:

"test"
"default string"
"test"

comment:7 Changed 6 years ago by goldfire

Summary: Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition)Relax functional dependency coherence check ("liberal coverage condition")
Type: bugfeature request

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.

comment:8 Changed 5 years ago 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 :)

This feature is very important to us. We are planning release of our software in 2 months from now and we have to use GHC-7.8.x (because we are using the newest Accelerate, which needs higher version than 7.6), but on the other hand we need -XDysfunctionalDependencies in one, specific place of our system and this is crutial for us. Is it possible to implement this feature in near future?

Edit: Ahh - it was not planned for 7.7, I'm sorry - I overlooked the information tab. Anyway I would love to know more about the progress and further possibilities :)

Last edited 5 years ago by danilo2 (previous) (diff)

comment:9 Changed 5 years ago by thoughtpolice

Milestone: 7.10.1

comment:10 Changed 5 years ago by goldfire

See also an attempt to implement this: https://phabricator.haskell.org/D69

Last edited 5 years ago by goldfire (previous) (diff)

comment:11 Changed 5 years ago 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.

comment:12 Changed 5 years ago by simonpj

comment:13 Changed 5 years ago by thoughtpolice

Differential Rev(s): Phab:D69

comment:14 Changed 5 years ago by simonpj

Provoked by this ticket, and other recent ones (#9227, #9103) I’ve taken another look. Here are my preliminary conclusions.

  • The 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 the following, which is exactly what https://phabricator.haskell.org/D69 proposes. Namely: that the behaviour for the Coverage Condition (see user manual) should be:

  • 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.

Last edited 5 years ago by simonpj (previous) (diff)

comment:15 Changed 5 years ago by simonpj

comment:16 Changed 5 years ago 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.

comment:17 Changed 5 years ago by simonpj

Cc: diatchki martin.sulzmann@… added

Martin, Iavor, I'd welcome feedback about the proposed course of action in comment:14 above. Thanks!

Simon

comment:18 Changed 5 years ago 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.

comment:19 Changed 5 years ago 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 -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 the one I've posted on https://phabricator.haskell.org/D69 :

{-# 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]
Last edited 5 years ago by danilo2 (previous) (diff)

comment:20 in reply to:  18 Changed 5 years ago by goldfire

Replying to diatchki:

No matter which rule we use to implement the consistency check for 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.

comment:21 Changed 5 years ago 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

comment:22 Changed 5 years ago by simonpj

See also #9267 for an interesting example.

comment:23 Changed 5 years ago by danilo2

@goldfire, you are right - I fixed my comment, thank you :)

comment:24 Changed 5 years ago 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.

comment:25 Changed 5 years ago 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

comment:26 Changed 5 years ago 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.
Last edited 5 years ago by simonpj (previous) (diff)

comment:27 Changed 5 years ago by danilo2

I've got a single question related to this topic - lets assume I've got a simple code:

{-# 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 one of the cases we need to use it right now (of course very simplified). For now it works for us very well even for large examples (passing all tests etc.). When such code "could" break and give us unpredictable results?

Last edited 5 years ago by danilo2 (previous) (diff)

comment:28 Changed 5 years ago 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).

comment:29 Changed 5 years ago 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 :)

comment:30 Changed 5 years ago 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:

  1. 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.
  1. 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.

comment:31 in reply to:  19 Changed 5 years ago 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 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 -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 the one I've posted on https://phabricator.haskell.org/D69 :

{-# 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]

comment:32 in reply to:  25 Changed 5 years ago 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 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

comment:33 Changed 5 years ago 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.

comment:34 Changed 5 years ago 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:

{-# 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.

comment:35 Changed 5 years ago 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)

comment:36 Changed 5 years ago by danilo2

@emertens: I know it really well, it would not work - look at this example:

{-# 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:

    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 :)

Exactly this problem told how the -XOverloadedRecordFields would be implemented (see: https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields?redirectedfrom=Records/OverloadedRecordFields/Plan) There are some documents why we have to use fundeps in such cases, like the one here: https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Design:

"[...] ​Edward Kmett points out that a previous version of this proposal, where the third parameter of the Has class was not functionally dependent on the first two, fell short in an important respect: composition of polymorphic record fields would lead to ambiguity errors, as the intermediate type cannot be determined. [...]"

This is exactly the same case as above. Of course -XOverloadedRecordFields does not need -XDysfunctionalDependencies, because this extension assumes, that all of the recotrds are parametrized with all type variables needed by the result type. In case of our system (the one developed by the company I'm working in) this assumption is not valid and we have to use the extension.

Still, I want to emphasize, that we are using it right now in a core part of our project (over 600 haskell files - just to show you it is pretty big) and it works great. We were developing the project using GHC 7.6 and then -XUndecidableInstances flag was lifting both Paterson and full Coverage condition! So right now the flag -XUndecidableInstances together with -XDysfunctionalDependencies works the same way as -XUndecidableInstances in GHC 7.6.

Last edited 5 years ago by danilo2 (previous) (diff)

comment:37 Changed 5 years ago 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.

comment:38 in reply to:  37 Changed 5 years ago by danilo2

Replying to rwbarton: It still would not work: 1) the following script does not compile 2) I really DO NOT want ambigous types and 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:

{-# 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)

Last edited 5 years ago by danilo2 (previous) (diff)

comment:39 Changed 5 years ago 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).

comment:40 in reply to:  39 Changed 5 years ago by danilo2

Replying to 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.

comment:41 Changed 5 years ago 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:

{-# 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:

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?

comment:42 in reply to:  41 Changed 5 years ago by danilo2

Replying to 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:

    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:

{-# 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

Of course I see what you were trying to do, but I think this ambiguity appears with the line of b <- y a. Then we can just shuffle Morph isntances and found more than 1 matching set.

Still, I completely agree with all the things you stated in your post.

Last edited 5 years ago by danilo2 (previous) (diff)

comment:43 Changed 5 years ago 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?

comment:44 Changed 5 years ago 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.

comment:45 Changed 5 years ago by danilo2

@goldfire: First of all - yes, this is the error, which appears after enabling -XDysfunctionalDependencies and including your instance. Please note, that current implementation of -XDysfunctionalDependencies ommits only checking for LCC, so it should theoretically work as -XUndecidableInstances in GHC-7.6 (so you could get the same error there).

Another topic is the error and why it appears there. So the code

f x y z = do a <- x
             b <- y a
             z b

is equivalent to

f x y z = x >>= (\a ->
              y a >>= (\b ->
                 z b
             ))

and going further (rebindable):

f x y z = morph x `bind` (morph . (\a ->
              morph (y a) `bind` (morph . (\b ->
                 z b
             ))))

And now we've got some interesting fragments here:

morph (y a) `bind` (morph . (\b -> z b))

tells that result of y a should be morphed to a monad m1, which is the same as monad of (morph . (\b -> z b)). Thats ok for now!

[example] Following functions compile just fine:

f x y z = do a <- x
             z a
f x y z = do b <- y x
             z b

[end of example] Going back to our problem: we know, that type of morph (y a) bind (morph . (\b -> z b)) is :: m1 _ (the wildcard is just to show, that I'm not interested in the tvar). Interesting part is here morph x bind (morph . (\a -> undefined :: m1 _)), because x is morphed to monad m2 and m1 is also morphed to the same monad. The only problem is, that m1 is already morphed monad (starting with some monad m0). And because of open world assumption there is situation, that there does not exist single way of converting m0 into m2 (becasue we can achive it by different m1!). So your code just cannot work, but we can fix it easly (by the way - I'm doing something simmilar in my work now). But before that, I would love to show another form of f:

f x y z = morph x `bind` (\a ->
              morph (morph (y a) `bind` (\b -> 
                  morph (z b) 
          )))

which even better shows the double morph problem.

Going back to the possible implementation. We can make this code running only If we know, some kind of "default morphism" for specific monads. Lets assume, we've got monad Pure which is just opposite of IO. hen our code looks like this one:

{-# LANGUAGE RebindableSyntax, MultiParamTypeClasses, FlexibleInstances,
             AllowAmbiguousTypes, FunctionalDependencies, UndecidableInstances, NoMonomorphismRestriction #-}

module PolyMonad where

import Prelude hiding ((>>=))
import qualified Prelude as P


newtype Pure a = Pure { fromPure :: a } deriving Show

instance Monad Pure where
    return         = Pure
    (Pure a) >>= f = f a

class (Monad m1, Monad m2, Monad m3) => MatchMonad m1 m2 m3 | m1 m2 -> m3 where
    matchMonad :: m1 a -> (a -> m2 b) -> m3 b

instance MatchMonad Pure Pure Pure where
    matchMonad (Pure a) f = f a

instance MatchMonad Pure IO IO where
    matchMonad (Pure a) f = f a

instance MatchMonad IO IO IO where
    matchMonad ma f = do
        a <- ma
        f a

instance MatchMonad IO Pure IO where
    matchMonad ma f = ma P.>>= (\a -> return . fromPure $ f a)

(>>=) = matchMonad

f x y z = do a <- x
             b <- y a
             z b

Maybe there is more general way. I see what you were trying to get - a slighty more general solution, but I do not see how we can achive it without adding further type signatures to the morph calls. Please note, that I do NOT use -XDysfunctionalDependencies above. Does it make sense?

Last edited 5 years ago by danilo2 (previous) (diff)

comment:46 Changed 5 years ago 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 same error while it worked with 7.6. My library (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 here and 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?

Last edited 5 years ago by neo (previous) (diff)

comment:47 in reply to:  46 Changed 5 years ago by syallop

Replying to 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 same error while it worked with 7.6.

I believe you do. I can confirm that your code compiles with -XDysfunctionalDependencies.

comment:48 in reply to:  46 Changed 5 years ago by emertens

Replying to 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.

comment:49 Changed 5 years ago 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.

comment:50 Changed 5 years ago 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

comment:51 Changed 5 years ago 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 (we are working on) to succeed 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

Last edited 5 years ago by danilo2 (previous) (diff)

comment:52 Changed 5 years ago 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?

comment:53 Changed 5 years ago 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

comment:54 Changed 5 years ago 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

comment:55 Changed 5 years ago by goldfire

This 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?

comment:56 Changed 5 years ago 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.

comment:57 Changed 5 years ago 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".)

comment:58 Changed 5 years ago by dfeuer

Milestone: 7.10.17.12.1

This is fairly obviously not going to happen in a feature freeze.

comment:59 Changed 4 years ago by atnnn

What is the status of this feature?

I ran into another case where it might be useful:

{-# 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.

comment:60 Changed 4 years ago 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

comment:61 in reply to:  59 Changed 4 years ago by rwbarton

Replying to atnnn:

What is the status of this feature?

I ran into another case where it might be useful:

{-# 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.

comment:62 Changed 4 years ago 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?)

comment:63 in reply to:  62 ; Changed 4 years ago by goldfire

Replying to rwbarton:

  • 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?

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.

comment:64 Changed 4 years ago 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

comment:65 Changed 4 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:66 Changed 4 years ago by bgamari

Milestone: 8.0.18.2.1
Priority: highnormal

This won't be happening in 8.0.

comment:67 Changed 4 years ago by thomie

Component: CompilerCompiler (Type checker)

comment:68 Changed 4 years ago by dfeuer

I think Simon's suggestion in comment 30 of a different notation for not-really-functional suggestions is much better than the per-instance pragma. Thus

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 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.

comment:69 Changed 3 years ago by rwbarton

Milestone: 8.2.18.4.1

comment:70 in reply to:  63 Changed 3 years ago by AntC

Replying to 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.

comment:71 in reply to:  34 Changed 3 years ago by AntC

Replying to 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:

{-# 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.

comment:72 in reply to:  63 Changed 2 years ago by AntC

Replying to 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).

comment:73 Changed 21 months ago by bgamari

Milestone: 8.4.18.6.1

This ticket won't be resolved in 8.4; remilestoning for 8.6. Do holler if you are affected by this or would otherwise like to work on it.

comment:74 Changed 16 months ago by bgamari

Milestone: 8.6.18.8.1

This won't be fixed in 8.6. Bumping to 8.8.

comment:75 Changed 11 months ago 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)?

comment:76 Changed 10 months ago by osa1

Milestone: 8.8.18.10.1

Bumping milestones of low-priority tickets.

Note: See TracTickets for help on using tickets.