{-# INLINE afvFolder #-}   -- so that specialization to (const True) works

 afvFolder :: (TyCoVar -> Bool) -> TyCoFolder (FV TyCoVarSet DM.Any)

 -- 'afvFolder' is short for "any-free-var folder", good for checking

 afvFolder check_fv = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]

                                 , tcf_tyvar = do_tcv, tcf_covar = do_tcv

                                 , tcf_hole = do_hole

                                 , tcf_tycobinder = addBndrFV }

   where

 anyFreeVarsOfType :: (TyCoVar -> Bool) -> Type -> Bool

 anyFreeVarsOfType check_fv ty = DM.getAny (runFVTop (f ty))

 -- plus the modification in Fig 5, of the QL paper:

 -- "A quick look at impredicativity" (ICFP'20).

 tcInstFun do_ql inst_final rn_head@(_, fun_lspan) tc_fun fun_sigma rn_args

                                    , text "rn_fun" <+> ppr rn_head

                                    , text "fun_sigma" <+> ppr fun_sigma

                                    , text "args:" <+> ppr rn_args

        ; fun_origin <- mk_origin rn_head

        ; res@(_, fun_ty) <- go fun_origin 1 [] fun_sigma rn_args

        ; traceTc "tcInstFun:ret" (ppr fun_ty)

                -- is not fully zonked, because ty_arg is fully zonked.

                -- See Note [Type application substitution].

        ; traceTc "tc_inst_forall_arg (VTA/VDQ)" (

                   vcat [ text "fun_ty" <+> ppr fun_ty

                        , text "tv" <+> ppr tv <+> dcolon <+> debugPprType kind

                        , text "ty_arg" <+> debugPprType ty_arg <+> dcolon

                                        <+> debugPprType (typeKind ty_arg)

                        , text "inner_ty" <+> debugPprType inner_ty

        ; return (ty_arg, insted_ty) }

 {- Note [Visible type application and abstraction]

          -- capture and save it in the `EValArgQL`.  See (QLA6) in

          -- Note [Quick Look at value arguments]

        ; traceTc "quickLookArg {" $

          vcat [ text "arg:" <+> ppr arg

               , text "orig_arg_rho:" <+> ppr orig_arg_rho

               , text "head:" <+> ppr rn_fun_arg <+> dcolon <+> ppr mb_fun_ty

        ; case mb_fun_ty of {

            Nothing -> skipQuickLook app_lspan larg sc_arg_ty ;    -- fun is too complicated

 --   * It may return without having made the argument types equal, of course;

 --     it just makes best efforts.

 qlUnify ty1 ty2

        ; go ty1 ty2 }

   where

     go :: TcType -> TcType -> TcM ()

     -- Decompose (arg1 -> res1) ~ (arg2 -> res2)

     -- and         (c1 => res1) ~   (c2 => res2)

     -- But for the latter we only learn instantiation info from res1~res2

        (FunTy { ft_af = af2, ft_arg = arg2, ft_res = res2 })

       | af1 == af2 -- Match the arrow TyCon

         -- NB: we do not unify the multiplicities; that would be too strong.

         -- We might only require mult1 ⩽ mult2, as in Note [Multiplicity in deep subsumption].

            ; go res1 res2 }

     -- Make sure to not unify "kappa := (a %1 -> b)". See (UQL5).

       -- NB: we do want to be able to unify "kappa := a => b", as that's

       -- the main point of QuickLook (allowing meta-variables to be unified

       -- with qualified types).

       | isMetaTyVar tv = go_kappa tv ty2

       | isMetaTyVar tv = go_kappa tv ty1

       | tc1 == tc2 -- See GHC.Tc.Utils.Unify

       = return ()  -- Note [Expanding synonyms during unification]

     -- Now, and only now, expand synonyms

       | Just rho1 <- coreView rho1 = go rho1 rho2

       | Just rho2 <- coreView rho2 = go rho1 rho2

       | tc1 == tc2

       , not (isTypeFamilyTyCon tc1)

       , tys1 `equalLength` tys2

     -- Don't allow unifying (a => b) with the AppTy 'arr[tau] a b'.

     -- To ensure this, use 'tcSplitAppTyNoView_maybe' which does not split (=>).

       | Just (t2a, t2b) <- tcSplitAppTyNoView_maybe ty2

       = do { go t1a t2a; go t1b t2b }

       | Just (t1a, t1b) <- tcSplitAppTyNoView_maybe ty1

       = do { go t1a t2a; go t1b t2b }

        -- Don't look under foralls; see (UQL4) of Note [QuickLook unification]

     ----------------

               -- Here we are in the TcM monad, which does not track enclosing

               -- Given equalities; so for quick-look unification we conservatively

               -- treat /any/ level outside this one as untouchable. Hence cur_lvl.

            ; case simpleUnifyCheck UC_QuickLook cur_lvl kappa ty2 of

               SUC_CanUnify ->

                 do { co <- unifyKind (Just (TypeThing ty2)) ty2_kind kappa_kind

                            -- unifyKind: see (UQL2) in Note [QuickLook unification]

                    ; traceTc "qlUnify:update" $

                      ppr kappa <+> text ":=" <+> ppr ty2

                    ; liftZonkM $ writeMetaTyVar kappa ty2' }

            }

       where

         kappa_kind = tyVarKind kappa

 import GHC.Types.Var as Var

 import GHC.Types.Var.Set

 import GHC.Types.Var.Env

 import GHC.Types.Basic

 import GHC.Types.Unique.Set (nonDetEltsUniqSet)

 import Control.Monad

 import Data.Functor.Identity (Identity(..))

 import qualified Data.List.NonEmpty as NE

 import qualified Data.Semigroup as S ( (<>) )

 import Data.Traversable (for)

     do { traceTc "uUnfilledVar2 not ok" $

              vcat [ text "tv1:" <+> ppr tv1

                   , text "ty2:" <+> ppr ty2

                   , text "simple-unify-chk:" <+> ppr (simpleUnifyCheck UC_OnTheFly given_eq_lvl tv1 ty2)

                   ]

                -- Occurs check or an untouchable: just defer

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 Question: given a homogeneous equality (alpha ~# ty), when is it OK to

 unify alpha := ty?

 (This note only applies to /homogeneous/ equalities, in which both

 sides have the same kind.)

     GHC.Tc.Solver.floatEqualities, around Nov 2020.  It's much easier

     to unify in-place, with no floating.

 Note [TyVar/TyVar orientation]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 See also Note [Fundeps with instances, and equality orientation]

 -- unification might still be OK, but it'll take more work to do

 -- (use the full 'checkTypeEq').

 --

 -- * Rejects if lhs_tv occurs in rhs_ty (occurs check)

 -- * Rejects foralls unless

 --      lhs_tv is RuntimeUnk (used by GHCi debugger)

   | otherwise

   = SUC_NotSure

   where

     lhs_tv_lvl         = tcTyVarLevel lhs_tv

     lhs_tv_is_concrete = isConcreteTyVar lhs_tv

                UC_OnTheFly   -> False

     rhs_is_ok (TyVarTy tv)

     rhs_is_ok (FunTy {ft_af = af, ft_mult = w, ft_arg = a, ft_res = r})

       | not forall_ok, isInvisibleFunArg af = False

       | otherwise = False

     rhs_is_ok (AppTy t1 t2)    = rhs_is_ok t1 && rhs_is_ok t2

     rhs_is_ok (LitTy {})       = True

 {- *********************************************************************

 *                                                                      *

         -- Occurs check (can promote)

         | OC_Check lhs_tv occ_prob <- occ

         , LC_Promote { lc_lvlp = lhs_tv_lvl } <- lc

               ; return $

                 if cterHasNoProblem reason

                 then pure co

 simpleOccursCheck OC_None _

   = TyVarCheck_Success

 simpleOccursCheck (OC_Check lhs_tv occ_prob) occ_tv

   where

 -------------------------

 tyVarLevelCheck :: LevelCheck m -> TcTyVar -> TyVarCheckResult m

 test('T23135', normal, compile, [''])

 test('LazyFieldAnnotations', normal, compile, [''])

 test('T27557', normal, compile, [''])