Opened 4 months ago

Last modified 2 months ago

#8634 new feature request

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

Reported by: danilo2 Owned by:
Priority: high Milestone:
Component: Compiler Version: 7.7
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Difficulty: Unknown
Test Case: Blocked By:
Blocking: Related Tickets: #1241, #2247, #8356

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

comment:1 follow-up: Changed 4 months 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 4 months ago by rwbarton

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

comment:3 in reply to: ↑ 1 Changed 4 months 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 4 months ago by danilo2 (previous) (diff)

comment:4 follow-ups: Changed 4 months 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 4 months 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 4 months ago by danilo2 (previous) (diff)

comment:6 in reply to: ↑ 4 Changed 4 months 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 2 months ago by goldfire

  • Summary changed from Code valid in GHC 7.6 is impossible to move over GHC 7.7 (because of liberal coverage condition) to Relax functional dependency coherence check ("liberal coverage condition")
  • Type changed from bug to feature 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.

Note: See TracTickets for help on using tickets.