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

[Derek Dreyer]

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).

The problem was *not* that by unpacking the GADT arguments you were
introducing instances into scope that overlapped with Num Int.  The
problem was that you were unpacking *two* arguments of type G a, which
introduced two overlapping instances of Num a.

The "bar" example above is fine, because you're just unpacking one
argument of type G a, and since "a" is a freshly bound type variable,
it's fine to introduce an instance of Num a (as it can't overlap with
anything else).

The "1 + 2" part is a different story.  In the MTC type system,
because the type of 1 and 2 is concrete, you can only typecheck "1 +
2" if there is a Num Int instance in the static environment, i.e. if
bar is typechecked under a "using" declaration for a Num Int instance.
 It doesn't matter if bar is invoked later on in the program in some
other scope where a different Num Int instance has been made
canonical.  The meaning of "1 + 2" can only depend on the static
context.  In particular, it doesn't matter if bar's type parameter "a"
is instantiated to Int.  In contrast, since the type of x is
universally quantified, the canonical instance of Num a *must* be
determined dynamically (i.e. passed in as an argument).

Best regards,
Derek