Note [FunTy vs FunTy case in tc_sub_type_deep]

The goal of tc_sub_type_deep is to produce an HsWrapper that "proves" that the
actual type is a subtype of the expected type. The most important case is how
we deal with function arrows. Suppose we have:

  ty_actual   = act_arg -> act_res
  ty_expected = exp_arg -> exp_res

To produce fun_wrap :: (act_arg -> act_res) ~> (exp_arg -> exp_res), we use
the fact that the function arrow is contravariant in its argument type and
covariant in its result type. Thus we recursively perform subtype checks
on the argument types (with actual/expected switched) and the result types,
to get:

  arg_wrap :: exp_arg ~> act_arg   -- NB: expected/actual have switched sides
  res_wrap :: act_res ~> exp_res

Then fun_wrap = mkWpFun arg_wrap res_wrap.

Wrinkle [Representation-polymorphism checking during subtyping]

  Inserting a WpFun HsWrapper amounts to impedance matching in deep subsumption
  via eta-expansion:

    f  ==>  \ (x :: exp_arg) -> res_wrap [ f (arg_wrap [x]) ]

  As we produce a lambda, we must enforce the representation polymorphism
  invariants described in Note [Representation polymorphism invariants] in GHC.Core.
  That is, we must ensure that both x (the lambda binder) and (arg_wrap [x]) (the function argument)
  have a fixed runtime representation.

  Note however that desugaring mkWpFun does not always introduce a lambda: if
  both the argument and result HsWrappers are casts, then a FunCo cast suffices,
  in which case we should not perform representation-polymorphism checking.

  This means that, in the FunTy/FunTy case of tc_sub_type_deep, we can skip
  the representation-polymorphism checks if the produced argument and result
  wrappers are identities or casts.
  It is important to do so, otherwise we reject valid programs.

    Here's a contrived example (there are undoubtedly more natural examples)
    (see testsuite/tests/rep-poly/NoEtaRequired):

      type Id :: k -> k
      type family Id a where

      type T :: TYPE r -> TYPE (Id r)
      type family T a where

      test :: forall r (a :: TYPE r). a :~~: T a -> ()
      test HRefl =
        let
          f :: (a -> a) -> ()
          f _ = ()
          g :: T a -> T a
          g = undefined
        in f g

    We don't need to eta-expand `g` to make `f g` typecheck; a cast suffices.
    Hence we should not perform representation-polymorphism checks; they would
    fail here.