newtype coercion wrapping status

[Joachim Breitner]

Hi,

after following SPJ’s latest advise and implementing the newtype
coercion classes directly and ad-hoc in the type checker (in TcInteract,
similarly to the SingI), this rewrite of the code is now working (for
some value of working):

What works now
==============

The setup:
Prelude> :info GHC.NT.castNT
castNT :: NT a b => a -> b     -- Defined in ‛GHC.NT’

Simple cases:

Prelude> newtype Age = Age Int deriving Show
Prelude> GHC.NT.castNT (Age 1) :: Int
1
Prelude> GHC.NT.castNT (1::Int) :: Age
Age 1

Unrolling several newtypes at the same time:

Prelude> newtype Bar = Bar Age deriving Show
Prelude> newtype Baz = Baz Int deriving Show
Prelude> GHC.NT.castNT (Baz 1) :: Bar
Bar (Age 1)

Unrolling newtypes with type arguments, even polymorphically:

Prelude> newtype MyMB a = MyMB (Maybe a) deriving Show
Prelude> GHC.NT.castNT (Just ()) :: MyMB ()
MyMB (Just ())
Prelude> let f1 = (\x -> GHC.NT.castNT (Just x)) :: a -> MyMB a
Prelude> f1 True
MyMB (Just True)
Prelude> let f2 = (\x -> GHC.NT.castNT (Just x)) :: GHC.NT.NT a b => a -> MyMB b
Prelude> f2 (Baz 1) :: MyMB Bar
MyMB (Just (Bar (Age 1)))


Unrolling inside type constructor arguments, including functions and
tuples:

Prelude> GHC.NT.castNT (Just (Age 1)) :: Maybe Int
Just 1
Prelude> (GHC.NT.castNT Age :: (Baz -> Bar)) (Baz 1)
Bar (Age 1)
Prelude> GHC.NT.castNT (Age 1, Baz 1) :: (Bar, Int)
(Bar (Age 1),1)


Arbitrary changing of Phantom types:

Prelude> data Proxy a = Proxy deriving Show
Prelude> GHC.NT.castNT (Proxy :: Proxy Int) :: Proxy Bool
Proxy

Unwanted casting can be prevented by role annotations:

Prelude> :set -XRoleAnnotations 
Prelude> data Map a at N b = Map a b deriving Show
Prelude> GHC.NT.castNT (Map () (1::Int)) :: Map () Bar
Map () (Bar (Age 1))
Prelude> GHC.NT.castNT (Map (1::Int) ()) :: Map Bar ()

<interactive>:24:1:
    No instance for (GHC.NT.NT (Map Int ()) (Map Bar ()))
      arising from a use of ‛GHC.NT.castNT’
    In the expression: GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()
    In an equation for ‛it’:
        it = GHC.NT.castNT (Map (1 :: Int) ()) :: Map Bar ()

GADTs have the roles set automatically, so this does not work either, as
expected:

Prelude> :set -XGADTs -XStandaloneDeriving
Prelude> data GADT a where GADT :: GADT Int
Prelude> deriving instance Show (GADT a)
Prelude> GHC.NT.castNT GADT :: GADT Age

<interactive>:37:1:
    No instance for (GHC.NT.NT (GADT Int) (GADT Age))
      arising from a use of ‛GHC.NT.castNT’
    In the expression: GHC.NT.castNT GADT :: GADT Age
    In an equation for ‛it’: it = GHC.NT.castNT GADT :: GADT Age


What is still missing
=====================

 * Good error messages (see above)
 * Checking if all involved data constructors are in scope
 * Marking these data constructors as used (to avoid unused import 
   warnings)
 * Prevent the user from writing NT instances himself.
 * Code documentation
 * User documentation
 * Tests.
 * More testing, especially with weird types and advanced type system 
   features, e.g. type families.

What needs more thought
=======================

 * How to handle recursive newtypes, such as
   newtype Void = Void Void
   or worse
   newtype Foo a = Foo (Foo (a,a))?
   With the current setup, which is equivalent to an instance
   instance NT (Foo (a,a)) b => NT (Foo a) b
   it will cause constraint checking to loop.
   
   I’m inclined to simply not create instances for recursive newtypes, 
   or alternatively only in modules with UndecidableInstances turned on.

The code
========

The code can be reviewed at
https://github.com/nomeata/ghc/compare/ntclass-clean
with the corresponding ghc-prim changes at
https://github.com/nomeata/packages-ghc-prim/compare/ntclass-clean

I followed the example of SingI and created a new constructor in data
EvTerm for NT evidences. There are three kinds of evidence for NT t1 t2:
One for t1 == t2, one for unfolding a newtype (at t1 or t2), and one if
t1 and t2 have the same type constructor at the head. This corresponds
to the the shapes of NT instances one would write by hand.

The evidence is created in TcInteract, in a function called by
matchClassInst, and turned into Core by dsEvTerm in DsBinds.

Currently there is both a type constructor GHC.Types.EqR that boxes EqR#
and is built-in, and a type class GHC.NT.NT, which has just one method
of type EqR. This is because it seems to be quite tricky to create a
built-in class in GHC.Prim, but also causes a bit of extra bookkeeping.
I guess the final patch will somehow avoid this indirection.

Richard, can you have a look at my changes to
compiler/types/Coercion.lhs, if they are sound? I found that there was a
hardcoded role of Nominal where, with my code, also Representational
could occur.


Is this going in the right direction, both design and
implementation-wise?


Thanks,
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/20130902/246dcd0d/attachment.pgp>