Problem with functional dependencies

[Simon Peyton-Jones]

I think you can simplify the example.  Given

	class HasFoo a b | a -> b where
	  foo :: a -> b

	instance HasFoo Int Bool where ...

Is this legal?

	f :: HasFoo Int b => Int -> b
	f x = foo x

You might think so, since 
	HasFoo Int b => Int -> b
is a substitution instance of
	HasFoo a b => a -> b

but if we infer the type (HasFoo Int b => Int -> b)
for f's RHS, we can then "improve" it using the instance
decl to (HasFoo Int Bool => Int -> Bool), and now the signature
isn't a substitution insance of the type of the RHS.  Indeed,
this is just what will happen if you try with GHC, because
GHC takes advantage of type signatures when typechecking a 
function defn, rather than first typechecking the defn and only
then comparing with the signature.

I don't know what the answers are here, but there's more to this
functional dependency stuff than meets the eye.  Even whether
one type is more general than another has changed!

Simon

| -----Original Message-----
| From: qrczak@knm.org.pl [mailto:qrczak@knm.org.pl]
| Sent: 17 December 2000 19:30
| To: haskell@haskell.org
| Subject: Problem with functional dependencies
| 
| 
| The following module is rejected by both
|     ghc -fglasgow-exts -fallow-undecidable-instances
| and
|     hugs -98
| 
| --------------------------------------------------------------
| ----------
| class HasFoo a foo | a -> foo where
|     foo :: a -> foo
| 
| data A = A Int
| data B = B A
| 
| instance HasFoo A Int where
|     foo (A x) = x
| 
| instance HasFoo A foo => HasFoo B foo where
|     foo (B a) = foo a
| --------------------------------------------------------------
| ----------
| 
| The error messsage says that the type inferred for foo in B's instance
| is not general enough: the rhs has type "HasFoo B Int => B -> 
| Int", but
| "HasFoo B foo => B -> foo" was expected.