On Wed, Jun 30, 2010 at 20:57:04 +0100, Ganesh Sittampalam wrote:
> >> type CommuteFunction = FORALL(x y) (Prim :< Prim) C(x y) -> Perhaps ((Prim 
> >> :< Prim) C(x y))
> >>-subcommutes :: [(String, CommuteFunction)]
> >>+subcommutes :: [(String, (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) 
> >>C(x y)))]

> No, it is necessary :-) CommuteFunction has an explicit forall -
> it's just a type alias and those get expanded at each use site, so
> the old code had a forall inside the tuple type.

Whoops! :-)

> In other words a pair is something that takes two type variables as
> type parameters. As you say in the rest of your review,
> impredicativity makes it legal to instantiate those variables with
> types that have a top-level forall. Without impredicativity, that
> isn't legal so we have to change it somehow. It turns out that in
> this case the forall there isn't actually needed so I just remove
> it.

All clear.  Thanks for confirming away the shakiness too.

-- 
Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow>
PGP Key ID: 08AC04F9

Attachment: pgpE4DxrGElPy.pgp
Description: PGP signature

_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users

Reply via email to