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