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@haskell.org] On Behalf Of | Joachim Breitner | Sent: 02 September 2013 15:43 | To: ghc-devs@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@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@joachim-breitner.de • http://www.joachim-breitner.de/ | Jabber: nomeata@joachim-breitner.de • GPG-Key: 0x4743206C | Debian Developer: nomeata@debian.org