[Git][ghc/ghc][wip/T18432-T18455] Clean up the inferred type variable restriction

Ryan Scott gitlab at gitlab.haskell.org
Fri Jul 17 12:28:46 UTC 2020



Ryan Scott pushed to branch wip/T18432-T18455 at Glasgow Haskell Compiler / GHC


Commits:
360112d8 by Ryan Scott at 2020-07-17T08:26:08-04:00
Clean up the inferred type variable restriction

This patch primarily:

* Documents `checkInferredVars` (previously called
  `check_inferred_vars`) more carefully. This is the
  function which throws an error message if a user quantifies an
  inferred type variable in a place where specificity cannot be
  observed. See `Note [Unobservably inferred type variables]` in
  `GHC.Rename.HsType`.

  Note that I now invoke `checkInferredVars` _alongside_
  `rnHsSigType`, `rnHsWcSigType`, etc. rather than doing so _inside_
  of these functions. This results in slightly more call sites for
  `checkInferredVars`, but it makes it much easier to enumerate the
  spots where the inferred type variable restriction comes into
  effect.
* Removes the inferred type variable restriction for default method
  type signatures, per the discussion in #18432. As a result, this
  patch fixes #18432.

Along the way, I performed some various cleanup:

* I moved `no_nested_foralls_contexts_err` into `GHC.Rename.Utils`
  (under the new name `noNestedForallsContextsErr`), since it now
  needs to be invoked from multiple modules. I also added a helper
  function `addNoNestedForallsContextsErr` that throws the error
  message after producing it, as this is a common idiom.
* In order to ensure that users cannot sneak inferred type variables
  into `SPECIALISE instance` pragmas by way of nested `forall`s, I
  now invoke `addNoNestedForallsContextsErr` when renaming
  `SPECIALISE instance` pragmas, much like when we rename normal
  instance declarations. (This probably should have originally been
  done as a part of the fix for #18240, but this task was somehow
  overlooked.) As a result, this patch fixes #18455 as a side effect.

- - - - -


14 changed files:

- compiler/GHC/Hs/Type.hs
- compiler/GHC/Rename/Bind.hs
- compiler/GHC/Rename/Expr.hs
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Rename/Pat.hs
- compiler/GHC/Rename/Utils.hs
- + testsuite/tests/quantified-constraints/T18432.hs
- testsuite/tests/quantified-constraints/all.T
- testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.hs → testsuite/tests/typecheck/should_compile/ExplicitSpecificity4.hs
- testsuite/tests/typecheck/should_compile/all.T
- + testsuite/tests/typecheck/should_fail/T18455.hs
- + testsuite/tests/typecheck/should_fail/T18455.stderr
- testsuite/tests/typecheck/should_fail/all.T


Changes:

=====================================
compiler/GHC/Hs/Type.hs
=====================================
@@ -1628,6 +1628,12 @@ instance types, which makes things like the instance above become illegal.
 For the sake of consistency, we also disallow nested contexts, even though they
 don't have the same strange interaction with ScopedTypeVariables.
 
+Just as we forbid nested `forall`s and contexts in normal instance
+declarations, we also forbid them in SPECIALISE instance pragmas (#18455).
+Unlike normal instance declarations, ScopedTypeVariables don't have any impact
+on SPECIALISE instance pragmas, but we use the same validity checks for
+SPECIALISE instance pragmas anyway to be consistent.
+
 -----
 -- Wrinkle: Derived instances
 -----


=====================================
compiler/GHC/Rename/Bind.hs
=====================================
@@ -43,7 +43,8 @@ import GHC.Rename.Fixity
 import GHC.Rename.Utils ( HsDocContext(..), mapFvRn, extendTyVarEnvFVRn
                         , checkDupRdrNames, warnUnusedLocalBinds
                         , checkUnusedRecordWildcard
-                        , checkDupAndShadowedNames, bindLocalNamesFV )
+                        , checkDupAndShadowedNames, bindLocalNamesFV
+                        , addNoNestedForallsContextsErr, checkInferredVars )
 import GHC.Driver.Session
 import GHC.Unit.Module
 import GHC.Types.Name
@@ -955,7 +956,7 @@ renameSig _ (IdSig _ x)
 renameSig ctxt sig@(TypeSig _ vs ty)
   = do  { new_vs <- mapM (lookupSigOccRn ctxt sig) vs
         ; let doc = TypeSigCtx (ppr_sig_bndrs vs)
-        ; (new_ty, fvs) <- rnHsSigWcType doc Nothing ty
+        ; (new_ty, fvs) <- rnHsSigWcType doc ty
         ; return (TypeSig noExtField new_vs new_ty, fvs) }
 
 renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty)
@@ -963,20 +964,25 @@ renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty)
         ; when (is_deflt && not defaultSigs_on) $
           addErr (defaultSigErr sig)
         ; new_v <- mapM (lookupSigOccRn ctxt sig) vs
-        ; (new_ty, fvs) <- rnHsSigType ty_ctxt TypeLevel inf_msg ty
+        ; (new_ty, fvs) <- rnHsSigType ty_ctxt TypeLevel ty
         ; return (ClassOpSig noExtField is_deflt new_v new_ty, fvs) }
   where
     (v1:_) = vs
     ty_ctxt = GenericCtx (text "a class method signature for"
                           <+> quotes (ppr v1))
-    inf_msg = if is_deflt
-      then Just (text "A default type signature cannot contain inferred type variables")
-      else Nothing
 
 renameSig _ (SpecInstSig _ src ty)
-  = do  { (new_ty, fvs) <- rnHsSigType SpecInstSigCtx TypeLevel inf_msg ty
+  = do  { checkInferredVars doc inf_msg ty
+        ; (new_ty, fvs) <- rnHsSigType doc TypeLevel ty
+          -- Check if there are any nested `forall`s or contexts, which are
+          -- illegal in the type of an instance declaration (see
+          -- Note [No nested foralls or contexts in instance types] in
+          -- GHC.Hs.Type).
+        ; addNoNestedForallsContextsErr doc (text "SPECIALISE instance type")
+            (getLHsInstDeclHead new_ty)
         ; return (SpecInstSig noExtField src new_ty,fvs) }
   where
+    doc = SpecInstSigCtx
     inf_msg = Just (text "Inferred type variables are not allowed")
 
 -- {-# SPECIALISE #-} pragmas can refer to imported Ids
@@ -993,7 +999,7 @@ renameSig ctxt sig@(SpecSig _ v tys inl)
     ty_ctxt = GenericCtx (text "a SPECIALISE signature for"
                           <+> quotes (ppr v))
     do_one (tys,fvs) ty
-      = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt TypeLevel Nothing ty
+      = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt TypeLevel ty
            ; return ( new_ty:tys, fvs_ty `plusFV` fvs) }
 
 renameSig ctxt sig@(InlineSig _ v s)
@@ -1010,7 +1016,7 @@ renameSig ctxt sig@(MinimalSig _ s (L l bf))
 
 renameSig ctxt sig@(PatSynSig _ vs ty)
   = do  { new_vs <- mapM (lookupSigOccRn ctxt sig) vs
-        ; (ty', fvs) <- rnHsSigType ty_ctxt TypeLevel Nothing ty
+        ; (ty', fvs) <- rnHsSigType ty_ctxt TypeLevel ty
         ; return (PatSynSig noExtField new_vs ty', fvs) }
   where
     ty_ctxt = GenericCtx (text "a pattern synonym signature for"


=====================================
compiler/GHC/Rename/Expr.hs
=====================================
@@ -318,7 +318,7 @@ rnExpr (RecordUpd { rupd_expr = expr, rupd_flds = rbinds })
                  , fvExpr `plusFV` fvRbinds) }
 
 rnExpr (ExprWithTySig _ expr pty)
-  = do  { (pty', fvTy)    <- rnHsSigWcType ExprWithTySigCtx Nothing pty
+  = do  { (pty', fvTy)    <- rnHsSigWcType ExprWithTySigCtx pty
         ; (expr', fvExpr) <- bindSigTyVarsFV (hsWcScopedTvs pty') $
                              rnLExpr expr
         ; return (ExprWithTySig noExtField expr' pty', fvExpr `plusFV` fvTy) }


=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -39,7 +39,6 @@ import GHC.Prelude
 
 import {-# SOURCE #-} GHC.Rename.Splice( rnSpliceType )
 
-import GHC.Core.Type
 import GHC.Driver.Session
 import GHC.Hs
 import GHC.Rename.Doc    ( rnLHsDoc, rnMbLHsDoc )
@@ -68,7 +67,7 @@ import GHC.Data.FastString
 import GHC.Data.Maybe
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List          ( nubBy, partition, find )
+import Data.List          ( nubBy, partition )
 import Control.Monad      ( unless, when )
 
 #include "HsVersions.h"
@@ -124,19 +123,16 @@ data HsSigWcTypeScoping
     -- "GHC.Hs.Type".
 
 rnHsSigWcType :: HsDocContext
-              -> Maybe SDoc
-              -- ^ The error msg if the signature is not allowed to contain
-              --   manually written inferred variables.
               -> LHsSigWcType GhcPs
               -> RnM (LHsSigWcType GhcRn, FreeVars)
-rnHsSigWcType doc inf_err (HsWC { hswc_body = HsIB { hsib_body = hs_ty }})
-  = rn_hs_sig_wc_type BindUnlessForall doc inf_err hs_ty $ \nwcs imp_tvs body ->
+rnHsSigWcType doc (HsWC { hswc_body = HsIB { hsib_body = hs_ty }})
+  = rn_hs_sig_wc_type BindUnlessForall doc hs_ty $ \nwcs imp_tvs body ->
     let ib_ty = HsIB { hsib_ext = imp_tvs, hsib_body = body  }
         wc_ty = HsWC { hswc_ext = nwcs,    hswc_body = ib_ty } in
     pure (wc_ty, emptyFVs)
 
 rnHsPatSigType :: HsSigWcTypeScoping
-               -> HsDocContext -> Maybe SDoc
+               -> HsDocContext
                -> HsPatSigType GhcPs
                -> (HsPatSigType GhcRn -> RnM (a, FreeVars))
                -> RnM (a, FreeVars)
@@ -147,10 +143,10 @@ rnHsPatSigType :: HsSigWcTypeScoping
 -- Wildcards are allowed
 --
 -- See Note [Pattern signature binders and scoping] in GHC.Hs.Type
-rnHsPatSigType scoping ctx inf_err sig_ty thing_inside
+rnHsPatSigType scoping ctx sig_ty thing_inside
   = do { ty_sig_okay <- xoptM LangExt.ScopedTypeVariables
        ; checkErr ty_sig_okay (unexpectedPatSigTypeErr sig_ty)
-       ; rn_hs_sig_wc_type scoping ctx inf_err (hsPatSigType sig_ty) $
+       ; rn_hs_sig_wc_type scoping ctx (hsPatSigType sig_ty) $
          \nwcs imp_tvs body ->
     do { let sig_names = HsPSRn { hsps_nwcs = nwcs, hsps_imp_tvs = imp_tvs }
              sig_ty'   = HsPS { hsps_ext = sig_names, hsps_body = body }
@@ -158,16 +154,15 @@ rnHsPatSigType scoping ctx inf_err sig_ty thing_inside
        } }
 
 -- The workhorse for rnHsSigWcType and rnHsPatSigType.
-rn_hs_sig_wc_type :: HsSigWcTypeScoping -> HsDocContext -> Maybe SDoc
+rn_hs_sig_wc_type :: HsSigWcTypeScoping -> HsDocContext
                   -> LHsType GhcPs
                   -> ([Name]    -- Wildcard names
                       -> [Name] -- Implicitly bound type variable names
                       -> LHsType GhcRn
                       -> RnM (a, FreeVars))
                   -> RnM (a, FreeVars)
-rn_hs_sig_wc_type scoping ctxt inf_err hs_ty thing_inside
-  = do { check_inferred_vars ctxt inf_err hs_ty
-       ; free_vars <- filterInScopeM (extractHsTyRdrTyVars hs_ty)
+rn_hs_sig_wc_type scoping ctxt hs_ty thing_inside
+  = do { free_vars <- filterInScopeM (extractHsTyRdrTyVars hs_ty)
        ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
        ; implicit_bndrs <- case scoping of
@@ -318,17 +313,13 @@ of the HsWildCardBndrs structure, and we are done.
 
 rnHsSigType :: HsDocContext
             -> TypeOrKind
-            -> Maybe SDoc
-            -- ^ The error msg if the signature is not allowed to contain
-            --   manually written inferred variables.
             -> LHsSigType GhcPs
             -> RnM (LHsSigType GhcRn, FreeVars)
 -- Used for source-language type signatures
 -- that cannot have wildcards
-rnHsSigType ctx level inf_err (HsIB { hsib_body = hs_ty })
+rnHsSigType ctx level (HsIB { hsib_body = hs_ty })
   = do { traceRn "rnHsSigType" (ppr hs_ty)
        ; rdr_env <- getLocalRdrEnv
-       ; check_inferred_vars ctx inf_err hs_ty
        ; vars0 <- forAllOrNothing (isLHsForAllTy hs_ty)
            $ filterInScope rdr_env
            $ extractHsTyRdrTyVars hs_ty
@@ -415,26 +406,6 @@ type signature, since the type signature implicitly carries their binding
 sites. This is less precise, but more accurate.
 -}
 
-check_inferred_vars :: HsDocContext
-                    -> Maybe SDoc
-                    -- ^ The error msg if the signature is not allowed to contain
-                    --   manually written inferred variables.
-                    -> LHsType GhcPs
-                    -> RnM ()
-check_inferred_vars _    Nothing    _  = return ()
-check_inferred_vars ctxt (Just msg) ty =
-  let bndrs = forallty_bndrs ty
-  in case find ((==) InferredSpec . hsTyVarBndrFlag) bndrs of
-    Nothing -> return ()
-    Just _  -> addErr $ withHsDocContext ctxt msg
-  where
-    forallty_bndrs :: LHsType GhcPs -> [HsTyVarBndr Specificity GhcPs]
-    forallty_bndrs (L _ ty) = case ty of
-      HsParTy _ ty' -> forallty_bndrs ty'
-      HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }}
-                    -> map unLoc tvs
-      _             -> []
-
 {- ******************************************************
 *                                                       *
            LHsType and HsType


=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -34,7 +34,8 @@ import GHC.Rename.Utils ( HsDocContext(..), mapFvRn, bindLocalNames
                         , checkDupRdrNames, bindLocalNamesFV
                         , checkShadowedRdrNames, warnUnusedTypePatterns
                         , extendTyVarEnvFVRn, newLocalBndrsRn
-                        , withHsDocContext )
+                        , withHsDocContext, noNestedForallsContextsErr
+                        , addNoNestedForallsContextsErr, checkInferredVars )
 import GHC.Rename.Unbound ( mkUnboundName, notInScopeErr )
 import GHC.Rename.Names
 import GHC.Rename.Doc   ( rnHsDoc, rnMbLHsDoc )
@@ -65,7 +66,6 @@ import GHC.Data.List.SetOps ( findDupsEq, removeDups, equivClasses )
 import GHC.Data.Graph.Directed ( SCC, flattenSCC, flattenSCCs, Node(..)
                                , stronglyConnCompFromEdgedVerticesUniq )
 import GHC.Types.Unique.Set
-import GHC.Data.Maybe ( whenIsJust )
 import GHC.Data.OrdList
 import qualified GHC.LanguageExtensions as LangExt
 
@@ -371,7 +371,7 @@ rnHsForeignDecl :: ForeignDecl GhcPs -> RnM (ForeignDecl GhcRn, FreeVars)
 rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec })
   = do { topEnv :: HscEnv <- getTopEnv
        ; name' <- lookupLocatedTopBndrRn name
-       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel Nothing ty
+       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty
 
         -- Mark any PackageTarget style imports as coming from the current package
        ; let unitId = homeUnit $ hsc_dflags topEnv
@@ -383,7 +383,7 @@ rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec })
 
 rnHsForeignDecl (ForeignExport { fd_name = name, fd_sig_ty = ty, fd_fe = spec })
   = do { name' <- lookupLocatedOccRn name
-       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel Nothing ty
+       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty
        ; return (ForeignExport { fd_e_ext = noExtField
                                , fd_name = name', fd_sig_ty = ty'
                                , fd_fe = spec }
@@ -602,13 +602,14 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
                            , cid_sigs = uprags, cid_tyfam_insts = ats
                            , cid_overlap_mode = oflag
                            , cid_datafam_insts = adts })
-  = do { (inst_ty', inst_fvs) <- rnHsSigType ctxt TypeLevel inf_err inst_ty
+  = do { checkInferredVars ctxt inf_err inst_ty
+       ; (inst_ty', inst_fvs) <- rnHsSigType ctxt TypeLevel inst_ty
        ; let (ktv_names, _, head_ty') = splitLHsInstDeclTy inst_ty'
              -- Check if there are any nested `forall`s or contexts, which are
              -- illegal in the type of an instance declaration (see
              -- Note [No nested foralls or contexts in instance types] in
              -- GHC.Hs.Type)...
-             mb_nested_msg = no_nested_foralls_contexts_err
+             mb_nested_msg = noNestedForallsContextsErr
                                (text "Instance head") head_ty'
              -- ...then check if the instance head is actually headed by a
              -- class type constructor...
@@ -1010,22 +1011,22 @@ rnSrcDerivDecl :: DerivDecl GhcPs -> RnM (DerivDecl GhcRn, FreeVars)
 rnSrcDerivDecl (DerivDecl _ ty mds overlap)
   = do { standalone_deriv_ok <- xoptM LangExt.StandaloneDeriving
        ; unless standalone_deriv_ok (addErr standaloneDerivErr)
-       ; (mds', ty', fvs)
-           <- rnLDerivStrategy ctxt mds $ rnHsSigWcType ctxt inf_err ty
+       ; checkInferredVars ctxt inf_err nowc_ty
+       ; (mds', ty', fvs) <- rnLDerivStrategy ctxt mds $ rnHsSigWcType ctxt ty
          -- Check if there are any nested `forall`s or contexts, which are
          -- illegal in the type of an instance declaration (see
          -- Note [No nested foralls or contexts in instance types] in
          -- GHC.Hs.Type).
-       ; whenIsJust (no_nested_foralls_contexts_err
-                       (text "Standalone-derived instance head")
-                       (getLHsInstDeclHead $ dropWildCards ty')) $ \(l, err_msg) ->
-           addErrAt l $ withHsDocContext ctxt err_msg
+       ; addNoNestedForallsContextsErr ctxt
+           (text "Standalone-derived instance head")
+           (getLHsInstDeclHead $ dropWildCards ty')
        ; warnNoDerivStrat mds' loc
        ; return (DerivDecl noExtField ty' mds' overlap, fvs) }
   where
     ctxt    = DerivDeclCtx
     inf_err = Just (text "Inferred type variables are not allowed")
-    loc = getLoc $ hsib_body $ hswc_body ty
+    loc = getLoc $ hsib_body nowc_ty
+    nowc_ty = dropWildCards ty
 
 standaloneDerivErr :: SDoc
 standaloneDerivErr
@@ -1091,7 +1092,7 @@ bindRuleTmVars doc tyvs vars names thing_inside
 
     go ((L l (RuleBndrSig _ (L loc _) bsig)) : vars)
        (n : ns) thing_inside
-      = rnHsPatSigType bind_free_tvs doc Nothing bsig $ \ bsig' ->
+      = rnHsPatSigType bind_free_tvs doc bsig $ \ bsig' ->
         go vars ns $ \ vars' ->
         thing_inside (L l (RuleBndrSig noExtField (L loc n) bsig') : vars')
 
@@ -1431,7 +1432,7 @@ rnStandaloneKindSignature tc_names (StandaloneKindSig _ v ki)
         ; unless standalone_ki_sig_ok $ addErr standaloneKiSigErr
         ; new_v <- lookupSigCtxtOccRn (TopSigCtxt tc_names) (text "standalone kind signature") v
         ; let doc = StandaloneKindSigCtx (ppr v)
-        ; (new_ki, fvs) <- rnHsSigType doc KindLevel Nothing ki
+        ; (new_ki, fvs) <- rnHsSigType doc KindLevel ki
         ; return (StandaloneKindSig noExtField new_v new_ki, fvs)
         }
   where
@@ -1841,15 +1842,14 @@ rnLHsDerivingClause doc
     rn_clause_pred :: LHsSigType GhcPs -> RnM (LHsSigType GhcRn, FreeVars)
     rn_clause_pred pred_ty = do
       let inf_err = Just (text "Inferred type variables are not allowed")
-      ret@(pred_ty', _) <- rnHsSigType doc TypeLevel inf_err pred_ty
+      checkInferredVars doc inf_err pred_ty
+      ret@(pred_ty', _) <- rnHsSigType doc TypeLevel pred_ty
       -- Check if there are any nested `forall`s, which are illegal in a
       -- `deriving` clause.
       -- See Note [No nested foralls or contexts in instance types]
       -- (Wrinkle: Derived instances) in GHC.Hs.Type.
-      whenIsJust (no_nested_foralls_contexts_err
-                    (text "Derived class type")
-                    (getLHsInstDeclHead pred_ty')) $ \(l, err_msg) ->
-            addErrAt l $ withHsDocContext doc err_msg
+      addNoNestedForallsContextsErr doc (text "Derived class type")
+        (getLHsInstDeclHead pred_ty')
       pure ret
 
 rnLDerivStrategy :: forall a.
@@ -1883,7 +1883,8 @@ rnLDerivStrategy doc mds thing_inside
         AnyclassStrategy -> boring_case AnyclassStrategy
         NewtypeStrategy  -> boring_case NewtypeStrategy
         ViaStrategy via_ty ->
-          do (via_ty', fvs1) <- rnHsSigType doc TypeLevel inf_err via_ty
+          do checkInferredVars doc inf_err via_ty
+             (via_ty', fvs1) <- rnHsSigType doc TypeLevel via_ty
              let HsIB { hsib_ext  = via_imp_tvs
                       , hsib_body = via_body } = via_ty'
                  (via_exp_tv_bndrs, via_rho) = splitLHsForAllTyInvis_KP via_body
@@ -1893,10 +1894,8 @@ rnLDerivStrategy doc mds thing_inside
              -- `via` type.
              -- See Note [No nested foralls or contexts in instance types]
              -- (Wrinkle: Derived instances) in GHC.Hs.Type.
-             whenIsJust (no_nested_foralls_contexts_err
-                           (quotes (text "via") <+> text "type")
-                           via_rho) $ \(l, err_msg) ->
-               addErrAt l $ withHsDocContext doc err_msg
+             addNoNestedForallsContextsErr doc
+               (quotes (text "via") <+> text "type") via_rho
              (thing, fvs2) <- extendTyVarEnvFVRn via_tvs thing_inside
              pure (ViaStrategy via_ty', thing, fvs1 `plusFV` fvs2)
 
@@ -2211,7 +2210,7 @@ rnConDecl (XConDecl (ConDeclGADTPrefixPs { con_gp_names = names, con_gp_ty = ty
        ; mb_doc'   <- rnMbLHsDoc mb_doc
 
        ; let ctxt = ConDeclCtx new_names
-       ; (ty', fvs) <- rnHsSigType ctxt TypeLevel Nothing ty
+       ; (ty', fvs) <- rnHsSigType ctxt TypeLevel ty
        ; linearTypes <- xopt LangExt.LinearTypes <$> getDynFlags
 
          -- Now that operator precedence has been resolved, we can split the
@@ -2230,10 +2229,8 @@ rnConDecl (XConDecl (ConDeclGADTPrefixPs { con_gp_names = names, con_gp_ty = ty
          -- Ensure that there are no nested `forall`s or contexts, per
          -- Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)
          -- in GHC.Hs.Type.
-       ; whenIsJust (no_nested_foralls_contexts_err
-                       (text "GADT constructor type signature")
-                       res_ty) $ \(l, err_msg) ->
-           addErrAt l $ withHsDocContext ctxt err_msg
+       ; addNoNestedForallsContextsErr ctxt
+           (text "GADT constructor type signature") res_ty
 
        ; traceRn "rnConDecl (ConDeclGADTPrefixPs)"
            (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
@@ -2271,41 +2268,6 @@ rnConDeclDetails con doc (RecCon (L l fields))
                 -- since that is done by GHC.Rename.Names.extendGlobalRdrEnvRn
         ; return (RecCon (L l new_fields), fvs) }
 
--- | Examines a non-outermost type for @forall at s or contexts, which are assumed
--- to be nested. Returns @'Just' err_msg@ if such a @forall@ or context is
--- found, and returns @Nothing@ otherwise.
---
--- This is currently used in two places:
---
--- * In GADT constructor types (in 'rnConDecl').
---   See @Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)@
---   in "GHC.Hs.Type".
---
--- * In instance declaration types (in 'rnClsIntDecl' and 'rnSrcDerivDecl').
---   See @Note [No nested foralls or contexts in instance types]@ in
---   "GHC.Hs.Type".
-no_nested_foralls_contexts_err :: SDoc -> LHsType GhcRn -> Maybe (SrcSpan, SDoc)
-no_nested_foralls_contexts_err what lty =
-  case ignoreParens lty of
-    L l (HsForAllTy { hst_tele = tele })
-      |  HsForAllVis{} <- tele
-         -- The only two places where this function is called correspond to
-         -- types of terms, so we give a slightly more descriptive error
-         -- message in the event that they contain visible dependent
-         -- quantification (currently only allowed in kinds).
-      -> Just (l, vcat [ text "Illegal visible, dependent quantification" <+>
-                         text "in the type of a term"
-                       , text "(GHC does not yet support this)" ])
-      |  HsForAllInvis{} <- tele
-      -> Just (l, nested_foralls_contexts_err)
-    L l (HsQualTy {})
-      -> Just (l, nested_foralls_contexts_err)
-    _ -> Nothing
-  where
-    nested_foralls_contexts_err =
-      what <+> text "cannot contain nested"
-      <+> quotes forAllLit <> text "s or contexts"
-
 -------------------------------------------------
 
 -- | Brings pattern synonym names and also pattern synonym selectors


=====================================
compiler/GHC/Rename/Pat.hs
=====================================
@@ -412,7 +412,7 @@ rnPatAndThen mk (SigPat x pat sig)
        ; return (SigPat x pat' sig' ) }
   where
     rnHsPatSigTypeAndThen :: HsPatSigType GhcPs -> CpsRn (HsPatSigType GhcRn)
-    rnHsPatSigTypeAndThen sig = CpsRn (rnHsPatSigType AlwaysBind PatCtx Nothing sig)
+    rnHsPatSigTypeAndThen sig = CpsRn (rnHsPatSigType AlwaysBind PatCtx sig)
 
 rnPatAndThen mk (LitPat x lit)
   | HsString src s <- lit


=====================================
compiler/GHC/Rename/Utils.hs
=====================================
@@ -26,8 +26,10 @@ module GHC.Rename.Utils (
 
         bindLocalNames, bindLocalNamesFV,
 
-        addNameClashErrRn, extendTyVarEnvFVRn
+        addNameClashErrRn, extendTyVarEnvFVRn,
 
+        checkInferredVars,
+        noNestedForallsContextsErr, addNoNestedForallsContextsErr
 )
 
 where
@@ -35,6 +37,7 @@ where
 
 import GHC.Prelude
 
+import GHC.Core.Type
 import GHC.Hs
 import GHC.Types.Name.Reader
 import GHC.Driver.Types
@@ -49,6 +52,7 @@ import GHC.Utils.Outputable
 import GHC.Utils.Misc
 import GHC.Types.Basic  ( TopLevelFlag(..) )
 import GHC.Data.List.SetOps ( removeDups )
+import GHC.Data.Maybe ( whenIsJust )
 import GHC.Driver.Session
 import GHC.Data.FastString
 import Control.Monad
@@ -176,6 +180,137 @@ checkShadowedOccs (global_env,local_env) get_loc_occ ns
                              || xopt LangExt.RecordWildCards dflags) }
     is_shadowed_gre _other = return True
 
+-------------------------------------
+-- | Throw an error message if a user attempts to quantify an inferred type
+-- variable in a place where specificity cannot be observed.
+-- See @Note [Unobservably inferred type variables]@.
+checkInferredVars :: HsDocContext
+                  -> Maybe SDoc
+                  -- ^ The error msg if the signature is not allowed to contain
+                  --   manually written inferred variables.
+                  -> LHsSigType GhcPs
+                  -> RnM ()
+checkInferredVars _    Nothing    _  = return ()
+checkInferredVars ctxt (Just msg) ty =
+  let bndrs = forallty_bndrs (hsSigType ty)
+  in case find ((==) InferredSpec . hsTyVarBndrFlag) bndrs of
+    Nothing -> return ()
+    Just _  -> addErr $ withHsDocContext ctxt msg
+  where
+    forallty_bndrs :: LHsType GhcPs -> [HsTyVarBndr Specificity GhcPs]
+    forallty_bndrs (L _ ty) = case ty of
+      HsParTy _ ty' -> forallty_bndrs ty'
+      HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }}
+                    -> map unLoc tvs
+      _             -> []
+
+{-
+Note [Unobservably inferred type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+While GHC's parser allows the use of inferred type variables
+(e.g., `forall {a}. <...>`) just about anywhere that type variable binders can
+appear, there are some situations where the distinction between inferred and
+specified type variables cannot be observed. For example, consider this
+instance declaration:
+
+  instance forall {a}. Eq (T a) where ...
+
+Making {a} inferred is essentially pointless, as there is no way for user code
+to "apply" an instance declaration in a way where the inferred/specified
+distinction would make a difference. Anyone who writes such code is likely
+confused, so in an attempt to be helpful, we throw an error message if a user
+writes code like this. The checkInferredVars function is responsible for
+implementing this restriction.
+
+It turns out to be somewhat cumbersome to enforce this restriction in certain
+cases. Ultimately, nothing goes wrong if this restriction is *not* enforced (as
+it is simply a suggestion to the user to think twice about how they quantify
+their type variables), so we only use checkInferredVars in places where it is
+feasible to do so. Two examples of places where it is *not* feasible are:
+
+* Quantified constraints. In the type `f :: (forall {a}. C a) => Proxy Int`,
+  there is no way to observe that {a} is inferred. Nevertheless, actually
+  rejecting this code would be tricky, as we would need to reject
+  `forall {a}. <...>` as a constraint but *accept* other uses of
+  `forall {a}. <...>` as a type (e.g., `g :: (forall {a}. a -> a) -> b -> b`).
+  This is quite tedious to do in practice, so we don't bother.
+* Default method type signatures (#18432). These are tricky because inferred
+  type variables can appear nested, e.g.,
+
+    class C a where
+      m         :: forall b. a -> b -> forall c.   c -> c
+      default m :: forall b. a -> b -> forall {c}. c -> c
+      m _ _ = id
+
+  Robustly checking for nested, inferred type variables ends up being a pain,
+  so we don't try to do this.
+
+Since nested type variables are a pain, one might wonder if they end up being
+painful for other places where we *do* enforce this restriction. The answer is
+"no", as it turns out. This is because in every other place where the
+restriction is enforced, GHC bans the use of nested `forall`s already. For
+example, GHC would not accept the following:
+
+  instance forall a. forall {b}. Eq (Either a b) where ...
+
+The fact that GHC does not permit nested `forall`s there is a bit of a
+coincidence (see Note [No nested foralls or contexts in instance types] in
+GHC.Hs.Type). But is sure is a useful coincidence, and one that we take
+advantage of. Because nested `forall`s are banned, checking for inferred
+type variables in instance declarations is as simple as peeling off the
+outer `forall`s and checking if any of them are inferred.
+-}
+
+-- | Examines a non-outermost type for @forall at s or contexts, which are assumed
+-- to be nested. For example, in the following declaration:
+--
+-- @
+-- instance forall a. forall b. C (Either a b)
+-- @
+--
+-- The outermost @forall a@ is fine, but the nested @forall b@ is not. We
+-- invoke 'noNestedForallsContextsErr' on the type @forall b. C (Either a b)@
+-- to catch the nested @forall@ and create a suitable error message.
+-- 'noNestedForallsContextsErr' returns @'Just' err_msg@ if such a @forall@ or
+-- context is found, and returns @Nothing@ otherwise.
+--
+-- This is currently used in the following places:
+--
+-- * In GADT constructor types (in 'rnConDecl').
+--   See @Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)@
+--   in "GHC.Hs.Type".
+--
+-- * In instance declaration types (in 'rnClsIntDecl' and 'rnSrcDerivDecl' in
+--   "GHC.Rename.Module" and 'renameSig' in "GHC.Rename.Bind").
+--   See @Note [No nested foralls or contexts in instance types]@ in
+--   "GHC.Hs.Type".
+noNestedForallsContextsErr :: SDoc -> LHsType GhcRn -> Maybe (SrcSpan, SDoc)
+noNestedForallsContextsErr what lty =
+  case ignoreParens lty of
+    L l (HsForAllTy { hst_tele = tele })
+      |  HsForAllVis{} <- tele
+         -- The only two places where this function is called correspond to
+         -- types of terms, so we give a slightly more descriptive error
+         -- message in the event that they contain visible dependent
+         -- quantification (currently only allowed in kinds).
+      -> Just (l, vcat [ text "Illegal visible, dependent quantification" <+>
+                         text "in the type of a term"
+                       , text "(GHC does not yet support this)" ])
+      |  HsForAllInvis{} <- tele
+      -> Just (l, nested_foralls_contexts_err)
+    L l (HsQualTy {})
+      -> Just (l, nested_foralls_contexts_err)
+    _ -> Nothing
+  where
+    nested_foralls_contexts_err =
+      what <+> text "cannot contain nested"
+      <+> quotes forAllLit <> text "s or contexts"
+
+-- | A common way to invoke 'noNestedForallsContextsErr'.
+addNoNestedForallsContextsErr :: HsDocContext -> SDoc -> LHsType GhcRn -> RnM ()
+addNoNestedForallsContextsErr ctxt what lty =
+  whenIsJust (noNestedForallsContextsErr what lty) $ \(l, err_msg) ->
+    addErrAt l $ withHsDocContext ctxt err_msg
 
 {-
 ************************************************************************


=====================================
testsuite/tests/quantified-constraints/T18432.hs
=====================================
@@ -0,0 +1,10 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+module Bug where
+
+import Data.Proxy
+
+class C a where
+  m :: Proxy a
+
+f :: (forall {a}. C a) => Proxy Int
+f = m


=====================================
testsuite/tests/quantified-constraints/all.T
=====================================
@@ -29,3 +29,4 @@ test('T17267c', normal, compile_fail, [''])
 test('T17267d', normal, compile_and_run, [''])
 test('T17267e', normal, compile_fail, [''])
 test('T17458', normal, compile_fail, [''])
+test('T18432', normal, compile, [''])


=====================================
testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.hs → testsuite/tests/typecheck/should_compile/ExplicitSpecificity4.hs
=====================================


=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -712,6 +712,7 @@ test('T18129', expect_broken(18129), compile, [''])
 test('T18185', normal, compile, [''])
 test('ExplicitSpecificityA1', normal, compile, [''])
 test('ExplicitSpecificityA2', normal, compile, [''])
+test('ExplicitSpecificity4', normal, compile, [''])
 test('T17775-viewpats-a', normal, compile, [''])
 test('T17775-viewpats-b', normal, compile_fail, [''])
 test('T17775-viewpats-c', normal, compile_fail, [''])


=====================================
testsuite/tests/typecheck/should_fail/T18455.hs
=====================================
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes #-}
+module T18455 where
+
+class C a
+
+instance C (Either a b) where
+  {-# SPECIALISE instance forall a. forall b. C (Either a b) #-}


=====================================
testsuite/tests/typecheck/should_fail/T18455.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T18455.hs:7:37: error:
+    SPECIALISE instance type cannot contain nested ‘forall’s or contexts
+    In a SPECIALISE instance pragma


=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -568,7 +568,6 @@ test('T18127a', normal, compile_fail, [''])
 test('ExplicitSpecificity1', normal, compile_fail, [''])
 test('ExplicitSpecificity2', normal, compile_fail, [''])
 test('ExplicitSpecificity3', normal, compile_fail, [''])
-test('ExplicitSpecificity4', normal, compile_fail, [''])
 test('ExplicitSpecificity5', normal, compile_fail, [''])
 test('ExplicitSpecificity6', normal, compile_fail, [''])
 test('ExplicitSpecificity7', normal, compile_fail, [''])
@@ -578,3 +577,4 @@ test('ExplicitSpecificity10', normal, compile_fail, [''])
 test('T18357', normal, compile_fail, [''])
 test('T18357a', normal, compile_fail, [''])
 test('T18357b', normal, compile_fail, [''])
+test('T18455', normal, compile_fail, [''])



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/360112d81e46d1d4bee280b281ce6742bc0db205

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/360112d81e46d1d4bee280b281ce6742bc0db205
You're receiving this email because of your account on gitlab.haskell.org.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200717/71e3cc63/attachment-0001.html>


More information about the ghc-commits mailing list