Dodgy newtype axioms

[Tim Chevalier]

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).

Cheers,
Tim

On 4/11/08, Tim Chevalier <catamorphism at gmail.com> wrote:
> Hi, Simon-
>
>  I'm currently trying to generate External Core for all the GHC
>  libraries and typecheck them using the stand-alone ext-core
>  typechecker (updated by me for the current incarnation of Core). I'm
>  running into a problem with the Data.String library. The generated
>  .hcr file includes, in part:
>
>   %newtype DataziString.ZCTIsString a
>     ^ (DataziString.ZCCoZCTIsString :: ((DataziString.ZCTIsString) :=:
>  (GHCziPrim.ZLzmzgZR (GHCziBase.ZMZN GHCziBase.Char))))
>     = GHCziBase.ZMZN GHCziBase.Char -> a;
>
>  (Hopefully the syntax I introduced for newtype coercion decls is
>  obvious.)  This coercion is saying that :TIsString equals ((->)
>  [Char]). But on the ext-core side, this doesn't typecheck because the
>  lhs has kind (*->*), and the rhs has type (?->*).
>
>  Is this a bug in GHC? It would be a pretty minor bug if so, since GHC
>  won't generate Core where the :CoZCTIsString coercion got used to
>  coerce anything that *didn't* have kind (*->*), but nevertless, the
>  coercion here isn't kind-correct according to the rules in fig. 3 of
>  the System FC paper (which say that both sides of the coercion have to
>  have the same kind.)
>
>  Note that there wouldn't be any problem if GHC didn't do the
>  eta-contraction thing for newtypes... but I don't know how easy it
>  would be to eta-expand again before printing out External Core.
>
>  Thanks,
>  Tim
>
>
>  --
>  Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt
>  "Modesty...is both alien and irrelevant to people who are happy in
>  themselves, in their beings, in their skins, their natures, their
>  capacities."--Anne Sayre
>