Exposing newtype coercions to Haskell

[Simon Peyton-Jones]

| > If you CAN do that, then it's ok (internally) to use ordinary coercion
| > lifting, roughly
| > 	ntT g = T g refl
| > The above per-constructor-arg testing is just to make sure that all
| > the relevant witnesses are in scope, to preserve abstraction.  It's
| > not for soundness.
| 
| I understand the approach, but I think it is insufficient. Assume that
| the user wants to cheat for some reason and has this definition for ntS,
| clearly writable without having access to S’s internals:
| 
| ntS :: NT p p' -> NT q q' -> NT (S p q) (S p' q')
| ntS _ _ = error "nah nah"

Quite right!  My mistake was to say "if you CAN do that..." and then discard the evidence that you can do it.  What I should have said is

	* prove a large bunch of NT constraints (one per constructor field)
	* then `seq` them 
	* before returning the "ordinary coercion lifting" result.

The thing is, that the "ordinary coercion lifting" is sound (roles permitting -- should check that right off the bat).  But we are making a stronger check here, namely that the programmer has exported enough evidence, to expose abstractions.

Simon