diff options
Diffstat (limited to 'compiler/GHC/Tc/Gen/Bind.hs')
| -rw-r--r-- | compiler/GHC/Tc/Gen/Bind.hs | 160 |
1 files changed, 76 insertions, 84 deletions
diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index 0d2ba18503..193292c797 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -41,6 +41,8 @@ import GHC.Tc.Utils.Env import GHC.Tc.Utils.Unify import GHC.Tc.Solver import GHC.Tc.Types.Evidence +import GHC.Tc.Types.Constraint +import GHC.Core.Predicate import GHC.Tc.Gen.HsType import GHC.Tc.Gen.Pat import GHC.Tc.Utils.TcMType @@ -48,6 +50,7 @@ import GHC.Core.Reduction ( Reduction(..) ) import GHC.Core.Multiplicity import GHC.Core.FamInstEnv( normaliseType ) import GHC.Tc.Instance.Family( tcGetFamInstEnvs ) +import GHC.Core.Class ( Class ) import GHC.Tc.Utils.TcType import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy) import GHC.Builtin.Types ( mkBoxedTupleTy ) @@ -250,48 +253,36 @@ tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside ; (given_ips, ip_binds') <- mapAndUnzipM (wrapLocSndMA (tc_ip_bind ipClass)) ip_binds - -- If the binding binds ?x = E, we must now - -- discharge any ?x constraints in expr_lie - -- See Note [Implicit parameter untouchables] + -- Add all the IP bindings as givens for the body of the 'let' ; (ev_binds, result) <- checkConstraints (IPSkol ips) [] given_ips thing_inside ; return (HsIPBinds x (IPBinds ev_binds ip_binds') , result) } where - ips = [ip | (L _ (IPBind _ (Left (L _ ip)) _)) <- ip_binds] + ips = [ip | (L _ (IPBind _ (L _ ip) _)) <- ip_binds] -- I wonder if we should do these one at a time -- Consider ?x = 4 -- ?y = ?x + 1 - tc_ip_bind ipClass (IPBind _ (Left (L _ ip)) expr) + tc_ip_bind :: Class -> IPBind GhcRn -> TcM (DictId, IPBind GhcTc) + tc_ip_bind ipClass (IPBind _ l_name@(L _ ip) expr) = do { ty <- newOpenFlexiTyVarTy ; let p = mkStrLitTy $ hsIPNameFS ip ; ip_id <- newDict ipClass [ p, ty ] ; expr' <- tcCheckMonoExpr expr ty - ; let d = toDict ipClass p ty `fmap` expr' - ; return (ip_id, (IPBind noAnn (Right ip_id) d)) } - tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind" + ; let d = mapLoc (toDict ipClass p ty) expr' + ; return (ip_id, (IPBind ip_id l_name d)) } -- Coerces a `t` into a dictionary for `IP "x" t`. -- co : t -> IP "x" t + toDict :: Class -- IP class + -> Type -- type-level string for name of IP + -> Type -- type of IP + -> HsExpr GhcTc -- def'n of IP variable + -> HsExpr GhcTc -- dictionary for IP toDict ipClass x ty = mkHsWrap $ mkWpCastR $ wrapIP $ mkClassPred ipClass [x,ty] -{- Note [Implicit parameter untouchables] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We add the type variables in the types of the implicit parameters -as untouchables, not so much because we really must not unify them, -but rather because we otherwise end up with constraints like this - Num alpha, Implic { wanted = alpha ~ Int } -The constraint solver solves alpha~Int by unification, but then -doesn't float that solved constraint out (it's not an unsolved -wanted). Result disaster: the (Num alpha) is again solved, this -time by defaulting. No no no. - -However [Oct 10] this is all handled automatically by the -untouchable-range idea. --} - tcValBinds :: TopLevelFlag -> [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM thing @@ -726,12 +717,19 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list ; mapM_ (checkOverloadedSig mono) sigs ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted) - ; (qtvs, givens, ev_binds, insoluble) - <- simplifyInfer tclvl infer_mode sigs name_taus wanted + ; ((qtvs, givens, ev_binds, insoluble), residual) + <- captureConstraints $ simplifyInfer tclvl infer_mode sigs name_taus wanted ; let inferred_theta = map evVarPred givens ; exports <- checkNoErrs $ - mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos + mapM (mkExport prag_fn residual insoluble qtvs inferred_theta) mono_infos + + -- NB: *after* the checkNoErrs call above. This ensures that we don't get an error + -- cascade in case mkExport runs into trouble. In particular, this avoids duplicate + -- errors when a partial type signature cannot be quantified in chooseInferredQuantifiers. + -- See Note [Quantification and partial signatures] in GHC.Tc.Solver, Wrinkle 4. + -- Tested in partial-sigs/should_fail/NamedWilcardExplicitForall. + ; emitConstraints residual ; loc <- getSrcSpanM ; let poly_ids = map abe_poly exports @@ -748,6 +746,7 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list -------------- mkExport :: TcPragEnv + -> WantedConstraints -- residual constraints, already emitted (for errors only) -> Bool -- True <=> there was an insoluble type error -- when typechecking the bindings -> [TyVar] -> TcThetaType -- Both already zonked @@ -766,12 +765,12 @@ mkExport :: TcPragEnv -- Pre-condition: the qtvs and theta are already zonked -mkExport prag_fn insoluble qtvs theta - mono_info@(MBI { mbi_poly_name = poly_name - , mbi_sig = mb_sig - , mbi_mono_id = mono_id }) +mkExport prag_fn residual insoluble qtvs theta + (MBI { mbi_poly_name = poly_name + , mbi_sig = mb_sig + , mbi_mono_id = mono_id }) = do { mono_ty <- zonkTcType (idType mono_id) - ; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty + ; poly_id <- mkInferredPolyId residual insoluble qtvs theta poly_name mb_sig mono_ty -- NB: poly_id has a zonked type ; poly_id <- addInlinePrags poly_id prag_sigs @@ -793,14 +792,21 @@ mkExport prag_fn insoluble qtvs theta 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 addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $ - tcSubTypeSigma sig_ctxt sel_poly_ty poly_ty + else tcSubTypeSigma GhcBug20076 + sig_ctxt sel_poly_ty poly_ty + -- as Note [Impedance matching] explains, this should never fail, + -- and thus we'll never see an error message. It *may* do + -- instantiation, but no message will ever be printed to the + -- user, and so we use Shouldn'tHappenOrigin. + -- Actually, there is a bug here: #20076. So we tell the user + -- that they hit the bug. Once #20076 is fixed, change this + -- back to Shouldn'tHappenOrigin. ; localSigWarn poly_id mb_sig ; return (ABE { abe_ext = noExtField , abe_wrap = wrap - -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => mono_ty) + -- abe_wrap :: (forall qtvs. theta => mono_ty) ~ idType poly_id , abe_poly = poly_id , abe_mono = mono_id , abe_prags = SpecPrags spec_prags }) } @@ -808,12 +814,13 @@ mkExport prag_fn insoluble qtvs theta prag_sigs = lookupPragEnv prag_fn poly_name sig_ctxt = InfSigCtxt poly_name -mkInferredPolyId :: Bool -- True <=> there was an insoluble error when +mkInferredPolyId :: WantedConstraints -- the residual constraints, already emitted + -> Bool -- True <=> there was an insoluble error when -- checking the binding group for this Id -> [TyVar] -> TcThetaType -> Name -> Maybe TcIdSigInst -> TcType -> TcM TcId -mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty +mkInferredPolyId residual insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty | Just (TISI { sig_inst_sig = sig }) <- mb_sig_inst , CompleteSig { sig_bndr = poly_id } <- sig = return poly_id @@ -833,7 +840,7 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty -- We can discard the coercion _co, because we'll reconstruct -- it in the call to tcSubType below - ; (binders, theta') <- chooseInferredQuantifiers inferred_theta + ; (binders, theta') <- chooseInferredQuantifiers residual inferred_theta (tyCoVarsOfType mono_ty') qtvs mb_sig_inst ; let inferred_poly_ty = mkInvisForAllTys binders (mkPhiTy theta' mono_ty') @@ -851,14 +858,16 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty ; return (mkLocalId poly_name Many inferred_poly_ty) } -chooseInferredQuantifiers :: TcThetaType -- inferred +chooseInferredQuantifiers :: WantedConstraints -- residual constraints + -> TcThetaType -- inferred -> TcTyVarSet -- tvs free in tau type -> [TcTyVar] -- inferred quantified tvs -> Maybe TcIdSigInst -> TcM ([InvisTVBinder], TcThetaType) -chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing +chooseInferredQuantifiers _residual inferred_theta tau_tvs qtvs Nothing = -- No type signature (partial or complete) for this binder, do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs) + -- See Note [growThetaTyVars vs closeWrtFunDeps] in GHC.Tc.Solver -- Include kind variables! #7916 my_theta = pickCapturedPreds free_tvs inferred_theta binders = [ mkTyVarBinder InferredSpec tv @@ -866,11 +875,11 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing , tv `elemVarSet` free_tvs ] ; return (binders, my_theta) } -chooseInferredQuantifiers inferred_theta tau_tvs qtvs - (Just (TISI { sig_inst_sig = sig -- Always PartialSig - , sig_inst_wcx = wcx - , sig_inst_theta = annotated_theta - , sig_inst_skols = annotated_tvs })) +chooseInferredQuantifiers residual inferred_theta tau_tvs qtvs + (Just (TISI { sig_inst_sig = sig@(PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty }) + , sig_inst_wcx = wcx + , sig_inst_theta = annotated_theta + , sig_inst_skols = annotated_tvs })) = -- Choose quantifiers for a partial type signature do { let (psig_qtv_nms, psig_qtv_bndrs) = unzip annotated_tvs ; psig_qtv_bndrs <- mapM zonkInvisTVBinder psig_qtv_bndrs @@ -888,8 +897,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs -- signature is not actually quantified. How can that happen? -- See Note [Quantification and partial signatures] Wrinkle 4 -- in GHC.Tc.Solver - ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs - , not (tv `elem` qtvs) ] + ; mapM_ report_mono_sig_tv_err [ pr | pr@(_,tv) <- psig_qtv_prs + , not (tv `elem` qtvs) ] ; annotated_theta <- zonkTcTypes annotated_theta ; (free_tvs, my_theta) <- choose_psig_context psig_qtv_set annotated_theta wcx @@ -905,16 +914,20 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs ; return (final_qtvs, my_theta) } where report_dup_tyvar_tv_err (n1,n2) - | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig = addErrTc (TcRnPartialTypeSigTyVarMismatch n1 n2 fn_name hs_ty) - | otherwise -- Can't happen; by now we know it's a partial sig - = pprPanic "report_tyvar_tv_err" (ppr sig) - report_mono_sig_tv_err n - | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig - = addErrTc (TcRnPartialTypeSigBadQuantifier n fn_name hs_ty) - | otherwise -- Can't happen; by now we know it's a partial sig - = pprPanic "report_mono_sig_tv_err" (ppr sig) + report_mono_sig_tv_err (n,tv) + = addErrTc (TcRnPartialTypeSigBadQuantifier n fn_name m_unif_ty hs_ty) + where + m_unif_ty = listToMaybe + [ rhs + -- recall that residuals are always implications + | residual_implic <- bagToList $ wc_impl residual + , residual_ct <- bagToList $ wc_simple (ic_wanted residual_implic) + , let residual_pred = ctPred residual_ct + , Just (Nominal, lhs, rhs) <- [ getEqPredTys_maybe residual_pred ] + , Just lhs_tv <- [ tcGetTyVar_maybe lhs ] + , lhs_tv == tv ] choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType -> TcM (VarSet, TcThetaType) @@ -925,7 +938,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs choose_psig_context psig_qtvs annotated_theta (Just wc_var_ty) = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs) - -- growThetaVars just like the no-type-sig case + -- growThetaTyVars just like the no-type-sig case + -- See Note [growThetaTyVars vs closeWrtFunDeps] in GHC.Tc.Solver -- Omitting this caused #12844 seed_tvs = tyCoVarsOfTypes annotated_theta -- These are put there `unionVarSet` tau_tvs -- by the user @@ -961,25 +975,8 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs -- Hack alert! See GHC.Tc.Gen.HsType: -- Note [Extra-constraint holes in partial type signatures] -mk_impedance_match_msg :: MonoBindInfo - -> TcType -> TcType - -> TidyEnv -> TcM (TidyEnv, SDoc) --- This is a rare but rather awkward error messages -mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig }) - inf_ty sig_ty tidy_env - = do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env inf_ty - ; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty - ; let msg = vcat [ text "When checking that the inferred type" - , nest 2 $ ppr name <+> dcolon <+> ppr inf_ty - , text "is as general as its" <+> what <+> text "signature" - , nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ] - ; return (tidy_env2, msg) } - where - what = case mb_sig of - Nothing -> text "inferred" - Just sig | isPartialSig sig -> text "(partial)" - | otherwise -> empty - +chooseInferredQuantifiers _ _ _ _ (Just (TISI { sig_inst_sig = sig@(CompleteSig {}) })) + = pprPanic "chooseInferredQuantifiers" (ppr sig) mk_inf_msg :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) mk_inf_msg poly_name poly_ty tidy_env @@ -988,7 +985,6 @@ mk_inf_msg poly_name poly_ty tidy_env , nest 2 $ ppr poly_name <+> dcolon <+> ppr poly_ty ] ; return (tidy_env1, msg) } - -- | Warn the user about polymorphic local binders that lack type signatures. localSigWarn :: Id -> Maybe TcIdSigInst -> TcM () localSigWarn id mb_sig @@ -1103,7 +1099,6 @@ Examples that might fail: or multi-parameter type classes - an inferred type that includes unboxed tuples - Note [Impedance matching] ~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -1128,8 +1123,8 @@ We can get these by "impedance matching": tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool) tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono) - f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f - g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g + f a d1 d2 = case tuple a Any d1 d2 of (f_mono, g_mono) -> f_mono + g b = case tuple Integer b dEqInteger dNumInteger of (f_mono,g_mono) -> g_mono Suppose the shared quantified tyvars are qtvs and constraints theta. Then we want to check that @@ -1138,13 +1133,10 @@ and the proof is the impedance matcher. Notice that the impedance matcher may do defaulting. See #7173. -It also cleverly does an ambiguity check; for example, rejecting - f :: F a -> F a -where F is a non-injective type function. --} +If we've gotten the constraints right during inference (and we assume we have), +this sub-type check should never fail. It's not really a check -- it's more of +a procedure to produce the right wrapper. - -{- Note [SPECIALISE pragmas] ~~~~~~~~~~~~~~~~~~~~~~~~~ There is no point in a SPECIALISE pragma for a non-overloaded function: |