Exposing newtype coercions to Haskell
simonpj at microsoft.com
Mon Jul 8 11:39:30 CEST 2013
| > 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.
More information about the ghc-devs