fundeps known beforehand (was RE: fundeps for extended Monad definition)

[Hal Daume III]

Hi Simon, all,

> Here's a less complicated variant of the same problem:
> 
> 	class C a b | a -> b where {}
> 
> 	instance C Int Int where {}
> 
> 	f :: (C Int b) => Int -> b
> 	f x = x

This is interesting, but I'm not entirely sure what the problem is (from a
theoretical, not practical, standpoint).  Obviously there is no problem in
a one module program, so let's assume we have the following modules:

  module C where
    class C a b | a -> b where {}

  module I1 where
    import C
    instance C Int Int where {}

  module I2 where
    import C
    instance C Int Bool where {}

  module U where
    import C
    import ?
    f :: C Int b => Int -> b
    f x = x

Now, there are four cases:

  1) U (transitively) imports I1
  2) U (transitively) imports I2
  3) U (transitively) imports both I1 and I2
  4) U (transitively) imports neither I1 nor I2

Suppose we are in case 1.  Then the programmer has written a too-general
type signature on f.  The programmer *must* know that b=Int in this case
otherwise his function definition makes no sense.  However, I don't really
see a reason why this should be an error rather than just a warning.  If
some other module K imports both U and (for instance) I2, then we'll get a
fundep clash and the whole program will be invalid.

Suppose we are in case 2.  Then the programmer has clearly screwed up
because we know b=Bool and x::Int and x::Bool are incompatible.  This
should clearly be a type error.

Case 3 is impossible, as this will be a fundep clash.

Case 4 should produce an error (IMO).  Of course, there could be a module
K which imports this U and also I1 in which case you might argue that this
should be allowed, but I don't think that makes much sense.

> I suppose I could use (unsafeCoerce x) as the RHS, which amounts to
> saying "in every call to f, b will be Int, so we know that the coercion
> is safe".  But that is a scarily global property.  For example, if a
> call site of f does not "see" the instance declaration, it might call f
> with an argument of type (C Int Bool) or something.  Nor can I see an
> easy way to insert the 'right' coercions in general.

Is this possible?  In order for this to happen, this evil module M must
import U.  This means that it has transitively imported I1 and thus has
the instance declaration.  Or am I missing something.  I think the
unsafeCoerce x is safe in these cases.

> Bottom line: excellent point, but I can't see how to fix it.  Maybe
> there are some fundep experts out there who can guide us through the
> swamp?  

Yes, please!

 - Hal