Re: [GHC] #14661: Cannot derive (newtype I a b = I (F a -> F b) deriving newtype Category) for type family F

1 Feb 2018

      #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