newtype coercion wrapping status

[Simon Peyton-Jones]

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

-------------- next part --------------
An embedded message was scrubbed...
From: unknown sender
Subject: no subject
Date: no date
Size: 38
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130906/74f62c38/attachment.eml>