Note [FunTy vs non-FunTy case in tc_sub_type_deep]

GHC/Tc/Utils/Unify.hs:1859 compiler

Consider this, without Quick Look, but with Deep Subsumption:
   f :: ∀a b c. a b c -> Int
   g :: Bool -> ∀d. d -> d
To typecheck the application (f g), we need to do the subsumption test

  (Bool -> ∀ d. d->d)   <=   alpha beta gamma

where alpha, beta, gamma are the unification variables that instantiate a,b,c
(respectively). We must not drop down to unification, or we will reject the call.
Instead, we should only unify alpha := (->), in which case we end up with the
usual FunTy vs FunTy case of Note [FunTy vs FunTy case in tc_sub_type_deep]:

  (Bool -> ∀ d. d->d)   <=   beta -> gamma

which is straightforwardly solved by beta := Bool, using covariance in the return
type of the function arrow, and instantiating the forall before unifying with gamma.

The conclusion is this: when doing a deep subtype check (in tc_sub_type_deep),
if the LHS is a FunTy and the RHS is a rho-type which is not a FunTy,
then unify the RHS with a FunTy and continue by performing a sub-type check on
the LHS vs the new RHS. And vice-versa (if it's the RHS that is a FunTy).

See T11305 and T26225 for examples of when this is important.

References 1

Referenced by 2