Replace HsImplicitBndrs with HsOuterTyVarBndrs

This refactors the GHC AST to remove `HsImplicitBndrs` and replace it with
`HsOuterTyVarBndrs`, a type which records whether the outermost quantification
in a type is explicit (i.e., with an outermost, invisible `forall`) or
implicit. As a result of this refactoring, it is now evident in the AST where
the `forall`-or-nothing rule applies: it's all the places that use
`HsOuterTyVarBndrs`. See the revamped `Note [forall-or-nothing rule]` in
`GHC.Hs.Type` (previously in `GHC.Rename.HsType`).

Moreover, the places where `ScopedTypeVariables` brings lexically scoped type
variables into scope are a subset of the places that adhere to the
`forall`-or-nothing rule, so this also makes places that interact with
`ScopedTypeVariables` easier to find. See the revamped
`Note [Lexically scoped type variables]` in `GHC.Hs.Type` (previously in
`GHC.Tc.Gen.Sig`).

`HsOuterTyVarBndrs` are used in type signatures (see `HsOuterSigTyVarBndrs`)
and type family equations (see `HsOuterFamEqnTyVarBndrs`). The main difference
between the former and the latter is that the former cares about specificity
but the latter does not.

There are a number of knock-on consequences:

* There is now a dedicated `HsSigType` type, which is the combination of
  `HsOuterSigTyVarBndrs` and `HsType`. `LHsSigType` is now an alias for an
  `XRec` of `HsSigType`.
* Working out the details led us to a substantial refactoring of
  the handling of explicit (user-written) and implicit type-variable
  bindings in `GHC.Tc.Gen.HsType`.

  Instead of a confusing family of higher order functions, we now
  have a local data type, `SkolemInfo`, that controls how these
  binders are kind-checked.

  It remains very fiddly, not fully satisfying. But it's better
  than it was.

Fixes #16762. Bumps the Haddock submodule.

Co-authored-by: Simon Peyton Jones <simonpj@microsoft.com>
Co-authored-by: Richard Eisenberg <rae@richarde.dev>
Co-authored-by: Zubin Duggal <zubin@cmi.ac.in>

1 files changed, 47 insertions, 35 deletions

diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index 10727e1e17..fc0ad8a007 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -1231,7 +1231,7 @@ ty_decl :: { LTyClDecl GhcPs }
 
 -- standalone kind signature
 standalone_kind_sig :: { LStandaloneKindSig GhcPs }
-  : 'type' sks_vars '::' ktype
+  : 'type' sks_vars '::' sigktype
       {% amms (mkStandaloneKindSig (comb2 $1 $4) $2 $4)
               [mj AnnType $1,mu AnnDcolon $3] }
 
@@ -1251,7 +1251,7 @@ inst_decl :: { LInstDecl GhcPs }
                                      , cid_tyfam_insts = ats
                                      , cid_overlap_mode = $2
                                      , cid_datafam_insts = adts }
-             ; ams (L (comb3 $1 (hsSigType $3) $4) (ClsInstD { cid_d_ext = noExtField, cid_inst = cid }))
+             ; ams (L (comb3 $1 $3 $4) (ClsInstD { cid_d_ext = noExtField, cid_inst = cid }))
                    (mj AnnInstance $1 : (fst $ unLoc $4)) } }
 
            -- type instance declarations
@@ -1261,7 +1261,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_inst constrs
+        | data_or_newtype 'instance' capi_ctype datafam_inst_hdr constrs
                           maybe_derivings
             {% amms (mkDataFamInst (comb4 $1 $4 $5 $6) (snd $ unLoc $1) $3 (snd $ unLoc $4)
                                       Nothing (reverse (snd  $ unLoc $5))
@@ -1269,7 +1269,7 @@ inst_decl :: { LInstDecl GhcPs }
                     ((fst $ unLoc $1):mj AnnInstance $2:(fst $ unLoc $4)++(fst $ unLoc $5)) }
 
           -- GADT instance declaration
-        | data_or_newtype 'instance' capi_ctype tycl_hdr_inst opt_kind_sig
+        | data_or_newtype 'instance' capi_ctype datafam_inst_hdr opt_kind_sig
                  gadt_constrlist
                  maybe_derivings
             {% amms (mkDataFamInst (comb4 $1 $4 $6 $7) (snd $ unLoc $1) $3 (snd $ unLoc $4)
@@ -1298,7 +1298,7 @@ deriv_strategy_no_via :: { LDerivStrategy GhcPs }
                                        [mj AnnNewtype $1] }
 
 deriv_strategy_via :: { LDerivStrategy GhcPs }
-  : 'via' ktype             {% ams (sLL $1 $> (ViaStrategy (mkLHsSigType $2)))
+  : 'via' sigktype          {% ams (sLL $1 $> (ViaStrategy $2))
                                        [mj AnnVia $1] }
 
 deriv_standalone_strategy :: { Maybe (LDerivStrategy GhcPs) }
@@ -1361,12 +1361,12 @@ ty_fam_inst_eqns :: { Located [LTyFamInstEqn GhcPs] }
 ty_fam_inst_eqn :: { Located ([AddAnn],TyFamInstEqn GhcPs) }
         : 'forall' tv_bndrs '.' type '=' ktype
               {% do { hintExplicitForall $1
-                    ; tvb <- fromSpecTyVarBndrs $2
-                    ; (eqn,ann) <- mkTyFamInstEqn (Just tvb) $4 $6
+                    ; tvbs <- fromSpecTyVarBndrs $2
+                    ; (eqn,ann) <- mkTyFamInstEqn (mkHsOuterExplicit tvbs) $4 $6
                     ; return (sLL $1 $>
                                (mu AnnForall $1:mj AnnDot $3:mj AnnEqual $5:ann,eqn)) } }
         | type '=' ktype
-              {% do { (eqn,ann) <- mkTyFamInstEqn Nothing $1 $3
+              {% do { (eqn,ann) <- mkTyFamInstEqn mkHsOuterImplicit $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
@@ -1432,14 +1432,14 @@ at_decl_inst :: { LInstDecl GhcPs }
                         (mj AnnType $1:$2++(fst $ unLoc $3)) }
 
         -- data/newtype instance declaration, with optional 'instance' keyword
-        | data_or_newtype opt_instance capi_ctype tycl_hdr_inst constrs maybe_derivings
+        | data_or_newtype opt_instance capi_ctype datafam_inst_hdr constrs maybe_derivings
                {% amms (mkDataFamInst (comb4 $1 $4 $5 $6) (snd $ unLoc $1) $3 (snd $ unLoc $4)
                                     Nothing (reverse (snd $ unLoc $5))
                                             (fmap reverse $6))
                        ((fst $ unLoc $1):$2++(fst $ unLoc $4)++(fst $ unLoc $5)) }
 
         -- GADT instance declaration, with optional 'instance' keyword
-        | data_or_newtype opt_instance capi_ctype tycl_hdr_inst opt_kind_sig
+        | data_or_newtype opt_instance capi_ctype datafam_inst_hdr opt_kind_sig
                  gadt_constrlist
                  maybe_derivings
                 {% amms (mkDataFamInst (comb4 $1 $4 $6 $7) (snd $ unLoc $1) $3
@@ -1490,23 +1490,23 @@ tycl_hdr :: { Located (Maybe (LHsContext GhcPs), LHsType GhcPs) }
                                     }
         | type                      { sL1 $1 (Nothing, $1) }
 
-tycl_hdr_inst :: { Located ([AddAnn],(Maybe (LHsContext GhcPs), Maybe [LHsTyVarBndr () GhcPs], LHsType GhcPs)) }
+datafam_inst_hdr :: { Located ([AddAnn],(Maybe (LHsContext GhcPs), HsOuterFamEqnTyVarBndrs GhcPs, LHsType GhcPs)) }
         : 'forall' tv_bndrs '.' context '=>' type   {% hintExplicitForall $1
                                                        >> fromSpecTyVarBndrs $2
                                                          >>= \tvbs -> (addAnnotation (gl $4) (toUnicodeAnn AnnDarrow $5) (gl $5)
                                                              >> return (sLL $1 $> ([mu AnnForall $1, mj AnnDot $3]
-                                                                                  , (Just $4, Just tvbs, $6)))
+                                                                                  , (Just $4, mkHsOuterExplicit tvbs, $6)))
                                                           )
                                                     }
         | 'forall' tv_bndrs '.' type   {% do { hintExplicitForall $1
                                              ; tvbs <- fromSpecTyVarBndrs $2
                                              ; return (sLL $1 $> ([mu AnnForall $1, mj AnnDot $3]
-                                                                 , (Nothing, Just tvbs, $4)))
+                                                                 , (Nothing, mkHsOuterExplicit tvbs, $4)))
                                        } }
         | context '=>' type         {% addAnnotation (gl $1) (toUnicodeAnn AnnDarrow $2) (gl $2)
-                                       >> (return (sLL $1 $>([], (Just $1, Nothing, $3))))
+                                       >> (return (sLL $1 $>([], (Just $1, mkHsOuterImplicit, $3))))
                                     }
-        | type                      { sL1 $1 ([], (Nothing, Nothing, $1)) }
+        | type                      { sL1 $1 ([], (Nothing, mkHsOuterImplicit, $1)) }
 
 
 capi_ctype :: { Maybe (Located CType) }
@@ -1529,7 +1529,7 @@ stand_alone_deriving :: { LDerivDecl GhcPs }
   : 'deriving' deriv_standalone_strategy 'instance' overlap_pragma inst_type
                 {% do { let { err = text "in the stand-alone deriving instance"
                                     <> colon <+> quotes (ppr $5) }
-                      ; ams (sLL $1 (hsSigType $>)
+                      ; ams (sLL $1 $>
                                  (DerivDecl noExtField (mkHsWildCardBndrs $5) $2 $4))
                             [mj AnnDeriving $1, mj AnnInstance $3] } }
 
@@ -1602,7 +1602,7 @@ where_decls :: { Located ([AddAnn]
 
 pattern_synonym_sig :: { LSig GhcPs }
         : 'pattern' con_list '::' sigtype
-                   {% ams (sLL $1 $> $ PatSynSig noExtField (unLoc $2) (mkLHsSigType $4))
+                   {% ams (sLL $1 $> $ PatSynSig noExtField (unLoc $2) $4)
                           [mj AnnPattern $1, mu AnnDcolon $3] }
 
 -----------------------------------------------------------------------------
@@ -1620,7 +1620,7 @@ decl_cls  : at_decl_cls                 { $1 }
                        do { v <- checkValSigLhs $2
                           ; let err = text "in default signature" <> colon <+>
                                       quotes (ppr $2)
-                          ; ams (sLL $1 $> $ SigD noExtField $ ClassOpSig noExtField True [v] $ mkLHsSigType $4)
+                          ; ams (sLL $1 $> $ SigD noExtField $ ClassOpSig noExtField True [v] $4)
                                 [mj AnnDefault $1,mu AnnDcolon $3] } }
 
 decls_cls :: { Located ([AddAnn],OrdList (LHsDecl GhcPs)) }  -- Reversed
@@ -1941,9 +1941,9 @@ fspec :: { Located ([AddAnn]
                     ,(Located StringLiteral, Located RdrName, LHsSigType GhcPs)) }
        : STRING var '::' sigtype        { sLL $1 $> ([mu AnnDcolon $3]
                                              ,(L (getLoc $1)
-                                                    (getStringLiteral $1), $2, mkLHsSigType $4)) }
+                                                    (getStringLiteral $1), $2, $4)) }
        |        var '::' sigtype        { sLL $1 $> ([mu AnnDcolon $2]
-                                             ,(noLoc (StringLiteral NoSourceText nilFS), $1, mkLHsSigType $3)) }
+                                             ,(noLoc (StringLiteral NoSourceText nilFS), $1, $3)) }
          -- if the entity string is missing, it defaults to the empty string;
          -- the meaning of an empty entity string depends on the calling
          -- convention
@@ -1953,14 +1953,26 @@ fspec :: { Located ([AddAnn]
 
 opt_sig :: { ([AddAnn], Maybe (LHsType GhcPs)) }
         : {- empty -}                   { ([],Nothing) }
-        | '::' sigtype                  { ([mu AnnDcolon $1],Just $2) }
+        | '::' ctype                    { ([mu AnnDcolon $1],Just $2) }
 
 opt_tyconsig :: { ([AddAnn], Maybe (Located RdrName)) }
              : {- empty -}              { ([], Nothing) }
              | '::' gtycon              { ([mu AnnDcolon $1], Just $2) }
 
-sigtype :: { LHsType GhcPs }
-        : ctype                            { $1 }
+-- Like ktype, but for types that obey the forall-or-nothing rule.
+-- See Note [forall-or-nothing rule] in GHC.Hs.Type.
+sigktype :: { LHsSigType GhcPs }
+        : sigtype              { $1 }
+        | ctype '::' kind      {% ams (sLL $1 $> $ mkHsImplicitSigType $
+                                       sLL $1 $> $ HsKindSig noExtField $1 $3)
+                                      [mu AnnDcolon $2] }
+
+-- Like ctype, but for types that obey the forall-or-nothing rule.
+-- See Note [forall-or-nothing rule] in GHC.Hs.Type. To avoid duplicating the
+-- logic in ctype here, we simply reuse the ctype production and perform
+-- surgery on the LHsType it returns to turn it into an LHsSigType.
+sigtype :: { LHsSigType GhcPs }
+        : ctype                            { hsTypeToHsSigType $1 }
 
 sig_vars :: { Located [Located RdrName] }    -- Returned in reversed order
          : sig_vars ',' var           {% addAnnotation (gl $ head $ unLoc $1)
@@ -1969,9 +1981,9 @@ sig_vars :: { Located [Located RdrName] }    -- Returned in reversed order
          | var                        { sL1 $1 [$1] }
 
 sigtypes1 :: { (OrdList (LHsSigType GhcPs)) }
-   : sigtype                 { unitOL (mkLHsSigType $1) }
+   : sigtype                 { unitOL $1 }
    | sigtype ',' sigtypes1   {% addAnnotation (gl $1) AnnComma (gl $2)
-                                >> return (unitOL (mkLHsSigType $1) `appOL` $3) }
+                                >> return (unitOL $1 `appOL` $3) }
 
 -----------------------------------------------------------------------------
 -- Types
@@ -1996,7 +2008,6 @@ ktype :: { LHsType GhcPs }
         : ctype                { $1 }
         | ctype '::' kind      {% ams (sLL $1 $> $ HsKindSig noExtField $1 $3)
                                       [mu AnnDcolon $2] }
-
 -- A ctype is a for-all type
 ctype   :: { LHsType GhcPs }
         : forall_telescope ctype      {% let (forall_anns, forall_tele) = unLoc $1 in
@@ -2162,13 +2173,13 @@ atype :: { LHsType GhcPs }
 --      e.g.  (Foo a, Gaz b) => Wibble a b
 -- It's kept as a single type for convenience.
 inst_type :: { LHsSigType GhcPs }
-        : sigtype                       { mkLHsSigType $1 }
+        : sigtype                       { $1 }
 
 deriv_types :: { [LHsSigType GhcPs] }
-        : ktype                         { [mkLHsSigType $1] }
+        : sigktype                      { [$1] }
 
-        | ktype ',' deriv_types         {% addAnnotation (gl $1) AnnComma (gl $2)
-                                           >> return (mkLHsSigType $1 : $3) }
+        | sigktype ',' deriv_types      {% addAnnotation (gl $1) AnnComma (gl $2)
+                                           >> return ($1 : $3) }
 
 comma_types0  :: { [LHsType GhcPs] }  -- Zero or more:  ty,ty,ty
         : comma_types1                  { $1 }
@@ -2381,8 +2392,9 @@ deriving :: { LHsDerivingClause GhcPs }
                         [mj AnnDeriving $1] }
 
 deriv_clause_types :: { LDerivClauseTys GhcPs }
-        : qtycon              { let { tc = sL1 $1 (HsTyVar noExtField NotPromoted $1) } in
-                                sL1 $1 (DctSingle noExtField (mkLHsSigType tc)) }
+        : qtycon              { let { tc = sL1 $1 $ mkHsImplicitSigType $
+                                           sL1 $1 $ HsTyVar noExtField NotPromoted $1 } in
+                                sL1 $1 (DctSingle noExtField tc) }
         | '(' ')'             {% ams (sLL $1 $> (DctMulti noExtField []))
                                      [mop $1,mcp $2] }
         | '(' deriv_types ')' {% ams (sLL $1 $> (DctMulti noExtField $2))
@@ -2466,11 +2478,11 @@ sigdecl :: { LHsDecl GhcPs }
                               ; v <- checkValSigLhs $1
                               ; _ <- amsL (comb2 $1 $>) [mu AnnDcolon $2]
                               ; return (sLL $1 $> $ SigD noExtField $
-                                  TypeSig noExtField [v] (mkLHsSigWcType $3))} }
+                                  TypeSig noExtField [v] (mkHsWildCardBndrs $3))} }
 
         | var ',' sig_vars '::' sigtype
            {% do { let sig = TypeSig noExtField ($1 : reverse (unLoc $3))
-                                     (mkLHsSigWcType $5)
+                                     (mkHsWildCardBndrs $5)
                  ; addAnnotation (gl $1) AnnComma (gl $2)
                  ; ams ( sLL $1 $> $ SigD noExtField sig )
                        [mu AnnDcolon $4] } }
@@ -2556,7 +2568,7 @@ quasiquote :: { Located (HsSplice GhcPs) }
                             in sL (getLoc $1) (mkHsQuasiQuote quoterId (mkSrcSpanPs quoteSpan) quote) }
 
 exp   :: { ECP }
-        : infixexp '::' sigtype
+        : infixexp '::' ctype
                                 { ECP $
                                    unECP $1 >>= \ $1 ->
                                    rejectPragmaPV $1 >>