Refactor treatment of wildcards

This patch began as a modest refactoring of HsType and friends, to
clarify and tidy up exactly where quantification takes place in types.
Although initially driven by making the implementation of wildcards more
tidy (and fixing a number of bugs), I gradually got drawn into a pretty
big process, which I've been doing on and off for quite a long time.

There is one compiler performance regression as a result of all
this, in perf/compiler/T3064.  I still need to look into that.

* The principal driving change is described in Note [HsType binders]
  in HsType.  Well worth reading!

* Those data type changes drive almost everything else.  In particular
  we now statically know where

       (a) implicit quantification only (LHsSigType),
           e.g. in instance declaratios and SPECIALISE signatures

       (b) implicit quantification and wildcards (LHsSigWcType)
           can appear, e.g. in function type signatures

* As part of this change, HsForAllTy is (a) simplified (no wildcards)
  and (b) split into HsForAllTy and HsQualTy.  The two contructors
  appear when and only when the correponding user-level construct
  appears.  Again see Note [HsType binders].

  HsExplicitFlag disappears altogether.

* Other simplifications

     - ExprWithTySig no longer needs an ExprWithTySigOut variant

     - TypeSig no longer needs a PostRn name [name] field
       for wildcards

     - PatSynSig records a LHsSigType rather than the decomposed
       pieces

     - The mysterious 'GenericSig' is now 'ClassOpSig'

* Renamed LHsTyVarBndrs to LHsQTyVars

* There are some uninteresting knock-on changes in Haddock,
  because of the HsSyn changes

I also did a bunch of loosely-related changes:

* We already had type synonyms CoercionN/CoercionR for nominal and
  representational coercions.  I've added similar treatment for

      TcCoercionN/TcCoercionR

      mkWpCastN/mkWpCastN

  All just type synonyms but jolly useful.

* I record-ised ForeignImport and ForeignExport

* I improved the (poor) fix to Trac #10896, by making
  TcTyClsDecls.checkValidTyCl recover from errors, but adding a
  harmless, abstract TyCon to the envt if so.

* I did some significant refactoring in RnEnv.lookupSubBndrOcc,
  for reasons that I have (embarrassingly) now totally forgotten.
  It had to do with something to do with import and export

Updates haddock submodule.

1 files changed, 43 insertions, 24 deletions

diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index d1ba2d571c..b8e193b0bf 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -389,24 +389,24 @@ the let binding.
 
 simplifyInfer :: TcLevel               -- Used when generating the constraints
               -> Bool                  -- Apply monomorphism restriction
-              -> [TcTyVar]             -- The quantified tyvars of any signatures
-                                       --   see Note [Which type variables to quantify]
+              -> [TcIdSigInfo]         -- Any signatures (possibly partial)
               -> [(Name, TcTauType)]   -- Variables to be generalised,
                                        -- and their tau-types
               -> WantedConstraints
               -> TcM ([TcTyVar],    -- Quantify over these type variables
                       [EvVar],      -- ... and these constraints (fully zonked)
                       TcEvBinds)    -- ... binding these evidence variables
-simplifyInfer rhs_tclvl apply_mr sig_qtvs name_taus wanteds
+simplifyInfer rhs_tclvl apply_mr sigs name_taus wanteds
   | isEmptyWC wanteds
   = do { gbl_tvs <- tcGetGlobalTyVars
-       ; qtkvs <- quantifyTyVars gbl_tvs (tyVarsOfTypes (map snd name_taus))
+       ; qtkvs <- quantify_tvs sigs gbl_tvs (tyVarsOfTypes (map snd name_taus))
        ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
        ; return (qtkvs, [], emptyTcEvBinds) }
 
   | otherwise
   = do { traceTc "simplifyInfer {"  $ vcat
-             [ ptext (sLit "binds =") <+> ppr name_taus
+             [ ptext (sLit "sigs =") <+> ppr sigs
+             , ptext (sLit "binds =") <+> ppr name_taus
              , ptext (sLit "rhs_tclvl =") <+> ppr rhs_tclvl
              , ptext (sLit "apply_mr =") <+> ppr apply_mr
              , ptext (sLit "(unzonked) wanted =") <+> ppr wanteds
@@ -473,8 +473,8 @@ simplifyInfer rhs_tclvl apply_mr sig_qtvs name_taus wanteds
          -- Decide what type variables and constraints to quantify
        ; zonked_taus <- mapM (TcM.zonkTcType . snd) name_taus
        ; let zonked_tau_tvs = tyVarsOfTypes zonked_taus
-       ; (qtvs, bound_theta) <- decideQuantification apply_mr sig_qtvs name_taus
-                                                     quant_pred_candidates zonked_tau_tvs
+       ; (qtvs, bound_theta) <- decideQuantification apply_mr sigs name_taus
+                                        quant_pred_candidates zonked_tau_tvs
 
          -- Emit an implication constraint for the
          -- remaining constraints from the RHS
@@ -565,37 +565,38 @@ and the quantified constraints are empty/insoluble
 
 decideQuantification
     :: Bool                       -- Apply monomorphism restriction
-    -> [TcTyVar]
+    -> [TcIdSigInfo]
     -> [(Name, TcTauType)]        -- Variables to be generalised (just for error msg)
     -> [PredType] -> TcTyVarSet   -- Constraints and type variables from RHS
     -> TcM ( [TcTyVar]            -- Quantify over these tyvars (skolems)
            , [PredType])          -- and this context (fully zonked)
 -- See Note [Deciding quantification]
-decideQuantification apply_mr sig_qtvs name_taus constraints zonked_tau_tvs
+decideQuantification apply_mr sigs name_taus constraints zonked_tau_tvs
   | apply_mr     -- Apply the Monomorphism restriction
   = do { gbl_tvs <- tcGetGlobalTyVars
        ; let constrained_tvs = tyVarsOfTypes constraints
              mono_tvs = gbl_tvs `unionVarSet` constrained_tvs
-             mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs
-       ; qtvs <- quantify_tvs mono_tvs zonked_tau_tvs
-       ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
-                                                , ppr qtvs, ppr mr_bites])
+       ; qtvs <- quantify_tvs sigs mono_tvs zonked_tau_tvs
 
        -- Warn about the monomorphism restriction
        ; warn_mono <- woptM Opt_WarnMonomorphism
+       ; let mr_bites = constrained_tvs `intersectsVarSet` zonked_tau_tvs
        ; warnTc (warn_mono && mr_bites) $
          hang (ptext (sLit "The Monomorphism Restriction applies to the binding")
                <> plural bndrs <+> ptext (sLit "for") <+> pp_bndrs)
              2 (ptext (sLit "Consider giving a type signature for")
                 <+> if isSingleton bndrs then pp_bndrs else ptext (sLit "these binders"))
 
+       -- All done
+       ; traceTc "decideQuantification 1" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
+                                                , ppr qtvs, ppr mr_bites])
        ; return (qtvs, []) }
 
   | otherwise
   = do { gbl_tvs <- tcGetGlobalTyVars
-       ; let mono_tvs     = growThetaTyVars (filter isEqPred constraints) gbl_tvs
+       ; let mono_tvs     = growThetaTyVars equality_constraints gbl_tvs
              tau_tvs_plus = growThetaTyVars constraints zonked_tau_tvs
-       ; qtvs        <- quantify_tvs mono_tvs tau_tvs_plus
+       ; qtvs        <- quantify_tvs sigs mono_tvs tau_tvs_plus
        ; constraints <- zonkTcThetaType constraints
               -- quantifyTyVars turned some meta tyvars into
               -- quantified skolems, so we have to zonk again
@@ -606,14 +607,21 @@ decideQuantification apply_mr sig_qtvs name_taus constraints zonked_tau_tvs
        ; traceTc "decideQuantification 2" (vcat [ppr constraints, ppr gbl_tvs, ppr mono_tvs
                                                 , ppr tau_tvs_plus, ppr qtvs, ppr min_theta])
        ; return (qtvs, min_theta) }
-
   where
     bndrs    = map fst name_taus
     pp_bndrs = pprWithCommas (quotes . ppr) bndrs
-    quantify_tvs mono_tvs tau_tvs   -- See Note [Which type variable to quantify]
-      | null sig_qtvs = quantifyTyVars mono_tvs tau_tvs
-      | otherwise     = quantifyTyVars (mono_tvs `delVarSetList`    sig_qtvs)
-                                       (tau_tvs  `extendVarSetList` sig_qtvs)
+    equality_constraints = filter isEqPred constraints
+
+quantify_tvs :: [TcIdSigInfo] -> TcTyVarSet -> TcTyVarSet -> TcM [TcTyVar]
+-- See Note [Which type variable to quantify]
+quantify_tvs sigs mono_tvs tau_tvs
+  = quantifyTyVars (mono_tvs `delVarSetList`    sig_qtvs)
+                   (tau_tvs  `extendVarSetList` sig_qtvs `extendVarSetList` sig_wcs)
+                   -- NB: quantifyTyVars zonks its arguments
+  where
+    sig_qtvs = [ skol | sig <- sigs, (_, skol) <- sig_skols sig ]
+    sig_wcs  = [ wc   | TISI { sig_bndr = PartialSig { sig_wcs = wcs } } <- sigs
+                      , (_, wc) <- wcs ]
 
 ------------------
 pickQuantifiablePreds :: TyVarSet         -- Quantifying over these
@@ -681,21 +689,32 @@ quantify over all type variables that are
 
 However, for a pattern binding, or with wildcards, we might
 be doing inference *in the presence of a type signature*.
-Mostly, if there is a signature, we use CheckGen, not InferGen,
-but with pattern bindings or wildcards we might do inference
+Mostly, if there is a signature we use CheckGen, not InferGen,
+but with pattern bindings or wildcards we might do InferGen
 and still have a type signature.  For example:
    f :: _ -> a
    f x = ...
 or
+   g :: (Eq _a) => _b -> _b
+or
    p :: a -> a
    (p,q) = e
-In both cases we use plan InferGen, and hence call simplifyInfer.
+In all these cases we use plan InferGen, and hence call simplifyInfer.
 But those 'a' variables are skolems, and we should be sure to quantify
 over them, regardless of the monomorphism restriction etc.  If we
 don't, when reporting a type error we panic when we find that a
 skolem isn't bound by any enclosing implication.
 
-That's why we pass sig_qtvs to simplifyInfer, and make sure (in
+Moreover we must quantify over all wildcards that are not free in
+the environment.  In the case of 'g' for example, silly though it is,
+we want to get the inferred type
+   g :: forall t. Eq t => Int -> Int
+and then report ambiguity, rather than *not* quantifying over 't'
+and getting some much more mysterious error later.  A similar case
+is
+  h :: F _a -> Int
+
+That's why we pass sigs to simplifyInfer, and make sure (in
 quantify_tvs) that we do quantify over them.  Trac #10615 is
 a case in point.