[Haskell] MPTCs and type inference

[Iavor Diatchki]

Hello,
The type inference for "d1", goes on like this:
1. suppose "x" is of some type "a"
2. now lets infer a type for "p"
3. using the usual rules we infer that "p :: b -> ()",
subject to the constraint that "D a b" holds.
4. "p" does not look like a function so the monomorphism restriction
applies, and we shall not attempt to infer a polymorphic type for "p",
so the final type for "p :: b -> ()" (for a particular but yet unknown
"b").
5. now lets infer the body of the "let", it is of type "()"
6. now we can infer that "d1 :: a -> ()", if we can solve the goal "D a b"
7. "d1" looks like a function, so we can generalize its type, to get
"forall a b. D a b => a -> ()"
8. This type is ambiguos, because the body of the function does not
mention "b", so we could not really use this function.  Hugs chooses
to complain immediately, while GHC delays the error until the funciton
is used in a particular place.

The inference for "d2" is similar up to step 4, and then it proceeds like this:
4. "p" looks like a function, so we are going to generalize its type,
to get: "forall b. D a b => b -> ()"
(note that the quantifier is only over the "b", and there is no
constraint to solve anymore, as it was "packaged" with the type of
"p")
5. the body of the "let" is still ()
6. the type of "d2" is "a -> ()", (no additional constraints)
7. "d2" looks like a function so we can generalize its type to get:
"forall a. a -> ()"

Basically the constraint disappeared in the second case, because it
was due to the definition of "p", and "p" was never used.  It is
perhaps more surprising that it did not disappear in the first case: 
because of the monomorphism restriction,"p" cannot have a polymorphic
type, and so all of its constraints are propagated to be constraints
on its polymorphic "parent" ("d1").

Hope this helps
-Iavor


On 4/25/05, Andreas Rossberg <rossberg at ps.uni-sb.de> wrote:
> This may well be stupidity on my side, but some experiments with multi
> parameter type classes got me slightly confused. Can somebody explain
> the following behaviour to me?
> 
>    class D a b where fd :: a -> b -> ()
> 
>    d1 x = let p = fd x in ()
>    d2 x = let p y = fd x y in ()
> 
> GHC derives the following types:
> 
>    d1 :: D a b => a -> ()
>    d2 :: a -> ()
> 
> Hugs rejects d1 on the grounds that the type is ambiguous, but agrees on
> the type of d2. I do not understand where the context disappears to in
> this example - 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.
> 
> --
> Andreas Rossberg, rossberg at ps.uni-sb.de
> 
> Let's get rid of those possible thingies!  -- TB
> 
> _______________________________________________
> Haskell mailing list
> Haskell at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell
>