[Git][ghc/ghc][wip/T18126] 3 commits: QL wibbles following RAE review
Simon Peyton Jones
gitlab at gitlab.haskell.org
Mon Sep 14 12:17:31 UTC 2020
Simon Peyton Jones pushed to branch wip/T18126 at Glasgow Haskell Compiler / GHC
Commits:
c707d999 by Simon Peyton Jones at 2020-09-14T13:12:05+01:00
QL wibbles following RAE review
- - - - -
2e5c372a by Simon Peyton Jones at 2020-09-14T13:15:33+01:00
QL wibbles following RAE review
- - - - -
4c56d0af by Simon Peyton Jones at 2020-09-14T13:16:50+01:00
wibbles generalilsation
- - - - -
14 changed files:
- compiler/GHC/Tc/Gen/App.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Expr.hs-boot
- compiler/GHC/Tc/Gen/Head.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Module.hs
- compiler/GHC/Tc/Solver.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- docs/users_guide/exts/impredicative_types.rst
- docs/users_guide/ghci.rst
- testsuite/tests/impredicative/all.T
- + testsuite/tests/impredicative/expr-sig.hs
Changes:
=====================================
compiler/GHC/Tc/Gen/App.hs
=====================================
@@ -102,7 +102,7 @@ tcInferSigma inst (L loc rn_expr)
= addExprCtxt rn_expr $
setSrcSpan loc $
do { do_ql <- wantQuickLook rn_fun
- ; (tc_fun, fun_sigma) <- tcInferAppHead rn_fun rn_args
+ ; (tc_fun, fun_sigma) <- tcInferAppHead rn_fun rn_args Nothing
; (_delta, inst_args, app_res_sigma) <- tcInstFun do_ql inst rn_fun fun_sigma rn_args
; _tc_args <- tcValArgs do_ql tc_fun inst_args
; return app_res_sigma }
@@ -133,7 +133,10 @@ head ::= f -- HsVar: variables
When tcExpr sees something that starts an application chain (namely,
any of the constructors in 'app' or 'head'), it invokes tcApp to
-typecheck it: see Note [tcApp: typechecking applications].
+typecheck it: see Note [tcApp: typechecking applications]. However,
+for HsPar and HsPragE, there is no tcWrapResult (which would
+instantiate types, bypassing Quick Look), so nothing is gained by
+using the application chain route, and we can just recurse to tcExpr.
A "head" has three special cases (for which we can infer a polytype
using tcInferAppHead_maybe); otherwise is just any old expression (for
@@ -142,6 +145,14 @@ which we can infer a rho-type (via tcInfer).
There is no special treatment for HsUnboundVar, HsOverLit etc, because
we can't get a polytype from them.
+It may not be immediately obvious why ExprWithTySig (e::ty) should be
+dealt with by tcApp, even when it is not applied to anything. Consider
+ f :: [forall a. a->a] -> Int
+ ...(f (undefined :: forall b. b))...
+Clearly this should work! But it will /only/ work because if we
+instantiate that (forall b. b) impredicatively! And that only happens
+in tcApp.
+
Note [tcApp: typechecking applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
tcApp implements the APP-Downarrow/Uparrow rule of
@@ -211,6 +222,7 @@ tcApp :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
tcApp rn_expr exp_res_ty
| (rn_fun, rn_args, rebuild) <- splitHsApps rn_expr
= do { (tc_fun, fun_sigma) <- tcInferAppHead rn_fun rn_args
+ (checkingExpType_maybe exp_res_ty)
-- Instantiate
; do_ql <- wantQuickLook rn_fun
@@ -706,7 +718,7 @@ quickLookArg1 :: Bool -> Delta -> LHsExpr GhcRn -> TcSigmaType
quickLookArg1 guarded delta larg@(L loc arg) arg_ty
= setSrcSpan loc $
do { let (rn_fun,rn_args,rebuild) = splitHsApps arg
- ; mb_fun_ty <- tcInferAppHead_maybe rn_fun rn_args
+ ; mb_fun_ty <- tcInferAppHead_maybe rn_fun rn_args (Just arg_ty)
; traceTc "quickLookArg 1" $
vcat [ text "arg:" <+> ppr arg
, text "head:" <+> ppr rn_fun <+> dcolon <+> ppr mb_fun_ty
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -17,7 +17,7 @@ module GHC.Tc.Gen.Expr
( tcCheckPolyExpr, tcCheckPolyExprNC,
tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC,
tcInferRho, tcInferRhoNC,
- tcExpr, tcExprWithSig,
+ tcExpr,
tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,
tcCheckId,
addAmbiguousNameErr,
@@ -39,9 +39,7 @@ import GHC.Core.UsageEnv
import GHC.Tc.Utils.Instantiate
import GHC.Tc.Gen.App
import GHC.Tc.Gen.Head
-import GHC.Tc.Gen.Bind ( chooseInferredQuantifiers, tcLocalBinds )
-import GHC.Tc.Gen.Sig ( tcUserTypeSig, tcInstSig )
-import GHC.Tc.Solver ( simplifyInfer, InferMode(..) )
+import GHC.Tc.Gen.Bind ( tcLocalBinds )
import GHC.Tc.Instance.Family ( tcGetFamInstEnvs )
import GHC.Core.FamInstEnv ( FamInstEnvs )
import GHC.Rename.Env ( addUsedGRE )
@@ -63,7 +61,6 @@ import GHC.Types.Name.Env
import GHC.Types.Name.Set
import GHC.Types.Name.Reader
import GHC.Core.TyCon
-import GHC.Core.TyCo.Rep
import GHC.Core.Type
import GHC.Tc.Types.Evidence
import GHC.Types.Var.Set
@@ -183,9 +180,13 @@ tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
-- - HsVar: lone variables, to ensure that they can get an
-- impredicative instantiation (via Quick Look
-- driven by res_ty (in checking mode).
-tcExpr e@(HsVar {}) res_ty = tcApp e res_ty
-tcExpr e@(HsApp {}) res_ty = tcApp e res_ty
-tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty
+-- - ExprWithTySig: (e :: type)
+-- See Note [Application chains and heads] in GHC.Tc.Gen.App
+tcExpr e@(HsVar {}) res_ty = tcApp e res_ty
+tcExpr e@(HsApp {}) res_ty = tcApp e res_ty
+tcExpr e@(HsAppType {}) res_ty = tcApp e res_ty
+tcExpr e@(ExprWithTySig {}) res_ty = tcApp e res_ty
+tcExpr e@(HsRecFld {}) res_ty = tcApp e res_ty
-- Typecheck an occurrence of an unbound Id
--
@@ -287,10 +288,6 @@ tcExpr e@(HsLamCase x matches) res_ty
, text "requires"]
match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody }
-tcExpr e@(ExprWithTySig _ expr hs_ty) res_ty
- = do { (expr', poly_ty) <- tcExprWithSig expr hs_ty
- ; tcWrapResult e expr' poly_ty res_ty }
-
{-
Note [Type-checking overloaded labels]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -910,8 +907,6 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
; tcWrapResult expr expr' rec_res_ty res_ty }
-tcExpr e@(HsRecFld _ f) res_ty
- = tcCheckRecSelId e f res_ty
{-
************************************************************************
@@ -1066,7 +1061,9 @@ tcSyntaxOpGen :: CtOrigin
-> ([TcSigmaType] -> [Mult] -> TcM a)
-> TcM (a, SyntaxExprTc)
tcSyntaxOpGen orig (SyntaxExprRn op) arg_tys res_ty thing_inside
- = do { (expr, sigma) <- tcInferAppHead op []
+ = do { (expr, sigma) <- tcInferAppHead op [] Nothing
+ -- Nothing here might be improved, but all this
+ -- code is scheduled for demolition anyway
; traceTc "tcSyntaxOpGen" (ppr op $$ ppr expr $$ ppr sigma)
; (result, expr_wrap, arg_wraps, res_wrap)
<- tcSynArgA orig sigma arg_tys res_ty $
@@ -1239,99 +1236,6 @@ Here's an example where it actually makes a real difference
With the change, f1 will type-check, because the 'Char' info from
the signature is propagated into MkQ's argument. With the check
in the other order, the extra signature in f2 is reqd.
-
-************************************************************************
-* *
- Expressions with a type signature
- expr :: type
-* *
-********************************************************************* -}
-
-tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn)
- -> TcM (HsExpr GhcTc, TcSigmaType)
-tcExprWithSig expr hs_ty
- = do { sig_info <- checkNoErrs $ -- Avoid error cascade
- tcUserTypeSig loc hs_ty Nothing
- ; (expr', poly_ty) <- tcExprSig expr sig_info
- ; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) }
- where
- loc = getLoc (hsSigWcType hs_ty)
-
-tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
-tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
- = setSrcSpan loc $ -- Sets the location for the implication constraint
- do { let poly_ty = idType poly_id
- ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty ->
- tcCheckMonoExprNC expr rho_ty
- ; return (mkLHsWrap wrap expr', poly_ty) }
-
-tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
- = setSrcSpan loc $ -- Sets the location for the implication constraint
- do { (tclvl, wanted, (expr', sig_inst))
- <- pushLevelAndCaptureConstraints $
- do { sig_inst <- tcInstSig sig
- ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $
- tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $
- tcCheckPolyExprNC expr (sig_inst_tau sig_inst)
- ; return (expr', sig_inst) }
- -- See Note [Partial expression signatures]
- ; let tau = sig_inst_tau sig_inst
- infer_mode | null (sig_inst_theta sig_inst)
- , isNothing (sig_inst_wcx sig_inst)
- = ApplyMR
- | otherwise
- = NoRestrictions
- ; (qtvs, givens, ev_binds, residual, _)
- <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
- ; emitConstraints residual
-
- ; tau <- zonkTcType tau
- ; let inferred_theta = map evVarPred givens
- tau_tvs = tyCoVarsOfType tau
- ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta
- tau_tvs qtvs (Just sig_inst)
- ; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau
- my_sigma = mkInvisForAllTys binders (mkPhiTy my_theta tau)
- ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis.
- then return idHsWrapper -- Fast path; also avoids complaint when we infer
- -- an ambiguous type and have AllowAmbiguousType
- -- e..g infer x :: forall a. F a -> Int
- else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma
-
- ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
- ; let poly_wrap = wrap
- <.> mkWpTyLams qtvs
- <.> mkWpLams givens
- <.> mkWpLet ev_binds
- ; return (mkLHsWrap poly_wrap expr', my_sigma) }
-
-
-{- Note [Partial expression signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Partial type signatures on expressions are easy to get wrong. But
-here is a guiding principile
- e :: ty
-should behave like
- let x :: ty
- x = e
- in x
-
-So for partial signatures we apply the MR if no context is given. So
- e :: IO _ apply the MR
- e :: _ => IO _ do not apply the MR
-just like in GHC.Tc.Gen.Bind.decideGeneralisationPlan
-
-This makes a difference (#11670):
- peek :: Ptr a -> IO CLong
- peek ptr = peekElemOff undefined 0 :: _
-from (peekElemOff undefined 0) we get
- type: IO w
- constraints: Storable w
-
-We must NOT try to generalise over 'w' because the signature specifies
-no constraints so we'll complain about not being able to solve
-Storable w. Instead, don't generalise; then _ gets instantiated to
-CLong, as it should.
-}
{- *********************************************************************
=====================================
compiler/GHC/Tc/Gen/Expr.hs-boot
=====================================
@@ -1,11 +1,11 @@
module GHC.Tc.Gen.Expr where
import GHC.Hs ( HsExpr, LHsExpr, SyntaxExprRn
- , SyntaxExprTc, LHsSigWcType )
+ , SyntaxExprTc )
import GHC.Tc.Utils.TcType ( TcRhoType, TcSigmaType, SyntaxOpType, ExpType, ExpRhoType )
import GHC.Tc.Types ( TcM )
import GHC.Tc.Types.Origin ( CtOrigin )
import GHC.Core.Type ( Mult )
-import GHC.Hs.Extension ( GhcRn, GhcTc, NoGhcTc )
+import GHC.Hs.Extension ( GhcRn, GhcTc )
tcCheckPolyExpr, tcCheckPolyExprNC ::
LHsExpr GhcRn
@@ -23,9 +23,6 @@ tcCheckMonoExpr, tcCheckMonoExprNC ::
tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTc)
-tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn)
- -> TcM (HsExpr GhcTc, TcSigmaType)
-
tcInferRho, tcInferRhoNC ::
LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)
=====================================
compiler/GHC/Tc/Gen/Head.hs
=====================================
@@ -19,16 +19,18 @@ module GHC.Tc.Gen.Head
, tcInferAppHead, tcInferAppHead_maybe
, tcInferId, tcCheckId
- , tcCheckRecSelId
- , disambiguateSelector, obviousSig, addAmbiguousNameErr
+ , obviousSig, addAmbiguousNameErr
, tyConOf, tyConOfET, lookupParents, fieldNotInType
, notSelector, nonBidirectionalErr
, exprCtxt, addLExprCtxt, addExprCtxt, addFunResCtxt ) where
-import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcExprWithSig )
+import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcExpr, tcCheckMonoExprNC, tcCheckPolyExprNC )
-import GHC.Hs
+import GHC.Tc.Gen.HsType
+import GHC.Tc.Gen.Pat
+import GHC.Tc.Gen.Bind( chooseInferredQuantifiers )
+import GHC.Tc.Gen.Sig( tcUserTypeSig, tcInstSig )
import GHC.Tc.TyCl.PatSyn( patSynBuilderOcc )
import GHC.Tc.Utils.Monad
import GHC.Tc.Utils.Unify
@@ -39,13 +41,12 @@ import GHC.Core.FamInstEnv ( FamInstEnvs )
import GHC.Core.UsageEnv ( unitUE )
import GHC.Rename.Env ( addUsedGRE )
import GHC.Rename.Utils ( addNameClashErrRn, unknownSubordinateErr )
+import GHC.Tc.Solver ( InferMode(..), simplifyInfer )
import GHC.Tc.Utils.Env
-import GHC.Tc.Gen.HsType
-import GHC.Tc.Gen.Pat
-import GHC.Tc.Gen.Sig( isCompleteHsSig )
import GHC.Tc.Utils.TcMType
import GHC.Tc.Types.Origin
import GHC.Tc.Utils.TcType as TcType
+import GHC.Hs
import GHC.Types.Id
import GHC.Types.Id.Info
import GHC.Core.ConLike
@@ -317,7 +318,8 @@ pprHsExprArgTc arg = ppr arg
********************************************************************* -}
tcInferAppHead :: HsExpr GhcRn
- -> [HsExprArg 'TcpRn]
+ -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
+ -- These two args are solely for tcInferRecSelId
-> TcM (HsExpr GhcTc, TcSigmaType)
-- Infer type of the head of an application
-- i.e. the 'f' in (f e1 ... en)
@@ -339,26 +341,29 @@ tcInferAppHead :: HsExpr GhcRn
-- cases are dealt with by splitHsApps.
--
-- See Note [tcApp: typechecking applications] in GHC.Tc.Gen.App
-tcInferAppHead fun args
- = setSrcSpanFromArgs args $
- do { mb_tc_fun <- tcInferAppHead_maybe fun args
+tcInferAppHead fun args mb_res_ty
+ = setSrcSpanFromArgs args $
+ do { mb_tc_fun <- tcInferAppHead_maybe fun args mb_res_ty
; case mb_tc_fun of
Just (fun', fun_sigma) -> return (fun', fun_sigma)
- Nothing -> addExprCtxt fun $
- tcInfer (tcExpr fun) }
+ Nothing -> tcInfer (tcExpr fun) }
tcInferAppHead_maybe :: HsExpr GhcRn
- -> [HsExprArg 'TcpRn]
+ -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
+ -- These two args are solely for tcInferRecSelId
-> TcM (Maybe (HsExpr GhcTc, TcSigmaType))
-- Returns Nothing for a complicated head
-tcInferAppHead_maybe fun args
+tcInferAppHead_maybe fun args mb_res_ty
= case fun of
HsVar _ (L _ nm) -> Just <$> tcInferId nm
- HsRecFld _ f -> Just <$> tcInferRecSelId f args
- ExprWithTySig _ e hs_ty
- | isCompleteHsSig hs_ty -> addErrCtxt (exprCtxt fun) $
+ HsRecFld _ f -> Just <$> tcInferRecSelId f args mb_res_ty
+ ExprWithTySig _ e hs_ty -> add_ctxt $
Just <$> tcExprWithSig e hs_ty
_ -> return Nothing
+ where
+ add_ctxt thing_inside
+ | null args = thing_inside -- We havea already pushed the context
+ | otherwise = addExprCtxt fun thing_inside
{- *********************************************************************
@@ -456,40 +461,20 @@ non-obvious ways.
See also Note [HsRecField and HsRecUpdField] in GHC.Hs.Pat.
-}
-tcCheckRecSelId :: HsExpr GhcRn -> AmbiguousFieldOcc GhcRn
- -> ExpRhoType -> TcM (HsExpr GhcTc)
-tcCheckRecSelId rn_expr (Unambiguous sel_name lbl) res_ty
- = do { sel_id <- tc_rec_sel_id lbl sel_name
- ; let expr = HsRecFld noExtField (Unambiguous sel_id lbl)
- ; tcWrapResult rn_expr expr (idType sel_id) res_ty }
-tcCheckRecSelId rn_expr (Ambiguous _ lbl) res_ty
- = case tcSplitFunTy_maybe =<< checkingExpType_maybe res_ty of
- Nothing -> ambiguousSelector lbl
- Just (arg, _) -> do { sel_name <- disambiguateSelector lbl (scaledThing arg)
- ; sel_id <- tc_rec_sel_id lbl sel_name
- ; let expr = HsRecFld noExtField (Ambiguous sel_id lbl)
- ; tcWrapResult rn_expr expr (idType sel_id) res_ty }
-
-tcInferRecSelId :: AmbiguousFieldOcc GhcRn -> [HsExprArg 'TcpRn]
+tcInferRecSelId :: AmbiguousFieldOcc GhcRn
+ -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
-> TcM (HsExpr GhcTc, TcSigmaType)
--- Disgusting special case for ambiguous record selectors
-tcInferRecSelId (Ambiguous _ lbl) args
- | arg1 : _ <- dropWhile (not . isVisibleArg) args -- A value arg is first
- , EValArg { eva_arg = ValArg (L _ arg) } <- arg1
- , Just sig_ty <- obviousSig arg -- A type sig on the arg disambiguates
- = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty
- ; sel_name <- disambiguateSelector lbl sig_tc_ty
- ; sel_id <- tc_rec_sel_id lbl sel_name
- ; let expr = HsRecFld noExtField (Ambiguous sel_id lbl)
- ; return (expr, idType sel_id) }
- | otherwise
- = ambiguousSelector lbl
-
-tcInferRecSelId (Unambiguous sel_name lbl) _args
+tcInferRecSelId (Unambiguous sel_name lbl) _args _mb_res_ty
= do { sel_id <- tc_rec_sel_id lbl sel_name
; let expr = HsRecFld noExtField (Unambiguous sel_id lbl)
; return (expr, idType sel_id) }
+tcInferRecSelId (Ambiguous _ lbl) args mb_res_ty
+ = do { sel_name <- tcInferAmbiguousRecSelId lbl args mb_res_ty
+ ; sel_id <- tc_rec_sel_id lbl sel_name
+ ; let expr = HsRecFld noExtField (Ambiguous sel_id lbl)
+ ; return (expr, idType sel_id) }
+
------------------------
tc_rec_sel_id :: Located RdrName -> Name -> TcM TcId
-- Like tc_infer_id, but returns an Id not a HsExpr,
@@ -498,13 +483,11 @@ tc_rec_sel_id lbl sel_name
= do { thing <- tcLookup sel_name
; case thing of
ATcId { tct_id = id }
- -> do { check_naughty occ id -- Note [Local record selectors]
- ; checkThLocalId id
- ; tcEmitBindingUsage $ unitUE sel_name One
+ -> do { check_local_id occ id
; return id }
AGlobal (AnId id)
- -> do { check_naughty occ id
+ -> do { check_global_id occ id
; return id }
-- A global cannot possibly be ill-staged
-- nor does it need the 'lifting' treatment
@@ -515,28 +498,44 @@ tc_rec_sel_id lbl sel_name
where
occ = rdrNameOcc (unLoc lbl)
-check_naughty :: OccName -> TcId -> TcM ()
-check_naughty lbl id
- | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl)
- | otherwise = return ()
-
------------------------
+tcInferAmbiguousRecSelId :: Located RdrName
+ -> [HsExprArg 'TcpRn] -> Maybe TcRhoType
+ -> TcM Name
+-- Disgusting special case for ambiguous record selectors
-- Given a RdrName that refers to multiple record fields, and the type
-- of its argument, try to determine the name of the selector that is
-- meant.
-- See Note [Disambiguating record fields]
-disambiguateSelector :: Located RdrName -> Type -> TcM Name
-disambiguateSelector lr@(L _ rdr) parent_type
+tcInferAmbiguousRecSelId lbl args mb_res_ty
+ | arg1 : _ <- dropWhile (not . isVisibleArg) args -- A value arg is first
+ , EValArg { eva_arg = ValArg (L _ arg) } <- arg1
+ , Just sig_ty <- obviousSig arg -- A type sig on the arg disambiguates
+ = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty
+ ; finish_ambiguous_selector lbl sig_tc_ty }
+
+ | Just res_ty <- mb_res_ty
+ , Just (arg_ty,_) <- tcSplitFunTy_maybe res_ty
+ = finish_ambiguous_selector lbl (scaledThing arg_ty)
+
+ | otherwise
+ = ambiguousSelector lbl
+
+finish_ambiguous_selector :: Located RdrName -> Type -> TcM Name
+finish_ambiguous_selector lr@(L _ rdr) parent_type
= do { fam_inst_envs <- tcGetFamInstEnvs
- ; case tyConOf fam_inst_envs parent_type of
- Nothing -> ambiguousSelector lr
+ ; case tyConOf fam_inst_envs parent_type of {
+ Nothing -> ambiguousSelector lr ;
Just p ->
- do { xs <- lookupParents rdr
- ; let parent = RecSelData p
- ; case lookup parent xs of
- Just gre -> do { addUsedGRE True gre
- ; return (gre_name gre) }
- Nothing -> failWithTc (fieldNotInType parent rdr) } }
+
+ do { xs <- lookupParents rdr
+ ; let parent = RecSelData p
+ ; case lookup parent xs of {
+ Nothing -> failWithTc (fieldNotInType parent rdr) ;
+ Just gre ->
+
+ do { addUsedGRE True gre
+ ; return (gre_name gre) } } } } }
-- This field name really is ambiguous, so add a suitable "ambiguous
-- occurrence" error, then give up.
@@ -608,6 +607,101 @@ naughtyRecordSel lbl
text "Probable fix: use pattern-matching syntax instead"
+{- *********************************************************************
+* *
+ Expressions with a type signature
+ expr :: type
+* *
+********************************************************************* -}
+
+tcExprWithSig :: LHsExpr GhcRn -> LHsSigWcType (NoGhcTc GhcRn)
+ -> TcM (HsExpr GhcTc, TcSigmaType)
+tcExprWithSig expr hs_ty
+ = do { sig_info <- checkNoErrs $ -- Avoid error cascade
+ tcUserTypeSig loc hs_ty Nothing
+ ; (expr', poly_ty) <- tcExprSig expr sig_info
+ ; return (ExprWithTySig noExtField expr' hs_ty, poly_ty) }
+ where
+ loc = getLoc (hsSigWcType hs_ty)
+
+tcExprSig :: LHsExpr GhcRn -> TcIdSigInfo -> TcM (LHsExpr GhcTc, TcType)
+tcExprSig expr (CompleteSig { sig_bndr = poly_id, sig_loc = loc })
+ = setSrcSpan loc $ -- Sets the location for the implication constraint
+ do { let poly_ty = idType poly_id
+ ; (wrap, expr') <- tcSkolemiseScoped ExprSigCtxt poly_ty $ \rho_ty ->
+ tcCheckMonoExprNC expr rho_ty
+ ; return (mkLHsWrap wrap expr', poly_ty) }
+
+tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc })
+ = setSrcSpan loc $ -- Sets the location for the implication constraint
+ do { (tclvl, wanted, (expr', sig_inst))
+ <- pushLevelAndCaptureConstraints $
+ do { sig_inst <- tcInstSig sig
+ ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $
+ tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $
+ tcCheckPolyExprNC expr (sig_inst_tau sig_inst)
+ ; return (expr', sig_inst) }
+ -- See Note [Partial expression signatures]
+ ; let tau = sig_inst_tau sig_inst
+ infer_mode | null (sig_inst_theta sig_inst)
+ , isNothing (sig_inst_wcx sig_inst)
+ = ApplyMR
+ | otherwise
+ = NoRestrictions
+ ; (qtvs, givens, ev_binds, residual, _)
+ <- simplifyInfer tclvl infer_mode [sig_inst] [(name, tau)] wanted
+ ; emitConstraints residual
+
+ ; tau <- zonkTcType tau
+ ; let inferred_theta = map evVarPred givens
+ tau_tvs = tyCoVarsOfType tau
+ ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta
+ tau_tvs qtvs (Just sig_inst)
+ ; let inferred_sigma = mkInfSigmaTy qtvs inferred_theta tau
+ my_sigma = mkInvisForAllTys binders (mkPhiTy my_theta tau)
+ ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis.
+ then return idHsWrapper -- Fast path; also avoids complaint when we infer
+ -- an ambiguous type and have AllowAmbiguousType
+ -- e..g infer x :: forall a. F a -> Int
+ else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma
+
+ ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma)
+ ; let poly_wrap = wrap
+ <.> mkWpTyLams qtvs
+ <.> mkWpLams givens
+ <.> mkWpLet ev_binds
+ ; return (mkLHsWrap poly_wrap expr', my_sigma) }
+
+
+{- Note [Partial expression signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Partial type signatures on expressions are easy to get wrong. But
+here is a guiding principile
+ e :: ty
+should behave like
+ let x :: ty
+ x = e
+ in x
+
+So for partial signatures we apply the MR if no context is given. So
+ e :: IO _ apply the MR
+ e :: _ => IO _ do not apply the MR
+just like in GHC.Tc.Gen.Bind.decideGeneralisationPlan
+
+This makes a difference (#11670):
+ peek :: Ptr a -> IO CLong
+ peek ptr = peekElemOff undefined 0 :: _
+from (peekElemOff undefined 0) we get
+ type: IO w
+ constraints: Storable w
+
+We must NOT try to generalise over 'w' because the signature specifies
+no constraints so we'll complain about not being able to solve
+Storable w. Instead, don't generalise; then _ gets instantiated to
+CLong, as it should.
+-}
+
+
{- *********************************************************************
* *
tcInferId, tcCheckId
@@ -653,19 +747,12 @@ tc_infer_id id_name
= do { thing <- tcLookup id_name
; case thing of
ATcId { tct_id = id }
- -> do { check_naughty occ id
- -- See Note [HsVar: naughty record selectors]
- ; checkThLocalId id
- ; tcEmitBindingUsage $ unitUE id_name One
+ -> do { check_local_id occ id
; return_id id }
AGlobal (AnId id)
- -> do { check_naughty occ id
- -- See Note [HsVar: naughty record selectors]
+ -> do { check_global_id occ id
; return_id id }
- -- A global cannot possibly be ill-staged
- -- nor does it need the 'lifting' treatment
- -- hence no checkTh stuff here
AGlobal (AConLike cl) -> case cl of
RealDataCon con -> return_data_con con
@@ -725,6 +812,23 @@ tc_infer_id id_name
, mkInvisForAllTys tvs $ mkInvisFunTysMany theta $ mkVisFunTys scaled_arg_tys res)
}
+check_local_id :: OccName -> Id -> TcM ()
+check_local_id occ id
+ = do { check_naughty occ id -- See Note [HsVar: naughty record selectors]
+ ; checkThLocalId id
+ ; tcEmitBindingUsage $ unitUE (idName id) One }
+
+check_global_id :: OccName -> Id -> TcM ()
+check_global_id occ id
+ = check_naughty occ id -- See Note [HsVar: naughty record selectors]
+ -- A global cannot possibly be ill-staged
+ -- nor does it need the 'lifting' treatment
+ -- Hence no checkTh stuff here
+
+check_naughty :: OccName -> TcId -> TcM ()
+check_naughty lbl id
+ | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl)
+ | otherwise = return ()
nonBidirectionalErr :: Outputable name => name -> TcM a
nonBidirectionalErr name = failWithTc $
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -267,11 +267,10 @@ kind-generalisation, is done by
kindGeneraliseSome
kindGeneraliseNone
-perform kind generalisation. Here, we have to deal with the fact that
-metatyvars generated in the type will have a bumped TcLevel, because
-explicit foralls raise the TcLevel. To avoid these variables from ever
-being visible in the surrounding context, we must obey the following
-dictum:
+Here, we have to deal with the fact that metatyvars generated in the
+type will have a bumped TcLevel, because explicit foralls raise the
+TcLevel. To avoid these variables from ever being visible in the
+surrounding context, we must obey the following dictum:
Every metavariable in a type must either be
(A) generalized, or
@@ -1057,7 +1056,7 @@ tc_hs_type mode forall@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
= do { (tclvl, wanted, (tv_bndrs, ty'))
<- pushLevelAndCaptureConstraints $
-- No need to solve equalities here; we will do that later
- bindExplicitTKTele mode tele $
+ bindExplicitTKTele_Skol_M mode tele $
-- The _M variant passes on the mode from the type, to
-- any wildards in kind signatures on the forall'd variables
-- e.g. f :: _ -> Int -> forall (a :: _). blah
@@ -3024,12 +3023,12 @@ cloneFlexiKindedTyVarTyVar = newFlexiKindedTyVar cloneTyVarTyVar
--------------------------------------
-- | Skolemise the 'HsTyVarBndr's in an 'LHsForAllTelescope.
-bindExplicitTKTele
+bindExplicitTKTele_Skol_M
:: TcTyMode
-> HsForAllTelescope GhcRn
-> TcM a
-> TcM ([TcTyVarBinder], a)
-bindExplicitTKTele mode tele thing_inside = case tele of
+bindExplicitTKTele_Skol_M mode tele thing_inside = case tele of
HsForAllVis { hsf_vis_bndrs = bndrs }
-> do { (req_tv_bndrs, thing) <- bindExplicitTKBndrs_Skol_M mode bndrs thing_inside
-- req_tv_bndrs :: [VarBndr TyVar ()],
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -2631,7 +2631,7 @@ https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0179-printi
re-generalising, as discussed in #11376.
> :type reverse
- reverse :: forall a. a -> a
+ reverse :: forall a. [a] -> [a]
-- foo :: forall a f b. (Show a, Num b, Foldable f) => a -> f b -> String
> :type +v foo @Int
=====================================
compiler/GHC/Tc/Solver.hs
=====================================
@@ -159,6 +159,8 @@ simplifyTop wanteds
pushLevelAndSolveEqualities :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
-- Push level, and solve all resulting equalities
+-- If there are any unsolved equalities, report them
+-- and fail (in the monad)
pushLevelAndSolveEqualities skol_info skol_tvs thing_inside
= do { (tclvl, wanted, res) <- pushLevelAndSolveEqualitiesX
"pushLevelAndSolveEqualities" thing_inside
@@ -167,6 +169,9 @@ pushLevelAndSolveEqualities skol_info skol_tvs thing_inside
pushLevelAndSolveEqualitiesX :: String -> TcM a
-> TcM (TcLevel, WantedConstraints, a)
+-- Push the level, gather equality constraints, and then solve them.
+-- Returns any remaining unsolved equalities.
+-- Does not report errors.
pushLevelAndSolveEqualitiesX callsite thing_inside
= do { traceTc "pushLevelAndSolveEqualitiesX {" (text "Called from" <+> text callsite)
; (tclvl, (wanted, res))
@@ -180,7 +185,7 @@ pushLevelAndSolveEqualitiesX callsite thing_inside
-- | Type-check a thing that emits only equality constraints, solving any
-- constraints we can and re-emitting constraints that we can't.
--- We'll get another crack at it later
+-- Use this variant only when we'll get another crack at it later
-- See Note [Failure in local type signatures]
solveEqualities :: String -> TcM a -> TcM a
solveEqualities callsite thing_inside
@@ -347,6 +352,9 @@ See also #18062, #11506
reportUnsolvedEqualities :: SkolemInfo -> [TcTyVar] -> TcLevel
-> WantedConstraints -> TcM ()
+-- Reports all unsolved wanteds provided; fails in the monad if there are any.
+-- The provided SkolemInfo and [TcTyVar] arguments are used in an implication to
+-- provide skolem info for any errors.
reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
| isEmptyWC wanted
= return ()
@@ -2370,7 +2378,7 @@ beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
h :: F Int -> ()
h = undefined
-o data TEx where
+ data TEx where
TEx :: a -> TEx
f (x::beta) =
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -58,6 +58,7 @@ import GHC.Core.Class
import GHC.Core.Coercion.Axiom
import GHC.Core.TyCon
import GHC.Core.DataCon
+import GHC.Hs.Decls( newOrDataToFlavour )
import GHC.Types.Id
import GHC.Types.Var
import GHC.Types.Var.Env
@@ -2317,7 +2318,7 @@ tcClassDecl1 roles_info class_name hs_ctxt meths fundeps sigs ats at_defs
; return (ctxt, fds, sig_stuff, at_stuff) }
- -- The reportUnsolvedEqualities will report errors for any
+ -- The pushLevelAndSolveEqualities will report errors for any
-- unsolved equalities, so these zonks should not encounter
-- any unfilled coercion variables unless there is such an error
-- The zonk also squeeze out the TcTyCons, and converts
@@ -2795,8 +2796,7 @@ tcDataDefn err_ctxt roles_info tc_name
; return (tycon, [deriv_info]) }
where
skol_info = TyConSkol flav tc_name
- flav = case new_or_data of { NewType -> NewtypeFlavour
- ; DataType -> DataTypeFlavour }
+ flav = newOrDataToFlavour new_or_data
-- Abstract data types in hsig files can have arbitrary kinds,
-- because they may be implemented by type synonyms
@@ -3305,12 +3305,12 @@ tcConDecl rep_tycon tag_map tmpl_bndrs _res_kind res_tmpl new_or_data
; let skol_tvs = imp_tvs ++ binderVars exp_tvbndrs
; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
- ; let fake_ty = mkSpecForAllTys imp_tvs $
- mkInvisForAllTys exp_tvbndrs $
- mkPhiTy ctxt $
- mkVisFunTys arg_tys $
- res_ty
- ; tkvs <- kindGeneralizeAll fake_ty
+ ; let con_ty = mkSpecForAllTys imp_tvs $
+ mkInvisForAllTys exp_tvbndrs $
+ mkPhiTy ctxt $
+ mkVisFunTys arg_tys $
+ res_ty
+ ; tkvs <- kindGeneralizeAll con_ty
; let tvbndrs = mkTyVarBinders InferredSpec tkvs
++ mkTyVarBinders SpecifiedSpec imp_tvs
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -969,6 +969,8 @@ addHoles wc holes
dropMisleading :: WantedConstraints -> WantedConstraints
-- Drop misleading constraints; really just class constraints
-- See Note [Constraints and errors] in GHC.Tc.Utils.Monad
+-- for why this function is so strange, treating the 'simples'
+-- and the implications differently. Sigh.
dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes })
= WC { wc_simple = filterBag insolubleCt simples
, wc_impl = mapBag drop_implic implics
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -468,7 +468,7 @@ readExpType exp_ty
-- | Returns the expected type when in checking mode.
checkingExpType_maybe :: ExpType -> Maybe TcType
checkingExpType_maybe (Check ty) = Just ty
-checkingExpType_maybe _ = Nothing
+checkingExpType_maybe (Infer {}) = Nothing
-- | Returns the expected type when in checking mode. Panics if in inference
-- mode.
@@ -1646,11 +1646,11 @@ alpha[1] and beta[2]? Their levels. beta[2] has the right TcLevel for
generalisation, and so we generalise it. alpha[1] does not, and so
we leave it alone.
-Note that not *every* variable with a higher level will get generalised,
-either due to the monomorphism restriction or other quirks. See, for
-example, the code in GHC.Tc.Solver.decideMonoTyVars and in
-GHC.Tc.Gen.HsType.kindGeneralize, both of which exclude certain otherwise-eligible
-variables from being generalised.
+Note that not *every* variable with a higher level will get
+generalised, either due to the monomorphism restriction or other
+quirks. See, for example, the code in GHC.Tc.Solver.decideMonoTyVars
+and in GHC.Tc.Gen.HsType.kindGeneralizeSome, both of which exclude
+certain otherwise-eligible variables from being generalised.
Using level numbers for quantification is implemented in the candidateQTyVars...
functions, by adding only those variables with a level strictly higher than
@@ -1690,7 +1690,7 @@ quantifyTyVars dvs@(DV{ dv_kvs = dep_tkvs, dv_tvs = nondep_tkvs })
| otherwise
= do { traceTc "quantifyTyVars {" (ppr dvs)
- ; let !(dep_kvs, nondep_tvs) = candidateKiTyVars dvs
+ ; let (dep_kvs, nondep_tvs) = candidateKiTyVars dvs
-- In the non-PolyKinds case, default the kind variables
-- to *, and zonk the tyvars as usual. Notice that this
=====================================
docs/users_guide/exts/impredicative_types.rst
=====================================
@@ -25,7 +25,7 @@ instantiate ``id``\'s type with ``b := (forall s. ST s a) -> a``, and
that is not allowed. Instantiating polymorphic type variables with
polymorphic types is called *impredicative polymorphism*.
-GHC has robut support for *impredicative polymorphism*,
+GHC has robust support for *impredicative polymorphism*,
enabled with :extension:`ImpredicativeTypes`, using the so-called Quick Look
inference algorithm. It is described in the paper
`A quick look at impredicativity
@@ -38,7 +38,7 @@ Switching on :extension:`ImpredicativeTypes`
For example ``f :: Maybe (forall a. [a] -> [a])`` is a legal type signature.
- Switches on the Quick Look type inference algorithm, as described
- in the paper. The allow the compiler to infer impredicative instantiations of polymorphic
+ in the paper. This allows the compiler to infer impredicative instantiations of polymorphic
functions in many cases. For example, ``reverse xs`` will typecheck even if ``xs :: [forall a. a->a]``,
by instantiating ``reverse`` at type ``forall a. a->a``.
=====================================
docs/users_guide/ghci.rst
=====================================
@@ -2975,11 +2975,6 @@ commonly used commands.
*X> :type length
length :: Foldable t => t a -> Int
-.. ghci-cmd:: :type +v; ⟨expression⟩
-
- Infers and prints the type of ⟨expression⟩, binding inferred type variables
- with :ref:`*specified* visibility <inferred-vs-specified>`.
-
.. ghci-cmd:: :type +d; ⟨expression⟩
Infers and prints the type of ⟨expression⟩, instantiating *all* the forall
=====================================
testsuite/tests/impredicative/all.T
=====================================
@@ -19,3 +19,4 @@ test('T9730', normal, compile, [''])
test('T7026', normal, compile, [''])
test('T8808', normal, compile, [''])
test('T17332', normal, compile_fail, [''])
+test('expr-sig', normal, compile, [''])
=====================================
testsuite/tests/impredicative/expr-sig.hs
=====================================
@@ -0,0 +1,18 @@
+{-# LANGUAGE ImpredicativeTypes, RankNTypes #-}
+
+module ExprSig where
+
+import Data.Kind
+
+f :: [forall a. a->a] -> Int
+f x = error "urk"
+
+g1 = f undefined
+
+-- This should be accepted (and wasn't)
+g2 = f (undefined :: forall b. b)
+
+f3 :: [forall a. a->a] -> b
+f3 x = error "urk"
+
+g3 = f3 (undefined :: forall b. b)
\ No newline at end of file
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a6ee690e7828d95e174c422ac13df70a1d25e27a...4c56d0afda9fe4741fc3aaf2539cd3d6ba87eb00
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/a6ee690e7828d95e174c422ac13df70a1d25e27a...4c56d0afda9fe4741fc3aaf2539cd3d6ba87eb00
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/20200914/7479c9f2/attachment-0001.html>
More information about the ghc-commits
mailing list