| > 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
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
