Liberal coverage condition introduced in GHC 7.7 breaks code valid in GHC 7.6
The idea
I'm writing a DSL, 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 (which is pre-release of 7.8) (Newer versions can be compiled from sources). 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
EDIT:
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)
This is not a bug in GHC 7.7. It was a long-standing bug in GHC when it allowed instances that violate functional dependencies. It seems, fortunately, that this problem is finally fixed. The error message emitted by GHC 7.7 is quite detailed, pointing out the problem with your instance Method1 (Vector a) Vector_testid out . Recall the meaning of functional dependencies. Given
class C a b | a -> b
it follows that if the types a , b and b1 are such that C ab and C a b1 both hold, it must be true that b and b1 are the same. Let's look at your instance:
Method1 (Vector a) Vector_testid (t1->t1)
If we have types b and b1 that satisfy Method1 (Vector Int) Vector_testid (b->b) and Method1 (Vector a) Vector_testid (b1->b1) , nothing at all implies that b and b1 must be the same. Hence your instance is ill-formed. The fact that GHC 7.6 and before accepted the program was a well-known bug in GHC (discussed about every year).
What you seem to be trying is to define something like
Method1 (Vector a) Vector_testid (forall t. t -> t)
Alas, this syntax is not allowed, although many worksrounds exist. One, for example, involves the Apply class (see the HList paper, for example). A simpler way is as follows
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
-- import Data.Tuple.OneTuple
newtype OneTuple x = OneTuple x deriving Show
------------------------------
-- data types
------------------------------
data Vector a = Vector {x :: a, y :: a, z :: a} deriving (Show)
-- testx x = call (method1 x) $ OneTuple "test"
testx x = call x Method1 $ OneTuple "test"
-- associate methods to classes
class Methods cls m x y | cls m x -> y where
call :: cls -> m -> x -> y
instance Methods (Vector a) Method1 x x where
call self _ x = x
data Method1 = Method1 -- method label
上一篇: 对'类型'的迷惑