Coercible class (Was: newtype wrappers)

[Simon Peyton-Jones]

> a) A newtype can be casted only if its constructor is visible.
> b) Casting below a type constructor (instance Coercible a b => Coercible
>        (Maybe a) (Maybe b)) is possible if the roles allow it; the constructor
>        does not have to be visible or exposed, except that
> c) in Safe Haskell code, the constructor or the typecon (and all
>        constructors of all typecons used in the definition of the typecon) has
>        to be visible.

Has anyone talked to David Terei about the Safe Haskell check (c) above?  It's not clear to me whether (c) is necessary.  (And it would need to recursively check those tycoons, I think.  Are you doing that?)

As to Generalised Newtype Deriving, my earnest hope is that we can make GND safe for Safe Haskell.  it was only excluded before because of #1496, which is now solved.

For GND Richard proposes:

|  I propose that (deriving instance Class Newtype) should work when
|  	
|  1) The roles allow it (i.e., the role of the last parameter of Class is not nominal)
|       (as currently implemented),
|  2) The constructor of Newtype is visible (as currently implemented), AND
|  3) If we imagine Constraint and * to be the same, we could derive Coercible a b
|        => Coercible (Class a) (Class b), according to the check Joachim just elaborated.
|        (the new bit)

But what does (3) mean?  It means (a,b,c) above.  Well, (a) holds because of (2), (b) holds because of (1), which leaves (c).  That is, the all the class methods must be visible here.  That makes sense.  If you were to write the instance by hand, you'd need to be able to see the class methods. It's analogous to (c).

So replace (3) by "All the class methods are visible".  And think of (3) like (c); that is, only reqd for Safe Haskell.

But let's see if David and David even want (c)/(3) for Safe Haskell!

Simon


|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Richard
|  Eisenberg
|  Sent: 15 September 2013 22:57
|  To: Joachim Breitner
|  Cc: ghc-devs at haskell.org
|  Subject: Re: Coercible class (Was: newtype wrappers)
|  
|  Great -- that makes a lot of sense to me. Sorry if you had to repeat yourself here.
|  
|  Does this mean that it is impossible to coerce a (Map String Int) to a (Map String
|  Age) in Safe code? I expect so. I think this is suboptimal, but there might be a
|  small way to patch this small weakness in the design without large changes.
|  
|  The Safe Haskell check seems a little global, but that might be the only sensible
|  way to do it, and I was somewhat hoping that would be your answer. Why?
|  Because I think GeneralizedNewtypeDeriving (GND) should piggyback on your
|  algorithm:
|  
|  In specific, I propose that (deriving instance Class Newtype) should work when
|  
|  1) The roles allow it (i.e., the role of the last parameter of Class is not nominal)
|  (as currently implemented),
|  2) The constructor of Newtype is visible (as currently implemented), AND
|  3) If we imagine Constraint and * to be the same, we could derive Coercible a b
|  => Coercible (Class a) (Class b), according to the check Joachim just elaborated.
|  (the new bit)
|  
|  Clause (3) is trivially satisfied outside of Safe Haskell. In Safe Haskell, it would
|  require looking at all the types used in all the methods in Class. This makes good
|  sense to me, as it would (I think) fix #5498. Does this idea make sense?
|  
|  A question about the existing check: How does it treat constraints? For example,
|  say we have
|  
|  > data Foo a where        -- a's role is representational; this is NOT a GADT
|  >   MkFoo :: Ord a => a -> Foo a
|  >
|  > newtype Age = MkAge Int deriving Eq   -- the Eq is to satisfy Ord's superclass
|  constraint
|  > instance Ord Age where
|  >   (MkAge a) `compare` (MkAge b) = b `compare` a   -- args are reversed
|  >
|  > fooInt :: Foo Int
|  > fooInt = MkFoo 5
|  >
|  > fooAge :: Foo Age
|  > fooAge = coerce fooInt   -- it seems this would be accepted
|  >
|  > confused :: Foo Age -> Ordering
|  > confused (MkFoo x) = x `compare` (MkAge 0)
|  
|  What will confused do? It has potentially two, conflicting instances for Ord to
|  hand: one in the global context; and one from pattern-matching MkFoo, which was
|  creating by coercing from Ord Int. I have a hard time seeing the solution to be
|  IncoherentInstances, because it's not clear which chunk of code would trigger the
|  need for that extension.
|  
|  Also, it's possible for there to be "abstract" classes, which don't export all of their
|  methods or use other tricks to prevent instances (non-exported superclasses, for
|  example) outside of the library. Are these checked for?
|  
|  Actually, come to think of it, the example I have above doesn't really interact with
|  the Safe Haskell check -- it's a problem regardless, unless I'm confused.
|  
|  Richard
|  
|  PS: If these concerns are answered in documentation you've already written, feel
|  free just to send a link, even just to a file on github -- I hate repeating myself
|  about these things, too!
|  
|  On Sep 15, 2013, at 5:13 PM, Joachim Breitner <mail at joachim-breitner.de>
|  wrote:
|  
|  > Hi,
|  >
|  > Am Sonntag, den 15.09.2013, 16:48 -0400 schrieb Richard Eisenberg:
|  >> What was the end result of the discussion on abstraction? Can a
|  >> library control how its types are coerced?
|  >
|  > there is no end result, as this is just a language feature. But the
|  > current state of affairs is that:
|  > * A newtype can be casted only if its constructor is visible.
|  > * Casting below a type constructor (instance Coercible a b => Coercible
|  > (Maybe a) (Maybe b)) is possible if the roles allow it; the constructor
|  > does not have to be visible or exposed, except that
|  > * in Safe Haskell code, the constructor or the typecon (and all
|  > constructors of all typecons used in the definition of the typecon) has
|  > to be visible.
|  >
|  > So once you know your syntax for role annotations it would make sense to
|  > annotate the arguments of Set and Map (first one only) in base before we
|  > release 7.8.
|  >
|  > Greetings,
|  > Joachim
|  >
|  > PS: Do we have regular builds of master, including users' guide and
|  > haddock, somewhere that I can link to in such a mail?
|  >
|  > --
|  > Joachim Breitner
|  >  e-Mail: mail at joachim-breitner.de
|  >  Homepage: http://www.joachim-breitner.de
|  >  ICQ#: 74513189
|  >  Jabber-ID: nomeata at joachim-breitner.de
|  > _______________________________________________
|  > ghc-devs mailing list
|  > ghc-devs at haskell.org
|  > http://www.haskell.org/mailman/listinfo/ghc-devs
|  
|  _______________________________________________
|  ghc-devs mailing list
|  ghc-devs at haskell.org
|  http://www.haskell.org/mailman/listinfo/ghc-devs