diff options
Diffstat (limited to 'compiler/GHC/Tc')
30 files changed, 1895 insertions, 1705 deletions
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs index e2a7f5f251..41bc8cd269 100644 --- a/compiler/GHC/Tc/Errors.hs +++ b/compiler/GHC/Tc/Errors.hs @@ -221,6 +221,7 @@ report_unsolved type_errors expr_holes , text "Wanted:" <+> ppr wanted ] ; warn_redundant <- woptM Opt_WarnRedundantConstraints + ; exp_syns <- goptM Opt_PrintExpandedSynonyms ; let err_ctxt = CEC { cec_encl = [] , cec_tidy = tidy_env , cec_defer_type_errors = type_errors @@ -234,6 +235,7 @@ report_unsolved type_errors expr_holes -- See #15539 and c.f. setting ic_status -- in GHC.Tc.Solver.setImplicationStatus , cec_warn_redundant = warn_redundant + , cec_expand_syns = exp_syns , cec_binds = binds_var } ; tc_lvl <- getTcLevel @@ -337,6 +339,7 @@ data ReportErrCtxt , cec_out_of_scope_holes :: HoleChoice -- Out of scope holes , cec_warn_redundant :: Bool -- True <=> -Wredundant-constraints + , cec_expand_syns :: Bool -- True <=> -fprint-expanded-synonyms , cec_suppress :: Bool -- True <=> More important errors have occurred, -- so create bindings if need be, but @@ -351,6 +354,7 @@ instance Outputable ReportErrCtxt where , cec_type_holes = th , cec_out_of_scope_holes = osh , cec_warn_redundant = wr + , cec_expand_syns = es , cec_suppress = sup }) = text "CEC" <+> braces (vcat [ text "cec_binds" <+> equals <+> ppr bvar @@ -359,6 +363,7 @@ instance Outputable ReportErrCtxt where , text "cec_type_holes" <+> equals <+> ppr th , text "cec_out_of_scope_holes" <+> equals <+> ppr osh , text "cec_warn_redundant" <+> equals <+> ppr wr + , text "cec_expand_syns" <+> equals <+> ppr es , text "cec_suppress" <+> equals <+> ppr sup ]) -- | Returns True <=> the ReportErrCtxt indicates that something is deferred @@ -403,7 +408,7 @@ previously suppressed. (e.g. partial-sigs/should_fail/T14584) -} reportImplic :: ReportErrCtxt -> Implication -> TcM () -reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope +reportImplic ctxt implic@(Implic { ic_skols = tvs , ic_given = given , ic_wanted = wanted, ic_binds = evb , ic_status = status, ic_info = info @@ -417,10 +422,12 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_telescope = m_telescope | otherwise = do { traceTc "reportImplic" (ppr implic') + ; when bad_telescope $ reportBadTelescope ctxt tcl_env info tvs + -- Do /not/ use the tidied tvs because then are in the + -- wrong order, so tidying will rename things wrongly ; reportWanteds ctxt' tc_lvl wanted ; when (cec_warn_redundant ctxt) $ - warnRedundantConstraints ctxt' tcl_env info' dead_givens - ; when bad_telescope $ reportBadTelescope ctxt tcl_env m_telescope tvs } + warnRedundantConstraints ctxt' tcl_env info' dead_givens } where tcl_env = ic_env implic insoluble = isInsolubleStatus status @@ -492,8 +499,8 @@ warnRedundantConstraints ctxt env info ev_vars improving pred -- (transSuperClasses p) does not include p = any isImprovementPred (pred : transSuperClasses pred) -reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> Maybe SDoc -> [TcTyVar] -> TcM () -reportBadTelescope ctxt env (Just telescope) skols +reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcTyVar] -> TcM () +reportBadTelescope ctxt env (ForAllSkol _ telescope) skols = do { msg <- mkErrorReport ctxt env (important doc) ; reportError msg } where @@ -503,8 +510,8 @@ reportBadTelescope ctxt env (Just telescope) skols sorted_tvs = scopedSort skols -reportBadTelescope _ _ Nothing skols - = pprPanic "reportBadTelescope" (ppr skols) +reportBadTelescope _ _ skol_info skols + = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols) {- Note [Redundant constraints in instance decls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -752,8 +759,7 @@ mkGivenErrorReporter ctxt cts report = important inaccessible_msg `mappend` mk_relevant_bindings binds_msg - ; err <- mkEqErr_help dflags ctxt report ct' - Nothing ty1 ty2 + ; err <- mkEqErr_help dflags ctxt report ct' ty1 ty2 ; traceTc "mkGivenErrorReporter" (ppr ct) ; reportWarning (Reason Opt_WarnInaccessibleCode) err } @@ -1126,7 +1132,7 @@ mkIrredErr ctxt cts ; let orig = ctOrigin ct1 msg = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig) ; mkErrorMsgFromCt ctxt ct1 $ - important msg `mappend` mk_relevant_bindings binds_msg } + msg `mappend` mk_relevant_bindings binds_msg } where (ct1:_) = cts @@ -1276,14 +1282,14 @@ mkIPErr ctxt cts preds = map ctPred cts givens = getUserGivens ctxt msg | null givens - = addArising orig $ + = important $ addArising orig $ sep [ text "Unbound implicit parameter" <> plural cts , nest 2 (pprParendTheta preds) ] | otherwise = couldNotDeduce givens (preds, orig) ; mkErrorMsgFromCt ctxt ct1 $ - important msg `mappend` mk_relevant_bindings binds_msg } + msg `mappend` mk_relevant_bindings binds_msg } where (ct1:_) = cts @@ -1356,56 +1362,17 @@ mkEqErr1 ctxt ct -- Wanted or derived; = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct ; rdr_env <- getGlobalRdrEnv ; fam_envs <- tcGetFamInstEnvs - ; exp_syns <- goptM Opt_PrintExpandedSynonyms - ; let (keep_going, is_oriented, wanted_msg) - = mk_wanted_extra (ctLoc ct) exp_syns - coercible_msg = case ctEqRel ct of + ; let coercible_msg = case ctEqRel ct of NomEq -> empty ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2 ; dflags <- getDynFlags - ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going) - ; let report = mconcat [important wanted_msg, important coercible_msg, - mk_relevant_bindings binds_msg] - ; if keep_going - then mkEqErr_help dflags ctxt report ct is_oriented ty1 ty2 - else mkErrorMsgFromCt ctxt ct report } + ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct)) + ; let report = mconcat [ important coercible_msg + , mk_relevant_bindings binds_msg] + ; mkEqErr_help dflags ctxt report ct ty1 ty2 } where (ty1, ty2) = getEqPredTys (ctPred ct) - -- If the types in the error message are the same as the types - -- we are unifying, don't add the extra expected/actual message - mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc) - mk_wanted_extra loc expandSyns - = case ctLocOrigin loc of - orig@TypeEqOrigin {} -> mkExpectedActualMsg ty1 ty2 orig - t_or_k expandSyns - where - t_or_k = ctLocTypeOrKind_maybe loc - - KindEqOrigin cty1 mb_cty2 sub_o sub_t_or_k - -> (True, Nothing, msg1 $$ msg2) - where - sub_what = case sub_t_or_k of Just KindLevel -> text "kinds" - _ -> text "types" - msg1 = sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions -> - case mb_cty2 of - Just cty2 - | printExplicitCoercions - || not (cty1 `pickyEqType` cty2) - -> hang (text "When matching" <+> sub_what) - 2 (vcat [ ppr cty1 <+> dcolon <+> - ppr (tcTypeKind cty1) - , ppr cty2 <+> dcolon <+> - ppr (tcTypeKind cty2) ]) - _ -> text "When matching the kind of" <+> quotes (ppr cty1) - msg2 = case sub_o of - TypeEqOrigin {} - | Just cty2 <- mb_cty2 -> - thdOf3 (mkExpectedActualMsg cty1 cty2 sub_o sub_t_or_k - expandSyns) - _ -> empty - _ -> (True, Nothing, empty) - -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint -- is left over. mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs @@ -1453,76 +1420,43 @@ mkCoercibleExplanation rdr_env fam_envs ty1 ty2 | otherwise = False -{- --- | Make a listing of role signatures for all the parameterised tycons --- used in the provided types - - --- SLPJ Jun 15: I could not convince myself that these hints were really --- useful. Maybe they are, but I think we need more work to make them --- actually helpful. -mkRoleSigs :: Type -> Type -> SDoc -mkRoleSigs ty1 ty2 - = ppUnless (null role_sigs) $ - hang (text "Relevant role signatures:") - 2 (vcat role_sigs) - where - tcs = nameEnvElts $ tyConsOfType ty1 `plusNameEnv` tyConsOfType ty2 - role_sigs = mapMaybe ppr_role_sig tcs - - ppr_role_sig tc - | null roles -- if there are no parameters, don't bother printing - = Nothing - | isBuiltInSyntax (tyConName tc) -- don't print roles for (->), etc. - = Nothing - | otherwise - = Just $ hsep $ [text "type role", ppr tc] ++ map ppr roles - where - roles = tyConRoles tc --} - mkEqErr_help :: DynFlags -> ReportErrCtxt -> Report -> Ct - -> Maybe SwapFlag -- Nothing <=> not sure -> TcType -> TcType -> TcM ErrMsg -mkEqErr_help dflags ctxt report ct oriented ty1 ty2 +mkEqErr_help dflags ctxt report ct ty1 ty2 | Just (tv1, _) <- tcGetCastedTyVar_maybe ty1 - = mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 + = mkTyVarEqErr dflags ctxt report ct tv1 ty2 | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2 - = mkTyVarEqErr dflags ctxt report ct swapped tv2 ty1 + = mkTyVarEqErr dflags ctxt report ct tv2 ty1 | otherwise - = reportEqErr ctxt report ct oriented ty1 ty2 - where - swapped = fmap flipSwap oriented + = reportEqErr ctxt report ct ty1 ty2 reportEqErr :: ReportErrCtxt -> Report -> Ct - -> Maybe SwapFlag -- Nothing <=> not sure -> TcType -> TcType -> TcM ErrMsg -reportEqErr ctxt report ct oriented ty1 ty2 +reportEqErr ctxt report ct ty1 ty2 = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, report, eqInfo]) - where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2 - eqInfo = important $ mkEqInfoMsg ct ty1 ty2 + where + misMatch = misMatchOrCND False ctxt ct ty1 ty2 + eqInfo = mkEqInfoMsg ct ty1 ty2 mkTyVarEqErr, mkTyVarEqErr' :: DynFlags -> ReportErrCtxt -> Report -> Ct - -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg + -> TcTyVar -> TcType -> TcM ErrMsg -- tv1 and ty2 are already tidied -mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2 +mkTyVarEqErr dflags ctxt report ct tv1 ty2 = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2) - ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 } + ; mkTyVarEqErr' dflags ctxt report ct tv1 ty2 } -mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 - | not insoluble_occurs_check -- See Note [Occurs check wins] - , isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar, or else the thing would - -- be oriented the other way round; - -- see GHC.Tc.Solver.Canonical.canEqTyVarTyVar +mkTyVarEqErr' dflags ctxt report ct tv1 ty2 + | isUserSkolem ctxt tv1 -- ty2 won't be a meta-tyvar; we would have + -- swapped in Solver.Canonical.canEqTyVarHomo || isTyVarTyVar tv1 && not (isTyVarTy ty2) || ctEqRel ct == ReprEq - -- the cases below don't really apply to ReprEq (except occurs check) + -- The cases below don't really apply to ReprEq (except occurs check) = mkErrorMsgFromCt ctxt ct $ mconcat - [ important $ misMatchOrCND ctxt ct oriented ty1 ty2 - , important $ extraTyVarEqInfo ctxt tv1 ty2 + [ headline_msg + , extraTyVarEqInfo ctxt tv1 ty2 , report ] @@ -1531,11 +1465,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 -- function; it's not insoluble (because in principle F could reduce) -- but we have certainly been unable to solve it -- See Note [Occurs check error] in GHC.Tc.Solver.Canonical - = do { let main_msg = addArising (ctOrigin ct) $ - hang (text "Occurs check: cannot construct the infinite" <+> what <> colon) - 2 (sep [ppr ty1, char '~', ppr ty2]) - - extra2 = important $ mkEqInfoMsg ct ty1 ty2 + = do { let extra2 = mkEqInfoMsg ct ty1 ty2 interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $ filter isTyVar $ @@ -1549,17 +1479,16 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) ; mkErrorMsgFromCt ctxt ct $ - mconcat [important main_msg, extra2, extra3, report] } + mconcat [headline_msg, extra2, extra3, report] } | MTVU_Bad <- occ_check_expand = do { let msg = vcat [ text "Cannot instantiate unification variable" <+> quotes (ppr tv1) - , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) - , nest 2 (text "GHC doesn't yet support impredicative polymorphism") ] + , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ] -- Unlike the other reports, this discards the old 'report_important' -- instead of augmenting it. This is because the details are not likely -- to be helpful since this is just an unimplemented feature. - ; mkErrorMsgFromCt ctxt ct $ report { report_important = [msg] } } + ; mkErrorMsgFromCt ctxt ct $ mconcat [ headline_msg, important msg, report ] } -- If the immediately-enclosing implication has 'tv' a skolem, and -- we know by now its an InferSkol kind of skolem, then presumably @@ -1569,8 +1498,8 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , Implic { ic_skols = skols } <- implic , tv1 `elem` skols = mkErrorMsgFromCt ctxt ct $ mconcat - [ important $ misMatchMsg ct oriented ty1 ty2 - , important $ extraTyVarEqInfo ctxt tv1 ty2 + [ misMatchMsg ctxt ct ty1 ty2 + , extraTyVarEqInfo ctxt tv1 ty2 , report ] @@ -1579,7 +1508,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , Implic { ic_skols = skols, ic_info = skol_info } <- implic , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols , not (null esc_skols) - = do { let msg = important $ misMatchMsg ct oriented ty1 ty2 + = do { let msg = misMatchMsg ctxt ct ty1 ty2 esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols <+> pprQuotedList esc_skols , text "would escape" <+> @@ -1607,7 +1536,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , Implic { ic_given = given, ic_tclvl = lvl, ic_info = skol_info } <- implic = ASSERT2( not (isTouchableMetaTyVar lvl tv1) , ppr tv1 $$ ppr lvl ) -- See Note [Error messages for untouchables] - do { let msg = important $ misMatchMsg ct oriented ty1 ty2 + do { let msg = misMatchMsg ctxt ct ty1 ty2 tclvl_extra = important $ nest 2 $ sep [ quotes (ppr tv1) <+> text "is untouchable" @@ -1615,33 +1544,38 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 , nest 2 $ text "bound by" <+> ppr skol_info , nest 2 $ text "at" <+> ppr (tcl_loc (ic_env implic)) ] - tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2 - add_sig = important $ suggestAddSig ctxt ty1 ty2 + tv_extra = extraTyVarEqInfo ctxt tv1 ty2 + add_sig = suggestAddSig ctxt ty1 ty2 ; mkErrorMsgFromCt ctxt ct $ mconcat [msg, tclvl_extra, tv_extra, add_sig, report] } | otherwise - = reportEqErr ctxt report ct oriented (mkTyVarTy tv1) ty2 + = reportEqErr ctxt report ct (mkTyVarTy tv1) ty2 -- This *can* happen (#6123, and test T2627b) -- Consider an ambiguous top-level constraint (a ~ F a) -- Not an occurs check, because F is a type function. where + headline_msg = misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2 + ty1 = mkTyVarTy tv1 occ_check_expand = occCheckForErrors dflags tv1 ty2 insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2 - what = case ctLocTypeOrKind_maybe (ctLoc ct) of - Just KindLevel -> text "kind" - _ -> text "type" + what = text $ levelString $ + ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel -mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc +levelString :: TypeOrKind -> String +levelString TypeLevel = "type" +levelString KindLevel = "kind" + +mkEqInfoMsg :: Ct -> TcType -> TcType -> Report -- Report (a) ambiguity if either side is a type function application -- e.g. F a0 ~ Int -- (b) warning about injectivity if both sides are the same -- type function application F a ~ F b -- See Note [Non-injective type functions] mkEqInfoMsg ct ty1 ty2 - = tyfun_msg $$ ambig_msg + = important (tyfun_msg $$ ambig_msg) where mb_fun1 = isTyFun_maybe ty1 mb_fun2 = isTyFun_maybe ty2 @@ -1669,29 +1603,34 @@ isUserSkolem ctxt tv is_user_skol_info (InferSkol {}) = False is_user_skol_info _ = True -misMatchOrCND :: ReportErrCtxt -> Ct - -> Maybe SwapFlag -> TcType -> TcType -> SDoc +misMatchOrCND :: Bool -> ReportErrCtxt -> Ct + -> TcType -> TcType -> Report -- If oriented then ty1 is actual, ty2 is expected -misMatchOrCND ctxt ct oriented ty1 ty2 - | null givens || - (isRigidTy ty1 && isRigidTy ty2) || - isGivenCt ct - -- If the equality is unconditionally insoluble - -- or there is no context, don't report the context - = misMatchMsg ct oriented ty1 ty2 +misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2 + | insoluble_occurs_check -- See Note [Insoluble occurs check] + || (isRigidTy ty1 && isRigidTy ty2) + || isGivenCt ct + || null givens + = -- If the equality is unconditionally insoluble + -- or there is no context, don't report the context + misMatchMsg ctxt ct ty1 ty2 + | otherwise - = couldNotDeduce givens ([eq_pred], orig) + = mconcat [ couldNotDeduce givens ([eq_pred], orig) + , important $ mk_supplementary_ea_msg ctxt level ty1 ty2 orig ] where ev = ctEvidence ct eq_pred = ctEvPred ev orig = ctEvOrigin ev + level = ctLocTypeOrKind_maybe (ctEvLoc ev) `orElse` TypeLevel givens = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)] -- Keep only UserGivens that have some equalities. -- See Note [Suppress redundant givens during error reporting] -couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc +couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> Report couldNotDeduce givens (wanteds, orig) - = vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds) + = important $ + vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds) , vcat (pp_givens givens)] pp_givens :: [UserGiven] -> [SDoc] @@ -1763,11 +1702,11 @@ addition to superclasses (see Note [Remove redundant provided dicts] in GHC.Tc.TyCl.PatSyn). -} -extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc +extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> Report -- Add on extra info about skolem constants -- NB: The types themselves are already tidied extraTyVarEqInfo ctxt tv1 ty2 - = extraTyVarInfo ctxt tv1 $$ ty_extra ty2 + = important (extraTyVarInfo ctxt tv1 $$ ty_extra ty2) where ty_extra ty = case tcGetCastedTyVar_maybe ty of Just (tv, _) -> extraTyVarInfo ctxt tv @@ -1781,15 +1720,15 @@ extraTyVarInfo ctxt tv RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem" MetaTv {} -> empty -suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc +suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report -- See Note [Suggest adding a type signature] suggestAddSig ctxt ty1 ty2 | null inferred_bndrs - = empty + = mempty | [bndr] <- inferred_bndrs - = text "Possible fix: add a type signature for" <+> quotes (ppr bndr) + = important $ text "Possible fix: add a type signature for" <+> quotes (ppr bndr) | otherwise - = text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs) + = important $ text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs) where inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2) get_inf ty | Just tv <- tcGetTyVar_maybe ty @@ -1800,47 +1739,55 @@ suggestAddSig ctxt ty1 ty2 = [] -------------------- -misMatchMsg :: Ct -> Maybe SwapFlag -> TcType -> TcType -> SDoc +misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report -- Types are already tidy -- If oriented then ty1 is actual, ty2 is expected -misMatchMsg ct oriented ty1 ty2 - | Just NotSwapped <- oriented - = misMatchMsg ct (Just IsSwapped) ty2 ty1 - - -- These next two cases are when we're about to report, e.g., that - -- 'LiftedRep doesn't match 'VoidRep. Much better just to say - -- lifted vs. unlifted - | isLiftedRuntimeRep ty1 - = lifted_vs_unlifted - - | isLiftedRuntimeRep ty2 - = lifted_vs_unlifted - - | otherwise -- So now we have Nothing or (Just IsSwapped) - -- For some reason we treat Nothing like IsSwapped - = addArising orig $ - pprWithExplicitKindsWhenMismatch ty1 ty2 (ctOrigin ct) $ +misMatchMsg ctxt ct ty1 ty2 + = important $ + addArising orig $ + pprWithExplicitKindsWhenMismatch ty1 ty2 orig $ + sep [ case orig of + TypeEqOrigin {} -> tk_eq_msg ctxt ct ty1 ty2 orig + KindEqOrigin {} -> tk_eq_msg ctxt ct ty1 ty2 orig + _ -> headline_eq_msg False ct ty1 ty2 + , sameOccExtra ty2 ty1 ] + where + orig = ctOrigin ct + +headline_eq_msg :: Bool -> Ct -> Type -> Type -> SDoc +-- Generates the main "Could't match 't1' against 't2' +-- headline message +headline_eq_msg add_ea ct ty1 ty2 + + | (isLiftedRuntimeRep ty1 && isUnliftedRuntimeRep ty2) || + (isLiftedRuntimeRep ty2 && isUnliftedRuntimeRep ty1) + = text "Couldn't match a lifted type with an unlifted type" + + | isAtomicTy ty1 || isAtomicTy ty2 + = -- Print with quotes sep [ text herald1 <+> quotes (ppr ty1) , nest padding $ - text herald2 <+> quotes (ppr ty2) - , sameOccExtra ty2 ty1 ] + text herald2 <+> quotes (ppr ty2) ] + + | otherwise + = -- Print with vertical layout + vcat [ text herald1 <> colon <+> ppr ty1 + , nest padding $ + text herald2 <> colon <+> ppr ty2 ] where herald1 = conc [ "Couldn't match" - , if is_repr then "representation of" else "" - , if is_oriented then "expected" else "" + , if is_repr then "representation of" else "" + , if add_ea then "expected" else "" , what ] herald2 = conc [ "with" - , if is_repr then "that of" else "" - , if is_oriented then ("actual " ++ what) else "" ] + , if is_repr then "that of" else "" + , if add_ea then ("actual " ++ what) else "" ] + padding = length herald1 - length herald2 is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False } - is_oriented = isJust oriented - orig = ctOrigin ct - what = case ctLocTypeOrKind_maybe (ctLoc ct) of - Just KindLevel -> "kind" - _ -> "type" + what = levelString (ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel) conc :: [String] -> String conc = foldr1 add_space @@ -1850,114 +1797,49 @@ misMatchMsg ct oriented ty1 ty2 | null s2 = s1 | otherwise = s1 ++ (' ' : s2) - lifted_vs_unlifted - = addArising orig $ - text "Couldn't match a lifted type with an unlifted type" --- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a --- type mismatch occurs to due invisible kind arguments. --- --- This function first checks to see if the 'CtOrigin' argument is a --- 'TypeEqOrigin', and if so, uses the expected/actual types from that to --- check for a kind mismatch (as these types typically have more surrounding --- types and are likelier to be able to glean information about whether a --- mismatch occurred in an invisible argument position or not). If the --- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types --- themselves. -pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin - -> SDoc -> SDoc -pprWithExplicitKindsWhenMismatch ty1 ty2 ct - = pprWithExplicitKindsWhen show_kinds - where - (act_ty, exp_ty) = case ct of - TypeEqOrigin { uo_actual = act - , uo_expected = exp } -> (act, exp) - _ -> (ty1, ty2) - show_kinds = tcEqTypeVis act_ty exp_ty - -- True when the visible bit of the types look the same, - -- so we want to show the kinds in the displayed type - -mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool - -> (Bool, Maybe SwapFlag, SDoc) --- NotSwapped means (actual, expected), IsSwapped is the reverse --- First return val is whether or not to print a herald above this msg -mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act +tk_eq_msg :: ReportErrCtxt + -> Ct -> Type -> Type -> CtOrigin -> SDoc +tk_eq_msg ctxt ct ty1 ty2 orig@(TypeEqOrigin { uo_actual = act , uo_expected = exp - , uo_thing = maybe_thing }) - m_level printExpanded - | KindLevel <- level, occurs_check_error = (True, Nothing, empty) - | isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2) - | isLiftedTypeKind act, isUnliftedTypeKind exp = (False, Nothing, msg3) - | tcIsLiftedTypeKind exp = (False, Nothing, msg4) - | Just msg <- num_args_msg = (False, Nothing, msg $$ msg1) - | KindLevel <- level, Just th <- maybe_thing = (False, Nothing, msg5 th) - | act `pickyEqType` ty1, exp `pickyEqType` ty2 = (True, Just NotSwapped, empty) - | exp `pickyEqType` ty1, act `pickyEqType` ty2 = (True, Just IsSwapped, empty) - | otherwise = (True, Nothing, msg1) - where - level = m_level `orElse` TypeLevel + , uo_thing = mb_thing }) + -- We can use the TypeEqOrigin to + -- improve the error message quite a lot + + | isUnliftedTypeKind act, isLiftedTypeKind exp + = sep [ text "Expecting a lifted type, but" + , thing_msg mb_thing (text "an") (text "unlifted") ] + + | isLiftedTypeKind act, isUnliftedTypeKind exp + = sep [ text "Expecting an unlifted type, but" + , thing_msg mb_thing (text "a") (text "lifted") ] + + | tcIsLiftedTypeKind exp + = maybe_num_args_msg $$ + sep [ text "Expected a type, but" + , case mb_thing of + Nothing -> text "found something with kind" + Just thing -> quotes thing <+> text "has kind" + , quotes (pprWithTYPE act) ] + + | Just nargs_msg <- num_args_msg + = nargs_msg $$ + mk_ea_msg ctxt (Just ct) level orig + + | -- pprTrace "check" (ppr ea_looks_same $$ ppr exp $$ ppr act $$ ppr ty1 $$ ppr ty2) $ + ea_looks_same ty1 ty2 exp act + = mk_ea_msg ctxt (Just ct) level orig + + | otherwise -- The mismatched types are /inside/ exp and act + = vcat [ headline_eq_msg False ct ty1 ty2 + , mk_ea_msg ctxt Nothing level orig ] - occurs_check_error - | Just tv <- tcGetTyVar_maybe ty1 - , tv `elemVarSet` tyCoVarsOfType ty2 - = True - | Just tv <- tcGetTyVar_maybe ty2 - , tv `elemVarSet` tyCoVarsOfType ty1 - = True - | otherwise - = False - - sort = case level of - TypeLevel -> text "type" - KindLevel -> text "kind" - - msg1 = case level of - KindLevel - | Just th <- maybe_thing - -> msg5 th - - _ | not (act `pickyEqType` exp) - -> pprWithExplicitKindsWhenMismatch ty1 ty2 ct $ - vcat [ text "Expected" <+> sort <> colon <+> ppr exp - , text " Actual" <+> sort <> colon <+> ppr act - , if printExpanded then expandedTys else empty ] - - | otherwise - -> empty - - thing_msg = case maybe_thing of - Just thing -> \_ levity -> - quotes thing <+> text "is" <+> levity - Nothing -> \vowel levity -> - text "got a" <> - (if vowel then char 'n' else empty) <+> - levity <+> - text "type" - msg2 = sep [ text "Expecting a lifted type, but" - , thing_msg True (text "unlifted") ] - msg3 = sep [ text "Expecting an unlifted type, but" - , thing_msg False (text "lifted") ] - msg4 = maybe_num_args_msg $$ - sep [ text "Expected a type, but" - , maybe (text "found something with kind") - (\thing -> quotes thing <+> text "has kind") - maybe_thing - , quotes (pprWithTYPE act) ] - - msg5 th = pprWithExplicitKindsWhenMismatch ty1 ty2 ct $ - hang (text "Expected" <+> kind_desc <> comma) - 2 (text "but" <+> quotes th <+> text "has kind" <+> - quotes (ppr act)) - where - kind_desc | tcIsConstraintKind exp = text "a constraint" - - -- TYPE t0 - | Just arg <- kindRep_maybe exp - , tcIsTyVarTy arg = sdocOption sdocPrintExplicitRuntimeReps $ \case - True -> text "kind" <+> quotes (ppr exp) - False -> text "a type" + where + ct_loc = ctLoc ct + level = ctLocTypeOrKind_maybe ct_loc `orElse` TypeLevel - | otherwise = text "kind" <+> quotes (ppr exp) + thing_msg (Just thing) _ levity = quotes thing <+> text "is" <+> levity + thing_msg Nothing an levity = text "got" <+> an <+> levity <+> text "type" num_args_msg = case level of KindLevel @@ -1970,7 +1852,7 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act case n_act - n_exp of n | n > 0 -- we don't know how many args there are, so don't -- recommend removing args that aren't - , Just thing <- maybe_thing + , Just thing <- mb_thing -> Just $ text "Expecting" <+> speakN (abs n) <+> more <+> quotes thing where @@ -1981,25 +1863,125 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act _ -> Nothing - maybe_num_args_msg = case num_args_msg of - Nothing -> empty - Just m -> m + maybe_num_args_msg = num_args_msg `orElse` empty count_args ty = count isVisibleBinder $ fst $ splitPiTys ty - expandedTys = - ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat - [ text "Type synonyms expanded:" - , text "Expected type:" <+> ppr expTy1 - , text " Actual type:" <+> ppr expTy2 - ] +tk_eq_msg ctxt ct ty1 ty2 + (KindEqOrigin cty1 mb_cty2 sub_o mb_sub_t_or_k) + = vcat [ headline_eq_msg False ct ty1 ty2 + , supplementary_msg ] + where + sub_t_or_k = mb_sub_t_or_k `orElse` TypeLevel + sub_whats = text (levelString sub_t_or_k) <> char 's' + -- "types" or "kinds" + + supplementary_msg + = sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions -> + case mb_cty2 of + Just cty2 + | printExplicitCoercions + || not (cty1 `pickyEqType` cty2) + -> vcat [ hang (text "When matching" <+> sub_whats) + 2 (vcat [ ppr cty1 <+> dcolon <+> + ppr (tcTypeKind cty1) + , ppr cty2 <+> dcolon <+> + ppr (tcTypeKind cty2) ]) + , mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o ] + _ -> text "When matching the kind of" <+> quotes (ppr cty1) + +tk_eq_msg _ _ _ _ _ = panic "typeeq_mismatch_msg" + +ea_looks_same :: Type -> Type -> Type -> Type -> Bool +-- True if the faulting types (ty1, ty2) look the same as +-- the expected/actual types (exp, act). +-- If so, we don't want to redundantly report the latter +ea_looks_same ty1 ty2 exp act + = (act `looks_same` ty1 && exp `looks_same` ty2) || + (exp `looks_same` ty1 && act `looks_same` ty2) + where + looks_same t1 t2 = t1 `pickyEqType` t2 + || t1 `eqType` liftedTypeKind && t2 `eqType` liftedTypeKind + -- pickyEqType is sensitive to synonyms, so only replies True + -- when the types really look the same. However, + -- (TYPE 'LiftedRep) and Type both print the same way. + +mk_supplementary_ea_msg :: ReportErrCtxt -> TypeOrKind + -> Type -> Type -> CtOrigin -> SDoc +mk_supplementary_ea_msg ctxt level ty1 ty2 orig + | TypeEqOrigin { uo_expected = exp, uo_actual = act } <- orig + , not (ea_looks_same ty1 ty2 exp act) + = mk_ea_msg ctxt Nothing level orig + | otherwise + = empty + +mk_ea_msg :: ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc +-- Constructs a "Couldn't match" message +-- The (Maybe Ct) says whether this is the main top-level message (Just) +-- or a supplementary message (Nothing) +mk_ea_msg ctxt at_top level + (TypeEqOrigin { uo_actual = act, uo_expected = exp, uo_thing = mb_thing }) + | Just thing <- mb_thing + , KindLevel <- level + = hang (text "Expected" <+> kind_desc <> comma) + 2 (text "but" <+> quotes thing <+> text "has kind" <+> + quotes (ppr act)) + + | otherwise + = vcat [ case at_top of + Just ct -> headline_eq_msg True ct exp act + Nothing -> supplementary_ea_msg + , ppWhen expand_syns expandedTys ] + + where + supplementary_ea_msg = vcat [ text "Expected:" <+> ppr exp + , text " Actual:" <+> ppr act ] + + kind_desc | tcIsConstraintKind exp = text "a constraint" + | Just arg <- kindRep_maybe exp -- TYPE t0 + , tcIsTyVarTy arg = sdocOption sdocPrintExplicitRuntimeReps $ \case + True -> text "kind" <+> quotes (ppr exp) + False -> text "a type" + | otherwise = text "kind" <+> quotes (ppr exp) + + expand_syns = cec_expand_syns ctxt + + expandedTys = ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat + [ text "Type synonyms expanded:" + , text "Expected type:" <+> ppr expTy1 + , text " Actual type:" <+> ppr expTy2 ] (expTy1, expTy2) = expandSynonymsToMatch exp act -mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg" +mk_ea_msg _ _ _ _ = empty + +-- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a +-- type mismatch occurs to due invisible kind arguments. +-- +-- This function first checks to see if the 'CtOrigin' argument is a +-- 'TypeEqOrigin', and if so, uses the expected/actual types from that to +-- check for a kind mismatch (as these types typically have more surrounding +-- types and are likelier to be able to glean information about whether a +-- mismatch occurred in an invisible argument position or not). If the +-- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types +-- themselves. +pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin + -> SDoc -> SDoc +pprWithExplicitKindsWhenMismatch ty1 ty2 ct + = pprWithExplicitKindsWhen show_kinds + where + (act_ty, exp_ty) = case ct of + TypeEqOrigin { uo_actual = act + , uo_expected = exp } -> (act, exp) + _ -> (ty1, ty2) + show_kinds = tcEqTypeVis act_ty exp_ty + -- True when the visible bit of the types look the same, + -- so we want to show the kinds in the displayed type + + -{- Note [Insoluble occurs check wins] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +{- Note [Insoluble occurs check] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider [G] a ~ [a], [W] a ~ [a] (#13674). The Given is insoluble so we don't use it for rewriting. The Wanted is also insoluble, and we don't solve it from the Given. It's very confusing to say @@ -2009,7 +1991,8 @@ And indeed even thinking about the Givens is silly; [W] a ~ [a] is just as insoluble as Int ~ Bool. Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck) -then report it first. +then report it directly, not in the "cannot deduce X from Y" form. +This is done in misMatchOrCND (via the insoluble_occurs_check arg) (NB: there are potentially-soluble ones, like (a ~ F a b), and we don't want to be as draconian with them.) diff --git a/compiler/GHC/Tc/Errors/Hole.hs b/compiler/GHC/Tc/Errors/Hole.hs index 0639e79073..7c0eaa7912 100644 --- a/compiler/GHC/Tc/Errors/Hole.hs +++ b/compiler/GHC/Tc/Errors/Hole.hs @@ -43,7 +43,7 @@ import Data.Graph ( graphFromEdges, topSort ) import GHC.Tc.Solver ( simpl_top, runTcSDeriveds ) -import GHC.Tc.Utils.Unify ( tcSubType_NC ) +import GHC.Tc.Utils.Unify ( tcSubTypeSigma ) import GHC.HsToCore.Docs ( extractDocs ) import qualified Data.Map as Map @@ -933,7 +933,7 @@ tcCheckHoleFit (TypedHole {..}) hole_ty ty = discardErrs $ -- imp is the innermost implication (imp:_) -> return (ic_tclvl imp) ; (wrap, wanted) <- setTcLevel innermost_lvl $ captureConstraints $ - tcSubType_NC ExprSigCtxt ty hole_ty + tcSubTypeSigma ExprSigCtxt ty hole_ty ; traceTc "Checking hole fit {" empty ; traceTc "wanteds are: " $ ppr wanted ; if isEmptyWC wanted && isEmptyBag th_relevant_cts diff --git a/compiler/GHC/Tc/Gen/Arrow.hs b/compiler/GHC/Tc/Gen/Arrow.hs index ef60b3cea7..c21a885970 100644 --- a/compiler/GHC/Tc/Gen/Arrow.hs +++ b/compiler/GHC/Tc/Gen/Arrow.hs @@ -14,7 +14,8 @@ module GHC.Tc.Gen.Arrow ( tcProc ) where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcLExpr, tcInferRho, tcSyntaxOp, tcCheckId, tcCheckExpr ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckMonoExpr, tcInferRho, tcSyntaxOp + , tcCheckId, tcCheckPolyExpr ) import GHC.Hs import GHC.Tc.Gen.Match @@ -161,7 +162,7 @@ tc_cmd env in_cmd@(HsCmdLamCase x matches) (stk, res_ty) return (mkHsCmdWrap (mkWpCastN co) (HsCmdLamCase x matches')) tc_cmd env (HsCmdIf x NoSyntaxExprRn pred b1 b2) res_ty -- Ordinary 'if' - = do { pred' <- tcLExpr pred (mkCheckExpType boolTy) + = do { pred' <- tcCheckMonoExpr pred boolTy ; b1' <- tcCmd env b1 res_ty ; b2' <- tcCmd env b2 res_ty ; return (HsCmdIf x NoSyntaxExprTc pred' b1' b2') @@ -179,7 +180,7 @@ tc_cmd env (HsCmdIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty -- Rebindable syn ; (pred', fun') <- tcSyntaxOp IfOrigin fun (map synKnownType [pred_ty, r_ty, r_ty]) (mkCheckExpType r_ty) $ \ _ -> - tcLExpr pred (mkCheckExpType pred_ty) + tcCheckMonoExpr pred pred_ty ; b1' <- tcCmd env b1 res_ty ; b2' <- tcCmd env b2 res_ty @@ -206,9 +207,9 @@ tc_cmd env cmd@(HsCmdArrApp _ fun arg ho_app lr) (_, res_ty) = addErrCtxt (cmdCtxt cmd) $ do { arg_ty <- newOpenFlexiTyVarTy ; let fun_ty = mkCmdArrTy env arg_ty res_ty - ; fun' <- select_arrow_scope (tcLExpr fun (mkCheckExpType fun_ty)) + ; fun' <- select_arrow_scope (tcCheckMonoExpr fun fun_ty) - ; arg' <- tcLExpr arg (mkCheckExpType arg_ty) + ; arg' <- tcCheckMonoExpr arg arg_ty ; return (HsCmdArrApp fun_ty fun' arg' ho_app lr) } where @@ -233,7 +234,7 @@ tc_cmd env cmd@(HsCmdApp x fun arg) (cmd_stk, res_ty) = addErrCtxt (cmdCtxt cmd) $ do { arg_ty <- newOpenFlexiTyVarTy ; fun' <- tcCmd env fun (mkPairTy arg_ty cmd_stk, res_ty) - ; arg' <- tcLExpr arg (mkCheckExpType arg_ty) + ; arg' <- tcCheckMonoExpr arg arg_ty ; return (HsCmdApp x fun' arg') } ------------------------------------------- @@ -310,7 +311,7 @@ tc_cmd env cmd@(HsCmdArrForm x expr f fixity cmd_args) (cmd_stk, res_ty) ; let e_ty = mkInfForAllTy alphaTyVar $ mkVisFunTys cmd_tys $ mkCmdArrTy env (mkPairTy alphaTy cmd_stk) res_ty - ; expr' <- tcCheckExpr expr e_ty + ; expr' <- tcCheckPolyExpr expr e_ty ; return (HsCmdArrForm x expr' f fixity cmd_args') } where diff --git a/compiler/GHC/Tc/Gen/Bind.hs b/compiler/GHC/Tc/Gen/Bind.hs index 1870531f60..bd9d14e2d4 100644 --- a/compiler/GHC/Tc/Gen/Bind.hs +++ b/compiler/GHC/Tc/Gen/Bind.hs @@ -23,8 +23,9 @@ where import GHC.Prelude import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun ) -import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcLExpr ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr ( tcCheckMonoExpr ) import {-# SOURCE #-} GHC.Tc.TyCl.PatSyn ( tcPatSynDecl, tcPatSynBuilderBind ) + import GHC.Core (Tickish (..)) import GHC.Types.CostCentre (mkUserCC, CCFlavour(DeclCC)) import GHC.Driver.Session @@ -354,7 +355,7 @@ tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside = do { ty <- newOpenFlexiTyVarTy ; let p = mkStrLitTy $ hsIPNameFS ip ; ip_id <- newDict ipClass [ p, ty ] - ; expr' <- tcLExpr expr (mkCheckExpType ty) + ; expr' <- tcCheckMonoExpr expr ty ; let d = toDict ipClass p ty `fmap` expr' ; return (ip_id, (IPBind noExtField (Right ip_id) d)) } tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind" @@ -389,22 +390,25 @@ tcValBinds top_lvl binds sigs thing_inside -- It's easier to do so now, once for all the SCCs together -- because a single signature f,g :: <type> -- might relate to more than one SCC - ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $ + (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $ tcTySigs sigs - -- Extend the envt right away with all the Ids - -- declared with complete type signatures - -- Do not extend the TcBinderStack; instead - -- we extend it on a per-rhs basis in tcExtendForRhs - ; tcExtendSigIds top_lvl poly_ids $ do - { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do - { thing <- thing_inside - -- See Note [Pattern synonym builders don't yield dependencies] - -- in GHC.Rename.Bind - ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns - ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ] - ; return (extra_binds, thing) } - ; return (binds' ++ extra_binds', thing) }} + -- Extend the envt right away with all the Ids + -- declared with complete type signatures + -- Do not extend the TcBinderStack; instead + -- we extend it on a per-rhs basis in tcExtendForRhs + -- See Note [Relevant bindings and the binder stack] + ; tcExtendSigIds top_lvl poly_ids $ + do { (binds', (extra_binds', thing)) + <- tcBindGroups top_lvl sig_fn prag_fn binds $ + do { thing <- thing_inside + -- See Note [Pattern synonym builders don't yield dependencies] + -- in GHC.Rename.Bind + ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns + ; let extra_binds = [ (NonRecursive, builder) + | builder <- patsyn_builders ] + ; return (extra_binds, thing) } + ; return (binds' ++ extra_binds', thing) }} where patsyns = getPatSynBinds binds prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds) @@ -686,50 +690,60 @@ tcPolyCheck prag_fn (CompleteSig { sig_bndr = poly_id , sig_ctxt = ctxt , sig_loc = sig_loc }) - (L loc (FunBind { fun_id = (L nm_loc name) - , fun_matches = matches })) - = setSrcSpan sig_loc $ - do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc) - ; (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id - -- See Note [Instantiate sig with fresh variables] + (L bind_loc (FunBind { fun_id = L nm_loc name + , fun_matches = matches })) + = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc) ; mono_name <- newNameAt (nameOccName name) nm_loc - ; ev_vars <- newEvVars theta - ; let mono_id = mkLocalId mono_name tau - skol_info = SigSkol ctxt (idType poly_id) tv_prs - skol_tvs = map snd tv_prs - - ; (ev_binds, (co_fn, matches')) - <- checkConstraints skol_info skol_tvs ev_vars $ - tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $ - tcExtendNameTyVarEnv tv_prs $ - setSrcSpan loc $ - tcMatchesFun (L nm_loc mono_name) matches (mkCheckExpType tau) + ; (wrap_gen, (wrap_res, matches')) + <- setSrcSpan sig_loc $ -- Sets the binding location for the skolems + tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty -> + -- Unwraps multiple layers; e.g + -- f :: forall a. Eq a => forall b. Ord b => blah + -- NB: tcSkolemise makes fresh type variables + -- See Note [Instantiate sig with fresh variables] + + let mono_id = mkLocalId mono_name rho_ty in + tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $ + -- Why mono_id in the BinderStack? + -- See Note [Relevant bindings and the binder stack] + + setSrcSpan bind_loc $ + tcMatchesFun (L nm_loc mono_name) matches + (mkCheckExpType rho_ty) + + -- We make a funny AbsBinds, abstracting over nothing, + -- just so we haev somewhere to put the SpecPrags. + -- Otherwise we could just use the FunBind + -- Hence poly_id2 is just a clone of poly_id; + -- We re-use mono-name, but we could equally well use a fresh one ; let prag_sigs = lookupPragEnv prag_fn name - ; spec_prags <- tcSpecPrags poly_id prag_sigs + poly_id2 = mkLocalId mono_name (idType poly_id) + ; spec_prags <- tcSpecPrags poly_id prag_sigs ; poly_id <- addInlinePrags poly_id prag_sigs ; mod <- getModule - ; tick <- funBindTicks nm_loc mono_id mod prag_sigs - ; let bind' = FunBind { fun_id = L nm_loc mono_id + ; tick <- funBindTicks nm_loc poly_id mod prag_sigs + + ; let bind' = FunBind { fun_id = L nm_loc poly_id2 , fun_matches = matches' - , fun_ext = co_fn + , fun_ext = wrap_gen <.> wrap_res , fun_tick = tick } export = ABE { abe_ext = noExtField , abe_wrap = idHsWrapper , abe_poly = poly_id - , abe_mono = mono_id + , abe_mono = poly_id2 , abe_prags = SpecPrags spec_prags } - abs_bind = L loc $ + abs_bind = L bind_loc $ AbsBinds { abs_ext = noExtField - , abs_tvs = skol_tvs - , abs_ev_vars = ev_vars - , abs_ev_binds = [ev_binds] + , abs_tvs = [] + , abs_ev_vars = [] + , abs_ev_binds = [] , abs_exports = [export] - , abs_binds = unitBag (L loc bind') + , abs_binds = unitBag (L bind_loc bind') , abs_sig = True } ; return (unitBag abs_bind, [poly_id]) } @@ -862,7 +876,7 @@ mkExport prag_fn insoluble qtvs theta -- 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) $ - tcSubType_NC sig_ctxt sel_poly_ty poly_ty + tcSubTypeSigma sig_ctxt sel_poly_ty poly_ty ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures ; when warn_missing_sigs $ @@ -943,8 +957,12 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs , sig_inst_theta = annotated_theta , sig_inst_skols = annotated_tvs })) = -- Choose quantifiers for a partial type signature - do { psig_qtvbndr_prs <- zonkTyVarTyVarPairs annotated_tvs - ; let psig_qtv_prs = mapSnd binderVar psig_qtvbndr_prs + do { let (psig_qtv_nms, psig_qtv_bndrs) = unzip annotated_tvs + ; psig_qtv_bndrs <- mapM zonkInvisTVBinder psig_qtv_bndrs + ; let psig_qtvs = map binderVar psig_qtv_bndrs + psig_qtv_set = mkVarSet psig_qtvs + psig_qtv_prs = psig_qtv_nms `zip` psig_qtvs + -- Check whether the quantified variables of the -- partial signature have been unified together @@ -958,17 +976,14 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs , not (tv `elem` qtvs) ] - ; let psig_qtvbndrs = map snd psig_qtvbndr_prs - psig_qtvs = mkVarSet (map snd psig_qtv_prs) - ; annotated_theta <- zonkTcTypes annotated_theta - ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx + ; (free_tvs, my_theta) <- choose_psig_context psig_qtv_set annotated_theta wcx - ; let keep_me = free_tvs `unionVarSet` psig_qtvs + ; let keep_me = free_tvs `unionVarSet` psig_qtv_set final_qtvs = [ mkTyVarBinder vis tv | tv <- qtvs -- Pulling from qtvs maintains original order , tv `elemVarSet` keep_me - , let vis = case lookupVarBndr tv psig_qtvbndrs of + , let vis = case lookupVarBndr tv psig_qtv_bndrs of Just spec -> spec Nothing -> InferredSpec ] @@ -1454,17 +1469,7 @@ tcExtendTyVarEnvFromSig sig_inst thing_inside thing_inside tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a --- Extend the TcBinderStack for the RHS of the binding, with --- the monomorphic Id. That way, if we have, say --- f = \x -> blah --- and something goes wrong in 'blah', we get a "relevant binding" --- looking like f :: alpha -> beta --- This applies if 'f' has a type signature too: --- f :: forall a. [a] -> [a] --- f x = True --- We can't unify True with [a], and a relevant binding is f :: [a] -> [a] --- If we had the *polymorphic* version of f in the TcBinderStack, it --- would not be reported as relevant, because its type is closed +-- See Note [Relevant bindings and the binder stack] tcExtendIdBinderStackForRhs infos thing_inside = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel | MBI { mbi_mono_id = mono_id } <- infos ] @@ -1480,7 +1485,22 @@ getMonoBindInfo tc_binds get_info (TcPatBind infos _ _ _) rest = infos ++ rest -{- Note [Typechecking pattern bindings] +{- Note [Relevant bindings and the binder stack] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When typecking a binding we extend the TcBinderStack for the RHS of +the binding, with the /monomorphic/ Id. That way, if we have, say + f = \x -> blah +and something goes wrong in 'blah', we get a "relevant binding" +looking like f :: alpha -> beta +This applies if 'f' has a type signature too: + f :: forall a. [a] -> [a] + f x = True +We can't unify True with [a], and a relevant binding is f :: [a] -> [a] +If we had the *polymorphic* version of f in the TcBinderStack, it +would not be reported as relevant, because its type is closed. +(See TcErrors.relevantBindings.) + +Note [Typechecking pattern bindings] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Look at: - typecheck/should_compile/ExPat diff --git a/compiler/GHC/Tc/Gen/Default.hs b/compiler/GHC/Tc/Gen/Default.hs index ab5e021653..9f31d7938a 100644 --- a/compiler/GHC/Tc/Gen/Default.hs +++ b/compiler/GHC/Tc/Gen/Default.hs @@ -70,8 +70,8 @@ tcDefaults decls@(L locn (DefaultDecl _ _) : _) tc_default_ty :: [Class] -> LHsType GhcRn -> TcM Type tc_default_ty deflt_clss hs_ty - = do { (ty, _kind) <- solveEqualities $ - tcLHsType hs_ty + = do { ty <- solveEqualities $ + tcInferLHsType hs_ty ; ty <- zonkTcTypeToType ty -- establish Type invariants ; checkValidType DefaultDeclCtxt ty diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs index 2d6b25df10..b4c3b6275c 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs +++ b/compiler/GHC/Tc/Gen/Expr.hs @@ -13,20 +13,15 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} --- | Typecheck an expression module GHC.Tc.Gen.Expr - ( tcCheckExpr - , tcLExpr, tcLExprNC, tcExpr - , tcInferSigma - , tcInferRho, tcInferRhoNC - , tcSyntaxOp, tcSyntaxOpGen - , SyntaxOpType(..) - , synKnownType - , tcCheckId - , addAmbiguousNameErr - , getFixedTyVars - ) -where + ( tcCheckPolyExpr, + tcCheckMonoExpr, tcCheckMonoExprNC, tcMonoExpr, tcMonoExprNC, + tcInferSigma, tcInferRho, tcInferRhoNC, + tcExpr, + tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType, + tcCheckId, + addAmbiguousNameErr, + getFixedTyVars ) where #include "HsVersions.h" @@ -101,25 +96,35 @@ import qualified Data.Set as Set ************************************************************************ -} -tcCheckExpr, tcCheckExprNC + +tcCheckPolyExpr, tcCheckPolyExprNC :: LHsExpr GhcRn -- Expression to type check -> TcSigmaType -- Expected type (could be a polytype) -> TcM (LHsExpr GhcTc) -- Generalised expr with expected type --- tcCheckExpr is a convenient place (frequent but not too frequent) +-- tcCheckPolyExpr is a convenient place (frequent but not too frequent) -- place to add context information. -- The NC version does not do so, usually because the caller wants -- to do so himself. -tcCheckExpr expr res_ty +tcCheckPolyExpr expr res_ty = tcPolyExpr expr (mkCheckExpType res_ty) +tcCheckPolyExprNC expr res_ty = tcPolyExprNC expr (mkCheckExpType res_ty) + +-- These versions take an ExpType +tcPolyExpr, tcPolyExprNC + :: LHsExpr GhcRn -> ExpSigmaType + -> TcM (LHsExpr GhcTcId) + +tcPolyExpr expr res_ty = addExprCtxt expr $ - tcCheckExprNC expr res_ty + do { traceTc "tcPolyExpr" (ppr res_ty) + ; tcPolyExprNC expr res_ty } -tcCheckExprNC (L loc expr) res_ty +tcPolyExprNC (L loc expr) res_ty = setSrcSpan loc $ - do { traceTc "tcCheckExprNC" (ppr res_ty) - ; (wrap, expr') <- tcSkolemise GenSigCtxt res_ty $ \ _ res_ty -> - tcExpr expr (mkCheckExpType res_ty) + do { traceTc "tcPolyExprNC" (ppr res_ty) + ; (wrap, expr') <- tcSkolemiseET GenSigCtxt res_ty $ \ res_ty -> + tcExpr expr res_ty ; return $ L loc (mkHsWrap wrap expr') } --------------- @@ -134,6 +139,30 @@ tcInferSigma le@(L loc expr) ; return (L loc (applyHsArgs fun args), ty) } --------------- +tcCheckMonoExpr, tcCheckMonoExprNC + :: LHsExpr GhcRn -- Expression to type check + -> TcRhoType -- Expected type + -- Definitely no foralls at the top + -> TcM (LHsExpr GhcTcId) +tcCheckMonoExpr expr res_ty = tcMonoExpr expr (mkCheckExpType res_ty) +tcCheckMonoExprNC expr res_ty = tcMonoExprNC expr (mkCheckExpType res_ty) + +tcMonoExpr, tcMonoExprNC + :: LHsExpr GhcRn -- Expression to type check + -> ExpRhoType -- Expected type + -- Definitely no foralls at the top + -> TcM (LHsExpr GhcTcId) + +tcMonoExpr expr res_ty + = addExprCtxt expr $ + tcMonoExprNC expr res_ty + +tcMonoExprNC (L loc expr) res_ty + = setSrcSpan loc $ + do { expr' <- tcExpr expr res_ty + ; return (L loc expr') } + +--------------- tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType) -- Infer a *rho*-type. The return type is always instantiated. tcInferRho le = addExprCtxt le (tcInferRhoNC le) @@ -144,15 +173,11 @@ tcInferRhoNC (L loc expr) ; return (L loc expr', rho) } -{- -************************************************************************ +{- ********************************************************************* * * tcExpr: the main expression typechecker * * -************************************************************************ - -NB: The res_ty is always deeply skolemised. --} +********************************************************************* -} tcLExpr, tcLExprNC :: LHsExpr GhcRn -- Expression to type check @@ -241,7 +266,7 @@ tcExpr e@(HsOverLabel _ mb_fromLabel l) res_ty (mkEmptyWildCardBndrs (L loc (HsTyLit noExtField (HsStrTy NoSourceText l)))) tcExpr (HsLam x match) res_ty - = do { (match', wrap) <- tcMatchLambda herald match_ctxt match res_ty + = do { (wrap, match') <- tcMatchLambda herald match_ctxt match res_ty ; return (mkHsWrap wrap (HsLam x match')) } where match_ctxt = MC { mc_what = LambdaExpr, mc_body = tcBody } @@ -252,7 +277,7 @@ tcExpr (HsLam x match) res_ty text "has"] tcExpr e@(HsLamCase x matches) res_ty - = do { (matches', wrap) + = do { (wrap, matches') <- tcMatchLambda msg match_ctxt matches res_ty -- The laziness annotation is because we don't want to fail here -- if there are multiple arguments @@ -335,7 +360,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty ; let doc = text "The first argument of ($) takes" orig1 = lexprCtOrigin arg1 ; (wrap_arg1, [arg2_sigma], op_res_ty) <- - matchActualFunTys doc orig1 (Just (unLoc arg1)) 1 arg1_ty + matchActualFunTysRho doc orig1 (Just (unLoc arg1)) 1 arg1_ty -- We have (arg1 $ arg2) -- So: arg1_ty = arg2_ty -> op_res_ty @@ -351,7 +376,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty (tcTypeKind arg2_sigma) liftedTypeKind -- Ignore the evidence. arg2_sigma must have type * or #, -- because we know (arg2_sigma -> op_res_ty) is well-kinded - -- (because otherwise matchActualFunTys would fail) + -- (because otherwise matchActualFunTysRho would fail) -- So this 'unifyKind' will either succeed with Refl, or will -- produce an insoluble constraint * ~ #, which we'll report later. @@ -385,7 +410,8 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty ; (op', op_ty) <- tcInferRhoNC op ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) - <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty + <- matchActualFunTysRho (mk_op_msg op) fn_orig + (Just (unLoc op)) 2 op_ty -- You might think we should use tcInferApp here, but there is -- too much impedance-matching, because tcApp may return wrappers as -- well as type-checked arguments. @@ -405,12 +431,13 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty tcExpr expr@(SectionR x op arg2) res_ty = do { (op', op_ty) <- tcInferRhoNC op ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) - <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty - ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr) - (mkVisFunTy arg1_ty op_res_ty) res_ty + <- matchActualFunTysRho (mk_op_msg op) fn_orig + (Just (unLoc op)) 2 op_ty ; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2 - ; return ( mkHsWrap wrap_res $ - SectionR x (mkLHsWrap wrap_fun op') arg2' ) } + ; let expr' = SectionR x (mkLHsWrap wrap_fun op') arg2' + act_res_ty = mkVisFunTy arg1_ty op_res_ty + ; tcWrapResultMono expr expr' act_res_ty res_ty } + where fn_orig = lexprCtOrigin op -- It's important to use the origin of 'op', so that call-stacks @@ -424,13 +451,12 @@ tcExpr expr@(SectionL x arg1 op) res_ty | otherwise = 2 ; (wrap_fn, (arg1_ty:arg_tys), op_res_ty) - <- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) - n_reqd_args op_ty - ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr) - (mkVisFunTys arg_tys op_res_ty) res_ty + <- matchActualFunTysRho (mk_op_msg op) fn_orig + (Just (unLoc op)) n_reqd_args op_ty ; arg1' <- tcArg (unLoc op) arg1 arg1_ty 1 - ; return ( mkHsWrap wrap_res $ - SectionL x arg1' (mkLHsWrap wrap_fn op') ) } + ; let expr' = SectionL x arg1' (mkLHsWrap wrap_fn op') + act_res_ty = mkVisFunTys arg_tys op_res_ty + ; tcWrapResultMono expr expr' act_res_ty res_ty } where fn_orig = lexprCtOrigin op -- It's important to use the origin of 'op', so that call-stacks @@ -460,19 +486,19 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty ; arg_tys <- case boxity of { Boxed -> newFlexiTyVarTys arity liftedTypeKind ; Unboxed -> replicateM arity newOpenFlexiTyVarTy } - ; let actual_res_ty - = mkVisFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args] - (mkTupleTy1 boxity arg_tys) - -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make - - ; wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "ExpTuple") - (Just expr) - actual_res_ty res_ty -- Handle tuple sections where ; tup_args1 <- tcTupArgs tup_args arg_tys - ; return $ mkHsWrap wrap (ExplicitTuple x tup_args1 boxity) } + ; let expr' = ExplicitTuple x tup_args1 boxity + act_res_ty = mkVisFunTys [ty | (ty, (L _ (Missing _))) + <- arg_tys `zip` tup_args] + (mkTupleTy1 boxity arg_tys) + -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make + + ; traceTc "ExplicitTuple" (ppr act_res_ty $$ ppr res_ty) + + ; tcWrapResultMono expr expr' act_res_ty res_ty } tcExpr (ExplicitSum _ alt arity expr) res_ty = do { let sum_tc = sumTyCon arity @@ -480,7 +506,7 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty ; (coi, arg_tys) <- matchExpectedTyConApp sum_tc res_ty ; -- Drop levity vars, we don't care about them here let arg_tys' = drop arity arg_tys - ; expr' <- tcCheckExpr expr (arg_tys' `getNth` (alt - 1)) + ; expr' <- tcCheckPolyExpr expr (arg_tys' `getNth` (alt - 1)) ; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) } -- This will see the empty list only when -XOverloadedLists. @@ -502,7 +528,7 @@ tcExpr (ExplicitList _ witness exprs) res_ty ; return (exprs', elt_ty) } ; return $ ExplicitList elt_ty (Just fln') exprs' } - where tc_elt elt_ty expr = tcCheckExpr expr elt_ty + where tc_elt elt_ty expr = tcCheckPolyExpr expr elt_ty {- ************************************************************************ @@ -527,6 +553,13 @@ tcExpr (HsCase x scrut matches) res_ty -- -- But now, in the GADT world, we need to typecheck the scrutinee -- first, to get type info that may be refined in the case alternatives + + -- Typecheck the scrutinee. We use tcInferRho but tcInferSigma + -- would also be possible (tcMatchesCase accepts sigma-types) + -- Interesting litmus test: do these two behave the same? + -- case id of {..} + -- case (\v -> v) of {..} + -- This design choice is discussed in #17790 (scrut', scrut_ty) <- tcInferRho scrut ; traceTc "HsCase" (ppr scrut_ty) @@ -550,9 +583,9 @@ tcExpr (HsIf x fun@(SyntaxExprRn {}) pred b1 b2) res_ty = do { ((pred', b1', b2'), fun') <- tcSyntaxOp IfOrigin fun [SynAny, SynAny, SynAny] res_ty $ \ [pred_ty, b1_ty, b2_ty] -> - do { pred' <- tcCheckExpr pred pred_ty - ; b1' <- tcCheckExpr b1 b1_ty - ; b2' <- tcCheckExpr b2 b2_ty + do { pred' <- tcCheckPolyExpr pred pred_ty + ; b1' <- tcCheckPolyExpr b1 b1_ty + ; b2' <- tcCheckPolyExpr b2 b2_ty ; return (pred', b1', b2') } ; return (HsIf x fun' pred' b1' b2') } @@ -591,7 +624,7 @@ tcExpr (HsStatic fvs expr) res_ty addErrCtxt (hang (text "In the body of a static form:") 2 (ppr expr) ) $ - tcCheckExprNC expr expr_ty + tcCheckPolyExprNC expr expr_ty -- Check that the free variables of the static form are closed. -- It's OK to use nonDetEltsUniqSet here as the only side effects of @@ -637,25 +670,26 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name ; checkMissingFields con_like rbinds ; (con_expr, con_sigma) <- tcInferId con_name - ; (con_wrap, con_tau) <- - topInstantiate (OccurrenceOf con_name) con_sigma + ; (con_wrap, con_tau) <- topInstantiate orig con_sigma -- a shallow instantiation should really be enough for -- a data constructor. ; let arity = conLikeArity con_like Right (arg_tys, actual_res_ty) = tcSplitFunTysN arity con_tau - ; case conLikeWrapId_maybe con_like of - Nothing -> nonBidirectionalErr (conLikeName con_like) - Just con_id -> do { - res_wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "RecordCon") - (Just expr) actual_res_ty res_ty - ; rbinds' <- tcRecordBinds con_like arg_tys rbinds - ; return $ - mkHsWrap res_wrap $ - RecordCon { rcon_ext = RecordConTc - { rcon_con_like = con_like - , rcon_con_expr = mkHsWrap con_wrap con_expr } - , rcon_con_name = L loc con_id - , rcon_flds = rbinds' } } } + ; case conLikeWrapId_maybe con_like of { + Nothing -> nonBidirectionalErr (conLikeName con_like) ; + Just con_id -> + + do { rbinds' <- tcRecordBinds con_like arg_tys rbinds + ; let rcon_tc = RecordConTc + { rcon_con_like = con_like + , rcon_con_expr = mkHsWrap con_wrap con_expr } + expr' = RecordCon { rcon_ext = rcon_tc + , rcon_con_name = L loc con_id + , rcon_flds = rbinds' } + + ; tcWrapResultMono expr expr' actual_res_ty res_ty } } } + where + orig = OccurrenceOf con_name {- Note [Type of a record update] @@ -906,8 +940,6 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty scrut_ty = TcType.substTy scrut_subst con1_res_ty con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys - ; wrap_res <- tcSubTypeHR (exprCtOrigin expr) - (Just expr) rec_res_ty res_ty ; co_scrut <- unifyType (Just (unLoc record_expr)) record_rho scrut_ty -- NB: normal unification is OK here (as opposed to subsumption), -- because for this to work out, both record_rho and scrut_ty have @@ -937,16 +969,16 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty ; req_wrap <- instCallConstraints RecordUpdOrigin req_theta' -- Phew! - ; return $ - mkHsWrap wrap_res $ - RecordUpd { rupd_expr - = mkLHsWrap fam_co (mkLHsWrapCo co_scrut record_expr') - , rupd_flds = rbinds' - , rupd_ext = RecordUpdTc - { rupd_cons = relevant_cons - , rupd_in_tys = scrut_inst_tys - , rupd_out_tys = result_inst_tys - , rupd_wrap = req_wrap }} } + ; let upd_tc = RecordUpdTc { rupd_cons = relevant_cons + , rupd_in_tys = scrut_inst_tys + , rupd_out_tys = result_inst_tys + , rupd_wrap = req_wrap } + expr' = RecordUpd { rupd_expr = mkLHsWrap fam_co $ + mkLHsWrapCo co_scrut record_expr' + , rupd_flds = rbinds' + , rupd_ext = upd_tc } + + ; tcWrapResult expr expr' rec_res_ty res_ty } tcExpr e@(HsRecFld _ f) res_ty = tcCheckRecSelId e f res_ty @@ -1038,7 +1070,7 @@ tcArithSeq :: Maybe (SyntaxExpr GhcRn) -> ArithSeqInfo GhcRn -> ExpRhoType tcArithSeq witness seq@(From expr) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr' <- tcCheckExpr expr elt_ty + ; expr' <- tcCheckPolyExpr expr elt_ty ; enum_from <- newMethodFromName (ArithSeqOrigin seq) enumFromName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1046,8 +1078,8 @@ tcArithSeq witness seq@(From expr) res_ty tcArithSeq witness seq@(FromThen expr1 expr2) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckExpr expr1 elt_ty - ; expr2' <- tcCheckExpr expr2 elt_ty + ; expr1' <- tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcCheckPolyExpr expr2 elt_ty ; enum_from_then <- newMethodFromName (ArithSeqOrigin seq) enumFromThenName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1055,8 +1087,8 @@ tcArithSeq witness seq@(FromThen expr1 expr2) res_ty tcArithSeq witness seq@(FromTo expr1 expr2) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckExpr expr1 elt_ty - ; expr2' <- tcCheckExpr expr2 elt_ty + ; expr1' <- tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcCheckPolyExpr expr2 elt_ty ; enum_from_to <- newMethodFromName (ArithSeqOrigin seq) enumFromToName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1064,9 +1096,9 @@ tcArithSeq witness seq@(FromTo expr1 expr2) res_ty tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty = do { (wrap, elt_ty, wit') <- arithSeqEltType witness res_ty - ; expr1' <- tcCheckExpr expr1 elt_ty - ; expr2' <- tcCheckExpr expr2 elt_ty - ; expr3' <- tcCheckExpr expr3 elt_ty + ; expr1' <- tcCheckPolyExpr expr1 elt_ty + ; expr2' <- tcCheckPolyExpr expr2 elt_ty + ; expr3' <- tcCheckPolyExpr expr3 elt_ty ; eft <- newMethodFromName (ArithSeqOrigin seq) enumFromThenToName [elt_ty] ; return $ mkHsWrap wrap $ @@ -1251,13 +1283,11 @@ tcInferApp expr Nothing -> thing_inside -- Don't set the location twice Just loc -> setSrcSpan loc thing_inside ---------------------- tcInferApp_finish :: HsExpr GhcRn -- Renamed function -> HsExpr GhcTc -> TcSigmaType -- Function and its type -> [LHsExprArgIn] -- Arguments -> TcM (HsExpr GhcTc, [LHsExprArgOut], TcSigmaType) - tcInferApp_finish rn_fun tc_fun fun_sigma rn_args = do { (tc_args, actual_res_ty) <- tcArgs rn_fun fun_sigma rn_args ; return (tc_fun, tc_args, actual_res_ty) } @@ -1364,9 +1394,9 @@ tcArgs fun orig_fun_ty orig_args _ -> ty_app_err upsilon_ty hs_ty_arg } go n so_far fun_ty (HsEValArg loc arg : args) - = do { (wrap, [arg_ty], res_ty) - <- matchActualFunTysPart herald fun_orig (Just fun) - n_val_args so_far 1 fun_ty + = do { (wrap, arg_ty, res_ty) + <- matchActualFunTySigma herald fun_orig (Just fun) + (n_val_args, so_far) fun_ty ; arg' <- tcArg fun arg arg_ty n ; (args', inner_res_ty) <- go (n+1) (arg_ty:so_far) res_ty args ; return ( addArgWrap wrap $ HsEValArg loc arg' : args' @@ -1465,13 +1495,12 @@ tcArg :: HsExpr GhcRn -- The function (for error messages) -> Int -- # of argument -> TcM (LHsExpr GhcTc) -- Resulting argument tcArg fun arg ty arg_no - = addErrCtxt (funAppCtxt fun arg arg_no) $ - do { traceTc "tcArg {" $ - vcat [ text "arg #" <> ppr arg_no <+> dcolon <+> ppr ty - , text "arg:" <+> ppr arg ] - ; arg' <- tcCheckExprNC arg ty - ; traceTc "tcArg }" empty - ; return arg' } + = addErrCtxt (funAppCtxt fun arg arg_no) $ + do { traceTc "tcArg" $ + vcat [ ppr arg_no <+> text "of" <+> ppr fun + , text "arg type:" <+> ppr ty + , text "arg:" <+> ppr arg ] + ; tcCheckPolyExprNC arg ty } ---------------- tcTupArgs :: [LHsTupArg GhcRn] -> [TcSigmaType] -> TcM [LHsTupArg GhcTc] @@ -1479,7 +1508,7 @@ tcTupArgs args tys = ASSERT( equalLength args tys ) mapM go (args `zip` tys) where go (L l (Missing {}), arg_ty) = return (L l (Missing arg_ty)) - go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckExpr expr arg_ty + go (L l (Present x expr), arg_ty) = do { expr' <- tcCheckPolyExpr expr arg_ty ; return (L l (Present x expr')) } --------------------------- @@ -1536,7 +1565,7 @@ tcSynArgE :: CtOrigin -- ^ returns a wrapper :: (type of right shape) "->" (type passed in) tcSynArgE orig sigma_ty syn_ty thing_inside = do { (skol_wrap, (result, ty_wrapper)) - <- tcSkolemise GenSigCtxt sigma_ty $ \ _ rho_ty -> + <- tcSkolemise GenSigCtxt sigma_ty $ \ rho_ty -> go rho_ty syn_ty ; return (result, skol_wrap <.> ty_wrapper) } where @@ -1554,11 +1583,11 @@ tcSynArgE orig sigma_ty syn_ty thing_inside ; return (result, mkWpCastN list_co) } go rho_ty (SynFun arg_shape res_shape) - = do { ( ( ( (result, arg_ty, res_ty) - , res_wrapper ) -- :: res_ty_out "->" res_ty - , arg_wrapper1, [], arg_wrapper2 ) -- :: arg_ty "->" arg_ty_out - , match_wrapper ) -- :: (arg_ty -> res_ty) "->" rho_ty - <- matchExpectedFunTys herald 1 (mkCheckExpType rho_ty) $ + = do { ( match_wrapper -- :: (arg_ty -> res_ty) "->" rho_ty + , ( ( (result, arg_ty, res_ty) + , res_wrapper ) -- :: res_ty_out "->" res_ty + , arg_wrapper1, [], arg_wrapper2 ) ) -- :: arg_ty "->" arg_ty_out + <- matchExpectedFunTys herald GenSigCtxt 1 (mkCheckExpType rho_ty) $ \ [arg_ty] res_ty -> do { arg_tc_ty <- expTypeToType arg_ty ; res_tc_ty <- expTypeToType res_ty @@ -1604,7 +1633,8 @@ tcSynArgA :: CtOrigin -- and a wrapper to be applied to the overall expression tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside = do { (match_wrapper, arg_tys, res_ty) - <- matchActualFunTys herald orig Nothing (length arg_shapes) sigma_ty + <- matchActualFunTysRho herald orig Nothing + (length arg_shapes) sigma_ty -- match_wrapper :: sigma_ty "->" (arg_tys -> res_ty) ; ((result, res_wrapper), arg_wrappers) <- tc_syn_args_e arg_tys arg_shapes $ \ arg_results -> @@ -1634,7 +1664,7 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside = do { result <- thing_inside [res_ty] ; return (result, idHsWrapper) } tc_syn_arg res_ty SynRho thing_inside - = do { (inst_wrap, rho_ty) <- deeplyInstantiate orig res_ty + = do { (inst_wrap, rho_ty) <- topInstantiate orig res_ty -- inst_wrap :: res_ty "->" rho_ty ; result <- thing_inside [rho_ty] ; return (result, inst_wrap) } @@ -1648,7 +1678,7 @@ tcSynArgA orig sigma_ty arg_shapes res_shape thing_inside tc_syn_arg _ (SynFun {}) _ = pprPanic "tcSynArgA hits a SynFun" (ppr orig) tc_syn_arg res_ty (SynType the_ty) thing_inside - = do { wrap <- tcSubTypeO orig GenSigCtxt res_ty the_ty + = do { wrap <- tcSubType orig GenSigCtxt res_ty the_ty ; result <- thing_inside [] ; return (result, wrap) } @@ -1687,22 +1717,10 @@ in the other order, the extra signature in f2 is reqd. 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 { (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id - ; given <- newEvVars theta - ; traceTc "tcExprSig: CompleteSig" $ - vcat [ text "poly_id:" <+> ppr poly_id <+> dcolon <+> ppr (idType poly_id) - , text "tv_prs:" <+> ppr tv_prs ] - - ; let skol_info = SigSkol ExprSigCtxt (idType poly_id) tv_prs - skol_tvs = map snd tv_prs - ; (ev_binds, expr') <- checkConstraints skol_info skol_tvs given $ - tcExtendNameTyVarEnv tv_prs $ - tcCheckExprNC expr tau - - ; let poly_wrap = mkWpTyLams skol_tvs - <.> mkWpLams given - <.> mkWpLet ev_binds - ; return (mkLHsWrap poly_wrap expr', idType poly_id) } + 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 @@ -1711,7 +1729,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) do { sig_inst <- tcInstSig sig ; expr' <- tcExtendNameTyVarEnv (mapSnd binderVar $ sig_inst_skols sig_inst) $ tcExtendNameTyVarEnv (sig_inst_wcs sig_inst) $ - tcCheckExprNC expr (sig_inst_tau 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 @@ -1735,7 +1753,7 @@ tcExprSig expr sig@(PartialSig { psig_name = name, sig_loc = loc }) 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 tcSubType_NC ExprSigCtxt inferred_sigma my_sigma + else tcSubTypeSigma ExprSigCtxt inferred_sigma my_sigma ; traceTc "tcExpSig" (ppr qtvs $$ ppr givens $$ ppr inferred_sigma $$ ppr my_sigma) ; let poly_wrap = wrap @@ -2476,7 +2494,7 @@ tcRecordField :: ConLike -> Assoc Name Type tcRecordField con_like flds_w_tys (L loc (FieldOcc sel_name lbl)) rhs | Just field_ty <- assocMaybe flds_w_tys sel_name = addErrCtxt (fieldCtxt field_lbl) $ - do { rhs' <- tcCheckExprNC rhs field_ty + do { rhs' <- tcCheckPolyExprNC rhs field_ty ; let field_id = mkUserLocal (nameOccName sel_name) (nameUnique sel_name) field_ty loc @@ -2584,7 +2602,7 @@ addFunResCtxt has_args fun fun_res_ty env_ty -- function types] (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res' -- No need to call tcSplitNestedSigmaTys here, since env_ty is - -- an ExpRhoTy, i.e., it's already deeply instantiated. + -- an ExpRhoTy, i.e., it's already instantiated. (_, _, env_tau) = tcSplitSigmaTy env' (args_fun, res_fun) = tcSplitFunTys fun_tau (args_env, res_env) = tcSplitFunTys env_tau diff --git a/compiler/GHC/Tc/Gen/Expr.hs-boot b/compiler/GHC/Tc/Gen/Expr.hs-boot index d9138a4d7e..1f26ef242a 100644 --- a/compiler/GHC/Tc/Gen/Expr.hs-boot +++ b/compiler/GHC/Tc/Gen/Expr.hs-boot @@ -6,16 +6,26 @@ import GHC.Tc.Types ( TcM ) import GHC.Tc.Types.Origin ( CtOrigin ) import GHC.Hs.Extension ( GhcRn, GhcTcId ) -tcCheckExpr :: LHsExpr GhcRn -> TcSigmaType -> TcM (LHsExpr GhcTcId) - -tcLExpr, tcLExprNC - :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId) -tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId) - -tcInferRho, tcInferRhoNC - :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcRhoType) - -tcInferSigma :: LHsExpr GhcRn-> TcM (LHsExpr GhcTcId, TcSigmaType) +tcCheckPolyExpr :: + LHsExpr GhcRn + -> TcSigmaType + -> TcM (LHsExpr GhcTcId) + +tcMonoExpr, tcMonoExprNC :: + LHsExpr GhcRn + -> ExpRhoType + -> TcM (LHsExpr GhcTcId) +tcCheckMonoExpr, tcCheckMonoExprNC :: + LHsExpr GhcRn + -> TcRhoType + -> TcM (LHsExpr GhcTcId) + +tcExpr :: HsExpr GhcRn -> ExpRhoType -> TcM (HsExpr GhcTcId) + +tcInferSigma :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType) + +tcInferRho, tcInferRhoNC :: + LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcRhoType) tcSyntaxOp :: CtOrigin -> SyntaxExprRn diff --git a/compiler/GHC/Tc/Gen/Foreign.hs b/compiler/GHC/Tc/Gen/Foreign.hs index 8163e6820d..06febcef33 100644 --- a/compiler/GHC/Tc/Gen/Foreign.hs +++ b/compiler/GHC/Tc/Gen/Foreign.hs @@ -388,7 +388,7 @@ tcFExport fo@(ForeignExport { fd_name = L loc nm, fd_sig_ty = hs_ty, fd_fe = spe = addErrCtxt (foreignDeclCtxt fo) $ do sig_ty <- tcHsSigType (ForSigCtxt nm) hs_ty - rhs <- tcCheckExpr (nlHsVar nm) sig_ty + rhs <- tcCheckPolyExpr (nlHsVar nm) sig_ty (norm_co, norm_sig_ty, gres) <- normaliseFfiType sig_ty diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs index 328ed43d65..2c2345724f 100644 --- a/compiler/GHC/Tc/Gen/HsType.hs +++ b/compiler/GHC/Tc/Gen/HsType.hs @@ -31,8 +31,8 @@ module GHC.Tc.Gen.HsType ( bindExplicitTKBndrs_Q_Tv, bindExplicitTKBndrs_Q_Skol, ContextKind(..), - -- Type checking type and class decls - bindTyClTyVars, + -- Type checking type and class decls, and instances thereof + bindTyClTyVars, tcFamTyPats, etaExpandAlgTyCon, tcbVisibilities, -- tyvars @@ -46,13 +46,11 @@ module GHC.Tc.Gen.HsType ( tcNamedWildCardBinders, tcHsLiftedType, tcHsOpenType, tcHsLiftedTypeNC, tcHsOpenTypeNC, - tcLHsType, tcLHsTypeUnsaturated, tcCheckLHsType, - tcHsMbContext, tcHsContext, tcLHsPredType, tcInferApps, + tcInferLHsType, tcInferLHsTypeUnsaturated, tcCheckLHsType, + tcHsMbContext, tcHsContext, tcLHsPredType, failIfEmitsConstraints, solveEqualities, -- useful re-export - typeLevelMode, kindLevelMode, - kindGeneralizeAll, kindGeneralizeSome, kindGeneralizeNone, -- Sort-checking kinds @@ -115,6 +113,7 @@ import GHC.Driver.Session import qualified GHC.LanguageExtensions as LangExt import GHC.Data.Maybe +import GHC.Data.Bag( unitBag ) import Data.List ( find ) import Control.Monad @@ -159,6 +158,91 @@ checking until step (3). Check types AND do validity checking * * ************************************************************************ + +Note [Keeping implicitly quantified variables in order] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When the user implicitly quantifies over variables (say, in a type +signature), we need to come up with some ordering on these variables. +This is done by bumping the TcLevel, bringing the tyvars into scope, +and then type-checking the thing_inside. The constraints are all +wrapped in an implication, which is then solved. Finally, we can +zonk all the binders and then order them with scopedSort. + +It's critical to solve before zonking and ordering in order to uncover +any unifications. You might worry that this eager solving could cause +trouble elsewhere. I don't think it will. Because it will solve only +in an increased TcLevel, it can't unify anything that was mentioned +elsewhere. Additionally, we require that the order of implicitly +quantified variables is manifest by the scope of these variables, so +we're not going to learn more information later that will help order +these variables. + +Note [Recipe for checking a signature] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Checking a user-written signature requires several steps: + + 1. Generate constraints. + 2. Solve constraints. + 3. Promote tyvars and/or kind-generalize. + 4. Zonk. + 5. Check validity. + +There may be some surprises in here: + +Step 2 is necessary for two reasons: most signatures also bring +implicitly quantified variables into scope, and solving is necessary +to get these in the right order (see Note [Keeping implicitly +quantified variables in order]). Additionally, solving is necessary in +order to kind-generalize correctly: otherwise, we do not know which +metavariables are left unsolved. + +Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to +kindGeneralize{All,Some,None}. Here, we have to deal with the fact that +metatyvars generated in the type may 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 + (B) promoted, or See Note [Promotion in signatures] + (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType + +The kindGeneralize functions do not require pre-zonking; they zonk as they +go. + +If you are actually doing kind-generalization, you need to bump the level +before generating constraints, as we will only generalize variables with +a TcLevel higher than the ambient one. + +After promoting/generalizing, we need to zonk again because both +promoting and generalizing fill in metavariables. + +Note [Promotion in signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +If an unsolved metavariable in a signature is not generalized +(because we're not generalizing the construct -- e.g., pattern +sig -- or because the metavars are constrained -- see kindGeneralizeSome) +we need to promote to maintain (WantedTvInv) of Note [TcLevel and untouchable type variables] +in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing +and the reinstantiating with a fresh metavariable at the current level. +So in some sense, we generalize *all* variables, but then re-instantiate +some of them. + +Here is an example of why we must promote: + foo (x :: forall a. a -> Proxy b) = ... + +In the pattern signature, `b` is unbound, and will thus be brought into +scope. We do not know its kind: it will be assigned kappa[2]. Note that +kappa is at TcLevel 2, because it is invented under a forall. (A priori, +the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel +than the surrounding context.) This kappa cannot be solved for while checking +the pattern signature (which is not kind-generalized). When we are checking +the *body* of foo, though, we need to unify the type of x with the argument +type of bar. At this point, the ambient TcLevel is 1, and spotting a +matavariable with level 2 would violate the (WantedTvInv) invariant of +Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing, +we promote the metavariable to level 1. This is all done in kindGeneralizeNone. + -} funsSigCtxt :: [Located Name] -> UserTypeCtxt @@ -213,19 +297,21 @@ kcClassSigType skol_info names (HsIB { hsib_ext = sig_vars <- pushTcLevelM $ solveLocalEqualitiesX "kcClassSigType" $ bindImplicitTKBndrs_Skol sig_vars $ - tc_lhs_type typeLevelMode hs_ty liftedTypeKind + tcLHsType hs_ty liftedTypeKind - ; emitResidualTvConstraint skol_info Nothing spec_tkvs - tc_lvl wanted } + ; emitResidualTvConstraint skol_info spec_tkvs tc_lvl wanted } tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type -- Does not do validity checking tcClassSigType skol_info names sig_ty = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $ - snd <$> tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind) + do { (implic, ty) <- tc_hs_sig_type skol_info sig_ty (TheKind liftedTypeKind) + ; emitImplication implic + ; return ty } -- Do not zonk-to-Type, nor perform a validity check -- We are in a knot with the class and associated types -- Zonking and validity checking is done by tcClassDecl + -- -- No need to fail here if the type has an error: -- If we're in the kind-checking phase, the solveEqualities -- in kcTyClGroup catches the error @@ -247,46 +333,36 @@ tcHsSigType ctxt sig_ty do { traceTc "tcHsSigType {" (ppr sig_ty) -- Generalise here: see Note [Kind generalisation] - ; (insol, ty) <- tc_hs_sig_type skol_info sig_ty - (expectedKindInCtxt ctxt) - ; ty <- zonkTcType ty + ; (implic, ty) <- tc_hs_sig_type skol_info sig_ty (expectedKindInCtxt ctxt) - ; when insol failM - -- See Note [Fail fast if there are insoluble kind equalities] in GHC.Tc.Solver + -- Spit out the implication (and perhaps fail fast) + -- See Note [Failure in local type signatures] in GHC.Tc.Solver + ; emitFlatConstraints (mkImplicWC (unitBag implic)) + ; ty <- zonkTcType ty ; checkValidType ctxt ty ; traceTc "end tcHsSigType }" (ppr ty) ; return ty } where skol_info = SigTypeSkol ctxt --- Does validity checking and zonking. -tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind) -tcStandaloneKindSig (L _ kisig) = case kisig of - StandaloneKindSig _ (L _ name) ksig -> - let ctxt = StandaloneKindSigCtxt name in - addSigCtxt ctxt (hsSigType ksig) $ - do { kind <- tcTopLHsType kindLevelMode ksig (expectedKindInCtxt ctxt) - ; checkValidType ctxt kind - ; return (name, kind) } - tc_hs_sig_type :: SkolemInfo -> LHsSigType GhcRn - -> ContextKind -> TcM (Bool, TcType) + -> ContextKind -> TcM (Implication, TcType) -- Kind-checks/desugars an 'LHsSigType', -- solve equalities, -- and then kind-generalizes. -- This will never emit constraints, as it uses solveEqualities internally. -- No validity checking or zonking --- Returns also a Bool indicating whether the type induced an insoluble constraint; --- True <=> constraint is insoluble +-- Returns also an implication for the unsolved constraints tc_hs_sig_type skol_info hs_sig_type ctxt_kind | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type = do { (tc_lvl, (wanted, (spec_tkvs, ty))) <- pushTcLevelM $ solveLocalEqualitiesX "tc_hs_sig_type" $ + -- See Note [Failure in local type signatures] bindImplicitTKBndrs_Skol sig_vars $ do { kind <- newExpectedKind ctxt_kind - ; tc_lhs_type typeLevelMode hs_ty kind } + ; tcLHsType hs_ty kind } -- Any remaining variables (unsolved in the solveLocalEqualities) -- should be in the global tyvars, and therefore won't be quantified @@ -301,18 +377,67 @@ tc_hs_sig_type skol_info hs_sig_type ctxt_kind ; let should_gen = not . (`elemVarSet` constrained) ; kvs <- kindGeneralizeSome should_gen ty1 - ; emitResidualTvConstraint skol_info Nothing (kvs ++ spec_tkvs) - tc_lvl wanted - ; return (insolubleWC wanted, mkInfForAllTys kvs ty1) } + -- Build an implication for any as-yet-unsolved kind equalities + -- See Note [Skolem escape in type signatures] + ; implic <- buildTvImplication skol_info (kvs ++ spec_tkvs) tc_lvl wanted + + ; return (implic, mkInfForAllTys kvs ty1) } + +{- Note [Skolem escape in type signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +tcHsSigType is tricky. Consider (T11142) + foo :: forall b. (forall k (a :: k). SameKind a b) -> () +This is ill-kinded becuase of a nested skolem-escape. + +That will show up as an un-solvable constraint in the implication +returned by buildTvImplication in tc_hs_sig_type. See Note [Skolem +escape prevention] in GHC.Tc.Utils.TcType for why it is unsolvable +(the unification variable for b's kind is untouchable). + +Then, in GHC.Tc.Solver.emitFlatConstraints (called from tcHsSigType) +we'll try to float out the constraint, be unable to do so, and fail. +See GHC.Tc.Solver Note [Failure in local type signatures] for more +detail on this. + +The separation between tcHsSigType and tc_hs_sig_type is because +tcClassSigType wants to use the latter, but *not* fail fast, because +there are skolems from the class decl which are in scope; but it's fine +not to because tcClassDecl1 has a solveEqualities wrapped around all +the tcClassSigType calls. + +That's why tcHsSigType does emitFlatConstraints (which fails fast) but +tcClassSigType just does emitImplication (which does not). Ugh. + +c.f. see also Note [Skolem escape and forall-types]. The difference +is that we don't need to simplify at a forall type, only at the +top level of a signature. +-} + +-- Does validity checking and zonking. +tcStandaloneKindSig :: LStandaloneKindSig GhcRn -> TcM (Name, Kind) +tcStandaloneKindSig (L _ kisig) = case kisig of + StandaloneKindSig _ (L _ name) ksig -> + let ctxt = StandaloneKindSigCtxt name in + addSigCtxt ctxt (hsSigType ksig) $ + do { let mode = mkMode KindLevel + ; kind <- tc_top_lhs_type mode ksig (expectedKindInCtxt ctxt) + ; checkValidType ctxt kind + ; return (name, kind) } + -tcTopLHsType :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type +tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type +tcTopLHsType hs_ty ctxt_kind + = tc_top_lhs_type (mkMode TypeLevel) hs_ty ctxt_kind + +tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type -- tcTopLHsType is used for kind-checking top-level HsType where -- we want to fully solve /all/ equalities, and report errors -- Does zonking, but not validity checking because it's used -- for things (like deriving and instances) that aren't -- ordinary types -tcTopLHsType mode hs_sig_type ctxt_kind +-- Used for both types and kinds +tc_top_lhs_type mode hs_sig_type ctxt_kind | HsIB { hsib_ext = sig_vars, hsib_body = hs_ty } <- hs_sig_type = do { traceTc "tcTopLHsType {" (ppr hs_ty) ; (spec_tkvs, ty) @@ -340,7 +465,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], Class, [Type], [Kind]) tcHsDeriv hs_ty = do { ty <- checkNoErrs $ -- Avoid redundant error report -- with "illegal deriving", below - tcTopLHsType typeLevelMode hs_ty AnyKind + tcTopLHsType hs_ty AnyKind ; let (tvs, pred) = splitForAllTys ty (kind_args, _) = splitFunTys (tcTypeKind pred) ; case getClassPredTys_maybe pred of @@ -369,7 +494,7 @@ tcDerivStrategy mb_lds tc_deriv_strategy AnyclassStrategy = boring_case AnyclassStrategy tc_deriv_strategy NewtypeStrategy = boring_case NewtypeStrategy tc_deriv_strategy (ViaStrategy ty) = do - ty' <- checkNoErrs $ tcTopLHsType typeLevelMode ty AnyKind + ty' <- checkNoErrs $ tcTopLHsType ty AnyKind let (via_tvs, via_pred) = splitForAllTys ty' pure (ViaStrategy via_pred, via_tvs) @@ -387,7 +512,7 @@ tcHsClsInstType user_ctxt hs_inst_ty -- eagerly avoids follow-on errors when checkValidInstance -- sees an unsolved coercion hole inst_ty <- checkNoErrs $ - tcTopLHsType typeLevelMode hs_inst_ty (TheKind constraintKind) + tcTopLHsType hs_inst_ty (TheKind constraintKind) ; checkValidInstance user_ctxt hs_inst_ty inst_ty ; return inst_ty } @@ -397,14 +522,15 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType tcHsTypeApp wc_ty kind | HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty - = do { ty <- solveLocalEqualities "tcHsTypeApp" $ + = do { mode <- mkHoleMode TypeLevel HM_VTA + -- HM_VTA: See Note [Wildcards in visible type application] + ; ty <- addTypeCtxt hs_ty $ + solveLocalEqualities "tcHsTypeApp" $ -- We are looking at a user-written type, very like a -- signature so we want to solve its equalities right now - unsetWOptM Opt_WarnPartialTypeSignatures $ - setXOptM LangExt.PartialTypeSignatures $ - -- See Note [Wildcards in visible type application] tcNamedWildCardBinders sig_wcs $ \ _ -> - tcCheckLHsType hs_ty (TheKind kind) + tc_lhs_type mode hs_ty kind + -- We do not kind-generalize type applications: we just -- instantiate with exactly what the user says. -- See Note [No generalization in type application] @@ -448,6 +574,31 @@ There is also the possibility of mentioning a wildcard -} +tcFamTyPats :: TyCon + -> HsTyPats GhcRn -- Patterns + -> TcM (TcType, TcKind) -- (lhs_type, lhs_kind) +-- Check the LHS of a type/data family instance +-- e.g. type instance F ty1 .. tyn = ... +-- Used for both type and data families +tcFamTyPats fam_tc hs_pats + = do { traceTc "tcFamTyPats {" $ + vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ] + + ; mode <- mkHoleMode TypeLevel HM_FamPat + -- HM_FamPat: See Note [Wildcards in family instances] in + -- GHC.Rename.Module + ; let fun_ty = mkTyConApp fam_tc [] + ; (fam_app, res_kind) <- tcInferTyApps mode lhs_fun fun_ty hs_pats + + ; traceTc "End tcFamTyPats }" $ + vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ] + + ; return (fam_app, res_kind) } + where + fam_name = tyConName fam_tc + fam_arity = tyConArity fam_tc + lhs_fun = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name)) + {- ************************************************************************ * * @@ -465,38 +616,38 @@ tcHsOpenType ty = addTypeCtxt ty $ tcHsOpenTypeNC ty tcHsLiftedType ty = addTypeCtxt ty $ tcHsLiftedTypeNC ty tcHsOpenTypeNC ty = do { ek <- newOpenTypeKind - ; tc_lhs_type typeLevelMode ty ek } -tcHsLiftedTypeNC ty = tc_lhs_type typeLevelMode ty liftedTypeKind + ; tcLHsType ty ek } +tcHsLiftedTypeNC ty = tcLHsType ty liftedTypeKind -- Like tcHsType, but takes an expected kind tcCheckLHsType :: LHsType GhcRn -> ContextKind -> TcM TcType tcCheckLHsType hs_ty exp_kind = addTypeCtxt hs_ty $ do { ek <- newExpectedKind exp_kind - ; tc_lhs_type typeLevelMode hs_ty ek } + ; tcLHsType hs_ty ek } -tcLHsType :: LHsType GhcRn -> TcM (TcType, TcKind) +tcInferLHsType :: LHsType GhcRn -> TcM TcType -- Called from outside: set the context -tcLHsType ty = addTypeCtxt ty (tc_infer_lhs_type typeLevelMode ty) - --- Like tcLHsType, but use it in a context where type synonyms and type families --- do not need to be saturated, like in a GHCi :kind call -tcLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind) -tcLHsTypeUnsaturated hs_ty - | Just (hs_fun_ty, hs_args) <- splitHsAppTys (unLoc hs_ty) +tcInferLHsType hs_ty = addTypeCtxt hs_ty $ - do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty - ; tcInferApps_nosat mode hs_fun_ty fun_ty hs_args } - -- Notice the 'nosat'; do not instantiate trailing - -- invisible arguments of a type family. - -- See Note [Dealing with :kind] + do { (ty, _kind) <- tc_infer_lhs_type (mkMode TypeLevel) hs_ty + ; return ty } - | otherwise +-- Used to check the argument of GHCi :kind +-- Allow and report wildcards, e.g. :kind T _ +-- Do not saturate family applications: see Note [Dealing with :kind] +tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind) +tcInferLHsTypeUnsaturated hs_ty = addTypeCtxt hs_ty $ - tc_infer_lhs_type mode hs_ty - - where - mode = typeLevelMode + do { mode <- mkHoleMode TypeLevel HM_Sig -- Allow and report holes + ; case splitHsAppTys (unLoc hs_ty) of + Just (hs_fun_ty, hs_args) + -> do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty + ; tcInferTyApps_nosat mode hs_fun_ty fun_ty hs_args } + -- Notice the 'nosat'; do not instantiate trailing + -- invisible arguments of a type family. + -- See Note [Dealing with :kind] + Nothing -> tc_infer_lhs_type mode hs_ty } {- Note [Dealing with :kind] ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -507,7 +658,7 @@ Consider this GHCi command We will only get the 'forall' if we /refrain/ from saturating those invisible binders. But generally we /do/ saturate those invisible -binders (see tcInferApps), and we want to do so for nested application +binders (see tcInferTyApps), and we want to do so for nested application even in GHCi. Consider for example (#16287) ghci> type family F :: k ghci> data T :: (forall k. k) -> Type @@ -515,7 +666,7 @@ even in GHCi. Consider for example (#16287) We want to reject this. It's just at the very top level that we want to switch off saturation. -So tcLHsTypeUnsaturated does a little special case for top level +So tcInferLHsTypeUnsaturated does a little special case for top level applications. Actually the common case is a bare variable, as above. @@ -538,21 +689,46 @@ concern things that the renamer can't handle. -- grow, at least to include the distinction between patterns and -- not-patterns. -- --- To find out where the mode is used, search for 'mode_level' -data TcTyMode = TcTyMode { mode_level :: TypeOrKind } - -typeLevelMode :: TcTyMode -typeLevelMode = TcTyMode { mode_level = TypeLevel } - -kindLevelMode :: TcTyMode -kindLevelMode = TcTyMode { mode_level = KindLevel } +-- To find out where the mode is used, search for 'mode_tyki' +-- +-- This data type is purely local, not exported from this module +data TcTyMode + = TcTyMode { mode_tyki :: TypeOrKind + + -- See Note [Levels for wildcards] + -- Nothing <=> no wildcards expected + , mode_holes :: Maybe (TcLevel, HoleMode) + } + +-- HoleMode says how to treat the occurrences +-- of anonymous wildcards; see tcAnonWildCardOcc +data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int + | HM_FamPat -- Family instances: F _ Int = Bool + | HM_VTA -- Visible type and kind application: + -- f @(Maybe _) + -- Maybe @(_ -> _) + +mkMode :: TypeOrKind -> TcTyMode +mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing } + +mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode +mkHoleMode tyki hm + = do { lvl <- getTcLevel + ; return (TcTyMode { mode_tyki = tyki + , mode_holes = Just (lvl,hm) }) } --- switch to kind level kindLevel :: TcTyMode -> TcTyMode -kindLevel mode = mode { mode_level = KindLevel } +kindLevel mode = mode { mode_tyki = KindLevel } + +instance Outputable HoleMode where + ppr HM_Sig = text "HM_Sig" + ppr HM_FamPat = text "HM_FamPat" + ppr HM_VTA = text "HM_VTA" instance Outputable TcTyMode where - ppr = ppr . mode_level + ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm }) + = text "TcTyMode" <+> braces (sep [ ppr tyki <> comma + , ppr hm ]) {- Note [Bidirectional type checking] @@ -627,11 +803,12 @@ tc_infer_hs_type mode (HsParTy _ t) tc_infer_hs_type mode ty | Just (hs_fun_ty, hs_args) <- splitHsAppTys ty - = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty - ; tcInferApps mode hs_fun_ty fun_ty hs_args } + = do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty + ; tcInferTyApps mode hs_fun_ty fun_ty hs_args } tc_infer_hs_type mode (HsKindSig _ ty sig) - = do { sig' <- tcLHsKindSig KindSigCtxt sig + = do { let mode' = mode { mode_tyki = KindLevel } + ; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig -- We must typecheck the kind signature, and solve all -- its equalities etc; from this point on we may do -- things like instantiate its foralls, so it needs @@ -665,6 +842,10 @@ tc_infer_hs_type mode other_ty ; return (ty', kv) } ------------------------------------------ +tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType +tcLHsType hs_ty exp_kind + = tc_lhs_type (mkMode TypeLevel) hs_ty exp_kind + tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType tc_lhs_type mode (L span ty) exp_kind = setSrcSpan span $ @@ -718,18 +899,25 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs , hst_body = ty }) exp_kind = do { (tclvl, wanted, (inv_tv_bndrs, ty')) - <- pushLevelAndCaptureConstraints $ - bindExplicitTKBndrs_Skol hs_tvs $ + <- pushLevelAndCaptureConstraints $ + bindExplicitTKBndrs_Skol_M mode hs_tvs $ + -- 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 tc_lhs_type mode ty exp_kind - -- Do not kind-generalise here! See Note [Kind generalisation] - -- Why exp_kind? See Note [Body kind of HsForAllTy] - ; let skol_info = ForAllSkol (ppr forall) - m_telescope = Just (sep (map ppr hs_tvs)) + -- Why exp_kind? See Note [Body kind of HsForAllTy] - ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs + -- Do not kind-generalise here! See Note [Kind generalisation] - ; emitResidualTvConstraint skol_info m_telescope (binderVars tv_bndrs) tclvl wanted + ; let skol_info = ForAllSkol (ppr forall) (sep (map ppr hs_tvs)) + skol_tvs = binderVars inv_tv_bndrs + ; implic <- buildTvImplication skol_info skol_tvs tclvl wanted + ; emitImplication implic + -- /Always/ emit this implication even if wanted is empty + -- We need the implication so that we check for a bad telescope + -- See Note [Skolem escape and forall-types] + ; tv_bndrs <- mapM construct_bndr inv_tv_bndrs ; return (mkForAllTys tv_bndrs ty') } where construct_bndr :: TcInvisTVBinder -> TcM TcTyVarBinder @@ -846,7 +1034,7 @@ tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind --------- Constraint types tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind - = do { MASSERT( isTypeLevel (mode_level mode) ) + = do { MASSERT( isTypeLevel (mode_tyki mode) ) ; ty' <- tc_lhs_type mode ty liftedTypeKind ; let n' = mkStrLitTy $ hsIPNameFS n ; ipClass <- tcLookupClass ipClassName @@ -875,7 +1063,7 @@ tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek tc_hs_type mode ty@(XHsType (NHsCoreTy{})) ek = tc_infer_hs_type_ek mode ty ek -tc_hs_type _ wc@(HsWildCardTy _) ek = tcAnonWildCardOcc wc ek +tc_hs_type mode ty@(HsWildCardTy _) ek = tcAnonWildCardOcc mode ty ek {- Note [Variable Specificity and Forall Visibility] @@ -903,7 +1091,7 @@ Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep. ------------------------------------------ tc_fun_type :: TcTyMode -> LHsType GhcRn -> LHsType GhcRn -> TcKind -> TcM TcType -tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of +tc_fun_type mode ty1 ty2 exp_kind = case mode_tyki mode of TypeLevel -> do { arg_k <- newOpenTypeKind ; res_k <- newOpenTypeKind @@ -917,46 +1105,10 @@ tc_fun_type mode ty1 ty2 exp_kind = case mode_level mode of ; checkExpectedKind (HsFunTy noExtField ty1 ty2) (mkVisFunTy ty1' ty2') liftedTypeKind exp_kind } ---------------------------- -tcAnonWildCardOcc :: HsType GhcRn -> Kind -> TcM TcType -tcAnonWildCardOcc wc exp_kind - = do { wc_tv <- newWildTyVar -- The wildcard's kind will be an un-filled-in meta tyvar - - ; part_tysig <- xoptM LangExt.PartialTypeSignatures - ; warning <- woptM Opt_WarnPartialTypeSignatures - - ; unless (part_tysig && not warning) $ - emitAnonTypeHole wc_tv - -- Why the 'unless' guard? - -- See Note [Wildcards in visible kind application] - - ; checkExpectedKind wc (mkTyVarTy wc_tv) - (tyVarKind wc_tv) exp_kind } - -{- Note [Wildcards in visible kind application] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -There are cases where users might want to pass in a wildcard as a visible kind -argument, for instance: - -data T :: forall k1 k2. k1 → k2 → Type where - MkT :: T a b -x :: T @_ @Nat False n -x = MkT - -So we should allow '@_' without emitting any hole constraints, and -regardless of whether PartialTypeSignatures is enabled or not. But how would -the typechecker know which '_' is being used in VKA and which is not when it -calls emitNamedTypeHole in tcHsPartialSigType on all HsWildCardBndrs? -The solution then is to neither rename nor include unnamed wildcards in HsWildCardBndrs, -but instead give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc. -And whenever we see a '@', we automatically turn on PartialTypeSignatures and -turn off hole constraint warnings, and do not call emitAnonTypeHole -under these conditions. -See related Note [Wildcards in visible type application] here and -Note [The wildcard story for types] in GHC.Hs.Types +{- Note [Skolem escape and forall-types] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +See also Note [Checking telescopes]. -Note [Skolem escape and forall-types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider f :: forall a. (forall kb (b :: kb). Proxy '[a, b]) -> () @@ -970,11 +1122,19 @@ unification variable, because it would be untouchable inside this inner implication. That's what the pushLevelAndCaptureConstraints, plus subsequent -emitResidualTvConstraint is all about, when kind-checking +buildTvImplication/emitImplication is all about, when kind-checking HsForAllTy. -Note that we don't need to /simplify/ the constraints here -because we aren't generalising. We just capture them. +Note that + +* We don't need to /simplify/ the constraints here + because we aren't generalising. We just capture them. + +* We can't use emitResidualTvConstraint, because that has a fast-path + for empty constraints. We can't take that fast path here, because + we must do the bad-telescope check even if there are no inner wanted + constraints. See Note [Checking telescopes] in + GHC.Tc.Types.Constraint. Lacking this check led to #16247. -} {- ********************************************************************* @@ -1117,14 +1277,14 @@ splitHsAppTys hs_ty go f as = (f, as) --------------------------- -tcInferAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind) +tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind) -- Version of tc_infer_lhs_type specialised for the head of an -- application. In particular, for a HsTyVar (which includes type --- constructors, it does not zoom off into tcInferApps and family +-- constructors, it does not zoom off into tcInferTyApps and family -- saturation -tcInferAppHead mode (L _ (HsTyVar _ _ (L _ tv))) +tcInferTyAppHead mode (L _ (HsTyVar _ _ (L _ tv))) = tcTyVar mode tv -tcInferAppHead mode ty +tcInferTyAppHead mode ty = tc_infer_lhs_type mode ty --------------------------- @@ -1135,24 +1295,24 @@ tcInferAppHead mode ty -- These kinds should be used to instantiate invisible kind variables; -- they come from an enclosing class for an associated type/data family. -- --- tcInferApps also arranges to saturate any trailing invisible arguments +-- tcInferTyApps also arranges to saturate any trailing invisible arguments -- of a type-family application, which is usually the right thing to do --- tcInferApps_nosat does not do this saturation; it is used only +-- tcInferTyApps_nosat does not do this saturation; it is used only -- by ":kind" in GHCi -tcInferApps, tcInferApps_nosat +tcInferTyApps, tcInferTyApps_nosat :: TcTyMode -> LHsType GhcRn -- ^ Function (for printing only) -> TcType -- ^ Function -> [LHsTypeArg GhcRn] -- ^ Args -> TcM (TcType, TcKind) -- ^ (f args, args, result kind) -tcInferApps mode hs_ty fun hs_args - = do { (f_args, res_k) <- tcInferApps_nosat mode hs_ty fun hs_args +tcInferTyApps mode hs_ty fun hs_args + = do { (f_args, res_k) <- tcInferTyApps_nosat mode hs_ty fun hs_args ; saturateFamApp f_args res_k } -tcInferApps_nosat mode orig_hs_ty fun orig_hs_args - = do { traceTc "tcInferApps {" (ppr orig_hs_ty $$ ppr orig_hs_args) +tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args + = do { traceTc "tcInferTyApps {" (ppr orig_hs_ty $$ ppr orig_hs_args) ; (f_args, res_k) <- go_init 1 fun orig_hs_args - ; traceTc "tcInferApps }" (ppr f_args <+> dcolon <+> ppr res_k) + ; traceTc "tcInferTyApps }" (ppr f_args <+> dcolon <+> ppr res_k) ; return (f_args, res_k) } where @@ -1205,21 +1365,18 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args Anon InvisArg _ -> instantiate ki_binder inner_ki Named (Bndr _ Specified) -> -- Visible kind application - do { traceTc "tcInferApps (vis kind app)" + do { traceTc "tcInferTyApps (vis kind app)" (vcat [ ppr ki_binder, ppr hs_ki_arg , ppr (tyBinderType ki_binder) , ppr subst ]) ; let exp_kind = substTy subst $ tyBinderType ki_binder - + ; arg_mode <- mkHoleMode KindLevel HM_VTA + -- HM_VKA: see Note [Wildcards in visible kind application] ; ki_arg <- addErrCtxt (funAppCtxt orig_hs_ty hs_ki_arg n) $ - unsetWOptM Opt_WarnPartialTypeSignatures $ - setXOptM LangExt.PartialTypeSignatures $ - -- Urgh! see Note [Wildcards in visible kind application] - -- ToDo: must kill this ridiculous messing with DynFlags - tc_lhs_type (kindLevel mode) hs_ki_arg exp_kind + tc_lhs_type arg_mode hs_ki_arg exp_kind - ; traceTc "tcInferApps (vis kind app)" (ppr exp_kind) + ; traceTc "tcInferTyApps (vis kind app)" (ppr exp_kind) ; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg ; go (n+1) fun' subst' inner_ki hs_args } @@ -1241,7 +1398,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args -- "normal" case | otherwise - -> do { traceTc "tcInferApps (vis normal app)" + -> do { traceTc "tcInferTyApps (vis normal app)" (vcat [ ppr ki_binder , ppr arg , ppr (tyBinderType ki_binder) @@ -1249,7 +1406,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args ; let exp_kind = substTy subst $ tyBinderType ki_binder ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $ tc_lhs_type mode arg exp_kind - ; traceTc "tcInferApps (vis normal app) 2" (ppr exp_kind) + ; traceTc "tcInferTyApps (vis normal app) 2" (ppr exp_kind) ; (subst', fun') <- mkAppTyM subst fun ki_binder arg' ; go (n+1) fun' subst' inner_ki args } @@ -1263,7 +1420,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args -- This zonk is essential, to expose the fruits -- of matchExpectedFunKind to the 'go' loop - ; traceTc "tcInferApps (no binder)" $ + ; traceTc "tcInferTyApps (no binder)" $ vcat [ ppr fun <+> dcolon <+> ppr fun_ki , ppr arrows_needed , ppr co @@ -1272,7 +1429,7 @@ tcInferApps_nosat mode orig_hs_ty fun orig_hs_args -- Use go_init to establish go's INVARIANT where instantiate ki_binder inner_ki - = do { traceTc "tcInferApps (need to instantiate)" + = do { traceTc "tcInferTyApps (need to instantiate)" (vcat [ ppr ki_binder, ppr subst]) ; (subst', arg') <- tcInstInvisibleTyBinder subst ki_binder ; go n (mkAppTy fun arg') subst' inner_ki all_args } @@ -1375,7 +1532,7 @@ The way in which tcTypeKind can crash is in applications if 'a' is a type variable whose kind doesn't have enough arrows or foralls. (The crash is in piResultTys.) -The loop in tcInferApps has to be very careful to maintain the (PKTI). +The loop in tcInferTyApps has to be very careful to maintain the (PKTI). For example, suppose kappa is a unification variable We have already unified kappa := Type @@ -1387,7 +1544,7 @@ If we call tcTypeKind on that, we'll crash, because the (un-zonked) kind of 'a' is just kappa, not an arrow kind. So we must zonk first. So the type inference engine is very careful when building applications. -This happens in tcInferApps. Suppose we are kind-checking the type (a Int), +This happens in tcInferTyApps. Suppose we are kind-checking the type (a Int), where (a :: kappa). Then in tcInferApps we'll run out of binders on a's kind, so we'll call matchExpectedFunKind, and unify kappa := kappa1 -> kappa2, with evidence co :: kappa ~ (kappa1 ~ kappa2) @@ -1530,10 +1687,10 @@ tcHsMbContext Nothing = return [] tcHsMbContext (Just cxt) = tcHsContext cxt tcHsContext :: LHsContext GhcRn -> TcM [PredType] -tcHsContext = tc_hs_context typeLevelMode +tcHsContext cxt = tc_hs_context (mkMode TypeLevel) cxt tcLHsPredType :: LHsType GhcRn -> TcM PredType -tcLHsPredType = tc_lhs_pred typeLevelMode +tcLHsPredType pred = tc_lhs_pred (mkMode TypeLevel) pred tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType] tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt) @@ -1553,7 +1710,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference] - unless (isTypeLevel (mode_level mode)) + unless (isTypeLevel (mode_tyki mode)) (promotionErr name TyConPE) ; check_tc tc_tc ; return (mkTyConTy tc_tc, tyConKind tc_tc) } @@ -1584,7 +1741,7 @@ tcTyVar mode name -- Could be a tyvar, a tycon, or a datacon where check_tc :: TyCon -> TcM () check_tc tc = do { data_kinds <- xoptM LangExt.DataKinds - ; unless (isTypeLevel (mode_level mode) || + ; unless (isTypeLevel (mode_tyki mode) || data_kinds || isKindTyCon tc) $ promotionErr name NoDataKindsTC } @@ -1731,8 +1888,6 @@ in the e2 example, we'll desugar the type, zonking the kind unification variables as we go. When we encounter the unconstrained kappa, we want to default it to '*', not to (Any *). -Help functions for type applications -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -} addTypeCtxt :: LHsType GhcRn -> TcM a -> TcM a @@ -1744,98 +1899,12 @@ addTypeCtxt (L _ ty) thing where doc = text "In the type" <+> quotes (ppr ty) -{- -************************************************************************ + +{- ********************************************************************* * * Type-variable binders -%* * -%************************************************************************ - -Note [Keeping implicitly quantified variables in order] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When the user implicitly quantifies over variables (say, in a type -signature), we need to come up with some ordering on these variables. -This is done by bumping the TcLevel, bringing the tyvars into scope, -and then type-checking the thing_inside. The constraints are all -wrapped in an implication, which is then solved. Finally, we can -zonk all the binders and then order them with scopedSort. - -It's critical to solve before zonking and ordering in order to uncover -any unifications. You might worry that this eager solving could cause -trouble elsewhere. I don't think it will. Because it will solve only -in an increased TcLevel, it can't unify anything that was mentioned -elsewhere. Additionally, we require that the order of implicitly -quantified variables is manifest by the scope of these variables, so -we're not going to learn more information later that will help order -these variables. - -Note [Recipe for checking a signature] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Checking a user-written signature requires several steps: - - 1. Generate constraints. - 2. Solve constraints. - 3. Promote tyvars and/or kind-generalize. - 4. Zonk. - 5. Check validity. - -There may be some surprises in here: - -Step 2 is necessary for two reasons: most signatures also bring -implicitly quantified variables into scope, and solving is necessary -to get these in the right order (see Note [Keeping implicitly -quantified variables in order]). Additionally, solving is necessary in -order to kind-generalize correctly: otherwise, we do not know which -metavariables are left unsolved. - -Step 3 is done by a call to candidateQTyVarsOfType, followed by a call to -kindGeneralize{All,Some,None}. Here, we have to deal with the fact that -metatyvars generated in the type may 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 - (B) promoted, or See Note [Promotion in signatures] - (C) a cause to error See Note [Naughty quantification candidates] in GHC.Tc.Utils.TcMType - -The kindGeneralize functions do not require pre-zonking; they zonk as they -go. - -If you are actually doing kind-generalization, you need to bump the level -before generating constraints, as we will only generalize variables with -a TcLevel higher than the ambient one. - -After promoting/generalizing, we need to zonk again because both -promoting and generalizing fill in metavariables. - -Note [Promotion in signatures] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -If an unsolved metavariable in a signature is not generalized -(because we're not generalizing the construct -- e.g., pattern -sig -- or because the metavars are constrained -- see kindGeneralizeSome) -we need to promote to maintain (WantedTvInv) of Note [TcLevel and untouchable type variables] -in GHC.Tc.Utils.TcType. Note that promotion is identical in effect to generalizing -and the reinstantiating with a fresh metavariable at the current level. -So in some sense, we generalize *all* variables, but then re-instantiate -some of them. - -Here is an example of why we must promote: - foo (x :: forall a. a -> Proxy b) = ... - -In the pattern signature, `b` is unbound, and will thus be brought into -scope. We do not know its kind: it will be assigned kappa[2]. Note that -kappa is at TcLevel 2, because it is invented under a forall. (A priori, -the kind kappa might depend on `a`, so kappa rightly has a higher TcLevel -than the surrounding context.) This kappa cannot be solved for while checking -the pattern signature (which is not kind-generalized). When we are checking -the *body* of foo, though, we need to unify the type of x with the argument -type of bar. At this point, the ambient TcLevel is 1, and spotting a -matavariable with level 2 would violate the (WantedTvInv) invariant of -Note [TcLevel and untouchable type variables]. So, instead of kind-generalizing, -we promote the metavariable to level 1. This is all done in kindGeneralizeNone. - --} +* * +********************************************************************* -} tcNamedWildCardBinders :: [Name] -> ([(Name, TcTyVar)] -> TcM a) @@ -1844,22 +1913,119 @@ tcNamedWildCardBinders :: [Name] -- plain wildcards _ are anonymous and dealt with by HsWildCardTy -- Soe Note [The wildcard story for types] in GHC.Hs.Types tcNamedWildCardBinders wc_names thing_inside - = do { wcs <- mapM (const newWildTyVar) wc_names + = do { wcs <- mapM newNamedWildTyVar wc_names ; let wc_prs = wc_names `zip` wcs ; tcExtendNameTyVarEnv wc_prs $ thing_inside wc_prs } -newWildTyVar :: TcM TcTyVar +newNamedWildTyVar :: Name -> TcM TcTyVar -- ^ New unification variable '_' for a wildcard -newWildTyVar +newNamedWildTyVar _name -- Currently ignoring the "_x" wildcard name used in the type = do { kind <- newMetaKindVar - ; uniq <- newUnique ; details <- newMetaDetails TauTv - ; let name = mkSysTvName uniq (fsLit "_") - tyvar = mkTcTyVar name kind details + ; wc_name <- newMetaTyVarName (fsLit "w") -- See Note [Wildcard names] + ; let tyvar = mkTcTyVar wc_name kind details ; traceTc "newWildTyVar" (ppr tyvar) ; return tyvar } +--------------------------- +tcAnonWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType +tcAnonWildCardOcc (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) }) + ty exp_kind + -- hole_lvl: see Note [Checking partial type signatures] + -- esp the bullet on nested forall types + = do { kv_details <- newTauTvDetailsAtLevel hole_lvl + ; kv_name <- newMetaTyVarName (fsLit "k") + ; wc_details <- newTauTvDetailsAtLevel hole_lvl + ; wc_name <- newMetaTyVarName (fsLit wc_nm) + ; let kv = mkTcTyVar kv_name liftedTypeKind kv_details + wc_kind = mkTyVarTy kv + wc_tv = mkTcTyVar wc_name wc_kind wc_details + + ; traceTc "tcAnonWildCardOcc" (ppr hole_lvl <+> ppr emit_holes) + ; when emit_holes $ + emitAnonTypeHole wc_tv + -- Why the 'when' guard? + -- See Note [Wildcards in visible kind application] + + -- You might think that this would always just unify + -- wc_kind with exp_kind, so we could avoid even creating kv + -- But the level numbers might not allow that unification, + -- so we have to do it properly (T14140a) + ; checkExpectedKind ty (mkTyVarTy wc_tv) wc_kind exp_kind } + where + -- See Note [Wildcard names] + wc_nm = case hole_mode of + HM_Sig -> "w" + HM_FamPat -> "_" + HM_VTA -> "w" + + emit_holes = case hole_mode of + HM_Sig -> True + HM_FamPat -> False + HM_VTA -> False + +tcAnonWildCardOcc mode ty _ +-- mode_holes is Nothing. Should not happen, because renamer +-- should already have rejected holes in unexpected places + = pprPanic "tcWildCardOcc" (ppr mode $$ ppr ty) + +{- Note [Wildcard names] +~~~~~~~~~~~~~~~~~~~~~~~~ +So we hackily use the mode_holes flag to control the name used +for wildcards: + +* For proper holes (whether in a visible type application (VTA) or no), + we rename the '_' to 'w'. This is so that we see variables like 'w0' + or 'w1' in error messages, a vast improvement upon '_0' and '_1'. For + example, we prefer + Found type wildcard ‘_’ standing for ‘w0’ + over + Found type wildcard ‘_’ standing for ‘_1’ + + Even in the VTA case, where we do not emit an error to be printed, we + want to do the renaming, as the variables may appear in other, + non-wildcard error messages. + +* However, holes in the left-hand sides of type families ("type + patterns") stand for type variables which we do not care to name -- + much like the use of an underscore in an ordinary term-level + pattern. When we spot these, we neither wish to generate an error + message nor to rename the variable. We don't rename the variable so + that we can pretty-print a type family LHS as, e.g., + F _ Int _ = ... + and not + F w1 Int w2 = ... + + See also Note [Wildcards in family instances] in + GHC.Rename.Module. The choice of HM_FamPat is made in + tcFamTyPats. There is also some unsavory magic, relying on that + underscore, in GHC.Core.Coercion.tidyCoAxBndrsForUser. + +Note [Wildcards in visible kind application] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +There are cases where users might want to pass in a wildcard as a visible kind +argument, for instance: + +data T :: forall k1 k2. k1 → k2 → Type where + MkT :: T a b +x :: T @_ @Nat False n +x = MkT + +So we should allow '@_' without emitting any hole constraints, and +regardless of whether PartialTypeSignatures is enabled or not. But how +would the typechecker know which '_' is being used in VKA and which is +not when it calls emitNamedTypeHole in +tcHsPartialSigType on all HsWildCardBndrs? The solution is to neither +rename nor include unnamed wildcards in HsWildCardBndrs, but instead +give every anonymous wildcard a fresh wild tyvar in tcAnonWildCardOcc. + +And whenever we see a '@', we set mode_holes to HM_VKA, so that +we do not call emitAnonTypeHole in tcAnonWildCardOcc. +See related Note [Wildcards in visible type application] here and +Note [The wildcard story for types] in GHC.Hs.Types +-} + {- ********************************************************************* * * Kind inference for type declarations @@ -2703,8 +2869,17 @@ bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv -> TcM a -> TcM ([VarBndr TyVar flag], a) -bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar) -bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar) +bindExplicitTKBndrs_Skol_M, bindExplicitTKBndrs_Tv_M + :: (OutputableBndrFlag flag) + => TcTyMode + -> [LHsTyVarBndr flag GhcRn] + -> TcM a + -> TcM ([VarBndr TyVar flag], a) + +bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) newSkolemTyVar) +bindExplicitTKBndrs_Skol_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) newSkolemTyVar) +bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) cloneTyVarTyVar) +bindExplicitTKBndrs_Tv_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) cloneTyVarTyVar) -- newSkolemTyVar: see Note [Non-cloning for tyvar binders] -- cloneTyVarTyVar: see Note [Cloning for tyvar binders] @@ -2752,13 +2927,13 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside ; return ((Bndr tv (hsTyVarBndrFlag hs_tv)):tvs, res) } ----------------- -tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar) +tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar) -> HsTyVarBndr flag GhcRn -> TcM TcTyVar -tcHsTyVarBndr new_tv (UserTyVar _ _ (L _ tv_nm)) +tcHsTyVarBndr _ new_tv (UserTyVar _ _ (L _ tv_nm)) = do { kind <- newMetaKindVar ; new_tv tv_nm kind } -tcHsTyVarBndr new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind) - = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind +tcHsTyVarBndr mode new_tv (KindedTyVar _ _ (L _ tv_nm) lhs_kind) + = do { kind <- tc_lhs_kind_sig mode (TyVarBndrKindCtxt tv_nm) lhs_kind ; new_tv tv_nm kind } ----------------- @@ -2861,15 +3036,14 @@ kindGeneralizeSome should_gen kind_or_type ; let (to_promote, dvs') = partitionCandidates dvs (not . should_gen) - ; (_, promoted) <- promoteTyVarSet (dVarSetToVarSet to_promote) + ; _ <- promoteTyVarSet to_promote ; qkvs <- quantifyTyVars dvs' ; traceTc "kindGeneralizeSome }" $ vcat [ text "Kind or type:" <+> ppr kind_or_type , text "dvs:" <+> ppr dvs , text "dvs':" <+> ppr dvs' - , text "to_promote:" <+> pprTyVars (dVarSetElems to_promote) - , text "promoted:" <+> pprTyVars (nonDetEltsUniqSet promoted) + , text "to_promote:" <+> ppr to_promote , text "qkvs:" <+> pprTyVars qkvs ] ; return qkvs } @@ -3046,6 +3220,7 @@ data DataSort checkDataKindSig :: DataSort -> Kind -> TcM () checkDataKindSig data_sort kind = do dflags <- getDynFlags + traceTc "checkDataKindSig" (ppr kind) checkTc (is_TYPE_or_Type dflags || is_kind_var) (err_msg dflags) where pp_dec :: SDoc @@ -3211,19 +3386,20 @@ tcHsPartialSigType ctxt sig_ty , hsib_body = hs_ty } <- ib_ty , (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTyInvis hs_ty = addSigCtxt ctxt hs_ty $ - do { (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau))) + do { mode <- mkHoleMode TypeLevel HM_Sig + ; (implicit_tvs, (explicit_tvbndrs, (wcs, wcx, theta, tau))) <- solveLocalEqualities "tcHsPartialSigType" $ - -- This solveLocalEqualiltes fails fast if there are - -- insoluble equalities. See GHC.Tc.Solver - -- Note [Fail fast if there are insoluble kind equalities] + -- See Note [Failure in local type signatures] tcNamedWildCardBinders sig_wcs $ \ wcs -> - bindImplicitTKBndrs_Tv implicit_hs_tvs $ - bindExplicitTKBndrs_Tv explicit_hs_tvs $ + bindImplicitTKBndrs_Tv implicit_hs_tvs $ + bindExplicitTKBndrs_Tv_M mode explicit_hs_tvs $ do { -- Instantiate the type-class context; but if there -- is an extra-constraints wildcard, just discard it here - (theta, wcx) <- tcPartialContext hs_ctxt + (theta, wcx) <- tcPartialContext mode hs_ctxt - ; tau <- tcHsOpenType hs_tau + ; ek <- newOpenTypeKind + ; tau <- addTypeCtxt hs_tau $ + tc_lhs_type mode hs_tau ek ; return (wcs, wcx, theta, tau) } @@ -3241,10 +3417,12 @@ tcHsPartialSigType ctxt sig_ty ; mapM_ emitNamedTypeHole wcs -- Zonk, so that any nested foralls can "see" their occurrences - -- See Note [Checking partial type signatures], in - -- the bullet on Nested foralls. - ; theta <- mapM zonkTcType theta - ; tau <- zonkTcType tau + -- See Note [Checking partial type signatures], and in particular + -- Note [Levels for wildcards] + ; implicit_tvbndrs <- mapM zonkInvisTVBinder implicit_tvbndrs + ; explicit_tvbndrs <- mapM zonkInvisTVBinder explicit_tvbndrs + ; theta <- mapM zonkTcType theta + ; tau <- zonkTcType tau -- We return a proper (Name,InvisTVBinder) environment, to be sure that -- we bring the right name into scope in the function body. @@ -3259,16 +3437,16 @@ tcHsPartialSigType ctxt sig_ty ; traceTc "tcHsPartialSigType" (ppr tv_prs) ; return (wcs, wcx, tv_prs, theta, tau) } -tcPartialContext :: HsContext GhcRn -> TcM (TcThetaType, Maybe TcType) -tcPartialContext hs_theta +tcPartialContext :: TcTyMode -> HsContext GhcRn -> TcM (TcThetaType, Maybe TcType) +tcPartialContext mode hs_theta | Just (hs_theta1, hs_ctxt_last) <- snocView hs_theta - , L wc_loc wc@(HsWildCardTy _) <- ignoreParens hs_ctxt_last + , L wc_loc ty@(HsWildCardTy _) <- ignoreParens hs_ctxt_last = do { wc_tv_ty <- setSrcSpan wc_loc $ - tcAnonWildCardOcc wc constraintKind - ; theta <- mapM tcLHsPredType hs_theta1 + tcAnonWildCardOcc mode ty constraintKind + ; theta <- mapM (tc_lhs_pred mode) hs_theta1 ; return (theta, Just wc_tv_ty) } | otherwise - = do { theta <- mapM tcLHsPredType hs_theta + = do { theta <- mapM (tc_lhs_pred mode) hs_theta ; return (theta, Nothing) } {- Note [Checking partial type signatures] @@ -3312,29 +3490,48 @@ we do the following g x = True It's really as if we'd written two distinct signatures. -* Nested foralls. Consider - f :: forall b. (forall a. a -> _) -> b - We do /not/ allow the "_" to be instantiated to 'a'; but we do - (as before) allow it to be instantiated to the (top level) 'b'. - Why not? Because suppose - f x = (x True, x 'c') - We must instantiate that (forall a. a -> _) when typechecking - f's body, so we must know precisely where all the a's are; they - must not be hidden under (filled-in) unification variables! - - We achieve this in the usual way: we push a level at a forall, - so now the unification variable for the "_" can't unify with - 'a'. - -* Just as for ordinary signatures, we must zonk the type after - kind-checking it, to ensure that all the nested forall binders can - see their occurrenceds +* Nested foralls. See Note [Levels for wildcards] + +* Just as for ordinary signatures, we must solve local equalities and + zonk the type after kind-checking it, to ensure that all the nested + forall binders can "see" their occurrenceds Just as for ordinary signatures, this zonk also gets any Refl casts out of the way of instantiation. Example: #18008 had foo :: (forall a. (Show a => blah) |> Refl) -> _ and that Refl cast messed things up. See #18062. +Note [Levels for wildcards] +~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + f :: forall b. (forall a. a -> _) -> b +We do /not/ allow the "_" to be instantiated to 'a'; although we do +(as before) allow it to be instantiated to the (top level) 'b'. +Why not? Suppose + f x = (x True, x 'c') + +During typecking the RHS we must instantiate that (forall a. a -> _), +so we must know /precisely/ where all the a's are; they must not be +hidden under (possibly-not-yet-filled-in) unification variables! + +We achieve this as follows: + +- For /named/ wildcards such sas + g :: forall b. (forall la. a -> _x) -> b + there is no problem: we create them at the outer level (ie the + ambient level of teh signature itself), and push the level when we + go inside a forall. So now the unification variable for the "_x" + can't unify with skolem 'a'. + +- For /anonymous/ wildcards, such as 'f' above, we carry the ambient + level of the signature to the hole in the TcLevel part of the + mode_holes field of TcTyMode. Then, in tcAnonWildCardOcc we us that + level (and /not/ the level ambient at the occurrence of "_") to + create the unification variable for the wildcard. That is the sole + purpose of the TcLevel in the mode_holes field: to transport the + ambient level of the signature down to the anonymous wildcard + occurrences. + Note [Extra-constraint holes in partial type signatures] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider @@ -3399,14 +3596,16 @@ tcHsPatSigType ctxt , hsps_body = hs_ty }) = addSigCtxt ctxt hs_ty $ do { sig_tkv_prs <- mapM new_implicit_tv sig_ns + ; mode <- mkHoleMode TypeLevel HM_Sig ; (wcs, sig_ty) - <- solveLocalEqualities "tcHsPatSigType" $ - -- Always solve local equalities if possible, - -- else casts get in the way of deep skolemisation - -- (#16033) + <- addTypeCtxt hs_ty $ + solveLocalEqualities "tcHsPatSigType" $ + -- See Note [Failure in local type signatures] + -- and c.f #16033 tcNamedWildCardBinders sig_wcs $ \ wcs -> tcExtendNameTyVarEnv sig_tkv_prs $ - do { sig_ty <- tcHsOpenType hs_ty + do { ek <- newOpenTypeKind + ; sig_ty <- tc_lhs_type mode hs_ty ek ; return (wcs, sig_ty) } ; mapM_ emitNamedTypeHole wcs @@ -3509,10 +3708,15 @@ It does sort checking and desugaring at the same time, in one single pass. tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind tcLHsKindSig ctxt hs_kind + = tc_lhs_kind_sig (mkMode KindLevel) ctxt hs_kind + +tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsKind GhcRn -> TcM Kind +tc_lhs_kind_sig mode ctxt hs_kind -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType -- Result is zonked - = do { kind <- solveLocalEqualities "tcLHsKindSig" $ - tc_lhs_kind kindLevelMode hs_kind + = do { kind <- addErrCtxt (text "In the kind" <+> quotes (ppr hs_kind)) $ + solveLocalEqualities "tcLHsKindSig" $ + tc_lhs_type mode hs_kind liftedTypeKind ; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind) -- No generalization: ; kindGeneralizeNone kind @@ -3528,11 +3732,6 @@ tcLHsKindSig ctxt hs_kind ; traceTc "tcLHsKindSig2" (ppr kind) ; return kind } -tc_lhs_kind :: TcTyMode -> LHsKind GhcRn -> TcM Kind -tc_lhs_kind mode k - = addErrCtxt (text "In the kind" <+> quotes (ppr k)) $ - tc_lhs_type (kindLevel mode) k liftedTypeKind - promotionErr :: Name -> PromotionErr -> TcM a promotionErr name err = failWithTc (hang (pprPECategory err <+> quotes (ppr name) <+> text "cannot be used here") diff --git a/compiler/GHC/Tc/Gen/Match.hs b/compiler/GHC/Tc/Gen/Match.hs index 350be10236..b9eaad4adb 100644 --- a/compiler/GHC/Tc/Gen/Match.hs +++ b/compiler/GHC/Tc/Gen/Match.hs @@ -36,9 +36,10 @@ where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRhoNC, tcInferRho - , tcCheckId, tcLExpr, tcLExprNC, tcExpr - , tcCheckExpr ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcInferRho, tcInferRhoNC + , tcMonoExpr, tcMonoExprNC, tcExpr + , tcCheckMonoExpr, tcCheckMonoExprNC + , tcCheckPolyExpr, tcCheckId ) import GHC.Types.Basic (LexicalFixity(..)) import GHC.Hs @@ -79,17 +80,11 @@ import Control.Arrow ( second ) @FunMonoBind@. The second argument is the name of the function, which is used in error messages. It checks that all the equations have the same number of arguments before using @tcMatches@ to do the work. - -Note [Polymorphic expected type for tcMatchesFun] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -tcMatchesFun may be given a *sigma* (polymorphic) type -so it must be prepared to use tcSkolemise to skolemise it. -See Note [sig_tau may be polymorphic] in GHC.Tc.Gen.Pat. -} tcMatchesFun :: Located Name -> MatchGroup GhcRn (LHsExpr GhcRn) - -> ExpSigmaType -- Expected type of function + -> ExpRhoType -- Expected type of function -> TcM (HsWrapper, MatchGroup GhcTcId (LHsExpr GhcTcId)) -- Returns type of body tcMatchesFun fn@(L _ fun_name) matches exp_ty @@ -102,20 +97,17 @@ tcMatchesFun fn@(L _ fun_name) matches exp_ty traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty) ; checkArgs fun_name matches - ; (wrap_gen, (wrap_fun, group)) - <- tcSkolemiseET (FunSigCtxt fun_name True) exp_ty $ \ exp_rho -> - -- Note [Polymorphic expected type for tcMatchesFun] - do { (matches', wrap_fun) - <- matchExpectedFunTys herald arity exp_rho $ - \ pat_tys rhs_ty -> - tcMatches match_ctxt pat_tys rhs_ty matches - ; return (wrap_fun, matches') } - ; return (wrap_gen <.> wrap_fun, group) } + ; matchExpectedFunTys herald ctxt arity exp_ty $ \ pat_tys rhs_ty -> + -- NB: exp_type may be polymorphic, but + -- matchExpectedFunTys can cope with that + tcMatches match_ctxt pat_tys rhs_ty matches } where - arity = matchGroupArity matches + arity = matchGroupArity matches herald = text "The equation(s) for" <+> quotes (ppr fun_name) <+> text "have" - what = FunRhs { mc_fun = fn, mc_fixity = Prefix, mc_strictness = strictness } + ctxt = GenSigCtxt -- Was: FunSigCtxt fun_name True + -- But that's wrong for f :: Int -> forall a. blah + what = FunRhs { mc_fun = fn, mc_fixity = Prefix, mc_strictness = strictness } match_ctxt = MC { mc_what = what, mc_body = tcBody } strictness | [L _ match] <- unLoc $ mg_alts matches @@ -144,10 +136,10 @@ tcMatchesCase ctxt scrut_ty matches res_ty tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in GHC.Tc.Utils.Unify -> TcMatchCtxt HsExpr -> MatchGroup GhcRn (LHsExpr GhcRn) - -> ExpRhoType -- deeply skolemised - -> TcM (MatchGroup GhcTcId (LHsExpr GhcTcId), HsWrapper) + -> ExpRhoType + -> TcM (HsWrapper, MatchGroup GhcTcId (LHsExpr GhcTcId)) tcMatchLambda herald match_ctxt match res_ty - = matchExpectedFunTys herald n_pats res_ty $ \ pat_tys rhs_ty -> + = matchExpectedFunTys herald GenSigCtxt n_pats res_ty $ \ pat_tys rhs_ty -> tcMatches match_ctxt pat_tys rhs_ty match where n_pats | isEmptyMatchGroup match = 1 -- must be lambda-case @@ -332,7 +324,7 @@ tcDoStmts ctxt _ _ = pprPanic "tcDoStmts" (pprStmtContext ctxt) tcBody :: LHsExpr GhcRn -> ExpRhoType -> TcM (LHsExpr GhcTcId) tcBody body res_ty = do { traceTc "tcBody" (ppr res_ty) - ; tcLExpr body res_ty + ; tcMonoExpr body res_ty } {- @@ -412,7 +404,7 @@ tcStmtsAndThen ctxt stmt_chk (L loc stmt : stmts) res_ty thing_inside tcGuardStmt :: TcExprStmtChecker tcGuardStmt _ (BodyStmt _ guard _ _) res_ty thing_inside - = do { guard' <- tcLExpr guard (mkCheckExpType boolTy) + = do { guard' <- tcCheckMonoExpr guard boolTy ; thing <- thing_inside res_ty ; return (BodyStmt boolTy guard' noSyntaxExpr noSyntaxExpr, thing) } @@ -445,21 +437,21 @@ tcLcStmt :: TyCon -- The list type constructor ([]) -> TcExprStmtChecker tcLcStmt _ _ (LastStmt x body noret _) elt_ty thing_inside - = do { body' <- tcLExprNC body elt_ty + = do { body' <- tcMonoExprNC body elt_ty ; thing <- thing_inside (panic "tcLcStmt: thing_inside") ; return (LastStmt x body' noret noSyntaxExpr, thing) } -- A generator, pat <- rhs tcLcStmt m_tc ctxt (BindStmt _ pat rhs) elt_ty thing_inside = do { pat_ty <- newFlexiTyVarTy liftedTypeKind - ; rhs' <- tcLExpr rhs (mkCheckExpType $ mkTyConApp m_tc [pat_ty]) + ; rhs' <- tcCheckMonoExpr rhs (mkTyConApp m_tc [pat_ty]) ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ thing_inside elt_ty ; return (mkTcBindStmt pat' rhs', thing) } -- A boolean guard tcLcStmt _ _ (BodyStmt _ rhs _ _) elt_ty thing_inside - = do { rhs' <- tcLExpr rhs (mkCheckExpType boolTy) + = do { rhs' <- tcCheckMonoExpr rhs boolTy ; thing <- thing_inside elt_ty ; return (BodyStmt boolTy rhs' noSyntaxExpr noSyntaxExpr, thing) } @@ -517,7 +509,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts by_arrow $ poly_arg_ty `mkVisFunTy` poly_res_ty - ; using' <- tcCheckExpr using using_poly_ty + ; using' <- tcCheckPolyExpr using using_poly_ty ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using' -- 'stmts' returns a result of type (m1_ty tuple_ty), @@ -559,7 +551,7 @@ tcMcStmt _ (LastStmt x body noret return_op) res_ty thing_inside = do { (body', return_op') <- tcSyntaxOp MCompOrigin return_op [SynRho] res_ty $ \ [a_ty] -> - tcLExprNC body (mkCheckExpType a_ty) + tcCheckMonoExprNC body a_ty ; thing <- thing_inside (panic "tcMcStmt: thing_inside") ; return (LastStmt x body' noret return_op', thing) } @@ -575,7 +567,7 @@ tcMcStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside <- tcSyntaxOp MCompOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] -> - do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty) + do { rhs' <- tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ thing_inside (mkCheckExpType new_res_ty) ; return (rhs', pat', thing, new_res_ty) } @@ -607,7 +599,7 @@ tcMcStmt _ (BodyStmt _ rhs then_op guard_op) res_ty thing_inside <- tcSyntaxOp MCompOrigin guard_op [SynAny] (mkCheckExpType rhs_ty) $ \ [test_ty] -> - tcLExpr rhs (mkCheckExpType test_ty) + tcCheckMonoExpr rhs test_ty ; thing <- thing_inside (mkCheckExpType new_res_ty) ; return (thing, rhs', rhs_ty, guard_op') } ; return (BodyStmt rhs_ty rhs' then_op' guard_op', thing) } @@ -667,8 +659,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap (mkCheckExpType using_arg_ty) $ \res_ty' -> do { by' <- case by of Nothing -> return Nothing - Just e -> do { e' <- tcLExpr e - (mkCheckExpType by_e_ty) + Just e -> do { e' <- tcCheckMonoExpr e by_e_ty ; return (Just e') } -- Find the Ids (and hence types) of all old binders @@ -693,7 +684,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap --------------- Typecheck the 'fmap' function ------------- ; fmap_op' <- case form of ThenForm -> return noExpr - _ -> fmap unLoc . tcCheckExpr (noLoc fmap_op) $ + _ -> fmap unLoc . tcCheckPolyExpr (noLoc fmap_op) $ mkInfForAllTy alphaTyVar $ mkInfForAllTy betaTyVar $ (alphaTy `mkVisFunTy` betaTy) @@ -703,7 +694,7 @@ tcMcStmt ctxt (TransStmt { trS_stmts = stmts, trS_bndrs = bindersMap --------------- Typecheck the 'using' function ------------- -- using :: ((a,b,c)->t) -> m1 (a,b,c) -> m2 (n (a,b,c)) - ; using' <- tcCheckExpr using using_poly_ty + ; using' <- tcCheckPolyExpr using using_poly_ty ; let final_using = fmap (mkHsWrap (WpTyApp tup_ty)) using' --------------- Building the bindersMap ---------------- @@ -765,7 +756,7 @@ tcMcStmt ctxt (ParStmt _ bndr_stmts_s mzip_op bind_op) res_ty thing_inside (m_ty `mkAppTy` betaTy) `mkVisFunTy` (m_ty `mkAppTy` mkBoxedTupleTy [alphaTy, betaTy]) - ; mzip_op' <- unLoc `fmap` tcCheckExpr (noLoc mzip_op) mzip_ty + ; mzip_op' <- unLoc `fmap` tcCheckPolyExpr (noLoc mzip_op) mzip_ty -- type dummies since we don't know all binder types yet ; id_tys_s <- (mapM . mapM) (const (newFlexiTyVarTy liftedTypeKind)) @@ -827,7 +818,7 @@ tcMcStmt _ stmt _ _ tcDoStmt :: TcExprStmtChecker tcDoStmt _ (LastStmt x body noret _) res_ty thing_inside - = do { body' <- tcLExprNC body res_ty + = do { body' <- tcMonoExprNC body res_ty ; thing <- thing_inside (panic "tcDoStmt: thing_inside") ; return (LastStmt x body' noret noSyntaxExpr, thing) } @@ -840,7 +831,7 @@ tcDoStmt ctxt (BindStmt xbsrn pat rhs) res_ty thing_inside ((rhs', pat', new_res_ty, thing), bind_op') <- tcSyntaxOp DoOrigin (xbsrn_bindOp xbsrn) [SynRho, SynFun SynAny SynRho] res_ty $ \ [rhs_ty, pat_ty, new_res_ty] -> - do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty) + do { rhs' <- tcCheckMonoExprNC rhs rhs_ty ; (pat', thing) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ thing_inside (mkCheckExpType new_res_ty) ; return (rhs', pat', new_res_ty, thing) } @@ -873,7 +864,7 @@ tcDoStmt _ (BodyStmt _ rhs then_op _) res_ty thing_inside ; ((rhs', rhs_ty, thing), then_op') <- tcSyntaxOp DoOrigin then_op [SynRho, SynRho] res_ty $ \ [rhs_ty, new_res_ty] -> - do { rhs' <- tcLExprNC rhs (mkCheckExpType rhs_ty) + do { rhs' <- tcCheckMonoExprNC rhs rhs_ty ; thing <- thing_inside (mkCheckExpType new_res_ty) ; return (rhs', rhs_ty, thing) } ; return (BodyStmt rhs_ty rhs' then_op' noSyntaxExpr, thing) } @@ -1043,7 +1034,7 @@ tcApplicativeStmts ctxt pairs rhs_ty thing_inside }, pat_ty, exp_ty) = setSrcSpan (combineSrcSpans (getLoc pat) (getLoc rhs)) $ addErrCtxt (pprStmtInCtxt ctxt (mkRnBindStmt pat rhs)) $ - do { rhs' <- tcLExprNC rhs (mkCheckExpType exp_ty) + do { rhs' <- tcCheckMonoExprNC rhs exp_ty ; (pat', _) <- tcCheckPat (StmtCtxt ctxt) pat pat_ty $ return () ; fail_op' <- fmap join . forM fail_op $ \fail -> diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs index 58f64f84ae..21b5165d5b 100644 --- a/compiler/GHC/Tc/Gen/Pat.hs +++ b/compiler/GHC/Tc/Gen/Pat.hs @@ -30,7 +30,7 @@ where import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferSigma ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcSyntaxOp, tcSyntaxOpGen, tcInferRho ) import GHC.Hs import GHC.Tc.Utils.Zonk @@ -406,16 +406,13 @@ tc_pat pat_ty penv ps_pat thing_inside = case ps_pat of -- An exotic example: -- pair :: forall a. a -> forall b. b -> (a,b) -- f (pair True -> x) = ...here (x :: forall b. b -> (Bool,b)) - -- - -- TEMPORARY: pending simple subsumption, use tcInferSigma - -- When removing this, remove it from Expr.hs-boot too - ; (expr',expr_ty) <- tcInferSigma expr + ; (expr',expr_ty) <- tcInferRho expr -- Expression must be a function ; let expr_orig = lexprCtOrigin expr herald = text "A view pattern expression expects" ; (expr_wrap1, [inf_arg_ty], inf_res_ty) - <- matchActualFunTys herald expr_orig (Just (unLoc expr)) 1 expr_ty + <- matchActualFunTysRho herald expr_orig (Just (unLoc expr)) 1 expr_ty -- expr_wrap1 :: expr_ty "->" (inf_arg_ty -> inf_res_ty) -- Check that overall pattern is more polymorphic than arg type diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs index c788f15437..63377c74d5 100644 --- a/compiler/GHC/Tc/Gen/Rule.hs +++ b/compiler/GHC/Tc/Gen/Rule.hs @@ -199,7 +199,7 @@ generateRuleConstraints ty_bndrs tm_bndrs lhs rhs do { -- See Note [Solve order for RULES] ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs) ; (rhs', rhs_wanted) <- captureConstraints $ - tcLExpr rhs (mkCheckExpType rule_ty) + tcCheckMonoExpr rhs rule_ty ; let all_lhs_wanted = bndr_wanted `andWC` lhs_wanted ; return (id_bndrs, lhs', all_lhs_wanted, rhs', rhs_wanted, rule_ty) } } diff --git a/compiler/GHC/Tc/Gen/Sig.hs b/compiler/GHC/Tc/Gen/Sig.hs index fb313d9297..2ac2823fb5 100644 --- a/compiler/GHC/Tc/Gen/Sig.hs +++ b/compiler/GHC/Tc/Gen/Sig.hs @@ -635,6 +635,7 @@ to connect the two, something like This wrapper is put in the TcSpecPrag, in the ABExport record of the AbsBinds. + f :: (Eq a, Ix b) => a -> b -> Bool {-# SPECIALISE f :: (Ix p, Ix q) => Int -> (p,q) -> Bool #-} f = <poly_rhs> @@ -674,12 +675,13 @@ delicate, but works. Some wrinkles -1. We don't use full-on tcSubType, because that does co and contra - variance and that in turn will generate too complex a LHS for the - RULE. So we use a single invocation of skolemise / - topInstantiate in tcSpecWrapper. (Actually I think that even - the "deeply" stuff may be too much, because it introduces lambdas, - though I think it can be made to work without too much trouble.) +1. In tcSpecWrapper, rather than calling tcSubType, we directly call + skolemise/instantiate. That is mainly because of wrinkle (2). + + Historical note: in the past, tcSubType did co/contra stuff, which + could generate too complex a LHS for the RULE, which was another + reason for not using tcSubType. But that reason has gone away + with simple subsumption (#17775). 2. We need to take care with type families (#5821). Consider type instance F Int = Bool @@ -775,7 +777,7 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper -- See Note [Handling SPECIALISE pragmas], wrinkle 1 tcSpecWrapper ctxt poly_ty spec_ty = do { (sk_wrap, inst_wrap) - <- tcSkolemise ctxt spec_ty $ \ _ spec_tau -> + <- tcSkolemise ctxt spec_ty $ \ spec_tau -> do { (inst_wrap, tau) <- topInstantiate orig poly_ty ; _ <- unifyType Nothing spec_tau tau -- Deliberately ignore the evidence diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs index aa792ee6b7..766704166d 100644 --- a/compiler/GHC/Tc/Gen/Splice.hs +++ b/compiler/GHC/Tc/Gen/Splice.hs @@ -288,7 +288,7 @@ tcPendingSplice m_var (PendingRnSplice flavour splice_name expr) = do { meta_ty <- tcMetaTy meta_ty_name -- Expected type of splice, e.g. m Exp ; let expected_type = mkAppTy m_var meta_ty - ; expr' <- tcCheckExpr expr expected_type + ; expr' <- tcCheckPolyExpr expr expected_type ; return (PendingTcSplice splice_name expr') } where meta_ty_name = case flavour of @@ -618,7 +618,7 @@ tcNestedSplice pop_stage (TcPending ps_var lie_var q@(QuoteWrapper _ m_var)) spl ; meta_exp_ty <- tcTExpTy m_var res_ty ; expr' <- setStage pop_stage $ setConstraintVar lie_var $ - tcLExpr expr (mkCheckExpType meta_exp_ty) + tcCheckMonoExpr expr meta_exp_ty ; untypeq <- tcLookupId unTypeQName ; let expr'' = mkHsApp (mkLHsWrap (applyQuoteWrapper q) @@ -647,7 +647,7 @@ tcTopSplice expr res_ty -- Top level splices must still be of type Q (TExp a) ; meta_exp_ty <- tcTExpTy q_type res_ty ; q_expr <- tcTopSpliceExpr Typed $ - tcLExpr expr (mkCheckExpType meta_exp_ty) + tcCheckMonoExpr expr meta_exp_ty ; lcl_env <- getLclEnv ; let delayed_splice = DelayedSplice lcl_env expr res_ty q_expr @@ -684,7 +684,7 @@ runTopSplice (DelayedSplice lcl_env orig_expr res_ty q_expr) captureConstraints $ addErrCtxt (spliceResultDoc zonked_q_expr) $ do { (exp3, _fvs) <- rnLExpr expr2 - ; tcLExpr exp3 (mkCheckExpType zonked_ty)} + ; tcCheckMonoExpr exp3 zonked_ty } ; ev <- simplifyTop wcs ; return $ unLoc (mkHsDictLet (EvBinds ev) res) } @@ -717,7 +717,7 @@ tcTopSpliceExpr :: SpliceType -> TcM (LHsExpr GhcTc) -> TcM (LHsExpr GhcTc) -- Note that set the level to Splice, regardless of the original level, -- before typechecking the expression. For example: -- f x = $( ...$(g 3) ... ) --- The recursive call to tcCheckExpr will simply expand the +-- The recursive call to tcCheckPolyExpr will simply expand the -- inner escape before dealing with the outer one tcTopSpliceExpr isTypedSplice tc_action @@ -1438,7 +1438,7 @@ reifyInstances th_nm th_tys <- pushTcLevelM_ $ solveEqualities $ -- Avoid error cascade if there are unsolved bindImplicitTKBndrs_Skol tv_names $ - fst <$> tcLHsType rn_ty + tcInferLHsType rn_ty ; ty <- zonkTcTypeToType ty -- Substitute out the meta type variables -- In particular, the type might have kind diff --git a/compiler/GHC/Tc/Module.hs b/compiler/GHC/Tc/Module.hs index 94402c0989..dab7bc499e 100644 --- a/compiler/GHC/Tc/Module.hs +++ b/compiler/GHC/Tc/Module.hs @@ -1781,11 +1781,11 @@ check_main dflags tcg_env explicit_mod_hdr export_ies ; res_ty <- newFlexiTyVarTy liftedTypeKind ; let io_ty = mkTyConApp ioTyCon [res_ty] skol_info = SigSkol (FunSigCtxt main_name False) io_ty [] + main_expr_rn = L loc (HsVar noExtField (L loc main_name)) ; (ev_binds, main_expr) <- checkConstraints skol_info [] [] $ addErrCtxt mainCtxt $ - tcLExpr (L loc (HsVar noExtField (L loc main_name))) - (mkCheckExpType io_ty) + tcCheckMonoExpr main_expr_rn io_ty -- See Note [Root-main Id] -- Construct the binding @@ -2476,6 +2476,7 @@ data TcRnExprMode = TM_Inst -- ^ Instantiate the type fully (:type) | TM_Default -- ^ Default the type eagerly (:type +d) -- | tcRnExpr just finds the type of an expression +-- for :type tcRnExpr :: HscEnv -> TcRnExprMode -> LHsExpr GhcPs @@ -2590,7 +2591,7 @@ tcRnType hsc_env flexi normalise rdr_type solveEqualities $ tcNamedWildCardBinders wcs $ \ wcs' -> do { mapM_ emitNamedTypeHole wcs' - ; tcLHsTypeUnsaturated rn_type } + ; tcInferLHsTypeUnsaturated rn_type } -- Do kind generalisation; see Note [Kind-generalise in tcRnType] ; kvs <- kindGeneralizeAll kind @@ -2623,7 +2624,7 @@ considers this example, with -fprint-explicit-foralls enabled: In this mode, we report the type that would be inferred if a variable were assigned to expression e, without applying the monomorphism restriction. - This means we deeply instantiate the type and then regeneralize, as discussed + This means we instantiate the type and then regeneralize, as discussed in #11376. > :type foo @Int diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs index b1017de024..8736206188 100644 --- a/compiler/GHC/Tc/Solver.hs +++ b/compiler/GHC/Tc/Solver.hs @@ -16,8 +16,7 @@ module GHC.Tc.Solver( simpl_top, - promoteTyVar, - promoteTyVarSet, + promoteTyVarSet, emitFlatConstraints, -- For Rules we need these solveWanteds, solveWantedsAndDrop, @@ -65,7 +64,6 @@ import Control.Monad import Data.Foldable ( toList ) import Data.List ( partition ) import Data.List.NonEmpty ( NonEmpty(..) ) -import GHC.Data.Maybe ( isJust ) {- ********************************************************************************* @@ -162,27 +160,143 @@ simplifyTop wanteds -- should generally bump the TcLevel to make sure that this run of the solver -- doesn't affect anything lying around. solveLocalEqualities :: String -> TcM a -> TcM a +-- Note [Failure in local type signatures] solveLocalEqualities callsite thing_inside = do { (wanted, res) <- solveLocalEqualitiesX callsite thing_inside - ; emitConstraints wanted + ; emitFlatConstraints wanted + ; return res } - -- See Note [Fail fast if there are insoluble kind equalities] - ; when (insolubleWC wanted) $ - failM +emitFlatConstraints :: WantedConstraints -> TcM () +-- See Note [Failure in local type signatures] +emitFlatConstraints wanted + = do { wanted <- TcM.zonkWC wanted + ; case floatKindEqualities wanted of + Nothing -> do { traceTc "emitFlatConstraints: failing" (ppr wanted) + ; emitConstraints wanted -- So they get reported! + ; failM } + Just (simples, holes) + -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples) + ; traceTc "emitFlatConstraints:" $ + vcat [ text "simples:" <+> ppr simples + , text "holes: " <+> ppr holes ] + ; emitHoles holes -- Holes don't need promotion + ; emitSimples simples } } + +floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole) +-- Float out all the constraints from the WantedConstraints, +-- Return Nothing if any constraints can't be floated (captured +-- by skolems), or if there is an insoluble constraint, or +-- IC_Telescope telescope error +floatKindEqualities wc = float_wc emptyVarSet wc + where + float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag Hole) + float_wc trapping_tvs (WC { wc_simple = simples + , wc_impl = implics + , wc_holes = holes }) + | all is_floatable simples + = do { (inner_simples, inner_holes) + <- flatMapBagPairM (float_implic trapping_tvs) implics + ; return ( simples `unionBags` inner_simples + , holes `unionBags` inner_holes) } + | otherwise + = Nothing + where + is_floatable ct + | insolubleEqCt ct = False + | otherwise = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs + + float_implic :: TcTyCoVarSet -> Implication -> Maybe (Bag Ct, Bag Hole) + float_implic trapping_tvs (Implic { ic_wanted = wanted, ic_no_eqs = no_eqs + , ic_skols = skols, ic_status = status }) + | isInsolubleStatus status + = Nothing -- A short cut /plus/ we must keep track of IC_BadTelescope + | otherwise + = do { (simples, holes) <- float_wc new_trapping_tvs wanted + ; when (not (isEmptyBag simples) && not no_eqs) $ + Nothing + -- If there are some constraints to float out, but we can't + -- because we don't float out past local equalities + -- (c.f GHC.Tc.Solver.approximateWC), then fail + ; return (simples, holes) } + where + new_trapping_tvs = trapping_tvs `extendVarSetList` skols - ; return res } -{- Note [Fail fast if there are insoluble kind equalities] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Rather like in simplifyInfer, fail fast if there is an insoluble -constraint. Otherwise we'll just succeed in kind-checking a nonsense -type, with a cascade of follow-up errors. +{- Note [Failure in local type signatures] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +When kind checking a type signature, we like to fail fast if we can't +solve all the kind equality constraints: see Note [Fail fast on kind +errors]. But what about /local/ type signatures, mentioning in-scope +type variables for which there might be given equalities. Here's +an example (T15076b): + + class (a ~ b) => C a b + data SameKind :: k -> k -> Type where { SK :: SameKind a b } + + bar :: forall (a :: Type) (b :: Type). + C a b => Proxy a -> Proxy b -> () + bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y) + +Consider the type singature on 'undefined'. It's ill-kinded unless +a~b. But the superclass of (C a b) means that indeed (a~b). So all +should be well. BUT it's hard to see that when kind-checking the signature +for undefined. We want to emit a residual (a~b) constraint, to solve +later. + +Another possiblity is that we might have something like + F alpha ~ [Int] +where alpha is bound further out, which might become soluble +"later" when we learn more about alpha. So we want to emit +those residual constraints. + +BUT it's no good simply wrapping all unsolved constraints from +a type signature in an implication constraint to solve later. The +problem is that we are going to /use/ that signature, including +instantiate it. Say we have + f :: forall a. (forall b. blah) -> blah2 + f x = <body> +To typecheck the definition of f, we have to instantiate those +foralls. Moreover, any unsolved kind equalities will be coercion +holes in the type. If we naively wrap them in an implication like + forall a. (co1:k1~k2, forall b. co2:k3~k4) +hoping to solve it later, we might end up filling in the holes +co1 and co2 with coercions involving 'a' and 'b' -- but by now +we've instantiated the type. Chaos! + +Moreover, the unsolved constraints might be skolem-escpae things, and +if we proceed with f bound to a nonsensical type, we get a cascade of +follow-up errors. For example polykinds/T12593, T15577, and many others. + +So here's the plan: -For example polykinds/T12593, T15577, and many others. +* solveLocalEqualitiesX: try to solve the constraints (solveLocalEqualitiesX) -Take care to ensure that you emit the insoluble constraints before -failing, because they are what will ultimately lead to the error -messsage! +* buildTvImplication: build an implication for the residual, unsolved + constraint + +* emitFlatConstraints: try to float out every unsolved equalities + inside that implication, in the hope that it constrains only global + type variables, not the locally-quantified ones. + + * If we fail, or find an insoluble constraint, emit the implication, + so that the errors will be reported, and fail. + + * If we succeed in floating all the equalities, promote them and + re-emit them as flat constraint, not wrapped at all (since they + don't mention any of the quantified variables. + +* Note that this float-and-promote step means that anonymous + wildcards get floated to top level, as we want; see + Note [Checking partial type signatures] in GHC.Tc.Gen.HsType. + +All this is done: + +* in solveLocalEqualities, where there is no kind-generalisation + to complicate matters. + +* in GHC.Tc.Gen.HsType.tcHsSigType, where quantification intervenes. + +See also #18062, #11506 -} solveLocalEqualitiesX :: String -> TcM a -> TcM (WantedConstraints, a) @@ -867,7 +981,6 @@ mkResidualConstraints rhs_tclvl ev_binds_var return $ unitBag $ implic1 { ic_tclvl = rhs_tclvl , ic_skols = qtvs - , ic_telescope = Nothing , ic_given = full_theta_vars , ic_wanted = inner_wanted , ic_binds = ev_binds_var @@ -1168,7 +1281,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates = do { -- Promote any tyvars that we cannot generalise -- See Note [Promote momomorphic tyvars] ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs) - ; (prom, _) <- promoteTyVarSet mono_tvs + ; any_promoted <- promoteTyVarSet mono_tvs -- Default any kind/levity vars ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} @@ -1186,7 +1299,7 @@ defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates ; case () of _ | some_default -> simplify_cand candidates - | prom -> mapM TcM.zonkTcType candidates + | any_promoted -> mapM TcM.zonkTcType candidates | otherwise -> return candidates } where @@ -1789,9 +1902,9 @@ setImplicationStatus implic@(Implic { ic_status = status checkBadTelescope :: Implication -> TcS Bool -- True <=> the skolems form a bad telescope -- See Note [Checking telescopes] in GHC.Tc.Types.Constraint -checkBadTelescope (Implic { ic_telescope = m_telescope - , ic_skols = skols }) - | isJust m_telescope +checkBadTelescope (Implic { ic_info = info + , ic_skols = skols }) + | ForAllSkol {} <- info = do{ skols <- mapM TcS.zonkTyCoVarKind skols ; return (go emptyVarSet (reverse skols))} @@ -2063,7 +2176,7 @@ we'll get more Givens (a unification is like adding a Given) to allow the implication to make progress. -} -promoteTyVar :: TcTyVar -> TcM (Bool, TcTyVar) +promoteTyVar :: TcTyVar -> TcM Bool -- When we float a constraint out of an implication we must restore -- invariant (WantedInv) in Note [TcLevel and untouchable type variables] in GHC.Tc.Utils.TcType -- Return True <=> we did some promotion @@ -2075,16 +2188,16 @@ promoteTyVar tv then do { cloned_tv <- TcM.cloneMetaTyVar tv ; let rhs_tv = setMetaTyVarTcLevel cloned_tv tclvl ; TcM.writeMetaTyVar tv (mkTyVarTy rhs_tv) - ; return (True, rhs_tv) } - else return (False, tv) } + ; return True } + else return False } -- Returns whether or not *any* tyvar is defaulted -promoteTyVarSet :: TcTyVarSet -> TcM (Bool, TcTyVarSet) +promoteTyVarSet :: TcTyVarSet -> TcM Bool promoteTyVarSet tvs - = do { (bools, tyvars) <- mapAndUnzipM promoteTyVar (nonDetEltsUniqSet tvs) - -- non-determinism is OK because order of promotion doesn't matter + = do { bools <- mapM promoteTyVar (nonDetEltsUniqSet tvs) + -- Non-determinism is OK because order of promotion doesn't matter - ; return (or bools, mkVarSet tyvars) } + ; return (or bools) } promoteTyVarTcS :: TcTyVar -> TcS () -- When we float a constraint out of an implication we must restore @@ -2122,7 +2235,7 @@ approximateWC float_past_equalities wc float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics }) = filterBag (is_floatable trapping_tvs) simples `unionBags` - do_bag (float_implic trapping_tvs) implics + concatMapBag (float_implic trapping_tvs) implics where float_implic :: TcTyCoVarSet -> Implication -> Cts @@ -2134,9 +2247,6 @@ approximateWC float_past_equalities wc where new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp - do_bag :: (a -> Bag c) -> Bag a -> Bag c - do_bag f = foldr (unionBags.f) emptyBag - is_floatable skol_tvs ct | isGivenCt ct = False | insolubleEqCt ct = False @@ -2419,21 +2529,20 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs | otherwise = acc -- Identify which equalities are candidates for floating - -- Float out alpha ~ ty, or ty ~ alpha which might be unified outside + -- Float out alpha ~ ty which might be unified outside -- See Note [Which equalities to float] is_float_eq_candidate ct | pred <- ctPred ct , EqPred NomEq ty1 ty2 <- classifyPredType pred - = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of - (Just tv1, _) -> float_tv_eq_candidate tv1 ty2 - (_, Just tv2) -> float_tv_eq_candidate tv2 ty1 - _ -> False - | otherwise = False - - float_tv_eq_candidate tv1 ty2 -- See Note [Which equalities to float] - = isMetaTyVar tv1 - && (not (isTyVarTyVar tv1) || isTyVarTy ty2) + = float_eq ty1 ty2 || float_eq ty2 ty1 + | otherwise + = False + float_eq ty1 ty2 + = case getTyVar_maybe ty1 of + Just tv1 -> isMetaTyVar tv1 + && (not (isTyVarTyVar tv1) || isTyVarTy ty2) + Nothing -> False {- Note [Float equalities from under a skolem binding] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -2470,6 +2579,12 @@ happen. In particular, float out equalities that are: case, floating out won't help either, and it may affect grouping of error messages. + NB: generally we won't see (ty ~ alpha), with alpha on the right because + of Note [Unification variables on the left] in GHC.Tc.Utils.Unify. + But if we start with (F tys ~ alpha), it will orient as (fmv ~ alpha), + and unflatten back to (F tys ~ alpha). So we must look for alpha on + the right too. Example T4494. + * Nominal. No point in floating (alpha ~R# ty), because we do not unify representational equalities even if alpha is touchable. See Note [Do not unify representational equalities] in GHC.Tc.Solver.Interact. diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs index 57cf913aa4..1bf603d3fd 100644 --- a/compiler/GHC/Tc/Solver/Canonical.hs +++ b/compiler/GHC/Tc/Solver/Canonical.hs @@ -904,22 +904,23 @@ It is conceivable to do a better job at tracking whether or not a type is flattened, but this is left as future work. (Mar '15) -Note [FunTy and decomposing tycon applications] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked. -This means that we may very well have a FunTy containing a type of some unknown -kind. For instance, we may have, +Note [Decomposing FunTy] +~~~~~~~~~~~~~~~~~~~~~~~~ +can_eq_nc' may attempt to decompose a FunTy that is un-zonked. This +means that we may very well have a FunTy containing a type of some +unknown kind. For instance, we may have, FunTy (a :: k) Int -Where k is a unification variable. tcRepSplitTyConApp_maybe panics in the event -that it sees such a type as it cannot determine the RuntimeReps which the (->) -is applied to. Consequently, it is vital that we instead use -tcRepSplitTyConApp_maybe', which simply returns Nothing in such a case. - -When this happens can_eq_nc' will fail to decompose, zonk, and try again. +Where k is a unification variable. So the calls to getRuntimeRep_maybe may +fail (returning Nothing). In that case we'll fall through, zonk, and try again. Zonking should fill the variable k, meaning that decomposition will succeed the second time around. + +Also note that we require the AnonArgFlag to match. This will stop +us decomposing + (Int -> Bool) ~ (Show a => blah) +It's as if we treat (->) and (=>) as different type constructors. -} canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct) @@ -1003,13 +1004,26 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _ = do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1) ; stopWith ev "Equal LitTy" } --- Try to decompose type constructor applications --- Including FunTy (s -> t) -can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _ - --- See Note [FunTy and decomposing type constructor applications]. - | Just (tc1, tys1) <- repSplitTyConApp_maybe ty1 - , Just (tc2, tys2) <- repSplitTyConApp_maybe ty2 - , not (isTypeFamilyTyCon tc1) +-- Decompose FunTy: (s -> t) and (c => t) +-- NB: don't decompose (Int -> blah) ~ (Show a => blah) +can_eq_nc' _flat _rdr_env _envs ev eq_rel + (FunTy { ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ + (FunTy { ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ + | af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah) + , Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe: + , Just ty1b_rep <- getRuntimeRep_maybe ty1b -- see Note [Decomposing FunTy] + , Just ty2a_rep <- getRuntimeRep_maybe ty2a + , Just ty2b_rep <- getRuntimeRep_maybe ty2b + = canDecomposableTyConAppOK ev eq_rel funTyCon + [ty1a_rep, ty1b_rep, ty1a, ty1b] + [ty2a_rep, ty2b_rep, ty2a, ty2b] + +-- Decompose type constructor applications +-- NB: e have expanded type synonyms already +can_eq_nc' _flat _rdr_env _envs ev eq_rel + (TyConApp tc1 tys1) _ + (TyConApp tc2 tys2) _ + | not (isTypeFamilyTyCon tc1) , not (isTypeFamilyTyCon tc2) = canTyConApp ev eq_rel tc1 tys1 tc2 tys2 @@ -1452,15 +1466,13 @@ canTyConApp :: CtEvidence -> EqRel -> TyCon -> [TcType] -> TcS (StopOrContinue Ct) -- See Note [Decomposing TyConApps] +-- Neither tc1 nor tc2 is a saturated funTyCon canTyConApp ev eq_rel tc1 tys1 tc2 tys2 | tc1 == tc2 , tys1 `equalLength` tys2 = do { inerts <- getTcSInerts ; if can_decompose inerts - then do { traceTcS "canTyConApp" - (ppr ev $$ ppr eq_rel $$ ppr tc1 $$ ppr tys1 $$ ppr tys2) - ; canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 - ; stopWith ev "Decomposed TyConApp" } + then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2 else canEqFailure ev eq_rel ty1 ty2 } -- See Note [Skolem abstract data] (at tyConSkolem) @@ -1476,6 +1488,10 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2 | otherwise = canEqHardFailure ev ty1 ty2 where + -- Reconstruct the types for error messages. This would do + -- the wrong thing (from a pretty printing point of view) + -- for functions, because we've lost the AnonArgFlag; but + -- in fact we never call canTyConApp on a saturated FunTyCon ty1 = mkTyConApp tc1 tys1 ty2 = mkTyConApp tc2 tys2 @@ -1673,30 +1689,35 @@ Conclusion: canDecomposableTyConAppOK :: CtEvidence -> EqRel -> TyCon -> [TcType] -> [TcType] - -> TcS () + -> TcS (StopOrContinue Ct) -- Precondition: tys1 and tys2 are the same length, hence "OK" canDecomposableTyConAppOK ev eq_rel tc tys1 tys2 = ASSERT( tys1 `equalLength` tys2 ) - case ev of - CtDerived {} - -> unifyDeriveds loc tc_roles tys1 tys2 - - CtWanted { ctev_dest = dest } - -- new_locs and tc_roles are both infinite, so - -- we are guaranteed that cos has the same length - -- as tys1 and tys2 - -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 - ; setWantedEq dest (mkTyConAppCo role tc cos) } - - CtGiven { ctev_evar = evar } - -> do { let ev_co = mkCoVarCo evar - ; given_evs <- newGivenEvVars loc $ - [ ( mkPrimEqPredRole r ty1 ty2 - , evCoercion $ mkNthCo r i ev_co ) - | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] - , r /= Phantom - , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] - ; emitWorkNC given_evs } + do { traceTcS "canDecomposableTyConAppOK" + (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2) + ; case ev of + CtDerived {} + -> unifyDeriveds loc tc_roles tys1 tys2 + + CtWanted { ctev_dest = dest } + -- new_locs and tc_roles are both infinite, so + -- we are guaranteed that cos has the same length + -- as tys1 and tys2 + -> do { cos <- zipWith4M unifyWanted new_locs tc_roles tys1 tys2 + ; setWantedEq dest (mkTyConAppCo role tc cos) } + + CtGiven { ctev_evar = evar } + -> do { let ev_co = mkCoVarCo evar + ; given_evs <- newGivenEvVars loc $ + [ ( mkPrimEqPredRole r ty1 ty2 + , evCoercion $ mkNthCo r i ev_co ) + | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] + , r /= Phantom + , not (isCoercionTy ty1) && not (isCoercionTy ty2) ] + ; emitWorkNC given_evs } + + ; stopWith ev "Decomposed TyConApp" } + where loc = ctEvLoc ev role = eqRelRole eq_rel @@ -1747,7 +1768,8 @@ canEqHardFailure :: CtEvidence -> TcType -> TcType -> TcS (StopOrContinue Ct) -- See Note [Make sure that insolubles are fully rewritten] canEqHardFailure ev ty1 ty2 - = do { (s1, co1) <- flatten FM_SubstOnly ev ty1 + = do { traceTcS "canEqHardFailure" (ppr ty1 $$ ppr ty2) + ; (s1, co1) <- flatten FM_SubstOnly ev ty1 ; (s2, co2) <- flatten FM_SubstOnly ev ty2 ; new_ev <- rewriteEqEvidence ev NotSwapped s1 s2 co1 co2 ; continueWith (mkIrredCt InsolubleCIS new_ev) } @@ -2007,7 +2029,7 @@ canEqTyVarHomo ev eq_rel swapped tv1 ps_xi1 xi2 _ -- this guarantees (TyEq:TV) | Just (tv2, co2) <- tcGetCastedTyVar_maybe xi2 - , swapOverTyVars tv1 tv2 + , swapOverTyVars (isGiven ev) tv1 tv2 = do { traceTcS "canEqTyVar swapOver" (ppr tv1 $$ ppr tv2 $$ ppr swapped) ; let role = eqRelRole eq_rel sym_co2 = mkTcSymCo co2 diff --git a/compiler/GHC/Tc/Solver/Flatten.hs b/compiler/GHC/Tc/Solver/Flatten.hs index 4dff585840..7f0b6a6120 100644 --- a/compiler/GHC/Tc/Solver/Flatten.hs +++ b/compiler/GHC/Tc/Solver/Flatten.hs @@ -1174,7 +1174,7 @@ flatten_one (TyConApp tc tys) -- _ -> fmode = flatten_ty_con_app tc tys -flatten_one ty@(FunTy _ ty1 ty2) +flatten_one ty@(FunTy { ft_arg = ty1, ft_res = ty2 }) = do { (xi1,co1) <- flatten_one ty1 ; (xi2,co2) <- flatten_one ty2 ; role <- getRole diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs index 144021caea..98550132c5 100644 --- a/compiler/GHC/Tc/TyCl.hs +++ b/compiler/GHC/Tc/TyCl.hs @@ -2313,18 +2313,18 @@ newtype instance T [a] :: <kind> where ... -- See Point 5 2. Where these kinds come from: Return kinds are processed through several different code paths: - data/newtypes: The return kind is part of the TyCon kind, gotten either + Data/newtypes: The return kind is part of the TyCon kind, gotten either by checkInitialKind (standalone kind signature / CUSK) or inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is then passed to tcDataDefn. - families: The return kind is either written in a standalone signature + Families: The return kind is either written in a standalone signature or extracted from a family declaration in getInitialKind. If a family declaration is missing a result kind, it is assumed to be Type. This assumption is in getInitialKind for CUSKs or get_fam_decl_initial_kind for non-signature & non-CUSK cases. - instances: The data family already has a known kind. The return kind + Instances: The data family already has a known kind. The return kind of an instance is then calculated by applying the data family tycon to the patterns provided, as computed by the typeKind lhs_ty in the end of tcDataFamInstHeader. In the case of an instance written in GADT @@ -2350,10 +2350,9 @@ newtype instance T [a] :: <kind> where ... -- See Point 5 4. Datatype return kind restriction: A data/data-instance return kind must end in a type that, after type-synonym expansion, yields `TYPE LiftedRep`. By "end in", we mean we strip any foralls and function arguments off before - checking: this remaining part of the type is returned from - etaExpandAlgTyCon. Note that we do *not* do type family reduction here. - Examples: + checking: this remaining part of the type is returned from etaExpandAlgTyCon. + Examples: data T1 :: Type -- good data T2 :: Bool -> Type -- good data T3 :: Bool -> forall k. Type -- strange, but still accepted @@ -2361,27 +2360,38 @@ newtype instance T [a] :: <kind> where ... -- See Point 5 data T5 :: Bool -- bad data T6 :: Type -> Bool -- bad + Exactly the same applies to data instance (but not data family) + declarations. Examples + data instance D1 :: Type -- good + data instance D2 :: Boool -> Type -- good + + We can "look through" type synonyms + type Star = Type + data T7 :: Bool -> Star -- good (synonym expansion ok) type Arrow = (->) - data T7 :: Arrow Bool Type -- good + data T8 :: Arrow Bool Type -- good (ditto) + But we specifically do *not* do type family reduction here. type family ARROW where ARROW = (->) - data T8 :: ARROW Bool Type -- bad - - type Star = Type - data T9 :: Bool -> Star -- good + data T9 :: ARROW Bool Type -- bad type family F a where F Int = Bool F Bool = Type data T10 :: Bool -> F Bool -- bad + The /principle/ here is that in the TyCon for a data type or data instance, + we must be able to lay out all the type-variable binders, one by one, until + we reach (TYPE xx). There is no place for a cast here. We could add one, + but let's not! + This check is done in checkDataKindSig. For data declarations, this call is in tcDataDefn; for data instances, this call is in tcDataFamInstDecl. - However, because data instances in GADT syntax can have two return kinds (see - point (2) above), we must check both return kinds. The user-written return - kind is checked in tc_kind_sig within tcDataFamInstHeader. Examples: +4a Because data instances in GADT syntax can have two return kinds (see + point (2) above), we must check both return kinds. The user-written return + kind is checked by the call to checkDataKindSig in tcDataFamInstDecl. Examples: data family D (a :: Nat) :: k -- good (see Point 6) @@ -2906,36 +2916,11 @@ tcTyFamInstEqnGuts fam_tc mb_clsinfo imp_vars exp_bndrs hs_pats hs_rhs_ty ; return (qtvs, pats, rhs_ty) } ----------------- -tcFamTyPats :: TyCon - -> HsTyPats GhcRn -- Patterns - -> TcM (TcType, TcKind) -- (lhs_type, lhs_kind) --- Used for both type and data families -tcFamTyPats fam_tc hs_pats - = do { traceTc "tcFamTyPats {" $ - vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ] - - ; let fun_ty = mkTyConApp fam_tc [] - - ; (fam_app, res_kind) <- unsetWOptM Opt_WarnPartialTypeSignatures $ - setXOptM LangExt.PartialTypeSignatures $ - -- See Note [Wildcards in family instances] in - -- GHC.Rename.Module - tcInferApps typeLevelMode lhs_fun fun_ty hs_pats - - ; traceTc "End tcFamTyPats }" $ - vcat [ ppr fam_tc, text "res_kind:" <+> ppr res_kind ] - - ; return (fam_app, res_kind) } - where - fam_name = tyConName fam_tc - fam_arity = tyConArity fam_tc - lhs_fun = noLoc (HsTyVar noExtField NotPromoted (noLoc fam_name)) - unravelFamInstPats :: TcType -> [TcType] -- Decompose fam_app to get the argument patterns -- -- We expect fam_app to look like (F t1 .. tn) --- tcInferApps is capable of returning ((F ty1 |> co) ty2), +-- tcFamTyPats is capable of returning ((F ty1 |> co) ty2), -- but that can't happen here because we already checked the -- arity of F matches the number of pattern unravelFamInstPats fam_app @@ -4749,20 +4734,20 @@ badDataConTyCon data_con res_ty_tmpl $+$ hang (text "Suggestion: instead use this type signature:") 2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty) - -- To construct a type that GHC would accept (suggested_ty), we: - -- - -- 1) Find the existentially quantified type variables and the class - -- predicates from the datacon. (NB: We don't need the universally - -- quantified type variables, since rejigConRes won't substitute them in - -- the result type if it fails, as in this scenario.) - -- 2) Split apart the return type (which is headed by a forall or a - -- context) using tcSplitNestedSigmaTys, collecting the type variables - -- and class predicates we find, as well as the rho type lurking - -- underneath the nested foralls and contexts. - -- 3) Smash together the type variables and class predicates from 1) and - -- 2), and prepend them to the rho type from 2). - (tvs, theta, rho) = tcSplitNestedSigmaTys (dataConUserType data_con) + -- To construct a type that GHC would accept (suggested_ty), we + -- simply drag all the foralls and (=>) contexts to the front + -- of the type. suggested_ty = mkSpecSigmaTy tvs theta rho + (tvs, theta, rho) = go (dataConUserType data_con) + + go :: Type -> ([TyVar],ThetaType,Type) + -- The returned Type has no foralls or =>, even to the right of an (->) + go ty | null arg_tys = (tvs1, theta1, rho1) + | otherwise = (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2) + where + (tvs1, theta1, rho1) = tcSplitNestedSigmaTys ty + (arg_tys, ty2) = tcSplitFunTys rho1 + (tvs2, theta2, rho2) = go ty2 badGadtDecl :: Name -> SDoc badGadtDecl tc_name diff --git a/compiler/GHC/Tc/TyCl/Instance.hs b/compiler/GHC/Tc/TyCl/Instance.hs index 734ec05512..4c43d91f3e 100644 --- a/compiler/GHC/Tc/TyCl/Instance.hs +++ b/compiler/GHC/Tc/TyCl/Instance.hs @@ -699,8 +699,10 @@ tcDataFamInstDecl mb_clsinfo tv_skol_env -- we did it before the "extra" tvs from etaExpandAlgTyCon -- would always be eta-reduced -- - -- See also Note [Datatype return kinds] in GHC.Tc.TyCl ; (extra_tcbs, final_res_kind) <- etaExpandAlgTyCon full_tcbs res_kind + + -- Check the result kind; it may come from a user-written signature. + -- See Note [Datatype return kinds] in GHC.Tc.TyCl point 4(a) ; checkDataKindSig (DataInstanceSort new_or_data) final_res_kind ; let extra_pats = map (mkTyVarTy . binderVar) extra_tcbs all_pats = pats `chkAppend` extra_pats @@ -847,7 +849,8 @@ tcDataFamInstHeader -- Here the "header" is the bit before the "where" tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity hs_ctxt hs_pats m_ksig hs_cons new_or_data - = do { (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, lhs_applied_kind))) + = do { traceTc "tcDataFamInstHeader {" (ppr fam_tc <+> ppr hs_pats) + ; (imp_tvs, (exp_tvs, (stupid_theta, lhs_ty, res_kind))) <- pushTcLevelM_ $ solveEqualities $ bindImplicitTKBndrs_Q_Skol imp_vars $ @@ -872,10 +875,15 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; let lhs_applied_ty = lhs_ty `mkTcAppTys` lhs_extra_args hs_lhs = nlHsTyConApp fixity (getName fam_tc) hs_pats ; _ <- unifyKind (Just (unLoc hs_lhs)) lhs_applied_kind res_kind + -- Check that the result kind of the TyCon applied to its args + -- is compatible with the explicit signature (or Type, if there + -- is none) + ; traceTc "tcDataFamInstHeader" $ + vcat [ ppr fam_tc, ppr m_ksig, ppr lhs_applied_kind, ppr res_kind ] ; return ( stupid_theta , lhs_applied_ty - , lhs_applied_kind ) } + , res_kind ) } -- See GHC.Tc.TyCl Note [Generalising in tcFamTyPatsGuts] -- This code (and the stuff immediately above) is very similar @@ -888,10 +896,15 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; qtvs <- quantifyTyVars dvs -- Zonk the patterns etc into the Type world - ; (ze, qtvs) <- zonkTyBndrs qtvs - ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty - ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta - ; lhs_applied_kind <- zonkTcTypeToTypeX ze lhs_applied_kind + ; (ze, qtvs) <- zonkTyBndrs qtvs + ; lhs_ty <- zonkTcTypeToTypeX ze lhs_ty + ; stupid_theta <- zonkTcTypesToTypesX ze stupid_theta + ; res_kind <- zonkTcTypeToTypeX ze res_kind + + -- We check that res_kind is OK with checkDataKindSig in + -- tcDataFamInstDecl, after eta-expansion. We need to check that + -- it's ok because res_kind can come from a user-written kind signature. + -- See Note [Datatype return kinds], point (4a) -- Check that type patterns match the class instance head -- The call to splitTyConApp_maybe here is just an inlining of @@ -899,7 +912,8 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; pats <- case splitTyConApp_maybe lhs_ty of Just (_, pats) -> pure pats Nothing -> pprPanic "tcDataFamInstHeader" (ppr lhs_ty) - ; return (qtvs, pats, lhs_applied_kind, stupid_theta) } + + ; return (qtvs, pats, res_kind, stupid_theta) } where fam_name = tyConName fam_tc data_ctxt = DataKindCtxt fam_name @@ -920,11 +934,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity ; lvl <- getTcLevel ; (subst, _tvs') <- tcInstSkolTyVarsAt lvl False emptyTCvSubst tvs -- Perhaps surprisingly, we don't need the skolemised tvs themselves - ; let final_kind = substTy subst inner_kind - ; checkDataKindSig (DataInstanceSort new_or_data) $ - snd $ tcSplitPiTys final_kind - -- See Note [Datatype return kinds], end of point (4) - ; return final_kind } + ; return (substTy subst inner_kind) } {- Note [Result kind signature for a data family instance] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -932,7 +942,7 @@ The expected type might have a forall at the type. Normally, we can't skolemise in kinds because we don't have type-level lambda. But here, we're at the top-level of an instance declaration, so we actually have a place to put the regeneralised variables. -Thus: skolemise away. cf. Inst.deeplySkolemise and GHC.Tc.Utils.Unify.tcSkolemise +Thus: skolemise away. cf. GHC.Tc.Utils.Unify.tcSkolemise Examples in indexed-types/should_compile/T12369 Note [Implementing eta reduction for data families] @@ -1781,7 +1791,7 @@ tcMethodBodyHelp hs_sig_fn sel_id local_meth_id meth_bind -- The instance-sig is the focus here; the class-meth-sig -- is fixed (#18036) ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name sig_ty local_meth_ty) $ - tcSubType_NC ctxt sig_ty local_meth_ty + tcSubTypeSigma ctxt sig_ty local_meth_ty ; return (sig_ty, hs_wrap) } ; inner_meth_name <- newName (nameOccName sel_name) diff --git a/compiler/GHC/Tc/TyCl/PatSyn.hs b/compiler/GHC/Tc/TyCl/PatSyn.hs index 957506c7c5..a785fbbb7a 100644 --- a/compiler/GHC/Tc/TyCl/PatSyn.hs +++ b/compiler/GHC/Tc/TyCl/PatSyn.hs @@ -431,9 +431,9 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details = do { -- Look up the variable actually bound by lpat -- and check that it has the expected type arg_id <- tcLookupId arg_name - ; wrap <- tcSubType_NC GenSigCtxt - (idType arg_id) - (substTyUnchecked subst arg_ty) + ; wrap <- tcSubTypeSigma GenSigCtxt + (idType arg_id) + (substTyUnchecked subst arg_ty) -- Why do we need tcSubType here? -- See Note [Pattern synonyms and higher rank types] ; return (mkLHsWrap wrap $ nlHsVar arg_id) } diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs index 908a23ff26..3f01a7d03a 100644 --- a/compiler/GHC/Tc/Types/Constraint.hs +++ b/compiler/GHC/Tc/Types/Constraint.hs @@ -29,7 +29,7 @@ module GHC.Tc.Types.Constraint ( WantedConstraints(..), insolubleWC, emptyWC, isEmptyWC, isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC, - addInsols, insolublesOnly, addSimples, addImplics, addHole, + addInsols, dropMisleading, addSimples, addImplics, addHoles, tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, tyCoVarsOfWCList, insolubleCt, insolubleEqCt, isDroppableCt, insolubleImplic, @@ -961,19 +961,24 @@ addInsols :: WantedConstraints -> Bag Ct -> WantedConstraints addInsols wc cts = wc { wc_simple = wc_simple wc `unionBags` cts } -addHole :: WantedConstraints -> Hole -> WantedConstraints -addHole wc hole - = wc { wc_holes = hole `consBag` wc_holes wc } +addHoles :: WantedConstraints -> Bag Hole -> WantedConstraints +addHoles wc holes + = wc { wc_holes = holes `unionBags` wc_holes wc } -insolublesOnly :: WantedConstraints -> WantedConstraints --- Keep only the definitely-insoluble constraints -insolublesOnly (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) - = WC { wc_simple = filterBag insolubleCt simples - , wc_impl = mapBag implic_insols_only implics +dropMisleading :: WantedConstraints -> WantedConstraints +-- Drop misleading constraints; really just class constraints +-- See Note [Constraints and errors] in GHC.Tc.Utils.Monad +dropMisleading (WC { wc_simple = simples, wc_impl = implics, wc_holes = holes }) + = WC { wc_simple = filterBag keep_ct simples + , wc_impl = mapBag drop_implic implics , wc_holes = filterBag isOutOfScopeHole holes } where - implic_insols_only implic - = implic { ic_wanted = insolublesOnly (ic_wanted implic) } + drop_implic implic + = implic { ic_wanted = dropMisleading (ic_wanted implic) } + keep_ct ct + = case classifyPredType (ctPred ct) of + ClassPred {} -> False + _ -> True isSolvedStatus :: ImplicStatus -> Bool isSolvedStatus (IC_Solved {}) = True @@ -1100,9 +1105,6 @@ data Implication ic_info :: SkolemInfo, -- See Note [Skolems in an implication] -- See Note [Shadowing in a constraint] - ic_telescope :: Maybe SDoc, -- User-written telescope, if there is one - -- See Note [Checking telescopes] - ic_given :: [EvVar], -- Given evidence variables -- (order does not matter) -- See Invariant (GivenInv) in GHC.Tc.Utils.TcType @@ -1153,7 +1155,6 @@ implicationPrototype -- The rest have sensible default values , ic_skols = [] - , ic_telescope = Nothing , ic_given = [] , ic_wanted = emptyWC , ic_no_eqs = False @@ -1228,17 +1229,18 @@ all at once, creating one implication constraint for the lot: variables (ic_skols). This is done in setImplicationStatus. * This check is only necessary if the implication was born from a - user-written signature. If, say, it comes from checking a pattern - match that binds existentials, where the type of the data constructor - is known to be valid (it in tcConPat), no need for the check. + 'forall' in a user-written signature (the HsForAllTy case in + GHC.Tc.Gen.HsType. If, say, it comes from checking a pattern match + that binds existentials, where the type of the data constructor is + known to be valid (it in tcConPat), no need for the check. - So the check is done if and only if ic_telescope is (Just blah). + So the check is done if and only if ic_info is ForAllSkol -* If ic_telesope is (Just d), the d::SDoc displays the original, - user-written type variables. +* If ic_info is (ForAllSkol dt dvs), the dvs::SDoc displays the + original, user-written type variables. -* Be careful /NOT/ to discard an implication with non-Nothing - ic_telescope, even if ic_wanted is empty. We must give the +* Be careful /NOT/ to discard an implication with a ForAllSkol + ic_info, even if ic_wanted is empty. We must give the constraint solver a chance to make that bad-telescope test! Hence the extra guard in emitResidualTvConstraint; see #16247 diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs index 381cdd03ba..b453633c65 100644 --- a/compiler/GHC/Tc/Types/Origin.hs +++ b/compiler/GHC/Tc/Types/Origin.hs @@ -125,7 +125,7 @@ data UserTypeCtxt pprUserTypeCtxt :: UserTypeCtxt -> SDoc pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n) pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n) -pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n) +pprUserTypeCtxt (RuleSigCtxt n) = text "the type signature for" <+> quotes (ppr n) pprUserTypeCtxt ExprSigCtxt = text "an expression type signature" pprUserTypeCtxt KindSigCtxt = text "a kind signature" pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature for" <+> quotes (ppr n) @@ -184,7 +184,10 @@ data SkolemInfo -- like SigSkol, but when we're kind-checking the *type* -- hence, we have less info - | ForAllSkol SDoc -- Bound by a user-written "forall". + | ForAllSkol -- Bound by a user-written "forall". + SDoc -- Shows the entire forall type + SDoc -- Shows just the binders, used when reporting a bad telescope + -- See Note [Checking telescopes] in GHC.Tc.Types.Constraint | DerivSkol Type -- Bound by a 'deriving' clause; -- the type is the instance we are trying to derive @@ -242,7 +245,7 @@ pprSkolInfo :: SkolemInfo -> SDoc -- Complete the sentence "is a rigid type variable bound by..." pprSkolInfo (SigSkol cx ty _) = pprSigSkolInfo cx ty pprSkolInfo (SigTypeSkol cx) = pprUserTypeCtxt cx -pprSkolInfo (ForAllSkol doc) = quotes doc +pprSkolInfo (ForAllSkol pt _) = quotes pt pprSkolInfo (IPSkol ips) = text "the implicit-parameter binding" <> plural ips <+> text "for" <+> pprWithCommas ppr ips pprSkolInfo (DerivSkol pred) = text "the deriving clause for" <+> quotes (ppr pred) @@ -306,8 +309,8 @@ is fine. We could do more, but it doesn't seem worth it. Note [SigSkol SkolemInfo] ~~~~~~~~~~~~~~~~~~~~~~~~~ -Suppose we (deeply) skolemise a type - f :: forall a. a -> forall b. b -> a +Suppose we skolemise a type + f :: forall a. Eq a => forall b. b -> a Then we'll instantiate [a :-> a', b :-> b'], and with the instantiated a' -> b' -> a. But when, in an error message, we report that "b is a rigid type @@ -321,8 +324,8 @@ in the right place. So we proceed as follows: * Then when tidying in GHC.Tc.Utils.TcMType.tidySkolemInfo, we first tidy a' to whatever it tidies to, say a''; and then we walk over the type replacing the binder a by the tidied version a'', to give - forall a''. a'' -> forall b''. b'' -> a'' - We need to do this under function arrows, to match what deeplySkolemise + forall a''. Eq a'' => forall b''. b'' -> a'' + We need to do this under (=>) arrows, to match what topSkolemise does. * Typically a'' will have a nice pretty name like "a", but the point is diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs index 8c2a60ba50..2563ff7348 100644 --- a/compiler/GHC/Tc/Utils/Env.hs +++ b/compiler/GHC/Tc/Utils/Env.hs @@ -593,24 +593,29 @@ tc_extend_local_env top_lvl extra_env thing_inside -- that are bound together with extra_env and should not be regarded -- as free in the types of extra_env. = do { traceTc "tc_extend_local_env" (ppr extra_env) - ; env0 <- getLclEnv - ; let env1 = tcExtendLocalTypeEnv env0 extra_env ; stage <- getStage - ; let env2 = extend_local_env (top_lvl, thLevel stage) extra_env env1 - ; setLclEnv env2 thing_inside } - where - extend_local_env :: (TopLevelFlag, ThLevel) -> [(Name, TcTyThing)] -> TcLclEnv -> TcLclEnv - -- Extend the local LocalRdrEnv and Template Haskell staging env simultaneously - -- Reason for extending LocalRdrEnv: after running a TH splice we need - -- to do renaming. - extend_local_env thlvl pairs env@(TcLclEnv { tcl_rdr = rdr_env - , tcl_th_bndrs = th_bndrs }) - = env { tcl_rdr = extendLocalRdrEnvList rdr_env - [ n | (n, _) <- pairs, isInternalName n ] - -- The LocalRdrEnv contains only non-top-level names - -- (GlobalRdrEnv handles the top level) - , tcl_th_bndrs = extendNameEnvList th_bndrs -- We only track Ids in tcl_th_bndrs - [(n, thlvl) | (n, ATcId {}) <- pairs] } + ; env0@(TcLclEnv { tcl_rdr = rdr_env + , tcl_th_bndrs = th_bndrs + , tcl_env = lcl_type_env }) <- getLclEnv + + ; let thlvl = (top_lvl, thLevel stage) + + env1 = env0 { tcl_rdr = extendLocalRdrEnvList rdr_env + [ n | (n, _) <- extra_env, isInternalName n ] + -- The LocalRdrEnv contains only non-top-level names + -- (GlobalRdrEnv handles the top level) + + , tcl_th_bndrs = extendNameEnvList th_bndrs + [(n, thlvl) | (n, ATcId {}) <- extra_env] + -- We only track Ids in tcl_th_bndrs + + , tcl_env = extendNameEnvList lcl_type_env extra_env } + + -- tcl_rdr and tcl_th_bndrs: extend the local LocalRdrEnv and + -- Template Haskell staging env simultaneously. Reason for extending + -- LocalRdrEnv: after running a TH splice we need to do renaming. + + ; setLclEnv env1 thing_inside } tcExtendLocalTypeEnv :: TcLclEnv -> [(Name, TcTyThing)] -> TcLclEnv tcExtendLocalTypeEnv lcl_env@(TcLclEnv { tcl_env = lcl_type_env }) tc_ty_things diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index ea8ffd912b..df9cf982ee 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -10,10 +10,9 @@ {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-} {-# OPTIONS_GHC -Wno-incomplete-record-updates #-} --- | The @Inst@ type: dictionaries or method instances module GHC.Tc.Utils.Instantiate ( - deeplySkolemise, - topInstantiate, topInstantiateInferred, deeplyInstantiate, + topSkolemise, + topInstantiate, topInstantiateInferred, instCall, instDFunType, instStupidTheta, instTyVarsWith, newWanted, newWanteds, @@ -36,11 +35,10 @@ module GHC.Tc.Utils.Instantiate ( import GHC.Prelude -import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckExpr, tcSyntaxOp ) +import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp ) import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType, unifyKind ) import GHC.Types.Basic ( IntegralLit(..), SourceText(..) ) -import GHC.Data.FastString import GHC.Hs import GHC.Tc.Utils.Zonk import GHC.Tc.Utils.Monad @@ -117,66 +115,62 @@ newMethodFromName origin name ty_args {- ************************************************************************ * * - Deep instantiation and skolemisation + Instantiation and skolemisation * * ************************************************************************ -Note [Deep skolemisation] -~~~~~~~~~~~~~~~~~~~~~~~~~ -deeplySkolemise decomposes and skolemises a type, returning a type -with all its arrows visible (ie not buried under foralls) +Note [Skolemisation] +~~~~~~~~~~~~~~~~~~~~ +topSkolemise decomposes and skolemises a type, returning a type +with no top level foralls or (=>) Examples: - deeplySkolemise (Int -> forall a. Ord a => blah) - = ( wp, [a], [d:Ord a], Int -> blah ) - where wp = \x:Int. /\a. \(d:Ord a). <hole> x + topSkolemise (forall a. Ord a => a -> a) + = ( wp, [a], [d:Ord a], a->a ) + where wp = /\a. \(d:Ord a). <hole> a d - deeplySkolemise (forall a. Ord a => Maybe a -> forall b. Eq b => blah) - = ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah ) - where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x + topSkolemise (forall a. Ord a => forall b. Eq b => a->b->b) + = ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b ) + where wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2 + +This second example is the reason for the recursive 'go' +function in topSkolemise: we must remove successive layers +of foralls and (=>). In general, - if deeplySkolemise ty = (wrap, tvs, evs, rho) + if topSkolemise ty = (wrap, tvs, evs, rho) and e :: rho then wrap e :: ty - and 'wrap' binds tvs, evs + and 'wrap' binds {tvs, evs} -ToDo: this eta-abstraction plays fast and loose with termination, - because it can introduce extra lambdas. Maybe add a `seq` to - fix this -} -deeplySkolemise :: TcSigmaType - -> TcM ( HsWrapper - , [(Name,TyVar)] -- All skolemised variables - , [EvVar] -- All "given"s - , TcRhoType ) - -deeplySkolemise ty - = go init_subst ty +topSkolemise :: TcSigmaType + -> TcM ( HsWrapper + , [(Name,TyVar)] -- All skolemised variables + , [EvVar] -- All "given"s + , TcRhoType ) +-- See Note [Skolemisation] +topSkolemise ty + = go init_subst idHsWrapper [] [] ty where init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty)) - go subst ty - | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty - = do { let arg_tys' = substTys subst arg_tys - ; ids1 <- newSysLocalIds (fsLit "dk") arg_tys' - ; (subst', tvs1) <- tcInstSkolTyVarsX subst tvs + -- Why recursive? See Note [Skolemisation] + go subst wrap tv_prs ev_vars ty + | (tvs, theta, inner_ty) <- tcSplitSigmaTy ty + , not (null tvs && null theta) + = do { (subst', tvs1) <- tcInstSkolTyVarsX subst tvs ; ev_vars1 <- newEvVars (substTheta subst' theta) - ; (wrap, tvs_prs2, ev_vars2, rho) <- go subst' ty' - ; let tv_prs1 = map tyVarName tvs `zip` tvs1 - ; return ( mkWpLams ids1 - <.> mkWpTyLams tvs1 - <.> mkWpLams ev_vars1 - <.> wrap - <.> mkWpEvVarApps ids1 - , tv_prs1 ++ tvs_prs2 - , ev_vars1 ++ ev_vars2 - , mkVisFunTys arg_tys' rho ) } + ; go subst' + (wrap <.> mkWpTyLams tvs1 <.> mkWpLams ev_vars1) + (tv_prs ++ (map tyVarName tvs `zip` tvs1)) + (ev_vars ++ ev_vars1) + inner_ty } | otherwise - = return (idHsWrapper, [], [], substTy subst ty) + = return (wrap, tv_prs, ev_vars, substTy subst ty) -- substTy is a quick no-op on an empty substitution -- | Instantiate all outer type variables @@ -185,6 +179,7 @@ topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- if topInstantiate ty = (wrap, rho) -- and e :: ty -- then wrap e :: rho (that is, wrap :: ty "->" rho) +-- NB: always returns a rho-type, with no top-level forall or (=>) topInstantiate = top_instantiate True -- | Instantiate all outer 'Inferred' binders @@ -195,13 +190,16 @@ topInstantiateInferred :: CtOrigin -> TcSigmaType -- if topInstantiate ty = (wrap, rho) -- and e :: ty -- then wrap e :: rho +-- NB: may return a sigma-type topInstantiateInferred = top_instantiate False top_instantiate :: Bool -- True <=> instantiate *all* variables -- False <=> instantiate only the inferred ones -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) top_instantiate inst_all orig ty - | not (null binders && null theta) + | (binders, phi) <- tcSplitForAllVarBndrs ty + , (theta, rho) <- tcSplitPhiTy phi + , not (null binders && null theta) = do { let (inst_bndrs, leave_bndrs) = span should_inst binders (inst_theta, leave_theta) | null leave_bndrs = (theta, []) @@ -226,7 +224,7 @@ top_instantiate inst_all orig ty , text "theta:" <+> ppr inst_theta' ]) ; (wrap2, rho2) <- - if null leave_bndrs + if null leave_bndrs -- NB: if inst_all is True then leave_bndrs = [] -- account for types like forall a. Num a => forall b. Ord b => ... then top_instantiate inst_all orig sigma' @@ -238,67 +236,11 @@ top_instantiate inst_all orig ty | otherwise = return (idHsWrapper, ty) where - (binders, phi) = tcSplitForAllVarBndrs ty - (theta, rho) = tcSplitPhiTy phi should_inst bndr | inst_all = True | otherwise = binderArgFlag bndr == Inferred -deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) --- Int -> forall a. a -> a ==> (\x:Int. [] x alpha) :: Int -> alpha --- In general if --- if deeplyInstantiate ty = (wrap, rho) --- and e :: ty --- then wrap e :: rho --- That is, wrap :: ty ~> rho --- --- If you don't need the HsWrapper returned from this function, consider --- using tcSplitNestedSigmaTys in GHC.Tc.Utils.TcType, which is a pure alternative that --- only computes the returned TcRhoType. - -deeplyInstantiate orig ty = - deeply_instantiate orig - (mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))) - ty - -deeply_instantiate :: CtOrigin - -> TCvSubst - -> TcSigmaType -> TcM (HsWrapper, TcRhoType) --- Internal function to deeply instantiate that builds on an existing subst. --- It extends the input substitution and applies the final substitution to --- the types on return. See #12549. - -deeply_instantiate orig subst ty - | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty - = do { (subst', tvs') <- newMetaTyVarsX subst tvs - ; let arg_tys' = substTys subst' arg_tys - theta' = substTheta subst' theta - ; ids1 <- newSysLocalIds (fsLit "di") arg_tys' - ; wrap1 <- instCall orig (mkTyVarTys tvs') theta' - ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig - , text "type" <+> ppr ty - , text "with" <+> ppr tvs' - , text "args:" <+> ppr ids1 - , text "theta:" <+> ppr theta' - , text "subst:" <+> ppr subst']) - ; (wrap2, rho2) <- deeply_instantiate orig subst' rho - ; return (mkWpLams ids1 - <.> wrap2 - <.> wrap1 - <.> mkWpEvVarApps ids1, - mkVisFunTys arg_tys' rho2) } - - | otherwise - = do { let ty' = substTy subst ty - ; traceTc "deeply_instantiate final subst" - (vcat [ text "origin:" <+> pprCtOrigin orig - , text "type:" <+> ppr ty - , text "new type:" <+> ppr ty' - , text "subst:" <+> ppr subst ]) - ; return (idHsWrapper, ty') } - - instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst -- Use this when you want to instantiate (forall a b c. ty) with -- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might @@ -639,7 +581,7 @@ tcSyntaxName orig ty (std_nm, user_nm_expr) = do -- same type as the standard one. -- Tiresome jiggling because tcCheckSigma takes a located expression span <- getSrcSpanM - expr <- tcCheckExpr (L span user_nm_expr) sigma1 + expr <- tcCheckPolyExpr (L span user_nm_expr) sigma1 return (std_nm, unLoc expr) syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index 4f14d7b251..5bc6fe3034 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -98,7 +98,8 @@ module GHC.Tc.Utils.Monad( chooseUniqueOccTc, getConstraintVar, setConstraintVar, emitConstraints, emitStaticConstraints, emitSimple, emitSimples, - emitImplication, emitImplications, emitInsoluble, emitHole, + emitImplication, emitImplications, emitInsoluble, + emitHole, emitHoles, discardConstraints, captureConstraints, tryCaptureConstraints, pushLevelAndCaptureConstraints, pushTcLevelM_, pushTcLevelM, pushTcLevelsM, @@ -1111,7 +1112,7 @@ askNoErrs thing_inside ; addMessages msgs ; case mb_res of - Nothing -> do { emitConstraints (insolublesOnly lie) + Nothing -> do { emitConstraints (dropMisleading lie) ; failM } Just res -> do { emitConstraints lie @@ -1133,7 +1134,7 @@ tryCaptureConstraints thing_inside -- See Note [Constraints and errors] ; let lie_to_keep = case mb_res of - Nothing -> insolublesOnly lie + Nothing -> dropMisleading lie Just {} -> lie ; return (mb_res, lie_to_keep) } @@ -1555,7 +1556,13 @@ emitHole :: Hole -> TcM () emitHole hole = do { traceTc "emitHole" (ppr hole) ; lie_var <- getConstraintVar - ; updTcRef lie_var (`addHole` hole) } + ; updTcRef lie_var (`addHoles` unitBag hole) } + +emitHoles :: Bag Hole -> TcM () +emitHoles holes + = do { traceTc "emitHoles" (ppr holes) + ; lie_var <- getConstraintVar + ; updTcRef lie_var (`addHoles` holes) } -- | Throw out any constraints emitted by the thing_inside discardConstraints :: TcM a -> TcM a diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs index 90598e42c4..d02af1351a 100644 --- a/compiler/GHC/Tc/Utils/TcMType.hs +++ b/compiler/GHC/Tc/Utils/TcMType.hs @@ -27,7 +27,8 @@ module GHC.Tc.Utils.TcMType ( newFmvTyVar, newFskTyVar, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, - newMetaDetails, isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, + newTauTvDetailsAtLevel, newMetaDetails, newMetaTyVarName, + isFilledMetaTyVar_maybe, isFilledMetaTyVar, isUnfilledMetaTyVar, -------------------------------- -- Expected types @@ -70,7 +71,7 @@ module GHC.Tc.Utils.TcMType ( zonkTidyTcType, zonkTidyTcTypes, zonkTidyOrigin, tidyEvVar, tidyCt, tidyHole, tidySkolemInfo, zonkTcTyVar, zonkTcTyVars, - zonkTcTyVarToTyVar, zonkTyVarTyVarPairs, + zonkTcTyVarToTyVar, zonkInvisTVBinder, zonkTyCoVarsAndFV, zonkTcTypeAndFV, zonkDTyCoVarSetAndFV, zonkTyCoVarsAndFVList, candidateQTyVarsOfType, candidateQTyVarsOfKind, @@ -81,7 +82,7 @@ module GHC.Tc.Utils.TcMType ( zonkTcType, zonkTcTypes, zonkCo, zonkTyCoVarKind, zonkTyCoVarKindBinder, - zonkEvVar, zonkWC, zonkSimples, + zonkEvVar, zonkWC, zonkImplication, zonkSimples, zonkId, zonkCoVar, zonkCt, zonkSkolemInfo, @@ -119,7 +120,6 @@ import GHC.Builtin.Types import GHC.Builtin.Types.Prim import GHC.Types.Var.Env import GHC.Types.Name.Env -import GHC.Builtin.Names import GHC.Utils.Misc import GHC.Utils.Outputable import GHC.Data.FastString @@ -144,18 +144,13 @@ import qualified Data.Semigroup as Semi ************************************************************************ -} -mkKindName :: Unique -> Name -mkKindName unique = mkSystemName unique kind_var_occ - -kind_var_occ :: OccName -- Just one for all MetaKindVars - -- They may be jiggled by tidying -kind_var_occ = mkOccName tvName "k" - newMetaKindVar :: TcM TcKind newMetaKindVar = do { details <- newMetaDetails TauTv - ; uniq <- newUnique - ; let kv = mkTcTyVar (mkKindName uniq) liftedTypeKind details + ; name <- newMetaTyVarName (fsLit "k") + -- All MetaKindVars are called "k" + -- They may be jiggled by tidying + ; let kv = mkTcTyVar name liftedTypeKind details ; traceTc "newMetaKindVar" (ppr kv) ; return (mkTyVarTy kv) } @@ -834,6 +829,13 @@ newMetaDetails info , mtv_ref = ref , mtv_tclvl = tclvl }) } +newTauTvDetailsAtLevel :: TcLevel -> TcM TcTyVarDetails +newTauTvDetailsAtLevel tclvl + = do { ref <- newMutVar Flexi + ; return (MetaTv { mtv_info = TauTv + , mtv_ref = ref + , mtv_tclvl = tclvl }) } + cloneMetaTyVar :: TcTyVar -> TcM TcTyVar cloneMetaTyVar tv = ASSERT( isTcTyVar tv ) @@ -1060,18 +1062,15 @@ new_meta_tv_x info subst tv -- is not yet fixed so leaving as unchecked for now. -- OLD NOTE: -- Unchecked because we call newMetaTyVarX from - -- tcInstTyBinder, which is called from tcInferApps + -- tcInstTyBinder, which is called from tcInferTyApps -- which does not yet take enough trouble to ensure -- the in-scope set is right; e.g. #12785 trips -- if we use substTy here newMetaTyVarTyAtLevel :: TcLevel -> TcKind -> TcM TcType newMetaTyVarTyAtLevel tc_lvl kind - = do { ref <- newMutVar Flexi - ; name <- newMetaTyVarName (fsLit "p") - ; let details = MetaTv { mtv_info = TauTv - , mtv_ref = ref - , mtv_tclvl = tc_lvl } + = do { details <- newTauTvDetailsAtLevel tc_lvl + ; name <- newMetaTyVarName (fsLit "p") ; return (mkTyVarTy (mkTcTyVar name kind details)) } {- ********************************************************************* @@ -1254,13 +1253,14 @@ instance Outputable CandidatesQTvs where candidateKindVars :: CandidatesQTvs -> TyVarSet candidateKindVars dvs = dVarSetToVarSet (dv_kvs dvs) -partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (DTyVarSet, CandidatesQTvs) +partitionCandidates :: CandidatesQTvs -> (TyVar -> Bool) -> (TyVarSet, CandidatesQTvs) +-- The selected TyVars are returned as a non-deterministic TyVarSet partitionCandidates dvs@(DV { dv_kvs = kvs, dv_tvs = tvs }) pred = (extracted, dvs { dv_kvs = rest_kvs, dv_tvs = rest_tvs }) where (extracted_kvs, rest_kvs) = partitionDVarSet pred kvs (extracted_tvs, rest_tvs) = partitionDVarSet pred tvs - extracted = extracted_kvs `unionDVarSet` extracted_tvs + extracted = dVarSetToVarSet extracted_kvs `unionVarSet` dVarSetToVarSet extracted_tvs -- | Gathers free variables to use as quantification candidates (in -- 'quantifyTyVars'). This might output the same var @@ -2218,12 +2218,9 @@ zonkTcTyVarToTyVar tv (ppr tv $$ ppr ty) ; return tv' } -zonkTyVarTyVarPairs :: [(Name,VarBndr TcTyVar Specificity)] -> TcM [(Name,VarBndr TcTyVar Specificity)] -zonkTyVarTyVarPairs prs - = mapM do_one prs - where - do_one (nm, Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv - ; return (nm, Bndr tv' spec) } +zonkInvisTVBinder :: VarBndr TcTyVar spec -> TcM (VarBndr TyVar spec) +zonkInvisTVBinder (Bndr tv spec) = do { tv' <- zonkTcTyVarToTyVar tv + ; return (Bndr tv' spec) } -- zonkId is used *during* typechecking just to zonk the Id's type zonkId :: TcId -> TcM TcId @@ -2342,7 +2339,7 @@ tidySigSkol env cx ty tv_prs where (env', tv') = tidy_tv_bndr env tv - tidy_ty env ty@(FunTy _ arg res) + tidy_ty env ty@(FunTy InvisArg arg res) -- Look under c => t = ty { ft_arg = tidyType env arg, ft_res = tidy_ty env res } tidy_ty env ty = tidyType env ty diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs index fb1d6f432b..c1d7af0120 100644 --- a/compiler/GHC/Tc/Utils/TcType.hs +++ b/compiler/GHC/Tc/Utils/TcType.hs @@ -67,7 +67,7 @@ module GHC.Tc.Utils.TcType ( tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe, tcRepGetNumAppTys, tcGetCastedTyVar_maybe, tcGetTyVar_maybe, tcGetTyVar, - tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe, + tcSplitSigmaTy, tcSplitNestedSigmaTys, --------------------------------- -- Predicates. @@ -412,7 +412,7 @@ mkCheckExpType = Check -- This is defined here to avoid defining it in GHC.Tc.Gen.Expr boot file. data SyntaxOpType = SynAny -- ^ Any type - | SynRho -- ^ A rho type, deeply skolemised or instantiated as appropriate + | SynRho -- ^ A rho type, skolemised or instantiated as appropriate | SynList -- ^ A list type. You get back the element type of the list | SynFun SyntaxOpType SyntaxOpType -- ^ A function. @@ -431,11 +431,12 @@ mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys {- Note [TcRhoType] ~~~~~~~~~~~~~~~~ -A TcRhoType has no foralls or contexts at the top, or to the right of an arrow - YES (forall a. a->a) -> Int +A TcRhoType has no foralls or contexts at the top NO forall a. a -> Int NO Eq a => a -> a - NO Int -> forall a. a -> Int + YES a -> a + YES (forall a. a->a) -> Int + YES Int -> forall a. a -> Int ************************************************************************ @@ -1273,35 +1274,19 @@ tcSplitSigmaTy ty = case tcSplitForAllTys ty of -- if you instead called @tcSplitNestedSigmaTys@ on the type, it would return -- @([s,t,a,b,f], [Each s t a b, Applicative f], (a -> f b) -> s -> f t)@. tcSplitNestedSigmaTys :: Type -> ([TyVar], ThetaType, Type) --- NB: This is basically a pure version of deeplyInstantiate (from Inst) that +-- NB: This is basically a pure version of topInstantiate (from Inst) that -- doesn't compute an HsWrapper. tcSplitNestedSigmaTys ty -- If there's a forall, split it apart and try splitting the rho type -- underneath it. - | Just (arg_tys, tvs1, theta1, rho1) <- tcDeepSplitSigmaTy_maybe ty + | (tvs1, theta1, rho1) <- tcSplitSigmaTy ty + , not (null tvs1 && null theta1) = let (tvs2, theta2, rho2) = tcSplitNestedSigmaTys rho1 - in (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2) + in (tvs1 ++ tvs2, theta1 ++ theta2, rho2) -- If there's no forall, we're done. | otherwise = ([], [], ty) ----------------------- -tcDeepSplitSigmaTy_maybe - :: TcSigmaType -> Maybe ([TcType], [TyVar], ThetaType, TcSigmaType) --- Looks for a *non-trivial* quantified type, under zero or more function arrows --- By "non-trivial" we mean either tyvars or constraints are non-empty - -tcDeepSplitSigmaTy_maybe ty - | Just (arg_ty, res_ty) <- tcSplitFunTy_maybe ty - , Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe res_ty - = Just (arg_ty:arg_tys, tvs, theta, rho) - - | (tvs, theta, rho) <- tcSplitSigmaTy ty - , not (null tvs && null theta) - = Just ([], tvs, theta, rho) - - | otherwise = Nothing - ------------------------ tcTyConAppTyCon :: Type -> TyCon tcTyConAppTyCon ty = case tcTyConAppTyCon_maybe ty of @@ -1997,9 +1982,9 @@ isSigmaTy _ = False isRhoTy :: TcType -> Bool -- True of TcRhoTypes; see Note [TcRhoType] isRhoTy ty | Just ty' <- tcView ty = isRhoTy ty' -isRhoTy (ForAllTy {}) = False -isRhoTy (FunTy { ft_af = VisArg, ft_res = r }) = isRhoTy r -isRhoTy _ = True +isRhoTy (ForAllTy {}) = False +isRhoTy (FunTy { ft_af = InvisArg }) = False +isRhoTy _ = True -- | Like 'isRhoTy', but also says 'True' for 'Infer' types isRhoExpTy :: ExpType -> Bool diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index 7c14e56319..8ca3ae7723 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -13,11 +13,11 @@ -- | Type subsumption and unification module GHC.Tc.Utils.Unify ( -- Full-blown subsumption - tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET, - tcSubTypeHR, tcSubTypeO, tcSubType_NC, tcSubTypeDS, - tcSubTypeDS_NC_O, tcSubTypePat, + tcWrapResult, tcWrapResultO, tcWrapResultMono, + tcSkolemise, tcSkolemiseScoped, tcSkolemiseET, + tcSubType, tcSubTypeSigma, tcSubTypePat, checkConstraints, checkTvConstraints, - buildImplicationFor, emitResidualTvConstraint, + buildImplicationFor, buildTvImplication, emitResidualTvConstraint, -- Various unifications unifyType, unifyKind, @@ -31,7 +31,7 @@ module GHC.Tc.Utils.Unify ( matchExpectedTyConApp, matchExpectedAppTy, matchExpectedFunTys, - matchActualFunTys, matchActualFunTysPart, + matchActualFunTysRho, matchActualFunTySigma, matchExpectedFunKind, metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..) @@ -48,6 +48,7 @@ import GHC.Core.TyCo.Ppr( debugPprType ) import GHC.Tc.Utils.TcMType import GHC.Tc.Utils.Monad import GHC.Tc.Utils.TcType +import GHC.Tc.Utils.Env import GHC.Core.Type import GHC.Core.Coercion import GHC.Tc.Types.Evidence @@ -70,7 +71,6 @@ import GHC.Utils.Misc import qualified GHC.LanguageExtensions as LangExt import GHC.Utils.Outputable as Outputable -import Data.Maybe( isNothing ) import Control.Monad import Control.Arrow ( second ) @@ -139,34 +139,46 @@ passed in. -} -- Use this one when you have an "expected" type. +-- This function skolemises at each polytype. matchExpectedFunTys :: forall a. SDoc -- See Note [Herald for matchExpectedFunTys] + -> UserTypeCtxt -> Arity - -> ExpRhoType -- deeply skolemised + -> ExpRhoType -- Skolemised -> ([ExpSigmaType] -> ExpRhoType -> TcM a) - -- must fill in these ExpTypes here - -> TcM (a, HsWrapper) + -> TcM (HsWrapper, a) -- If matchExpectedFunTys n ty = (_, wrap) -- then wrap : (t1 -> ... -> tn -> ty_r) ~> ty, -- where [t1, ..., tn], ty_r are passed to the thing_inside -matchExpectedFunTys herald arity orig_ty thing_inside +matchExpectedFunTys herald ctx arity orig_ty thing_inside = case orig_ty of Check ty -> go [] arity ty _ -> defer [] arity orig_ty where - go acc_arg_tys 0 ty - = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType ty) - ; return (result, idHsWrapper) } + -- Skolemise any foralls /before/ the zero-arg case + -- so that we guarantee to return a rho-type + go acc_arg_tys n ty + | (tvs, theta, _) <- tcSplitSigmaTy ty + , not (null tvs && null theta) + = do { (wrap_gen, (wrap_res, result)) <- tcSkolemise ctx ty $ \ty' -> + go acc_arg_tys n ty' + ; return (wrap_gen <.> wrap_res, result) } + + -- No more args; do this /before/ tcView, so + -- that we do not unnecessarily unwrap synonyms + go acc_arg_tys 0 rho_ty + = do { result <- thing_inside (reverse acc_arg_tys) (mkCheckExpType rho_ty) + ; return (idHsWrapper, result) } go acc_arg_tys n ty | Just ty' <- tcView ty = go acc_arg_tys n ty' go acc_arg_tys n (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = ASSERT( af == VisArg ) - do { (result, wrap_res) <- go (mkCheckExpType arg_ty : acc_arg_tys) + do { (wrap_res, result) <- go (mkCheckExpType arg_ty : acc_arg_tys) (n-1) res_ty - ; return ( result - , mkWpFun idHsWrapper wrap_res arg_ty res_ty doc ) } + ; let fun_wrap = mkWpFun idHsWrapper wrap_res arg_ty res_ty doc + ; return ( fun_wrap, result ) } where doc = text "When inferring the argument type of a function with type" <+> quotes (ppr orig_ty) @@ -197,7 +209,7 @@ matchExpectedFunTys herald arity orig_ty thing_inside defer acc_arg_tys n (mkCheckExpType ty) ------------ - defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (a, HsWrapper) + defer :: [ExpSigmaType] -> Arity -> ExpRhoType -> TcM (HsWrapper, a) defer acc_arg_tys n fun_ty = do { more_arg_tys <- replicateM n newInferExpType ; res_ty <- newInferExpType @@ -205,9 +217,9 @@ matchExpectedFunTys herald arity orig_ty thing_inside ; more_arg_tys <- mapM readExpType more_arg_tys ; res_ty <- readExpType res_ty ; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty - ; wrap <- tcSubTypeDS AppOrigin GenSigCtxt unif_fun_ty fun_ty + ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty -- Not a good origin at all :-( - ; return (result, wrap) } + ; return (wrap, result) } ------------ mk_ctxt :: [ExpSigmaType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) @@ -220,36 +232,54 @@ matchExpectedFunTys herald arity orig_ty thing_inside -- Like 'matchExpectedFunTys', but used when you have an "actual" type, -- for example in function application -matchActualFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] - -> CtOrigin - -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType - -> Arity - -> TcSigmaType - -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) --- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r) --- then wrap : ty ~> (t1 -> ... -> tn -> ty_r) -matchActualFunTys herald ct_orig mb_thing n_val_args_wanted fun_ty - = matchActualFunTysPart herald ct_orig mb_thing - n_val_args_wanted [] - n_val_args_wanted fun_ty - --- | Variant of 'matchActualFunTys' that works when supplied only part --- (that is, to the right of some arrows) of the full function type -matchActualFunTysPart +matchActualFunTysRho :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> CtOrigin + -> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType + -> Arity + -> TcSigmaType + -> TcM (HsWrapper, [TcSigmaType], TcRhoType) +-- If matchActualFunTysRho n ty = (wrap, [t1,..,tn], res_ty) +-- then wrap : ty ~> (t1 -> ... -> tn -> res_ty) +-- and res_ty is a RhoType +-- NB: the returned type is top-instantiated; it's a RhoType +matchActualFunTysRho herald ct_orig mb_thing n_val_args_wanted fun_ty + = go n_val_args_wanted [] fun_ty + where + go 0 _ fun_ty + = do { (wrap, rho) <- topInstantiate ct_orig fun_ty + ; return (wrap, [], rho) } + go n so_far fun_ty + = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTySigma + herald ct_orig mb_thing + (n_val_args_wanted, so_far) + fun_ty + ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1 + ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc + ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) } + where + doc = text "When inferring the argument type of a function with type" <+> + quotes (ppr fun_ty) + +-- | matchActualFunTySigm does looks for just one function arrow +-- returning an uninstantiated sigma-type +matchActualFunTySigma :: SDoc -- See Note [Herald for matchExpectedFunTys] -> CtOrigin - -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType - -> Arity -- Total number of value args in the call - -> [TcSigmaType] -- Types of values args to which function has - -- been applied already (reversed) - -> Arity -- Number of new value args wanted - -> TcSigmaType -- Type to analyse - -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) + -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType + -> (Arity, [TcSigmaType]) -- Total number of value args in the call, and + -- types of values args to which function has + -- been applied already (reversed) + -- Both are used only for error messages) + -> TcSigmaType -- Type to analyse + -> TcM (HsWrapper, TcSigmaType, TcSigmaType) -- See Note [matchActualFunTys error handling] for all these arguments -matchActualFunTysPart herald ct_orig mb_thing - n_val_args_in_call arg_tys_so_far - n_val_args_wanted fun_ty - = go n_val_args_wanted arg_tys_so_far fun_ty + +-- If (wrap, arg_ty, res_ty) = matchActualFunTySigma ... fun_ty +-- then wrap :: fun_ty ~> (arg_ty -> res_ty) +-- and NB: res_ty is an (uninstantiated) SigmaType + +matchActualFunTySigma herald ct_orig mb_thing err_info fun_ty + = go fun_ty -- Does not allocate unnecessary meta variables: if the input already is -- a function, we just take it apart. Not only is this efficient, -- it's important for higher rank: the argument might be of form @@ -264,52 +294,28 @@ matchActualFunTysPart herald ct_orig mb_thing -- in elsewhere). where - -- This function has a bizarre mechanic: it accumulates arguments on - -- the way down and also builds an argument list on the way up. Why: - -- 1. The returns args list and the accumulated args list might be different. - -- The accumulated args include all the arg types for the function, - -- including those from before this function was called. The returned - -- list should include only those arguments produced by this call of - -- matchActualFunTys - -- - -- 2. The HsWrapper can be built only on the way up. It seems (more) - -- bizarre to build the HsWrapper but not the arg_tys. - -- - -- Refactoring is welcome. - go :: Arity - -> [TcSigmaType] -- Types of value args to which the function has - -- been applied so far (reversed) - -- Used only for error messages - -> TcSigmaType -- the remainder of the type as we're processing - -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) - go 0 _ ty = return (idHsWrapper, [], ty) - - go n so_far ty + go :: TcSigmaType -- The remainder of the type as we're processing + -> TcM (HsWrapper, TcSigmaType, TcSigmaType) + go ty | Just ty' <- tcView ty = go ty' + + go ty | not (null tvs && null theta) = do { (wrap1, rho) <- topInstantiate ct_orig ty - ; (wrap2, arg_tys, res_ty) <- go n so_far rho - ; return (wrap2 <.> wrap1, arg_tys, res_ty) } + ; (wrap2, arg_ty, res_ty) <- go rho + ; return (wrap2 <.> wrap1, arg_ty, res_ty) } where (tvs, theta, _) = tcSplitSigmaTy ty - go n so_far ty - | Just ty' <- tcView ty = go n so_far ty' - - go n so_far (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) + go (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty }) = ASSERT( af == VisArg ) - do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty:so_far) res_ty - ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc - , arg_ty : tys, ty_r ) } - where - doc = text "When inferring the argument type of a function with type" <+> - quotes (ppr fun_ty) + return (idHsWrapper, arg_ty, res_ty) - go n so_far ty@(TyVarTy tv) + go ty@(TyVarTy tv) | isMetaTyVar tv = do { cts <- readMetaTyVar tv ; case cts of - Indirect ty' -> go n so_far ty' - Flexi -> defer n ty } + Indirect ty' -> go ty' + Flexi -> defer ty } -- In all other cases we bale out into ordinary unification -- However unlike the meta-tyvar case, we are sure that the @@ -326,22 +332,23 @@ matchActualFunTysPart herald ct_orig mb_thing -- -- But in that case we add specialized type into error context -- anyway, because it may be useful. See also #9605. - go n so_far ty = addErrCtxtM (mk_ctxt so_far ty) (defer n ty) + go ty = addErrCtxtM (mk_ctxt ty) (defer ty) ------------ - defer n fun_ty - = do { arg_tys <- replicateM n newOpenFlexiTyVarTy - ; res_ty <- newOpenFlexiTyVarTy - ; let unif_fun_ty = mkVisFunTys arg_tys res_ty + defer fun_ty + = do { arg_ty <- newOpenFlexiTyVarTy + ; res_ty <- newOpenFlexiTyVarTy + ; let unif_fun_ty = mkVisFunTy arg_ty res_ty ; co <- unifyType mb_thing fun_ty unif_fun_ty - ; return (mkWpCastN co, arg_tys, res_ty) } + ; return (mkWpCastN co, arg_ty, res_ty) } ------------ - mk_ctxt :: [TcType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) - mk_ctxt arg_tys res_ty env + mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) + mk_ctxt res_ty env = do { (env', ty) <- zonkTidyTcType env $ - mkVisFunTys (reverse arg_tys) res_ty + mkVisFunTys (reverse arg_tys_so_far) res_ty ; return (env', mk_fun_tys_msg herald ty n_val_args_in_call) } + (n_val_args_in_call, arg_tys_so_far) = err_info mk_fun_tys_msg :: SDoc -> TcType -> Arity -> SDoc mk_fun_tys_msg herald ty n_args_in_call @@ -491,95 +498,51 @@ a place expecting a value of type expected_ty. I.e. that actual ty is more polymorphic than expected_ty -It returns a coercion function +It returns a wrapper function co_fn :: actual_ty ~ expected_ty which takes an HsExpr of type actual_ty into one of type expected_ty. - -These functions do not actually check for subsumption. They check if -expected_ty is an appropriate annotation to use for something of type -actual_ty. This difference matters when thinking about visible type -application. For example, - - forall a. a -> forall b. b -> b - DOES NOT SUBSUME - forall a b. a -> b -> b - -because the type arguments appear in a different order. (Neither does -it work the other way around.) BUT, these types are appropriate annotations -for one another. Because the user directs annotations, it's OK if some -arguments shuffle around -- after all, it's what the user wants. -Bottom line: none of this changes with visible type application. - -There are a number of wrinkles (below). - -Notice that Wrinkle 1 and 2 both require eta-expansion, which technically -may increase termination. We just put up with this, in exchange for getting -more predictable type inference. - -Wrinkle 1: Note [Deep skolemisation] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -We want (forall a. Int -> a -> a) <= (Int -> forall a. a->a) -(see section 4.6 of "Practical type inference for higher rank types") -So we must deeply-skolemise the RHS before we instantiate the LHS. - -That is why tc_sub_type starts with a call to tcSkolemise (which does the -deep skolemisation), and then calls the DS variant (which assumes -that expected_ty is deeply skolemised) - -Wrinkle 2: Note [Co/contra-variance of subsumption checking] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider g :: (Int -> Int) -> Int - f1 :: (forall a. a -> a) -> Int - f1 = g - - f2 :: (forall a. a -> a) -> Int - f2 x = g x -f2 will typecheck, and it would be odd/fragile if f1 did not. -But f1 will only typecheck if we have that - (Int->Int) -> Int <= (forall a. a->a) -> Int -And that is only true if we do the full co/contravariant thing -in the subsumption check. That happens in the FunTy case of -tcSubTypeDS_NC_O, and is the sole reason for the WpFun form of -HsWrapper. - -Another powerful reason for doing this co/contra stuff is visible -in #9569, involving instantiation of constraint variables, -and again involving eta-expansion. - -Wrinkle 3: Note [Higher rank types] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider tc150: - f y = \ (x::forall a. a->a). blah -The following happens: -* We will infer the type of the RHS, ie with a res_ty = alpha. -* Then the lambda will split alpha := beta -> gamma. -* And then we'll check tcSubType IsSwapped beta (forall a. a->a) - -So it's important that we unify beta := forall a. a->a, rather than -skolemising the type. -} --- | Call this variant when you are in a higher-rank situation and --- you know the right-hand type is deeply skolemised. -tcSubTypeHR :: CtOrigin -- ^ of the actual type - -> Maybe (HsExpr GhcRn) -- ^ If present, it has type ty_actual - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper -tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt +----------------- +-- tcWrapResult needs both un-type-checked (for origins and error messages) +-- and type-checked (for wrapping) expressions +tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType + -> TcM (HsExpr GhcTcId) +tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr + +tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType + -> TcM (HsExpr GhcTcId) +tcWrapResultO orig rn_expr expr actual_ty res_ty + = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty + , text "Expected:" <+> ppr res_ty ]) + ; wrap <- tcSubTypeNC orig GenSigCtxt (Just rn_expr) actual_ty res_ty + ; return (mkHsWrap wrap expr) } + +tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTcId + -> TcRhoType -- Actual -- a rho-type not a sigma-type + -> ExpRhoType -- Expected + -> TcM (HsExpr GhcTcId) +-- A version of tcWrapResult to use when the actual type is a +-- rho-type, so nothing to instantiate; just go straight to unify. +-- It means we don't need to pass in a CtOrigin +tcWrapResultMono rn_expr expr act_ty res_ty + = ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr ) + do { co <- case res_ty of + Infer inf_res -> fillInferResult act_ty inf_res + Check exp_ty -> unifyType (Just rn_expr) act_ty exp_ty + ; return (mkHsWrapCo co expr) } ------------------------ tcSubTypePat :: CtOrigin -> UserTypeCtxt -> ExpSigmaType -> TcSigmaType -> TcM HsWrapper +-- Used in patterns; polarity is backwards compared +-- to tcSubType -- If wrap = tc_sub_type_et t1 t2 -- => wrap :: t1 ~> t2 -tcSubTypePat orig ctxt (Check ty_actual) ty_expected - = tc_sub_tc_type eq_orig orig ctxt ty_actual ty_expected - where - eq_orig = TypeEqOrigin { uo_actual = ty_expected - , uo_expected = ty_actual - , uo_thing = Nothing - , uo_visible = True } +tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected + = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected tcSubTypePat _ _ (Infer inf_res) ty_expected = do { co <- fillInferResult ty_expected inf_res @@ -587,106 +550,72 @@ tcSubTypePat _ _ (Infer inf_res) ty_expected ; return (mkWpCastN (mkTcSymCo co)) } ------------------------- -tcSubTypeO :: CtOrigin -- ^ of the actual type - -> UserTypeCtxt -- ^ of the expected type - -> TcSigmaType - -> ExpRhoType - -> TcM HsWrapper -tcSubTypeO orig ctxt ty_actual ty_expected +--------------- +tcSubType :: CtOrigin -> UserTypeCtxt + -> TcSigmaType -- Actual + -> ExpRhoType -- Expected + -> TcM HsWrapper +-- Checks that 'actual' is more polymorphic than 'expected' +tcSubType orig ctxt ty_actual ty_expected = addSubTypeCtxt ty_actual ty_expected $ - do { traceTc "tcSubTypeDS_O" (vcat [ pprCtOrigin orig - , pprUserTypeCtxt ctxt - , ppr ty_actual - , ppr ty_expected ]) - ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } - -addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a -addSubTypeCtxt ty_actual ty_expected thing_inside - | isRhoTy ty_actual -- If there is no polymorphism involved, the - , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions) - = thing_inside -- gives enough context by itself - | otherwise - = addErrCtxtM mk_msg thing_inside - where - mk_msg tidy_env - = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual - -- might not be filled if we're debugging. ugh. - ; mb_ty_expected <- readExpType_maybe ty_expected - ; (tidy_env, ty_expected) <- case mb_ty_expected of - Just ty -> second mkCheckExpType <$> - zonkTidyTcType tidy_env ty - Nothing -> return (tidy_env, ty_expected) - ; ty_expected <- readExpType ty_expected - ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected - ; let msg = vcat [ hang (text "When checking that:") - 4 (ppr ty_actual) - , nest 2 (hang (text "is more polymorphic than:") - 2 (ppr ty_expected)) ] - ; return (tidy_env, msg) } + do { traceTc "tcSubType" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) + ; tcSubTypeNC orig ctxt Nothing ty_actual ty_expected } + +tcSubTypeNC :: CtOrigin -- Used when instantiating + -> UserTypeCtxt -- Used when skolemising + -> Maybe (HsExpr GhcRn) -- The expression that has type 'actual' (if known) + -> TcSigmaType -- Actual type + -> ExpRhoType -- Expected type + -> TcM HsWrapper +tcSubTypeNC inst_orig ctxt m_thing ty_actual res_ty + = case res_ty of + Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res + Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt + ty_actual ty_expected --------------- --- The "_NC" variants do not add a typechecker-error context; --- the caller is assumed to do that - -tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tcSubTypeSigma :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +-- External entry point, but no ExpTypes on either side -- Checks that actual <= expected -- Returns HsWrapper :: actual ~ expected -tcSubType_NC ctxt ty_actual ty_expected - = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tc_sub_tc_type origin origin ctxt ty_actual ty_expected } +tcSubTypeSigma ctxt ty_actual ty_expected + = tc_sub_type (unifyType Nothing) eq_orig ctxt ty_actual ty_expected where - origin = TypeEqOrigin { uo_actual = ty_actual - , uo_expected = ty_expected - , uo_thing = Nothing - , uo_visible = True } - -tcSubTypeDS :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised (hence "DS") -tcSubTypeDS orig ctxt ty_actual ty_expected - = addSubTypeCtxt ty_actual ty_expected $ - do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tcSubTypeDS_NC_O orig ctxt Nothing ty_actual ty_expected } - -tcSubTypeDS_NC_O :: CtOrigin -- origin used for instantiation only - -> UserTypeCtxt - -> Maybe (HsExpr GhcRn) - -> TcSigmaType -> ExpRhoType -> TcM HsWrapper --- Just like tcSubType, but with the additional precondition that --- ty_expected is deeply skolemised -tcSubTypeDS_NC_O inst_orig ctxt m_thing ty_actual ty_expected - = case ty_expected of - Infer inf_res -> instantiateAndFillInferResult inst_orig ty_actual inf_res - Check ty -> tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty - where - eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty - , uo_thing = ppr <$> m_thing - , uo_visible = True } + eq_orig = TypeEqOrigin { uo_actual = ty_actual + , uo_expected = ty_expected + , uo_thing = Nothing + , uo_visible = True } --------------- -tc_sub_tc_type :: CtOrigin -- used when calling uType - -> CtOrigin -- used when instantiating - -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN) -- How to unify + -> CtOrigin -- Used when instantiating + -> UserTypeCtxt -- Used when skolemising + -> TcSigmaType -- Actual; a sigma-type + -> TcSigmaType -- Expected; also a sigma-type + -> TcM HsWrapper +-- Checks that actual_ty is more polymorphic than expected_ty -- If wrap = tc_sub_type t1 t2 -- => wrap :: t1 ~> t2 -tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected +tc_sub_type unify inst_orig ctxt ty_actual ty_expected | definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily] , not (possibly_poly ty_actual) - = do { traceTc "tc_sub_tc_type (drop to equality)" $ + = do { traceTc "tc_sub_type (drop to equality)" $ vcat [ text "ty_actual =" <+> ppr ty_actual , text "ty_expected =" <+> ppr ty_expected ] ; mkWpCastN <$> - uType TypeLevel eq_orig ty_actual ty_expected } + unify ty_actual ty_expected } | otherwise -- This is the general case - = do { traceTc "tc_sub_tc_type (general case)" $ + = do { traceTc "tc_sub_type (general case)" $ vcat [ text "ty_actual =" <+> ppr ty_actual , text "ty_expected =" <+> ppr ty_expected ] - ; (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ - \ _ sk_rho -> - tc_sub_type_ds eq_orig inst_orig ctxt - ty_actual sk_rho + + ; (sk_wrap, inner_wrap) + <- tcSkolemise ctxt ty_expected $ \ sk_rho -> + do { (wrap, rho_a) <- topInstantiate inst_orig ty_actual + ; cow <- unify rho_a sk_rho + ; return (mkWpCastN cow <.> wrap) } + ; return (sk_wrap <.> inner_wrap) } where possibly_poly ty @@ -705,6 +634,31 @@ tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected | otherwise = False +------------------------ +addSubTypeCtxt :: TcType -> ExpType -> TcM a -> TcM a +addSubTypeCtxt ty_actual ty_expected thing_inside + | isRhoTy ty_actual -- If there is no polymorphism involved, the + , isRhoExpTy ty_expected -- TypeEqOrigin stuff (added by the _NC functions) + = thing_inside -- gives enough context by itself + | otherwise + = addErrCtxtM mk_msg thing_inside + where + mk_msg tidy_env + = do { (tidy_env, ty_actual) <- zonkTidyTcType tidy_env ty_actual + -- might not be filled if we're debugging. ugh. + ; mb_ty_expected <- readExpType_maybe ty_expected + ; (tidy_env, ty_expected) <- case mb_ty_expected of + Just ty -> second mkCheckExpType <$> + zonkTidyTcType tidy_env ty + Nothing -> return (tidy_env, ty_expected) + ; ty_expected <- readExpType ty_expected + ; (tidy_env, ty_expected) <- zonkTidyTcType tidy_env ty_expected + ; let msg = vcat [ hang (text "When checking that:") + 4 (ppr ty_actual) + , nest 2 (hang (text "is more polymorphic than:") + 2 (ppr ty_expected)) ] + ; return (tidy_env, msg) } + {- Note [Don't skolemise unnecessarily] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Suppose we are trying to solve @@ -740,98 +694,9 @@ accept (e.g. #13752). So the test (which is only to improve error message) is very conservative: * ty_actual is /definitely/ monomorphic * ty_expected is /definitely/ polymorphic --} - ---------------- -tc_sub_type_ds :: CtOrigin -- used when calling uType - -> CtOrigin -- used when instantiating - -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper --- If wrap = tc_sub_type_ds t1 t2 --- => wrap :: t1 ~> t2 --- Here is where the work actually happens! --- Precondition: ty_expected is deeply skolemised -tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected - = do { traceTc "tc_sub_type_ds" $ - vcat [ text "ty_actual =" <+> ppr ty_actual - , text "ty_expected =" <+> ppr ty_expected ] - ; go ty_actual ty_expected } - where - go ty_a ty_e | Just ty_a' <- tcView ty_a = go ty_a' ty_e - | Just ty_e' <- tcView ty_e = go ty_a ty_e' - go (TyVarTy tv_a) ty_e - = do { lookup_res <- lookupTcTyVar tv_a - ; case lookup_res of - Filled ty_a' -> - do { traceTc "tcSubTypeDS_NC_O following filled act meta-tyvar:" - (ppr tv_a <+> text "-->" <+> ppr ty_a') - ; tc_sub_type_ds eq_orig inst_orig ctxt ty_a' ty_e } - Unfilled _ -> unify } - - -- Historical note (Sept 16): there was a case here for - -- go ty_a (TyVarTy alpha) - -- which, in the impredicative case unified alpha := ty_a - -- where th_a is a polytype. Not only is this probably bogus (we - -- simply do not have decent story for impredicative types), but it - -- caused #12616 because (also bizarrely) 'deriving' code had - -- -XImpredicativeTypes on. I deleted the entire case. - - go (FunTy { ft_af = VisArg, ft_arg = act_arg, ft_res = act_res }) - (FunTy { ft_af = VisArg, ft_arg = exp_arg, ft_res = exp_res }) - = -- See Note [Co/contra-variance of subsumption checking] - do { res_wrap <- tc_sub_type_ds eq_orig inst_orig ctxt act_res exp_res - ; arg_wrap <- tc_sub_tc_type eq_orig given_orig GenSigCtxt exp_arg act_arg - -- GenSigCtxt: See Note [Setting the argument context] - ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res doc) } - -- arg_wrap :: exp_arg ~> act_arg - -- res_wrap :: act-res ~> exp_res - where - given_orig = GivenOrigin (SigSkol GenSigCtxt exp_arg []) - doc = text "When checking that" <+> quotes (ppr ty_actual) <+> - text "is more polymorphic than" <+> quotes (ppr ty_expected) - - go ty_a ty_e - | let (tvs, theta, _) = tcSplitSigmaTy ty_a - , not (null tvs && null theta) - = do { (in_wrap, in_rho) <- topInstantiate inst_orig ty_a - ; body_wrap <- tc_sub_type_ds - (eq_orig { uo_actual = in_rho - , uo_expected = ty_expected }) - inst_orig ctxt in_rho ty_e - ; return (body_wrap <.> in_wrap) } - - | otherwise -- Revert to unification - = inst_and_unify - -- It's still possible that ty_actual has nested foralls. Instantiate - -- these, as there's no way unification will succeed with them in. - -- See typecheck/should_compile/T11305 for an example of when this - -- is important. The problem is that we're checking something like - -- a -> forall b. b -> b <= alpha beta gamma - -- where we end up with alpha := (->) - - inst_and_unify = do { (wrap, rho_a) <- deeplyInstantiate inst_orig ty_actual - - -- If we haven't recurred through an arrow, then - -- the eq_orig will list ty_actual. In this case, - -- we want to update the origin to reflect the - -- instantiation. If we *have* recurred through - -- an arrow, it's better not to update. - ; let eq_orig' = case eq_orig of - TypeEqOrigin { uo_actual = orig_ty_actual } - | orig_ty_actual `tcEqType` ty_actual - , not (isIdHsWrapper wrap) - -> eq_orig { uo_actual = rho_a } - _ -> eq_orig - - ; cow <- uType TypeLevel eq_orig' rho_a ty_expected - ; return (mkWpCastN cow <.> wrap) } - - - -- use versions without synonyms expanded - unify = mkWpCastN <$> uType TypeLevel eq_orig ty_actual ty_expected - -{- Note [Settting the argument context] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Note [Settting the argument context] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider we are doing the ambiguity check for the (bogus) f :: (forall a b. C b => a -> a) -> Int @@ -857,24 +722,6 @@ to a UserTypeCtxt of GenSigCtxt. Why? See Note [When to build an implication] -} ------------------ --- needs both un-type-checked (for origins) and type-checked (for wrapping) --- expressions -tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType - -> TcM (HsExpr GhcTcId) -tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr - --- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more --- convenient. -tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType - -> TcM (HsExpr GhcTcId) -tcWrapResultO orig rn_expr expr actual_ty res_ty - = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty - , text "Expected:" <+> ppr res_ty ]) - ; cow <- tcSubTypeDS_NC_O orig GenSigCtxt - (Just rn_expr) actual_ty res_ty - ; return (mkHsWrap cow expr) } - {- ********************************************************************** %* * @@ -896,7 +743,7 @@ instantiateAndFillInferResult :: CtOrigin -> TcType -> InferResult -> TcM HsWrap -- => wrap :: t1 ~> t2 -- See Note [Instantiation of InferResult] instantiateAndFillInferResult orig ty inf_res - = do { (wrap, rho) <- deeplyInstantiate orig ty + = do { (wrap, rho) <- topInstantiate orig ty ; co <- fillInferResult rho inf_res ; return (mkWpCastN co <.> wrap) } @@ -1090,48 +937,64 @@ the thinking. * * ********************************************************************* -} --- | Take an "expected type" and strip off quantifiers to expose the --- type underneath, binding the new skolems for the @thing_inside@. --- The returned 'HsWrapper' has type @specific_ty -> expected_ty@. -tcSkolemise :: UserTypeCtxt -> TcSigmaType - -> ([TcTyVar] -> TcType -> TcM result) - -- ^ These are only ever used for scoped type variables. - -> TcM (HsWrapper, result) - -- ^ The expression has type: spec_ty -> expected_ty +{- Note [Skolemisation] +~~~~~~~~~~~~~~~~~~~~~~~ +tcSkolemise takes "expected type" and strip off quantifiers to expose the +type underneath, binding the new skolems for the 'thing_inside' +The returned 'HsWrapper' has type (specific_ty -> expected_ty). + +Note that for a nested type like + forall a. Eq a => forall b. Ord b => blah +we still only build one implication constraint + forall a b. (Eq a, Ord b) => <constraints> +This is just an optimisation, but it's why we use topSkolemise to +build the pieces from all the layers, before making a single call +to checkConstraints. + +tcSkolemiseScoped is very similar, but differs in two ways: + +* It deals specially with just the outer forall, bringing those + type variables into lexical scope. To my surprise, I found that + doing this regardless (in tcSkolemise) caused a non-trivial (1%-ish) + perf hit on the compiler. + +* It always calls checkConstraints, even if there are no skolem + variables at all. Reason: there might be nested deferred errors + that must not be allowed to float to top level. + See Note [When to build an implication] below. +-} + +tcSkolemise, tcSkolemiseScoped + :: UserTypeCtxt -> TcSigmaType + -> (TcType -> TcM result) + -> TcM (HsWrapper, result) + -- ^ The wrapper has type: spec_ty ~> expected_ty + +tcSkolemiseScoped ctxt expected_ty thing_inside + = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty + ; let skol_tvs = map snd tv_prs + skol_info = SigSkol ctxt expected_ty tv_prs + + ; (ev_binds, res) + <- checkConstraints skol_info skol_tvs given $ + tcExtendNameTyVarEnv tv_prs $ + thing_inside rho_ty + + ; return (wrap <.> mkWpLet ev_binds, res) } tcSkolemise ctxt expected_ty thing_inside - -- We expect expected_ty to be a forall-type - -- If not, the call is a no-op - = do { traceTc "tcSkolemise" Outputable.empty - ; (wrap, tv_prs, given, rho') <- deeplySkolemise expected_ty - - ; lvl <- getTcLevel - ; when debugIsOn $ - traceTc "tcSkolemise" $ vcat [ - ppr lvl, - text "expected_ty" <+> ppr expected_ty, - text "inst tyvars" <+> ppr tv_prs, - text "given" <+> ppr given, - text "inst type" <+> ppr rho' ] - - -- Generally we must check that the "forall_tvs" haven't been constrained - -- The interesting bit here is that we must include the free variables - -- of the expected_ty. Here's an example: - -- runST (newVar True) - -- Here, if we don't make a check, we'll get a type (ST s (MutVar s Bool)) - -- for (newVar True), with s fresh. Then we unify with the runST's arg type - -- forall s'. ST s' a. That unifies s' with s, and a with MutVar s Bool. - -- So now s' isn't unconstrained because it's linked to a. - -- - -- However [Oct 10] now that the untouchables are a range of - -- TcTyVars, all this is handled automatically with no need for - -- extra faffing around + | isRhoTy expected_ty -- Short cut for common case + = do { res <- thing_inside expected_ty + ; return (idHsWrapper, res) } + | otherwise + = do { (wrap, tv_prs, given, rho_ty) <- topSkolemise expected_ty - ; let tvs' = map snd tv_prs + ; let skol_tvs = map snd tv_prs skol_info = SigSkol ctxt expected_ty tv_prs - ; (ev_binds, result) <- checkConstraints skol_info tvs' given $ - thing_inside tvs' rho' + ; (ev_binds, result) + <- checkConstraints skol_info skol_tvs given $ + thing_inside rho_ty ; return (wrap <.> mkWpLet ev_binds, result) } -- The ev_binds returned by checkConstraints is very @@ -1144,7 +1007,8 @@ tcSkolemiseET :: UserTypeCtxt -> ExpSigmaType tcSkolemiseET _ et@(Infer {}) thing_inside = (idHsWrapper, ) <$> thing_inside et tcSkolemiseET ctxt (Check ty) thing_inside - = tcSkolemise ctxt ty $ \_ -> thing_inside . mkCheckExpType + = tcSkolemise ctxt ty $ \rho_ty -> + thing_inside (mkCheckExpType rho_ty) checkConstraints :: SkolemInfo -> [TcTyVar] -- Skolems @@ -1162,7 +1026,7 @@ checkConstraints skol_info skol_tvs given thing_inside ; emitImplications implics ; return (ev_binds, result) } - else -- Fast path. We check every function argument with tcCheckExpr, + else -- Fast path. We check every function argument with tcCheckPolyExpr, -- which uses tcSkolemise and hence checkConstraints. -- So this fast path is well-exercised do { res <- thing_inside @@ -1175,38 +1039,33 @@ checkTvConstraints :: SkolemInfo checkTvConstraints skol_info skol_tvs thing_inside = do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside - ; emitResidualTvConstraint skol_info Nothing skol_tvs tclvl wanted + ; emitResidualTvConstraint skol_info skol_tvs tclvl wanted ; return result } -emitResidualTvConstraint :: SkolemInfo -> Maybe SDoc -> [TcTyVar] +emitResidualTvConstraint :: SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM () -emitResidualTvConstraint skol_info m_telescope skol_tvs tclvl wanted +emitResidualTvConstraint skol_info skol_tvs tclvl wanted | isEmptyWC wanted - , isNothing m_telescope || skol_tvs `lengthAtMost` 1 - -- If m_telescope is (Just d), we must do the bad-telescope check, - -- so we must /not/ discard the implication even if there are no - -- wanted constraints. See Note [Checking telescopes] in GHC.Tc.Types.Constraint. - -- Lacking this check led to #16247 = return () | otherwise - = do { ev_binds <- newNoTcEvBinds + = do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted + ; emitImplication implic } + +buildTvImplication :: SkolemInfo -> [TcTyVar] + -> TcLevel -> WantedConstraints -> TcM Implication +buildTvImplication skol_info skol_tvs tclvl wanted + = do { ev_binds <- newNoTcEvBinds -- Used for equalities only, so all the constraints + -- are solved by filling in coercion holes, not + -- by creating a value-level evidence binding ; implic <- newImplication - ; let status | insolubleWC wanted = IC_Insoluble - | otherwise = IC_Unsolved - -- If the inner constraints are insoluble, - -- we should mark the outer one similarly, - -- so that insolubleWC works on the outer one - - ; emitImplication $ - implic { ic_status = status - , ic_tclvl = tclvl - , ic_skols = skol_tvs - , ic_no_eqs = True - , ic_telescope = m_telescope - , ic_wanted = wanted - , ic_binds = ev_binds - , ic_info = skol_info } } + + ; return (implic { ic_tclvl = tclvl + , ic_skols = skol_tvs + , ic_no_eqs = True + , ic_wanted = wanted + , ic_binds = ev_binds + , ic_info = skol_info }) } implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool -- See Note [When to build an implication] @@ -1319,21 +1178,35 @@ unifyType :: Maybe (HsExpr GhcRn) -- ^ If present, has type 'ty1' -> TcTauType -> TcTauType -> TcM TcCoercionN -- Actual and expected types -- Returns a coercion : ty1 ~ ty2 -unifyType thing ty1 ty2 = traceTc "utype" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> - uType TypeLevel origin ty1 ty2 +unifyType thing ty1 ty2 + = uType TypeLevel origin ty1 ty2 where - origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 - , uo_thing = ppr <$> thing - , uo_visible = True } -- always called from a visible context + origin = TypeEqOrigin { uo_actual = ty1 + , uo_expected = ty2 + , uo_thing = ppr <$> thing + , uo_visible = True } + +unifyTypeET :: TcTauType -> TcTauType -> TcM CoercionN +-- Like unifyType, but swap expected and actual in error messages +-- This is used when typechecking patterns +unifyTypeET ty1 ty2 + = uType TypeLevel origin ty1 ty2 + where + origin = TypeEqOrigin { uo_actual = ty2 -- NB swapped + , uo_expected = ty1 -- NB swapped + , uo_thing = Nothing + , uo_visible = True } + unifyKind :: Maybe (HsType GhcRn) -> TcKind -> TcKind -> TcM CoercionN -unifyKind thing ty1 ty2 = traceTc "ukind" (ppr ty1 $$ ppr ty2 $$ ppr thing) >> - uType KindLevel origin ty1 ty2 - where origin = TypeEqOrigin { uo_actual = ty1, uo_expected = ty2 - , uo_thing = ppr <$> thing - , uo_visible = True } -- also always from a visible context +unifyKind thing ty1 ty2 + = uType KindLevel origin ty1 ty2 + where + origin = TypeEqOrigin { uo_actual = ty1 + , uo_expected = ty2 + , uo_thing = ppr <$> thing + , uo_visible = True } ---------------- {- %************************************************************************ @@ -1639,7 +1512,7 @@ uUnfilledVar1 origin t_or_k swapped tv1 ty2 go tv2 | tv1 == tv2 -- Same type variable => no-op = return (mkNomReflCo (mkTyVarTy tv1)) - | swapOverTyVars tv1 tv2 -- Distinct type variables + | swapOverTyVars False tv1 tv2 -- Distinct type variables -- Swap meta tyvar to the left if poss = do { tv1 <- zonkTyCoVarKind tv1 -- We must zonk tv1's kind because that might @@ -1696,8 +1569,12 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2 defer = unSwap swapped (uType_defer t_or_k origin) ty1 ty2 -swapOverTyVars :: TcTyVar -> TcTyVar -> Bool -swapOverTyVars tv1 tv2 +swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool +swapOverTyVars is_given tv1 tv2 + -- See Note [Unification variables on the left] + | not is_given, pri1 == 0, pri2 > 0 = True + | not is_given, pri2 == 0, pri1 > 0 = False + -- Level comparison: see Note [TyVar/TyVar orientation] | lvl1 `strictlyDeeperThan` lvl2 = False | lvl2 `strictlyDeeperThan` lvl1 = True @@ -1786,6 +1663,24 @@ So we look for a positive reason to swap, using a three-step test: Uniques. See Note [Eliminate younger unification variables] (which also explains why we don't do this any more) +Note [Unification variables on the left] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +For wanteds, but not givens, swap (skolem ~ meta-tv) regardless of +level, so that the unification variable is on the left. + +* We /don't/ want this for Givens because if we ave + [G] a[2] ~ alpha[1] + [W] Bool ~ a[2] + we want to rewrite the wanted to Bool ~ alpha[1], + so we can float the constraint and solve it. + +* But for Wanteds putting the unification variable on + the left means an easier job when floating, and when + reporting errors -- just fewer cases to consider. + + In particular, we get better skolem-escape messages: + see #18114 + Note [Deeper level on the left] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The most important thing is that we want to put tyvars with diff --git a/compiler/GHC/Tc/Validity.hs b/compiler/GHC/Tc/Validity.hs index 4f6b4f5887..32dfc16ea3 100644 --- a/compiler/GHC/Tc/Validity.hs +++ b/compiler/GHC/Tc/Validity.hs @@ -27,7 +27,7 @@ import GHC.Prelude import GHC.Data.Maybe -- friends: -import GHC.Tc.Utils.Unify ( tcSubType_NC ) +import GHC.Tc.Utils.Unify ( tcSubTypeSigma ) import GHC.Tc.Solver ( simplifyAmbiguityCheck ) import GHC.Tc.Instance.Class ( matchGlobalInst, ClsInstResult(..), InstanceWhat(..), AssocInstInfo(..) ) import GHC.Core.TyCo.FVs @@ -216,7 +216,7 @@ checkAmbiguity ctxt ty ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes ; (_wrap, wanted) <- addErrCtxt (mk_msg allow_ambiguous) $ captureConstraints $ - tcSubType_NC ctxt ty ty + tcSubTypeSigma ctxt ty ty ; simplifyAmbiguityCheck ty wanted ; traceTc "Done ambiguity check for" (ppr ty) } |