newtype coercion wrapping status
simonpj at microsoft.com
Fri Sep 6 17:03:12 CEST 2013
Sounds amazing Joachim -- great work.
| 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
| 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?
-------------- next part --------------
An embedded message was scrubbed...
From: unknown sender
Subject: no subject
Date: no date
More information about the ghc-devs