[Haskell] MPTCs and type inference

[Andreas Rossberg]

Thanks for the detailed explanation that helped clearing up the smog in 
my head. I reckoned that once more the MR was to blame, at least for 
part of it.

>>>>in particular, when I compare with the single parameter case:
>>>>
>>>>   class C a where fc :: a -> a -> ()
>>>>
>>>>   c1 x = let p = fc x in ()
>>>>   c2 x = let p y = fc x y in ()
>>>>
>>>>where
>>>>
>>>>   c1 :: C a => a -> ()
>>>>   c2 :: C a => a -> ()
>>>>
>>>>is inferred, as I would expect.
> 
> The inference steps for this case are much the same except, that the
> inferred type for "p" now will be: "a -> ()", provided that we can
> solve the constraint "C a".  Because we have assumptions about "a" in
> the environment (namely it is mentioned in the type of the varible
> "x") we cannot generalize the type of "p".  It therefore remains
> monomorphic, and the constraint "C a" is propagated to the type of
> "c2".

To be more precise, p is not polymorphic *in the variables mentioned by 
the constraint* - the overall type of p could still be polymorphic, 
without changing the outcome.

My understanding now is as follows: a constraint is captured by a 
declaration if at least one of the type variables mentioned in the 
constraint is generalised in the respective type scheme. Is that a 
correct interpretation?

Of course, this is not the only possible rule. Alternatively, 
generalisation could always capture *all* unresolved constraints. For 
example, the type of p in c2 could be C a => a->() without a being 
quantified. That looks a bit more uniform in the face of MPTCs and would 
allow more programs, because contexts induced by dead code in form of an 
unused declaration could be forgotten consistently, not just when some 
of its free variables happen to be bound by a local quantifier.

-- 
Andreas Rossberg, rossberg at ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB