[TYPES] A show-stopping problem for modular type classes?

[Brian Hulley]

Derek Dreyer wrote:
> Hi, Brian.
> 
>> Thanks for pointing out that the compiler could just reject this clause: perhaps this would be an acceptable penalty to pay for the advantages of having scoped instances. However there are situations where it would not be so clear what the compiler should do eg:
>>
>>    bar :: forall a. G a -> (a, Int)
>>    bar (Problem x) = (x + x, 1 + 2)
>>    bar (Ok _)      = ((), 0)
>>
>> In the expression (x + x, 1 + 2), what instance should the compiler use for (1 + 2)? Since (bar) is polymorphic, the compiler, when compiling (bar), has no way of knowing whether or not the match against (Problem x) is going to introduce a Num Int dictionary.
> 
> I think you're getting confused about the problem Karl pointed out
> with the original example (at least why it would be a problem in the
> modular type class setting).

Hi Derek,

Yes after I'd posted that example I realised that I'd moved on to a different issue without properly explaining what I was trying to illustrate.

The point I wanted to make was that although for the reasons you explained the example could be considered to be acceptable (and would be accepted by MTC), since (a) is a fresh type variable and hence the type of (x + x) has nothing to do with (1 + 2), there is still something rather uneasy about the case where the caller instantiates (a) to (Int).

What I'm trying to get at is not whether or not the formal system described in the MTC paper would accept the example but whether or not the example should be accepted from the programmer's point of view i.e. staying at the design-space level, since I think there is something slightly odd about the fact that we have a situation where there is an expression with 4 integers but 2 of them are being added using a different addition function. I.e. when a == Int it is a different sort of Int from 1...

So I agree it does make perfect sense to hold the view that (1 + 2) would always be evaluated in the static environment, but equally one could hold the view that (1 + 2) should be evaluated in the same instance environment as (x + x), which in the case where (a == Int), would result in a conflict.

Cheers, Brian.