Fundep/Existential Types in 5.03

[Simon Peyton-Jones]

Ashley

Just leave out the existential in your defn of D!
The (C a b) in the defn of f will do the job.

But your example nevertheless does expose a delicate interaction in the
type checker.  5.02.2 happened not to expose the functional
dependency, so it simply use the (C a b) that f provided.
5.03 does expose the dependency, and so makes the two
b's the same, which is what gives the error message.

It's a problem that some subtlety in the inference algorithm
(I don't even know what it is) changes the behaviour.  I don't
know how to fix this, but perhaps someone else does.

GHC makes all type abstractions and applications explicit,
so the two b's really can't be the same: they don't have the
same scope.

Simon

| -----Original Message-----
| From: Ashley Yakeley [mailto:ashley@semantic.org]=20
| Sent: 06 April 2002 02:00
| To: GHC List
| Subject: Fundep/Existential Types in 5.03
|=20
|=20
| Consider this:
|=20
|   module Test3 where
|=20
|   class C a b | a -> b where
|      	m :: a -> b
|=20
|   data D a =3D forall b. (C a b) =3D> MkD a
|=20
|   f :: (C a b) =3D> D a -> b
|   f (MkD a) =3D m a
|=20
| This compiles fine under GHC 5.02.2. But under 5.03, it gives=20
| an error:
|=20
| Model/Test3.hs:9:
|     Inferred type is less polymorphic than expected
|         Quantified type variable `b' escapes
|     When checking an existential match that binds
|     and whose type is D a -> b1
|     In the definition of `f': f (MkD a) =3D m a
|=20
| I consider that the 5.02.2 behaviour is preferable, and that=20
| this is a=20
| perfectly good program. 'b' does not escape because it is=20
| fundep on 'a',=20
| which is specified in the type-signature. There can be only one.
|=20
| What was changed in 5.03 and why?
|=20
| --=20
| Ashley Yakeley, Seattle WA
|=20
| _______________________________________________
| Glasgow-haskell-users mailing list=20
| Glasgow-haskell-users@haskell.org=20
| http://www.haskell.org/mailman/listinfo/glasgow-| haskell-users
|=20