newtype coercion wrapping status

[Simon Peyton-Jones]

Joachim, 

How do I get your code?

bash$  git clone https://github.com/nomeata/ghc/compare/ntclass-clean newtype-wrappers
Cloning into 'newtype-wrappers'...
fatal: https://github.com/nomeata/ghc/compare/ntclass-clean/info/refs not found: did you run git update-server-info on the server?



| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of
| Joachim Breitner
| Sent: 02 September 2013 15:43
| To: ghc-devs at haskell.org
| Subject: newtype coercion wrapping status
| 
| 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