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@haskell.org] On Behalf Of Joachim | Breitner | Sent: 23 July 2013 12:45 | To: ghc-devs@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@joachim-breitner.de | Homepage: http://www.joachim-breitner.de | ICQ#: 74513189 | Jabber-ID: nomeata@joachim-breitner.de