Sounds amazing Joachim -- great work. | Consider | data Foo a = MkFoo (a,a). | The (virtual) instance | instance Coercible a b => Coercible (Foo a) (Foo b) | can only be used when MkFoo is in scope, as otherwise the user could | break abstraction barriers. This is enforced. Whoa! Where did this instance come from? I thought that we generated precisely two (virtual) instances for Foo: instance Coercible a (b,b) => Coercible a (Foo b) instance Coercible (a,b) b => Coercible (Foo a) b and no others. That it. Done. That was precisely the payload of my message of 2 August, attached. Each of the two is valid if the data constructor MkFoo is in scope. No other checks are needed. | Assume MkFoo is not in scope. Then the user could | define | data Hack a = MkHack (Foo a) | and use the (virtual) instance | instance Coercible a b => Coercible (Hack a) (Hack b) No no no! The virtual instances are instance Coercible (Foo a) b => Coercible (Hack a) b instance Coercible a (Foo b) => Coercible a (Hack b) and now the difficulty you describe disappears. | But it might, in corner cases, be too strict. Consider | data D a b = MkD (a, Foo b) | now the programmer might expect that, even without MkFoo in scope, that | instance Coercible a b => Coercible (D a c) (D b c) The two instances are instance Coercible (a, Foo b) x => Coercible (D a b) x instance Coercible x (a, Foo b) => Coercible x (D a b) Now can I prove (Coercible (D a c) (D b c))? Use the above rules twice; I then need Coercible (a, Foo c) (b, Foo c) and yes I can prove that if I have (Coerciable a b). In short, I think that if you use the approach I outlined, all these problems go away. Am I wrong? Simon