[Haskell-cafe] Re: type families and type signatures

[Manuel M T Chakravarty]

Hi Mark,

> I don't know if you have defined/studied corresponding notions of
> ambiguity/coherence in your framework.  Instead, I was referring to
> what Manuel described as "the equivalent problem using FDs":
>
>  class IdC a b | a -> b
>  instance IdC Int Int
>
>  bar :: IdC a b => b -> b
>  bar = id
>
>  bar' :: IdC a b => b -> b
>  bar' = bar
>
> In this program, both bar and bar' have ambiguous types (the
> variable 'a' in each of the contexts is not uniquely determined
> by the variable 'b' appearing on the right), and so *neither*
> one of these definitions is valid.  This behavior differs from
> what has been described for your approach, so perhaps Manuel's
> example isn't really "equivalent" after all.
>
> Technically, one could ignore the ambiguous type signature for
> bar, because the *principal* type of bar (as opposed to the
> *declared type*) is not ambiguous.  However, in practice, there
> is little reason to allow the definition of a function with an
> ambiguous type because such functions cannot be used in practice:
> the ambiguity that is introduced in the type of bar will propagate
> to any other function that calls it, either directly or indirectly.
> For this reason, it makes sense to report the ambiguity at the
> point where bar is defined, instead of deferring that error to
> places where it is used, like the definition of bar'.  (The latter
> is what I mean by "delayed" ambiguity checking.)

You are of course spot on, but this is a difference in how GHC handles  
functional dependencies compared to Hugs.  Hugs does reject bar as  
being ambiguous, but GHC does not!  In other words, it also uses  
"delayed" ambiguity checking for the FD version, and so raises an  
error only when seeing bar'.  The implementation of type families just  
mirrors GHC's behaviour for FDs.  (This is why I presented the FD  
example, but I should have mentioned that the equivalence is  
restricted to GHC.)

The rational for the decision to use delayed ambiguity checking in GHC  
is that it is, in general, not possible to spot and report all  
ambiguous signatures and *only* those.  So, there are three possible  
choices:

   (1) Reject all signatures that *may* be ambiguous (and hence reject  
some perfectly good programs).
   (2) Reject all signatures that are *guaranteed* to be ambiguous  
(and accept some programs with functions that can never be applied).
   (3) Don't check for ambiguity (or "delayed" ambiguity checking).

As you wrote, all three choices are perfectly safe - we will never  
accept a type-incorrect program, but they vary in terms of the range  
of accepted programs and quality of error messages.

Please correct me if I am wrong, but as I understand the situation,  
Hugs uses Choice (1) and GHC uses Choice (3).  As an example, consider  
this contrived program:

> class F a b | a -> b where
>   f1 :: a -> b
>   f2 :: b -> a
>
> instance F Int Int where
>   f1 = id
>   f2 = id
>
> class G x a b where
>   g :: x -> a -> b
>
> instance F a b => G Bool a b where
>   g c v = f1 v
>
> instance F b a => G Int a b where
>   g c v = f2 v
>
> foo1 :: (G Int a b) => a -> a
> foo1 v = v
>
> foo2 :: (G Bool a b) => a -> a
> foo2 v = v
>
> bar = foo2 (42::Int)

Here foo1 is actually ambiguous, but foo2 is fine due to the FD in the  
instance context of the (G Bool a b) instance.  GHC accepts this  
program (not checking for ambiguity) and allows you to evaluate bar.

In contrast, Hugs rejects both the signature of foo1 and of foo2,  
arguably being overly restrictive with foo2.

Cheers,
Manuel