Sorry Tim, it was the weekend. Here's your example, I think:
:TFunctor :: (*->*) -> *
(->) :: ? -> ? -> *
r :: *
Hence
(->) r :: ? -> *
You are concerned about the kind-correctness of
:TFunctor ((->) r)
Well, that's correct if
(? -> *) is a sub-kind of (* -> *)
which it is. So we're happy.
Admittedly, the whole sub-kinding system is an attempt to make systematic some
rather ad-hoc restrictions about what types must be boxed etc, and I don't want
to claim that it's as good as it could be. But on this occasion it looks ok.
Simon
| -----Original Message-----
| From: Tim Chevalier [mailto:[EMAIL PROTECTED]
| Sent: 14 April 2008 00:40
| To: Simon Peyton-Jones
| Cc: [email protected]
| Subject: Re: Dodgy newtype axioms
|
| On 4/13/08, Tim Chevalier <[EMAIL PROTECTED]> wrote:
| > For other reasons, I decided it was better to re-eta-expand newtype
| > declarations before printing out External Core, and this fixed the
| > problem I described below. But I'd still be curious whether you agree
| > that something mildly disturbing is going on here (the disturbing
| > thing can be summarized as: eta-contracting a type fails to preserve
| > kinds).
|
| One more comment and then I'll quit talking to myself: Actually,
| there's still a problem even if External Core requires newtype
| coercions to be declared in their fully-applied form. Consider the
| following (from compiling Control.Monad.Instances with -fext-core):
|
| ControlziMonadziInstances.zdf4 :: %forall r . GHCziBase.ZCTFunctor
| (GHCziPrim.ZLzmzgZR r) =
| %cast (\ @ r @ a @ b -> GHCziBase.zi @ a @ b @ r)
| (%forall r . GHCziPrim.sym
| GHCziBase.ZCCoZCTFunctor
| (GHCziPrim.ZLzmzgZR r))
|
| In particular, the cast (sym :TFunctor ((->) r)) is not kind-correct,
| because -- similarly to the example I originally gave -- :TFunctor has
| kind (*->*), but ((->) r) has kind (?->*). And indeed, it's not really
| true that :TFunctor and ((->) r) are interchangeable, because the
| latter could be applied to either an lifted or an unlifted type
| argument, whereas the former must be applied to a lifted type.
|
| Unlike with the previous example, I don't see an easy way to avoid
| exposing this in External Core. The fix would be to eta-expand all
| applications of the (->) tycon, which isn't trivial to do within the
| current External Core printer.
|
| Cheers,
| Tim
|
| --
| Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt
| "Instead of insight, maybe all a man gets is strength to wander for a
| while. Maybe the only gift is a chance to inquire, to know nothing for
| certain. An inheritance of wonder and nothing more." -- William Least
| Heat Moon
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
