## #14661 closed feature request (wontfix)

# Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F

Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | |

Component: | Compiler | Version: | 8.4.1-alpha1 |

Keywords: | DerivingStrategies, deriving, TypeFamilies | Cc: | |

Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |

Type of failure: | None/Unknown | Test Case: | |

Blocked By: | Blocking: | ||

Related Tickets: | Differential Rev(s): | ||

Wiki Page: |

### Description

This works fine

{-# Language PolyKinds #-} {-# Language GADTs #-} {-# Language GeneralizedNewtypeDeriving #-} {-# Language InstanceSigs #-} {-# Language RankNTypes #-} {-# Language ScopedTypeVariables #-} {-# Language StandaloneDeriving #-} {-# Language TypeApplications #-} {-# Language DataKinds #-} {-# Language DerivingStrategies #-} {-# Language TypeFamilies #-} import Data.Kind import Control.Category import Prelude hiding (id, (.)) import Data.Coerce data TY = TI | TB type family Interp ty where Interp TI = Int Interp TB = Bool newtype Ixed :: TY -> TY -> Type where Ixed :: (Interp ix -> Interp ix') -> (Ixed ix ix') -- deriving newtype Category instance Category Ixed where id :: forall a. Ixed a a id = coerce (id @(->) @(Interp a)) (.) :: forall b c a. Ixed b c -> Ixed a b -> Ixed a c (.) = coerce ((.) @(->) @(Interp b) @(Interp c) @(Interp a))

This instance can **not** be derived using `newtype`

deriving. Commenting the `Category`

-instance out and uncommenting `deriving newtype Category`

results in an error

$ ghci2 -ignore-dot-ghci hs/164-trac.hs GHCi, version 8.5.20180105: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( hs/164-trac.hs, interpreted ) hs/164-trac.hs:28:20: error: • Can't make a derived instance of ‘Category Ixed’ with the newtype strategy: cannot eta-reduce the representation type enough • In the newtype declaration for ‘Ixed’ | 28 | deriving newtype Category | ^^^^^^^^ Failed, no modules loaded. Prelude>

I may have asked this before, but can we make GHC smart enough to derive this instance? It consists entirely of the right visible type application of `method`

: `method = coerce (method @a @b @..)`

### Change History (15)

### comment:1 follow-up: 2 Changed 2 years ago by

### comment:2 Changed 2 years ago by

Replying to simonpj:

Same thing happens with

`data Interp a = I`

.

Well sure—you can't use `GeneralizedNewtypeDeriving`

on a non-newtype.

I agree that the type family is a red herring, though. Let's look at a slightly simpler example:

{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} import Control.Category data Bar a newtype Foo a b = MkFoo (Bar a -> Bar b) deriving newtype Category

• Can't make a derived instance of ‘Category Foo’ with the newtype strategy: cannot eta-reduce the representation type enough • In the newtype declaration for ‘Foo’ | 9 | deriving newtype Category | ^^^^^^^^

Why is this happening? As per the specification of `GeneralizedNewtypeDeriving`

in the users' guide, GHC must be able to eta-convert `Foo`

's underlying representation type (i.e., `Bar a -> Bar b`

) in order to generate a context. But you cannot eta-reduce the type variables `a`

and `b`

from `Bar a -> Bar b`

, try as you might.

Returning to your original example, you claim that the instance you hand-wrote "consists entirely of the right visible type application of `method: method = coerce (method @a @b @..)`

", but this isn't true. Look at your `id`

implementation, for instance:

id :: forall a. Ixed a a id = coerce (id @(->) @(Interp a))

This is a good deal more clever than what `GeneralizedNewtypeDeriving`

currently does. GND would try to coerce from `id :: forall a. Ixed a a`

to `id :: forall a. ??? a a`

, where `???`

is the eta-reduced representation type (that we were unable to obtain, as explained previously). But your implementation tunnels down through `(->)`

and exploits the fact that `Interp`

happens to be present on both sides of the arrow.

This insider knowledge would not be particularly simple to teach GHC—for instance, what happens if you chance `Ixed`

to be of type `(Interp ix -> Maybe (Interp ix') -> (Ixed ix ix')`

? Moreover, the kinds of tricks that would work for `Category`

/`(->)`

would likely not be applicable for other type class/type constructor combinations.

**tl;dr** I claim this is not a bug, but rather a misunderstanding of how `GeneralizedNewtypeDeriving`

works.

### comment:3 Changed 2 years ago by

Type: | bug → feature request |
---|

Changed it to a feature request. This is actually a new deriving strategy.

A second derivation for the same thing: I am able to mechanically write type constructors like this (clever / insider knowledge? I don't think so) and it compiles:

instance Category Ixed where id = Ixed id Ixed f . Ixed g = Ixed (f . g)

With this derivation your other example `newtype Ixed ix ix' = Ixed (Interp ix -> Maybe (Interp ix'))`

does not compile.

I am experimenting with categories over type families / data types and the above instance is boilerplate. This space may be too limited to be worth it, maybe someone else has useful examples of a different character.

### comment:4 Changed 2 years ago by

Similar example from Conal's Compiling to Categories, **7.6 Incremental Computation**

class HasDelta a where type Delta a :: Type newtype DelX a b = DelX (Delta a -> Delta b) instance Category DelX where type Ok DelX = HasDelta id = DelX id DelX g . DelX f = DelX (g . f) instance Cartesian DelX where exl = DelX exl exr = DelX exr DelX f &&& DelX g = DelX (f &&& g)

### comment:5 Changed 2 years ago by

This can be derived (clunkily) with GND + `singletons`

import Data.Singletons type Cat ob = ob -> ob -> Type newtype WRAP :: (k' ~> k) -> (Cat k -> Cat k') where WRAP :: cat (f@@a) (f@@b) -> WRAP f cat a b instance Category cat => Category (WRAP f cat) where id :: forall a. WRAP f cat a a id = WRAP (id @cat @(f@@a)) (.) :: forall b c a. WRAP f cat b c -> WRAP f cat a b -> WRAP f cat a c WRAP f . WRAP g = WRAP ((.) @cat @(f@@b) @(f@@c) @(f@@a) f g) data InterpSym0 :: TY ~> Type type instance InterpSym0 @@ ty = Interp ty

+

newtype Ixed a b = Ixed (WRAP InterpSym0 (->) a b) deriving newtype Category

or with `-XDerivingVia`

newtype Ixed a b = Ixed (Interp a -> Interp b) deriving Category via (WRAP InterpSym0 (->) a b)

### comment:6 Changed 2 years ago by

My belief is that `DerivingVia`

is exactly what you're looking for (instead of attempting to encode this into GHC somehow in an *ad hoc* fashion).

### comment:7 Changed 2 years ago by

Yes this logic should rather be defined in a module/library than in GHC. Any thoughts Simon? Can close this

### comment:8 Changed 2 years ago by

Well sure—you can't use GeneralizedNewtypeDeriving on a non-newtype

The newtype is called `Ixed`

. The type function is `Interp`

. Turning it into a data type (and removing the instances) simplifies the example, but does not affect the payload.

### comment:9 follow-up: 11 Changed 2 years ago by

Trac 14661

Hmm. What is `DerivingVia`

? Is it implemented, documented?

I agree this is a feature request, going significantly beyond what GHC can do right now.

However, the new feature looks tantalisingly close.
E.g. for `instance Category Ixed`

we need to find

id :: forall a. Ixed a a

Expanding the type representation gives

id1 :: forall a. Interp a -> Interp a

We have in hand the `(->)`

instance of `Category`

:

id @(->) :: forall b. b -> b

and in fact we can readily instantiate `id @(->)@`

to match the needed type.

So, could we imagine this? Given

newtype N a b = MkN (R t1 t2 t3) deriving( Category )

we want to derive `instance ... => C N`

given `instance ... => C R`

.
Suppose we have a method in class `C`

class R (c :: * -> * -> *) where foo :: forall p q. ...(c s1 s2)...

(NB: for now I will assume that `c`

appears fully applied in `foo`

's type.)
Then we will have available `foo1 :: forall p q. ...(R s1 s2)...`

and we want to get `foo2 :: forall p q. ...(N s1 s2)...`

.

Well from the newtype declaration we have an axiom that equates the representation
types of `(N a b)`

and `(R t1 t2 t3)`

:

ax :: forall a b. N a b ~R R t1 t2 t3

So, if we could find

foo3 :: forall p q. ...(R t1[s1/a,s2/q] t2[s1/a,s2/q] t3[s1/a,s2/q]) ...

we'd be home and dry, because then we can use `ax`

to get from `foo3`

to `foo2`

.

How can we get `foo3`

? Well, it's possible that we can get it just by instantiating
the type of `foo1`

. In the case of `id`

in `Category`

we have

id1 :: forall a. (->) a a -- Available, given id2 :: forall a. Ixed a a -- Wanted id3 :: forall a. (->) (Interp a) (Interp a) -- Wanted

And indeed we can get `id3`

from `id1`

by instantiation.

This won't always work as Ryan points out, but sometimes. And I suppose we could work that out.

It seems rather elaborate though!

### comment:10 Changed 2 years ago by

Resolution: | → wontfix |
---|---|

Status: | new → closed |

Apologies simonpj, comment:6 wouldn't have made sense except to Iceland_jack, myself, and a handful of other people.

`DerivingVia`

is the code name we're using to describe a work-in-progress deriving strategy that we're developing, based on this HaskellX talk that Iceland_jack gave. This would allow you to write something of the form:

newtype Ixed a b = Ixed (Interp a -> Interp b) deriving Category via (WRAP InterpSym0 (->) a b)

Where `WRAP`

is a separate data type that has exactly the right `Category`

instance that you'd want for `Ixed`

. It would generate the following code:

instance Category Ixed where id = coerce @(forall a. Ixed a a) @(forall a. WRAP InterpSym0 (->) a a) id (.) = coerce @(forall a b c. Ixed b c -> Ixed a b -> Ixed a c) @(forall a b c. WRAP InterpSym0 (->) b c -> WRAP InterpSym0 (->) a b -> WRAP InterpSym0 (->) a c) (.)

Another way of thinking about it is that it's an even more generalized form of `GeneralizedNewtypeDeriving`

where the user is allowed to specify their own type to `coerce`

from (instead of being required to use a newtype's underlying representation type).

It's not fully documented at the moment, but we do have a WIP specification here if you're curious.

Anyways, I'll opt to close this, since Iceland_jack seems OK with the idea of using `DerivingVia`

to accomplish this task.

### comment:11 Changed 23 months ago by

Replying to simonpj:

However, the new feature looks tantalisingly close.

This won't always work as Ryan points out, but sometimes. And I suppose we could work that out.

It seems rather elaborate though!

I agree that it's tantalising, if you think it's a general enough solution, enough “bang for the buck” then re-open. But there is no hurry on my end, I'd like more examples that need this.

### comment:12 Changed 23 months ago by

I don't know if this should be a separate ticket but it is another case that can be derived only by expanding constructors

import Data.Monoid (Endo) newtype ENDO = ENDO (forall xx. Endo xx) instance Semigroup ENDO where (<>) :: ENDO -> ENDO -> ENDO ENDO f <> ENDO g = ENDO (f <> g) instance Monoid ENDO where mempty :: ENDO mempty = ENDO mempty

Can also be derived using `via`

and quantified constraints (or constraints)

newtype ENDO = ENDO (forall xx. Endo xx) deriving (Semigroup, Monoid) via (Forall Endo) ---- instance Forall :: (k -> Type) -> Type where Forall :: (forall xx. f xx) -> Forall f instance (forall xx. Semigroup (f xx)) => Semigroup (Forall f) where Forall xs <> Forall ys = Forall (xs <> ys) instance (forall xx. Monoid (f xx)) => Monoid (Forall f) where mempty = Forall mempty

### comment:13 Changed 23 months ago by

Here is an interesting one:

class ListLike f where nil :: f a cons :: a -> f a -> f a (·) :: f a -> f a -> f a newtype LL a = LL (forall zz. ListLike zz => zz a)

You can implement (but not derive) `ListLike LL`

:

instance ListLike LL where nil :: LL a nil = LL nil cons :: a -> LL a -> LL a cons a (LL as) = LL (cons a as) (·) :: LL a -> LL a -> LL a LL as · LL bs = LL (as · bs)

I'll add further examples to this gist.

### comment:14 Changed 23 months ago by

Your example in comment:12 is quite interesting. It only fails because GHC attempts to generate the constraint `Semigroup (forall xx. Endo xx)`

and immediately chokes. But we never intended to generate that constraint—we wanted `forall xx. Semigroup (Endo xx)`

, a quantified constraint!

I would posit that if we derive instances that require slapping a class onto a type, we should be pushing the class through `forall`

s and other constraints. For instance, if we want to apply `Semigroup`

to `forall xx. Endo xx`

, we should push `Semigroup`

through `forall xx`

to obtain `forall xx. Show (Endo xx)`

, and then chuck *that* into the constraint solver.

(I think this same strategy would work with the program in comment:13, as we really want to generate the constraint `forall zz. ListLike zz => ListLike zz`

, which could be discharged immediately. But that might require #14733 to be fixed, so perhaps it's not as good of a motivating example.)

All of this assumes `QuantifiedConstraints`

, of course, so it's not really actionable right now. Iceland_jack, perhaps you could open a separate ticket for this? (With the keyword `deriving`

in there so that I can find it later.)

### comment:15 Changed 23 months ago by

I had a burning curiosity, so I quickly implemented the ideas sketched out in comment:14 to see if they'd work. To my great surprise, the changes almost work perfectly! But I did use the word "almost"—there's a pretty big snag that prevents `newtype ENDO = ENDO (forall xx. Endo xx) deriving Semigroup`

from working. To better explain what's going on, here is the code that `-ddump-deriv`

is producing:

{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} module Bug where import Data.Coerce import Data.Kind import Data.List.NonEmpty import Data.Monoid import Data.Semigroup newtype ENDO = ENDO (forall a. Endo a) instance Semigroup ENDO where (<>) = coerce @((forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ) @(ENDO -> ENDO -> ENDO) (<>) sconcat = coerce @(NonEmpty (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ) @(NonEmpty ENDO -> ENDO) sconcat stimes = coerce @(forall (b_a2d8 :: Type). Integral b_a2d8 => b_a2d8 -> (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ) @(forall (b_a2d8 :: Type). Integral b_a2d8 => b_a2d8 -> ENDO -> ENDO) stimes

`(<>)`

and `stimes`

actually typecheck without issue, to my great joy. But alas, `sconcat`

does not:

Bug.hs:25:9: error: • Couldn't match type ‘forall a_a3ZJ1. Endo a_a3ZJ1’ with ‘Endo a_a3ZJ’ Expected type: NonEmpty (forall a_a3ZJ1. Endo a_a3ZJ1) -> Endo a_a3ZJ Actual type: NonEmpty (Endo a_a3ZJ) -> Endo a_a3ZJ • In the third argument of ‘coerce’, namely ‘sconcat’ In the expression: coerce @(NonEmpty (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ) @(NonEmpty ENDO -> ENDO) sconcat In an equation for ‘sconcat’: sconcat = coerce @(NonEmpty (forall (a_a3ZJ :: Type). Endo a_a3ZJ) -> forall (a_a3ZJ :: Type). Endo a_a3ZJ) @(NonEmpty ENDO -> ENDO) sconcat | 25 | sconcat | ^^^^^^^

It seems that GHC is unwilling to instantiate `sconcat`

at an impredicative type, even with `ImpredicativeTypes`

enabled. What's annoying is that *this* typechecks:

{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} module Bug2 where import Data.Coerce import Data.Monoid import Data.List.NonEmpty import Data.Semigroup newtype ENDO = ENDO (forall a. Endo a) test :: (NonEmpty (forall a. Endo a) -> (forall a. Endo a)) -> (NonEmpty ENDO -> ENDO) test = coerce @(NonEmpty (forall a. Endo a) -> (forall a. Endo a)) @(NonEmpty ENDO -> ENDO)

But, as we saw in the earlier example, trying to give `sconcat`

as an argument to a function with such a type signature would cause GHC to choke. It seems that we'd need more impredicative smarts to make this all work.

**Note:**See TracTickets for help on using tickets.

Interesting. The type family is a red herring. Same thing happens with

`data Interp a = I`

.