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

12 Jan 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:  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