Dodgy newtype axioms

[Tim Chevalier]

On 4/14/08, Tim Chevalier <catamorphism at gmail.com> wrote:
>  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
>

Oops, typo, I meant something like:
forall a . (a -> (u::?)) :=: a -> (T::*)

-- 
Tim Chevalier * http://cs.pdx.edu/~tjc * Often in error, never in doubt
"...It's wonderful that I can trust you not to spit in my milk, but
what's the point if you're going to drink from the bottle?" -- Sarah
Barton