Yay! I'm really excited to see this coming along so nicely, especially as it has such a nice interaction with roles.
Here are some specific thoughts, upon reviewing your (surprisingly short!) patch:
- I strongly dislike the name NT (and derivatives), for at least two reasons: 1) Someone new to this work won't know what it means, and 2) it's useful for things unrelated to newtypes (because of phantoms). How about "safeCoerce"? The class could have the name "Coercible". Neither of these names conflict on a default search at Hoogle.
- Why box ~R#? Couldn't castEqR just take an unboxed R equality?
- If keeping boxed ~R#, you might want to add an ASSERT in mkEqReprBox ensuring that the coercion passed in has role R. (Use coercionRole.)
- It looks like you plan to make the NT class more wired in (line 507 of TcEvidence). Would this get rid of the Class parameter to EvNT and then simplify mkNT?
- getEqRolePredTys never seems to care about its Role return value. I'm happy about this, because the type-checker doesn't really know about roles. (It assumes everything is Nominal, which is how users would expect type-checking to behave, I think.)
- Without more comments, I get a little lost in the desugaring of EvNT and friends. But, I was able to trace the use of roles, and it looks sensible. In particular, it looks like mkTyConAppCo's preconditions around roles are satisfied, which can be tricky.
- It looks like you left some old code on line 1860 of TcInteract.
- The changes in Coercion are correct -- the use of Nominal that you removed harkened to the days when all CoVars were Nominal.
After looking at it all, I wonder if shoehorning this feature into the class / instance mechanism is the right way to go. How much is that buying us? The instance lookup mechanism for NT is totally customized (as it should be, it seems). So, how much harder would it be to make this a free-floating feature, separate from classes? This would mean adding a new thing with kind (* -> * -> Constraint) to replace "NT". (In a perfect world, this could be spelled ≈, but I'm not a huge fan of Unicode syntax in reality.) But, there would be no need to worry about user-defined instances, and all the wired-in class stuff could be gotten rid of. It's not that I think the class/instance approach is that bad, but we've had to wander so far away from using GHC's built-in features around instance lookup that I think we should re-examine.
Thoughts?
Thanks,
Richard
On Sep 2, 2013, at 10:42 AM, 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@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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs