More explicit foralls (GHC Proposal 0007)

Allow the user to explicitly bind type/kind variables in type and data
family instances (including associated instances), closed type family
equations, and RULES pragmas. Follows the specification of GHC
Proposal 0007, also fixes #2600. Advised by Richard Eisenberg.

This modifies the Template Haskell AST -- old code may break!

Other Changes:
- convert HsRule to a record
- make rnHsSigWcType more general
- add repMaybe to DsMeta

Includes submodule update for Haddock.

Test Plan: validate

Reviewers: goldfire, bgamari, alanz

Subscribers: simonpj, RyanGlScott, goldfire, rwbarton,
             thomie, mpickering, carter

GHC Trac Issues: #2600, #14268

Differential Revision: https://phabricator.haskell.org/D4894

1 files changed, 80 insertions, 43 deletions

diff --git a/compiler/rename/RnSource.hs b/compiler/rename/RnSource.hs
index 9687e72a10..48739cdf69 100644
--- a/compiler/rename/RnSource.hs
+++ b/compiler/rename/RnSource.hs
@@ -50,7 +50,7 @@ import NameEnv
 import Avail
 import Outputable
 import Bag
-import BasicTypes       ( RuleName, pprRuleName )
+import BasicTypes       ( pprRuleName )
 import FastString
 import SrcLoc
 import DynFlags
@@ -67,6 +67,7 @@ import Control.Arrow ( first )
 import Data.List ( mapAccumL )
 import qualified Data.List.NonEmpty as NE
 import Data.List.NonEmpty ( NonEmpty(..) )
+import Data.Maybe ( isNothing, maybe, fromMaybe )
 import qualified Data.Set as Set ( difference, fromList, toList, null )
 
 {- | @rnSourceDecl@ "renames" declarations.
@@ -693,33 +694,41 @@ rnFamInstEqn :: HsDocContext
              -> RnM (FamInstEqn GhcRn rhs', FreeVars)
 rnFamInstEqn doc mb_cls rhs_kvars
     (HsIB { hsib_body = FamEqn { feqn_tycon  = tycon
+                               , feqn_bndrs  = mb_bndrs
                                , feqn_pats   = pats
                                , feqn_fixity = fixity
                                , feqn_rhs    = payload }}) rn_payload
   = do { tycon'   <- lookupFamInstName (fmap fst mb_cls) tycon
-       ; let loc = case pats of
-                     []             -> pprPanic "rnFamInstEqn" (ppr tycon)
-                     (L loc _ : []) -> loc
-                     (L loc _ : ps) -> combineSrcSpans loc (getLoc (last ps))
-
-             pat_kity_vars_with_dups = extractHsTysRdrTyVarsDups pats
-             pat_vars = freeKiTyVarsAllVars $
-                        rmDupsInRdrTyVars pat_kity_vars_with_dups
+       ; let pat_kity_vars_with_dups = extractHsTysRdrTyVarsDups pats
              -- Use the "...Dups" form because it's needed
              -- below to report unsed binder on the LHS
-       ; pat_var_names <- mapM (newTyVarNameRn mb_cls . L loc . unLoc) pat_vars
-
+       ; let pat_kity_vars = rmDupsInRdrTyVars pat_kity_vars_with_dups
+
+         -- all pat vars not explicitly bound (see extractHsTvBndrs)
+       ; let mb_imp_kity_vars = extractHsTvBndrs <$> mb_bndrs <*> pure pat_kity_vars
+             imp_vars = case mb_imp_kity_vars of
+                          -- kind vars are the only ones free if we have an explicit forall
+                          Just nbnd_kity_vars -> freeKiTyVarsKindVars nbnd_kity_vars
+                          -- all pattern vars are free otherwise
+                          Nothing             -> freeKiTyVarsAllVars pat_kity_vars
+       ; imp_var_names <- mapM (newTyVarNameRn mb_cls) imp_vars
+
+       ; let bndrs = fromMaybe [] mb_bndrs
+             bnd_vars = map hsLTyVarLocName bndrs
+             payload_kvars = filterOut (`elemRdr` (bnd_vars ++ imp_vars)) rhs_kvars
              -- Make sure to filter out the kind variables that were explicitly
              -- bound in the type patterns.
-       ; let payload_vars = filterOut (`elemRdr` pat_vars) rhs_kvars
-       ; payload_var_names <- mapM (newTyVarNameRn mb_cls) payload_vars
+       ; payload_kvar_names <- mapM (newTyVarNameRn mb_cls) payload_kvars
 
-       ; let all_var_names = pat_var_names ++ payload_var_names
+         -- all names not bound in an explict forall
+       ; let all_imp_var_names = imp_var_names ++ payload_kvar_names
 
              -- All the free vars of the family patterns
              -- with a sensible binding location
-       ; ((pats', payload'), fvs)
-              <- bindLocalNamesFV all_var_names $
+       ; ((bndrs', pats', payload'), fvs)
+              <- bindLocalNamesFV all_imp_var_names $
+                 bindLHsTyVarBndrs doc (Just $ inHsDocContext doc)
+                                   mb_cls bndrs $ \bndrs' ->
                  do { (pats', pat_fvs) <- rnLHsTypes (FamPatCtx tycon) pats
                     ; (payload', rhs_fvs) <- rn_payload doc payload
 
@@ -728,7 +737,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
                     ; let groups :: [NonEmpty (Located RdrName)]
                           groups = equivClasses cmpLocated $
                                    freeKiTyVarsAllVars pat_kity_vars_with_dups
-                    ; tv_nms_dups <- mapM (lookupOccRn . unLoc) $
+                    ; nms_dups <- mapM (lookupOccRn . unLoc) $
                                      [ tv | (tv :| (_:_)) <- groups ]
                           -- Add to the used variables
                           --  a) any variables that appear *more than once* on the LHS
@@ -736,27 +745,27 @@ rnFamInstEqn doc mb_cls rhs_kvars
                           --  b) for associated instances, the variables
                           --     of the instance decl.  See
                           --     Note [Unused type variables in family instances]
-                    ; let tv_nms_used = extendNameSetList rhs_fvs $
-                                        inst_tvs ++ tv_nms_dups
+                    ; let nms_used = extendNameSetList rhs_fvs $
+                                        inst_tvs ++ nms_dups
                           inst_tvs = case mb_cls of
                                        Nothing            -> []
                                        Just (_, inst_tvs) -> inst_tvs
-                    ; warnUnusedTypePatterns pat_var_names tv_nms_used
+                          all_nms = all_imp_var_names
+                                      ++ map hsLTyVarName bndrs'
+                    ; warnUnusedTypePatterns all_nms nms_used
 
                          -- See Note [Renaming associated types]
-                    ; let bad_tvs = case mb_cls of
-                                      Nothing           -> []
-                                      Just (_,cls_tkvs) -> filter is_bad cls_tkvs
-                          var_name_set = mkNameSet all_var_names
-
+                    ; let bad_tvs = maybe [] (filter is_bad . snd) mb_cls
+                          var_name_set = mkNameSet (map hsLTyVarName bndrs'
+                                                    ++ all_imp_var_names)
                           is_bad cls_tkv = cls_tkv `elemNameSet` rhs_fvs
-                                        && not (cls_tkv `elemNameSet` var_name_set)
+                                           && not (cls_tkv `elemNameSet` var_name_set)
                     ; unless (null bad_tvs) (badAssocRhs bad_tvs)
 
-                    ; return ((pats', payload'), rhs_fvs `plusFV` pat_fvs) }
+                    ; return ((bndrs', pats', payload'), rhs_fvs `plusFV` pat_fvs) }
 
        ; let anon_wcs = concatMap collectAnonWildCards pats'
-             all_ibs  = anon_wcs ++ all_var_names
+             all_ibs  = anon_wcs ++ all_imp_var_names
                         -- all_ibs: include anonymous wildcards in the implicit
                         -- binders In a type pattern they behave just like any
                         -- other type variable except for being anoymous.  See
@@ -768,6 +777,7 @@ rnFamInstEqn doc mb_cls rhs_kvars
                       , hsib_body
                           = FamEqn { feqn_ext    = noExt
                                    , feqn_tycon  = tycon'
+                                   , feqn_bndrs  = bndrs' <$ mb_bndrs
                                    , feqn_pats   = pats'
                                    , feqn_fixity = fixity
                                    , feqn_rhs    = payload' } },
@@ -796,6 +806,7 @@ rnTyFamDefltEqn :: Name
                 -> TyFamDefltEqn GhcPs
                 -> RnM (TyFamDefltEqn GhcRn, FreeVars)
 rnTyFamDefltEqn cls (FamEqn { feqn_tycon  = tycon
+                            , feqn_bndrs  = bndrs
                             , feqn_pats   = tyvars
                             , feqn_fixity = fixity
                             , feqn_rhs    = rhs })
@@ -805,6 +816,8 @@ rnTyFamDefltEqn cls (FamEqn { feqn_tycon  = tycon
        ; (rhs', fvs) <- rnLHsType ctx rhs
        ; return (FamEqn { feqn_ext    = noExt
                         , feqn_tycon  = tycon'
+                        , feqn_bndrs  = ASSERT( isNothing bndrs )
+                                        Nothing
                         , feqn_pats   = tyvars'
                         , feqn_fixity = fixity
                         , feqn_rhs    = rhs' }, fvs) } }
@@ -959,7 +972,7 @@ rnSrcDerivDecl (DerivDecl _ ty mds overlap)
        ; (mds', ty', fvs)
            <- rnLDerivStrategy DerivDeclCtx mds $ \strat_tvs ppr_via_ty ->
               rnAndReportFloatingViaTvs strat_tvs loc ppr_via_ty "instance" $
-              rnHsSigWcType DerivDeclCtx ty
+              rnHsSigWcType BindUnlessForall DerivDeclCtx ty
        ; return (DerivDecl noExt ty' mds' overlap, fvs) }
   where
     loc = getLoc $ hsib_body $ hswc_body ty
@@ -979,51 +992,75 @@ standaloneDerivErr
 -}
 
 rnHsRuleDecls :: RuleDecls GhcPs -> RnM (RuleDecls GhcRn, FreeVars)
-rnHsRuleDecls (HsRules _ src rules)
+rnHsRuleDecls (HsRules { rds_src = src
+                       , rds_rules = rules })
   = do { (rn_rules,fvs) <- rnList rnHsRuleDecl rules
-       ; return (HsRules noExt src rn_rules,fvs) }
+       ; return (HsRules { rds_ext = noExt
+                         , rds_src = src
+                         , rds_rules = rn_rules }, fvs) }
 rnHsRuleDecls (XRuleDecls _) = panic "rnHsRuleDecls"
 
 rnHsRuleDecl :: RuleDecl GhcPs -> RnM (RuleDecl GhcRn, FreeVars)
-rnHsRuleDecl (HsRule _ rule_name act vars lhs rhs)
-  = do { let rdr_names_w_loc = map get_var vars
+rnHsRuleDecl (HsRule { rd_name = rule_name
+                     , rd_act  = act
+                     , rd_tyvs = tyvs
+                     , rd_tmvs = tmvs
+                     , rd_lhs  = lhs
+                     , rd_rhs  = rhs })
+  = do { let rdr_names_w_loc = map get_var tmvs
        ; checkDupRdrNames rdr_names_w_loc
        ; checkShadowedRdrNames rdr_names_w_loc
        ; names <- newLocalBndrsRn rdr_names_w_loc
-       ; bindHsRuleVars (snd $ unLoc rule_name) vars names $ \ vars' ->
+       ; let doc = RuleCtx (snd $ unLoc rule_name)
+       ; bindRuleTyVars doc in_rule tyvs $ \ tyvs' ->
+         bindRuleTmVars doc tyvs' tmvs names $ \ tmvs' ->
     do { (lhs', fv_lhs') <- rnLExpr lhs
        ; (rhs', fv_rhs') <- rnLExpr rhs
        ; checkValidRule (snd $ unLoc rule_name) names lhs' fv_lhs'
-       ; return (HsRule (HsRuleRn fv_lhs' fv_rhs') rule_name act vars'
-                                                                     lhs' rhs',
-                 fv_lhs' `plusFV` fv_rhs') } }
+       ; return (HsRule { rd_ext  = HsRuleRn fv_lhs' fv_rhs'
+                        , rd_name = rule_name
+                        , rd_act  = act
+                        , rd_tyvs = tyvs'
+                        , rd_tmvs = tmvs'
+                        , rd_lhs  = lhs'
+                        , rd_rhs  = rhs' }, fv_lhs' `plusFV` fv_rhs') } }
   where
     get_var (L _ (RuleBndrSig _ v _)) = v
     get_var (L _ (RuleBndr _ v)) = v
     get_var (L _ (XRuleBndr _)) = panic "rnHsRuleDecl"
+    in_rule = text "in the rule" <+> pprFullRuleName rule_name
 rnHsRuleDecl (XRuleDecl _) = panic "rnHsRuleDecl"
 
-bindHsRuleVars :: RuleName -> [LRuleBndr GhcPs] -> [Name]
+bindRuleTmVars :: HsDocContext -> Maybe ty_bndrs
+               -> [LRuleBndr GhcPs] -> [Name]
                -> ([LRuleBndr GhcRn] -> RnM (a, FreeVars))
                -> RnM (a, FreeVars)
-bindHsRuleVars rule_name vars names thing_inside
+bindRuleTmVars doc tyvs vars names thing_inside
   = go vars names $ \ vars' ->
     bindLocalNamesFV names (thing_inside vars')
   where
-    doc = RuleCtx rule_name
-
     go (L l (RuleBndr _ (L loc _)) : vars) (n : ns) thing_inside
       = go vars ns $ \ vars' ->
         thing_inside (L l (RuleBndr noExt (L loc n)) : vars')
 
     go (L l (RuleBndrSig _ (L loc _) bsig) : vars) (n : ns) thing_inside
-      = rnHsSigWcTypeScoped doc bsig $ \ bsig' ->
+      = rnHsSigWcTypeScoped bind_free_tvs doc bsig $ \ bsig' ->
         go vars ns $ \ vars' ->
         thing_inside (L l (RuleBndrSig noExt (L loc n) bsig') : vars')
 
     go [] [] thing_inside = thing_inside []
     go vars names _ = pprPanic "bindRuleVars" (ppr vars $$ ppr names)
 
+    bind_free_tvs = case tyvs of Nothing -> AlwaysBind
+                                 Just _  -> NeverBind
+
+bindRuleTyVars :: HsDocContext -> SDoc -> Maybe [LHsTyVarBndr GhcPs]
+               -> (Maybe [LHsTyVarBndr GhcRn]  -> RnM (b, FreeVars))
+               -> RnM (b, FreeVars)
+bindRuleTyVars doc in_doc (Just bndrs) thing_inside
+  = bindLHsTyVarBndrs doc (Just in_doc) Nothing bndrs (thing_inside . Just)
+bindRuleTyVars _ _ _ thing_inside = thing_inside Nothing
+
 {-
 Note [Rule LHS validity checking]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1062,7 +1099,7 @@ validRuleLhs foralls lhs
     check (OpApp _ e1 op e2)              = checkl op `mplus` checkl_e e1
                                                       `mplus` checkl_e e2
     check (HsApp _ e1 e2)                 = checkl e1 `mplus` checkl_e e2
-    check (HsAppType _ e)                 = checkl e
+    check (HsAppType _ e _)               = checkl e
     check (HsVar _ (L _ v)) | v `notElem` foralls = Nothing
     check other                           = Just other  -- Failure