qlUnify ::  TcType -> TcType -> TcM ()

 -- Unify ty1 with ty2:

 --   * It does not return a coercion (unlike unifyType); it is called

 --     for the sole purpose of unifying instantiation variables, although it

 --     may also (opportunistically) unify regular unification variables.

 That is the entire point of qlUnify!   Wrinkles:

 (UQL1) Before unifying an instantiation variable in `go_flexi`, we must check

     * An occurs-check

     * An attempt to unify a concrete type variable with a non-concrete type.

 (UQL2) What if kappa and ty have different kinds?  We simply call the

   ordinary unifier and use the coercion to connect the two.

   The simplest thing is to say that `qlUnify` unifies /only/ instantiation variables

   (see calls to `isQLInstTyVar`).  We could be more ambitious, perhaps, in future.

 (UQL7) If `qlUnify` sees a concrete `kaapa`, thus

             kappa[conc] ~ some-type

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

 -- * Rejects foralls unless

 --      lhs_tv is RuntimeUnk (used by GHCi debugger)

 -- * Rejects a non-concrete type if lhs_tv is concrete

 -- * Rejects type families unless fam_ok=True

 -- * Does a level-check for type variables, to avoid skolem escape

        | isCoVar tcv                                      = occ_check

        | tcTyVarLevel tcv `strictlyDeeperThan` lhs_tv_lvl = True

        | lhs_tv_is_concrete, not (isConcreteTyVar tcv)    = True

        | occ_check                                        = True

        | otherwise                                        = False

        where

     rhs_is_bad (TyVarTy tv) = rhs_tcv_is_bad tv

     rhs_is_bad (CoercionTy co)  = co_is_bad co

     rhs_is_bad (LitTy {})       = False

     co_is_bad co = anyFreeVarsOfCo rhs_tcv_is_bad co

 {- Note [simpleUnifyCheck]

 (SUC_NotSure).  In the latter case we will later use `checkTyEqRhs` to resolve.

 In particular, `simpleUnifyCheck`:

 * Rejects foralls unless

       lhs_tv is RuntimeUnk (used by GHCi debugger)

 * Rejects a non-concrete type if lhs_tv is concrete

 * Rejects type families unless fam_ok=True

 * Does a level-check for type variables, to avoid skolem escape

 This function is pretty heavily used, so it's optimised not to allocate.

 -}

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

         , LC_Promote { lc_lvlp = lhs_tv_lvl } <- lc

         -> do { reason <- checkPromoteFreeVars occ_prob lhs_tv lhs_tv_lvl $

                           tyCoVarsOfCo co

               ; return $

                 if cterHasNoProblem reason

                 then pure co

                   -- so the only reason for a filled meta-tyvar is promotion

                 else do_rhs_checks

                      , tyVarLevelCheck        lc   occ_tv

                      , tyVarConcretenessCheck conc occ_tv ]

               }

 promotionDone _      _               _ = return False

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

 -- ^ The "interpreter" for 'OccursCheck'

   = TyVarCheck_Success

   where

     is_bad :: TyCoVar -> Bool

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

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

 -- but was erroneously accpeted with ImpredicativeTypes

 -- See !16566

 import Data.Kind

 import Data.Proxy