Weird Undecidable Instances Bug

[Martin Sulzmann]

 > original, "g" is actually a method in a class, and its definition is in 
 > an instance declaration. Its type is actually given, not annotated. For 
 > instance:
 > 

Ah, g is meant to be a method. Well, ...

 > -- ghc -fglasgow-exts -fallow-undecidable-instances -c WeirdInsts.hs
 > module WeirdInsts where
 > 	{
 > 	data T r = MkT;
 > 
 > 	class C t;
 > 
 > 	class D b t;
 > 
 > 	instance (C (T r)) => D b (T r); -- (1)
 > 
 > 	class F a b | a -> b;
 > 
 > 	f :: (F a b,D b t) => (a,t);
 > 	f = undefined;
 > 
 > 	class G t where
 > 		{
 > 		g :: forall a b. (F a b,D b t) => (a,t);
 > 		};
 > 
 > 	instance G (T r) where
 > 		{
 > 		g = f;
 > 		};
 > 	}
 > 
 > This exhibits the same behaviour.

... not quite. Cause we never can improve class declarations.

The short answer is, the above code won't type check in
a compilation-based evidence translation scheme. 
(There are no issues with decidable inference etc.)

Reason:

g's method declaration (i.e. annotation) is too general.
When type checking the instance, we need to check for

(F a' b',D b' t') => (a',t')

 "subsumes"

(F a b,D b (T r)) => (a,t)

(foralls are implicit)

In a compilation-based evidence translation scheme this check fails.
(BTW, there were similar problems mentioned when trying to define Monad2
instances some time ago on Haskell mail).

There are two solutions:

(1)
In an interpreter-based evidence translation scheme this
check would succeed. (i.e. we only
construct evidence at run-time, though this requires to pass around
run-time type information, see "A Theory of Overloading", journal
version, for details
http://www.comp.nus.edu.sg/~sulzmann/chr/publications.html)

(2) 
We need to find a different encoding. In essence, we need to give
up the class declaration. 

That is, we first generate

class G a where g :: a

instance (F a b, D b (T r)) => G (a, T r) where
   g = f

however, this won't work either, same problem as before.
Additionally, we need to improve
the instance (an instance is nothing else than a type annotation).
Finally, the following works

class G a where g :: a
instance (F a b, C (T r)) => G (a, T r) where
    g = f

Martin