Comments and tiny refactorwip/T16728

* Added Note [Quantified varaibles in partial type signatures]
  in TcRnTypes

* Kill dVarSetElemsWellScoped; it was only called in
  one function, quantifyTyVars.  I inlined it because it
  was only scopedSort . dVarSetElems

* Kill Type.tyCoVarsOfBindersWellScoped, never called.

3 files changed, 33 insertions, 24 deletions

diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index fdb956aedd..99f4475cb6 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -1432,9 +1432,9 @@ quantifyTyVars gbl_tvs
               -- NB: All variables in the kind of a covar must not be
               -- quantified over, as we don't quantify over the covar.
 
-             dep_kvs = dVarSetElemsWellScoped $
+             dep_kvs = scopedSort $ dVarSetElems $
                        dep_tkvs `dVarSetMinusVarSet` mono_tvs
-                       -- dVarSetElemsWellScoped: put the kind variables into
+                       -- scopedSort: put the kind variables into
                        --    well-scoped order.
                        --    E.g.  [k, (a::k)] not the other way roud
 
@@ -1452,7 +1452,7 @@ quantifyTyVars gbl_tvs
 
        -- This block uses level numbers to decide what to quantify
        -- and emits a warning if the two methods do not give the same answer
-       ; let dep_kvs2    = dVarSetElemsWellScoped $
+       ; let dep_kvs2    = scopedSort $ dVarSetElems $
                            filterDVarSet (quantifiableTv outer_tclvl) dep_tkvs
              nondep_tvs2 = filter (quantifiableTv outer_tclvl) $
                            dVarSetElems (nondep_tkvs `minusDVarSet` dep_tkvs)
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 3c6b8ca685..3bd26e9f76 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -1542,6 +1542,10 @@ data TcIdSigInst
                -- No need to keep track of whether they are truly lexically
                --   scoped because the renamer has named them uniquely
                -- See Note [Binding scoped type variables] in TcSigs
+               --
+               -- NB: The order of sig_inst_skols is irrelevant
+               --     for a CompleteSig, but for a PartialSig see
+               --     Note [Quantified varaibles in partial type signatures]
 
          , sig_inst_theta  :: TcThetaType
                -- Instantiated theta.  In the case of a
@@ -1553,9 +1557,9 @@ data TcIdSigInst
 
          -- Relevant for partial signature only
          , sig_inst_wcs   :: [(Name, TcTyVar)]
-               -- Like sig_inst_skols, but for wildcards.  The named
-               -- wildcards scope over the binding, and hence their
-               -- Names may appear in type signatures in the binding
+               -- Like sig_inst_skols, but for /named/ wildcards (_a etc).
+               -- The named wildcards scope over the binding, and hence
+               -- their Names may appear in type signatures in the binding
 
          , sig_inst_wcx   :: Maybe TcType
                -- Extra-constraints wildcard to fill in, if any
@@ -1572,6 +1576,26 @@ if the original function had a signature like
 But that's ok: tcMatchesFun (called by tcRhs) can deal with that
 It happens, too!  See Note [Polymorphic methods] in TcClassDcl.
 
+Note [Quantified varaibles in partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f :: forall a b. _ -> a -> _ -> b
+   f (x,y) p q = q
+
+Then we expect f's final type to be
+  f :: forall {x,y}. forall a b. (x,y) -> a -> b -> b
+
+Note that x,y are Inferred, and can't be use for visible type
+application (VTA).  But a,b are Specified, and remain Specified
+in the final type, so we can use VTA for them.  (Exception: if
+it turns out that a's kind mentions b we need to reorder them
+with scopedSort.)
+
+The sig_inst_skols of the TISI from a partial signature records
+that original order, and is used to get the variables of f's
+final type in the correct order.
+
+
 Note [Wildcards in partial signatures]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The wildcards in psig_wcs may stand for a type mentioning
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index ff4501985e..1189fa64a4 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -156,8 +156,8 @@ module Type (
         typeSize, occCheckExpand,
 
         -- * Well-scoped lists of variables
-        dVarSetElemsWellScoped, scopedSort, tyCoVarsOfTypeWellScoped,
-        tyCoVarsOfTypesWellScoped, tyCoVarsOfBindersWellScoped,
+        scopedSort, tyCoVarsOfTypeWellScoped,
+        tyCoVarsOfTypesWellScoped,
 
         -- * Type comparison
         eqType, eqTypeX, eqTypes, nonDetCmpType, nonDetCmpTypes, nonDetCmpTypeX,
@@ -248,7 +248,7 @@ import UniqSet
 import Class
 import TyCon
 import TysPrim
-import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind, unitTy
+import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind
                                  , typeSymbolKind, liftedTypeKind
                                  , constraintKind )
 import PrelNames
@@ -2171,15 +2171,6 @@ scopedSort = go [] []
        -- lists not in correspondence
     insert _ _ _ = panic "scopedSort"
 
--- | Extract a well-scoped list of variables from a deterministic set of
--- variables. The result is deterministic.
--- NB: There used to exist varSetElemsWellScoped :: VarSet -> [Var] which
--- took a non-deterministic set and produced a non-deterministic
--- well-scoped list. If you care about the list being well-scoped you also
--- most likely care about it being in deterministic order.
-dVarSetElemsWellScoped :: DVarSet -> [Var]
-dVarSetElemsWellScoped = scopedSort . dVarSetElems
-
 -- | Get the free vars of a type in scoped order
 tyCoVarsOfTypeWellScoped :: Type -> [TyVar]
 tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
@@ -2188,12 +2179,6 @@ tyCoVarsOfTypeWellScoped = scopedSort . tyCoVarsOfTypeList
 tyCoVarsOfTypesWellScoped :: [Type] -> [TyVar]
 tyCoVarsOfTypesWellScoped = scopedSort . tyCoVarsOfTypesList
 
--- | Given the suffix of a telescope, returns the prefix.
--- Ex: given [(k :: j), (a :: Proxy k)], returns [(j :: *)].
-tyCoVarsOfBindersWellScoped :: [TyVar] -> [TyVar]
-tyCoVarsOfBindersWellScoped tvs
-  = tyCoVarsOfTypeWellScoped (mkInvForAllTys tvs unitTy)
-
 ------------- Closing over kinds -----------------
 
 -- | Add the kind variables free in the kinds of the tyvars in the given set.