Exposing newtype coercions to Haskell

[Joachim Breitner]

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
-------------- 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/20130723/795d6de2/attachment.pgp>