Fix a QuickLook bug

This MR fixes the bug exposed by #24676.  The problem was that
quickLookArg was trying to avoid calling tcInstFun unnecessarily; but
it was in fact necessary.  But that in turn forced me into a
significant refactoring, putting more fields into EValArgQL.

Highlights: see Note [Quick Look overview] in GHC.Tc.Gen.App

* Instantiation variables are now distinguishable from ordinary
  unification variables, by level number = QLInstVar. This is
  treated like "level infinity".  See Note [The QLInstVar TcLevel]
  in GHC.Tc.Utils.TcType.

* In `tcApp`, we don't track the instantiation variables in a set Delta
  any more; instead, we just tell them apart by their level number.

* EValArgQL now much more clearly captures the "half-done" state
  of typechecking an argument, ready for later resumption.
  See Note [Quick Look at value arguments] in GHC.Tc.Gen.App

* Elminated a bogus (never used) fast-path in
  GHC.Tc.Utils.Instantiate.instCallConstraints
  See Note [Possible fast path for equality constraints]

Many other small refactorings.

compiler/GHC/Core.hs

@@ -694,7 +694,7 @@ an eta-expansion (see GHC.CoreToStg.Prep.maybeSaturate):
 However, this transformation would be invalid, because now the binding of x
 in the lambda abstraction would violate I1.
 
-See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Gen.Head
+See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete
 and Note [Linting representation-polymorphic builtins] in GHC.Core.Lint for
 more details.
 

compiler/GHC/Core/DataCon.hs

@@ -456,7 +456,7 @@ data DataCon
         -- variables of unboxed tuples and unboxed sums.
         --
         -- See Note [Representation-polymorphism checking built-ins]
-        -- in GHC.Tc.Gen.Head.
+        -- in GHC.Tc.Utils.Concrete.
         dcConcreteTyVars :: ConcreteTyVars,
 
         -- The type/coercion vars in the order the user wrote them [c,y,x,b]
@@ -1309,7 +1309,7 @@ dataConUnivAndExTyCoVars (MkData { dcUnivTyVars = univ_tvs, dcExTyCoVars = ex_tv
 -- For example: the RuntimeRep variables of unboxed tuples and unboxed sums.
 --
 -- See Note [Representation-polymorphism checking built-ins]
--- in GHC.Tc.Gen.Head.
+-- in GHC.Tc.Utils.Concrete
 dataConConcreteTyVars :: DataCon -> ConcreteTyVars
 dataConConcreteTyVars (MkData { dcConcreteTyVars = concs }) = concs
 

compiler/GHC/Core/Lint.hs

@@ -1300,7 +1300,7 @@ checkRepPolyBuiltinApp fun_id args = checkL (null not_concs) err_msg
 -- | Compute the 1-indexed positions in the outer forall'd quantified type variables
 -- of the type in which the concrete type variables occur.
 --
--- See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Gen.Head.
+-- See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete.
 concreteTyVarPositions :: Id -> ConcreteTyVars -> IntMap ConcreteTvOrigin
 concreteTyVarPositions fun_id conc_tvs
   | isNullUFM conc_tvs

compiler/GHC/Core/Rules.hs

@@ -1239,7 +1239,7 @@ Two wrinkles:
           [f :-> \x p. p*p]
      but that is fine.
 
-(W2) This wrinkle concerns the overlp between the new HOP rule and the existing
+(W2) This wrinkle concerns the overlap between the new HOP rule and the existing
      decompose-application rule.  See 3.1 of GHC Proposal #555 for a discussion.
 
      Consider potential match:

compiler/GHC/Core/TyCo/FVs.hs

@@ -59,7 +59,7 @@ import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind )
 
 import GHC.Builtin.Types.Prim( funTyFlagTyCon )
 
-import Data.Monoid as DM ( Endo(..), Any(..) )
+import Data.Monoid as DM ( Any(..) )
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCon
 import GHC.Core.Coercion.Axiom( coAxiomTyCon )
@@ -75,6 +75,8 @@ import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Data.Pair
 
+import Data.Semigroup
+
 {-
 %************************************************************************
 %*                                                                      *
@@ -228,6 +230,17 @@ then we won't look at it at all. If it is free, then all the variables free in i
 kind are free -- regardless of whether some local variable has the same Unique.
 So if we're looking at a variable occurrence at all, then all variables in its
 kind are free.
+
+Note [Free vars and synonyms]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When finding free variables we generally do not expand synonyms.  So given
+   type T a = Int
+the type (T [b]) will return `b` as a free variable, even though expanding the
+synonym would get rid of it.  Expanding synonyms might lead to types that look
+ill-scoped; an alternative we have not explored.
+
+But see `occCheckExpand` in this module for a function that does, selectively,
+expand synonyms to reduce free-var occurences.
 -}
 
 {- *********************************************************************
@@ -317,7 +330,7 @@ deep_cos :: [Coercion] -> Endo TyCoVarSet
 (deep_ty, deep_tys, deep_co, deep_cos) = foldTyCo deepTcvFolder emptyVarSet
 
 deepTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
-deepTcvFolder = TyCoFolder { tcf_view = noView
+deepTcvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
                            , tcf_tyvar = do_tcv, tcf_covar = do_tcv
                            , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
   where
@@ -375,7 +388,7 @@ shallow_cos :: [Coercion] -> Endo TyCoVarSet
 (shallow_ty, shallow_tys, shallow_co, shallow_cos) = foldTyCo shallowTcvFolder emptyVarSet
 
 shallowTcvFolder :: TyCoFolder TyCoVarSet (Endo TyCoVarSet)
-shallowTcvFolder = TyCoFolder { tcf_view = noView
+shallowTcvFolder = TyCoFolder { tcf_view = noView  -- See Note [Free vars and synonyms]
                               , tcf_tyvar = do_tcv, tcf_covar = do_tcv
                               , tcf_hole  = do_hole, tcf_tycobinder = do_bndr }
   where
@@ -592,6 +605,7 @@ tyCoFVsOfType (TyVarTy v)        f bound_vars (acc_list, acc_set)
                                emptyVarSet   -- See Note [Closing over free variable kinds]
                                (v:acc_list, extendVarSet acc_set v)
 tyCoFVsOfType (TyConApp _ tys)   f bound_vars acc = tyCoFVsOfTypes tys f bound_vars acc
+                                                    -- See Note [Free vars and synonyms]
 tyCoFVsOfType (LitTy {})         f bound_vars acc = emptyFV f bound_vars acc
 tyCoFVsOfType (AppTy fun arg)    f bound_vars acc = (tyCoFVsOfType fun `unionFV` tyCoFVsOfType arg) f bound_vars acc
 tyCoFVsOfType (FunTy _ w arg res)  f bound_vars acc = (tyCoFVsOfType w `unionFV` tyCoFVsOfType arg `unionFV` tyCoFVsOfType res) f bound_vars acc
@@ -950,7 +964,9 @@ invisibleVarsOfTypes = mapUnionFV invisibleVarsOfType
 
 {-# INLINE afvFolder #-}   -- so that specialization to (const True) works
 afvFolder :: (TyCoVar -> Bool) -> TyCoFolder TyCoVarSet DM.Any
-afvFolder check_fv = TyCoFolder { tcf_view = noView
+-- 'afvFolder' is short for "any-free-var folder", good for checking
+-- if any free var of a type satisfies a predicate `check_fv`
+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 = do_bndr }
   where

compiler/GHC/Driver/Config/Core/Lint.hs

@@ -132,7 +132,7 @@ perPassFlags dflags pass
     -- we have eta-expanded data constructors with representation-polymorphic
     -- bindings; so we switch off the representation-polymorphism checks.
     -- The very simple optimiser will beta-reduce them away.
-    -- See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Gen.Head.
+    -- See Note [Representation-polymorphism checking built-ins] in GHC.Tc.Utils.Concrete
     check_fixed_rep = case pass of
                         CoreDesugar -> False
                         _           -> True