Dodgy newtype axioms

[Tim Chevalier]

On 4/14/08, Simon Peyton-Jones <simonpj at microsoft.com> wrote:
> 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.
>

I don't think I explained myself very well. Actually, I'm concerned
about the kind-correctness of:

:Co:TFunctor ((->) r)

The axiom for :Co:TFunctor is:
:Co:TFunctor (f::(*->*)) :: (:TFunctor f) :=: (forall a b . (a > b) ->
f a -> f b)

Then there are two questions:
- Is it sound to apply a coercion (such as :Co:TFunctor) to a type
whose kind is a subkind of its argument kind? I would have thought no,
but you seem to be implying yes.
- Does anything actually go wrong if you do? In this case, certainly
not, since the partially-applied ((->) r) just gets fully applied to a
tyvar of kind *.

But I'm not so sure that it's sound in general. What if you had a coercion like:
:CoT (t:::*) (forall a . a -> t :=: a -> T)
where T :: *?
Then if you wrote (:CoT (u::?)), that would mean
forall a . a -> ? :=: a -> T

Do you see what I'm getting at now?

Cheers,
Tim

-- 
Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt
"Faith, faith is an island in the setting sun / But proof, yes, proof
is the bottom line for everyone."--Paul Simon