Refactor DeriveFunctor to handle rank-n field types better

DeriveFunctor falls over on constructors with sufficiently complicated rank-n field types, such as this one:

data T a = MkT (forall b. b -> (forall c. a -> c) -> a)
  deriving Functor

GHC will try to generate the following code for the derived Functor T instance:

instance Functor T where
  fmap f (MkT a1)
    = MkT
        ((\ b7 b8
            -> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
                 (b7 ((\ b1 -> b1) b8)))
           a1)

This fails to typecheck with the following error:

Bug.hs:15:12: error:
    • Couldn't match type ‘forall c. a -> c’ with ‘a -> p0’
      Expected type: b1 -> (a -> p0) -> a
        Actual type: b1 -> (forall c. a -> c) -> a
    • In the first argument of ‘\ b7 b8
                                  -> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
                                       (b7 ((\ b1 -> b1) b8))’, namely
        ‘a1’
      In the first argument of ‘MkT’, namely
        ‘((\ b7 b8
             -> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
                  (b7 ((\ b1 -> b1) b8)))
            a1)’
      In the expression:
        MkT
          ((\ b7 b8
              -> (\ b5 b6 -> f (b5 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6)))
                   (b7 ((\ b1 -> b1) b8)))
             a1)
    • Relevant bindings include
        a1 :: forall b. b -> (forall c. a -> c) -> a
          (bound at Bug.hs:10:15)
        f :: a -> b (bound at Bug.hs:10:8)
        fmap :: (a -> b) -> T a -> T b (bound at Bug.hs:10:3)
   |
15 |            a1)
   |            ^^

However, it would typecheck if the generated right-hand side were beta-reduced a little bit more:

instance Functor T where
  fmap f (MkT g)
      = MkT
          (\ b8
              -> (\ b6 -> f (g b8 ((\ b3 b4 -> (\ b2 -> b2) (b3 (f b4))) b6))))

We should refactor DeriveFunctor so that it generates this sort of code. Paraphrasing Simon's suggestion from !2600 (comment 256528), here is the current design of $fmap, the type-driven transformer function that powers DeriveFunctor's codegen:

  $(fmap 'a 'b)          =  \x -> x     -- when b does not contain a
  $(fmap 'a 'a)          =  f
  $(fmap 'a '(b1,b2))    =  \x -> case x of (x1,x2) -> ($(fmap 'a 'b1) x1, $(fmap 'a 'b2) x2)
  $(fmap 'a '(T b1 b2))  =  fmap $(fmap 'a 'b2)   -- when a only occurs in the last parameter, b2
  $(fmap 'a '(b -> c))   =  \x b -> $(fmap 'a' 'c) (x ($(cofmap 'a 'b) b))

$(fmap a ty) produces a term of type ty -> ty[b/a]. Notice how the case for function types (i.e., $(fmap 'a '(b -> c)) = \x b -> ...) generates a lambda expression with two arguments, where the first argument x is a function type. This is exactly the argument we want to beta reduce.

We can accomplish this beta reduction by giving $fmap an extra argument term (e.g., x1) along with its type (e.g., ty1). So in a call $(fmap a ty x), we have:

• There is a precondition that x :: ty.

• The call produces a term of type ty[b/a]:

  $(fmap 'a 'b x)          =  x     -- when b does not contain a
  $(fmap 'a 'a x)          =  f x
  $(fmap 'a '(b1,b2) x)    =  case x of (x1,x2) -> ($(fmap 'a x1 'b1) x1, $(fmap 'a x2 'b2))
  $(fmap 'a '(T b1 b2) x)  =  fmap (\y. $(fmap 'a y 'b2)) x   -- when a only occurs in the last parameter, b2
  $(fmap 'a '(tb -> tc) x) =  \(y:tb[b/a]) -> $(fmap 'a' 'tc' (x $(cofmap 'a 'tb y)))

This was spun off from this discussion, where this idea was proposed as a way to make DeriveFunctor continue to work on things like data T a = MkT (Int -> forall c. c -> a) deriving Functor after simplified subsumption is implemented. But this idea can be implemented independently, as it makes more programs typecheck even without the need for simplified subsumption.