Exposing newtype coercions to Haskell

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
25 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
If you add -XIncoherentInstances *just to the module that has instance IsNT a a*, then it'll work fine I think.  This says "pick this instance even though an instantiation of the constraint might match a more specific instance".  You don't need the flag in importing modules.

I think that's fine.  For the IsNT class, where users cannot define their own instances, it really is not incoherent to pick the IsNT a a instance.  The operational effect is always a no-op.

In short, I think this'll work fine.

Simon

|  -----Original Message-----
|  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Joachim
|  Breitner
|  Sent: 23 July 2013 12:45
|  To: ghc-devs at haskell.org
|  Subject: Re: Exposing newtype coercions to Haskell
|  
|  Hi,
|  
|  Am Dienstag, den 23.07.2013, 09:51 +0100 schrieb Richard Eisenberg:
|  > I think that thinking about the base case is also
|  > productive, but I don't have a clear enough opinion to express on that
|  > front.
|  
|  and it seems to tricky; Here we are hitting problems that we did not
|  have with the non-class-approach.
|  
|  tl;dr: "IsNT a a" only works with IncoherentInstances, which are in
|         principle fine for this class (it is univalent in a sense), but
|         requiring this extension would be quite unfortunate.
|  
|  
|  Consider this ghci session (this already works here):
|  
|  Prelude GHC.NT> newtype Age = Age Int deriving Show
|  Prelude GHC.NT> deriving instance IsNT Int Age
|  Prelude GHC.NT> castNT (1::Int) :: Age -- good, works
|  Age 1
|  Prelude GHC.NT> deriving instance (IsNT a a', IsNT b b') => IsNT (Either a b)
|  (Either a' b')
|  Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Age -- also works
|  Left (Age 1)
|  Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- does not work
|  yet
|  
|  <interactive>:12:1:
|      No instance for (IsNT Int Int) arising from a use of ?castNT?
|      In the expression:
|          castNT (Left 1 :: Either Int Int) :: Either Age Int
|      In an equation for ?it?:
|          it = castNT (Left 1 :: Either Int Int) :: Either Age Int
|  Prelude GHC.NT> deriving instance IsNT Int Int
|  Prelude GHC.NT> castNT (Left 1::Either Int Int) :: Either Age Int -- works now
|  Left (Age 1)
|  Prelude GHC.NT> :t castNT :: (Either Int Int) -> (Either Age Int)
|  castNT :: (Either Int Int) -> (Either Age Int) :: Either Int Int -> Either Age Int
|  
|  But we are not able to cast such that one type parameter changes while
|  leaving another type _variable_ untouched:
|  
|  Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)
|  
|  <interactive>:1:1:
|      No instance for (IsNT a1 a1) arising from a use of ?castNT?
|      Possible fix:
|        add (IsNT a1 a1) to the context of
|          an expression type signature: Either Int a1 -> Either Age a1
|          or the inferred type of it :: Either Int a -> Either Age a
|      In the expression: castNT :: (Either Int a) -> (Either Age a)
|  
|  and if we add "IsNT a a" as a base case:
|  
|  Prelude GHC.NT> instance IsNT a a
|  
|  <interactive>:34:10: Warning:
|      No explicit method or default declaration for ?coercion?
|      In the instance declaration for ?IsNT a a?
|  
|  we get
|  
|  Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)
|  
|  <interactive>:1:1:
|      Overlapping instances for IsNT a1 a1 arising from a use of ?castNT?
|      Matching instances:
|        instance [overlap ok] IsNT a a -- Defined at <interactive>:34:10
|        instance IsNT Int Int -- Defined at <interactive>:13:1
|        instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
|          -- Defined at <interactive>:10:1
|      (The choice depends on the instantiation of ?a1?
|       To pick the first instance above, use -XIncoherentInstances
|       when compiling the other instance declarations)
|      In the expression: castNT :: (Either Int a) -> (Either Age a)
|  
|  
|  Re-doing the session with -XIncoherentInstances set helps, but requiring
|  that for every module that wants to derive a IsNT class is probably not
|  nice.
|  
|  
|  The one-parameter-variant does not help either.
|  
|  
|  One way to avoid the issue is to have two instances for Either:
|  
|  Prelude GHC.NT> deriving instance (IsNT a a') => IsNT (Either a b) (Either a' b)
|  Prelude GHC.NT> deriving instance (IsNT b b') => IsNT (Either a b) (Either a b')
|  
|  This still requires OverlappingInstances, but I can get the desired cast
|  without IncoherentInstances:
|  
|  Prelude GHC.NT> :t castNT :: Either Int a -> Either Age a
|  castNT :: Either Int a -> Either Age a
|    :: Either Int a -> Either Age a
|  
|  Other casts that should be ?normal? are more complicated now:
|  
|  Prelude GHC.NT> let c = (castNT :: Either Age Int -> Either Age Age) . (castNT ::
|  Either Int Int -> Either Age Int)
|  Prelude GHC.NT> :t c
|  c :: Either Int Int -> Either Age Age
|  Prelude GHC.NT> c (Left 1)
|  Left (Age 1)
|  
|  
|  
|  In any case, the whole thing needs a bit more massaging until it becomes
|  sufficiently elegant.
|  
|  Greetings,
|  Joachim
|  
|  --
|  Joachim Breitner
|    e-Mail: mail at joachim-breitner.de
|    Homepage: http://www.joachim-breitner.de
|    ICQ#: 74513189
|    Jabber-ID: nomeata at joachim-breitner.de

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Richard Eisenberg-2
In reply to this post by Simon Peyton Jones
Yes, that's what I got from Joachim's response to my design, also. My only other thought is to have some way to store an _axiom_, instead of an R coercion. But, that seems very fishy and wrong-headed. So, I guess we'll have to have ~R#. I'm tempted to use "~R#" as its name, to make it impossible to write in Haskell code. Would there be any problems with this? I'll go ahead and include the new coercion form when I commit roles.

Richard

On Jul 23, 2013, at 7:46 PM, Simon Peyton-Jones wrote:

> I thought about the design you suggest below, but rejected it because I don't see how to do lifting -- which is really the whole point! In particular, what are you going to write for
>
> ntList :: NT a b -> NT [a] [b]
> ntList (MkNT castNT uncastNT) = MkNT ??? ???
>
> For lists you could write (fmap castNT), but the whole point of this exercise is not to write that -- and the type might not be an instance of Functor.
>
> I'm thinking we need (~R#) as a type constructor.
>
> Simon
>
> |  -----Original Message-----
> |  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Richard
> |  Eisenberg
> |  Sent: 23 July 2013 09:51
> |  To: Joachim Breitner
> |  Cc: ghc-devs at haskell.org
> |  Subject: Re: Exposing newtype coercions to Haskell
> |  
> |  A few responses:
> |  
> |  - As Simon said, there is no great reason we don't have ~R# in Core.
> |  It's just that we looked through GHC and, without newtype coercions,
> |  there is no need for ~R#, so we opted not to include it. I'm still not
> |  convinced we need it for newtype coercions, though. What if we have this
> |  in Core?
> |  
> |  > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a }
> |  > NTCo:Age :: Age ~R# Int         -- see [1]
> |  > NTAgeInst :: NT Age Int
> |  > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT = \(x
> |  > :: Int). x |> sym NTCo:Age }
> |  
> |  [1]: We still do have representational coercions, even though it would
> |  be bogus to extract their type, as the type constructor ~R# does not
> |  exist. But, coercionKind, which returns the two coerced types, and the
> |  new coercionRole (which would return Representational in this case) work
> |  just fine.
> |  
> |  Here, we don't need to abstract over ~R#, by just referring to the
> |  global axiom directly. Does this compose well? I think so; you'll just
> |  have to inline all of the coercions. But, the coercions won't ever get
> |  too big, as they will always mirror exactly the structure of the types
> |  being coerced. Simon, this is the sort of "magic" I was thinking of,
> |  magical because I can't imagine a way this could be produced from an
> |  HsExpr.
> |  
> |  Also, nice example of how the one-parameter design might aid the
> |  programmer. I think that thinking about the base case is also
> |  productive, but I don't have a clear enough opinion to express on that
> |  front.
> |  
> |  Richard
> |  
> |  On 2013-07-23 08:21, Joachim Breitner wrote:
> |  > Hi Richard and Simon,
> |  >
> |  > thanks for your detailed notes.
> |  >
> |  > Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg:
> |  >
> |  >> - I think you *do* want HsExprs not CoreExprs. Though I haven't worked
> |  >> much in TcDeriv myself, I imagine everything uses HsExprs so that they
> |  >> can be type-checked. This allows nice error messages to be reported at
> |  >> the site of a user's "deriving instance IsNT ...".
> |  >
> |  > My plan was to make all checks (constructors in scope; IsNT classes for
> |  > all data constructor arguments present) in TcDeriv, so you get nice
> |  > error messages. If it turns out that the actual coercion can only be
> |  > generated in a later pass, then it the checks just need to be strong
> |  > enough to make that pass always succeed.
> |  >
> |  >> - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:)
> |  >> (the last is from the soon-to-be Data.Type.Equality), all work over
> |  >> so-called *nominal* coercions.
> |  >
> |  > I know; I was just using them until representational equality is in and
> |  > plan to switch then.
> |  >
> |  >>  (Nominal coercions correspond to the "C" coercions from this paper)
> |  >
> |  > I got confused by C and T in my previous mails. In any case, I am only
> |  > concerned with representational equality (T, it seems) for this
> |  > project.
> |  >
> |  >> Or, it's possible
> |  >> that we could add abstraction over representational coercions, but I
> |  >> prefer the magical approach, because I don't see a general need for
> |  >> the
> |  >> ability to abstract.
> |  >
> |  > Hmm, I must admit I was assuming that once the roles implementation is
> |  > in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse
> |  > moniker) available in Core.
> |  >
> |  >
> |  >> Now that I think of it, you may need to generalize the deriving
> |  >> mechanism a bit. All current "deriving"s generate code that the user
> |  >> could write. (Typeable is something of an exception here.) Here, the
> |  >> generated code is something that a user can not write. Maybe that's
> |  >> why
> |  >> you wanted CoreExprs in the first place!
> |  >
> |  > Exactly. But it is also the reason why we are aiming for deriving
> |  > classes (and not NT values), because it is already an established way
> |  > of
> |  > having the compiler generate code for you.
> |  >
> |  >
> |  >> - I prefer the two-parameter class over a one-parameter, as it seems
> |  >> more flexible.
> |  >
> |  > Thanks for spotting the phantom type replacing example, which is a
> |  > features I?d also like to have. The type family was just a quick idea
> |  > (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)"
> |  > what t looks like with all newtypes unfolded), but it?s not worth the
> |  > loss of flexibility.
> |  >
> |  >
> |  > In some cases, the type family might require less type annotations.
> |  > Consider
> |  > newtype Age = Age Int
> |  > newtype NT1 = NT1 Int
> |  > newtype NT2 = NT2 Int
> |  >
> |  > myCast :: Either NT1 Age -> Either NT2 Age
> |  > myCast = castNT . uncastNT
> |  >
> |  > With two parameters, GHC will not know whether it should cast via
> |  > "Either Int Age" or "Either Int Int", while with a type family there
> |  > will be only one choice, "Concrete (Either NT1 Age) = Either Int Int".
> |  > In general, castNT . uncastNT would have the nice type
> |  >         castNT . uncastNT  :: Concrete a ~ Concrete b => a -> b
> |  > which plainly expresses ?Cast between any to values who have the same
> |  > concrete representation.?. Just as a side remark in case this comes up
> |  > later again.
> |  >
> |  >
> |  >
> |  > BTW, what should the base-case be? I believe most user-friendly is a
> |  > least-specific class
> |  >         instance IsNT a a
> |  > so that the cast "Either Age a -> Either Int a" is possible. Or are
> |  > overlapping instances too bad and the user should derive instances for
> |  > all non-container non-newtype types himself:
> |  >         instance IsNT Int Int ....
> |  >
> |  >
> |  > Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones:
> |  >> The question of how to represent all this in HsSyn, to communicate
> |  >> between TcDeriv and TcInstDcls, is a somewhat separate matter.  We can
> |  >> solve that in several ways.  But first we need be sure what the FC
> |  >> story is.
> |  >
> |  > For now what I am doing is that in TcDeriv, I am implementing the
> |  > method
> |  > with a value "unfinishedNTInstance :: a" which I am then replacing in a
> |  > always-run simplCore pass with the real implementation in Core. It is a
> |  > work-around that lets me explore the design-space and implementation
> |  > issues without having to rewire GHC.
> |  >
> |  > Greetings,
> |  > Joachim
> |  >
> |  >
> |  > _______________________________________________
> |  > 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
>




Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Simon Peyton Jones
|  that seems very fishy and wrong-headed. So, I guess we'll have to have ~R#. I'm
|  tempted to use "~R#" as its name, to make it impossible to write in Haskell code.

Sounds ok to me.

Simon

|  -----Original Message-----
|  From: Richard Eisenberg [mailto:eir at cis.upenn.edu]
|  Sent: 23 July 2013 23:12
|  To: Simon Peyton-Jones
|  Cc: Joachim Breitner; ghc-devs at haskell.org
|  Subject: Re: Exposing newtype coercions to Haskell
|  
|  Yes, that's what I got from Joachim's response to my design, also. My only other
|  thought is to have some way to store an _axiom_, instead of an R coercion. But,
|  that seems very fishy and wrong-headed. So, I guess we'll have to have ~R#. I'm
|  tempted to use "~R#" as its name, to make it impossible to write in Haskell code.
|  Would there be any problems with this? I'll go ahead and include the new coercion
|  form when I commit roles.
|  
|  Richard
|  
|  On Jul 23, 2013, at 7:46 PM, Simon Peyton-Jones wrote:
|  
|  > I thought about the design you suggest below, but rejected it because I don't
|  see how to do lifting -- which is really the whole point! In particular, what are you
|  going to write for
|  >
|  > ntList :: NT a b -> NT [a] [b]
|  > ntList (MkNT castNT uncastNT) = MkNT ??? ???
|  >
|  > For lists you could write (fmap castNT), but the whole point of this exercise is
|  not to write that -- and the type might not be an instance of Functor.
|  >
|  > I'm thinking we need (~R#) as a type constructor.
|  >
|  > Simon
|  >
|  > |  -----Original Message-----
|  > |  From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Richard
|  > |  Eisenberg
|  > |  Sent: 23 July 2013 09:51
|  > |  To: Joachim Breitner
|  > |  Cc: ghc-devs at haskell.org
|  > |  Subject: Re: Exposing newtype coercions to Haskell
|  > |
|  > |  A few responses:
|  > |
|  > |  - As Simon said, there is no great reason we don't have ~R# in Core.
|  > |  It's just that we looked through GHC and, without newtype coercions,
|  > |  there is no need for ~R#, so we opted not to include it. I'm still not
|  > |  convinced we need it for newtype coercions, though. What if we have this
|  > |  in Core?
|  > |
|  > |  > class NT a b = MkNT { castNT :: a -> b ; uncastNT :: b -> a }
|  > |  > NTCo:Age :: Age ~R# Int         -- see [1]
|  > |  > NTAgeInst :: NT Age Int
|  > |  > NTAgeInst = MkNT { castNT = \(a :: Age). a |> NTCo:Age ; uncastNT =
|  \(x
|  > |  > :: Int). x |> sym NTCo:Age }
|  > |
|  > |  [1]: We still do have representational coercions, even though it would
|  > |  be bogus to extract their type, as the type constructor ~R# does not
|  > |  exist. But, coercionKind, which returns the two coerced types, and the
|  > |  new coercionRole (which would return Representational in this case) work
|  > |  just fine.
|  > |
|  > |  Here, we don't need to abstract over ~R#, by just referring to the
|  > |  global axiom directly. Does this compose well? I think so; you'll just
|  > |  have to inline all of the coercions. But, the coercions won't ever get
|  > |  too big, as they will always mirror exactly the structure of the types
|  > |  being coerced. Simon, this is the sort of "magic" I was thinking of,
|  > |  magical because I can't imagine a way this could be produced from an
|  > |  HsExpr.
|  > |
|  > |  Also, nice example of how the one-parameter design might aid the
|  > |  programmer. I think that thinking about the base case is also
|  > |  productive, but I don't have a clear enough opinion to express on that
|  > |  front.
|  > |
|  > |  Richard
|  > |
|  > |  On 2013-07-23 08:21, Joachim Breitner wrote:
|  > |  > Hi Richard and Simon,
|  > |  >
|  > |  > thanks for your detailed notes.
|  > |  >
|  > |  > Am Montag, den 22.07.2013, 17:01 +0100 schrieb Richard Eisenberg:
|  > |  >
|  > |  >> - I think you *do* want HsExprs not CoreExprs. Though I haven't worked
|  > |  >> much in TcDeriv myself, I imagine everything uses HsExprs so that they
|  > |  >> can be type-checked. This allows nice error messages to be reported at
|  > |  >> the site of a user's "deriving instance IsNT ...".
|  > |  >
|  > |  > My plan was to make all checks (constructors in scope; IsNT classes for
|  > |  > all data constructor arguments present) in TcDeriv, so you get nice
|  > |  > error messages. If it turns out that the actual coercion can only be
|  > |  > generated in a later pass, then it the checks just need to be strong
|  > |  > enough to make that pass always succeed.
|  > |  >
|  > |  >> - But, there's a wrinkle here. The (~#) type, along with (~) and (:=:)
|  > |  >> (the last is from the soon-to-be Data.Type.Equality), all work over
|  > |  >> so-called *nominal* coercions.
|  > |  >
|  > |  > I know; I was just using them until representational equality is in and
|  > |  > plan to switch then.
|  > |  >
|  > |  >>  (Nominal coercions correspond to the "C" coercions from this paper)
|  > |  >
|  > |  > I got confused by C and T in my previous mails. In any case, I am only
|  > |  > concerned with representational equality (T, it seems) for this
|  > |  > project.
|  > |  >
|  > |  >> Or, it's possible
|  > |  >> that we could add abstraction over representational coercions, but I
|  > |  >> prefer the magical approach, because I don't see a general need for
|  > |  >> the
|  > |  >> ability to abstract.
|  > |  >
|  > |  > Hmm, I must admit I was assuming that once the roles implementation is
|  > |  > in there will be ~# and ~#/T (or ~R#, which is a less-easy-to-confuse
|  > |  > moniker) available in Core.
|  > |  >
|  > |  >
|  > |  >> Now that I think of it, you may need to generalize the deriving
|  > |  >> mechanism a bit. All current "deriving"s generate code that the user
|  > |  >> could write. (Typeable is something of an exception here.) Here, the
|  > |  >> generated code is something that a user can not write. Maybe that's
|  > |  >> why
|  > |  >> you wanted CoreExprs in the first place!
|  > |  >
|  > |  > Exactly. But it is also the reason why we are aiming for deriving
|  > |  > classes (and not NT values), because it is already an established way
|  > |  > of
|  > |  > having the compiler generate code for you.
|  > |  >
|  > |  >
|  > |  >> - I prefer the two-parameter class over a one-parameter, as it seems
|  > |  >> more flexible.
|  > |  >
|  > |  > Thanks for spotting the phantom type replacing example, which is a
|  > |  > features I'd also like to have. The type family was just a quick idea
|  > |  > (and it would be neat to be able to ask GHCi via ":kind! (Concrete t)"
|  > |  > what t looks like with all newtypes unfolded), but it's not worth the
|  > |  > loss of flexibility.
|  > |  >
|  > |  >
|  > |  > In some cases, the type family might require less type annotations.
|  > |  > Consider
|  > |  > newtype Age = Age Int
|  > |  > newtype NT1 = NT1 Int
|  > |  > newtype NT2 = NT2 Int
|  > |  >
|  > |  > myCast :: Either NT1 Age -> Either NT2 Age
|  > |  > myCast = castNT . uncastNT
|  > |  >
|  > |  > With two parameters, GHC will not know whether it should cast via
|  > |  > "Either Int Age" or "Either Int Int", while with a type family there
|  > |  > will be only one choice, "Concrete (Either NT1 Age) = Either Int Int".
|  > |  > In general, castNT . uncastNT would have the nice type
|  > |  >         castNT . uncastNT  :: Concrete a ~ Concrete b => a -> b
|  > |  > which plainly expresses "Cast between any to values who have the same
|  > |  > concrete representation.". Just as a side remark in case this comes up
|  > |  > later again.
|  > |  >
|  > |  >
|  > |  >
|  > |  > BTW, what should the base-case be? I believe most user-friendly is a
|  > |  > least-specific class
|  > |  >         instance IsNT a a
|  > |  > so that the cast "Either Age a -> Either Int a" is possible. Or are
|  > |  > overlapping instances too bad and the user should derive instances for
|  > |  > all non-container non-newtype types himself:
|  > |  >         instance IsNT Int Int ....
|  > |  >
|  > |  >
|  > |  > Am Dienstag, den 23.07.2013, 05:23 +0000 schrieb Simon Peyton-Jones:
|  > |  >> The question of how to represent all this in HsSyn, to communicate
|  > |  >> between TcDeriv and TcInstDcls, is a somewhat separate matter.  We can
|  > |  >> solve that in several ways.  But first we need be sure what the FC
|  > |  >> story is.
|  > |  >
|  > |  > For now what I am doing is that in TcDeriv, I am implementing the
|  > |  > method
|  > |  > with a value "unfinishedNTInstance :: a" which I am then replacing in a
|  > |  > always-run simplCore pass with the real implementation in Core. It is a
|  > |  > work-around that lets me explore the design-space and implementation
|  > |  > issues without having to rewire GHC.
|  > |  >
|  > |  > Greetings,
|  > |  > Joachim
|  > |  >
|  > |  >
|  > |  > _______________________________________________
|  > |  > 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
|  >
|  





Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Joachim Breitner-2
In reply to this post by Simon Peyton Jones
Hi,

Am Dienstag, den 23.07.2013, 18:58 +0000 schrieb Simon Peyton-Jones:
> If you add -XIncoherentInstances *just to the module that has instance
> IsNT a a*, then it'll work fine I think.  This says "pick this
> instance even though an instantiation of the constraint might match a
> more specific instance".  You don't need the flag in importing
> modules.

That does not seem to be the case: Enabling the flag just for the
special "IsNT a a" instance does not work:


Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)

<interactive>:1:1:
    Overlapping instances for IsNT a1 a1 arising from a use of ?castNT?
    Matching instances:
      instance [incoherent] IsNT a a -- Defined at <interactive>:12:10
      instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
        -- Defined at <interactive>:7:1
    (The choice depends on the instantiation of ?a1?
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the expression: castNT :: (Either Int a) -> (Either Age a)

(as correctly specified by the error message.)


But now the solution is easy to see: When deriving IsNT, simply set the
incoherent flag for every instance, independent of any active pragmas.

Greetings,
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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130724/c899a940/attachment.pgp>

Reply | Threaded
Open this post in threaded view
|

Exposing newtype coercions to Haskell

Richard Eisenberg-2
Hi Joachim,

As discussed previously, I do think we need a way to store representational coercions. In my roles branch (which is getting close to pushing, I believe), I have created eqReprPrimTyCon, which is like eqPrimTyCon, but it is the type of coercions witnessing representational equality. The Id stored in a CoVarCo can usefully have a type headed by eqReprPrimTyCon.

If you're really eager to take a look, I use github to coordinate among computers; you can see the roles branch at github.com/goldfirere/ghc.

Richard

On Jul 24, 2013, at 8:31 AM, Joachim Breitner wrote:

> Hi,
>
> Am Dienstag, den 23.07.2013, 18:58 +0000 schrieb Simon Peyton-Jones:
>> If you add -XIncoherentInstances *just to the module that has instance
>> IsNT a a*, then it'll work fine I think.  This says "pick this
>> instance even though an instantiation of the constraint might match a
>> more specific instance".  You don't need the flag in importing
>> modules.
>
> That does not seem to be the case: Enabling the flag just for the
> special "IsNT a a" instance does not work:
>
>
> Prelude GHC.NT> :t  castNT :: (Either Int a) -> (Either Age a)
>
> <interactive>:1:1:
>    Overlapping instances for IsNT a1 a1 arising from a use of ?castNT?
>    Matching instances:
>      instance [incoherent] IsNT a a -- Defined at <interactive>:12:10
>      instance (IsNT a a', IsNT b b') => IsNT (Either a b) (Either a' b')
>        -- Defined at <interactive>:7:1
>    (The choice depends on the instantiation of ?a1?
>     To pick the first instance above, use -XIncoherentInstances
>     when compiling the other instance declarations)
>    In the expression: castNT :: (Either Int a) -> (Either Age a)
>
> (as correctly specified by the error message.)
>
>
> But now the solution is easy to see: When deriving IsNT, simply set the
> incoherent flag for every instance, independent of any active pragmas.
>
> Greetings,
> 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
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs




12