newtype coercion wrapping status

[Joachim Breitner]

Hi,

another small update on the newtype coercion stuff (which is now named
Prelude GHC.Types GHC.Prim> :info coerce
coerce :: Coercible a b => a -> b        -- Defined in ‛GHC.Prim’
), diffs at:
https://github.com/nomeata/ghc/compare/ntclass-clean
https://github.com/nomeata/packages-ghc-prim/compare/ntclass-clean
https://github.com/nomeata/ghc-testsuite/compare/ntclass-clean

Am Montag, den 02.09.2013, 16:42 +0200 schrieb Joachim Breitner:
> What is still missing
> =====================
> 
>  * Good error messages (see above)

Done; at a first approximation to good, see 
https://github.com/nomeata/ghc-testsuite/blob/ntclass-clean/tests/typecheck/should_fail/TcCoercibleFail.stderr
for the error messages for most cases, corresponding to the code at
https://github.com/nomeata/ghc-testsuite/blob/ntclass-clean/tests/typecheck/should_fail/TcCoercibleFail.hs

>  * Checking if all involved data constructors are in scope
✓

>  * Code documentation
✓, Note [Coercible Instances]

>  * Tests.
✓; see https://github.com/nomeata/ghc-testsuite/compare/ntclass-clean

I have also removed the previous indirection of
        data EqR a b = EqR# (a ~R# b)
        class Coercible a b where coercion :: EqR a b
and instead have only type constructor akin to EqR, which is also the
type constructor of the Coercible class. I hope it does not break any
implicit invariants somewhere.

> * Prevent the user from writing NT instances himself.
✓

Left to do:

>  * Marking these data constructors as used (to avoid unused import 
>    warnings)
>  * User documentation
>  * More testing, especially with weird types and advanced type system 
>    features, e.g. type families.


NB, there is a wart with regard to constructor-in-scope-testing:

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.

But it is not enough: 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)
to convert "Foo Int" to "Foo Age". So not only the constructor of the
data type needs to be in scope, but also _all constructors_ of _all
typecons_ used in the definition of Hack. This is also enforced.

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)
is possible. Currently, the code is not flexible enough. Is that problem
relevant? (I’d be inclined to leave it simple for now and see if someone
complains.)

Interesting fact: If the last example would read 
        newtype D a b = MkD (a, Foo b)
and the constraint to solve would be
        Coercible (D Int ()) (D Age ()),
then GHC would actually solve it; not with
        instance Coercible a a
        instance Coercible a b => Coercible a Age
        instance Coercible a b => Coercible (D a c) (D b c)
(becaue the latter instance is not allowed, as explaint above), but
using a slight detour:
        instance Coercible a a
        instance Coercible a b => Coercible a Age
        instance (Coercible a b, Coercible c d) => Coercible (a,c) (b,d)
        instance Coercible (a, Foo b) c => Coercible (D a b) c
        instance Coercible a (b, Foo c) => Coercible a (D b c)
That it works with data but not with newtype might be
counter-intuitive... but still, this is probably far to specific to
worry about.

Greetings,
Joachim  

-- 
Joachim “nomeata” Breitner
  mail at joachim-breitner.de • http://www.joachim-breitner.de/
  Jabber: nomeata at joachim-breitner.de  • GPG-Key: 0x4743206C
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130906/1c42ebaa/attachment.pgp>