| > 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