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