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/... for the error messages for most cases, corresponding to the code at https://github.com/nomeata/ghc-testsuite/blob/ntclass-clean/tests/typecheck/...
* 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@joachim-breitner.de • http://www.joachim-breitner.de/ Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C Debian Developer: nomeata@debian.org