Type-checker bug related to implicit parameters.

John Hughes rjmh@cs.chalmers.se
Wed, 19 Sep 2001 22:24:18 +0200 (MET DST)


	I believe if you're (more) explicit about the scope
	of the scoped type variable, you'll be fine. i.e.,

	 foo :: (forall b.(?x :: Int) =3D> b)) -> Int -> b
	 foo s z =3D s with ?x =3D z

Not at all, Sigbj=F6rn! You didn't just make the scope of the type variable more
explicit, you changed it. In my type signature

	 foo :: ((?x :: Int) =3D> b)) -> Int -> b

both occurrences of b are the same, and the argument need not be
polymorphic. Your type would rule out the call I want to make

         foo ?x 42

(which should evaluate to 42), and just about any other call also.

	i.e., 'foo' is running into the same issue as the bug
	reported in
	http://haskell.cs.yale.edu/pipermail/hugs-bugs/2001-January/000084.html,

I don't think it is the same bug, although it may be related. The example you
quote involves "rank 2 overloading", whereas mine involves "rank 2 implicit
parameters". Moreover, it seems to be the *type of the implicit parameter*
which is wrongly unified with the result type of foo, which suggests that this
is something specific to implicit parameters.

Another observation is that "rank 2 overloading", without polymorphism, is
quite useless: there's no advantage in a signature such as

      f :: (Ord a =3D> a -> a) -> a

since a can be only one type in the body of f, and so the "overloaded"
parameter might just as well be instantiated before it is passed. That's why
you assumed there should be a "forall b" in my example: in this one, "forall
a" must be inserted if the context is to be useful. With implicit parameters
the situation is different, because the value is supplied *explicitly* in the
body of f, so one can very well supply two different ones. E.g.

     f :: (?x :: Int =3D> Int) -> (Int,Int)
     f z =3D (z with ?x=3D1, z with ?x=3D2)

     > f (?x*2)
     (2,4)


	>
	> Hugs -98 (Feb 2001) rejects the following program (which should be
	well-typed)
	>
	> > foo :: ((?x :: Int) =3D> b) -> Int -> b
	> > foo s z =3D s with ?x =3D z
	>
	> with the message
	>
	> ERROR Bug.hs:2 - Inferred type is not general enough
	> *** Expression    : foo
	> *** Expected type : ((?x :: Int) =3D> a) -> Int -> a
	> *** Inferred type : ((?x :: Int) =3D> a) -> Int -> Int
	>
	> It seems to unify the type of the implicit parameter with the type of
	> the result.
	>
	> GHC accepts this program (but generates wrong code).
	>
	> John Hughes
	>
	> _______________________________________________
	> Hugs-Bugs mailing list
	> Hugs-Bugs@haskell.org
	> http://www.haskell.org/mailman/listinfo/hugs-bugs