Commit 01c948eb authored by Ryan Scott's avatar Ryan Scott Committed by Marge Bot

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.
parent 502de556
Pipeline #22812 passed with stages
in 475 minutes and 49 seconds
......@@ -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
-----
......
......@@ -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"
......
......@@ -317,7 +317,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) }
......
......@@ -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
......
This diff is collapsed.
......@@ -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
......
......@@ -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,136 @@ 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. For example,
-- @forall {a}. [a] -> [a]@ would be rejected to the inferred type variable
-- @{a}@, but @forall a. [a] -> [a]@ would be accepted.
-- 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 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. (Notably, there is no opportunity
for visible type application of an instance declaration.) Anyone who
writes such code is likely confused, so in an attempt to be helpful,
we emit 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. Specifically:
* 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.
For now, we simply allow inferred quantifiers to be specified here,
even though doing so is pointless. All we lose is a warning.
Aside from the places where we already use checkInferredVars, most of
the other places where inferred vars don't make sense are in any case
already prohibited from having foralls /at all/. For example:
instance forall a. forall {b}. Eq (Either a b) where ...
Here the nested `forall {b}` is already prohibited. (See
Note [No nested foralls or contexts in instance types] in GHC.Hs.Type).
-}
-- | Examines a non-outermost type for @forall@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
{-
************************************************************************
......
{-# LANGUAGE QuantifiedConstraints #-}
module Bug where
import Data.Proxy
class C a where
m :: Proxy a
f :: (forall {a}. C a) => Proxy Int
f = m
......@@ -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, [''])
......@@ -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, [''])
......
{-# LANGUAGE RankNTypes #-}
module T18455 where
class C a
instance C (Either a b) where
{-# SPECIALISE instance forall a. forall b. C (Either a b) #-}
T18455.hs:7:37: error:
SPECIALISE instance type cannot contain nested ‘forall’s or contexts
In a SPECIALISE instance pragma
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment