Note [FunTy vs non-FunTy case in tc_sub_type_deep]
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
- FunTy vs FunTy case in tc_sub_type_deep GHC.Tc.Utils.Unify
Referenced by 2
- Deep subsumption GHC.Tc.Utils.Unify
- GHC.Tc.Utils.Unify call site