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

2 files changed, 167 insertions, 63 deletions

diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y
index 9f43e36984..8a10516819 100644
--- a/compiler/parser/Parser.y
+++ b/compiler/parser/Parser.y
@@ -1,3 +1,4 @@
+
 --                                                              -*-haskell-*-
 -- ---------------------------------------------------------------------------
 -- (c) The University of Glasgow 1997-2003
@@ -81,13 +82,13 @@ import TysWiredIn       ( unitTyCon, unitDataCon, tupleTyCon, tupleDataCon, nilD
                           listTyCon_RDR, consDataCon_RDR, eqTyCon_RDR )
 
 -- compiler/utils
-import Util             ( looksLikePackageName )
+import Util             ( looksLikePackageName, fstOf3, sndOf3, thdOf3 )
 import GhcPrelude
 
 import qualified GHC.LanguageExtensions as LangExt
 }
 
-%expect 235 -- shift/reduce conflicts
+%expect 236 -- shift/reduce conflicts
 
 {- Last updated: 04 June 2018
 
@@ -120,16 +121,7 @@ follows. Shift parses as if the 'module' keyword follows.
 
 -------------------------------------------------------------------------------
 
-state 57 contains 2 shift/reduce conflicts.
-
-    *** strict_mark -> unpackedness .
-        strict_mark -> unpackedness . strictness
-
-    Conflicts: '~' '!'
-
--------------------------------------------------------------------------------
-
-state 61 contains 1 shift/reduce conflict.
+state 60 contains 1 shift/reduce conflict.
 
         context -> btype .
     *** type -> btype .
@@ -139,7 +131,7 @@ state 61 contains 1 shift/reduce conflict.
 
 -------------------------------------------------------------------------------
 
-state 62 contains 46 shift/reduce conflicts.
+state 61 contains 46 shift/reduce conflicts.
 
     *** btype -> tyapps .
         tyapps -> tyapps . tyapp
@@ -157,7 +149,7 @@ Shift parses as (per longest-parse rule):
 
 -------------------------------------------------------------------------------
 
-state 144 contains 15 shift/reduce conflicts.
+state 143 contains 15 shift/reduce conflicts.
 
         exp -> infixexp . '::' sigtype
         exp -> infixexp . '-<' exp
@@ -182,7 +174,7 @@ Shift parses as (per longest-parse rule):
 
 -------------------------------------------------------------------------------
 
-state 149 contains 67 shift/reduce conflicts.
+state 148 contains 67 shift/reduce conflicts.
 
     *** exp10 -> fexp .
         fexp -> fexp . aexp
@@ -200,7 +192,7 @@ Shift parses as (per longest-parse rule):
 
 -------------------------------------------------------------------------------
 
-state 204 contains 27 shift/reduce conflicts.
+state 203 contains 27 shift/reduce conflicts.
 
         aexp2 -> TH_TY_QUOTE . tyvar
         aexp2 -> TH_TY_QUOTE . gtycon
@@ -219,7 +211,7 @@ Shift parses as (per longest-parse rule):
 
 -------------------------------------------------------------------------------
 
-state 300 contains 1 shift/reduce conflicts.
+state 299 contains 1 shift/reduce conflicts.
 
         rule -> STRING . rule_activation rule_forall infixexp '=' exp
 
@@ -237,7 +229,7 @@ a rule instructing how to rewrite the expression '[0] f'.
 
 -------------------------------------------------------------------------------
 
-state 310 contains 1 shift/reduce conflict.
+state 309 contains 1 shift/reduce conflict.
 
     *** type -> btype .
         type -> btype . '->' ctype
@@ -248,7 +240,7 @@ Same as state 61 but without contexts.
 
 -------------------------------------------------------------------------------
 
-state 354 contains 1 shift/reduce conflicts.
+state 353 contains 1 shift/reduce conflicts.
 
         tup_exprs -> commas . tup_tail
         sysdcon_nolist -> '(' commas . ')'
@@ -263,7 +255,7 @@ if -XTupleSections is not specified.
 
 -------------------------------------------------------------------------------
 
-state 409 contains 1 shift/reduce conflicts.
+state 408 contains 1 shift/reduce conflicts.
 
         tup_exprs -> commas . tup_tail
         sysdcon_nolist -> '(#' commas . '#)'
@@ -275,7 +267,7 @@ Same as State 354 for unboxed tuples.
 
 -------------------------------------------------------------------------------
 
-state 417 contains 67 shift/reduce conflicts.
+state 416 contains 67 shift/reduce conflicts.
 
     *** exp10 -> '-' fexp .
         fexp -> fexp . aexp
@@ -299,7 +291,7 @@ parenthesized infix type expression of length 1.
 
 -------------------------------------------------------------------------------
 
-state 675 contains 1 shift/reduce conflicts.
+state 678 contains 1 shift/reduce conflicts.
 
     *** aexp2 -> ipvar .
         dbind -> ipvar . '=' exp
@@ -314,7 +306,7 @@ sensible meaning, namely the lhs of an implicit binding.
 
 -------------------------------------------------------------------------------
 
-state 752 contains 1 shift/reduce conflicts.
+state 756 contains 1 shift/reduce conflicts.
 
         rule -> STRING rule_activation . rule_forall infixexp '=' exp
 
@@ -331,7 +323,7 @@ doesn't include 'forall'.
 
 -------------------------------------------------------------------------------
 
-state 986 contains 1 shift/reduce conflicts.
+state 992 contains 1 shift/reduce conflicts.
 
         transformqual -> 'then' 'group' . 'using' exp
         transformqual -> 'then' 'group' . 'by' exp 'using' exp
@@ -341,7 +333,29 @@ state 986 contains 1 shift/reduce conflicts.
 
 -------------------------------------------------------------------------------
 
-state 1367 contains 1 shift/reduce conflict.
+state 1089 contains 1 shift/reduce conflicts.
+
+        rule_foralls -> 'forall' rule_vars '.' . 'forall' rule_vars '.'
+    *** rule_foralls -> 'forall' rule_vars '.' .
+
+    Conflict: 'forall'
+
+Example ambigutiy: '{-# RULES "name" forall a. forall ... #-}'
+
+Here the parser cannot tell whether the second 'forall' is the beginning of
+a term-level quantifier, for example:
+
+'{-# RULES "name" forall a. forall x. id @a x = x #-}'
+
+or a valid variable named 'forall', for example a function @:: Int -> Int@
+
+'{-# RULES "name" forall a. forall 0 = 0 #-}'
+
+Shift means the parser only allows the former. Also see conflict 753 above.
+
+-------------------------------------------------------------------------------
+
+state 1390 contains 1 shift/reduce conflict.
 
     *** atype -> tyvar .
         tv_bndr -> '(' tyvar . '::' kind ')'
@@ -1125,7 +1139,7 @@ inst_decl :: { LInstDecl GhcPs }
                     (mj AnnType $1:mj AnnInstance $2:(fst $ unLoc $3)) }
 
           -- data/newtype instance declaration
-        | data_or_newtype 'instance' capi_ctype tycl_hdr constrs
+        | data_or_newtype 'instance' capi_ctype tycl_hdr_inst constrs
                           maybe_derivings
             {% amms (mkDataFamInst (comb4 $1 $4 $5 $6) (snd $ unLoc $1) $3 $4
                                       Nothing (reverse (snd  $ unLoc $5))
@@ -1133,7 +1147,7 @@ inst_decl :: { LInstDecl GhcPs }
                     ((fst $ unLoc $1):mj AnnInstance $2:(fst $ unLoc $5)) }
 
           -- GADT instance declaration
-        | data_or_newtype 'instance' capi_ctype tycl_hdr opt_kind_sig
+        | data_or_newtype 'instance' capi_ctype tycl_hdr_inst opt_kind_sig
                  gadt_constrlist
                  maybe_derivings
             {% amms (mkDataFamInst (comb4 $1 $4 $6 $7) (snd $ unLoc $1) $3 $4
@@ -1223,11 +1237,16 @@ ty_fam_inst_eqns :: { Located [LTyFamInstEqn GhcPs] }
         | {- empty -}                 { noLoc [] }
 
 ty_fam_inst_eqn :: { Located ([AddAnn],TyFamInstEqn GhcPs) }
-        : type '=' ktype
-                -- Note the use of type for the head; this allows
-                -- infix type constructors and type patterns
-              {% do { (eqn,ann) <- mkTyFamInstEqn $1 $3
+        : 'forall' tv_bndrs '.' type '=' ktype
+              {% do { hintExplicitForall (getLoc $1)
+                    ; (eqn,ann) <- mkTyFamInstEqn (Just $2) $4 $6
+                    ; ams (sLL $4 $> (mj AnnEqual $5:ann, eqn))
+                          [mu AnnForall $1, mj AnnDot $3]  } }
+        | type '=' ktype
+              {% do { (eqn,ann) <- mkTyFamInstEqn Nothing $1 $3
                     ; return (sLL $1 $> (mj AnnEqual $2:ann, eqn))  } }
+              -- Note the use of type for the head; this allows
+              -- infix type constructors and type patterns
 
 -- Associated type family declarations
 --
@@ -1291,13 +1310,13 @@ at_decl_inst :: { LInstDecl GhcPs }
 
         -- data/newtype instance declaration, with optional 'instance' keyword
         -- (can't use opt_instance because you get reduce/reduce errors)
-        | data_or_newtype capi_ctype tycl_hdr constrs maybe_derivings
+        | data_or_newtype capi_ctype tycl_hdr_inst constrs maybe_derivings
                {% amms (mkDataFamInst (comb4 $1 $3 $4 $5) (snd $ unLoc $1) $2 $3
                                     Nothing (reverse (snd $ unLoc $4))
                                             (fmap reverse $5))
                        ((fst $ unLoc $1):(fst $ unLoc $4)) }
 
-        | data_or_newtype 'instance' capi_ctype tycl_hdr constrs maybe_derivings
+        | data_or_newtype 'instance' capi_ctype tycl_hdr_inst constrs maybe_derivings
                {% amms (mkDataFamInst (comb4 $1 $4 $5 $6) (snd $ unLoc $1) $3 $4
                                     Nothing (reverse (snd $ unLoc $5))
                                             (fmap reverse $6))
@@ -1305,7 +1324,7 @@ at_decl_inst :: { LInstDecl GhcPs }
 
         -- GADT instance declaration, with optional 'instance' keyword
         -- (can't use opt_instance because you get reduce/reduce errors)
-        | data_or_newtype capi_ctype tycl_hdr opt_kind_sig
+        | data_or_newtype capi_ctype tycl_hdr_inst opt_kind_sig
                  gadt_constrlist
                  maybe_derivings
                 {% amms (mkDataFamInst (comb4 $1 $3 $5 $6) (snd $ unLoc $1) $2
@@ -1313,7 +1332,7 @@ at_decl_inst :: { LInstDecl GhcPs }
                                 (fmap reverse $6))
                         ((fst $ unLoc $1):(fst $ unLoc $4)++(fst $ unLoc $5)) }
 
-        | data_or_newtype 'instance' capi_ctype tycl_hdr opt_kind_sig
+        | data_or_newtype 'instance' capi_ctype tycl_hdr_inst opt_kind_sig
                  gadt_constrlist
                  maybe_derivings
                 {% amms (mkDataFamInst (comb4 $1 $4 $6 $7) (snd $ unLoc $1) $3
@@ -1362,6 +1381,22 @@ tycl_hdr :: { Located (Maybe (LHsContext GhcPs), LHsType GhcPs) }
                                     }
         | type                      { sL1 $1 (Nothing, $1) }
 
+tycl_hdr_inst :: { Located (Maybe (LHsContext GhcPs), Maybe [LHsTyVarBndr GhcPs], LHsType GhcPs) }
+        : 'forall' tv_bndrs '.' context '=>' type   {% hintExplicitForall (getLoc $1)
+                                                       >> (addAnnotation (gl $4) (toUnicodeAnn AnnDarrow $5) (gl $5)
+                                                           >> ams (sLL $1 $> $ (Just $4, Just $2, $6))
+                                                                  [mu AnnForall $1, mj AnnDot $3])
+                                                    }
+        | 'forall' tv_bndrs '.' type   {% hintExplicitForall (getLoc $1)
+                                          >> ams (sLL $1 $> $ (Nothing, Just $2, $4))
+                                                 [mu AnnForall $1, mj AnnDot $3]
+                                       }
+        | context '=>' type         {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2)
+                                       >> (return (sLL $1 $> (Just $1, Nothing, $3)))
+                                    }
+        | type                      { sL1 $1 (Nothing, Nothing, $1) }
+
+
 capi_ctype :: { Maybe (Located CType) }
 capi_ctype : '{-# CTYPE' STRING STRING '#-}'
                        {% ajs (Just (sLL $1 $> (CType (getCTYPEs $1) (Just (Header (getSTRINGs $2) (getSTRING $2)))
@@ -1607,11 +1642,13 @@ rules   :: { OrdList (LRuleDecl GhcPs) }
         |  {- empty -}                 { nilOL }
 
 rule    :: { LRuleDecl GhcPs }
-        : STRING rule_activation rule_forall infixexp '=' exp
-         {%ams (sLL $1 $> $ (HsRule noExt (L (gl $1) (getSTRINGs $1,getSTRING $1))
-                                  ((snd $2) `orElse` AlwaysActive)
-                                  (snd $3) $4 $6))
-               (mj AnnEqual $5 : (fst $2) ++ (fst $3)) }
+        : STRING rule_activation rule_foralls infixexp '=' exp
+         {%ams (sLL $1 $> $ HsRule { rd_ext = noExt
+                                   , rd_name = L (gl $1) (getSTRINGs $1, getSTRING $1)
+                                   , rd_act = (snd $2) `orElse` AlwaysActive
+                                   , rd_tyvs = sndOf3 $3, rd_tmvs = thdOf3 $3
+                                   , rd_lhs = $4, rd_rhs = $6 })
+               (mj AnnEqual $5 : (fst $2) ++ (fstOf3 $3)) }
 
 -- Rules can be specified to be NeverActive, unlike inline/specialize pragmas
 rule_activation :: { ([AddAnn],Maybe Activation) }
@@ -1627,20 +1664,48 @@ rule_explicit_activation :: { ([AddAnn]
         | '[' '~' ']'           { ([mos $1,mj AnnTilde $2,mcs $3]
                                   ,NeverActive) }
 
-rule_forall :: { ([AddAnn],[LRuleBndr GhcPs]) }
-        : 'forall' rule_var_list '.'     { ([mu AnnForall $1,mj AnnDot $3],$2) }
-        | {- empty -}                    { ([],[]) }
-
-rule_var_list :: { [LRuleBndr GhcPs] }
-        : rule_var                              { [$1] }
-        | rule_var rule_var_list                { $1 : $2 }
-
-rule_var :: { LRuleBndr GhcPs }
-        : varid                         { sLL $1 $> (RuleBndr noExt $1) }
-        | '(' varid '::' ctype ')'      {% ams (sLL $1 $> (RuleBndrSig noExt $2
-                                                       (mkLHsSigWcType $4)))
+rule_foralls :: { ([AddAnn], Maybe [LHsTyVarBndr GhcPs], [LRuleBndr GhcPs]) }
+        : 'forall' rule_vars '.' 'forall' rule_vars '.'    {% let tyvs = mkRuleTyVarBndrs $2
+                                                              in hintExplicitForall (getLoc $1)
+                                                              >> checkRuleTyVarBndrNames (mkRuleTyVarBndrs $2)
+                                                              >> return ([mu AnnForall $1,mj AnnDot $3,
+                                                                          mu AnnForall $4,mj AnnDot $6],
+                                                                         Just (mkRuleTyVarBndrs $2), mkRuleBndrs $5) }
+        | 'forall' rule_vars '.'                           { ([mu AnnForall $1,mj AnnDot $3],
+                                                              Nothing, mkRuleBndrs $2) }
+        | {- empty -}                                      { ([], Nothing, []) }
+
+rule_vars :: { [LRuleTyTmVar] }
+        : rule_var rule_vars                    { $1 : $2 }
+        | {- empty -}                           { [] }
+
+rule_var :: { LRuleTyTmVar }
+        : varid                         { sLL $1 $> (RuleTyTmVar $1 Nothing) }
+        | '(' varid '::' ctype ')'      {% ams (sLL $1 $> (RuleTyTmVar $2 (Just $4)))
                                                [mop $1,mu AnnDcolon $3,mcp $5] }
 
+{- Note [Parsing explicit foralls in Rules]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We really want the above definition of rule_foralls to be:
+
+  rule_foralls : 'forall' tv_bndrs '.' 'forall' rule_vars '.'
+               | 'forall' rule_vars '.'
+               | {- empty -}
+
+where rule_vars (term variables) can be named "forall", "family", or "role",
+but tv_vars (type variables) cannot be. However, such a definition results
+in a reduce/reduce conflict. For example, when parsing:
+> {-# RULE "name" forall a ... #-}
+before the '...' it is impossible to determine whether we should be in the
+first or second case of the above.
+
+This is resolved by using rule_vars (which is more general) for both, and
+ensuring that type-level quantified variables do not have the names "forall",
+"family", or "role" in the function 'checkRuleTyVarBndrNames' in RdrHsSyn.hs
+Thus, whenever the definition of tyvarid (used for tv_bndrs) is changed relative
+to varid (used for rule_vars), 'checkRuleTyVarBndrNames' must be updated.
+-}
+
 -----------------------------------------------------------------------------
 -- Warnings and deprecations (c.f. rules)
 
@@ -2463,7 +2528,7 @@ quasiquote :: { Located (HsSplice GhcPs) }
                             in sL (getLoc $1) (mkHsQuasiQuote quoterId (RealSrcSpan quoteSpan) quote) }
 
 exp   :: { LHsExpr GhcPs }
-        : infixexp '::' sigtype {% ams (sLL $1 $> $ ExprWithTySig (mkLHsSigWcType $3) $1)
+        : infixexp '::' sigtype {% ams (sLL $1 $> $ ExprWithTySig noExt $1 (mkLHsSigWcType $3))
                                        [mu AnnDcolon $2] }
         | infixexp '-<' exp     {% ams (sLL $1 $> $ HsArrApp noExt $1 $3
                                                         HsFirstOrderApp True)
@@ -2561,7 +2626,7 @@ fexp    :: { LHsExpr GhcPs }
         : fexp aexp                  {% checkBlockArguments $1 >> checkBlockArguments $2 >>
                                         return (sLL $1 $> $ (HsApp noExt $1 $2)) }
         | fexp TYPEAPP atype         {% checkBlockArguments $1 >>
-                                        ams (sLL $1 $> $ HsAppType (mkHsWildCardBndrs $3) $1)
+                                        ams (sLL $1 $> $ HsAppType noExt $1 (mkHsWildCardBndrs $3))
                                             [mj AnnAt $2] }
         | 'static' aexp              {% ams (sLL $1 $> $ HsStatic noExt $2)
                                             [mj AnnStatic $1] }
@@ -3308,6 +3373,8 @@ tyvarid :: { Located RdrName }
         | 'unsafe'         { sL1 $1 $! mkUnqual tvName (fsLit "unsafe") }
         | 'safe'           { sL1 $1 $! mkUnqual tvName (fsLit "safe") }
         | 'interruptible'  { sL1 $1 $! mkUnqual tvName (fsLit "interruptible") }
+        -- If this changes relative to varid, update 'checkRuleTyVarBndrNames' in RdrHsSyn.hs
+        -- See Note [Parsing explicit foralls in Rules]
 
 -----------------------------------------------------------------------------
 -- Variables
@@ -3348,6 +3415,8 @@ varid :: { Located RdrName }
         | 'forall'         { sL1 $1 $! mkUnqual varName (fsLit "forall") }
         | 'family'         { sL1 $1 $! mkUnqual varName (fsLit "family") }
         | 'role'           { sL1 $1 $! mkUnqual varName (fsLit "role") }
+        -- If this changes relative to tyvarid, update 'checkRuleTyVarBndrNames' in RdrHsSyn.hs
+        -- See Note [Parsing explicit foralls in Rules]
 
 qvarsym :: { Located RdrName }
         : varsym                { $1 }
diff --git a/compiler/parser/RdrHsSyn.hs b/compiler/parser/RdrHsSyn.hs
index 1e89d5a459..9917d960f8 100644
--- a/compiler/parser/RdrHsSyn.hs
+++ b/compiler/parser/RdrHsSyn.hs
@@ -54,6 +54,9 @@ module   RdrHsSyn (
         checkValDef,          -- (SrcLoc, HsExp, HsRhs, [HsDecl]) -> P HsDecl
         checkValSigLhs,
         checkDoAndIfThenElse,
+        LRuleTyTmVar, RuleTyTmVar(..),
+        mkRuleBndrs, mkRuleTyVarBndrs,
+        checkRuleTyVarBndrNames,
         checkRecordSyntax,
         checkEmptyGADTs,
         parseErrorSDoc, hintBangPat,
@@ -174,11 +177,13 @@ mkATDefault :: LTyFamInstDecl GhcPs
 -- some necessary paren annotations to the parsing context. Naturally, this
 -- is not something that the "Convert" use cares about.
 mkATDefault (L loc (TyFamInstDecl { tfid_eqn = HsIB { hsib_body = e }}))
-      | FamEqn { feqn_tycon = tc, feqn_pats = pats, feqn_fixity = fixity
-               , feqn_rhs = rhs } <- e
+      | FamEqn { feqn_tycon = tc, feqn_bndrs = bndrs, feqn_pats = pats
+               , feqn_fixity = fixity, feqn_rhs = rhs } <- e
       = do { (tvs, anns) <- checkTyVars (text "default") equalsDots tc pats
            ; let f = L loc (FamEqn { feqn_ext    = noExt
                                    , feqn_tycon  = tc
+                                   , feqn_bndrs  = ASSERT( isNothing bndrs )
+                                                   Nothing
                                    , feqn_pats   = tvs
                                    , feqn_fixity = fixity
                                    , feqn_rhs    = rhs })
@@ -235,14 +240,16 @@ mkTySynonym loc lhs rhs
                                 , tcdFixity = fixity
                                 , tcdRhs = rhs })) }
 
-mkTyFamInstEqn :: LHsType GhcPs
+mkTyFamInstEqn :: Maybe [LHsTyVarBndr GhcPs]
+               -> LHsType GhcPs
                -> LHsType GhcPs
                -> P (TyFamInstEqn GhcPs,[AddAnn])
-mkTyFamInstEqn lhs rhs
+mkTyFamInstEqn bndrs lhs rhs
   = do { (tc, tparams, fixity, ann) <- checkTyClHdr False lhs
        ; return (mkHsImplicitBndrs
                   (FamEqn { feqn_ext    = noExt
                           , feqn_tycon  = tc
+                          , feqn_bndrs  = bndrs
                           , feqn_pats   = tparams
                           , feqn_fixity = fixity
                           , feqn_rhs    = rhs }),
@@ -251,18 +258,19 @@ mkTyFamInstEqn lhs rhs
 mkDataFamInst :: SrcSpan
               -> NewOrData
               -> Maybe (Located CType)
-              -> Located (Maybe (LHsContext GhcPs), LHsType GhcPs)
+              -> Located (Maybe (LHsContext GhcPs), Maybe [LHsTyVarBndr GhcPs], LHsType GhcPs)
               -> Maybe (LHsKind GhcPs)
               -> [LConDecl GhcPs]
               -> HsDeriving GhcPs
               -> P (LInstDecl GhcPs)
-mkDataFamInst loc new_or_data cType (L _ (mcxt, tycl_hdr)) ksig data_cons maybe_deriv
+mkDataFamInst loc new_or_data cType (L _ (mcxt, bndrs, tycl_hdr)) ksig data_cons maybe_deriv
   = do { (tc, tparams, fixity, ann) <- checkTyClHdr False tycl_hdr
        ; mapM_ (\a -> a loc) ann -- Add any API Annotations to the top SrcSpan
        ; defn <- mkDataDefn new_or_data cType mcxt ksig data_cons maybe_deriv
        ; return (L loc (DataFamInstD noExt (DataFamInstDecl (mkHsImplicitBndrs
                   (FamEqn { feqn_ext    = noExt
                           , feqn_tycon  = tc
+                          , feqn_bndrs  = bndrs
                           , feqn_pats   = tparams
                           , feqn_fixity = fixity
                           , feqn_rhs    = defn }))))) }
@@ -844,6 +852,33 @@ checkDatatypeContext (Just (L loc c))
                  (text "Illegal datatype context (use DatatypeContexts):" <+>
                   pprHsContext c)
 
+type LRuleTyTmVar = Located RuleTyTmVar
+data RuleTyTmVar = RuleTyTmVar (Located RdrName) (Maybe (LHsType GhcPs))
+-- ^ Essentially a wrapper for a @RuleBndr GhcPs@
+
+-- turns RuleTyTmVars into RuleBnrs - this is straightforward
+mkRuleBndrs :: [LRuleTyTmVar] -> [LRuleBndr GhcPs]
+mkRuleBndrs = fmap (fmap cvt_one)
+  where cvt_one (RuleTyTmVar v Nothing)    = RuleBndr    noExt v
+        cvt_one (RuleTyTmVar v (Just sig)) = RuleBndrSig noExt v (mkLHsSigWcType sig)
+
+-- turns RuleTyTmVars into HsTyVarBndrs - this is more interesting
+mkRuleTyVarBndrs :: [LRuleTyTmVar] -> [LHsTyVarBndr GhcPs]
+mkRuleTyVarBndrs = fmap (fmap cvt_one)
+  where cvt_one (RuleTyTmVar v Nothing)    = UserTyVar   noExt (fmap tm_to_ty v)
+        cvt_one (RuleTyTmVar v (Just sig)) = KindedTyVar noExt (fmap tm_to_ty v) sig
+        -- takes something in namespace 'varName' to something in namespace 'tvName'
+        tm_to_ty (Unqual occ) = Unqual (setOccNameSpace tvName occ)
+        tm_to_ty _ = panic "mkRuleTyVarBndrs"
+
+-- See note [Parsing explicit foralls in Rules] in Parser.y
+checkRuleTyVarBndrNames :: [LHsTyVarBndr GhcPs] -> P ()
+checkRuleTyVarBndrNames = mapM_ (check . fmap hsTyVarName)
+  where check (L loc (Unqual occ)) = do
+          when ((occNameString occ ==) `any` ["forall","family","role"])
+               (parseErrorSDoc loc (text $ "parse error on input " ++ occNameString occ))
+        check _ = panic "checkRuleTyVarBndrNames"
+
 checkRecordSyntax :: Outputable a => Located a -> P (Located a)
 checkRecordSyntax lr@(L loc r)
     = do allowed <- extension traditionalRecordSyntaxEnabled
@@ -1038,8 +1073,8 @@ checkAPat msg loc e0 = do
    -- view pattern is well-formed if the pattern is
    EViewPat _ expr patE -> checkLPat msg patE >>=
                             (return . (\p -> ViewPat noExt expr p))
-   ExprWithTySig t e   -> do e <- checkLPat msg e
-                             return (SigPat t e)
+   ExprWithTySig _ e t  -> do e <- checkLPat msg e
+                              return (SigPat noExt e t)
 
    -- n+k patterns
    OpApp _ (L nloc (HsVar _ (L _ n))) (L _ (HsVar _ (L _ plus)))
@@ -1114,7 +1149,7 @@ checkValDef :: SDoc
 checkValDef msg _strictness lhs (Just sig) grhss
         -- x :: ty = rhs  parses as a *pattern* binding
   = checkPatBind msg (L (combineLocs lhs sig)
-                        (ExprWithTySig (mkLHsSigWcType sig) lhs)) grhss
+                        (ExprWithTySig noExt lhs (mkLHsSigWcType sig))) grhss
 
 checkValDef msg strictness lhs Nothing g@(L l (_,grhss))
   = do  { mb_fun <- isFunLhs lhs