CC: Functional dependencies question

[oleg@pobox.com]

Hello!

Andrew J Bromage wrote:

>         class Foo a b | a -> b where
>             foo :: a -> b
>
>         bar :: (Foo Char t) => t
>         bar = foo 'a'
>
> All well and good so far.  Let's add an instance of Foo...
>
>         instance Foo Char Bool where
>             foo c = isAlpha c
>
> Now neither GHC nor Hugs will allow this to compile, as the declared
> type of bar is "too general".

The type of bar is indeed too general. It should be
	bar:: forall t. (Foo Char t | Char -> t) => t
or
	bar:: exists t. (Foo Char t) => t
because the functional dependency implies that there can be only one
such type that relates to Char.

Yet such types are not expressible. Perhaps because of that, GHC and
Hugs delay reporting an error. For example, if we omit the instance
declaration, both GHC and Hugs seem happy. But they only seem. In
Hugs, if we try to actually evaluate 'bar', we get

	Main> bar
	ERROR - Unresolved overloading
	*** Type       : Foo Char a => a
	*** Expression : bar

Indeed, an instance declaration is required. Incidentally, GHC can
report the error even before running the code: if we just want to see
the type of bar:

	*Main> :t bar

	No instance for (Foo Char t)
	arising from use of `bar' at <No locn>

If we add an instance of Foo, such as "instance Foo Char Bool", then
the signature of bar is clearly too polymorphic: there can be only one
type t (namely, Bool) for which the constraint Foo Char t is true.

Incidentally, local type variable again seem to help -- they can
help express types that are normally inexpressible. If we define bar as

bar :: (Foo Char t) => t
bar ::tbar
	= (foo::(Char->tbar)) 'a'

we get an error:

/tmp/f.hs:10:
    Inferred type is less polymorphic than expected
        Quantified type variable `t' escapes
        It is mentioned in the environment:
          tbar = t is bound by the pattern type signature at /tmp/f.hs:1
    When trying to generalize the type inferred for `bar'
        Signature type:     forall t. (Foo Char t) => t
        Type to generalise: t
    When checking the type signature for `bar'
    When generalising the type(s) for `bar'

which alerts us that the given type of bar is indeed too general. Now, we
get the error right away. If we drop the explicit type declaration,

bar ::tbar
	= (foo::(Char->tbar)) 'a'

we get another error, 
/tmp/f.hs:12:
    No instance for (Foo Char tbar)
    arising from use of `foo' at /tmp/f.hs:12
    When checking the type signature of the expression:
          foo :: Char -> tbar
    In the definition of `bar': (foo :: Char -> tbar) 'a'

The compiler demands to see an instance of Foo Char t. If we add the instance
now, the compiler is happy.

	bar ::tbar
	   = (foo::(Char->tbar)) 'a'

	instance Foo Char Bool where
	  foo c = c == 'a'
	*Main> bar
	True

and the code even runs.