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.