[GHC] #14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Keywords: | Operating System: Unknown/Multiple DerivingStrategies, deriving, | TypeFamilies | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This works fine {{{#!hs {-# 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 @..)` -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Interesting. The type family is a red herring. Same thing happens with `data Interp a = I`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:1 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: {{{#!hs {-# 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 [https://downloads.haskell.org/~ghc/8.2.2/docs/html/users_guide/glasgow_exts.... -more-precise-specification 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * type: bug => feature request Comment: 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: {{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Similar example from Conal's [http://conal.net/papers/compiling-to- categories/compiling-to-categories.pdf Compiling to Categories], **7.6 Incremental Computation** {{{#!hs 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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): This can be derived (clunkily) with GND + `singletons` {{{#!hs 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 }}} + {{{#!hs newtype Ixed a b = Ixed (WRAP InterpSym0 (->) a b) deriving newtype Category }}} or with `-XDerivingVia` {{{#!hs newtype Ixed a b = Ixed (Interp a -> Interp b) deriving Category via (WRAP InterpSym0 (->) a b) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Yes this logic should rather be defined in a module/library than in GHC. Any thoughts Simon? Can close this -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): 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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: wontfix | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => wontfix Comment: 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 [https://skillsmatter.com/skillscasts/10934-lightning-talk-stolen- instances-taste-just-fine HaskellX talk] that Iceland_jack gave. This would allow you to write something of the form: {{{#!hs 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: {{{#!hs 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 [https://github.com/Icelandjack/deriving- via/blob/06cb4fffbac68a7ca788ce1778f76c971906911e/paper/Specification_sketch.markdown 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: wontfix | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:9 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: wontfix | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I don't know if this should be a separate ticket but it is another case that can be derived only by expanding constructors {{{#!hs 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: wontfix | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Here is an interesting one: {{{#!hs 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`: {{{#!hs 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 [https://gist.github.com/Icelandjack/b1185398719f5932b6906396fb67a9f9 gist]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:13 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: wontfix | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:14 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.4.1-alpha1 Resolution: wontfix | Keywords: | DerivingStrategies, deriving, | TypeFamilies Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): 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: {{{#!hs {-# 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: {{{#!hs {-# 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14661#comment:15 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC