diff options
| author | Richard Eisenberg <eir@cis.upenn.edu> | 2015-12-24 14:33:19 -0500 |
|---|---|---|
| committer | Richard Eisenberg <eir@cis.upenn.edu> | 2015-12-24 14:37:39 -0500 |
| commit | 2db18b8135335da2da9918b722699df684097be9 (patch) | |
| tree | 660dd90916aa6568694bbe39cdab83c7af98c5d7 /compiler | |
| parent | 48db13d279d592ed3044cbaf3513854bcb0d3dce (diff) | |
| download | haskell-2db18b8135335da2da9918b722699df684097be9.tar.gz | |
Visible type application
This re-working of the typechecker algorithm is based on
the paper "Visible type application", by Richard Eisenberg,
Stephanie Weirich, and Hamidhasan Ahmed, to be published at
ESOP'16.
This patch introduces -XTypeApplications, which allows users
to say, for example `id @Int`, which has type `Int -> Int`. See
the changes to the user manual for details.
This patch addresses tickets #10619, #5296, #10589.
Diffstat (limited to 'compiler')
51 files changed, 2096 insertions, 982 deletions
diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs index 712a9b2b86..466e3c1604 100644 --- a/compiler/basicTypes/DataCon.hs +++ b/compiler/basicTypes/DataCon.hs @@ -768,7 +768,7 @@ mkDataCon name declared_infix prom_info tag = assoc "mkDataCon" (tyConDataCons rep_tycon `zip` [fIRST_TAG..]) con rep_arg_tys = dataConRepArgTys con - rep_ty = mkInvForAllTys univ_tvs $ mkInvForAllTys ex_tvs $ + rep_ty = mkSpecForAllTys univ_tvs $ mkInvForAllTys ex_tvs $ mkFunTys rep_arg_tys $ mkTyConApp rep_tycon (mkTyVarTys univ_tvs) @@ -1024,8 +1024,8 @@ dataConUserType (MkData { dcUnivTyVars = univ_tvs, dcExTyVars = ex_tvs, dcEqSpec = eq_spec, dcOtherTheta = theta, dcOrigArgTys = arg_tys, dcOrigResTy = res_ty }) - = mkInvForAllTys ((univ_tvs `minusList` map eqSpecTyVar eq_spec) ++ - ex_tvs) $ + = mkSpecForAllTys ((univ_tvs `minusList` map eqSpecTyVar eq_spec) ++ + ex_tvs) $ mkFunTys theta $ mkFunTys arg_tys $ res_ty diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs index 691e087ac2..f690732909 100644 --- a/compiler/basicTypes/MkId.hs +++ b/compiler/basicTypes/MkId.hs @@ -281,8 +281,8 @@ mkDictSelId name clas arg_tys = dataConRepArgTys data_con -- Includes the dictionary superclasses val_index = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name - sel_ty = mkInvForAllTys tyvars (mkFunTy (mkClassPred clas (mkTyVarTys tyvars)) - (getNth arg_tys val_index)) + sel_ty = mkSpecForAllTys tyvars (mkFunTy (mkClassPred clas (mkTyVarTys tyvars)) + (getNth arg_tys val_index)) base_info = noCafIdInfo `setArityInfo` 1 @@ -930,7 +930,7 @@ mkPrimOpId prim_op = id where (tyvars,arg_tys,res_ty, arity, strict_sig) = primOpSig prim_op - ty = mkInvForAllTys tyvars (mkFunTys arg_tys res_ty) + ty = mkSpecForAllTys tyvars (mkFunTys arg_tys res_ty) name = mkWiredInName gHC_PRIM (primOpOcc prim_op) (mkPrimOpIdUnique (primOpTag prim_op)) (AnId id) UserSyntax @@ -1014,7 +1014,7 @@ mkDictFunId dfun_name tvs theta clas tys mkDictFunTy :: [TyVar] -> ThetaType -> Class -> [Type] -> Type mkDictFunTy tvs theta clas tys - = mkInvSigmaTy tvs theta (mkClassPred clas tys) + = mkSpecSigmaTy tvs theta (mkClassPred clas tys) {- ************************************************************************ @@ -1062,7 +1062,7 @@ dollarId = pcMiscPrelId dollarName ty (noCafIdInfo `setUnfoldingInfo` unf) where fun_ty = mkFunTy alphaTy openBetaTy - ty = mkInvForAllTys [levity2TyVar, alphaTyVar, openBetaTyVar] $ + ty = mkSpecForAllTys [levity2TyVar, alphaTyVar, openBetaTyVar] $ mkFunTy fun_ty fun_ty unf = mkInlineUnfolding (Just 2) rhs [f,x] = mkTemplateLocals [fun_ty, alphaTy] @@ -1076,7 +1076,7 @@ proxyHashId = pcMiscPrelId proxyName ty (noCafIdInfo `setUnfoldingInfo` evaldUnfolding) -- Note [evaldUnfoldings] where - ty = mkInvForAllTys [kv, tv] (mkProxyPrimTy k t) + ty = mkSpecForAllTys [kv, tv] (mkProxyPrimTy k t) kv = kKiVar k = mkTyVarTy kv [tv] = mkTemplateTyVars [k] @@ -1091,9 +1091,9 @@ unsafeCoerceId info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding rhs - ty = mkInvForAllTys [ levity1TyVar, levity2TyVar - , openAlphaTyVar, openBetaTyVar ] - (mkFunTy openAlphaTy openBetaTy) + ty = mkSpecForAllTys [ levity1TyVar, levity2TyVar + , openAlphaTyVar, openBetaTyVar ] + (mkFunTy openAlphaTy openBetaTy) [x] = mkTemplateLocals [openAlphaTy] rhs = mkLams [ levity1TyVar, levity2TyVar @@ -1125,8 +1125,8 @@ seqId = pcMiscPrelId seqName ty info -- LHS of rules. That way we can have rules for 'seq'; -- see Note [seqId magic] - ty = mkInvForAllTys [alphaTyVar,betaTyVar] - (mkFunTy alphaTy (mkFunTy betaTy betaTy)) + ty = mkSpecForAllTys [alphaTyVar,betaTyVar] + (mkFunTy alphaTy (mkFunTy betaTy betaTy)) [x,y] = mkTemplateLocals [alphaTy, betaTy] rhs = mkLams [alphaTyVar,betaTyVar,x,y] (Case (Var x) x betaTy [(DEFAULT, [], Var y)]) @@ -1158,16 +1158,16 @@ lazyId :: Id -- See Note [lazyId magic] lazyId = pcMiscPrelId lazyIdName ty info where info = noCafIdInfo - ty = mkInvForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy) + ty = mkSpecForAllTys [alphaTyVar] (mkFunTy alphaTy alphaTy) oneShotId :: Id -- See Note [The oneShot function] oneShotId = pcMiscPrelId oneShotName ty info where info = noCafIdInfo `setInlinePragInfo` alwaysInlinePragma `setUnfoldingInfo` mkCompulsoryUnfolding rhs - ty = mkInvForAllTys [ levity1TyVar, levity2TyVar - , openAlphaTyVar, openBetaTyVar ] - (mkFunTy fun_ty fun_ty) + ty = mkSpecForAllTys [ levity1TyVar, levity2TyVar + , openAlphaTyVar, openBetaTyVar ] + (mkFunTy fun_ty fun_ty) fun_ty = mkFunTy alphaTy betaTy [body, x] = mkTemplateLocals [fun_ty, openAlphaTy] x' = setOneShotLambda x @@ -1188,7 +1188,7 @@ runRWId = pcMiscPrelId runRWName ty info arg_ty = stateRW `mkFunTy` ret_ty -- (State# RealWorld -> (# State# RealWorld, o #)) -- -> (# State# RealWorld, o #) - ty = mkInvForAllTys [levity1TyVar, openAlphaTyVar] $ + ty = mkSpecForAllTys [levity1TyVar, openAlphaTyVar] $ arg_ty `mkFunTy` ret_ty -------------------------------------------------------------------------------- @@ -1196,7 +1196,7 @@ magicDictId :: Id -- See Note [magicDictId magic] magicDictId = pcMiscPrelId magicDictName ty info where info = noCafIdInfo `setInlinePragInfo` neverInlinePragma - ty = mkInvForAllTys [alphaTyVar] alphaTy + ty = mkSpecForAllTys [alphaTyVar] alphaTy -------------------------------------------------------------------------------- @@ -1210,7 +1210,7 @@ coerceId = pcMiscPrelId coerceName ty info eqRPrimTy = mkTyConApp eqReprPrimTyCon [ liftedTypeKind , liftedTypeKind , alphaTy, betaTy ] - ty = mkInvForAllTys [alphaTyVar, betaTyVar] $ + ty = mkSpecForAllTys [alphaTyVar, betaTyVar] $ mkFunTys [eqRTy, alphaTy] betaTy [eqR,x,eq] = mkTemplateLocals [eqRTy, alphaTy, eqRPrimTy] diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs index c35bcf3e13..a884e963b1 100644 --- a/compiler/basicTypes/PatSyn.hs +++ b/compiler/basicTypes/PatSyn.hs @@ -25,7 +25,7 @@ module PatSyn ( #include "HsVersions.h" import Type -import TcType( mkInvSigmaTy ) +import TcType( mkSpecSigmaTy ) import Name import Outputable import Unique @@ -328,8 +328,8 @@ patSynType :: PatSyn -> Type patSynType (MkPatSyn { psUnivTyVars = univ_tvs, psReqTheta = req_theta , psExTyVars = ex_tvs, psProvTheta = prov_theta , psArgs = orig_args, psOrigResTy = orig_res_ty }) - = mkInvSigmaTy univ_tvs req_theta $ - mkInvSigmaTy ex_tvs prov_theta $ + = mkSpecSigmaTy univ_tvs req_theta $ -- use mkSpecSigmaTy because it + mkSpecSigmaTy ex_tvs prov_theta $ -- prints better mkFunTys orig_args orig_res_ty -- | Should the 'PatSyn' be presented infix? diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs index 07db78a931..2f1b67fe79 100644 --- a/compiler/coreSyn/MkCore.hs +++ b/compiler/coreSyn/MkCore.hs @@ -62,7 +62,7 @@ import TysWiredIn import PrelNames import HsUtils ( mkChunkified, chunkify ) -import TcType ( mkInvSigmaTy ) +import TcType ( mkSpecSigmaTy ) import Type import Coercion ( isCoVar ) import TysPrim @@ -684,8 +684,8 @@ mkRuntimeErrorId name = pc_bottoming_Id1 name runtimeErrorTy runtimeErrorTy :: Type -- The runtime error Ids take a UTF8-encoded string as argument -runtimeErrorTy = mkInvSigmaTy [levity1TyVar, openAlphaTyVar] [] - (mkFunTy addrPrimTy openAlphaTy) +runtimeErrorTy = mkSpecSigmaTy [levity1TyVar, openAlphaTyVar] [] + (mkFunTy addrPrimTy openAlphaTy) errorName :: Name errorName = mkWiredInIdName gHC_ERR (fsLit "error") errorIdKey eRROR_ID @@ -694,7 +694,7 @@ eRROR_ID :: Id eRROR_ID = pc_bottoming_Id2 errorName errorTy errorTy :: Type -- See Note [Error and friends have an "open-tyvar" forall] -errorTy = mkInvSigmaTy [levity1TyVar, openAlphaTyVar] [] +errorTy = mkSpecSigmaTy [levity1TyVar, openAlphaTyVar] [] (mkFunTys [ mkClassPred ipClass [ mkStrLitTy (fsLit "callStack") @@ -709,7 +709,7 @@ uNDEFINED_ID :: Id uNDEFINED_ID = pc_bottoming_Id1 undefinedName undefinedTy undefinedTy :: Type -- See Note [Error and friends have an "open-tyvar" forall] -undefinedTy = mkInvSigmaTy [levity1TyVar, openAlphaTyVar] [] +undefinedTy = mkSpecSigmaTy [levity1TyVar, openAlphaTyVar] [] (mkFunTy (mkClassPred ipClass [ mkStrLitTy (fsLit "callStack") @@ -727,7 +727,7 @@ Notice the levity polymophism. This ensures that * unboxed as well as boxed types * polymorphic types This is OK because it never returns, so the return type is irrelevant. -See Note [Sort-polymorphic tyvars accept foralls] in TcUnify. +See Note [Sort-polymorphic tyvars accept foralls] in TcMType. ************************************************************************ diff --git a/compiler/deSugar/Coverage.hs b/compiler/deSugar/Coverage.hs index 57d77c7eef..2711925161 100644 --- a/compiler/deSugar/Coverage.hs +++ b/compiler/deSugar/Coverage.hs @@ -632,7 +632,7 @@ addTickHsExpr (ExprWithTySigOut e ty) = (addTickLHsExprNever e) -- No need to tick the inner expression (return ty) -- for expressions with signatures -addTickHsExpr e@(HsType _) = return e +addTickHsExpr e@(HsTypeOut _) = return e -- Others should never happen in expression content. addTickHsExpr e = pprPanic "addTickHsExpr" (ppr e) @@ -870,8 +870,8 @@ addTickHsCmd (HsCmdArrForm e fix cmdtop) = (return fix) (mapM (liftL (addTickHsCmdTop)) cmdtop) -addTickHsCmd (HsCmdCast co cmd) - = liftM2 HsCmdCast (return co) (addTickHsCmd cmd) +addTickHsCmd (HsCmdWrap w cmd) + = liftM2 HsCmdWrap (return w) (addTickHsCmd cmd) -- Others should never happen in a command context. --addTickHsCmd e = pprPanic "addTickHsCmd" (ppr e) diff --git a/compiler/deSugar/DsArrows.hs b/compiler/deSugar/DsArrows.hs index 56c44c59d5..cc831d7c05 100644 --- a/compiler/deSugar/DsArrows.hs +++ b/compiler/deSugar/DsArrows.hs @@ -614,9 +614,9 @@ dsCmd _ids local_vars _stack_ty _res_ty (HsCmdArrForm op _ args) env_ids = do return (mkApps (App core_op (Type env_ty)) core_args, unionVarSets fv_sets) -dsCmd ids local_vars stack_ty res_ty (HsCmdCast coercion cmd) env_ids = do +dsCmd ids local_vars stack_ty res_ty (HsCmdWrap wrap cmd) env_ids = do (core_cmd, env_ids') <- dsCmd ids local_vars stack_ty res_ty cmd env_ids - wrapped_cmd <- dsHsWrapper (mkWpCastN coercion) core_cmd + wrapped_cmd <- dsHsWrapper wrap core_cmd return (wrapped_cmd, env_ids') dsCmd _ _ _ _ _ c = pprPanic "dsCmd" (ppr c) diff --git a/compiler/deSugar/DsBinds.hs b/compiler/deSugar/DsBinds.hs index 7bc12cb2bd..a79e9fa7e7 100644 --- a/compiler/deSugar/DsBinds.hs +++ b/compiler/deSugar/DsBinds.hs @@ -160,20 +160,23 @@ dsHsBind dflags (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dicts , abs_exports = [export] , abs_ev_binds = ev_binds, abs_binds = binds }) - | ABE { abe_wrap = wrap, abe_poly = global + | ABE { abe_inst_wrap = inst_wrap, abe_wrap = wrap, abe_poly = global , abe_mono = local, abe_prags = prags } <- export , not (xopt LangExt.Strict dflags) -- handle strict binds , not (anyBag (isBangedPatBind . unLoc) binds) -- in the next case = -- push type constraints deeper for pattern match check + -- See Note [AbsBinds wrappers] in HsBinds addDictsDs (toTcTypeBag (listToBag dicts)) $ do { (_, bind_prs) <- ds_lhs_binds binds ; let core_bind = Rec bind_prs ; ds_binds <- dsTcEvBinds_s ev_binds + ; inner_rhs <- dsHsWrapper inst_wrap $ + Let core_bind $ + Var local ; rhs <- dsHsWrapper wrap $ -- Usually the identity mkLams tyvars $ mkLams dicts $ mkCoreLets ds_binds $ - Let core_bind $ - Var local + inner_rhs ; (spec_binds, rules) <- dsSpecs rhs prags @@ -212,13 +215,17 @@ dsHsBind dflags -- Note [Desugar Strict binds] ; (exported_force_vars, extra_exports) <- get_exports local_force_vars - ; let mk_bind (ABE { abe_wrap = wrap, abe_poly = global + ; let mk_bind (ABE { abe_inst_wrap = inst_wrap, abe_wrap = wrap + , abe_poly = global , abe_mono = local, abe_prags = spec_prags }) + -- See Note [AbsBinds wrappers] in HsBinds = do { tup_id <- newSysLocalDs tup_ty + ; inner_rhs <- dsHsWrapper inst_wrap $ + mkTupleSelector all_locals local tup_id $ + mkVarApps (Var poly_tup_id) (tyvars ++ dicts) ; rhs <- dsHsWrapper wrap $ - mkLams tyvars $ mkLams dicts $ - mkTupleSelector all_locals local tup_id $ - mkVarApps (Var poly_tup_id) (tyvars ++ dicts) + mkLams tyvars $ mkLams dicts $ + inner_rhs ; let rhs_for_spec = Let (NonRec poly_tup_id poly_tup_rhs) rhs ; (spec_binds, rules) <- dsSpecs rhs_for_spec spec_prags ; let global' = (global `setInlinePragma` defaultInlinePragma) @@ -277,6 +284,7 @@ dsHsBind dflags return (ABE {abe_poly = global ,abe_mono = local ,abe_wrap = WpHole + ,abe_inst_wrap = WpHole ,abe_prags = SpecPrags []}) dsHsBind _ (PatSynBind{}) = panic "dsHsBind: PatSynBind" @@ -963,10 +971,10 @@ dsHsWrapper (WpLet ev_binds) e = do bs <- dsTcEvBinds ev_binds return (mkCoreLets bs e) dsHsWrapper (WpCompose c1 c2) e = do { e1 <- dsHsWrapper c2 e ; dsHsWrapper c1 e1 } -dsHsWrapper (WpFun c1 c2 t1 _) e = do { x <- newSysLocalDs t1 - ; e1 <- dsHsWrapper c1 (Var x) - ; e2 <- dsHsWrapper c2 (mkCoreAppDs (text "dsHsWrapper") e e1) - ; return (Lam x e2) } +dsHsWrapper (WpFun c1 c2 t1) e = do { x <- newSysLocalDs t1 + ; e1 <- dsHsWrapper c1 (Var x) + ; e2 <- dsHsWrapper c2 (mkCoreAppDs (text "dsHsWrapper") e e1) + ; return (Lam x e2) } dsHsWrapper (WpCast co) e = ASSERT(coercionRole co == Representational) return $ mkCastDs e co dsHsWrapper (WpEvLam ev) e = return $ Lam ev e diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs index 3b9a4cfbb0..999b945c0f 100644 --- a/compiler/deSugar/DsExpr.hs +++ b/compiler/deSugar/DsExpr.hs @@ -222,7 +222,10 @@ dsExpr (HsLamCase arg matches) ; return $ Lam arg_var $ bindNonRec discrim_var (Var arg_var) matching_code } dsExpr e@(HsApp fun arg) - = mkCoreAppDs (text "HsApp" <+> ppr e) <$> dsLExpr fun <*> dsLExpr arg + -- ignore type arguments here; they're in the wrappers instead at this point + | isLHsTypeExpr arg = dsLExpr fun + | otherwise = mkCoreAppDs (text "HsApp" <+> ppr e) + <$> dsLExpr fun <*> dsLExpr arg {- @@ -718,7 +721,8 @@ dsExpr (EWildPat {}) = panic "dsExpr:EWildPat" dsExpr (EAsPat {}) = panic "dsExpr:EAsPat" dsExpr (EViewPat {}) = panic "dsExpr:EViewPat" dsExpr (ELazyPat {}) = panic "dsExpr:ELazyPat" -dsExpr (HsType {}) = panic "dsExpr:HsType" +dsExpr (HsType {}) = panic "dsExpr:HsType" -- removed by typechecker +dsExpr (HsTypeOut {}) = panic "dsExpr:HsTypeOut" -- handled in HsApp case dsExpr (HsDo {}) = panic "dsExpr:HsDo" dsExpr (HsRecFld {}) = panic "dsExpr:HsRecFld" diff --git a/compiler/deSugar/Match.hs b/compiler/deSugar/Match.hs index b5a50e75af..7530a0a243 100644 --- a/compiler/deSugar/Match.hs +++ b/compiler/deSugar/Match.hs @@ -956,7 +956,7 @@ viewLExprEq (e1,_) (e2,_) = lexp e1 e2 -- equating different ways of writing a coercion) wrap WpHole WpHole = True wrap (WpCompose w1 w2) (WpCompose w1' w2') = wrap w1 w1' && wrap w2 w2' - wrap (WpFun w1 w2 _ _) (WpFun w1' w2' _ _) = wrap w1 w1' && wrap w2 w2' + wrap (WpFun w1 w2 _) (WpFun w1' w2' _) = wrap w1 w1' && wrap w2 w2' wrap (WpCast co) (WpCast co') = co `eqCoercion` co' wrap (WpEvApp et1) (WpEvApp et2) = et1 `ev_term` et2 wrap (WpTyApp t) (WpTyApp t') = eqType t t' diff --git a/compiler/hsSyn/HsBinds.hs b/compiler/hsSyn/HsBinds.hs index 7a1146395b..93dc5a9f10 100644 --- a/compiler/hsSyn/HsBinds.hs +++ b/compiler/hsSyn/HsBinds.hs @@ -236,11 +236,13 @@ deriving instance (DataId idL, DataId idR) -- See Note [AbsBinds] data ABExport id - = ABE { abe_poly :: id -- ^ Any INLINE pragmas is attached to this Id - , abe_mono :: id - , abe_wrap :: HsWrapper -- ^ See Note [AbsBinds wrappers] - -- Shape: (forall abs_tvs. abs_ev_vars => abe_mono) ~ abe_poly - , abe_prags :: TcSpecPrags -- ^ SPECIALISE pragmas + = ABE { abe_poly :: id -- ^ Any INLINE pragmas is attached to this Id + , abe_mono :: id + , abe_inst_wrap :: HsWrapper -- ^ See Note [AbsBinds wrappers] + -- ^ Shape: abe_mono ~ abe_insted + , abe_wrap :: HsWrapper -- ^ See Note [AbsBinds wrappers] + -- Shape: (forall abs_tvs. abs_ev_vars => abe_insted) ~ abe_poly + , abe_prags :: TcSpecPrags -- ^ SPECIALISE pragmas } deriving (Data, Typeable) -- | - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnPattern', @@ -375,6 +377,27 @@ The abe_wrap field deals with impedance-matching between and the thing we really want, which may have fewer type variables. The action happens in TcBinds.mkExport. +For abe_inst_wrap, consider this: + x = (*) +The abe_mono type will be forall a. Num a => a -> a -> a +because no instantiation happens during typechecking. Before inferring +a final type, we must instantiate this. See Note [Instantiate when inferring +a type] in TcBinds. The abe_inst_wrap takes the uninstantiated abe_mono type +to a proper instantiated type. In this case, the "abe_insted" is +(b -> b -> b). Note that the value of "abe_insted" isn't important; it's +just an intermediate form as we're going from abe_mono to abe_poly. See also +the desugaring code in DsBinds. + +It's conceivable that we could combine the two wrappers, but note that there +is a gap: neither wrapper tacks on the tvs and dicts from the outer AbsBinds. +These bits are added manually in desugaring. (See DsBinds.dsHsBind.) A problem +that would arise in combining them is that zonking becomes more challenging: +we want to zonk the tvs and dicts in the AbsBinds, but then we end up re-zonking +when we zonk the ABExport. And -- worse -- the combined wrapper would have +the tvs and dicts in binding positions, so they would shadow the original +tvs and dicts. This is all resolvable with some plumbing, but it seems simpler +just to keep the two wrappers distinct. + Note [Bind free vars] ~~~~~~~~~~~~~~~~~~~~~ The bind_fvs field of FunBind and PatBind records the free variables @@ -548,10 +571,12 @@ ppr_monobind (AbsBinds { abs_tvs = tyvars, abs_ev_vars = dictvars pprLHsBinds val_binds instance (OutputableBndr id) => Outputable (ABExport id) where - ppr (ABE { abe_wrap = wrap, abe_poly = gbl, abe_mono = lcl, abe_prags = prags }) + ppr (ABE { abe_wrap = wrap, abe_inst_wrap = inst_wrap + , abe_poly = gbl, abe_mono = lcl, abe_prags = prags }) = vcat [ ppr gbl <+> ptext (sLit "<=") <+> ppr lcl , nest 2 (pprTcSpecPrags prags) - , nest 2 (ppr wrap)] + , nest 2 (ppr wrap) + , nest 2 (ppr inst_wrap)] instance (OutputableBndr idL, OutputableBndr idR) => Outputable (PatSynBind idL idR) where ppr (PSB{ psb_id = L _ psyn, psb_args = details, psb_def = pat, psb_dir = dir }) diff --git a/compiler/hsSyn/HsExpr.hs b/compiler/hsSyn/HsExpr.hs index 6e02df7438..158993eb2e 100644 --- a/compiler/hsSyn/HsExpr.hs +++ b/compiler/hsSyn/HsExpr.hs @@ -502,7 +502,14 @@ data HsExpr id -- For details on above see note [Api annotations] in ApiAnnotation | ELazyPat (LHsExpr id) -- ~ pattern - | HsType (LHsType id) -- Explicit type argument; e.g f {| Int |} x y + -- | Use for type application in expressions. + -- 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnAt' + + -- For details on above see note [Api annotations] in ApiAnnotation + | HsType (LHsWcType id) -- Explicit type argument; e.g f @Int x y + -- NB: Has wildcards, but no implicit quant. + + | HsTypeOut (LHsWcType Name) -- just for pretty-printing --------------------------------------- -- Finally, HsWrap appears only in typechecker output @@ -762,7 +769,10 @@ ppr_expr (HsSCC _ (StringLiteral _ lbl) expr) pprParendExpr expr ] ppr_expr (HsWrap co_fn e) = pprHsWrapper (pprExpr e) co_fn -ppr_expr (HsType id) = ppr id +ppr_expr (HsType (HsWC { hswc_body = ty })) + = char '@' <> pprParendHsType (unLoc ty) +ppr_expr (HsTypeOut (HsWC { hswc_body = ty })) + = char '@' <> pprParendHsType (unLoc ty) ppr_expr (HsSpliceE s) = pprSplice s ppr_expr (HsBracket b) = pprHsBracket b @@ -864,6 +874,8 @@ hsExprNeedsParens (HsTcBracketOut {}) = False hsExprNeedsParens (HsDo sc _ _) | isListCompExpr sc = False hsExprNeedsParens (HsRecFld{}) = False +hsExprNeedsParens (HsType {}) = False +hsExprNeedsParens (HsTypeOut {}) = False hsExprNeedsParens _ = True @@ -970,10 +982,10 @@ data HsCmd id -- For details on above see note [Api annotations] in ApiAnnotation - | HsCmdCast TcCoercionN -- A simpler version of HsWrap in HsExpr + | HsCmdWrap HsWrapper (HsCmd id) -- If cmd :: arg1 --> res - -- co :: arg1 ~ arg2 - -- Then (HsCmdCast co cmd) :: arg2 --> res + -- wrap :: arg1 "->" arg2 + -- Then (HsCmdWrap wrap cmd) :: arg2 --> res deriving (Typeable) deriving instance (DataId id) => Data (HsCmd id) @@ -1054,9 +1066,9 @@ ppr_cmd (HsCmdLet (L _ binds) cmd) = sep [hang (ptext (sLit "let")) 2 (pprBinds binds), hang (ptext (sLit "in")) 2 (ppr cmd)] -ppr_cmd (HsCmdDo (L _ stmts) _) = pprDo ArrowExpr stmts -ppr_cmd (HsCmdCast co cmd) = sep [ ppr_cmd cmd - , ptext (sLit "|>") <+> ppr co ] +ppr_cmd (HsCmdDo (L _ stmts) _) = pprDo ArrowExpr stmts + +ppr_cmd (HsCmdWrap w cmd) = pprHsWrapper (ppr_cmd cmd) w ppr_cmd (HsCmdArrApp arrow arg _ HsFirstOrderApp True) = hsep [ppr_lexpr arrow, larrowt, ppr_lexpr arg] @@ -1186,6 +1198,13 @@ isInfixMatch match = case m_fixity match of isEmptyMatchGroup :: MatchGroup id body -> Bool isEmptyMatchGroup (MG { mg_alts = ms }) = null $ unLoc ms +-- | Is there only one RHS in this group? +isSingletonMatchGroup :: MatchGroup id body -> Bool +isSingletonMatchGroup (MG { mg_alts = L _ [match] }) + | L _ (Match { m_grhss = GRHSs { grhssGRHSs = [_] } }) <- match + = True +isSingletonMatchGroup _ = False + matchGroupArity :: MatchGroup id body -> Arity -- Precondition: MatchGroup is non-empty -- This is called before type checking, when mg_arg_tys is not set diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs index 9e8ea9af25..9576197b88 100644 --- a/compiler/hsSyn/HsUtils.hs +++ b/compiler/hsSyn/HsUtils.hs @@ -25,7 +25,7 @@ module HsUtils( mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo, mkHsDictLet, mkHsLams, mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo, - mkLHsPar, mkHsCmdCast, + mkLHsPar, mkHsCmdWrap, mkLHsCmdWrap, isLHsTypeExpr_maybe, isLHsTypeExpr, nlHsTyApp, nlHsTyApps, nlHsVar, nlHsLit, nlHsApp, nlHsApps, nlHsIntLit, nlHsVarApps, nlHsDo, nlHsOpApp, nlHsLam, nlHsPar, nlHsIf, nlHsCase, nlList, @@ -445,6 +445,21 @@ nlHsFunTy a b = noLoc (HsFunTy a b) nlHsTyConApp :: name -> [LHsType name] -> LHsType name nlHsTyConApp tycon tys = foldl nlHsAppTy (nlHsTyVar tycon) tys +-- | Extract a type argument from an HsExpr, with the list of wildcards in +-- the type +isLHsTypeExpr_maybe :: LHsExpr name -> Maybe (LHsWcType name) +isLHsTypeExpr_maybe (L _ (HsPar e)) = isLHsTypeExpr_maybe e +isLHsTypeExpr_maybe (L _ (HsType ty)) = Just ty + -- the HsTypeOut case is ill-typed. We never need it here anyway. +isLHsTypeExpr_maybe _ = Nothing + +-- | Is an expression a visible type application? +isLHsTypeExpr :: LHsExpr name -> Bool +isLHsTypeExpr (L _ (HsPar e)) = isLHsTypeExpr e +isLHsTypeExpr (L _ (HsType _)) = True +isLHsTypeExpr (L _ (HsTypeOut _)) = True +isLHsTypeExpr _ = False + {- Tuples. All these functions are *pre-typechecker* because they lack types on the tuple. @@ -609,9 +624,12 @@ mkHsWrapCoR co e = mkHsWrap (mkWpCastR co) e mkLHsWrapCo :: TcCoercionN -> LHsExpr id -> LHsExpr id mkLHsWrapCo co (L loc e) = L loc (mkHsWrapCo co e) -mkHsCmdCast :: TcCoercion -> HsCmd id -> HsCmd id -mkHsCmdCast co cmd | isTcReflCo co = cmd - | otherwise = HsCmdCast co cmd +mkHsCmdWrap :: HsWrapper -> HsCmd id -> HsCmd id +mkHsCmdWrap w cmd | isIdHsWrapper w = cmd + | otherwise = HsCmdWrap w cmd + +mkLHsCmdWrap :: HsWrapper -> LHsCmd id -> LHsCmd id +mkLHsCmdWrap w (L loc c) = L loc (mkHsCmdWrap w c) mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p diff --git a/compiler/hsSyn/PlaceHolder.hs b/compiler/hsSyn/PlaceHolder.hs index 8e3b9a3402..004f465d76 100644 --- a/compiler/hsSyn/PlaceHolder.hs +++ b/compiler/hsSyn/PlaceHolder.hs @@ -15,9 +15,9 @@ import RdrName import Var import Coercion import {-# SOURCE #-} ConLike (ConLike) -import TcEvidence (HsWrapper) import FieldLabel import SrcLoc (Located) +import TcEvidence ( HsWrapper ) import Data.Data hiding ( Fixity ) import BasicTypes (Fixity) @@ -65,6 +65,9 @@ placeHolderNames = PlaceHolder placeHolderNamesTc :: NameSet placeHolderNamesTc = emptyNameSet +placeHolderHsWrapper :: PlaceHolder +placeHolderHsWrapper = PlaceHolder + {- Note [Pass sensitive types] diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index 503653dd0e..6f26e231de 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -963,7 +963,7 @@ ppr_rough Nothing = dot ppr_rough (Just tc) = ppr tc tv_to_forall_bndr :: IfaceTvBndr -> IfaceForAllBndr -tv_to_forall_bndr tv = IfaceTv tv Invisible +tv_to_forall_bndr tv = IfaceTv tv Specified {- Note [Result type of a data family GADT] diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index 640d104b6a..154b7c46d8 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -696,8 +696,9 @@ pprIfaceForAll bndrs@(IfaceTv _ vis : _) (bndrs', doc) = ppr_itv_bndrs bndrs vis add_separator stuff = case vis of - Invisible -> stuff <> dot Visible -> stuff <+> arrow + _inv -> stuff <> dot + -- | Render the ... in @(forall ... .)@ or @(forall ... ->)@. -- Returns both the list of not-yet-rendered binders and the doc. @@ -705,9 +706,9 @@ pprIfaceForAll bndrs@(IfaceTv _ vis : _) ppr_itv_bndrs :: [IfaceForAllBndr] -> VisibilityFlag -- ^ visibility of the first binder in the list -> ([IfaceForAllBndr], SDoc) -ppr_itv_bndrs all_bndrs@(IfaceTv tv vis : bndrs) vis1 - | vis == vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in - (bndrs', pprIfaceTvBndr tv <+> doc) +ppr_itv_bndrs all_bndrs@(bndr@(IfaceTv _ vis) : bndrs) vis1 + | vis `sameVis` vis1 = let (bndrs', doc) = ppr_itv_bndrs bndrs vis1 in + (bndrs', pprIfaceForAllBndr bndr <+> doc) | otherwise = (all_bndrs, empty) ppr_itv_bndrs [] _ = ([], empty) @@ -719,7 +720,11 @@ pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc -pprIfaceForAllBndr (IfaceTv tv _) = pprIfaceTvBndr tv +pprIfaceForAllBndr (IfaceTv tv Invisible) = sdocWithDynFlags $ \dflags -> + if gopt Opt_PrintExplicitForalls dflags + then braces $ pprIfaceTvBndr tv + else pprIfaceTvBndr tv +pprIfaceForAllBndr (IfaceTv tv _) = pprIfaceTvBndr tv pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc pprIfaceForAllCoBndr (tv, kind_co) diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index 5efe8b3486..55260db67a 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -3210,6 +3210,7 @@ xFlags = [ flagSpec "TraditionalRecordSyntax" LangExt.TraditionalRecordSyntax, flagSpec "TransformListComp" LangExt.TransformListComp, flagSpec "TupleSections" LangExt.TupleSections, + flagSpec "TypeApplications" LangExt.TypeApplications, flagSpec "TypeInType" LangExt.TypeInType, flagSpec "TypeFamilies" LangExt.TypeFamilies, flagSpec "TypeOperators" LangExt.TypeOperators, @@ -3324,6 +3325,7 @@ impliedXFlags , (LangExt.TemplateHaskell, turnOn, LangExt.TemplateHaskellQuotes) , (LangExt.Strict, turnOn, LangExt.StrictData) + , (LangExt.TypeApplications, turnOn, LangExt.AllowAmbiguousTypes) ] -- Note [Documenting optimisation flags] diff --git a/compiler/main/PprTyThing.hs b/compiler/main/PprTyThing.hs index 365a57c7b9..d55b5083ec 100644 --- a/compiler/main/PprTyThing.hs +++ b/compiler/main/PprTyThing.hs @@ -147,18 +147,10 @@ ppr_ty_thing hdr_only path ty_thing -- Nothing is unexpected here; TyThings have External names pprTypeForUser :: Type -> SDoc --- We do two things here. --- a) We tidy the type, regardless --- b) Swizzle the foralls to the top, so that without --- -fprint-explicit-foralls we'll suppress all the foralls --- Prime example: a class op might have type --- forall a. C a => forall b. Ord b => stuff --- Then we want to display --- (C a, Ord b) => stuff +-- The type is tidied pprTypeForUser ty - = pprSigmaType (mkInvSigmaTy tvs ctxt tau) + = pprSigmaType tidy_ty where - (tvs, ctxt, tau) = tcSplitSigmaTy tidy_ty (_, tidy_ty) = tidyOpenType emptyTidyEnv ty -- Often the types/kinds we print in ghci are fully generalised -- and have no free variables, but it turns out that we sometimes diff --git a/compiler/parser/Lexer.x b/compiler/parser/Lexer.x index cee8540c09..1bbbfbf20f 100644 --- a/compiler/parser/Lexer.x +++ b/compiler/parser/Lexer.x @@ -394,6 +394,14 @@ $tab { warnTab } { lex_qquasiquote_tok } } + -- See Note [Lexing type applications] +<0> { + [^ $idchar \) ] ^ + "@" + / { ifExtension typeApplicationEnabled `alexAndPred` notFollowedBySymbol } + { token ITtypeApp } +} + <0> { "(|" / { ifExtension arrowsEnabled `alexAndPred` notFollowedBySymbol } { special IToparenbar } @@ -507,6 +515,32 @@ $tab { warnTab } \" { lex_string_tok } } +-- Note [Lexing type applications] +-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +-- The desired syntax for type applications is to prefix the type application +-- with '@', like this: +-- +-- foo @Int @Bool baz bum +-- +-- This, of course, conflicts with as-patterns. The conflict arises because +-- expressions and patterns use the same parser, and also because we want +-- to allow type patterns within expression patterns. +-- +-- Disambiguation is accomplished by requiring *something* to appear betwen +-- type application and the preceding token. This something must end with +-- a character that cannot be the end of the variable bound in an as-pattern. +-- Currently (June 2015), this means that the something cannot end with a +-- $idchar or a close-paren. (The close-paren is necessary if the as-bound +-- identifier is symbolic.) +-- +-- Note that looking for whitespace before the '@' is insufficient, because +-- of this pathological case: +-- +-- foo {- hi -}@Int +-- +-- This design is predicated on the fact that as-patterns are generally +-- whitespace-free, and also that this whole thing is opt-in, with the +-- TypeApplications extension. -- ----------------------------------------------------------------------------- -- Alex "Haskell code fragment bottom" @@ -686,8 +720,13 @@ data Token | ITLarrowtail IsUnicodeSyntax -- -<< | ITRarrowtail IsUnicodeSyntax -- >>- - | ITunknown String -- Used when the lexer can't make sense of it - | ITeof -- end of file token + -- type application '@' (lexed differently than as-pattern '@', + -- due to checking for preceding whitespace) + | ITtypeApp + + + | ITunknown String -- Used when the lexer can't make sense of it + | ITeof -- end of file token -- Documentation annotations | ITdocCommentNext String -- something beginning '-- |' @@ -2023,6 +2062,7 @@ data ExtBits | LambdaCaseBit | BinaryLiteralsBit | NegativeLiteralsBit + | TypeApplicationsBit deriving Enum @@ -2083,6 +2123,8 @@ negativeLiteralsEnabled :: ExtsBitmap -> Bool negativeLiteralsEnabled = xtest NegativeLiteralsBit patternSynonymsEnabled :: ExtsBitmap -> Bool patternSynonymsEnabled = xtest PatternSynonymsBit +typeApplicationEnabled :: ExtsBitmap -> Bool +typeApplicationEnabled = xtest TypeApplicationsBit -- PState for parsing options pragmas -- @@ -2153,6 +2195,8 @@ mkPState flags buf loc = .|. BinaryLiteralsBit `setBitIf` xopt LangExt.BinaryLiterals flags .|. NegativeLiteralsBit `setBitIf` xopt LangExt.NegativeLiterals flags .|. PatternSynonymsBit `setBitIf` xopt LangExt.PatternSynonyms flags + .|. TypeApplicationsBit `setBitIf` xopt LangExt.TypeApplications flags + -- setBitIf :: ExtBits -> Bool -> ExtsBitmap b `setBitIf` cond | cond = xbit b diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y index ead81ac337..11dc84f0a6 100644 --- a/compiler/parser/Parser.y +++ b/compiler/parser/Parser.y @@ -414,6 +414,7 @@ output it generates. '-<<' { L _ (ITLarrowtail _) } -- for arrow notation '>>-' { L _ (ITRarrowtail _) } -- for arrow notation '.' { L _ ITdot } + TYPEAPP { L _ ITtypeApp } '{' { L _ ITocurly } -- special symbols '}' { L _ ITccurly } @@ -2237,7 +2238,11 @@ fexp :: { LHsExpr RdrName } aexp :: { LHsExpr RdrName } : qvar '@' aexp {% ams (sLL $1 $> $ EAsPat $1 $3) [mj AnnAt $2] } + -- If you change the parsing, make sure to understand + -- Note [Lexing type applications] in Lexer.x + | '~' aexp {% ams (sLL $1 $> $ ELazyPat $2) [mj AnnTilde $1] } + | TYPEAPP atype {% ams (sLL $1 $> $ HsType (mkHsWildCardBndrs $2)) [mj AnnAt $1] } | aexp1 { $1 } aexp1 :: { LHsExpr RdrName } @@ -2954,6 +2959,10 @@ var :: { Located RdrName } | '(' varsym ')' {% ams (sLL $1 $> (unLoc $2)) [mop $1,mj AnnVal $2,mcp $3] } + -- Lexing type applications depends subtly on what characters can possibly + -- end a qvar. Currently (June 2015), only $idchars and ")" can end a qvar. + -- If you're changing this, please see Note [Lexing type applications] in + -- Lexer.x. qvar :: { Located RdrName } : qvarid { $1 } | '(' varsym ')' {% ams (sLL $1 $> (unLoc $2)) diff --git a/compiler/prelude/PrimOp.hs b/compiler/prelude/PrimOp.hs index 67a44cc462..66172acd24 100644 --- a/compiler/prelude/PrimOp.hs +++ b/compiler/prelude/PrimOp.hs @@ -536,7 +536,7 @@ primOpType op Compare _occ ty -> compare_fun_ty ty GenPrimOp _occ tyvars arg_tys res_ty -> - mkInvForAllTys tyvars (mkFunTys arg_tys res_ty) + mkSpecForAllTys tyvars (mkFunTys arg_tys res_ty) primOpOcc :: PrimOp -> OccName primOpOcc op = case primOpInfo op of diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs index a4715df0a6..14505850fd 100644 --- a/compiler/prelude/TysPrim.hs +++ b/compiler/prelude/TysPrim.hs @@ -648,7 +648,7 @@ mkProxyPrimTy k ty = TyConApp proxyPrimTyCon [k, ty] proxyPrimTyCon :: TyCon proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep - where kind = ForAllTy (Named kv Invisible) $ + where kind = ForAllTy (Named kv Specified) $ mkFunTy k unliftedTypeKind kv = kKiVar k = mkTyVarTy kv @@ -664,8 +664,8 @@ proxyPrimTyCon = mkPrimTyCon proxyPrimTyConName kind [Nominal,Nominal] VoidRep eqPrimTyCon :: TyCon -- The representation type for equality predicates -- See Note [The equality types story] eqPrimTyCon = mkPrimTyCon eqPrimTyConName kind roles VoidRep - where kind = ForAllTy (Named kv1 Invisible) $ - ForAllTy (Named kv2 Invisible) $ + where kind = ForAllTy (Named kv1 Specified) $ + ForAllTy (Named kv2 Specified) $ mkFunTys [k1, k2] unliftedTypeKind [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind] k1 = mkTyVarTy kv1 @@ -678,8 +678,8 @@ eqPrimTyCon = mkPrimTyCon eqPrimTyConName kind roles VoidRep eqReprPrimTyCon :: TyCon -- See Note [The equality types story] eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName kind roles VoidRep - where kind = ForAllTy (Named kv1 Invisible) $ - ForAllTy (Named kv2 Invisible) $ + where kind = ForAllTy (Named kv1 Specified) $ + ForAllTy (Named kv2 Specified) $ mkFunTys [k1, k2] unliftedTypeKind [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind] k1 = mkTyVarTy kv1 @@ -693,8 +693,8 @@ eqPhantPrimTyCon :: TyCon eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName kind [Nominal, Nominal, Phantom, Phantom] VoidRep - where kind = ForAllTy (Named kv1 Invisible) $ - ForAllTy (Named kv2 Invisible) $ + where kind = ForAllTy (Named kv1 Specified) $ + ForAllTy (Named kv2 Specified) $ mkFunTys [k1, k2] unliftedTypeKind [kv1, kv2] = mkTemplateTyVars [liftedTypeKind, liftedTypeKind] k1 = mkTyVarTy kv1 @@ -925,7 +925,7 @@ anyTyCon = mkFamilyTyCon anyTyConName kind [kKiVar] Nothing Nothing NotInjective where - kind = ForAllTy (Named kKiVar Invisible) (mkTyVarTy kKiVar) + kind = ForAllTy (Named kKiVar Specified) (mkTyVarTy kKiVar) anyTypeOfKind :: Kind -> Type anyTypeOfKind kind = TyConApp anyTyCon [kind] diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index 3c3eab66bf..02e693d5a0 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -573,7 +573,7 @@ mk_tuple boxity arity = (tycon, tuple_con) in ( UnboxedTuple , gHC_PRIM - , mkInvForAllTys lev_tvs $ + , mkSpecForAllTys lev_tvs $ mkFunTys (map tyVarKind open_tvs) $ unliftedTypeKind , arity * 2 @@ -633,7 +633,7 @@ heqSCSelId, coercibleSCSelId :: Id klass = mkClass tvs [] [sc_pred] [sc_sel_id] [] [] (mkAnd []) tycon datacon = pcDataCon heqDataConName tvs [sc_pred] tycon - kind = mkInvForAllTys [kv1, kv2] $ mkFunTys [k1, k2] constraintKind + kind = mkSpecForAllTys [kv1, kv2] $ mkFunTys [k1, k2] constraintKind kv1:kv2:_ = drop 9 alphaTyVars -- gets "j" and "k" k1 = mkTyVarTy kv1 k2 = mkTyVarTy kv2 @@ -654,7 +654,7 @@ heqSCSelId, coercibleSCSelId :: Id klass = mkClass tvs [] [sc_pred] [sc_sel_id] [] [] (mkAnd []) tycon datacon = pcDataCon coercibleDataConName tvs [sc_pred] tycon - kind = mkInvForAllTys [kKiVar] $ mkFunTys [k, k] constraintKind + kind = mkSpecForAllTys [kKiVar] $ mkFunTys [k, k] constraintKind k = mkTyVarTy kKiVar [av,bv] = mkTemplateTyVars [k, k] tvs = [kKiVar, av, bv] diff --git a/compiler/rename/RnExpr.hs b/compiler/rename/RnExpr.hs index c4e5bb2abe..03f4b62043 100644 --- a/compiler/rename/RnExpr.hs +++ b/compiler/rename/RnExpr.hs @@ -298,9 +298,9 @@ rnExpr (HsMultiIf _ty alts) -- ; return (HsMultiIf ty alts', fvs) } ; return (HsMultiIf placeHolderType alts', fvs) } -rnExpr (HsType a) - = do { (t, fvT) <- rnLHsType HsTypeCtx a - ; return (HsType t, fvT) } +rnExpr (HsType ty) + = do { (ty', fvT) <- rnHsWcType HsTypeCtx ty + ; return (HsType ty', fvT) } rnExpr (ArithSeq _ _ seq) = do { opt_OverloadedLists <- xoptM LangExt.OverloadedLists @@ -524,7 +524,7 @@ rnCmd (HsCmdDo (L l stmts) _) rnStmts ArrowExpr rnLCmd stmts (\ _ -> return ((), emptyFVs)) ; return ( HsCmdDo (L l stmts') placeHolderType, fvs ) } -rnCmd cmd@(HsCmdCast {}) = pprPanic "rnCmd" (ppr cmd) +rnCmd cmd@(HsCmdWrap {}) = pprPanic "rnCmd" (ppr cmd) --------------------------------------------------- type CmdNeeds = FreeVars -- Only inhabitants are @@ -541,7 +541,7 @@ methodNamesCmd (HsCmdArrApp _arrow _arg _ HsFirstOrderApp _rtl) methodNamesCmd (HsCmdArrApp _arrow _arg _ HsHigherOrderApp _rtl) = unitFV appAName methodNamesCmd (HsCmdArrForm {}) = emptyFVs -methodNamesCmd (HsCmdCast _ cmd) = methodNamesCmd cmd +methodNamesCmd (HsCmdWrap _ cmd) = methodNamesCmd cmd methodNamesCmd (HsCmdPar c) = methodNamesLCmd c @@ -1819,7 +1819,8 @@ sectionErr expr patSynErr :: HsExpr RdrName -> RnM (HsExpr Name, FreeVars) patSynErr e = do { addErr (sep [ptext (sLit "Pattern syntax in expression context:"), - nest 4 (ppr e)]) + nest 4 (ppr e)] $$ + text "Did you mean to enable TypeApplications?") ; return (EWildPat, emptyFVs) } badIpBinds :: Outputable a => SDoc -> a -> SDoc diff --git a/compiler/rename/RnSplice.hs b/compiler/rename/RnSplice.hs index 8f87d730d8..9ddf132311 100644 --- a/compiler/rename/RnSplice.hs +++ b/compiler/rename/RnSplice.hs @@ -45,7 +45,7 @@ import Var ( Id ) import THNames ( quoteExpName, quotePatName, quoteDecName, quoteTypeName , decsQTyConName, expQTyConName, patQTyConName, typeQTyConName, ) -import {-# SOURCE #-} TcExpr ( tcMonoExpr ) +import {-# SOURCE #-} TcExpr ( tcPolyExpr ) import {-# SOURCE #-} TcSplice ( runMetaD, runMetaE, runMetaP, runMetaT, tcTopSpliceExpr ) #endif @@ -295,7 +295,7 @@ runRnSplice flavour run_meta ppr_res splice -- Typecheck the expression ; meta_exp_ty <- tcMetaTy meta_ty_name ; zonked_q_expr <- tcTopSpliceExpr Untyped $ - tcMonoExpr the_expr meta_exp_ty + tcPolyExpr the_expr meta_exp_ty -- Run the expression ; result <- run_meta zonked_q_expr diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs index 52a164f105..5a58148170 100644 --- a/compiler/rename/RnTypes.hs +++ b/compiler/rename/RnTypes.hs @@ -751,7 +751,7 @@ checkExtraConstraintWildCard env wc = checkWildCard env mb_bad where mb_bad | not (extraConstraintWildCardsAllowed env) - = Just (ptext (sLit "Extra-contraint wildcard") <+> quotes (ppr wc) + = Just (ptext (sLit "Extra-constraint wildcard") <+> quotes (ppr wc) <+> ptext (sLit "not allowed")) | otherwise = Nothing @@ -774,6 +774,7 @@ wildCardsAllowed env RuleCtx {} -> True FamPatCtx {} -> True -- Not named wildcards though GHCiCtx {} -> True + HsTypeCtx {} -> True _ -> False rnAnonWildCard :: HsWildCardInfo RdrName -> RnM (HsWildCardInfo Name) diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs index 22f16b1f35..8878ba6b46 100644 --- a/compiler/typecheck/Inst.hs +++ b/compiler/typecheck/Inst.hs @@ -6,14 +6,15 @@ The @Inst@ type: dictionaries or method instances -} -{-# LANGUAGE CPP, MultiWayIf #-} +{-# LANGUAGE CPP, MultiWayIf, TupleSections #-} module Inst ( - deeplySkolemise, deeplyInstantiate, + deeplySkolemise, + topInstantiate, topInstantiateInferred, deeplyInstantiate, instCall, instDFunType, instStupidTheta, newWanted, newWanteds, - newOverloadedLit, mkOverLit, + newOverloadedLit, newNonTrivialOverloadedLit, mkOverLit, newClsInst, tcGetInsts, tcGetInstEnvs, getOverlapFlag, @@ -149,6 +150,65 @@ deeplySkolemise ty | otherwise = return (idHsWrapper, [], [], ty) +-- | Instantiate all outer type variables +-- and any context. Never looks through arrows. +topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) +-- if topInstantiate ty = (wrap, rho) +-- and e :: ty +-- then wrap e :: rho +topInstantiate = top_instantiate True + +-- | Instantiate all outer 'Invisible' binders +-- and any context. Never looks through arrows or specified type variables. +-- Used for visible type application. +topInstantiateInferred :: CtOrigin -> TcSigmaType + -> TcM (HsWrapper, TcSigmaType) +-- if topInstantiate ty = (wrap, rho) +-- and e :: ty +-- then wrap e :: rho +topInstantiateInferred = top_instantiate False + +top_instantiate :: Bool -- True <=> instantiate *all* variables + -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) +top_instantiate inst_all orig ty + | not (null binders && null theta) + = do { let (inst_bndrs, leave_bndrs) = span should_inst binders + (inst_theta, leave_theta) + | null leave_bndrs = (theta, []) + | otherwise = ([], theta) + ; (subst, inst_tvs') <- newMetaTyVars (map (binderVar "top_inst") inst_bndrs) + ; let inst_theta' = substTheta subst inst_theta + sigma' = substTy subst (mkForAllTys leave_bndrs $ + mkFunTys leave_theta rho) + + ; wrap1 <- instCall orig (mkTyVarTys inst_tvs') inst_theta' + ; traceTc "Instantiating" + (vcat [ text "all tyvars?" <+> ppr inst_all + , text "origin" <+> pprCtOrigin orig + , text "type" <+> ppr ty + , text "with" <+> ppr inst_tvs' + , text "theta:" <+> ppr inst_theta' ]) + + ; (wrap2, rho2) <- + if null leave_bndrs + + -- account for types like forall a. Num a => forall b. Ord b => ... + then top_instantiate inst_all orig sigma' + + -- but don't loop if there were any un-inst'able tyvars + else return (idHsWrapper, sigma') + + ; return (wrap2 <.> wrap1, rho2) } + + | otherwise = return (idHsWrapper, ty) + where + (binders, phi) = tcSplitNamedPiTys ty + (theta, rho) = tcSplitPhiTy phi + + should_inst bndr + | inst_all = True + | otherwise = binderVisibility bndr == Invisible + deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType) -- Int -> forall a. a -> a ==> (\x:Int. [] x alpha) :: Int -> alpha -- In general if @@ -176,6 +236,7 @@ deeplyInstantiate orig ty | otherwise = return (idHsWrapper, ty) + {- ************************************************************************ * * @@ -269,39 +330,54 @@ instStupidTheta orig theta * * ************************************************************************ +-} + +{- In newOverloadedLit we convert directly to an Int or Integer if we know that's what we want. This may save some time, by not temporarily generating overloaded literals, but it won't catch all cases (the rest are caught in lookupInst). --} -newOverloadedLit :: CtOrigin - -> HsOverLit Name - -> TcRhoType - -> TcM (HsOverLit TcId) -newOverloadedLit orig lit res_ty - = do dflags <- getDynFlags - newOverloadedLit' dflags orig lit res_ty - -newOverloadedLit' :: DynFlags - -> CtOrigin - -> HsOverLit Name - -> TcRhoType - -> TcM (HsOverLit TcId) -newOverloadedLit' dflags orig - lit@(OverLit { ol_val = val, ol_rebindable = rebindable - , ol_witness = meth_name }) res_ty +-} +newOverloadedLit :: HsOverLit Name + -> TcSigmaType -- if nec'y, this type is instantiated... + -> CtOrigin -- ... using this CtOrigin + -> TcM (HsWrapper, HsOverLit TcId) + -- wrapper :: input type "->" type of result +newOverloadedLit + lit@(OverLit { ol_val = val, ol_rebindable = rebindable }) res_ty res_orig | not rebindable - , Just expr <- shortCutLit dflags val res_ty + -- all built-in overloaded lits are not higher-rank, so skolemise. + -- this is necessary for shortCutLit. + = do { (wrap, insted_ty) <- deeplyInstantiate res_orig res_ty + ; dflags <- getDynFlags + ; case shortCutLit dflags val insted_ty of -- Do not generate a LitInst for rebindable syntax. -- Reason: If we do, tcSimplify will call lookupInst, which -- will call tcSyntaxName, which does unification, -- which tcSimplify doesn't like - = return (lit { ol_witness = expr, ol_type = res_ty - , ol_rebindable = rebindable }) + Just expr -> return ( wrap + , lit { ol_witness = expr, ol_type = insted_ty + , ol_rebindable = False } ) + Nothing -> (wrap, ) <$> + newNonTrivialOverloadedLit orig lit insted_ty } | otherwise + = do { lit' <- newNonTrivialOverloadedLit orig lit res_ty + ; return (idHsWrapper, lit') } + where + orig = LiteralOrigin lit + +-- Does not handle things that 'shortCutLit' can handle. See also +-- newOverloadedLit in TcUnify +newNonTrivialOverloadedLit :: CtOrigin + -> HsOverLit Name + -> TcSigmaType + -> TcM (HsOverLit TcId) +newNonTrivialOverloadedLit orig + lit@(OverLit { ol_val = val, ol_witness = meth_name + , ol_rebindable = rebindable }) res_ty = do { hs_lit <- mkOverLit val ; let lit_ty = hsLitType hs_lit ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty) @@ -310,8 +386,8 @@ newOverloadedLit' dflags orig -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2 -- However this'll be picked up by tcSyntaxOp if necessary ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit)) - ; return (lit { ol_witness = witness, ol_type = res_ty - , ol_rebindable = rebindable }) } + ; return (lit { ol_witness = witness, ol_type = res_ty, + ol_rebindable = rebindable }) } ------------ mkOverLit :: OverLitVal -> TcM HsLit diff --git a/compiler/typecheck/TcArrows.hs b/compiler/typecheck/TcArrows.hs index 444b148fbc..dac6aedadf 100644 --- a/compiler/typecheck/TcArrows.hs +++ b/compiler/typecheck/TcArrows.hs @@ -5,7 +5,7 @@ Typecheck arrow notation -} -{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RankNTypes, TupleSections #-} module TcArrows ( tcProc ) where @@ -250,7 +250,7 @@ tc_cmd env arg_tys = map hsLPatType pats' cmd' = HsCmdLam (MG { mg_alts = L l [match'], mg_arg_tys = arg_tys , mg_res_ty = res_ty, mg_origin = origin }) - ; return (mkHsCmdCast co cmd') } + ; return (mkHsCmdWrap (mkWpCastN co) cmd') } where n_pats = length pats match_ctxt = (LambdaExpr :: HsMatchContext Name) -- Maybe KappaExpr? @@ -272,7 +272,7 @@ tc_cmd env tc_cmd env (HsCmdDo (L l stmts) _) (cmd_stk, res_ty) = do { co <- unifyType noThing unitTy cmd_stk -- Expecting empty argument stack ; stmts' <- tcStmts ArrowExpr (tcArrDoStmt env) stmts res_ty - ; return (mkHsCmdCast co (HsCmdDo (L l stmts') res_ty)) } + ; return (mkHsCmdWrap (mkWpCastN co) (HsCmdDo (L l stmts') res_ty)) } ----------------------------------------------------------------- diff --git a/compiler/typecheck/TcBinds.hs b/compiler/typecheck/TcBinds.hs index 83f2eb98b1..113a5613c3 100644 --- a/compiler/typecheck/TcBinds.hs +++ b/compiler/typecheck/TcBinds.hs @@ -15,7 +15,7 @@ module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds, TcPragEnv, mkPragEnv, tcUserTypeSig, instTcTySig, chooseInferredQuantifiers, instTcTySigFromId, tcExtendTyVarEnvFromSig, - badBootDeclErr, mkExport ) where + badBootDeclErr ) where import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun ) import {-# SOURCE #-} TcExpr ( tcMonoExpr ) @@ -32,7 +32,7 @@ import TcEvidence import TcHsType import TcPat import TcMType -import Inst( deeplyInstantiate ) +import Inst( topInstantiate, deeplyInstantiate ) import FamInstEnv( normaliseType ) import FamInst( tcGetFamInstEnvs ) import TyCon @@ -556,7 +556,7 @@ tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list ; mono_ids' <- mapM tc_mono_info mono_infos ; return (binds', mono_ids') } where - tc_mono_info (name, _, mono_id) + tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id }) = do { mono_ty' <- zonkTcType (idType mono_id) -- Zonk, mainly to expose unboxed types to checkStrictBinds ; let mono_id' = setIdType mono_id mono_ty' @@ -601,11 +601,11 @@ tcPolyCheck rec_tc prag_fn ; spec_prags <- tcSpecPrags poly_id prag_sigs ; poly_id <- addInlinePrags poly_id prag_sigs - ; let (_, _, mono_id) = mono_info - export = ABE { abe_wrap = idHsWrapper - , abe_poly = poly_id - , abe_mono = mono_id - , abe_prags = SpecPrags spec_prags } + ; let export = ABE { abe_wrap = idHsWrapper + , abe_inst_wrap = idHsWrapper + , abe_poly = poly_id + , abe_mono = mbi_mono_id mono_info + , abe_prags = SpecPrags spec_prags } abs_bind = L loc $ AbsBinds { abs_tvs = skol_tvs , abs_ev_vars = ev_vars, abs_ev_binds = [ev_binds] @@ -616,6 +616,54 @@ tcPolyCheck _rec_tc _prag_fn sig _bind = pprPanic "tcPolyCheck" (ppr sig) ------------------ +{- +Note [Instantiate when inferring a type] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + f = (*) +As there is no incentive to instantiate the RHS, tcMonoBinds will +produce a type of forall a. Num a => a -> a -> a for `f`. This will then go +through simplifyInfer and such, remaining unchanged. + +There are two problems with this: + 1) If the definition were `g _ = (*)`, we get a very unusual type of + `forall {a}. a -> forall b. Num b => b -> b -> b` for `g`. This is + surely confusing for users. + + 2) The monomorphism restriction can't work. The MR is dealt with in + simplifyInfer, and simplifyInfer has no way of instantiating. This + could perhaps be worked around, but it may be hard to know even + when instantiation should happen. + +There is an easy solution to all three problems: instantiate (deeply) when +inferring a type. So that's what we do. Note that this decision is +user-facing. + +Here are the details: + * tcMonoBinds produces the "monomorphic" ids to be put in the AbsBinds. + It is inconvenient to instantiate in this function or below. So the + monomorphic ids will be uninstantiated (and hence actually polymorphic, + but that doesn't ruin anyone's day). + + * In the same captureConstraints as the tcMonoBinds, we instantiate all + the types of the monomorphic ids. Instantiating will produce constraints + to solve and instantiated types. These constraints and the instantiated + types go into simplifyInfer. HsWrappers are produced that go from + the "mono" types to the instantiated ones. + + * simplifyInfer does its magic, figuring out how to regeneralize. + + * mkExport then does the impedence matching and needs to connect the + monomorphic ids to the polymorphic types as decided by simplifyInfer. + Because the instantiation happens before simplifyInfer, we also pass in + the HsWrappers obtained via instantiating so that mkExport can connect + all the pieces. + + * We produce an AbsBinds with the right (instantiated and then, perhaps, + regeneralized) polytypes and the not-yet-instantiated "monomorphic" ids, + using the built HsWrappers to connect. Done! +-} + tcPolyInfer :: RecFlag -- Whether it's recursive after breaking -- dependencies based on type signatures @@ -624,19 +672,36 @@ tcPolyInfer -> [LHsBind Name] -> TcM (LHsBinds TcId, [TcId]) tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list - = do { (tclvl, wanted, (binds', mono_infos)) + = do { (tclvl, wanted, (binds', mono_infos, wrappers, insted_tys)) <- pushLevelAndCaptureConstraints $ - tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list + do { (binds', mono_infos) + <- tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list + -- See Note [Instantiate when inferring a type] + ; traceTc "Note [Instantiate when inferring a type]" $ + vcat (map (pprBndr LetBind . mbi_mono_id) mono_infos) + ; (wrappers, insted_tys) + <- tcExtendIdBndrs + [ TcIdBndr mono_id NotTopLevel + | MBI { mbi_mono_id = mono_id } <- mono_infos ] $ + mapAndUnzipM deeply_instantiate mono_infos + -- during instantiation, we might encounter an error + -- whose message will want to list these binders as + -- relevant. + + ; return (binds', mono_infos, wrappers, insted_tys) } + + ; let name_taus = [ (mbi_poly_name info, tau) + | (info, tau) <- zip mono_infos insted_tys] + sigs = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ] - ; let name_taus = [(name, idType mono_id) | (name, _, mono_id) <- mono_infos] - sigs = [ sig | (_, Just sig, _) <- mono_infos ] ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted) ; (qtvs, givens, ev_binds) <- simplifyInfer tclvl mono sigs name_taus wanted ; let inferred_theta = map evVarPred givens ; exports <- checkNoErrs $ - mapM (mkExport prag_fn qtvs inferred_theta) mono_infos + zipWith3M (mkExport prag_fn qtvs inferred_theta) + mono_infos wrappers insted_tys ; loc <- getSrcSpanM ; let poly_ids = map abe_poly exports @@ -649,12 +714,23 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list ; return (unitBag abs_bind, poly_ids) } -- poly_ids are guaranteed zonked by mkExport + where + deeply_instantiate :: MonoBindInfo -> TcM (HsWrapper, TcRhoType) + deeply_instantiate (MBI { mbi_mono_id = mono_id, mbi_orig = orig }) + = do { mono_ty <- zonkTcType (idType mono_id) + -- NB: zonk to uncover any foralls + ; addErrCtxtM (instErrCtxt mono_id mono_ty) $ + deeplyInstantiate orig mono_ty } + -------------- mkExport :: TcPragEnv -> [TyVar] -> TcThetaType -- Both already zonked -> MonoBindInfo + -> HsWrapper -- the instantiation wrapper; + -- see Note [Instantiate when inferring a type] + -> TcTauType -- the instantiated type -> TcM (ABExport Id) --- Only called for generalisation plan IferGen, not by CheckGen or NoGen +-- Only called for generalisation plan InferGen, not by CheckGen or NoGen -- -- mkExport generates exports with -- zonked type variables, @@ -667,14 +743,19 @@ mkExport :: TcPragEnv -- Pre-condition: the qtvs and theta are already zonked -mkExport prag_fn qtvs theta mono_info@(poly_name, mb_sig, mono_id) - = do { mono_ty <- zonkTcType (idType mono_id) +mkExport prag_fn qtvs theta + mono_info@(MBI { mbi_poly_name = poly_name + , mbi_sig = mb_sig + , mbi_mono_id = mono_id }) + inst_wrap inst_ty + = do { inst_ty <- zonkTcType inst_ty + ; poly_id <- case mb_sig of Just sig | Just poly_id <- completeIdSigPolyId_maybe sig -> return poly_id _other -> checkNoErrs $ mkInferredPolyId qtvs theta - poly_name mb_sig mono_ty + poly_name mb_sig inst_ty -- The checkNoErrs ensures that if the type is ambiguous -- we don't carry on to the impedence matching, and generate -- a duplicate ambiguity error. There is a similar @@ -688,9 +769,12 @@ mkExport prag_fn qtvs theta mono_info@(poly_name, mb_sig, mono_id) -- See Note [Impedence matching] -- NB: we have already done checkValidType, including an ambiguity check, -- on the type; either when we checked the sig or in mkInferredPolyId - ; let sel_poly_ty = mkInvSigmaTy qtvs theta mono_ty + ; let sel_poly_ty = mkInvSigmaTy qtvs theta inst_ty + -- this type is just going into tcSubType, so Inv vs. Spec doesn't + -- matter + poly_ty = idType poly_id - ; wrap <- if sel_poly_ty `eqType` poly_ty + ; wrap <- if sel_poly_ty `eqType` poly_ty -- NB: eqType ignores visibility then return idHsWrapper -- Fast path; also avoids complaint when we infer -- an ambiguouse type and have AllowAmbiguousType -- e..g infer x :: forall a. F a -> Int @@ -701,7 +785,8 @@ mkExport prag_fn qtvs theta mono_info@(poly_name, mb_sig, mono_id) ; when warn_missing_sigs $ localSigWarn poly_id mb_sig ; return (ABE { abe_wrap = wrap - -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => mono_ty) + -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => inst_ty) + , abe_inst_wrap = inst_wrap , abe_poly = poly_id , abe_mono = mono_id , abe_prags = SpecPrags spec_prags}) } @@ -724,13 +809,12 @@ mkInferredPolyId qtvs inferred_theta poly_name mb_sig mono_ty -- We can discard the coercion _co, because we'll reconstruct -- it in the call to tcSubType below - ; (my_tvs, theta') <- chooseInferredQuantifiers - inferred_theta (tyCoVarsOfType mono_ty') mb_sig + ; (binders, theta') <- chooseInferredQuantifiers inferred_theta + (tyCoVarsOfType mono_ty') qtvs mb_sig - ; let qtvs' = filter (`elemVarSet` my_tvs) qtvs -- Maintain original order - inferred_poly_ty = mkInvSigmaTy qtvs' theta' mono_ty' + ; let inferred_poly_ty = mkForAllTys binders (mkPhiTy theta' mono_ty') - ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr my_tvs, ppr theta' + ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta' , ppr inferred_poly_ty]) ; addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $ checkValidType (InfSigCtxt poly_name) inferred_poly_ty @@ -739,25 +823,32 @@ mkInferredPolyId qtvs inferred_theta poly_name mb_sig mono_ty ; return (mkLocalIdOrCoVar poly_name inferred_poly_ty) } -chooseInferredQuantifiers :: TcThetaType -> TcTyVarSet -> Maybe TcIdSigInfo - -> TcM (TcTyVarSet, TcThetaType) -chooseInferredQuantifiers inferred_theta tau_tvs Nothing +chooseInferredQuantifiers :: TcThetaType -- inferred + -> TcTyVarSet -- tvs free in tau type + -> [TcTyVar] -- inferred quantified tvs + -> Maybe TcIdSigInfo + -> TcM ([TcTyBinder], TcThetaType) +chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs) -- Include kind variables! Trac #7916 my_theta = pickQuantifiablePreds free_tvs inferred_theta - ; return (free_tvs, my_theta) } + binders = [ mkNamedBinder tv Invisible + | tv <- qtvs + , tv `elemVarSet` free_tvs ] + ; return (binders, my_theta) } -chooseInferredQuantifiers inferred_theta tau_tvs +chooseInferredQuantifiers inferred_theta tau_tvs qtvs (Just (TISI { sig_bndr = bndr_info , sig_ctxt = ctxt - , sig_theta = annotated_theta })) + , sig_theta = annotated_theta + , sig_skols = annotated_tvs })) | PartialSig { sig_cts = extra } <- bndr_info , Nothing <- extra = do { annotated_theta <- zonkTcTypes annotated_theta ; let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta `unionVarSet` tau_tvs) ; traceTc "ciq" (vcat [ ppr bndr_info, ppr annotated_theta, ppr free_tvs]) - ; return (free_tvs, annotated_theta) } + ; return (mk_binders free_tvs, annotated_theta) } | PartialSig { sig_cts = extra } <- bndr_info , Just loc <- extra @@ -786,7 +877,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs | otherwise -> return () False -> reportError msg - ; return (free_tvs, final_theta) } + ; return (mk_binders free_tvs, final_theta) } | otherwise = pprPanic "chooseInferredQuantifiers" (ppr bndr_info) @@ -798,12 +889,21 @@ chooseInferredQuantifiers inferred_theta tau_tvs , if suppress_hint then empty else pts_hint , typeSigCtxt ctxt bndr_info ] + spec_tv_set = mkVarSet $ map snd annotated_tvs + mk_binders free_tvs + = [ mkNamedBinder tv vis + | tv <- qtvs + , tv `elemVarSet` free_tvs + , let vis | tv `elemVarSet` spec_tv_set = Specified + | otherwise = Invisible ] + -- Pulling from qtvs maintains original order mk_impedence_match_msg :: MonoBindInfo -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) -- This is a rare but rather awkward error messages -mk_impedence_match_msg (name, mb_sig, _) inf_ty sig_ty tidy_env +mk_impedence_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig }) + inf_ty sig_ty tidy_env = do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env inf_ty ; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty ; let msg = vcat [ ptext (sLit "When checking that the inferred type") @@ -911,14 +1011,13 @@ We can get these by "impedance matching": Suppose the shared quantified tyvars are qtvs and constraints theta. Then we want to check that - f's final inferred polytype is more polymorphic than - forall qtvs. theta => f_mono_ty + forall qtvs. theta => f_mono_ty is more polymorphic than f's polytype and the proof is the impedance matcher. Notice that the impedance matcher may do defaulting. See Trac #7173. It also cleverly does an ambiguity check; for example, rejecting - f :: F a -> a + f :: F a -> F a where F is a non-injective type function. -} @@ -940,7 +1039,7 @@ recoveryCode binder_names sig_fn = mkLocalId name forall_a_a forall_a_a :: TcType -forall_a_a = mkInvForAllTys [levity1TyVar, openAlphaTyVar] openAlphaTy +forall_a_a = mkSpecForAllTys [levity1TyVar, openAlphaTyVar] openAlphaTy {- ********************************************************************* * * @@ -952,13 +1051,13 @@ Note [Handling SPECIALISE pragmas] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The basic idea is this: - f:: Num a => a -> b -> a + foo :: Num a => a -> b -> a {-# SPECIALISE foo :: Int -> b -> Int #-} We check that - (forall a. Num a => a -> a) + (forall a b. Num a => a -> b -> a) is more polymorphic than - Int -> Int + forall b. Int -> b -> Int (for which we could use tcSubType, but see below), generating a HsWrapper to connect the two, something like wrap = /\b. <hole> Int b dNumInt @@ -1009,8 +1108,8 @@ 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 deeplySkolemise / - deeplyInstantiate in tcSpecWrapper. (Actually I think that even + 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.) @@ -1142,8 +1241,8 @@ tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper -- See Note [Handling SPECIALISE pragmas], wrinkle 1 tcSpecWrapper ctxt poly_ty spec_ty = do { (sk_wrap, inst_wrap) - <- tcGen ctxt spec_ty $ \ _ spec_tau -> - do { (inst_wrap, tau) <- deeplyInstantiate orig poly_ty + <- tcSkolemise ctxt spec_ty $ \ _ spec_tau -> + do { (inst_wrap, tau) <- topInstantiate orig poly_ty ; _ <- unifyType noThing spec_tau tau -- Deliberately ignore the evidence -- See Note [Handling SPECIALISE pragmas], @@ -1377,24 +1476,31 @@ tcMonoBinds is_rec sig_fn no_gen -- use ReturnTv to allow impredicativity ; let rhs_ty = mkTyVarTy rhs_tv ; mono_id <- newNoSigLetBndr no_gen name rhs_ty - ; (co_fn, matches') <- tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel] $ - -- We extend the error context even for a non-recursive - -- function so that in type error messages we show the - -- type of the thing whose rhs we are type checking - tcMatchesFun name matches rhs_ty + ; (co_fn, matches') + <- tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel] $ + -- We extend the error context even for a non-recursive + -- function so that in type error messages we show the + -- type of the thing whose rhs we are type checking + tcMatchesFun name matches rhs_ty ; return (unitBag $ L b_loc $ FunBind { fun_id = L nm_loc mono_id, fun_matches = matches', bind_fvs = fvs, fun_co_fn = co_fn, fun_tick = [] }, - [(name, Nothing, mono_id)]) } + [MBI { mbi_poly_name = name + , mbi_sig = Nothing + , mbi_mono_id = mono_id + , mbi_orig = matchesCtOrigin matches }]) } tcMonoBinds _ sig_fn no_gen binds = do { tc_binds <- mapM (wrapLocM (tcLhs sig_fn no_gen)) binds -- Bring the monomorphic Ids, into scope for the RHSs ; let mono_info = getMonoBindInfo tc_binds - rhs_id_env = [(name, mono_id) | (name, mb_sig, mono_id) <- mono_info + rhs_id_env = [(name, mono_id) | MBI { mbi_poly_name = name + , mbi_sig = mb_sig + , mbi_mono_id = mono_id } + <- mono_info , case mb_sig of Just sig -> isPartialSig sig Nothing -> True ] @@ -1403,9 +1509,9 @@ tcMonoBinds _ sig_fn no_gen binds ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id) | (n,id) <- rhs_id_env] - ; binds' <- tcExtendLetEnvIds NotTopLevel rhs_id_env $ - mapM (wrapLocM tcRhs) tc_binds - ; return (listToBag binds', mono_info) } + ; (binds', mono_infos') <- tcExtendLetEnvIds NotTopLevel rhs_id_env $ + mapAndUnzipM (wrapLocFstM tcRhs) tc_binds + ; return (listToBag binds', concat mono_infos') } ------------------------ -- tcLhs typechecks the LHS of the bindings, to construct the environment in which @@ -1427,9 +1533,11 @@ data TcMonoBind -- Half completed; LHS done, RHS not done = TcFunBind MonoBindInfo SrcSpan (MatchGroup Name (LHsExpr Name)) | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name (LHsExpr Name)) TcSigmaType -type MonoBindInfo = (Name, Maybe TcIdSigInfo, TcId) - -- Type signature (if any), and - -- the monomorphic bound things +data MonoBindInfo = MBI { mbi_poly_name :: Name + , mbi_sig :: Maybe TcIdSigInfo + , mbi_mono_id :: TcId + , mbi_orig :: CtOrigin } + -- origin associated with RHS tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches }) @@ -1443,12 +1551,22 @@ tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches }) -- Both InferGen and CheckGen gives rise to LetLclBndr do { mono_name <- newLocalName name ; let mono_id = mkLocalIdOrCoVar mono_name tau - ; return (TcFunBind (name, Just sig, mono_id) nm_loc matches) } + ; return (TcFunBind (MBI { mbi_poly_name = name + , mbi_sig = Just sig + , mbi_mono_id = mono_id + , mbi_orig = + Shouldn'tHappenOrigin "FunBind sig" }) + nm_loc matches) } | otherwise = do { mono_ty <- newOpenFlexiTyVarTy ; mono_id <- newNoSigLetBndr no_gen name mono_ty - ; return (TcFunBind (name, Nothing, mono_id) nm_loc matches) } + ; return (TcFunBind (MBI { mbi_poly_name = name + , mbi_sig = Nothing + , mbi_mono_id = mono_id + , mbi_orig = + Shouldn'tHappenOrigin "FunBind nosig" }) + nm_loc matches) } tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss }) = do { let tc_pat exp_ty = tcLetPat sig_fn no_gen pat exp_ty $ @@ -1458,11 +1576,15 @@ tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss }) -- names, which the pattern has brought into scope. lookup_info :: Name -> TcM MonoBindInfo lookup_info name - = do { mono_id <- tcLookupId name - ; let mb_sig = case sig_fn name of - Just (TcIdSig sig) -> Just sig - _ -> Nothing - ; return (name, mb_sig, mono_id) } + = do { mono_id <- tcLookupId name + ; let mb_sig = case sig_fn name of + Just (TcIdSig sig) -> Just sig + _ -> Nothing + ; return (MBI { mbi_poly_name = name + , mbi_sig = mb_sig + , mbi_mono_id = mono_id + , mbi_orig = + Shouldn'tHappenOrigin "PatBind" }) } ; ((pat', infos), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $ tcInfer tc_pat @@ -1473,18 +1595,20 @@ tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind) -- AbsBind, VarBind impossible ------------------- -tcRhs :: TcMonoBind -> TcM (HsBind TcId) -tcRhs (TcFunBind info@(_, mb_sig, mono_id) loc matches) +tcRhs :: TcMonoBind -> TcM (HsBind TcId, [MonoBindInfo]) -- fills in the mbi_orig +tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id }) + loc matches) = tcExtendIdBinderStackForRhs [info] $ tcExtendTyVarEnvForRhs mb_sig $ do { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id)) ; (co_fn, matches') <- tcMatchesFun (idName mono_id) - matches (idType mono_id) - ; return (FunBind { fun_id = L loc mono_id - , fun_matches = matches' - , fun_co_fn = co_fn - , bind_fvs = placeHolderNamesTc - , fun_tick = [] }) } + matches (idType mono_id) + ; return ( FunBind { fun_id = L loc mono_id + , fun_matches = matches' + , fun_co_fn = co_fn + , bind_fvs = placeHolderNamesTc + , fun_tick = [] } + , [info { mbi_orig = matchesCtOrigin matches }] ) } -- TODO: emit Hole Constraints for wildcards tcRhs (TcPatBind infos pat' grhss pat_ty) @@ -1496,9 +1620,13 @@ tcRhs (TcPatBind infos pat' grhss pat_ty) do { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty) ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $ tcGRHSsPat grhss pat_ty - ; return (PatBind { pat_lhs = pat', pat_rhs = grhss', pat_rhs_ty = pat_ty - , bind_fvs = placeHolderNamesTc - , pat_ticks = ([],[]) }) } + ; let orig = grhssCtOrigin grhss + infos' = [ info { mbi_orig = orig } | info <- infos ] + ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss' + , pat_rhs_ty = pat_ty + , bind_fvs = placeHolderNamesTc + , pat_ticks = ([],[]) } + , infos' ) } tcExtendTyVarEnvForRhs :: Maybe TcIdSigInfo -> TcM a -> TcM a tcExtendTyVarEnvForRhs Nothing thing_inside @@ -1531,7 +1659,9 @@ tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a -- If we had the *polymorphic* version of f in the TcIdBinderStack, it -- would not be reported as relevant, because its type is closed tcExtendIdBinderStackForRhs infos thing_inside - = tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel | (_, _, mono_id) <- infos] thing_inside + = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel + | MBI { mbi_mono_id = mono_id } <- infos ] + thing_inside -- NotTopLevel: it's a monomorphic binding --------------------- @@ -1998,3 +2128,17 @@ typeSigCtxt ctxt (PartialSig { sig_hs_ty = hs_ty }) = pprSigCtxt ctxt empty (ppr hs_ty) typeSigCtxt ctxt (CompleteSig id) = pprSigCtxt ctxt empty (ppr (idType id)) + +instErrCtxt :: TcId -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc) +instErrCtxt id ty env + = do { let (env', ty') = tidyOpenType env ty + ; return (env', hang (text "When instantiating" <+> quotes (ppr id) <> + text ", initially inferred to have" $$ + text "this overly-general type:") + 2 (ppr ty') $$ + extra) } + where + extra = sdocWithDynFlags $ \dflags -> + ppWhen (xopt LangExt.MonomorphismRestriction dflags) $ + text "NB: This instantiation can be caused by the" <+> + text "monomorphism restriction." diff --git a/compiler/typecheck/TcClassDcl.hs b/compiler/typecheck/TcClassDcl.hs index 64bf2d5fe6..6411fa980d 100644 --- a/compiler/typecheck/TcClassDcl.hs +++ b/compiler/typecheck/TcClassDcl.hs @@ -247,13 +247,14 @@ tcDefMeth clas tyvars this_dict binds_in hs_sig_fn prag_fn tcPolyCheck NonRecursive no_prag_fn local_dm_sig (L bind_loc lm_bind) - ; let export = ABE { abe_poly = global_dm_id + ; let export = ABE { abe_poly = global_dm_id -- We have created a complete type signature in -- instTcTySig, hence it is safe to call -- completeSigPolyId - , abe_mono = completeIdSigPolyId local_dm_sig - , abe_wrap = idHsWrapper - , abe_prags = IsDefaultMethod } + , abe_mono = completeIdSigPolyId local_dm_sig + , abe_wrap = idHsWrapper + , abe_inst_wrap = idHsWrapper + , abe_prags = IsDefaultMethod } full_bind = AbsBinds { abs_tvs = tyvars , abs_ev_vars = [this_dict] , abs_exports = [export] diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs index b54d5f5d6c..d480dee9c3 100644 --- a/compiler/typecheck/TcErrors.hs +++ b/compiler/typecheck/TcErrors.hs @@ -1239,7 +1239,8 @@ mkEqInfoMsg ct ty1 ty2 = snd (mkAmbigMsg False ct) | otherwise = empty - invis_msg | Just Invisible <- tcEqTypeVis ty1 ty2 + invis_msg | Just vis <- tcEqTypeVis ty1 ty2 + , vis /= Visible = sdocWithDynFlags $ \dflags -> if gopt Opt_PrintExplicitKinds dflags then text "Use -fprint-explicit-kinds to see the kind arguments" @@ -2111,7 +2112,7 @@ pprSkol implics tv = case skol_info of UnkSkol -> pp_tv <+> ptext (sLit "is an unknown type variable") SigSkol ctxt ty -> ppr_rigid (pprSigSkolInfo ctxt - (mkInvForAllTys skol_tvs ty)) + (mkSpecForAllTys skol_tvs ty)) _ -> ppr_rigid (pprSkolInfo skol_info) where pp_tv = quotes (ppr tv) @@ -2167,7 +2168,8 @@ relevantBindings want_filtering ctxt ct vcat [ ppr ct , pprCtOrigin (ctLocOrigin loc) , ppr ct_tvs - , ppr [id | TcIdBndr id _ <- tcl_bndrs lcl_env] ] + , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id) + | TcIdBndr id _ <- tcl_bndrs lcl_env ] ] ; (tidy_env', docs, discards) <- go env1 ct_tvs (maxRelevantBinds dflags) diff --git a/compiler/typecheck/TcEvidence.hs b/compiler/typecheck/TcEvidence.hs index 78901156e4..184aa16334 100644 --- a/compiler/typecheck/TcEvidence.hs +++ b/compiler/typecheck/TcEvidence.hs @@ -8,7 +8,8 @@ module TcEvidence ( HsWrapper(..), (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, - mkWpFun, idHsWrapper, isIdHsWrapper, pprHsWrapper, + mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper, + symWrapper_maybe, -- Evidence bindings TcEvBinds(..), EvBindsVar(..), @@ -63,6 +64,10 @@ import FastString import SrcLoc import Data.IORef( IORef ) +#if __GLASGOW_HASKELL__ < 709 +import Control.Applicative ( (<*>), (<$>) ) +#endif + {- Note [TcCoercions] ~~~~~~~~~~~~~~~~~~ @@ -161,13 +166,14 @@ data HsWrapper -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. []) -- But ([] a) `WpCompose` ([] b) = ([] b a) - | WpFun HsWrapper HsWrapper TcType TcType - -- (WpFun wrap1 wrap2 t1 t2)[e] = \(x:t1). wrap2[ e wrap1[x] ] :: t2 + | WpFun HsWrapper HsWrapper TcType + -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ] -- So note that if wrap1 :: exp_arg <= act_arg -- wrap2 :: act_res <= exp_res -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res) -- This isn't the same as for mkFunCo, but it has to be this way -- because we can't use 'sym' to flip around these HsWrappers + -- The TcType is the "from" type of the first wrapper | WpCast TcCoercionR -- A cast: [] `cast` co -- Guaranteed not the identity coercion @@ -192,12 +198,26 @@ WpHole <.> c = c c <.> WpHole = c c1 <.> c2 = c1 `WpCompose` c2 -mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper +mkWpFun :: HsWrapper -> HsWrapper + -> TcType -- the "from" type of the first wrapper + -> TcType -- either type of the second wrapper (used only when the + -- second wrapper is the identity) + -> HsWrapper + -- NB: These optimisations are important, because we need + -- symWrapper_maybe to work in TcUnify.matchExpectedFunTys + -- See that function for more info. mkWpFun WpHole WpHole _ _ = WpHole -mkWpFun WpHole (WpCast co2) t1 _ = WpCast (mkFunCo Representational (mkRepReflCo t1) co2) -mkWpFun (WpCast co1) WpHole _ t2 = WpCast (mkFunCo Representational (mkSymCo co1) (mkRepReflCo t2)) -mkWpFun (WpCast co1) (WpCast co2) _ _ = WpCast (mkFunCo Representational (mkSymCo co1) co2) -mkWpFun co1 co2 t1 t2 = WpFun co1 co2 t1 t2 +mkWpFun WpHole (WpCast co2) t1 _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2) +mkWpFun (WpCast co1) WpHole _ t2 = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2)) +mkWpFun (WpCast co1) (WpCast co2) _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2) +mkWpFun co1 co2 t1 _ = WpFun co1 co2 t1 + +-- | @mkWpFuns arg_tys wrap@, where @wrap :: a "->" b@, gives a wrapper from +-- @arg_tys -> a@ to @arg_tys -> b@. +mkWpFuns :: [TcType] -> HsWrapper -> HsWrapper +mkWpFuns [] res_wrap = res_wrap +mkWpFuns (arg_ty : arg_tys) res_wrap + = WpFun idHsWrapper (mkWpFuns arg_tys res_wrap) arg_ty mkWpCastR :: TcCoercionR -> HsWrapper mkWpCastR co @@ -212,6 +232,21 @@ mkWpCastN co WpCast (mkTcSubCo co) -- The mkTcSubCo converts Nominal to Representational +-- | In a few limited cases, it is possible to reverse the direction +-- of an HsWrapper. This tries to do so. +symWrapper_maybe :: HsWrapper -> Maybe HsWrapper +symWrapper_maybe = go + where + go WpHole = return WpHole + go (WpCompose wp1 wp2) = WpCompose <$> go wp2 <*> go wp1 + go (WpFun {}) = Nothing + go (WpCast co) = return (WpCast (mkTcSymCo co)) + go (WpEvLam {}) = Nothing + go (WpEvApp {}) = Nothing + go (WpTyLam {}) = Nothing + go (WpTyApp {}) = Nothing + go (WpLet {}) = Nothing + mkWpTyApps :: [Type] -> HsWrapper mkWpTyApps tys = mk_co_app_fn WpTyApp tys @@ -710,7 +745,7 @@ pprHsWrapper doc wrap -- False <=> appears as body of let or lambda help it WpHole = it help it (WpCompose f1 f2) = help (help it f2) f1 - help it (WpFun f1 f2 t1 _) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+> + help it (WpFun f1 f2 t1) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+> help (\_ -> it True <+> help (\_ -> ptext (sLit "x")) f1 True) f2 False help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>") <+> pprParendCo co)] diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs index f299e9da9b..93ba3dbb98 100644 --- a/compiler/typecheck/TcExpr.hs +++ b/compiler/typecheck/TcExpr.hs @@ -6,11 +6,10 @@ \section[TcExpr]{Typecheck an expression} -} -{-# LANGUAGE CPP #-} -{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE CPP, TupleSections, ScopedTypeVariables #-} module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC, - tcInferRho, tcInferRhoNC, + tcInferSigma, tcInferSigmaNC, tcInferRho, tcInferRhoNC, tcSyntaxOp, tcCheckId, addExprErrCtxt, getFixedTyVars ) where @@ -51,9 +50,9 @@ import Name import RdrName import TyCon import Type +import TysPrim ( tYPE ) import TcEvidence import VarSet -import VarEnv import TysWiredIn import TysPrim( intPrimTy ) import PrimOp( tagToEnumKey ) @@ -62,9 +61,9 @@ import MkId ( proxyHashId ) import DynFlags import SrcLoc import Util +import VarEnv ( emptyTidyEnv ) import ListSetOps import Maybes -import ErrUtils import Outputable import FastString import Control.Monad @@ -97,11 +96,15 @@ tcPolyExpr expr res_ty = addExprErrCtxt expr $ do { traceTc "tcPolyExpr" (ppr res_ty); tcPolyExprNC expr res_ty } -tcPolyExprNC expr res_ty - = do { traceTc "tcPolyExprNC" (ppr res_ty) - ; (gen_fn, expr') <- tcGen GenSigCtxt res_ty $ \ _ rho -> - tcMonoExprNC expr rho - ; return (mkLHsWrap gen_fn expr') } +tcPolyExprNC (L loc expr) res_ty + = do { traceTc "tcPolyExprNC_O" (ppr res_ty) + ; (wrap, expr') + <- tcSkolemise GenSigCtxt res_ty $ \ _ res_ty -> + setSrcSpan loc $ + -- NB: setSrcSpan *after* skolemising, so we get better + -- skolem locations + tcExpr expr res_ty + ; return $ L loc (mkHsWrap wrap expr') } --------------- tcMonoExpr, tcMonoExprNC @@ -121,43 +124,25 @@ tcMonoExprNC (L loc expr) res_ty ; return (L loc expr') } --------------- +tcInferSigma, tcInferSigmaNC :: LHsExpr Name -> TcM ( LHsExpr TcId + , TcSigmaType ) +-- Infer a *sigma*-type. +tcInferSigma expr = addErrCtxt (exprCtxt expr) (tcInferSigmaNC expr) + +tcInferSigmaNC (L loc expr) + = setSrcSpan loc $ + do { (expr', sigma) <- tcInfer (tcExpr expr) + ; return (L loc expr', sigma) } + tcInferRho, tcInferRhoNC :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType) --- Infer a *rho*-type. This is, in effect, a special case --- for ids and partial applications, so that if --- f :: Int -> (forall a. a -> a) -> Int --- then we can infer --- f 3 :: (forall a. a -> a) -> Int --- And that in turn is useful --- (a) for the function part of any application (see tcApp) --- (b) for the special rule for '$' +-- Infer a *rho*-type. The return type is always (shallowly) instantiated. tcInferRho expr = addErrCtxt (exprCtxt expr) (tcInferRhoNC expr) -tcInferRhoNC (L loc expr) - = setSrcSpan loc $ - do { (expr', rho) <- tcInfer (tcExpr expr) - ; return (L loc expr', rho) } +tcInferRhoNC expr + = do { (expr', sigma) <- tcInferSigmaNC expr + ; (wrap, rho) <- topInstantiate (exprCtOrigin (unLoc expr)) sigma + ; return (mkLHsWrap wrap expr', rho) } -tcUnboundId :: OccName -> TcRhoType -> TcM (HsExpr TcId) --- Typechedk an occurrence of an unbound Id --- --- Some of these started life as a true hole "_". Others might simply --- be variables that accidentally have no binding site --- --- We turn all of them into HsVar, since HsUnboundVar can't contain an --- Id; and indeed the evidence for the CHoleCan does bind it, so it's --- not unbound any more! -tcUnboundId occ res_ty - = do { ty <- newFlexiTyVarTy liftedTypeKind - ; name <- newSysName occ - ; let ev = mkLocalId name ty - ; loc <- getCtLocM HoleOrigin Nothing - ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty - , ctev_dest = EvVarDest ev - , ctev_loc = loc} - , cc_occ = occ - , cc_hole = ExprHole } - ; emitInsoluble can - ; tcWrapResult (HsVar (noLoc ev)) ty res_ty } {- ************************************************************************ @@ -165,22 +150,23 @@ tcUnboundId occ res_ty tcExpr: the main expression typechecker * * ************************************************************************ + +NB: The res_ty is always deeply skolemised. -} tcExpr :: HsExpr Name -> TcRhoType -> TcM (HsExpr TcId) -tcExpr e res_ty | debugIsOn && isSigmaTy res_ty -- Sanity check - = pprPanic "tcExpr: sigma" (ppr res_ty $$ ppr e) - tcExpr (HsVar (L _ name)) res_ty = tcCheckId name res_ty tcExpr (HsUnboundVar v) res_ty = tcUnboundId v res_ty -tcExpr (HsApp e1 e2) res_ty = tcApp e1 [e2] res_ty +tcExpr (HsApp e1 e2) res_ty + = do { (wrap, fun, args) <- tcApp Nothing e1 [e2] res_ty + ; return (mkHsWrap wrap $ unLoc $ foldl mkHsApp fun args) } -tcExpr (HsLit lit) res_ty = do { let lit_ty = hsLitType lit - ; tcWrapResult (HsLit lit) lit_ty res_ty } +tcExpr e@(HsLit lit) res_ty = do { let lit_ty = hsLitType lit + ; tcWrapResult e (HsLit lit) lit_ty res_ty } -tcExpr (HsPar expr) res_ty = do { expr' <- tcMonoExprNC expr res_ty - ; return (HsPar expr') } +tcExpr (HsPar expr) res_ty = do { expr' <- tcMonoExprNC expr res_ty + ; return (HsPar expr') } tcExpr (HsSCC src lbl expr) res_ty = do { expr' <- tcMonoExpr expr res_ty @@ -195,7 +181,9 @@ tcExpr (HsCoreAnn src lbl expr) res_ty ; return (HsCoreAnn src lbl expr') } tcExpr (HsOverLit lit) res_ty - = do { lit' <- newOverloadedLit (LiteralOrigin lit) lit res_ty + = do { (_wrap, lit') <- newOverloadedLit lit res_ty + (Shouldn'tHappenOrigin "HsOverLit") + ; MASSERT( isIdHsWrapper _wrap ) ; return (HsOverLit lit') } tcExpr (NegApp expr neg_expr) res_ty @@ -204,25 +192,24 @@ tcExpr (NegApp expr neg_expr) res_ty ; expr' <- tcMonoExpr expr res_ty ; return (NegApp expr' neg_expr') } -tcExpr (HsIPVar x) res_ty - = do { let origin = IPOccOrigin x - {- Implicit parameters must have a *tau-type* not a. +tcExpr e@(HsIPVar x) res_ty + = do { {- Implicit parameters must have a *tau-type* not a type scheme. We enforce this by creating a fresh type variable as its type. (Because res_ty may not be a tau-type.) -} - ; ip_ty <- newOpenFlexiTyVarTy + ip_ty <- newOpenFlexiTyVarTy ; let ip_name = mkStrLitTy (hsIPNameFS x) ; ip_var <- emitWantedEvVar origin (mkClassPred ipClass [ip_name, ip_ty]) - ; tcWrapResult (fromDict ipClass ip_name ip_ty (HsVar (noLoc ip_var))) + ; tcWrapResult e (fromDict ipClass ip_name ip_ty (HsVar (noLoc ip_var))) ip_ty res_ty } where -- Coerces a dictionary for `IP "x" t` into `t`. fromDict ipClass x ty = HsWrap $ mkWpCastR $ unwrapIP $ mkClassPred ipClass [x,ty] + origin = IPOccOrigin x -tcExpr (HsOverLabel l) res_ty -- See Note [Type-checking overloaded labels] - = do { let origin = OverLabelOrigin l - ; isLabelClass <- tcLookupClass isLabelClassName +tcExpr e@(HsOverLabel l) res_ty -- See Note [Type-checking overloaded labels] + = do { isLabelClass <- tcLookupClass isLabelClassName ; alpha <- newOpenFlexiTyVarTy ; let lbl = mkStrLitTy l pred = mkClassPred isLabelClass [lbl, alpha] @@ -231,39 +218,43 @@ tcExpr (HsOverLabel l) res_ty -- See Note [Type-checking overloaded labels] ; let proxy_arg = L loc (mkHsWrap (mkWpTyApps [typeSymbolKind, lbl]) (HsVar (L loc proxyHashId))) tm = L loc (fromDict pred (HsVar (L loc var))) `HsApp` proxy_arg - ; tcWrapResult tm alpha res_ty } + ; tcWrapResult e tm alpha res_ty } where -- Coerces a dictionary for `IsLabel "x" t` into `Proxy# x -> t`. fromDict pred = HsWrap $ mkWpCastR $ unwrapIP pred + origin = OverLabelOrigin l tcExpr (HsLam match) res_ty - = do { (co_fn, match') <- tcMatchLambda match res_ty + = do { (co_fn, _, match') <- tcMatchLambda herald match_ctxt match res_ty ; return (mkHsWrap co_fn (HsLam match')) } + where + match_ctxt = MC { mc_what = LambdaExpr, mc_body = tcBody } + herald = sep [ ptext (sLit "The lambda expression") <+> + quotes (pprSetDepth (PartWay 1) $ + pprMatches (LambdaExpr :: HsMatchContext Name) match), + -- The pprSetDepth makes the abstraction print briefly + ptext (sLit "has")] tcExpr e@(HsLamCase _ matches) res_ty - = do { (co_fn, [arg_ty], body_ty) <- matchExpectedFunTys msg 1 res_ty - ; matches' <- tcMatchesCase match_ctxt arg_ty matches body_ty - ; return $ mkHsWrapCo co_fn $ HsLamCase arg_ty matches' } + = do { (co_fn, ~[arg_ty], 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 + ; return (mkHsWrap co_fn $ HsLamCase arg_ty matches') } where msg = sep [ ptext (sLit "The function") <+> quotes (ppr e) , ptext (sLit "requires")] match_ctxt = MC { mc_what = CaseAlt, mc_body = tcBody } -tcExpr (ExprWithTySig expr sig_ty) res_ty +tcExpr e@(ExprWithTySig expr sig_ty) res_ty = do { sig_info <- checkNoErrs $ -- Avoid error cascade tcUserTypeSig sig_ty Nothing ; (expr', poly_ty) <- tcExprSig expr sig_info - ; (inst_wrap, rho) <- deeplyInstantiate ExprSigOrigin poly_ty - ; let expr'' = mkHsWrap inst_wrap $ - ExprWithTySigOut expr' sig_ty - ; tcWrapResult expr'' rho res_ty } + ; let expr'' = ExprWithTySigOut expr' sig_ty + ; tcWrapResult e expr'' poly_ty res_ty } tcExpr (HsType ty) _ - = failWithTc (text "Can't handle type argument:" <+> ppr ty) - -- This is the syntax for type applications that I was planning - -- but there are difficulties (e.g. what order for type args) - -- so it's not enabled yet. - -- Can't eliminate it altogether from the parser, because the - -- same parser parses *patterns*. + = failWithTc (sep [ text "Type argument used outside of a function argument:" + , ppr ty ]) {- @@ -331,7 +322,7 @@ only going to work when it's fully applied, so it turns into So it seems more uniform to treat 'seq' as it it was a language construct. -See Note [seqId magic] in MkId, and +See also Note [seqId magic] in MkId -} tcExpr expr@(OpApp arg1 op fix arg2) res_ty @@ -349,17 +340,18 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty | (L loc (HsVar (L lv op_name))) <- op , op_name `hasKey` dollarIdKey -- Note [Typing rule for ($)] = do { traceTc "Application rule" (ppr op) - ; (arg1', arg1_ty) <- tcInferRho arg1 + ; (arg1', arg1_ty) <- tcInferSigma arg1 - ; let doc = ptext (sLit "The first argument of ($) takes") - ; (co_arg1, [arg2_ty], op_res_ty) <- matchExpectedFunTys doc 1 arg1_ty + ; let doc = ptext (sLit "The first argument of ($) takes") + orig1 = exprCtOrigin (unLoc arg1) + ; (wrap_arg1, [arg2_sigma], op_res_ty) <- + matchActualFunTys doc orig1 1 arg1_ty -- We have (arg1 $ arg2) -- So: arg1_ty = arg2_ty -> op_res_ty - -- where arg2_ty maybe polymorphic; that's the point + -- where arg2_sigma maybe polymorphic; that's the point - ; arg2' <- tcArg op (arg2, arg2_ty, 2) - ; co_b <- unifyType (Just expr) op_res_ty res_ty -- op_res ~ res + ; arg2' <- tcArg op (arg2, arg2_sigma, 2) -- Make sure that the argument type has kind '*' -- ($) :: forall (v:Levity) (a:*) (b:TYPE v). (a->b) -> a -> b @@ -372,19 +364,31 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty -- so we don't need to check anything for that ; a2_tv <- newReturnTyVar liftedTypeKind ; let a2_ty = mkTyVarTy a2_tv - ; co_a <- unifyType (Just arg2) arg2_ty a2_ty -- arg2 ~ a2 + ; co_a <- unifyType (Just arg2) arg2_sigma a2_ty -- arg2_sigma ~N a2_ty - ; op_id <- tcLookupId op_name + ; wrap_res <- tcSubTypeHR orig1 (Just expr) op_res_ty res_ty + -- op_res -> res + ; op_id <- tcLookupId op_name ; let op' = L loc (HsWrap (mkWpTyApps [ getLevity "tcExpr ($)" res_ty , a2_ty - , res_ty ]) + , res_ty]) (HsVar (L lv op_id))) - ; return $ - OpApp (mkLHsWrapCo (mkTcFunCo Nominal co_a co_b) $ - mkLHsWrapCo co_arg1 arg1') - op' fix - (mkLHsWrapCo co_a arg2') } + -- arg1' :: arg1_ty + -- wrap_arg1 :: arg1_ty "->" (arg2_sigma -> op_res_ty) + -- wrap_res :: op_res_ty "->" res_ty + -- co_a :: arg2_sigma ~N a2_ty + -- op' :: (a2_ty -> res_ty) -> a2_ty -> res_ty + + -- wrap1 :: arg1_ty "->" (a2_ty -> res_ty) + wrap1 = mkWpFun (mkWpCastN (mkTcSymCo co_a)) + wrap_res a2_ty res_ty <.> wrap_arg1 + + -- arg2' :: arg2_sigma + -- wrap_a :: a2_ty "->" arg2_sigma + ; return (OpApp (mkLHsWrap wrap1 arg1') + op' fix + (mkLHsWrapCo co_a arg2')) } | (L loc (HsRecFld (Ambiguous lbl _))) <- op , Just sig_ty <- obviousSig (unLoc arg1) @@ -397,23 +401,23 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty | otherwise = do { traceTc "Non Application rule" (ppr op) - ; (op', op_ty) <- tcInferFun op - ; (co_fn, arg_tys, op_res_ty) <- unifyOpFunTysWrap op 2 op_ty - ; co_res <- unifyType (Just expr) op_res_ty res_ty - ; [arg1', arg2'] <- tcArgs op [arg1, arg2] arg_tys - ; return $ mkHsWrapCo co_res $ - OpApp arg1' (mkLHsWrapCo co_fn op') fix arg2' } + ; (wrap, op', [arg1', arg2']) + <- tcApp (Just $ mk_op_msg op) + op [arg1, arg2] res_ty + ; return (mkHsWrap wrap $ OpApp arg1' op' fix arg2') } -- Right sections, equivalent to \ x -> x `op` expr, or -- \ x -> op x expr tcExpr expr@(SectionR op arg2) res_ty = do { (op', op_ty) <- tcInferFun op - ; (co_fn, [arg1_ty, arg2_ty], op_res_ty) <- unifyOpFunTysWrap op 2 op_ty - ; co_res <- unifyType (Just expr) (mkFunTy arg1_ty op_res_ty) res_ty + ; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty) <- + matchActualFunTys (mk_op_msg op) SectionOrigin 2 op_ty + ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr) + (mkFunTy arg1_ty op_res_ty) res_ty ; arg2' <- tcArg op (arg2, arg2_ty, 2) - ; return $ mkHsWrapCo co_res $ - SectionR (mkLHsWrapCo co_fn op') arg2' } + ; return ( mkHsWrap wrap_res $ + SectionR (mkLHsWrap wrap_fun op') arg2' ) } tcExpr expr@(SectionL arg1 op) res_ty = do { (op', op_ty) <- tcInferFun op @@ -421,11 +425,13 @@ tcExpr expr@(SectionL arg1 op) res_ty ; let n_reqd_args | xopt LangExt.PostfixOperators dflags = 1 | otherwise = 2 - ; (co_fn, (arg1_ty:arg_tys), op_res_ty) <- unifyOpFunTysWrap op n_reqd_args op_ty - ; co_res <- unifyType (Just expr) (mkFunTys arg_tys op_res_ty) res_ty + ; (wrap_fn, (arg1_ty:arg_tys), op_res_ty) + <- matchActualFunTys (mk_op_msg op) SectionOrigin n_reqd_args op_ty + ; wrap_res <- tcSubTypeHR SectionOrigin (Just expr) + (mkFunTys arg_tys op_res_ty) res_ty ; arg1' <- tcArg op (arg1, arg1_ty, 1) - ; return $ mkHsWrapCo co_res $ - SectionL arg1' (mkLHsWrapCo co_fn op') } + ; return ( mkHsWrap wrap_res $ + SectionL arg1' (mkLHsWrap wrap_fn op') ) } tcExpr expr@(ExplicitTuple tup_args boxity) res_ty | all tupArgPresent tup_args @@ -451,30 +457,35 @@ tcExpr expr@(ExplicitTuple tup_args boxity) res_ty = mkFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args] (mkTupleTy boxity arg_tys) - ; coi <- unifyType (Just expr) actual_res_ty res_ty + ; wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "ExpTuple") + (Just expr) + actual_res_ty res_ty -- Handle tuple sections where ; tup_args1 <- tcTupArgs tup_args arg_tys - ; return $ mkHsWrapCo coi (ExplicitTuple tup_args1 boxity) } + ; return $ mkHsWrap wrap (ExplicitTuple tup_args1 boxity) } tcExpr (ExplicitList _ witness exprs) res_ty = case witness of Nothing -> do { (coi, elt_ty) <- matchExpectedListTy res_ty ; exprs' <- mapM (tc_elt elt_ty) exprs - ; return $ mkHsWrapCo coi (ExplicitList elt_ty Nothing exprs') } + ; return $ + mkHsWrapCo coi $ ExplicitList elt_ty Nothing exprs' } - Just fln -> do { list_ty <- newFlexiTyVarTy liftedTypeKind + Just fln -> do { list_ty <- newFlexiTyVarTy liftedTypeKind ; fln' <- tcSyntaxOp ListOrigin fln (mkFunTys [intTy, list_ty] res_ty) ; (coi, elt_ty) <- matchExpectedListTy list_ty ; exprs' <- mapM (tc_elt elt_ty) exprs - ; return $ mkHsWrapCo coi (ExplicitList elt_ty (Just fln') exprs') } + ; return $ + mkHsWrapCo coi $ ExplicitList elt_ty (Just fln') exprs' } where tc_elt elt_ty expr = tcPolyExpr expr elt_ty tcExpr (ExplicitPArr _ exprs) res_ty -- maybe empty = do { (coi, elt_ty) <- matchExpectedPArrTy res_ty ; exprs' <- mapM (tc_elt elt_ty) exprs - ; return $ mkHsWrapCo coi (ExplicitPArr elt_ty exprs') } + ; return $ + mkHsWrapCo coi $ ExplicitPArr elt_ty exprs' } where tc_elt elt_ty expr = tcPolyExpr expr elt_ty @@ -512,33 +523,30 @@ tcExpr (HsCase scrut matches) exp_ty tcExpr (HsIf Nothing pred b1 b2) res_ty -- Ordinary 'if' = do { pred' <- tcMonoExpr pred boolTy + -- this forces the branches to be fully instantiated + -- (See #10619) + ; res_ty <- tauTvForReturnTv res_ty ; b1' <- tcMonoExpr b1 res_ty ; b2' <- tcMonoExpr b2 res_ty ; return (HsIf Nothing pred' b1' b2') } -tcExpr (HsIf (Just fun) pred b1 b2) res_ty -- Note [Rebindable syntax for if] - = do { pred_ty <- newOpenFlexiTyVarTy - ; b1_ty <- newOpenFlexiTyVarTy - ; b2_ty <- newOpenFlexiTyVarTy - ; let if_ty = mkFunTys [pred_ty, b1_ty, b2_ty] res_ty - ; fun' <- tcSyntaxOp IfOrigin fun if_ty - ; pred' <- tcMonoExpr pred pred_ty - ; b1' <- tcMonoExpr b1 b1_ty - ; b2' <- tcMonoExpr b2 b2_ty - -- Fundamentally we are just typing (ifThenElse e1 e2 e3) - -- so maybe we should use the code for function applications - -- (which would allow ifThenElse to be higher rank). - -- But it's a little awkward, so I'm leaving it alone for now - -- and it maintains uniformity with other rebindable syntax - ; return (HsIf (Just fun') pred' b1' b2') } +tcExpr (HsIf (Just fun) pred b1 b2) res_ty + -- Note [Rebindable syntax for if] + = do { (wrap, fun', [pred', b1', b2']) + <- tcApp (Just herald) (noLoc fun) [pred, b1, b2] res_ty + ; return ( mkHsWrap wrap $ + HsIf (Just (unLoc fun')) pred' b1' b2' ) } + where + herald = text "Rebindable" <+> quotes (text "if") <+> text "takes" tcExpr (HsMultiIf _ alts) res_ty = do { alts' <- mapM (wrapLocM $ tcGRHS match_ctxt res_ty) alts - ; return $ HsMultiIf res_ty alts' } + ; return (HsMultiIf res_ty alts') } where match_ctxt = MC { mc_what = IfAlt, mc_body = tcBody } tcExpr (HsDo do_or_lc stmts _) res_ty - = tcDoStmts do_or_lc stmts res_ty + = do { expr' <- tcDoStmts do_or_lc stmts res_ty + ; return expr' } tcExpr (HsProc pat cmd) res_ty = do { (pat', cmd', coi) <- tcProc pat cmd res_ty @@ -598,19 +606,25 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name -- Check for missing fields ; checkMissingFields con_like rbinds - ; (con_expr, con_tau) <- tcInferId con_name + ; (con_expr, con_sigma) <- tcInferId con_name + ; (con_wrap, con_tau) <- + topInstantiate (OccurrenceOf con_name) con_sigma + -- a shallow instantiation should really be enough for + -- a data constructor. ; let arity = conLikeArity con_like (arg_tys, actual_res_ty) = tcSplitFunTysN con_tau arity ; case conLikeWrapId_maybe con_like of Nothing -> nonBidirectionalErr (conLikeName con_like) Just con_id -> do { - co_res <- unifyType (Just expr) actual_res_ty res_ty + res_wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "RecordCon") + (Just expr) actual_res_ty res_ty ; rbinds' <- tcRecordBinds con_like arg_tys rbinds - ; return $ mkHsWrapCo co_res $ - RecordCon { rcon_con_name = L loc con_id - , rcon_con_expr = con_expr - , rcon_con_like = con_like - , rcon_flds = rbinds' } } } + ; return $ + mkHsWrap res_wrap $ + RecordCon { rcon_con_name = L loc con_id + , rcon_con_expr = mkHsWrap con_wrap con_expr + , rcon_con_like = con_like + , rcon_flds = rbinds' } } } {- Note [Type of a record update] @@ -749,12 +763,12 @@ following. tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty = ASSERT( notNull rbnds ) - do { -- STEP -2: typecheck the record_expr, the record to bd updated - (record_expr', record_tau) <- tcInferFun record_expr + do { -- STEP -2: typecheck the record_expr, the record to be updated + (record_expr', record_rho) <- tcInferRho record_expr -- STEP -1 See Note [Disambiguating record fields] -- After this we know that rbinds is unambiguous - ; rbinds <- disambiguateRecordBinds record_expr record_tau rbnds res_ty + ; rbinds <- disambiguateRecordBinds record_expr record_rho rbnds res_ty ; let upd_flds = map (unLoc . hsRecFieldLbl . unLoc) rbinds upd_fld_occs = map (occNameFS . rdrNameOcc . rdrNameAmbiguousFieldOcc) upd_flds sel_ids = map selectorAmbiguousFieldOcc upd_flds @@ -860,8 +874,12 @@ 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 - ; co_res <- unifyType (Just expr) rec_res_ty res_ty - ; co_scrut <- unifyType (Just record_expr) record_tau scrut_ty + ; wrap_res <- tcSubTypeHR (exprCtOrigin expr) + (Just expr) rec_res_ty res_ty + ; co_scrut <- unifyType (Just 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 + -- to be normal datatypes -- no contravariant stuff can go on -- STEP 5 -- Typecheck the bindings @@ -887,7 +905,8 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty ; req_wrap <- instCallConstraints RecordUpdOrigin req_theta' -- Phew! - ; return $ mkHsWrapCo co_res $ + ; return $ + mkHsWrap wrap_res $ RecordUpd { rupd_expr = mkLHsWrap fam_co (mkLHsWrapCo co_scrut record_expr') , rupd_flds = rbinds' , rupd_cons = relevant_cons, rupd_in_tys = scrut_inst_tys @@ -916,8 +935,8 @@ tcExpr (PArrSeq _ seq@(FromTo expr1 expr2)) res_ty ; enumFromToP <- initDsTc $ dsDPHBuiltin enumFromToPVar ; enum_from_to <- newMethodFromName (PArrSeqOrigin seq) (idName enumFromToP) elt_ty - ; return $ mkHsWrapCo coi - (PArrSeq enum_from_to (FromTo expr1' expr2')) } + ; return $ + mkHsWrapCo coi $ PArrSeq enum_from_to (FromTo expr1' expr2') } tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty = do { (coi, elt_ty) <- matchExpectedPArrTy res_ty @@ -927,8 +946,9 @@ tcExpr (PArrSeq _ seq@(FromThenTo expr1 expr2 expr3)) res_ty ; enumFromThenToP <- initDsTc $ dsDPHBuiltin enumFromThenToPVar ; eft <- newMethodFromName (PArrSeqOrigin seq) (idName enumFromThenToP) elt_ty -- !!!FIXME: chak - ; return $ mkHsWrapCo coi - (PArrSeq eft (FromThenTo expr1' expr2' expr3')) } + ; return $ + mkHsWrapCo coi $ + PArrSeq eft (FromThenTo expr1' expr2' expr3') } tcExpr (PArrSeq _ _) _ = panic "TcExpr.tcExpr: Infinite parallel array!" @@ -943,9 +963,12 @@ tcExpr (PArrSeq _ _) _ ************************************************************************ -} -tcExpr (HsSpliceE splice) res_ty = tcSpliceExpr splice res_ty -tcExpr (HsBracket brack) res_ty = tcTypedBracket brack res_ty -tcExpr (HsRnBracketOut brack ps) res_ty = tcUntypedBracket brack ps res_ty +tcExpr (HsSpliceE splice) res_ty + = tcSpliceExpr splice res_ty +tcExpr (HsBracket brack) res_ty + = tcTypedBracket brack res_ty +tcExpr (HsRnBracketOut brack ps) res_ty + = tcUntypedBracket brack ps res_ty {- ************************************************************************ @@ -1004,7 +1027,7 @@ tcArithSeq witness seq@(FromThenTo expr1 expr2 expr3) res_ty ----------------- arithSeqEltType :: Maybe (SyntaxExpr Name) -> TcRhoType - -> TcM (TcCoercion, TcType, Maybe (SyntaxExpr Id)) + -> TcM (TcCoercionN, TcType, Maybe (SyntaxExpr Id)) arithSeqEltType Nothing res_ty = do { (coi, elt_ty) <- matchExpectedListTy res_ty ; return (coi, elt_ty, Nothing) } @@ -1022,66 +1045,66 @@ arithSeqEltType (Just fl) res_ty ************************************************************************ -} -tcApp :: LHsExpr Name -> [LHsExpr Name] -- Function and args - -> TcRhoType -> TcM (HsExpr TcId) -- Translated fun and args - -tcApp (L _ (HsPar e)) args res_ty - = tcApp e args res_ty - -tcApp (L _ (HsApp e1 e2)) args res_ty - = tcApp e1 (e2:args) res_ty -- Accumulate the arguments - -tcApp (L loc (HsVar (L _ fun))) args res_ty - | fun `hasKey` tagToEnumKey - , [arg] <- args - = tcTagToEnum loc fun arg res_ty - - | fun `hasKey` seqIdKey - , [arg1,arg2] <- args - = tcSeq loc fun arg1 arg2 res_ty - --- Look for applications of ambiguous record selectors to arguments --- with type signatures, see Note [Disambiguating record fields] -tcApp (L loc (HsRecFld (Ambiguous lbl _))) args@(L _ arg:_) res_ty - | Just sig_ty <- obviousSig arg - = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty - ; sel_name <- disambiguateSelector lbl sig_tc_ty - ; tcApp (L loc (HsRecFld (Unambiguous lbl sel_name))) args res_ty } - -tcApp fun args res_ty - = do { -- Type-check the function - ; (fun1, fun_tau) <- tcInferFun fun - - -- Extract its argument types - ; (co_fun, expected_arg_tys, actual_res_ty) - <- matchExpectedFunTys (mk_app_msg fun) (length args) fun_tau - - -- Typecheck the result, thereby propagating - -- info (if any) from result into the argument types - -- Both actual_res_ty and res_ty are deeply skolemised - -- Rather like tcWrapResult, but (perhaps for historical reasons) - -- we do this before typechecking the arguments - ; wrap_res <- addErrCtxtM (funResCtxt True (unLoc fun) actual_res_ty res_ty) $ - tcSubTypeDS_NC GenSigCtxt (Just $ foldl mkHsApp fun args) - actual_res_ty res_ty - - -- Typecheck the arguments - ; args1 <- tcArgs fun args expected_arg_tys - - -- Assemble the result - ; let fun2 = mkLHsWrapCo co_fun fun1 - app = mkLHsWrap wrap_res (foldl mkHsApp fun2 args1) - - ; return (unLoc app) } - +tcApp :: Maybe SDoc -- like "The function `f' is applied to" + -- or leave out to get exactly that message + -> LHsExpr Name -> [LHsExpr Name] -- Function and args + -> TcRhoType -> TcM (HsWrapper, LHsExpr TcId, [LHsExpr TcId]) + -- (wrap, fun, args). For an ordinary function application, + -- these should be assembled as (wrap (fun args)). + -- But OpApp is slightly different, so that's why the caller + -- must assemble + +tcApp m_herald orig_fun orig_args res_ty + = go orig_fun orig_args + where + go (L _ (HsPar e)) args = go e args + go (L _ (HsApp e1 e2)) args = go e1 (e2:args) + + go (L loc (HsVar (L _ fun))) args + | fun `hasKey` tagToEnumKey + , count (not . isLHsTypeExpr) args == 1 + = do { (wrap, expr, args) <- tcTagToEnum loc fun args res_ty + ; return (wrap, expr, args) } + + | fun `hasKey` seqIdKey + , count (not . isLHsTypeExpr) args == 2 + = do { (wrap, expr, args) <- tcSeq loc fun args res_ty + ; return (wrap, expr, args) } + + go (L loc (HsRecFld (Ambiguous lbl _))) args@(L _ arg : _) + | Just sig_ty <- obviousSig arg + = do { sig_tc_ty <- tcHsSigWcType ExprSigCtxt sig_ty + ; sel_name <- disambiguateSelector lbl sig_tc_ty + ; go (L loc (HsRecFld (Unambiguous lbl sel_name))) args } + + go fun args + = do { -- Type-check the function + ; (fun1, fun_sigma) <- tcInferFun fun + ; let orig = exprCtOrigin (unLoc fun) + + ; (wrap_fun, args1, actual_res_ty) + <- tcArgs fun fun_sigma orig args + (m_herald `orElse` mk_app_msg fun) + + -- this is just like tcWrapResult, but the types don't line + -- up to call that function + ; wrap_res <- addFunResCtxt True (unLoc fun) actual_res_ty res_ty $ + tcSubTypeDS_NC_O orig GenSigCtxt + (Just $ foldl mkHsApp fun args) + actual_res_ty res_ty + + ; return (wrap_res, mkLHsWrap wrap_fun fun1, args1) } mk_app_msg :: LHsExpr Name -> SDoc mk_app_msg fun = sep [ ptext (sLit "The function") <+> quotes (ppr fun) , ptext (sLit "is applied to")] +mk_op_msg :: LHsExpr Name -> SDoc +mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes" + ---------------- -tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType) --- Infer and instantiate the type of a function +tcInferFun :: LHsExpr Name -> TcM (LHsExpr TcId, TcSigmaType) +-- Infer type of a function tcInferFun (L loc (HsVar (L _ name))) = do { (fun, ty) <- setSrcSpan loc (tcInferId name) -- Don't wrap a context around a plain Id @@ -1093,23 +1116,70 @@ tcInferFun (L loc (HsRecFld f)) ; return (L loc fun, ty) } tcInferFun fun - = do { (fun, fun_ty) <- tcInfer (tcMonoExpr fun) + = do { (fun, fun_ty) <- tcInferSigma fun -- Zonk the function type carefully, to expose any polymorphism -- E.g. (( \(x::forall a. a->a). blah ) e) -- We can see the rank-2 type of the lambda in time to generalise e ; fun_ty' <- zonkTcType fun_ty - ; (wrap, rho) <- deeplyInstantiate AppOrigin fun_ty' - ; return (mkLHsWrap wrap fun, rho) } + ; return (fun, fun_ty') } ---------------- -tcArgs :: LHsExpr Name -- The function (for error messages) - -> [LHsExpr Name] -> [TcSigmaType] -- Actual arguments and expected arg types - -> TcM [LHsExpr TcId] -- Resulting args - -tcArgs fun args expected_arg_tys - = mapM (tcArg fun) (zip3 args expected_arg_tys [1..]) +-- | Type-check the arguments to a function, possibly including visible type +-- applications +tcArgs :: LHsExpr Name -- ^ The function itself (for err msgs only) + -> TcSigmaType -- ^ the (uninstantiated) type of the function + -> CtOrigin -- ^ the origin for the function's type + -> [LHsExpr Name] -- ^ the args + -> SDoc -- ^ the herald for matchActualFunTys + -> TcM (HsWrapper, [LHsExpr TcId], TcSigmaType) + -- ^ (a wrapper for the function, the tc'd args, result type) +tcArgs fun orig_fun_ty fun_orig orig_args herald + = go [] 1 orig_fun_ty orig_args + where + orig_arity = length orig_args + + go _ _ fun_ty [] = return (idHsWrapper, [], fun_ty) + + go acc_args n fun_ty (arg:args) + | Just hs_ty_arg <- isLHsTypeExpr_maybe arg + = do { (wrap1, upsilon_ty) <- topInstantiateInferred fun_orig fun_ty + -- wrap1 :: fun_ty "->" upsilon_ty + ; case tcSplitForAllTy_maybe upsilon_ty of + Just (binder, inner_ty) + | Just tv <- binderVar_maybe binder -> + ASSERT( binderVisibility binder == Specified ) + do { let kind = tyVarKind tv + ; ty_arg <- tcHsTypeApp hs_ty_arg kind + ; let insted_ty = substTyWith [tv] [ty_arg] inner_ty + ; (inner_wrap, args', res_ty) + <- go acc_args (n+1) insted_ty args + -- inner_wrap :: insted_ty "->" (map typeOf args') -> res_ty + ; let inst_wrap = mkWpTyApps [ty_arg] + ; return ( inner_wrap <.> inst_wrap <.> wrap1 + , L (getLoc arg) (HsTypeOut hs_ty_arg) : args' + , res_ty ) } + _ -> ty_app_err upsilon_ty hs_ty_arg } + + | otherwise -- not a type application. + = do { (wrap, [arg_ty], res_ty) + <- matchActualFunTysPart herald fun_orig 1 fun_ty + acc_args orig_arity + -- wrap :: fun_ty "->" arg_ty -> res_ty + ; arg' <- tcArg fun (arg, arg_ty, n) + ; (inner_wrap, args', inner_res_ty) + <- go (arg_ty : acc_args) (n+1) res_ty args + -- inner_wrap :: res_ty "->" (map typeOf args') -> inner_res_ty + ; return ( mkWpFun idHsWrapper inner_wrap arg_ty res_ty <.> wrap + , arg' : args' + , inner_res_ty ) } + + ty_app_err ty arg + = do { (_, ty) <- zonkTidyTcType emptyTidyEnv ty + ; failWith $ + text "Cannot not apply expression of type" <+> quotes (ppr ty) $$ + text "to a visible type argument" <+> quotes (ppr arg) } ---------------- tcArg :: LHsExpr Name -- The function (for error messages) @@ -1127,23 +1197,16 @@ tcTupArgs args tys go (L l (Present expr), arg_ty) = do { expr' <- tcPolyExpr expr arg_ty ; return (L l (Present expr')) } ----------------- -unifyOpFunTysWrap :: LHsExpr Name -> Arity -> TcRhoType - -> TcM (TcCoercion, [TcSigmaType], TcRhoType) --- A wrapper for matchExpectedFunTys -unifyOpFunTysWrap op arity ty = matchExpectedFunTys herald arity ty - where - herald = ptext (sLit "The operator") <+> quotes (ppr op) <+> ptext (sLit "takes") - --------------------------- tcSyntaxOp :: CtOrigin -> HsExpr Name -> TcType -> TcM (HsExpr TcId) -- Typecheck a syntax operator, checking that it has the specified type -- The operator is always a variable at this stage (i.e. renamer output) -- This version assumes res_ty is a monotype tcSyntaxOp orig (HsVar (L _ op)) res_ty - = do { (expr, rho) <- tcInferIdWithOrig orig (nameRdrName op) op - ; tcWrapResult expr rho res_ty } -tcSyntaxOp _ other _ = pprPanic "tcSyntaxOp" (ppr other) + = do { (expr, rho) <- tcInferId op + ; tcWrapResultO orig expr rho res_ty } + +tcSyntaxOp _ other _ = pprPanic "tcSyntaxOp" (ppr other) {- Note [Push result type in] @@ -1170,7 +1233,6 @@ With the change, f1 will type-check, because the 'Char' info from the signature is propagated into MkQ's argument. With the check in the other order, the extra signature in f2 is reqd. - ************************************************************************ * * Expressions with a type signature @@ -1209,11 +1271,11 @@ tcExprSig expr sig@(TISI { sig_bndr = s_bndr ; tau <- zonkTcType tau ; let inferred_theta = map evVarPred givens tau_tvs = tyCoVarsOfType tau - ; (my_tv_set, my_theta) <- chooseInferredQuantifiers inferred_theta tau_tvs (Just sig) - ; let my_tvs = filter (`elemVarSet` my_tv_set) qtvs -- Maintain original order - inferred_sigma = mkInvSigmaTy qtvs inferred_theta tau - my_sigma = mkInvSigmaTy my_tvs my_theta tau - ; wrap <- if inferred_sigma `eqType` my_sigma + ; (binders, my_theta) <- chooseInferredQuantifiers inferred_theta + tau_tvs qtvs (Just sig) + ; let inferred_sigma = mkInvSigmaTy qtvs inferred_theta tau + my_sigma = mkForAllTys binders (mkPhiTy my_theta tau) + ; wrap <- if inferred_sigma `eqType` my_sigma -- NB: eqType ignores vis. then return idHsWrapper -- Fast path; also avoids complaint when we infer -- an ambiguouse type and have AllowAmbiguousType -- e..g infer x :: forall a. F a -> Int @@ -1223,7 +1285,7 @@ tcExprSig expr sig@(TISI { sig_bndr = s_bndr <.> mkWpTyLams qtvs <.> mkWpLams givens <.> mkWpLet ev_binds - ; return (mkLHsWrap poly_wrap expr', mkInvSigmaTy qtvs theta tau) } + ; return (mkLHsWrap poly_wrap expr', my_sigma) } | otherwise = panic "tcExprSig" -- Can't happen where @@ -1240,15 +1302,14 @@ tcCheckId :: Name -> TcRhoType -> TcM (HsExpr TcId) tcCheckId name res_ty = do { (expr, actual_res_ty) <- tcInferId name ; traceTc "tcCheckId" (vcat [ppr name, ppr actual_res_ty, ppr res_ty]) - ; addErrCtxtM (funResCtxt False (HsVar (noLoc name)) - actual_res_ty res_ty) $ - tcWrapResult expr actual_res_ty res_ty } + ; addFunResCtxt False (HsVar (noLoc name)) actual_res_ty res_ty $ + tcWrapResultO (OccurrenceOf name) expr actual_res_ty res_ty } tcCheckRecSelId :: AmbiguousFieldOcc Name -> TcRhoType -> TcM (HsExpr TcId) -tcCheckRecSelId f@(Unambiguous _ _) res_ty +tcCheckRecSelId f@(Unambiguous (L _ lbl) _) res_ty = do { (expr, actual_res_ty) <- tcInferRecSelId f - ; addErrCtxtM (funResCtxt False (HsRecFld f) actual_res_ty res_ty) $ - tcWrapResult expr actual_res_ty res_ty } + ; addFunResCtxt False (HsRecFld f) actual_res_ty res_ty $ + tcWrapResultO (OccurrenceOfRecSel lbl) expr actual_res_ty res_ty } tcCheckRecSelId (Ambiguous lbl _) res_ty = case tcSplitFunTy_maybe res_ty of Nothing -> ambiguousSelector lbl @@ -1256,21 +1317,17 @@ tcCheckRecSelId (Ambiguous lbl _) res_ty ; tcCheckRecSelId (Unambiguous lbl sel_name) res_ty } ------------------------ -tcInferId :: Name -> TcM (HsExpr TcId, TcRhoType) --- Infer type, and deeply instantiate -tcInferId n = tcInferIdWithOrig (OccurrenceOf n) (nameRdrName n) n - tcInferRecSelId :: AmbiguousFieldOcc Name -> TcM (HsExpr TcId, TcRhoType) tcInferRecSelId (Unambiguous (L _ lbl) sel) - = tcInferIdWithOrig (OccurrenceOfRecSel lbl) lbl sel + = do { (expr', ty) <- tc_infer_id lbl sel + ; return (expr', ty) } tcInferRecSelId (Ambiguous lbl _) = ambiguousSelector lbl ------------------------ -tcInferIdWithOrig :: CtOrigin -> RdrName -> Name -> - TcM (HsExpr TcId, TcRhoType) --- Look up an occurrence of an Id, and instantiate it (deeply) -tcInferIdWithOrig orig lbl id_name +tcInferId :: Name -> TcM (HsExpr TcId, TcSigmaType) +-- Look up an occurrence of an Id +tcInferId id_name | id_name `hasKey` tagToEnumKey = failWithTc (ptext (sLit "tagToEnum# must appear applied to one argument")) -- tcApp catches the case (tagToEnum# arg) @@ -1278,67 +1335,97 @@ tcInferIdWithOrig orig lbl id_name | id_name `hasKey` assertIdKey = do { dflags <- getDynFlags ; if gopt Opt_IgnoreAsserts dflags - then tc_infer_id orig lbl id_name - else tc_infer_assert orig } + then tc_infer_id (nameRdrName id_name) id_name + else tc_infer_assert id_name } | otherwise - = tc_infer_id orig lbl id_name + = do { (expr, ty) <- tc_infer_id (nameRdrName id_name) id_name + ; traceTc "tcInferId" (ppr id_name <+> dcolon <+> ppr ty) + ; return (expr, ty) } -tc_infer_assert :: CtOrigin -> TcM (HsExpr TcId, TcRhoType) +tc_infer_assert :: Name -> TcM (HsExpr TcId, TcSigmaType) -- Deal with an occurrence of 'assert' -- See Note [Adding the implicit parameter to 'assert'] -tc_infer_assert orig +tc_infer_assert assert_name = do { assert_error_id <- tcLookupId assertErrorName - ; (wrap, id_rho) <- deeplyInstantiate orig (idType assert_error_id) + ; (wrap, id_rho) <- topInstantiate (OccurrenceOf assert_name) + (idType assert_error_id) ; return (mkHsWrap wrap (HsVar (noLoc assert_error_id)), id_rho) } -tc_infer_id :: CtOrigin -> RdrName -> Name -> TcM (HsExpr TcId, TcRhoType) --- Return type is deeply instantiated -tc_infer_id orig lbl id_name +tc_infer_id :: RdrName -> Name -> TcM (HsExpr TcId, TcSigmaType) +tc_infer_id lbl id_name = do { thing <- tcLookup id_name ; case thing of ATcId { tct_id = id } -> do { check_naughty id -- Note [Local record selectors] ; checkThLocalId id - ; inst_normal_id id } + ; return_id id } AGlobal (AnId id) -> do { check_naughty id - ; inst_normal_id id } + ; return_id id } -- A global cannot possibly be ill-staged -- nor does it need the 'lifting' treatment -- hence no checkTh stuff here AGlobal (AConLike cl) -> case cl of - RealDataCon con -> inst_data_con con - PatSynCon ps -> tcPatSynBuilderOcc orig ps + RealDataCon con -> return_data_con con + PatSynCon ps -> tcPatSynBuilderOcc ps _ -> failWithTc $ ppr thing <+> ptext (sLit "used where a value identifier was expected") } where - inst_normal_id id - = do { (wrap, rho) <- deeplyInstantiate orig (idType id) - ; return (mkHsWrap wrap (HsVar (noLoc id)), rho) } - - inst_data_con con - -- For data constructors, - -- * Must perform the stupid-theta check - -- * No need to deeply instantiate because type has all foralls at top - = do { let wrap_id = dataConWrapId con - (tvs, theta, rho) = tcSplitSigmaTy (idType wrap_id) - ; (subst, tvs') <- newMetaTyVars tvs - ; let tys' = mkTyVarTys tvs' - theta' = substTheta subst theta - rho' = substTy subst rho - ; wrap <- instCall orig tys' theta' - ; addDataConStupidTheta con tys' - ; return (mkHsWrap wrap (HsVar (noLoc wrap_id)), rho') } + return_id id = return (HsVar (noLoc id), idType id) + + return_data_con con + -- For data constructors, must perform the stupid-theta check + | null stupid_theta + = return_id con_wrapper_id + + | otherwise + -- See Note [Instantiating stupid theta] + = do { let (tvs, theta, rho) = tcSplitSigmaTy (idType con_wrapper_id) + ; (subst, tvs') <- newMetaTyVars tvs + ; let tys' = mkTyVarTys tvs' + theta' = substTheta subst theta + rho' = substTy subst rho + ; wrap <- instCall (OccurrenceOf id_name) tys' theta' + ; addDataConStupidTheta con tys' + ; return (mkHsWrap wrap (HsVar (noLoc con_wrapper_id)), rho') } + + where + con_wrapper_id = dataConWrapId con + stupid_theta = dataConStupidTheta con check_naughty id | isNaughtyRecordSelector id = failWithTc (naughtyRecordSel lbl) | otherwise = return () + +tcUnboundId :: OccName -> TcRhoType -> TcM (HsExpr TcId) +-- Typechedk an occurrence of an unbound Id +-- +-- Some of these started life as a true hole "_". Others might simply +-- be variables that accidentally have no binding site +-- +-- We turn all of them into HsVar, since HsUnboundVar can't contain an +-- Id; and indeed the evidence for the CHoleCan does bind it, so it's +-- not unbound any more! +tcUnboundId occ res_ty + = do { ty <- newFlexiTyVarTy liftedTypeKind + ; name <- newSysName occ + ; let ev = mkLocalId name ty + ; loc <- getCtLocM HoleOrigin Nothing + ; let can = CHoleCan { cc_ev = CtWanted { ctev_pred = ty + , ctev_dest = EvVarDest ev + , ctev_loc = loc} + , cc_occ = occ + , cc_hole = ExprHole } + ; emitInsoluble can + ; tcWrapResultO (UnboundOccurrenceOf occ) (HsVar (noLoc ev)) ty res_ty } + + {- Note [Adding the implicit parameter to 'assert'] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1374,48 +1461,105 @@ Usually that coercion is hidden inside the wrappers for constructors of F [Int] but here we have to do it explicitly. It's all grotesquely complicated. + +Note [Instantiating stupid theta] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Normally, when we infer the type of an Id, we don't instantiate, +because we wish to allow for visible type application later on. +But if a datacon has a stupid theta, we're a bit stuck. We need +to emit the stupid theta constraints with instantiated types. It's +difficult to defer this to the lazy instantiation, because a stupid +theta has no spot to put it in a type. So we just instantiate eagerly +in this case. Thus, users cannot use visible type application with +a data constructor sporting a stupid theta. I won't feel so bad for +the users that complain. + -} -tcSeq :: SrcSpan -> Name -> LHsExpr Name -> LHsExpr Name - -> TcRhoType -> TcM (HsExpr TcId) +tcSeq :: SrcSpan -> Name -> [LHsExpr Name] + -> TcRhoType -> TcM (HsWrapper, LHsExpr TcId, [LHsExpr TcId]) -- (seq e1 e2) :: res_ty -- We need a special typing rule because res_ty can be unboxed -- See Note [Typing rule for seq] -tcSeq loc fun_name arg1 arg2 res_ty +tcSeq loc fun_name args res_ty = do { fun <- tcLookupId fun_name - ; (arg1', arg1_ty) <- tcInfer (tcMonoExpr arg1) + ; (arg1_ty, args1) <- case args of + (ty_arg_expr1 : args1) + | Just hs_ty_arg1 <- isLHsTypeExpr_maybe ty_arg_expr1 + -> do { ty_arg1 <- tcHsTypeApp hs_ty_arg1 liftedTypeKind + ; return (ty_arg1, args1) } + + _ -> do { arg_ty1 <- newFlexiTyVarTy liftedTypeKind + ; return (arg_ty1, args) } + + ; (arg1, arg2) <- case args1 of + [ty_arg_expr2, term_arg1, term_arg2] + | Just hs_ty_arg2 <- isLHsTypeExpr_maybe ty_arg_expr2 + -> do { lev_ty <- newFlexiTyVarTy levityTy + ; ty_arg2 <- tcHsTypeApp hs_ty_arg2 (tYPE lev_ty) + -- see Note [Typing rule for seq] + ; _ <- unifyType noThing ty_arg2 res_ty + ; return (term_arg1, term_arg2) } + [term_arg1, term_arg2] -> return (term_arg1, term_arg2) + _ -> too_many_args + + ; arg1' <- tcMonoExpr arg1 arg1_ty + ; res_ty <- zonkTcType res_ty -- just in case we learned something + -- interesting about it ; arg2' <- tcMonoExpr arg2 res_ty ; let fun' = L loc (HsWrap ty_args (HsVar (L loc fun))) ty_args = WpTyApp res_ty <.> WpTyApp arg1_ty - ; return (HsApp (L loc (HsApp fun' arg1')) arg2') } + ; return (idHsWrapper, fun', [arg1', arg2']) } + where + too_many_args :: TcM a + too_many_args + = failWith $ + hang (text "Too many type arguments to seq:") + 2 (sep (map pprParendExpr args)) -tcTagToEnum :: SrcSpan -> Name -> LHsExpr Name -> TcRhoType -> TcM (HsExpr TcId) + +tcTagToEnum :: SrcSpan -> Name -> [LHsExpr Name] -> TcRhoType + -> TcM (HsWrapper, LHsExpr TcId, [LHsExpr TcId]) -- tagToEnum# :: forall a. Int# -> a -- See Note [tagToEnum#] Urgh! -tcTagToEnum loc fun_name arg res_ty - = do { fun <- tcLookupId fun_name - ; ty' <- zonkTcType res_ty - - -- Check that the type is algebraic - ; let mb_tc_app = tcSplitTyConApp_maybe ty' - Just (tc, tc_args) = mb_tc_app - ; checkTc (isJust mb_tc_app) - (mk_error ty' doc1) - - -- Look through any type family - ; fam_envs <- tcGetFamInstEnvs - ; let (rep_tc, rep_args, coi) = tcLookupDataFamInst fam_envs tc tc_args - -- coi :: tc tc_args ~R rep_tc rep_args - - ; checkTc (isEnumerationTyCon rep_tc) - (mk_error ty' doc2) - - ; arg' <- tcMonoExpr arg intPrimTy - ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar (L loc fun))) - rep_ty = mkTyConApp rep_tc rep_args - - ; return (mkHsWrapCoR (mkTcSymCo coi) $ HsApp fun' arg') } - -- coi is a Representational coercion +tcTagToEnum loc fun_name args res_ty + = do { fun <- tcLookupId fun_name + + ; arg <- case args of + [ty_arg_expr, term_arg] + | Just hs_ty_arg <- isLHsTypeExpr_maybe ty_arg_expr + -> do { ty_arg <- tcHsTypeApp hs_ty_arg liftedTypeKind + ; _ <- unifyType noThing ty_arg res_ty + -- other than influencing res_ty, we just + -- don't care about a type arg passed in. + -- So drop the evidence. + ; return term_arg } + [term_arg] -> return term_arg + _ -> too_many_args + + ; ty' <- zonkTcType res_ty + + -- Check that the type is algebraic + ; let mb_tc_app = tcSplitTyConApp_maybe ty' + Just (tc, tc_args) = mb_tc_app + ; checkTc (isJust mb_tc_app) + (mk_error ty' doc1) + + -- Look through any type family + ; fam_envs <- tcGetFamInstEnvs + ; let (rep_tc, rep_args, coi) + = tcLookupDataFamInst fam_envs tc tc_args + -- coi :: tc tc_args ~R rep_tc rep_args + + ; checkTc (isEnumerationTyCon rep_tc) + (mk_error ty' doc2) + + ; arg' <- tcMonoExpr arg intPrimTy + ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar (L loc fun))) + rep_ty = mkTyConApp rep_tc rep_args + + ; return (mkWpCastR (mkTcSymCo coi), fun', [arg']) } + -- coi is a Representational coercion where doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature") , ptext (sLit "e.g. (tagToEnum# x) :: Bool") ] @@ -1427,6 +1571,12 @@ tcTagToEnum loc fun_name arg res_ty <+> ptext (sLit "at type") <+> ppr ty) 2 what + too_many_args :: TcM a + too_many_args + = failWith $ + hang (text "Too many type arguments to tagToEnum#:") + 2 (sep (map pprParendExpr args)) + {- ************************************************************************ * * @@ -1643,7 +1793,7 @@ See also Note [HsRecField and HsRecUpdField] in HsPat. -- Given a RdrName that refers to multiple record fields, and the type -- of its argument, try to determine the name of the selector that is -- meant. -disambiguateSelector :: Located RdrName -> Type -> RnM Name +disambiguateSelector :: Located RdrName -> Type -> TcM Name disambiguateSelector lr@(L _ rdr) parent_type = do { fam_inst_envs <- tcGetFamInstEnvs ; case tyConOf fam_inst_envs parent_type of @@ -1658,7 +1808,7 @@ disambiguateSelector lr@(L _ rdr) parent_type -- This field name really is ambiguous, so add a suitable "ambiguous -- occurrence" error, then give up. -ambiguousSelector :: Located RdrName -> RnM a +ambiguousSelector :: Located RdrName -> TcM a ambiguousSelector (L _ rdr) = do { env <- getGlobalRdrEnv ; let gres = lookupGRE_RdrName rdr env @@ -1667,10 +1817,10 @@ ambiguousSelector (L _ rdr) -- Disambiguate the fields in a record update. -- See Note [Disambiguating record fields] -disambiguateRecordBinds :: LHsExpr Name -> TcType +disambiguateRecordBinds :: LHsExpr Name -> TcRhoType -> [LHsRecUpdField Name] -> Type -> TcM [LHsRecField' (AmbiguousFieldOcc Id) (LHsExpr Name)] -disambiguateRecordBinds record_expr record_tau rbnds res_ty +disambiguateRecordBinds record_expr record_rho rbnds res_ty -- Are all the fields unambiguous? = case mapM isUnambiguous rbnds of -- If so, just skip to looking up the Ids @@ -1718,7 +1868,7 @@ disambiguateRecordBinds record_expr record_tau rbnds res_ty -- Does the expression being updated have a type signature? -- If so, try to extract a parent TyCon from it | Just {} <- obviousSig (unLoc record_expr) - , Just tc <- tyConOf fam_inst_envs record_tau + , Just tc <- tyConOf fam_inst_envs record_rho -> return (RecSelData tc) -- Nothing else we can try... @@ -1946,36 +2096,47 @@ fieldCtxt :: FieldLabelString -> SDoc fieldCtxt field_name = ptext (sLit "In the") <+> quotes (ppr field_name) <+> ptext (sLit "field of a record") -funResCtxt :: Bool -- There is at least one argument - -> HsExpr Name -> TcType -> TcType - -> TidyEnv -> TcM (TidyEnv, MsgDoc) +addFunResCtxt :: Bool -- There is at least one argument + -> HsExpr Name -> TcType -> TcType + -> TcM a -> TcM a -- When we have a mis-match in the return type of a function -- try to give a helpful message about too many/few arguments -- -- Used for naked variables too; but with has_args = False -funResCtxt has_args fun fun_res_ty env_ty tidy_env - = do { fun_res' <- zonkTcType fun_res_ty - ; env' <- zonkTcType env_ty - ; let (args_fun, res_fun) = tcSplitFunTys fun_res' - (args_env, res_env) = tcSplitFunTys env' - n_fun = length args_fun - n_env = length args_env - info | n_fun == n_env = Outputable.empty - | n_fun > n_env - , not_fun res_env = ptext (sLit "Probable cause:") <+> quotes (ppr fun) - <+> ptext (sLit "is applied to too few arguments") - | has_args - , not_fun res_fun = ptext (sLit "Possible cause:") <+> quotes (ppr fun) - <+> ptext (sLit "is applied to too many arguments") - | otherwise = Outputable.empty -- Never suggest that a naked variable is - -- applied to too many args! - ; return (tidy_env, info) } +addFunResCtxt has_args fun fun_res_ty env_ty + = addLandmarkErrCtxtM (\env -> (env, ) <$> mk_msg) + -- NB: use a landmark error context, so that an empty context + -- doesn't suppress some more useful context where - not_fun ty -- ty is definitely not an arrow type, - -- and cannot conceivably become one - = case tcSplitTyConApp_maybe ty of - Just (tc, _) -> isAlgTyCon tc - Nothing -> False + mk_msg + = do { fun_res' <- zonkTcType fun_res_ty + ; env' <- zonkTcType env_ty + ; let (_, _, fun_tau) = tcSplitSigmaTy fun_res' + (_, _, env_tau) = tcSplitSigmaTy env' + (args_fun, res_fun) = tcSplitFunTys fun_tau + (args_env, res_env) = tcSplitFunTys env_tau + n_fun = length args_fun + n_env = length args_env + info | n_fun == n_env = Outputable.empty + | n_fun > n_env + , not_fun res_env + = ptext (sLit "Probable cause:") <+> quotes (ppr fun) + <+> ptext (sLit "is applied to too few arguments") + + | has_args + , not_fun res_fun + = ptext (sLit "Possible cause:") <+> quotes (ppr fun) + <+> ptext (sLit "is applied to too many arguments") + + | otherwise + = Outputable.empty -- Never suggest that a naked variable is -- applied to too many args! + ; return info } + where + not_fun ty -- ty is definitely not an arrow type, + -- and cannot conceivably become one + = case tcSplitTyConApp_maybe ty of + Just (tc, _) -> isAlgTyCon tc + Nothing -> False badFieldTypes :: [(FieldLabelString,TcType)] -> SDoc badFieldTypes prs diff --git a/compiler/typecheck/TcExpr.hs-boot b/compiler/typecheck/TcExpr.hs-boot index acd5d8a747..8d60ba4662 100644 --- a/compiler/typecheck/TcExpr.hs-boot +++ b/compiler/typecheck/TcExpr.hs-boot @@ -14,7 +14,11 @@ tcMonoExpr, tcMonoExprNC :: -> TcRhoType -> TcM (LHsExpr TcId) -tcInferRho, tcInferRhoNC :: +tcInferSigma, tcInferSigmaNC :: + LHsExpr Name + -> TcM (LHsExpr TcId, TcSigmaType) + +tcInferRho :: LHsExpr Name -> TcM (LHsExpr TcId, TcRhoType) diff --git a/compiler/typecheck/TcGenDeriv.hs b/compiler/typecheck/TcGenDeriv.hs index 009d203128..ad36167a69 100644 --- a/compiler/typecheck/TcGenDeriv.hs +++ b/compiler/typecheck/TcGenDeriv.hs @@ -1639,10 +1639,10 @@ functorLikeTraverse var (FT { ft_triv = caseTrivial, ft_var = caseVar | otherwise = (caseWrongArg, True) -- Non-decomposable (eg type function) where (xrs,xcs) = unzip (map (go co) args) - go co (ForAllTy (Named v Invisible) x) | v /= var && xc = (caseForAll v xr,True) + go _ (ForAllTy (Named _ Visible) _) = panic "unexpected visible binder" + go co (ForAllTy (Named v _) x) | v /= var && xc = (caseForAll v xr,True) where (xr,xc) = go co x - go _ (ForAllTy (Named _ Visible) _) = panic "unexpected visible binder" go _ _ = (caseTrivial,False) -- Return all syntactic subterms of ty that contain var somewhere @@ -2052,7 +2052,7 @@ genAuxBindSpec loc (DerivCon2Tag tycon) rdr_name = con2tag_RDR tycon sig_ty = mkLHsSigWcType $ L loc $ HsCoreTy $ - mkInvSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $ + mkSpecSigmaTy (tyConTyVars tycon) (tyConStupidTheta tycon) $ mkParentType tycon `mkFunTy` intPrimTy lots_of_constructors = tyConFamilySize tycon > 8 @@ -2076,7 +2076,7 @@ genAuxBindSpec loc (DerivTag2Con tycon) L loc (TypeSig [L loc rdr_name] sig_ty)) where sig_ty = mkLHsSigWcType $ L loc $ - HsCoreTy $ mkInvForAllTys (tyConTyVars tycon) $ + HsCoreTy $ mkSpecForAllTys (tyConTyVars tycon) $ intTy `mkFunTy` mkParentType tycon rdr_name = tag2con_RDR tycon diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs index ee7038d546..210b1798e6 100644 --- a/compiler/typecheck/TcHsSyn.hs +++ b/compiler/typecheck/TcHsSyn.hs @@ -320,6 +320,7 @@ zonkTyBndrX :: ZonkEnv -> TyVar -> TcM (ZonkEnv, TyVar) zonkTyBndrX env tv = ASSERT( isImmutableTyVar tv ) do { ki <- zonkTcTypeToType env (tyVarKind tv) + -- Internal names tidy up better, for iface files. ; let tv' = mkTyVar (tyVarName tv) ki ; return (extendTyZonkEnv1 env tv', tv') } @@ -433,12 +434,15 @@ zonk_bind env (AbsBinds { abs_tvs = tyvars, abs_ev_vars = evs , abs_ev_binds = new_ev_binds , abs_exports = new_exports, abs_binds = new_val_bind }) } where - zonkExport env (ABE{ abe_wrap = wrap, abe_poly = poly_id + zonkExport env (ABE{ abe_wrap = wrap, abe_inst_wrap = inst_wrap + , abe_poly = poly_id , abe_mono = mono_id, abe_prags = prags }) = do new_poly_id <- zonkIdBndr env poly_id (_, new_wrap) <- zonkCoFn env wrap + (_, new_inst_wrap) <- zonkCoFn env inst_wrap new_prags <- zonkSpecPrags env prags - return (ABE{ abe_wrap = new_wrap, abe_poly = new_poly_id + return (ABE{ abe_wrap = new_wrap, abe_inst_wrap = new_inst_wrap + , abe_poly = new_poly_id , abe_mono = zonkIdOcc env mono_id , abe_prags = new_prags }) @@ -731,6 +735,9 @@ zonkExpr env (HsWrap co_fn expr) zonkExpr _ (HsUnboundVar v) = return (HsUnboundVar v) + -- nothing to do here. The payload is an LHsType, not a Type. +zonkExpr _ e@(HsTypeOut {}) = return e + zonkExpr _ expr = pprPanic "zonkExpr" (ppr expr) ------------------------------------------------------------------------- @@ -740,10 +747,10 @@ zonkCmd :: ZonkEnv -> HsCmd TcId -> TcM (HsCmd Id) zonkLCmd env cmd = wrapLocM (zonkCmd env) cmd -zonkCmd env (HsCmdCast co cmd) - = do { co' <- zonkCoToCo env co - ; cmd' <- zonkCmd env cmd - ; return (HsCmdCast co' cmd') } +zonkCmd env (HsCmdWrap w cmd) + = do { (env1, w') <- zonkCoFn env w + ; cmd' <- zonkCmd env1 cmd + ; return (HsCmdWrap w' cmd') } zonkCmd env (HsCmdArrApp e1 e2 ty ho rl) = do new_e1 <- zonkLExpr env e1 new_e2 <- zonkLExpr env e2 @@ -811,11 +818,10 @@ zonkCoFn env WpHole = return (env, WpHole) zonkCoFn env (WpCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1 ; (env2, c2') <- zonkCoFn env1 c2 ; return (env2, WpCompose c1' c2') } -zonkCoFn env (WpFun c1 c2 t1 t2) = do { (env1, c1') <- zonkCoFn env c1 - ; (env2, c2') <- zonkCoFn env1 c2 - ; t1' <- zonkTcTypeToType env2 t1 - ; t2' <- zonkTcTypeToType env2 t2 - ; return (env2, WpFun c1' c2' t1' t2') } +zonkCoFn env (WpFun c1 c2 t1) = do { (env1, c1') <- zonkCoFn env c1 + ; (env2, c2') <- zonkCoFn env1 c2 + ; t1' <- zonkTcTypeToType env2 t1 + ; return (env2, WpFun c1' c2' t1') } zonkCoFn env (WpCast co) = do { co' <- zonkCoToCo env co ; return (env, WpCast co') } zonkCoFn env (WpEvLam ev) = do { (env', ev') <- zonkEvBndrX env ev diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs index 769c45f43d..6214a8a94d 100644 --- a/compiler/typecheck/TcHsType.hs +++ b/compiler/typecheck/TcHsType.hs @@ -15,6 +15,7 @@ module TcHsType ( tcHsClsInstType, tcHsDeriv, tcHsVectInst, + tcHsTypeApp, UserTypeCtxt(..), tcImplicitTKBndrs, tcImplicitTKBndrsType, tcHsTyVarBndrs, @@ -202,7 +203,7 @@ tc_hs_sig_type (HsIB { hsib_body = hs_ty = do { (tkvs, ty) <- solveEqualities $ tcImplicitTKBndrsType sig_vars $ tc_lhs_type typeLevelMode hs_ty kind - ; return (mkInvForAllTys tkvs ty) } + ; return (mkSpecForAllTys tkvs ty) } ----------------- tcHsDeriv :: LHsSigType Name -> TcM ([TyVar], Class, [Type], Kind) @@ -244,7 +245,7 @@ tcHsClsInstType user_ctxt hs_inst_ty@(HsIB { hsib_vars = sig_vars ; head_ty' <- tc_lhs_type typeLevelMode head_ty constraintKind ; return (mkPhiTy theta head_ty') } - ; let inst_ty = mkInvForAllTys tkvs phi_ty + ; let inst_ty = mkSpecForAllTys tkvs phi_ty ; inst_ty <- kindGeneralizeType inst_ty ; inst_ty <- zonkTcType inst_ty ; checkValidInstance user_ctxt hs_inst_ty inst_ty } @@ -267,6 +268,21 @@ tcHsVectInst ty | otherwise = failWithTc $ ptext (sLit "Malformed instance type") +---------------------------------------------- +-- | Type-check a visible type application +tcHsTypeApp :: LHsWcType Name -> Kind -> TcM Type +tcHsTypeApp wc_ty kind + | HsWC { hswc_wcs = sig_wcs, hswc_ctx = extra, hswc_body = hs_ty } <- wc_ty + = ASSERT( isNothing extra ) -- handled in RnTypes.rnExtraConstraintWildCard + tcWildCardBinders sig_wcs $ \ _ -> + do { ty <- tcCheckLHsType hs_ty kind + ; ty <- zonkTcType ty + ; checkValidType TypeAppCtxt ty + ; return ty } + -- NB: we don't call emitWildcardHoleConstraints here, because + -- we want any holes in visible type applications to be used + -- without fuss. No errors, warnings, extensions, etc. + {- These functions are used during knot-tying in type and class declarations, when we have to @@ -504,7 +520,7 @@ tc_hs_type mode hs_ty@(HsForAllTy { hst_bndrs = hs_tvs, hst_body = ty }) exp_kin -- Why exp_kind? See Note [Body kind of forall] do { ty' <- tc_lhs_type mode ty exp_kind ; let bound_vars = allBoundVariables ty' - ; return (mkNakedInvSigmaTy tvs' [] ty', bound_vars) } + ; return (mkNakedSpecSigmaTy tvs' [] ty', bound_vars) } tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = ty }) exp_kind = do { ctxt' <- tc_hs_context mode ctxt @@ -1275,12 +1291,15 @@ kcHsTyVarBndrs cusk (HsQTvs { hsq_implicit = kv_ns do { (full_kind, _, stuff) <- bind_telescope hs_tvs (thing_inside kvs) ; let qkvs = filter (not . isMetaTyVar) $ tyCoVarsOfTypeWellScoped full_kind + -- these have to be the vars made with new_skolem_tv + -- above. Thus, they are known to the user and should + -- be Specified, not Invisible, when kind-generalizing -- the free non-meta variables in the returned kind will -- contain both *mentioned* kind vars and *unmentioned* kind -- vars (See case (1) under Note [Typechecking telescopes]) gen_kind = if cusk - then mkInvForAllTys qkvs $ full_kind + then mkSpecForAllTys qkvs $ full_kind else full_kind ; return (gen_kind, stuff) } } where diff --git a/compiler/typecheck/TcInstDcls.hs b/compiler/typecheck/TcInstDcls.hs index 3b931711c3..007abf0804 100644 --- a/compiler/typecheck/TcInstDcls.hs +++ b/compiler/typecheck/TcInstDcls.hs @@ -872,7 +872,8 @@ tcInstDecl2 (InstInfo { iSpec = ispec, iBinds = ibinds }) | otherwise = SpecPrags spec_inst_prags - export = ABE { abe_wrap = idHsWrapper, abe_poly = dfun_id + export = ABE { abe_wrap = idHsWrapper, abe_inst_wrap = idHsWrapper + , abe_poly = dfun_id , abe_mono = self_dict, abe_prags = dfun_spec_prags } -- NB: see Note [SPECIALISE instance pragmas] main_bind = AbsBinds { abs_tvs = inst_tyvars @@ -986,7 +987,9 @@ tcSuperClasses dfun_id cls tyvars dfun_evs inst_tys dfun_ev_binds _fam_envs sc_t ; addTcEvBind ev_binds_var $ mkWantedEvBind sc_ev_id sc_ev_tm ; let sc_top_ty = mkInvForAllTys tyvars (mkPiTypes dfun_evs sc_pred) sc_top_id = mkLocalId sc_top_name sc_top_ty - export = ABE { abe_wrap = idHsWrapper, abe_poly = sc_top_id + export = ABE { abe_wrap = idHsWrapper + , abe_inst_wrap = idHsWrapper + , abe_poly = sc_top_id , abe_mono = sc_ev_id , abe_prags = SpecPrags [] } local_ev_binds = TcEvBinds ev_binds_var @@ -1318,7 +1321,8 @@ tcMethods dfun_id clas tyvars dfun_ev_vars inst_tys -- method to this version. Note [INLINE and default methods] - export = ABE { abe_wrap = hs_wrap, abe_poly = meth_id1 + export = ABE { abe_wrap = hs_wrap, abe_inst_wrap = idHsWrapper + , abe_poly = meth_id1 , abe_mono = local_meth_id , abe_prags = mk_meth_spec_prags meth_id1 spec_inst_prags [] } bind = AbsBinds { abs_tvs = tyvars, abs_ev_vars = dfun_ev_vars @@ -1374,10 +1378,11 @@ tcMethodBody clas tyvars dfun_ev_vars inst_tys (L bind_loc lm_bind) ; let specs = mk_meth_spec_prags global_meth_id spec_inst_prags spec_prags - export = ABE { abe_poly = global_meth_id - , abe_mono = local_meth_id - , abe_wrap = hs_wrap - , abe_prags = specs } + export = ABE { abe_poly = global_meth_id + , abe_mono = local_meth_id + , abe_wrap = hs_wrap + , abe_inst_wrap = idHsWrapper + , abe_prags = specs } local_ev_binds = TcEvBinds ev_binds_var full_bind = AbsBinds { abs_tvs = tyvars @@ -1417,7 +1422,7 @@ mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id do { inst_sigs <- xoptM LangExt.InstanceSigs ; checkTc inst_sigs (misplacedInstSig sel_name lhs_ty) ; sig_ty <- tcHsSigType (FunSigCtxt sel_name False) lhs_ty - ; let poly_sig_ty = mkInvSigmaTy tyvars theta sig_ty + ; let poly_sig_ty = mkSpecSigmaTy tyvars theta sig_ty ctxt = FunSigCtxt sel_name True ; tc_sig <- instTcTySig ctxt lhs_ty sig_ty local_meth_name ; hs_wrap <- addErrCtxtM (methSigCtxt sel_name poly_sig_ty poly_meth_ty) $ @@ -1438,7 +1443,7 @@ mkMethIds sig_fn clas tyvars dfun_ev_vars inst_tys sel_id sel_name = idName sel_id sel_occ = nameOccName sel_name local_meth_ty = instantiateMethod clas sel_id inst_tys - poly_meth_ty = mkInvSigmaTy tyvars theta local_meth_ty + poly_meth_ty = mkSpecSigmaTy tyvars theta local_meth_ty theta = map idType dfun_ev_vars methSigCtxt :: Name -> TcType -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc) diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs index 9285f9ae22..cacaab23d8 100644 --- a/compiler/typecheck/TcMType.hs +++ b/compiler/typecheck/TcMType.hs @@ -21,11 +21,11 @@ module TcMType ( newFlexiTyVarTys, -- Int -> Kind -> TcM [TcType] newOpenFlexiTyVarTy, newReturnTyVar, newReturnTyVarTy, - newMaybeReturnTyVarTy, newOpenReturnTyVar, newMetaKindVar, newMetaKindVars, cloneMetaTyVar, newFmvTyVar, newFskTyVar, + tauTvForReturnTv, readMetaTyVar, writeMetaTyVar, writeMetaTyVarRef, newMetaDetails, isFilledMetaTyVar, isUnfilledMetaTyVar, @@ -632,12 +632,6 @@ newReturnTyVar kind = newAnonMetaTyVar ReturnTv kind newReturnTyVarTy :: Kind -> TcM TcType newReturnTyVarTy kind = mkTyVarTy <$> newReturnTyVar kind --- | Either makes a normal Flexi or a ReturnTv Flexi -newMaybeReturnTyVarTy :: Bool -- True <=> make a ReturnTv - -> Kind -> TcM TcType -newMaybeReturnTyVarTy True = newReturnTyVarTy -newMaybeReturnTyVarTy False = newFlexiTyVarTy - -- | Create a tyvar that can be a lifted or unlifted type. newOpenFlexiTyVarTy :: TcM TcType newOpenFlexiTyVarTy @@ -652,6 +646,23 @@ newOpenReturnTyVar ; tv <- newReturnTyVar k ; return (tv, k) } +-- | If the type is a ReturnTv, fill it with a new meta-TauTv. Otherwise, +-- no change. This function can look through ReturnTvs and returns a partially +-- zonked type as an optimisation. +tauTvForReturnTv :: TcType -> TcM TcType +tauTvForReturnTv ty + | Just tv <- tcGetTyVar_maybe ty + , isReturnTyVar tv + = do { contents <- readMetaTyVar tv + ; case contents of + Flexi -> do { tau_ty <- newFlexiTyVarTy (tyVarKind tv) + ; writeMetaTyVar tv tau_ty + ; return tau_ty } + Indirect ty -> tauTvForReturnTv ty } + | otherwise + = ASSERT( all (not . isReturnTyVar) (tyCoVarsOfTypeList ty) ) + return ty + newMetaSigTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) newMetaSigTyVars = mapAccumLM newMetaSigTyVarX emptyTCvSubst @@ -671,9 +682,8 @@ newMetaTyVarX :: TCvSubst -> TyVar -> TcM (TCvSubst, TcTyVar) newMetaTyVarX subst tyvar = do { uniq <- newUnique -- See Note [Levity polymorphic variables accept foralls] - ; let info = if isLevityPolymorphic (tyVarKind tyvar) - then ReturnTv - else TauTv + ; let info | isLevityPolymorphic (tyVarKind tyvar) = ReturnTv + | otherwise = TauTv ; details <- newMetaDetails info ; let name = mkSystemName uniq (getOccName tyvar) -- See Note [Name of an instantiated type variable] diff --git a/compiler/typecheck/TcMatches.hs b/compiler/typecheck/TcMatches.hs index 323adceaaa..2e4078b4ee 100644 --- a/compiler/typecheck/TcMatches.hs +++ b/compiler/typecheck/TcMatches.hs @@ -9,6 +9,7 @@ TcMatches: Typecheck some @Matches@ {-# LANGUAGE CPP #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TupleSections #-} module TcMatches ( tcMatchesFun, tcGRHS, tcGRHSsPat, tcMatchesCase, tcMatchLambda, TcMatchCtxt(..), TcStmtChecker, TcExprStmtChecker, TcCmdStmtChecker, @@ -16,11 +17,10 @@ module TcMatches ( tcMatchesFun, tcGRHS, tcGRHSsPat, tcMatchesCase, tcMatchLambd tcDoStmt, tcGuardStmt ) where -import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRhoNC, tcInferRho, tcCheckId, - tcMonoExpr, tcMonoExprNC, tcPolyExpr ) +import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferSigmaNC, tcInferSigma + , tcCheckId, tcMonoExpr, tcMonoExprNC, tcPolyExpr ) import HsSyn -import BasicTypes import TcRnMonad import TcEnv import TcPat @@ -47,6 +47,10 @@ import MkCore import Control.Monad +#if __GLASGOW_HASKELL__ < 709 +import Data.Traversable ( traverse ) +#endif + #include "HsVersions.h" {- @@ -64,7 +68,7 @@ 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 tcGen to skolemise it. +so it must be prepared to use tcSkolemise to skolemise it. See Note [sig_tau may be polymorphic] in TcPat. -} @@ -83,11 +87,14 @@ tcMatchesFun fun_name matches exp_ty traceTc "tcMatchesFun" (ppr fun_name $$ ppr exp_ty) ; checkArgs fun_name matches + ; exp_ty <- tauifyMultipleMatches matches exp_ty ; (wrap_gen, (wrap_fun, group)) - <- tcGen (FunSigCtxt fun_name True) exp_ty $ \ _ exp_rho -> + <- tcSkolemise (FunSigCtxt fun_name True) exp_ty $ \ _ exp_rho -> -- Note [Polymorphic expected type for tcMatchesFun] - matchFunTys herald arity exp_rho $ \ pat_tys rhs_ty -> - tcMatches match_ctxt pat_tys rhs_ty matches + do { (wrap_fun, pat_tys, rhs_ty) + <- matchExpectedFunTys herald arity exp_rho + ; matches' <- tcMatches match_ctxt pat_tys rhs_ty matches + ; return (wrap_fun, matches') } ; return (wrap_gen <.> wrap_fun, group) } where arity = matchGroupArity matches @@ -102,33 +109,38 @@ parser guarantees that each equation has exactly one argument. tcMatchesCase :: (Outputable (body Name)) => TcMatchCtxt body -- Case context - -> TcRhoType -- Type of scrutinee + -> TcSigmaType -- Type of scrutinee -> MatchGroup Name (Located (body Name)) -- The case alternatives -> TcRhoType -- Type of whole case expressions - -> TcM (MatchGroup TcId (Located (body TcId))) -- Translated alternatives + -> TcM (MatchGroup TcId (Located (body TcId))) + -- Translated alternatives + -- wrapper goes from MatchGroup's ty to expected ty tcMatchesCase ctxt scrut_ty matches res_ty | isEmptyMatchGroup matches -- Allow empty case expressions - = return (MG { mg_alts = noLoc [], mg_arg_tys = [scrut_ty] - , mg_res_ty = res_ty, mg_origin = mg_origin matches }) + = return (MG { mg_alts = noLoc [] + , mg_arg_tys = [scrut_ty] + , mg_res_ty = res_ty + , mg_origin = mg_origin matches }) | otherwise - = tcMatches ctxt [scrut_ty] res_ty matches - -tcMatchLambda :: MatchGroup Name (LHsExpr Name) -> TcRhoType - -> TcM (HsWrapper, MatchGroup TcId (LHsExpr TcId)) -tcMatchLambda match res_ty - = matchFunTys herald n_pats res_ty $ \ pat_tys rhs_ty -> - tcMatches match_ctxt pat_tys rhs_ty match + = do { res_ty <- tauifyMultipleMatches matches res_ty + ; tcMatches ctxt [scrut_ty] res_ty matches } + +tcMatchLambda :: SDoc -- see Note [Herald for matchExpectedFunTys] in TcUnify + -> TcMatchCtxt HsExpr + -> MatchGroup Name (LHsExpr Name) + -> TcRhoType -- deeply skolemised + -> TcM (HsWrapper, [TcSigmaType], MatchGroup TcId (LHsExpr TcId)) + -- also returns the argument types +tcMatchLambda herald match_ctxt match res_ty + = do { res_ty <- tauifyMultipleMatches match res_ty + ; (wrap, pat_tys, rhs_ty) <- matchExpectedFunTys herald n_pats res_ty + ; match' <- tcMatches match_ctxt pat_tys rhs_ty match + ; return (wrap, pat_tys, match') } where - n_pats = matchGroupArity match - herald = sep [ ptext (sLit "The lambda expression") - <+> quotes (pprSetDepth (PartWay 1) $ - pprMatches (LambdaExpr :: HsMatchContext Name) match), - -- The pprSetDepth makes the abstraction print briefly - ptext (sLit "has")] - match_ctxt = MC { mc_what = LambdaExpr, - mc_body = tcBody } + n_pats | isEmptyMatchGroup match = 1 -- must be lambda-case + | otherwise = matchGroupArity match -- @tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@. @@ -140,29 +152,59 @@ tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss res_ty match_ctxt = MC { mc_what = PatBindRhs, mc_body = tcBody } -matchFunTys - :: SDoc -- See Note [Herald for matchExpecteFunTys] in TcUnify - -> Arity - -> TcRhoType - -> ([TcSigmaType] -> TcRhoType -> TcM a) - -> TcM (HsWrapper, a) - --- Written in CPS style for historical reasons; --- could probably be un-CPSd, like matchExpectedTyConApp - -matchFunTys herald arity res_ty thing_inside - = do { (co, pat_tys, res_ty) <- matchExpectedFunTys herald arity res_ty - ; res <- thing_inside pat_tys res_ty - ; return (mkWpCastN (mkTcSymCo co), res) } - {- ************************************************************************ * * \subsection{tcMatch} * * ************************************************************************ + +Note [Case branches must be taus] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + + case ... of + ... -> \(x :: forall a. a -> a) -> x + ... -> \y -> y + +Should that type-check? The problem is that, if we check the second branch +first, then we'll get a type (b -> b) for the branches, which won't unify +with the polytype in the first branch. If we check the first branch first, +then everything is OK. This order-dependency is terrible. So we want only +proper tau-types in branches. This is what tauTvForReturnsTv ensures: +it gets rid of those pesky ReturnTvs that might unify with polytypes. + +An even trickier case looks like + + f x True = x undefined + f x False = x () + +Here, we see that the arguments must also be non-ReturnTvs. Thus, we must +tauify before calling matchFunTys. + +But we make a special case for a one-branch case. This is so that + + f = \(x :: forall a. a -> a) -> x + +still gets assigned a polytype. -} +-- | When the MatchGroup has multiple RHSs, convert any ReturnTvs in the +-- expected type into TauTvs. +-- See Note [Case branches must be taus] +tauifyMultipleMatches :: MatchGroup id body + -> TcType + -> TcM TcType +tauifyMultipleMatches group exp_ty + | isSingletonMatchGroup group + = return exp_ty + + | otherwise + = tauTvForReturnTv exp_ty + +-- | Type-check a MatchGroup. If there are multiple RHSs, the expected type +-- must already be tauified. See Note [Case branches must be taus] and +-- tauifyMultipleMatches tcMatches :: (Outputable (body Name)) => TcMatchCtxt body -> [TcSigmaType] -- Expected pattern types -> TcRhoType -- Expected result-type of the Match. @@ -176,11 +218,14 @@ data TcMatchCtxt body -- c.f. TcStmtCtxt, also in this module -> TcRhoType -> TcM (Located (body TcId)) } -tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches, mg_origin = origin }) +tcMatches ctxt pat_tys rhs_ty (MG { mg_alts = L l matches + , mg_origin = origin }) = ASSERT( not (null matches) ) -- Ensure that rhs_ty is filled in - do { matches' <- mapM (tcMatch ctxt pat_tys rhs_ty) matches - ; return (MG { mg_alts = L l matches', mg_arg_tys = pat_tys - , mg_res_ty = rhs_ty, mg_origin = origin }) } + do { matches' <- mapM (tcMatch ctxt pat_tys rhs_ty) matches + ; return (MG { mg_alts = L l matches' + , mg_arg_tys = pat_tys + , mg_res_ty = rhs_ty + , mg_origin = origin }) } ------------- tcMatch :: (Outputable (body Name)) => TcMatchCtxt body @@ -223,8 +268,9 @@ tcGRHSs :: TcMatchCtxt body -> GRHSs Name (Located (body Name)) -> TcRhoType -- but we don't need to do that any more tcGRHSs ctxt (GRHSs grhss (L l binds)) res_ty - = do { (binds', grhss') <- tcLocalBinds binds $ - mapM (wrapLocM (tcGRHS ctxt res_ty)) grhss + = do { (binds', grhss') + <- tcLocalBinds binds $ + mapM (wrapLocM (tcGRHS ctxt res_ty)) grhss ; return (GRHSs grhss' (L l binds')) } @@ -233,8 +279,9 @@ tcGRHS :: TcMatchCtxt body -> TcRhoType -> GRHS Name (Located (body Name)) -> TcM (GRHS TcId (Located (body TcId))) tcGRHS ctxt res_ty (GRHS guards rhs) - = do { (guards', rhs') <- tcStmtsAndThen stmt_ctxt tcGuardStmt guards res_ty $ - mc_body ctxt rhs + = do { (guards', rhs') + <- tcStmtsAndThen stmt_ctxt tcGuardStmt guards res_ty $ + mc_body ctxt rhs ; return (GRHS guards' rhs') } where stmt_ctxt = PatGuard (mc_what ctxt) @@ -280,8 +327,7 @@ tcDoStmts ctxt _ _ = pprPanic "tcDoStmts" (pprStmtContext ctxt) tcBody :: LHsExpr Name -> TcRhoType -> TcM (LHsExpr TcId) tcBody body res_ty = do { traceTc "tcBody" (ppr res_ty) - ; body' <- tcMonoExpr body res_ty - ; return body' + ; tcMonoExpr body res_ty } {- @@ -348,9 +394,9 @@ tcStmtsAndThen ctxt stmt_chk (L loc stmt : stmts) res_ty thing_inside | otherwise = do { (stmt', (stmts', thing)) <- setSrcSpan loc $ - addErrCtxt (pprStmtInCtxt ctxt stmt) $ + addErrCtxt (pprStmtInCtxt ctxt stmt) $ stmt_chk ctxt stmt res_ty $ \ res_ty' -> - popErrCtxt $ + popErrCtxt $ tcStmtsAndThen ctxt stmt_chk stmts res_ty' $ thing_inside ; return (L loc stmt' : stmts', thing) } @@ -366,8 +412,10 @@ tcGuardStmt _ (BodyStmt guard _ _ _) res_ty thing_inside ; return (BodyStmt guard' noSyntaxExpr noSyntaxExpr boolTy, thing) } tcGuardStmt ctxt (BindStmt pat rhs _ _) res_ty thing_inside - = do { (rhs', rhs_ty) <- tcInferRhoNC rhs -- Stmt has a context already - ; (pat', thing) <- tcPat (StmtCtxt ctxt) pat rhs_ty $ + = do { (rhs', rhs_ty) <- tcInferSigmaNC rhs + -- Stmt has a context already + ; (pat', thing) <- tcPat_O (StmtCtxt ctxt) (exprCtOrigin (unLoc rhs)) + pat rhs_ty $ thing_inside res_ty ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) } @@ -437,9 +485,7 @@ tcLcStmt m_tc ctxt (TransStmt { trS_form = form, trS_stmts = stmts -- passed in to tcStmtsAndThen is never looked at ; (stmts', (bndr_ids, by')) <- tcStmtsAndThen (TransStmtCtxt ctxt) (tcLcStmt m_tc) stmts unused_ty $ \_ -> do - { by' <- case by of - Nothing -> return Nothing - Just e -> do { e_ty <- tcInferRho e; return (Just e_ty) } + { by' <- traverse tcInferSigma by ; bndr_ids <- tcLookupLocalIds bndr_names ; return (bndr_ids, by') } diff --git a/compiler/typecheck/TcPat.hs b/compiler/typecheck/TcPat.hs index b951ad2197..a5da75c84d 100644 --- a/compiler/typecheck/TcPat.hs +++ b/compiler/typecheck/TcPat.hs @@ -11,12 +11,12 @@ TcPat: Typechecking patterns module TcPat ( tcLetPat, TcSigFun , TcPragEnv, lookupPragEnv, emptyPragEnv , LetBndrSpec(..), addInlinePrags - , tcPat, tcPats, newNoSigLetBndr + , tcPat, tcPat_O, tcPats, newNoSigLetBndr , addDataConStupidTheta, badFieldCon, polyPatSig ) where #include "HsVersions.h" -import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferRho) +import {-# SOURCE #-} TcExpr( tcSyntaxOp, tcInferSigma ) import HsSyn import TcHsSyn @@ -67,7 +67,8 @@ tcLetPat sig_fn no_gen pat pat_ty thing_inside = tc_lpat pat pat_ty penv thing_inside where penv = PE { pe_lazy = True - , pe_ctxt = LetPat sig_fn no_gen } + , pe_ctxt = LetPat sig_fn no_gen + , pe_orig = PatOrigin } ----------------- tcPats :: HsMatchContext Name @@ -90,23 +91,31 @@ tcPats :: HsMatchContext Name tcPats ctxt pats pat_tys thing_inside = tc_lpats penv pats pat_tys thing_inside where - penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt } + penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin } tcPat :: HsMatchContext Name -> LPat Name -> TcSigmaType - -> TcM a -- Checker for body, given - -- its result type + -> TcM a -- Checker for body -> TcM (LPat TcId, a) -tcPat ctxt pat pat_ty thing_inside +tcPat ctxt = tcPat_O ctxt PatOrigin + +-- | A variant of 'tcPat' that takes a custom origin +tcPat_O :: HsMatchContext Name + -> CtOrigin -- ^ origin to use if the type needs inst'ing + -> LPat Name -> TcSigmaType + -> TcM a -- Checker for body + -> TcM (LPat TcId, a) +tcPat_O ctxt orig pat pat_ty thing_inside = tc_lpat pat pat_ty penv thing_inside where - penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt } + penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig } ----------------- data PatEnv = PE { pe_lazy :: Bool -- True <=> lazy context, so no existentials allowed , pe_ctxt :: PatCtxt -- Context in which the whole pattern appears + , pe_orig :: CtOrigin -- origin to use if the pat_ty needs inst'ing } data PatCtxt @@ -171,6 +180,8 @@ tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty = return (mkTcNomReflCo pat_ty, mkLocalId bndr_name pat_ty) + -- whether or not there is a sig is irrelevant, as this + -- is local ------------ newNoSigLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId @@ -369,26 +380,20 @@ tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside tc_pat penv (ViewPat expr pat _) overall_pat_ty thing_inside = do { - -- Morally, expr must have type `forall a1...aN. OPT' -> B` + -- Expr must have type `forall a1...aN. OPT' -> B` -- where overall_pat_ty is an instance of OPT'. - -- Here, we infer a rho type for it, - -- which replaces the leading foralls and constraints - -- with fresh unification variables. - ; (expr',expr'_inferred) <- tcInferRho expr + ; (expr',expr'_inferred) <- tcInferSigma expr -- next, we check that expr is coercible to `overall_pat_ty -> pat_ty` - -- NOTE: this forces pat_ty to be a monotype (because we use a unification - -- variable to find it). this means that in an example like - -- (view -> f) where view :: _ -> forall b. b - -- we will only be able to use view at one instantation in the - -- rest of the view - ; (expr_co, pat_ty) <- tcInfer $ \ pat_ty -> - unifyType (Just expr) expr'_inferred (mkFunTy overall_pat_ty pat_ty) + ; (expr_wrap, pat_ty) <- tcInfer $ \ pat_ty -> + tcSubTypeDS_O (exprCtOrigin (unLoc expr)) GenSigCtxt (Just expr) + expr'_inferred + (mkFunTy overall_pat_ty pat_ty) -- pattern must have pat_ty ; (pat', res) <- tc_lpat pat pat_ty penv thing_inside - ; return (ViewPat (mkLHsWrapCo expr_co expr') pat' overall_pat_ty, res) } + ; return (ViewPat (mkLHsWrap expr_wrap expr') pat' overall_pat_ty, res) } -- Type signatures in patterns -- See Note [Pattern coercions] below @@ -403,7 +408,7 @@ tc_pat penv (SigPatIn pat sig_ty) pat_ty thing_inside ------------------------ -- Lists, tuples, arrays tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside - = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTyR pat_ty + = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv pat_ty ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty) pats penv thing_inside ; return (mkHsWrapPat coi (ListPat pats' elt_ty Nothing) pat_ty, res) @@ -412,14 +417,14 @@ tc_pat penv (ListPat pats _ Nothing) pat_ty thing_inside tc_pat penv (ListPat pats _ (Just (_,e))) pat_ty thing_inside = do { list_pat_ty <- newFlexiTyVarTy liftedTypeKind ; e' <- tcSyntaxOp ListOrigin e (mkFunTy pat_ty list_pat_ty) - ; (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTyR list_pat_ty + ; (coi, elt_ty) <- matchExpectedPatTy matchExpectedListTy penv list_pat_ty ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty) pats penv thing_inside ; return (mkHsWrapPat coi (ListPat pats' elt_ty (Just (pat_ty,e'))) list_pat_ty, res) } tc_pat penv (PArrPat pats _) pat_ty thing_inside - = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTyR pat_ty + = do { (coi, elt_ty) <- matchExpectedPatTy matchExpectedPArrTy penv pat_ty ; (pats', res) <- tcMultiple (\p -> tc_lpat p elt_ty) pats penv thing_inside ; return (mkHsWrapPat coi (PArrPat pats' elt_ty) pat_ty, res) @@ -428,7 +433,8 @@ tc_pat penv (PArrPat pats _) pat_ty thing_inside tc_pat penv (TuplePat pats boxity _) pat_ty thing_inside = do { let arity = length pats tc = tupleTyCon boxity arity - ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConAppR tc) pat_ty + ; (coi, arg_tys) <- matchExpectedPatTy (matchExpectedTyConApp tc) + penv pat_ty -- Unboxed tuples have levity vars, which we discard: -- See Note [Unboxed tuple levity vars] in TyCon ; let con_arg_tys = case boxity of Unboxed -> drop arity arg_tys @@ -470,9 +476,10 @@ tc_pat _ (LitPat simple_lit) pat_ty thing_inside ------------------------ -- Overloaded patterns: n, and n+k -tc_pat _ (NPat (L l over_lit) mb_neg eq) pat_ty thing_inside +tc_pat (PE { pe_orig = pat_orig }) + (NPat (L l over_lit) mb_neg eq) pat_ty thing_inside = do { let orig = LiteralOrigin over_lit - ; lit' <- newOverloadedLit orig over_lit pat_ty + ; (wrap, lit') <- newOverloadedLit over_lit pat_ty pat_orig ; eq' <- tcSyntaxOp orig eq (mkFunTys [pat_ty, pat_ty] boolTy) ; mb_neg' <- case mb_neg of Nothing -> return Nothing -- Positive literal @@ -481,18 +488,22 @@ tc_pat _ (NPat (L l over_lit) mb_neg eq) pat_ty thing_inside do { neg' <- tcSyntaxOp orig neg (mkFunTy pat_ty pat_ty) ; return (Just neg') } ; res <- thing_inside - ; return (NPat (L l lit') mb_neg' eq', res) } + ; return (mkHsWrapPat wrap (NPat (L l lit') mb_neg' eq') pat_ty, res) } tc_pat penv (NPlusKPat (L nm_loc name) (L loc lit) ge minus) pat_ty thing_inside = do { (co, bndr_id) <- setSrcSpan nm_loc (tcPatBndr penv name pat_ty) ; let pat_ty' = idType bndr_id orig = LiteralOrigin lit - ; lit' <- newOverloadedLit orig lit pat_ty' + ; (wrap_lit, lit') <- newOverloadedLit lit pat_ty' (pe_orig penv) -- The '>=' and '-' parts are re-mappable syntax ; ge' <- tcSyntaxOp orig ge (mkFunTys [pat_ty', pat_ty'] boolTy) ; minus' <- tcSyntaxOp orig minus (mkFunTys [pat_ty', pat_ty'] pat_ty') - ; let pat' = NPlusKPat (L nm_loc bndr_id) (L loc lit') ge' minus' + ; let pat' = mkHsWrapPat wrap_lit + (NPlusKPat (L nm_loc bndr_id) + (L loc lit') + ge' minus') + pat_ty -- The Report says that n+k patterns must be in Integral -- We may not want this when using re-mappable syntax, though (ToDo?) @@ -630,7 +641,7 @@ tcDataConPat penv (L con_span con_name) data_con pat_ty arg_pats thing_inside -- Instantiate the constructor type variables [a->ty] -- This may involve doing a family-instance coercion, -- and building a wrapper - ; (wrap, ctxt_res_tys) <- matchExpectedPatTy (matchExpectedConTy tycon) pat_ty + ; (wrap, ctxt_res_tys) <- matchExpectedConTy penv tycon pat_ty -- Add the stupid theta ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys @@ -750,57 +761,36 @@ tcPatSynPat penv (L con_span _) pat_syn pat_ty arg_pats thing_inside ; return (mkHsWrapPat wrap res_pat pat_ty, res) } ---------------------------- -downgrade :: (TcRhoType -> TcM (TcCoercionN, a)) - -> TcRhoType -> TcM (TcCoercionR, a) -downgrade f a = do { (co,res) <- f a; return (mkTcSubCo co, res) } - -matchExpectedListTyR :: TcRhoType -> TcM (TcCoercionR, TcRhoType) -matchExpectedListTyR = downgrade matchExpectedListTy -matchExpectedPArrTyR :: TcRhoType -> TcM (TcCoercionR, TcRhoType) -matchExpectedPArrTyR = downgrade matchExpectedPArrTy -matchExpectedTyConAppR :: TyCon -> TcRhoType -> TcM (TcCoercionR, [TcSigmaType]) -matchExpectedTyConAppR tc = downgrade (matchExpectedTyConApp tc) - ----------------------------- -matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionR, a)) - -> TcRhoType -- Type of the pattern - -> TcM (HsWrapper, a) +-- | Convenient wrapper for calling a matchExpectedXXX function +matchExpectedPatTy :: (TcRhoType -> TcM (TcCoercionN, a)) + -> PatEnv -> TcSigmaType -> TcM (HsWrapper, a) -- See Note [Matching polytyped patterns] -- Returns a wrapper : pat_ty ~R inner_ty -matchExpectedPatTy inner_match pat_ty - | null tvs && null theta - = do { (co, res) <- inner_match pat_ty -- 'co' is Representational - ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr co $$ ppr (isTcReflCo co)) - ; return (mkWpCastR (mkTcSymCo co), res) } - -- The Sym is because the inner_match returns a coercion - -- that is the other way round to matchExpectedPatTy - - | otherwise - = do { (subst, tvs') <- newMetaTyVars tvs - ; wrap1 <- instCall PatOrigin (mkTyVarTys tvs') (substTheta subst theta) - ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau) - ; return (wrap2 <.> wrap1, arg_tys) } - where - (tvs, theta, tau) = tcSplitSigmaTy pat_ty +matchExpectedPatTy inner_match (PE { pe_orig = orig }) pat_ty + = do { (wrap, pat_rho) <- topInstantiate orig pat_ty + ; (co, res) <- inner_match pat_rho + ; traceTc "matchExpectedPatTy" (ppr pat_ty $$ ppr wrap) + ; return (mkWpCastN (mkTcSymCo co) <.> wrap, res) } ---------------------------- -matchExpectedConTy :: TyCon -- The TyCon that this data +matchExpectedConTy :: PatEnv + -> TyCon -- The TyCon that this data -- constructor actually returns -- In the case of a data family this is -- the /representation/ TyCon - -> TcRhoType -- The type of the pattern; in the case - -- of a data family this would mention - -- the /family/ TyCon - -> TcM (TcCoercionR, [TcSigmaType]) + -> TcSigmaType -- The type of the pattern; in the case + -- of a data family this would mention + -- the /family/ TyCon + -> TcM (HsWrapper, [TcSigmaType]) -- See Note [Matching constructor patterns] --- Returns a coercion : T ty1 ... tyn ~R pat_ty --- This is the same way round as matchExpectedListTy etc --- but the other way round to matchExpectedPatTy -matchExpectedConTy data_tc pat_ty +-- Returns a wrapper : pat_ty "->" T ty1 ... tyn +matchExpectedConTy (PE { pe_orig = orig }) data_tc pat_ty | Just (fam_tc, fam_args, co_tc) <- tyConFamInstSig_maybe data_tc -- Comments refer to Note [Matching constructor patterns] -- co_tc :: forall a. T [a] ~ T7 a - = do { (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc) + = do { (wrap, pat_ty) <- topInstantiate orig pat_ty + + ; (subst, tvs') <- newMetaTyVars (tyConTyVars data_tc) -- tys = [ty1,ty2] ; traceTc "matchExpectedConTy" (vcat [ppr data_tc, @@ -808,16 +798,21 @@ matchExpectedConTy data_tc pat_ty ppr fam_tc, ppr fam_args]) ; co1 <- unifyType noThing (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty -- co1 : T (ty1,ty2) ~N pat_ty + -- could use tcSubType here... but it's the wrong way round + -- for actual vs. expected in error messages. ; let tys' = mkTyVarTys tvs' co2 = mkTcUnbranchedAxInstCo co_tc tys' [] -- co2 : T (ty1,ty2) ~R T7 ty1 ty2 - ; return (mkTcSymCo co2 `mkTcTransCo` mkTcSubCo co1, tys') } + ; return ( wrap <.> (mkWpCastR $ + mkTcSubCo (mkTcSymCo co1) `mkTcTransCo` co2) + , tys') } | otherwise - = matchExpectedTyConAppR data_tc pat_ty - -- coi : T tys ~R pat_ty + = do { (wrap, pat_rho) <- topInstantiate orig pat_ty + ; (coi, tys) <- matchExpectedTyConApp data_tc pat_rho + ; return (mkWpCastN (mkTcSymCo coi) <.> wrap, tys) } {- Note [Matching constructor patterns] diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 5f9225030b..9444ef241a 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -39,7 +39,6 @@ import TcEvidence import BuildTyCl import VarSet import MkId -import Inst import TcTyDecls import ConLike import FieldLabel @@ -209,7 +208,7 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, req_theta = map evVarPred req_dicts ; traceTc "tcInferPatSynDecl }" $ ppr name - ; tc_patsyn_finish lname dir is_infix lpat' + ; tc_patsyn_finish lname dir False {- no sig -} is_infix lpat' (univ_tvs, req_theta, ev_binds, req_dicts) (ex_tvs, mkTyVarTys ex_tvs, prov_theta, map EvId prov_dicts) (map nlHsVar args, map idType args) @@ -268,7 +267,7 @@ tcCheckPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details -- when that should be impossible ; traceTc "tcCheckPatSynDecl }" $ ppr name - ; tc_patsyn_finish lname dir is_infix lpat' + ; tc_patsyn_finish lname dir True {- has a sig -} is_infix lpat' (univ_tvs, req_theta, ev_binds, req_dicts) (ex_tvs, mkTyVarTys ex_tvs', prov_theta, prov_dicts) (args', arg_tys) @@ -365,6 +364,7 @@ wrongNumberOfParmsErr name decl_arity ty_arity -- Shared by both tcInferPatSyn and tcCheckPatSyn tc_patsyn_finish :: Located Name -- ^ PatSyn Name -> HsPatSynDir Name -- ^ PatSyn type (Uni/Bidir/ExplicitBidir) + -> Bool -- ^ True <=> signature provided -> Bool -- ^ Whether infix -> LPat Id -- ^ Pattern of the PatSyn -> ([TcTyVar], [PredType], TcEvBinds, [EvVar]) @@ -374,7 +374,7 @@ tc_patsyn_finish :: Located Name -- ^ PatSyn Name -> [Name] -- ^ Selector names -- ^ Whether fields, empty if not record PatSyn -> TcM (LHsBinds Id, TcGblEnv) -tc_patsyn_finish lname dir is_infix lpat' +tc_patsyn_finish lname dir has_sig is_infix lpat' (univ_tvs, req_theta, req_ev_binds, req_dicts) (ex_tvs, ex_tys, prov_theta, prov_dicts) (args, arg_tys) @@ -402,7 +402,7 @@ tc_patsyn_finish lname dir is_infix lpat' ppr pat_ty -- Make the 'matcher' - ; (matcher_id, matcher_bind) <- tcPatSynMatcher lname lpat' + ; (matcher_id, matcher_bind) <- tcPatSynMatcher has_sig lname lpat' (univ_tvs, req_theta, req_ev_binds, req_dicts) (ex_tvs, ex_tys, prov_theta, prov_dicts) (args, arg_tys) @@ -410,7 +410,7 @@ tc_patsyn_finish lname dir is_infix lpat' -- Make the 'builder' - ; builder_id <- mkPatSynBuilderId dir lname qtvs theta + ; builder_id <- mkPatSynBuilderId has_sig dir lname qtvs theta arg_tys pat_ty -- TODO: Make this have the proper information @@ -447,7 +447,8 @@ tc_patsyn_finish lname dir is_infix lpat' ************************************************************************ -} -tcPatSynMatcher :: Located Name +tcPatSynMatcher :: Bool -- True <=> signature provided + -> Located Name -> LPat Id -> ([TcTyVar], ThetaType, TcEvBinds, [EvVar]) -> ([TcTyVar], [TcType], ThetaType, [EvTerm]) @@ -455,7 +456,7 @@ tcPatSynMatcher :: Located Name -> TcType -> TcM ((Id, Bool), LHsBinds Id) -- See Note [Matchers and builders for pattern synonyms] in PatSyn -tcPatSynMatcher (L loc name) lpat +tcPatSynMatcher has_sig (L loc name) lpat (univ_tvs, req_theta, req_ev_binds, req_dicts) (ex_tvs, ex_tys, prov_theta, prov_dicts) (args, arg_tys) pat_ty @@ -471,10 +472,11 @@ tcPatSynMatcher (L loc name) lpat (cont_args, cont_arg_tys) | is_unlifted = ([nlHsVar voidPrimId], [voidPrimTy]) | otherwise = (args, arg_tys) - cont_ty = mkInvSigmaTy ex_tvs prov_theta $ + mk_sigma = if has_sig then mkSpecSigmaTy else mkInvSigmaTy + cont_ty = mk_sigma ex_tvs prov_theta $ mkFunTys cont_arg_tys res_ty - fail_ty = mkFunTy voidPrimTy res_ty + fail_ty = mkFunTy voidPrimTy res_ty ; matcher_name <- newImplicitBinder name mkMatcherOcc ; scrutinee <- newSysLocalId (fsLit "scrut") pat_ty @@ -555,22 +557,25 @@ isUnidirectional ExplicitBidirectional{} = False ************************************************************************ -} -mkPatSynBuilderId :: HsPatSynDir a -> Located Name +mkPatSynBuilderId :: Bool -- True <=> signature provided + -> HsPatSynDir a -> Located Name -> [TyVar] -> ThetaType -> [Type] -> Type -> TcM (Maybe (Id, Bool)) -mkPatSynBuilderId dir (L _ name) qtvs theta arg_tys pat_ty +mkPatSynBuilderId has_sig dir (L _ name) qtvs theta arg_tys pat_ty | isUnidirectional dir = return Nothing | otherwise = do { builder_name <- newImplicitBinder name mkBuilderOcc - ; let builder_sigma = mkInvSigmaTy qtvs theta (mkFunTys builder_arg_tys pat_ty) + ; let mk_sigma = if has_sig then mkSpecSigmaTy else mkInvSigmaTy + builder_sigma = add_void $ + mk_sigma qtvs theta (mkFunTys arg_tys pat_ty) builder_id = -- See Note [Exported LocalIds] in Id mkExportedLocalId VanillaId builder_name builder_sigma ; return (Just (builder_id, need_dummy_arg)) } where - builder_arg_tys | need_dummy_arg = [voidPrimTy] - | otherwise = arg_tys + add_void | need_dummy_arg = mkFunTy voidPrimTy + | otherwise = id need_dummy_arg = isUnLiftedType pat_ty && null arg_tys && null theta tcPatSynBuilderBind :: PatSynBind Name Name @@ -626,7 +631,8 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat InfixPatSyn arg1 arg2 -> [arg1, arg2] RecordPatSyn args -> map recordPatSynPatVar args - add_dummy_arg :: MatchGroup Name (LHsExpr Name) -> MatchGroup Name (LHsExpr Name) + add_dummy_arg :: MatchGroup Name (LHsExpr Name) + -> MatchGroup Name (LHsExpr Name) add_dummy_arg mg@(MG { mg_alts = L l [L loc (Match NonFunBindMatch [] ty grhss)] }) = mg { mg_alts @@ -634,19 +640,20 @@ tcPatSynBuilderBind PSB{ psb_id = L loc name, psb_def = lpat add_dummy_arg other_mg = pprPanic "add_dummy_arg" $ pprMatches (PatSyn :: HsMatchContext Name) other_mg -tcPatSynBuilderOcc :: CtOrigin -> PatSyn -> TcM (HsExpr TcId, TcRhoType) --- The result type should be fully instantiated -tcPatSynBuilderOcc orig ps +tcPatSynBuilderOcc :: PatSyn -> TcM (HsExpr TcId, TcSigmaType) +-- monadic only for failure +tcPatSynBuilderOcc ps | Just (builder_id, add_void_arg) <- builder - = do { (wrap, rho) <- deeplyInstantiate orig (idType builder_id) - ; let inst_fun = mkHsWrap wrap (HsVar (noLoc builder_id)) - ; if add_void_arg - then return ( HsApp (noLoc inst_fun) (nlHsVar voidPrimId) - , tcFunResultTy rho ) - else return ( inst_fun, rho ) } + , let builder_expr = HsVar (noLoc builder_id) + builder_ty = idType builder_id + = return $ + if add_void_arg + then ( HsApp (noLoc $ builder_expr) (nlHsVar voidPrimId) + , tcFunResultTy builder_ty ) + else (builder_expr, builder_ty) | otherwise -- Unidirectional - = nonBidirectionalErr name + = nonBidirectionalErr name where name = patSynName ps builder = patSynBuilder ps @@ -836,4 +843,3 @@ tcCollectEx pat = go pat goRecFd :: LHsRecField Id (LPat Id) -> (TyVarSet, [EvVar]) goRecFd (L _ HsRecField{ hsRecFieldArg = p }) = go p - diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs index 8764c33dcf..823bd38bb2 100644 --- a/compiler/typecheck/TcRnDriver.hs +++ b/compiler/typecheck/TcRnDriver.hs @@ -1974,7 +1974,7 @@ tcRnExpr hsc_env rdr_expr uniq <- newUnique ; let { fresh_it = itName uniq (getLoc rdr_expr) } ; (tclvl, lie, (_tc_expr, res_ty)) <- pushLevelAndCaptureConstraints $ - tcInferRho rn_expr ; + tcInferSigma rn_expr ; ((qtvs, dicts, _), lie_top) <- captureConstraints $ {-# SCC "simplifyInfer" #-} simplifyInfer tclvl diff --git a/compiler/typecheck/TcRnMonad.hs b/compiler/typecheck/TcRnMonad.hs index f5d5ed553b..7ce60bc852 100644 --- a/compiler/typecheck/TcRnMonad.hs +++ b/compiler/typecheck/TcRnMonad.hs @@ -972,14 +972,26 @@ getErrCtxt = do { env <- getLclEnv; return (tcl_ctxt env) } setErrCtxt :: [ErrCtxt] -> TcM a -> TcM a setErrCtxt ctxt = updLclEnv (\ env -> env { tcl_ctxt = ctxt }) +-- | Add a fixed message to the error context. This message should not +-- do any tidying. addErrCtxt :: MsgDoc -> TcM a -> TcM a addErrCtxt msg = addErrCtxtM (\env -> return (env, msg)) +-- | Add a message to the error context. This message may do tidying. addErrCtxtM :: (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a addErrCtxtM ctxt = updCtxt (\ ctxts -> (False, ctxt) : ctxts) +-- | Add a fixed landmark message to the error context. A landmark +-- message is always sure to be reported, even if there is a lot of +-- context. It also doesn't count toward the maximum number of contexts +-- reported. addLandmarkErrCtxt :: MsgDoc -> TcM a -> TcM a -addLandmarkErrCtxt msg = updCtxt (\ctxts -> (True, \env -> return (env,msg)) : ctxts) +addLandmarkErrCtxt msg = addLandmarkErrCtxtM (\env -> return (env, msg)) + +-- | Variant of 'addLandmarkErrCtxt' that allows for monadic operations +-- and tidying. +addLandmarkErrCtxtM :: (TidyEnv -> TcM (TidyEnv, MsgDoc)) -> TcM a -> TcM a +addLandmarkErrCtxtM ctxt = updCtxt (\ctxts -> (True, ctxt) : ctxts) -- Helper function for the above updCtxt :: ([ErrCtxt] -> [ErrCtxt]) -> TcM a -> TcM a diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs index 5275f904a3..d0cf737058 100644 --- a/compiler/typecheck/TcRnTypes.hs +++ b/compiler/typecheck/TcRnTypes.hs @@ -91,7 +91,8 @@ module TcRnTypes( ctLocTypeOrKind_maybe, ctLocDepth, bumpCtLocDepth, setCtLocOrigin, setCtLocEnv, setCtLocSpan, - CtOrigin(..), ErrorThing(..), mkErrorThing, errorThingNumArgs_maybe, + CtOrigin(..), exprCtOrigin, matchesCtOrigin, grhssCtOrigin, + ErrorThing(..), mkErrorThing, errorThingNumArgs_maybe, TypeOrKind(..), isTypeLevel, isKindLevel, pprCtOrigin, pprCtLoc, pushErrCtxt, pushErrCtxtSameOrigin, @@ -164,6 +165,7 @@ import Outputable import ListSetOps import FastString import GHC.Fingerprint +import qualified GHC.LanguageExtensions as LangExt import Control.Monad (ap, liftM, msum) #if __GLASGOW_HASKELL__ > 710 @@ -1211,7 +1213,7 @@ instance Outputable TcIdSigInfo where ppr (TISI { sig_bndr = bndr, sig_skols = tyvars , sig_theta = theta, sig_tau = tau }) = ppr (tcIdSigBndrName bndr) <+> dcolon <+> - vcat [ pprSigmaType (mkInvSigmaTy (map snd tyvars) theta tau) + vcat [ pprSigmaType (mkSpecSigmaTy (map snd tyvars) theta tau) , ppr (map fst tyvars) ] instance Outputable TcIdSigBndr where @@ -2648,12 +2650,16 @@ data CtOrigin -- is pinned on the entire error message | HoleOrigin - | UnboundOccurrenceOf RdrName + | UnboundOccurrenceOf OccName | ListOrigin -- An overloaded list | StaticOrigin -- A static form | FailablePattern (LPat TcId) -- A failable pattern in do-notation for the -- MonadFail Proposal (MFP). Obsolete when -- actual desugaring to MonadFail.fail is live. + | Shouldn'tHappenOrigin String + -- the user should never see this one, + -- unlesss ImpredicativeTypes is on, where all + -- bets are off -- | A thing that can be stored for error message generation only. -- It is stored with a function to zonk and tidy the thing. @@ -2695,6 +2701,78 @@ instance Outputable ErrorThing where ctoHerald :: SDoc ctoHerald = ptext (sLit "arising from") +-- | Extract a suitable CtOrigin from a HsExpr +exprCtOrigin :: HsExpr Name -> CtOrigin +exprCtOrigin (HsVar (L _ name)) = OccurrenceOf name +exprCtOrigin (HsUnboundVar occ) = UnboundOccurrenceOf occ +exprCtOrigin (HsRecFld f) = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f) +exprCtOrigin (HsOverLabel l) = OverLabelOrigin l +exprCtOrigin (HsIPVar ip) = IPOccOrigin ip +exprCtOrigin (HsOverLit lit) = LiteralOrigin lit +exprCtOrigin (HsLit {}) = Shouldn'tHappenOrigin "concrete literal" +exprCtOrigin (HsLam matches) = matchesCtOrigin matches +exprCtOrigin (HsLamCase _ ms) = matchesCtOrigin ms +exprCtOrigin (HsApp (L _ e1) _) = exprCtOrigin e1 +exprCtOrigin (OpApp _ (L _ op) _ _) = exprCtOrigin op +exprCtOrigin (NegApp (L _ e) _) = exprCtOrigin e +exprCtOrigin (HsPar (L _ e)) = exprCtOrigin e +exprCtOrigin (SectionL _ _) = SectionOrigin +exprCtOrigin (SectionR _ _) = SectionOrigin +exprCtOrigin (ExplicitTuple {}) = Shouldn'tHappenOrigin "explicit tuple" +exprCtOrigin (HsCase _ matches) = matchesCtOrigin matches +exprCtOrigin (HsIf (Just syn) _ _ _) = exprCtOrigin syn +exprCtOrigin (HsIf {}) = Shouldn'tHappenOrigin "if expression" +exprCtOrigin (HsMultiIf _ rhs) = lGRHSCtOrigin rhs +exprCtOrigin (HsLet _ (L _ e)) = exprCtOrigin e +exprCtOrigin (HsDo _ _ _) = DoOrigin +exprCtOrigin (ExplicitList {}) = Shouldn'tHappenOrigin "list" +exprCtOrigin (ExplicitPArr {}) = Shouldn'tHappenOrigin "parallel array" +exprCtOrigin (RecordCon {}) = Shouldn'tHappenOrigin "record construction" +exprCtOrigin (RecordUpd {}) = Shouldn'tHappenOrigin "record update" +exprCtOrigin (ExprWithTySig {}) = ExprSigOrigin +exprCtOrigin (ExprWithTySigOut {}) = panic "exprCtOrigin ExprWithTySigOut" +exprCtOrigin (ArithSeq {}) = Shouldn'tHappenOrigin "arithmetic sequence" +exprCtOrigin (PArrSeq {}) = Shouldn'tHappenOrigin "parallel array sequence" +exprCtOrigin (HsSCC _ _ (L _ e))= exprCtOrigin e +exprCtOrigin (HsCoreAnn _ _ (L _ e)) = exprCtOrigin e +exprCtOrigin (HsBracket {}) = Shouldn'tHappenOrigin "TH bracket" +exprCtOrigin (HsRnBracketOut {})= Shouldn'tHappenOrigin "HsRnBracketOut" +exprCtOrigin (HsTcBracketOut {})= panic "exprCtOrigin HsTcBracketOut" +exprCtOrigin (HsSpliceE {}) = Shouldn'tHappenOrigin "TH splice" +exprCtOrigin (HsProc {}) = Shouldn'tHappenOrigin "proc" +exprCtOrigin (HsStatic {}) = Shouldn'tHappenOrigin "static expression" +exprCtOrigin (HsArrApp {}) = panic "exprCtOrigin HsArrApp" +exprCtOrigin (HsArrForm {}) = panic "exprCtOrigin HsArrForm" +exprCtOrigin (HsTick _ (L _ e)) = exprCtOrigin e +exprCtOrigin (HsBinTick _ _ (L _ e)) = exprCtOrigin e +exprCtOrigin (HsTickPragma _ _ (L _ e)) = exprCtOrigin e +exprCtOrigin EWildPat = panic "exprCtOrigin EWildPat" +exprCtOrigin (EAsPat {}) = panic "exprCtOrigin EAsPat" +exprCtOrigin (EViewPat {}) = panic "exprCtOrigin EViewPat" +exprCtOrigin (ELazyPat {}) = panic "exprCtOrigin ELazyPat" +exprCtOrigin (HsType {}) = Shouldn'tHappenOrigin "type application" +exprCtOrigin (HsTypeOut {}) = panic "exprCtOrigin HsTypeOut" +exprCtOrigin (HsWrap {}) = panic "exprCtOrigin HsWrap" + +-- | Extract a suitable CtOrigin from a MatchGroup +matchesCtOrigin :: MatchGroup Name (LHsExpr Name) -> CtOrigin +matchesCtOrigin (MG { mg_alts = alts }) + | L _ [L _ match] <- alts + , Match { m_grhss = grhss } <- match + = grhssCtOrigin grhss + + | otherwise + = Shouldn'tHappenOrigin "multi-way match" + +-- | Extract a suitable CtOrigin from guarded RHSs +grhssCtOrigin :: GRHSs Name (LHsExpr Name) -> CtOrigin +grhssCtOrigin (GRHSs { grhssGRHSs = lgrhss }) = lGRHSCtOrigin lgrhss + +-- | Extract a suitable CtOrigin from a list of guarded RHSs +lGRHSCtOrigin :: [LGRHS Name (LHsExpr Name)] -> CtOrigin +lGRHSCtOrigin [L _ (GRHS _ (L _ e))] = exprCtOrigin e +lGRHSCtOrigin _ = Shouldn'tHappenOrigin "multi-way GRHS" + pprCtLoc :: CtLoc -> SDoc -- "arising from ... at ..." -- Not an instance of Outputable because of the "arising from" prefix @@ -2758,6 +2836,15 @@ pprCtOrigin (FailablePattern pat) $$ text "(this will become an error a future GHC release)" +pprCtOrigin (Shouldn'tHappenOrigin note) + = sdocWithDynFlags $ \dflags -> + if xopt LangExt.ImpredicativeTypes dflags + then text "a situation created by impredicative types" + else + vcat [ text "<< This should not appear in error messages. If you see this" + , text "in an error message, please report a bug mentioning" <+> quotes (text note) <+> text "at" + , text "https://ghc.haskell.org/trac/ghc/wiki/ReportABug >>" ] + pprCtOrigin simple_origin = ctoHerald <+> pprCtO simple_origin @@ -2774,7 +2861,7 @@ pprCtO ExprSigOrigin = ptext (sLit "an expression type signature") pprCtO PatSigOrigin = ptext (sLit "a pattern type signature") pprCtO PatOrigin = ptext (sLit "a pattern") pprCtO ViewPatOrigin = ptext (sLit "a view pattern") -pprCtO IfOrigin = ptext (sLit "an if statement") +pprCtO IfOrigin = ptext (sLit "an if expression") pprCtO (LiteralOrigin lit) = hsep [ptext (sLit "the literal"), quotes (ppr lit)] pprCtO (ArithSeqOrigin seq) = hsep [ptext (sLit "the arithmetic sequence"), quotes (ppr seq)] pprCtO (PArrSeqOrigin seq) = hsep [ptext (sLit "the parallel array sequence"), quotes (ppr seq)] diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs index e3b4fa8c7e..bf967aeb2f 100644 --- a/compiler/typecheck/TcSplice.hs +++ b/compiler/typecheck/TcSplice.hs @@ -75,6 +75,7 @@ import TyCoRep import FamInst import FamInstEnv import InstEnv +import Inst import NameEnv import PrelNames import TysWiredIn @@ -84,7 +85,6 @@ import Var import Module import LoadIface import Class -import Inst import TyCon import CoAxiom import PatSyn ( patSynName ) @@ -174,11 +174,12 @@ tcTypedBracket brack@(TExpBr expr) res_ty -- NC for no context; tcBracket does that ; meta_ty <- tcTExpTy expr_ty - ; co <- unifyType (Just expr) meta_ty res_ty ; ps' <- readMutVar ps_ref ; texpco <- tcLookupId unsafeTExpCoerceName - ; return (mkHsWrapCo co (unLoc (mkHsApp (nlHsTyApp texpco [expr_ty]) - (noLoc (HsTcBracketOut brack ps'))))) } + ; tcWrapResultO (Shouldn'tHappenOrigin "TExpBr") + (unLoc (mkHsApp (nlHsTyApp texpco [expr_ty]) + (noLoc (HsTcBracketOut brack ps')))) + meta_ty res_ty } tcTypedBracket other_brack _ = pprPanic "tcTypedBracket" (ppr other_brack) @@ -187,9 +188,9 @@ tcUntypedBracket brack ps res_ty = do { traceTc "tc_bracket untyped" (ppr brack $$ ppr ps) ; ps' <- mapM tcPendingSplice ps ; meta_ty <- tcBrackTy brack - ; co <- unifyType (Just brack) meta_ty res_ty ; traceTc "tc_bracket done untyped" (ppr meta_ty) - ; return (mkHsWrapCo co (HsTcBracketOut brack ps')) } + ; tcWrapResultO (Shouldn'tHappenOrigin "untyped bracket") + (HsTcBracketOut brack ps') meta_ty res_ty } --------------- tcBrackTy :: HsBracket Name -> TcM TcType @@ -512,7 +513,7 @@ tcTopSpliceExpr :: SpliceType -> TcM (LHsExpr Id) -> TcM (LHsExpr Id) -- 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 tcMonoExpr will simply expand the +-- The recursive call to tcPolyExpr will simply expand the -- inner escape before dealing with the outer one tcTopSpliceExpr isTypedSplice tc_action diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs index 51d6fc78f4..c17d78b9cc 100644 --- a/compiler/typecheck/TcTyDecls.hs +++ b/compiler/typecheck/TcTyDecls.hs @@ -626,10 +626,10 @@ initialRoleEnv1 is_boot annots_env tc _ -> replicate num_exps Nothing default_roles = build_default_roles visflags role_annots - build_default_roles (Invisible : viss) ras - = Nominal : build_default_roles viss ras build_default_roles (Visible : viss) (m_annot : ras) = (m_annot `orElse` default_role) : build_default_roles viss ras + build_default_roles (_inv : viss) ras + = Nominal : build_default_roles viss ras build_default_roles [] [] = [] build_default_roles _ _ = pprPanic "initialRoleEnv1 (2)" (vcat [ppr tc, ppr role_annots]) @@ -885,7 +885,7 @@ mkDefaultMethodIds tycons where mk_dm_ty :: Class -> Id -> DefMethSpec Type -> Type mk_dm_ty _ sel_id VanillaDM = idType sel_id - mk_dm_ty cls _ (GenericDM dm_ty) = mkInvSigmaTy cls_tvs [pred] dm_ty + mk_dm_ty cls _ (GenericDM dm_ty) = mkSpecSigmaTy cls_tvs [pred] dm_ty where cls_tvs = classTyVars cls pred = mkClassPred cls (mkTyVarTys cls_tvs) @@ -960,18 +960,19 @@ mkOneRecordSelector all_cons idDetails fl -- Selector type; Note [Polymorphic selectors] field_ty = conLikeFieldType con1 lbl - data_tvs = tyCoVarsOfType data_ty - is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tvs) + data_tvs = tyCoVarsOfTypeWellScoped data_ty + data_tv_set= mkVarSet data_tvs + is_naughty = not (tyCoVarsOfType field_ty `subVarSet` data_tv_set) (field_tvs, field_theta, field_tau) = tcSplitSigmaTy field_ty - all_tvs = varSetElemsWellScoped $ data_tvs `extendVarSetList` field_tvs sel_ty | is_naughty = unitTy -- See Note [Naughty record selectors] - | otherwise = ASSERT( all isTyVar all_tvs ) - mkInvForAllTys all_tvs $ + | otherwise = mkSpecForAllTys data_tvs $ mkPhiTy (conLikeStupidTheta con1) $ -- Urgh! - mkPhiTy field_theta $ -- Urgh! + mkFunTy data_ty $ + mkSpecForAllTys field_tvs $ + mkPhiTy field_theta $ -- req_theta is empty for normal DataCon mkPhiTy req_theta $ - mkFunTy data_ty field_tau + field_tau -- Make the binding: sel (C2 { fld = x }) = x -- sel (C7 { fld = x }) = x @@ -1017,7 +1018,8 @@ mkOneRecordSelector all_cons idDetails fl (univ_tvs, _, eq_spec, _, req_theta, _, data_ty) = conLikeFullSig con1 - inst_tys = substTyVars (mkTopTCvSubst (map eqSpecPair eq_spec)) univ_tvs + eq_subst = mkTopTCvSubst (map eqSpecPair eq_spec) + inst_tys = substTyVars eq_subst univ_tvs unit_rhs = mkLHsTupleExpr [] msg_lit = HsStringPrim "" (fastStringToByteString lbl) @@ -1025,14 +1027,14 @@ mkOneRecordSelector all_cons idDetails fl {- Note [Polymorphic selectors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When a record has a polymorphic field, we pull the foralls out to the front. - data T = MkT { f :: forall a. [a] -> a } -Then f :: forall a. T -> [a] -> a -NOT f :: T -> forall a. [a] -> a - -This is horrid. It's only needed in deeply obscure cases, which I hate. -The only case I know is test tc163, which is worth looking at. It's far -from clear that this test should succeed at all! +We take care to build the type of a polymorphic selector in the right +order, so that visible type application works. + + data Ord a => T a = MkT { field :: forall b. (Num a, Show b) => (a, b) } + +We want + + field :: forall a. Ord a => T a -> forall b. (Num a, Show b) => (a, b) Note [Naughty record selectors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs index 879f977045..97865f44a7 100644 --- a/compiler/typecheck/TcType.hs +++ b/compiler/typecheck/TcType.hs @@ -32,9 +32,8 @@ module TcType ( -- MetaDetails UserTypeCtxt(..), pprUserTypeCtxt, pprSigCtxt, isSigMaybe, TcTyVarDetails(..), pprTcTyVarDetails, vanillaSkolemTv, superSkolemTv, - MetaDetails(Flexi, Indirect), MetaInfo(..), - isImmutableTyVar, isSkolemTyVar, - isMetaTyVar, isMetaTyVarTy, isTyVarTy, + MetaDetails(Flexi, Indirect), MetaInfo(..), TauTvFlavour(..), + isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy, isSigTyVar, isOverlappableTyVar, isTyConableTyVar, isFskTyVar, isFmvTyVar, isFlattenTyVar, isReturnTyVar, isAmbiguousTyVar, metaTvRef, metaTyVarInfo, @@ -46,14 +45,15 @@ module TcType ( -------------------------------- -- Builders - mkPhiTy, mkInvSigmaTy, mkSigmaTy, + mkPhiTy, mkInvSigmaTy, mkSpecSigmaTy, mkSigmaTy, mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy, mkNakedFunTy, - mkNakedInvSigmaTy, mkNakedCastTy, mkNakedPhiTy, + mkNakedSpecSigmaTy, mkNakedCastTy, mkNakedPhiTy, -------------------------------- -- Splitters -- These are important because they do not look through newtypes getTyVar, + tcSplitForAllTy_maybe, tcSplitForAllTys, tcSplitPiTys, tcSplitNamedPiTys, tcSplitPhiTy, tcSplitPredFunTy_maybe, tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN, @@ -126,11 +126,12 @@ module TcType ( -- Rexported from Type Type, PredType, ThetaType, TyBinder, VisibilityFlag(..), - mkForAllTy, mkForAllTys, mkInvForAllTys, mkNamedForAllTy, + mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, mkNamedForAllTy, mkFunTy, mkFunTys, mkTyConApp, mkAppTy, mkAppTys, applyTys, mkTyConTy, mkTyVarTy, mkTyVarTys, + mkNamedBinder, isClassPred, isEqPred, isNomEqPred, isIPPred, mkClassPred, @@ -389,6 +390,10 @@ instance Outputable MetaDetails where ppr Flexi = ptext (sLit "Flexi") ppr (Indirect ty) = ptext (sLit "Indirect") <+> ppr ty +data TauTvFlavour + = VanillaTau + | WildcardTau -- ^ A tyvar that originates from a type wildcard. + data MetaInfo = TauTv -- This MetaTv is an ordinary unification variable -- A TauTv is always filled in with a tau-type, which @@ -428,7 +433,7 @@ data UserTypeCtxt | InfSigCtxt Name -- Inferred type for function | ExprSigCtxt -- Expression type signature - + | TypeAppCtxt -- Visible type application | ConArgCtxt Name -- Data constructor argument | TySynCtxt Name -- RHS of a type synonym decl | PatSynCtxt Name -- Type sig for a pattern synonym @@ -615,6 +620,7 @@ pprUserTypeCtxt (FunSigCtxt n _) = ptext (sLit "the type signature for") <+> qu pprUserTypeCtxt (InfSigCtxt n) = ptext (sLit "the inferred type for") <+> quotes (ppr n) pprUserTypeCtxt (RuleSigCtxt n) = ptext (sLit "a RULE for") <+> quotes (ppr n) pprUserTypeCtxt ExprSigCtxt = ptext (sLit "an expression type signature") +pprUserTypeCtxt TypeAppCtxt = ptext (sLit "a type argument") pprUserTypeCtxt (ConArgCtxt c) = ptext (sLit "the type of the constructor") <+> quotes (ppr c) pprUserTypeCtxt (TySynCtxt c) = ptext (sLit "the RHS of the type synonym") <+> quotes (ppr c) pprUserTypeCtxt (PatSynCtxt c) = ptext (sLit "the type signature for pattern synonym") <+> quotes (ppr c) @@ -967,6 +973,12 @@ mkInvSigmaTy :: [TyVar] -> [PredType] -> Type -> Type mkInvSigmaTy tyvars = mkSigmaTy (zipWith mkNamedBinder tyvars (repeat Invisible)) +-- | Make a sigma ty where all type variables are "specified". That is, +-- they can be used with visible type application +mkSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type +mkSpecSigmaTy tyvars + = mkSigmaTy (zipWith mkNamedBinder tyvars (repeat Specified)) + mkPhiTy :: [PredType] -> Type -> Type mkPhiTy = mkFunTys @@ -974,10 +986,10 @@ mkNakedSigmaTy :: [TyBinder] -> [PredType] -> Type -> Type -- See Note [Type-checking inside the knot] in TcHsType mkNakedSigmaTy bndrs theta tau = mkForAllTys bndrs (mkNakedPhiTy theta tau) -mkNakedInvSigmaTy :: [TyVar] -> [PredType] -> Type -> Type +mkNakedSpecSigmaTy :: [TyVar] -> [PredType] -> Type -> Type -- See Note [Type-checking inside the knot] in TcHsType -mkNakedInvSigmaTy tyvars - = mkNakedSigmaTy (zipWith mkNamedBinder tyvars (repeat Invisible)) +mkNakedSpecSigmaTy tyvars + = mkNakedSigmaTy (zipWith mkNamedBinder tyvars (repeat Specified)) mkNakedPhiTy :: [PredType] -> Type -> Type -- See Note [Type-checking inside the knot] in TcHsType @@ -1063,6 +1075,11 @@ variables. It's up to you to make sure this doesn't matter. tcSplitPiTys :: Type -> ([TyBinder], Type) tcSplitPiTys = splitPiTys +tcSplitForAllTy_maybe :: Type -> Maybe (TyBinder, Type) +tcSplitForAllTy_maybe ty | Just ty' <- coreView ty = tcSplitForAllTy_maybe ty' +tcSplitForAllTy_maybe (ForAllTy tv ty) = Just (tv, ty) +tcSplitForAllTy_maybe _ = Nothing + -- | Like 'tcSplitPiTys', but splits off only named binders, returning -- just the tycovars. tcSplitForAllTys :: Type -> ([TyVar], Type) @@ -1310,8 +1327,8 @@ tcEqTypeVis ty1 ty2 (<!>) :: Maybe VisibilityFlag -> Maybe VisibilityFlag -> Maybe VisibilityFlag Nothing <!> x = x Just Visible <!> _ = Just Visible -Just Invisible <!> Just Visible = Just Visible -Just Invisible <!> _ = Just Invisible +Just _inv <!> Just Visible = Just Visible +Just inv <!> _ = Just inv infixr 3 <!> -- | Real worker for 'tcEqType'. No kind check! @@ -1578,7 +1595,7 @@ occurCheckExpand dflags tv ty canUnifyWithPolyType :: DynFlags -> TcTyVarDetails -> Bool canUnifyWithPolyType dflags details = case details of - MetaTv { mtv_info = ReturnTv } -> True -- See Note [ReturnTv] + MetaTv { mtv_info = ReturnTv } -> True -- See Note [ReturnTv] MetaTv { mtv_info = SigTv } -> False MetaTv { mtv_info = TauTv } -> xopt LangExt.ImpredicativeTypes dflags _other -> True @@ -1992,6 +2009,40 @@ to_tc_type = mapType to_tc_mapper \subsection{Misc} * * ************************************************************************ + +Note [Visible type application] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +GHC implements a generalisation of the algorithm described in the +"Visible Type Application" paper (available from +http://www.cis.upenn.edu/~sweirich/publications.html). A key part +of that algorithm is to distinguish user-specified variables from inferred +variables. For example, the following should typecheck: + + f :: forall a b. a -> b -> b + f = const id + + g = const id + + x = f @Int @Bool 5 False + y = g 5 @Bool False + +The idea is that we wish to allow visible type application when we are +instantiating a specified, fixed variable. In practice, specified, fixed +variables are either written in a type signature (or +annotation), OR are imported from another module. (We could do better here, +for example by doing SCC analysis on parts of a module and considering any +type from outside one's SCC to be fully specified, but this is very confusing to +users. The simple rule above is much more straightforward and predictable.) + +So, both of f's quantified variables are specified and may be instantiated. +But g has no type signature, so only id's variable is specified (because id +is imported). We write the type of g as forall {a}. a -> forall b. b -> b. +Note that the a is in braces, meaning it cannot be instantiated with +visible type application. + +Tracking specified vs. inferred variables is done conveniently by a field +in TyBinder. + -} deNoteType :: Type -> Type diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs index 51a1eee695..b7bc77db73 100644 --- a/compiler/typecheck/TcUnify.hs +++ b/compiler/typecheck/TcUnify.hs @@ -6,12 +6,13 @@ Type subsumption and unification -} -{-# LANGUAGE CPP, MultiWayIf #-} +{-# LANGUAGE CPP, MultiWayIf, TupleSections #-} module TcUnify ( -- Full-blown subsumption - tcWrapResult, tcGen, - tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_NC, + tcWrapResult, tcWrapResultO, tcSkolemise, + tcSubTypeHR, tcSubType, tcSubType_NC, tcSubTypeDS, tcSubTypeDS_O, + tcSubTypeDS_NC, tcSubTypeDS_NC_O, checkConstraints, buildImplication, buildImplicationFor, -- Various unifications @@ -26,7 +27,7 @@ module TcUnify ( matchExpectedTyConApp, matchExpectedAppTy, matchExpectedFunTys, - + matchActualFunTys, matchActualFunTysPart, matchExpectedFunKind, wrapFunResCoercion @@ -92,7 +93,7 @@ This is used to construct a message of form Note [matchExpectedFunTys] ~~~~~~~~~~~~~~~~~~~~~~~~~~ -matchExpectedFunTys checks that an (Expected rho) has the form +matchExpectedFunTys checks that a sigma has the form of an n-ary function. It passes the decomposed type to the thing_inside, and returns a wrapper to coerce between the two types @@ -102,18 +103,77 @@ namely: A function definition An operator section -This is not (currently) where deep skolemisation occurs; -matchExpectedFunTys does not skolmise nested foralls in the -expected type, because it expects that to have been done already -} -matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] +-- Use this one when you have an "expected" type. +matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] -> Arity - -> TcRhoType - -> TcM (TcCoercionN, [TcSigmaType], TcRhoType) - --- If matchExpectFunTys n ty = (co, [t1,..,tn], ty_r) --- then co : ty ~N (t1 -> ... -> tn -> ty_r) + -> TcSigmaType -- deeply skolemised + -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) +-- If matchExpectedFunTys n ty = (wrap, [t1,..,tn], ty_r) +-- then wrap : (t1 -> ... -> tn -> ty_r) "->" ty + +-- This function is always called with a deeply skolemised expected result +-- type. This means that matchActualFunTys will never actually instantiate, +-- and the returned HsWrapper will be reversible (that is, just a coercion). +-- So we just piggyback on matchActualFunTys. This is just a bit dodgy, but +-- it's much better than duplicating all the logic in matchActualFunTys. +-- To keep expected/actual working out properly, we tell matchActualFunTys +-- to swap the arguments to unifyType. +matchExpectedFunTys herald arity ty + = ASSERT( is_deeply_skolemised ty ) + do { (wrap, arg_tys, res_ty) + <- match_fun_tys True herald + (Shouldn'tHappenOrigin "matchExpectedFunTys") + arity ty [] arity + ; return $ + case symWrapper_maybe wrap of + Just wrap' -> (wrap', arg_tys, res_ty) + Nothing -> pprPanic "matchExpectedFunTys" (ppr wrap $$ ppr ty) } + where + is_deeply_skolemised (TyVarTy {}) = True + is_deeply_skolemised (AppTy {}) = True + is_deeply_skolemised (TyConApp {}) = True + is_deeply_skolemised (LitTy {}) = True + is_deeply_skolemised (CastTy ty _) = is_deeply_skolemised ty + is_deeply_skolemised (CoercionTy {}) = True + + is_deeply_skolemised (ForAllTy (Anon _) res) = is_deeply_skolemised res + is_deeply_skolemised (ForAllTy (Named {}) _) = False + +matchActualFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> CtOrigin + -> Arity + -> TcSigmaType + -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) +matchActualFunTys herald ct_orig arity ty + = matchActualFunTysPart herald ct_orig arity ty [] arity + +-- | Variant of 'matchActualFunTys' that works when supplied only part +-- (that is, to the right of some arrows) of the full function type +matchActualFunTysPart :: SDoc -- See Note [Herald for matchExpectedFunTys] + -> CtOrigin + -> Arity + -> TcSigmaType + -> [TcSigmaType] -- reversed args. See (*) below. + -> Arity -- overall arity of the function, for errs + -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) +matchActualFunTysPart = match_fun_tys False + +match_fun_tys :: Bool -- True <=> swap the args when unifying, + -- for better expected/actual in error messages; + -- see comments with matchExpectedFunTys + -> SDoc + -> CtOrigin + -> Arity + -> TcSigmaType + -> [TcSigmaType] + -> Arity + -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) +match_fun_tys swap_tys herald ct_orig arity orig_ty orig_old_args full_arity + = go arity orig_old_args orig_ty +-- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r) +-- then wrap : ty "->" (t1 -> ... -> tn -> ty_r) -- -- Does not allocate unnecessary meta variables: if the input already is -- a function, we just take it apart. Not only is this efficient, @@ -122,29 +182,54 @@ matchExpectedFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys] -- If allocated (fresh-meta-var1 -> fresh-meta-var2) and unified, we'd -- hide the forall inside a meta-variable -matchExpectedFunTys herald arity orig_ty - = go arity orig_ty - where - -- If go n ty = (co, [t1,..,tn], ty_r) - -- then co : ty ~ t1 -> .. -> tn -> ty_r +-- (*) Sometimes it's necessary to call matchActualFunTys with only part +-- (that is, to the right of some arrows) of the type of the function in +-- question. (See TcExpr.tcArgs.) This argument is the reversed list of +-- arguments already seen (that is, not part of the TcSigmaType passed +-- in elsewhere). - go n_req ty - | n_req == 0 = return (mkTcNomReflCo ty, [], ty) + 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] -- accumulator of arguments (reversed) + -> TcSigmaType -- the remainder of the type as we're processing + -> TcM (HsWrapper, [TcSigmaType], TcSigmaType) + go 0 _ ty = return (idHsWrapper, [], ty) + + go n acc_args ty + | not (null tvs && null theta) + = do { (wrap1, rho) <- topInstantiate ct_orig ty + ; (wrap2, arg_tys, res_ty) <- go n acc_args rho + ; return (wrap2 <.> wrap1, arg_tys, res_ty) } + where + (tvs, theta, _) = tcSplitSigmaTy ty - go n_req ty - | Just ty' <- coreView ty = go n_req ty' + go n acc_args ty + | Just ty' <- coreView ty = go n acc_args ty' - go n_req (ForAllTy (Anon arg_ty) res_ty) - | not (isPredTy arg_ty) - = do { (co, tys, ty_r) <- go (n_req-1) res_ty - ; return (mkTcFunCo Nominal (mkTcNomReflCo arg_ty) co, arg_ty:tys, ty_r) } + go n acc_args (ForAllTy (Anon arg_ty) res_ty) + = ASSERT( not (isPredTy arg_ty) ) + do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty : acc_args) res_ty + ; return ( mkWpFun idHsWrapper wrap_res arg_ty (mkFunTys tys ty_r) + , arg_ty:tys, ty_r ) } - go n_req ty@(TyVarTy tv) + go n acc_args ty@(TyVarTy tv) | ASSERT( isTcTyVar tv) isMetaTyVar tv = do { cts <- readMetaTyVar tv ; case cts of - Indirect ty' -> go n_req ty' - Flexi -> defer n_req ty (isReturnTyVar tv) } + Indirect ty' -> go n acc_args ty' + Flexi -> defer n ty (isReturnTyVar tv) } -- In all other cases we bale out into ordinary unification -- However unlike the meta-tyvar case, we are sure that the @@ -161,19 +246,21 @@ matchExpectedFunTys herald arity orig_ty -- -- But in that case we add specialized type into error context -- anyway, because it may be useful. See also Trac #9605. - go n_req ty = addErrCtxtM mk_ctxt $ - defer n_req ty False + go n acc_args ty = addErrCtxtM (mk_ctxt (reverse acc_args) ty) $ + defer n ty False ------------ -- If we decide that a ReturnTv (see Note [ReturnTv] in TcType) should - -- really be a function type, then we need to allow the argument and - -- result types also to be ReturnTvs. - defer n_req fun_ty is_return - = do { arg_tys <- replicateM n_req new_flexi - -- See Note [Foralls to left of arrow] + -- really be a function type, then we need to allow the + -- result types also to be a ReturnTv. + defer n fun_ty is_return + = do { arg_tys <- replicateM n new_flexi ; res_ty <- new_flexi - ; co <- unifyType noThing fun_ty (mkFunTys arg_tys res_ty) - ; return (co, arg_tys, res_ty) } + ; let unif_fun_ty = mkFunTys arg_tys res_ty + ; co <- if swap_tys + then mkTcSymCo <$> unifyType noThing unif_fun_ty fun_ty + else unifyType noThing fun_ty unif_fun_ty + ; return (mkWpCastN co, arg_tys, res_ty) } where -- preserve ReturnTv-ness new_flexi :: TcM TcType @@ -181,35 +268,26 @@ matchExpectedFunTys herald arity orig_ty | otherwise = newOpenFlexiTyVarTy ------------ - mk_ctxt :: TidyEnv -> TcM (TidyEnv, MsgDoc) - mk_ctxt env = do { (env', ty) <- zonkTidyTcType env orig_ty - ; let (args, _) = tcSplitFunTys ty - n_actual = length args - (env'', orig_ty') = tidyOpenType env' orig_ty - ; return (env'', mk_msg orig_ty' ty n_actual) } - - mk_msg orig_ty ty n_args - = herald <+> speakNOf arity (ptext (sLit "argument")) <> comma $$ - if n_args == arity - then ptext (sLit "its type is") <+> quotes (pprType orig_ty) <> + mk_ctxt :: [TcSigmaType] -> TcSigmaType -> TidyEnv -> TcM (TidyEnv, MsgDoc) + mk_ctxt arg_tys res_ty env + = do { let ty = mkFunTys arg_tys res_ty + ; (env1, zonked) <- zonkTidyTcType env ty + -- zonking might change # of args + ; let (zonked_args, _) = tcSplitFunTys zonked + n_actual = length zonked_args + (env2, unzonked) = tidyOpenType env1 ty + ; return (env2, mk_msg unzonked zonked n_actual) } + + mk_msg full_ty ty n_args + = herald <+> speakNOf full_arity (text "argument") <> comma $$ + if n_args == full_arity + then ptext (sLit "its type is") <+> quotes (pprType full_ty) <> comma $$ ptext (sLit "it is specialized to") <+> quotes (pprType ty) else sep [ptext (sLit "but its type") <+> quotes (pprType ty), if n_args == 0 then ptext (sLit "has none") else ptext (sLit "has only") <+> speakN n_args] -{- -Note [Foralls to left of arrow] -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Consider - f (x :: forall a. a -> a) = x -We give 'f' the type (alpha -> beta), and then want to unify -the alpha with (forall a. a->a). We want to the arg and result -of (->) to be sort-polymorphic, and this also permits foralls, so -we are ok. See Note [Sort-polymorphic tyvars accept foralls] in TcUnify -and Note [TYPE] in TysPrim. --} - ---------------------- matchExpectedListTy :: TcRhoType -> TcM (TcCoercionN, TcRhoType) -- Special case for lists @@ -251,9 +329,9 @@ matchExpectedTyConApp tc orig_ty = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> go ty - Flexi -> defer (isReturnTyVar tv) } + Flexi -> defer } - go _ = defer False + go _ = defer -- If the common case does not occur, instantiate a template -- T k1 .. kn t1 .. tm, and unify with the original type @@ -265,12 +343,12 @@ matchExpectedTyConApp tc orig_ty -- (a::*) ~ Maybe -- because that'll make types that are utterly ill-kinded. -- This happened in Trac #7368 - defer is_return + defer = ASSERT2( classifiesTypeWithValues res_kind, ppr tc ) do { (k_subst, kvs') <- newMetaTyVars kvs ; let arg_kinds' = substTys k_subst arg_kinds kappa_tys = mkTyVarTys kvs' - ; tau_tys <- mapM (newMaybeReturnTyVarTy is_return) arg_kinds' + ; tau_tys <- mapM newFlexiTyVarTy arg_kinds' ; co <- unifyType noThing (mkTyConApp tc (kappa_tys ++ tau_tys)) orig_ty ; return (co, kappa_tys ++ tau_tys) } @@ -298,14 +376,14 @@ matchExpectedAppTy orig_ty = do { cts <- readMetaTyVar tv ; case cts of Indirect ty -> go ty - Flexi -> defer (isReturnTyVar tv) } + Flexi -> defer } - go _ = defer False + go _ = defer -- Defer splitting by generating an equality constraint - defer is_return - = do { ty1 <- newMaybeReturnTyVarTy is_return kind1 - ; ty2 <- newMaybeReturnTyVarTy is_return kind2 + defer + = do { ty1 <- newFlexiTyVarTy kind1 + ; ty2 <- newFlexiTyVarTy kind2 ; co <- unifyType noThing (mkAppTy ty1 ty2) orig_ty ; return (co, (ty1, ty2)) } @@ -338,11 +416,26 @@ It returns a coercion function 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 predicatble type inference. +more predictable type inference. Wrinkle 1: Note [Deep skolemisation] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -350,7 +443,7 @@ 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 tcGen (which does the +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) @@ -367,7 +460,7 @@ 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 -tc_sub_type_ds, and is the sole reason for the WpFun form 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 @@ -387,30 +480,53 @@ So it's important that we unify beta := forall a. a->a, rather than skolemising the type. -} -tcSubType :: UserTypeCtxt -> Maybe Id -- ^ If present, it has type ty_actual + +-- | Call this variant when you are in a higher-rank situation and +-- you know the right-hand type is deeply skolemised. +tcSubTypeHR :: Outputable a + => CtOrigin -- ^ of the actual type + -> Maybe a -- ^ If present, it has type ty_actual + -> TcSigmaType -> TcRhoType -> TcM HsWrapper +tcSubTypeHR orig = tcSubTypeDS_NC_O orig GenSigCtxt + +tcSubType :: Outputable a + => UserTypeCtxt -> Maybe a -- ^ If present, it has type ty_actual -> TcSigmaType -> TcSigmaType -> TcM HsWrapper -- Checks that actual <= expected -- Returns HsWrapper :: actual ~ expected -tcSubType ctxt maybe_id ty_actual ty_expected +tcSubType ctxt maybe_thing ty_actual ty_expected = addSubTypeCtxt ty_actual ty_expected $ do { traceTc "tcSubType" (vcat [ pprUserTypeCtxt ctxt - , ppr maybe_id + , ppr maybe_thing , ppr ty_actual , ppr ty_expected ]) - ; tc_sub_type origin ctxt ty_actual ty_expected } + ; tc_sub_type origin origin ctxt ty_actual ty_expected } where origin = TypeEqOrigin { uo_actual = ty_actual , uo_expected = ty_expected - , uo_thing = mkErrorThing <$> maybe_id } + , uo_thing = mkErrorThing <$> maybe_thing } -tcSubTypeDS :: Outputable a => UserTypeCtxt -> a -- ^ has type ty_actual +tcSubTypeDS :: Outputable a => UserTypeCtxt -> Maybe a -- ^ has type ty_actual -> TcSigmaType -> TcRhoType -> TcM HsWrapper -- Just like tcSubType, but with the additional precondition that -- ty_expected is deeply skolemised (hence "DS") -tcSubTypeDS ctxt expr ty_actual ty_expected +tcSubTypeDS ctxt m_expr ty_actual ty_expected = addSubTypeCtxt ty_actual ty_expected $ - tcSubTypeDS_NC ctxt (Just expr) ty_actual ty_expected - + tcSubTypeDS_NC ctxt m_expr ty_actual ty_expected + +-- | Like 'tcSubTypeDS', but takes a 'CtOrigin' to use when instantiating +-- the "actual" type +tcSubTypeDS_O :: Outputable a + => CtOrigin -> UserTypeCtxt + -> Maybe a -> TcSigmaType -> TcRhoType + -> TcM HsWrapper +tcSubTypeDS_O orig ctxt maybe_thing 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 maybe_thing ty_actual ty_expected } addSubTypeCtxt :: TcType -> TcType -> TcM a -> TcM a addSubTypeCtxt ty_actual ty_expected thing_inside @@ -436,7 +552,7 @@ addSubTypeCtxt ty_actual ty_expected thing_inside tcSubType_NC :: UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper tcSubType_NC ctxt ty_actual ty_expected = do { traceTc "tcSubType_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tc_sub_type origin ctxt ty_actual ty_expected } + ; tc_sub_type origin origin ctxt ty_actual ty_expected } where origin = TypeEqOrigin { uo_actual = ty_actual , uo_expected = ty_expected @@ -448,57 +564,157 @@ tcSubTypeDS_NC :: Outputable a -> TcSigmaType -> TcRhoType -> TcM HsWrapper tcSubTypeDS_NC ctxt maybe_thing ty_actual ty_expected = do { traceTc "tcSubTypeDS_NC" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected]) - ; tc_sub_type_ds origin ctxt ty_actual ty_expected } + ; tcSubTypeDS_NC_O origin ctxt maybe_thing ty_actual ty_expected } where origin = TypeEqOrigin { uo_actual = ty_actual , uo_expected = ty_expected , uo_thing = mkErrorThing <$> maybe_thing } +tcSubTypeDS_NC_O :: Outputable a + => CtOrigin -- origin used for instantiation only + -> UserTypeCtxt + -> Maybe a + -> TcSigmaType -> TcRhoType -> 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 + = tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected + where + eq_orig = TypeEqOrigin { uo_actual = ty_actual, uo_expected = ty_expected + , uo_thing = mkErrorThing <$> m_thing} + --------------- -tc_sub_type :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper -tc_sub_type origin ctxt ty_actual ty_expected - | isTyVarTy ty_actual -- See Note [Higher rank types] - = do { cow <- uType origin TypeLevel ty_actual ty_expected - ; return (mkWpCastN cow) } +tc_sub_type :: CtOrigin -- origin used when calling uType + -> CtOrigin -- origin used when instantiating + -> UserTypeCtxt -> TcSigmaType -> TcSigmaType -> TcM HsWrapper +tc_sub_type eq_orig inst_orig ctxt ty_actual ty_expected + | Just tv_actual <- tcGetTyVar_maybe ty_actual -- See Note [Higher rank types] + = do { lookup_res <- lookupTcTyVar tv_actual + ; case lookup_res of + Filled ty_actual' -> tc_sub_type eq_orig inst_orig + ctxt ty_actual' ty_expected + + -- It's tempting to see if tv_actual can unify with a polytype + -- and, if so, call uType; otherwise, skolemise first. But this + -- is wrong, because skolemising will bump the TcLevel and the + -- unification will fail anyway. + -- It's also tempting to call uUnfilledVar directly, but calling + -- uType seems safer in the presence of possible refactoring + -- later. + Unfilled _ -> mkWpCastN <$> + uType eq_orig TypeLevel ty_actual ty_expected } | otherwise -- See Note [Deep skolemisation] - = do { (sk_wrap, inner_wrap) <- tcGen ctxt ty_expected $ \ _ sk_rho -> - tc_sub_type_ds origin ctxt ty_actual sk_rho + = do { (sk_wrap, inner_wrap) <- tcSkolemise ctxt ty_expected $ + \ _ sk_rho -> + tc_sub_type_ds eq_orig inst_orig ctxt + ty_actual sk_rho ; return (sk_wrap <.> inner_wrap) } --------------- -tc_sub_type_ds :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper +tc_sub_type_ds :: CtOrigin -- used when calling uType + -> CtOrigin -- used when instantiating + -> UserTypeCtxt -> TcSigmaType -> TcRhoType -> TcM HsWrapper -- Just like tcSubType, but with the additional precondition that -- ty_expected is deeply skolemised -tc_sub_type_ds origin ctxt ty_actual ty_expected - | Just (act_arg, act_res) <- tcSplitFunTy_maybe ty_actual - , Just (exp_arg, exp_res) <- tcSplitFunTy_maybe ty_expected - = -- See Note [Co/contra-variance of subsumption checking] - do { res_wrap <- tc_sub_type_ds origin ctxt act_res exp_res - ; arg_wrap <- tc_sub_type origin ctxt exp_arg act_arg - ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) } - -- arg_wrap :: exp_arg ~ act_arg - -- res_wrap :: act-res ~ exp_res - - | (tvs, theta, in_rho) <- tcSplitSigmaTy ty_actual - , not (null tvs && null theta) - = do { (subst, tvs') <- newMetaTyVars tvs - ; let tys' = mkTyVarTys tvs' - theta' = substTheta subst theta - in_rho' = substTy subst in_rho - ; in_wrap <- instCall origin tys' theta' - ; body_wrap <- tcSubTypeDS_NC ctxt noThing in_rho' ty_expected - ; return (body_wrap <.> in_wrap) } - - | otherwise -- Revert to unification - = do { cow <- uType origin TypeLevel ty_actual ty_expected - ; return (mkWpCastN cow) } +tc_sub_type_ds eq_orig inst_orig ctxt ty_actual ty_expected + = go ty_actual ty_expected + where + go ty_a ty_e | Just ty_a' <- coreView ty_a = go ty_a' ty_e + | Just ty_e' <- coreView 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 _ -> mkWpCastN <$> unify } + + + go ty_a (TyVarTy tv_e) + = do { dflags <- getDynFlags + ; tclvl <- getTcLevel + ; lookup_res <- lookupTcTyVar tv_e + ; case lookup_res of + Filled ty_e' -> + do { traceTc "tcSubTypeDS_NC_O following filled exp meta-tyvar:" + (ppr tv_e <+> text "-->" <+> ppr ty_e') + ; tc_sub_type eq_orig inst_orig ctxt ty_a ty_e' } + Unfilled details + | canUnifyWithPolyType dflags details + && isTouchableMetaTyVar tclvl tv_e -- don't want skolems here + -> mkWpCastN <$> unify + + -- We've avoided instantiating ty_actual just in case ty_expected is + -- polymorphic. But we've now assiduously determined that it is *not* + -- polymorphic. So instantiate away. This is needed for e.g. test + -- typecheck/should_compile/T4284. + | otherwise + -> 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 + , uo_expected = orig_ty_expected + , uo_thing = thing } + | orig_ty_actual `tcEqType` ty_actual + -> TypeEqOrigin + { uo_actual = rho_a + , uo_expected = orig_ty_expected + , uo_thing = thing } + _ -> eq_orig + + ; cow <- uType eq_orig' TypeLevel rho_a ty_expected + ; return (mkWpCastN cow <.> wrap) } } + + go (ForAllTy (Anon act_arg) act_res) (ForAllTy (Anon exp_arg) exp_res) + | not (isPredTy act_arg) + , not (isPredTy exp_arg) + = -- 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_type eq_orig (GivenOrigin (SigSkol GenSigCtxt exp_arg)) + ctxt exp_arg act_arg + ; return (mkWpFun arg_wrap res_wrap exp_arg exp_res) } + -- arg_wrap :: exp_arg ~ act_arg + -- res_wrap :: act-res ~ exp_res + + 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 <- tcSubTypeDS_NC_O inst_orig ctxt noThing in_rho ty_e + ; return (body_wrap <.> in_wrap) } + + | otherwise -- Revert to unification + = do { cow <- unify + ; return (mkWpCastN cow) } + + -- use versions without synonyms expanded + unify = uType eq_orig TypeLevel ty_actual ty_expected ----------------- -tcWrapResult :: HsExpr TcId -> TcRhoType -> TcRhoType -> TcM (HsExpr TcId) -tcWrapResult expr actual_ty res_ty - = do { cow <- tcSubTypeDS GenSigCtxt expr actual_ty res_ty - -- Both types are deeply skolemised +-- needs both un-type-checked (for origins) and type-checked (for wrapping) +-- expressions +tcWrapResult :: HsExpr Name -> HsExpr TcId -> TcSigmaType -> TcRhoType + -> TcM (HsExpr TcId) +tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) + +-- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more +-- convenient. +tcWrapResultO :: CtOrigin -> HsExpr TcId -> TcSigmaType -> TcRhoType + -> TcM (HsExpr TcId) +tcWrapResultO orig 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 expr) actual_ty res_ty ; return (mkHsWrap cow expr) } ----------------------------------- @@ -540,23 +756,26 @@ tcInfer tc_check ************************************************************************ -} -tcGen :: UserTypeCtxt -> TcType - -> ([TcTyVar] -> TcRhoType -> TcM result) +-- | 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) -- ^ thing_inside is passed only the *type* variables, not -- *coercion* variables. They are only ever used for scoped type -- variables. - -> TcM (HsWrapper, result) - -- ^ The expression has type: spec_ty -> expected_ty + -> TcM (HsWrapper, result) + -- ^ The expression has type: spec_ty -> expected_ty -tcGen ctxt expected_ty thing_inside +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 "tcGen" Outputable.empty + = do { traceTc "tcSkolemise" Outputable.empty ; (wrap, tvs', given, rho') <- deeplySkolemise expected_ty ; lvl <- getTcLevel ; when debugIsOn $ - traceTc "tcGen" $ vcat [ + traceTc "tcSkolemise" $ vcat [ ppr lvl, text "expected_ty" <+> ppr expected_ty, text "inst tyvars" <+> ppr tvs', @@ -613,7 +832,7 @@ buildImplication skol_info skol_tvs given thing_inside then do { res <- thing_inside ; return (emptyBag, emptyTcEvBinds, res) } -- Fast path. We check every function argument with - -- tcPolyExpr, which uses tcGen and hence checkConstraints. + -- tcPolyExpr, which uses tcSkolemise and hence checkConstraints. -- But with the solver producing unlifted equalities, we need -- to have an EvBindsVar for them when they might be deferred to -- runtime. Otherwise, they end up as top-level unlifted bindings, diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs index 9555c0704a..98b78db450 100644 --- a/compiler/typecheck/TcValidity.hs +++ b/compiler/typecheck/TcValidity.hs @@ -309,11 +309,12 @@ checkValidType ctxt ty RuleSigCtxt _ -> rank1 TySynCtxt _ -> rank0 - ExprSigCtxt -> rank1 - FunSigCtxt {} -> rank1 - InfSigCtxt _ -> ArbitraryRank -- Inferred type - ConArgCtxt _ -> rank1 -- We are given the type of the entire - -- constructor, hence rank 1 + ExprSigCtxt -> rank1 + TypeAppCtxt -> rank0 + FunSigCtxt {} -> rank1 + InfSigCtxt _ -> ArbitraryRank -- Inferred type + ConArgCtxt _ -> rank1 -- We are given the type of the entire + -- constructor, hence rank 1 ForSigCtxt _ -> rank1 SpecInstCtxt -> rank1 @@ -381,6 +382,7 @@ expectedKindInCtxt GhciCtxt = AnythingKind -- The types in a 'default' decl can have varying kinds -- See Note [Extended defaults]" in TcEnv expectedKindInCtxt DefaultDeclCtxt = AnythingKind +expectedKindInCtxt TypeAppCtxt = AnythingKind expectedKindInCtxt (ForSigCtxt _) = TheKind liftedTypeKind expectedKindInCtxt InstDeclCtxt = TheKind constraintKind expectedKindInCtxt SpecInstCtxt = TheKind constraintKind @@ -791,6 +793,7 @@ okIPCtxt :: UserTypeCtxt -> Bool okIPCtxt (FunSigCtxt {}) = True okIPCtxt (InfSigCtxt {}) = True okIPCtxt ExprSigCtxt = True +okIPCtxt TypeAppCtxt = True okIPCtxt PatSigCtxt = True okIPCtxt ResSigCtxt = True okIPCtxt GenSigCtxt = True @@ -1080,7 +1083,7 @@ checkValidInstance ctxt hs_type ty else checkInstTermination inst_tys theta ; case (checkInstCoverage undecidable_ok clas theta inst_tys) of - IsValid -> return () -- Check succeeded + IsValid -> return () -- Check succeeded NotValid msg -> addErrTc (instTypeErr clas inst_tys msg) ; return (tvs, theta, clas, inst_tys) } diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs index 48f7c0f9a9..fd39a17133 100644 --- a/compiler/types/TyCoRep.hs +++ b/compiler/types/TyCoRep.hs @@ -38,9 +38,11 @@ module TyCoRep ( mkFunTy, mkFunTys, isLiftedTypeKind, isUnliftedTypeKind, isCoercionType, isLevityTy, isLevityVar, + sameVis, -- Functions over binders - binderType, delBinderVar, + binderType, delBinderVar, isInvisibleBinder, isVisibleBinder, + isNamedBinder, isAnonBinder, -- Functions over coercions pickLR, @@ -228,19 +230,32 @@ data TyBinder | Anon Type -- visibility is determined by the type (Constraint vs. *) deriving (Data.Typeable, Data.Data) --- | Is something required to appear in source Haskell ('Visible') or --- prohibited from appearing in source Haskell ('Invisible')? -data VisibilityFlag = Visible | Invisible +-- | Is something required to appear in source Haskell ('Visible'), +-- permitted by request ('Specified') (visible type application), or +-- prohibited entirely from appearing in source Haskell ('Invisible')? +-- Examples in Note [VisibilityFlag] +data VisibilityFlag = Visible | Specified | Invisible deriving (Eq, Data.Typeable, Data.Data) +-- | Do these denote the same level of visibility? Except that +-- 'Specified' and 'Invisible' are considered the same. Used +-- for printing. +sameVis :: VisibilityFlag -> VisibilityFlag -> Bool +sameVis Visible Visible = True +sameVis Visible _ = False +sameVis _ Visible = False +sameVis _ _ = True + instance Binary VisibilityFlag where put_ bh Visible = putByte bh 0 - put_ bh Invisible = putByte bh 1 + put_ bh Specified = putByte bh 1 + put_ bh Invisible = putByte bh 2 get bh = do h <- getByte bh case h of 0 -> return Visible + 1 -> return Specified _ -> return Invisible type KindOrType = Type -- See Note [Arguments to type constructors] @@ -309,6 +324,49 @@ two types have the same kind. This allows us to be a little sloppier in keeping track of coercions, which is a good thing. It also means that eqType does not depend on eqCoercion, which is also a good thing. +Note [VisibilityFlag] +~~~~~~~~~~~~~~~~~~~~~ +All named binders are equipped with a visibility flag, which says +whether or not arguments for this binder should be visible (explicit) +in source Haskell. Historically, all named binders (that is, polytype +binders) have been Invisible. But now it's more complicated. + +Invisible: + Argument does not ever appear in source Haskell. With visible type + application, only GHC-generated polytypes have Invisible binders. + This exactly corresponds to "generalized" variables from the + Visible Type Applications paper (ESOP'16). + + Example: f x = x + `f` will be inferred to have type `forall a. a -> a`, where `a` is + Invisible. Note that there is no type annotation for `f`. + + Printing: With -fprint-explicit-foralls, Invisible binders are written + in braces. Otherwise, they are printed like Specified binders. + +Specified: + The argument for this binder may appear in source Haskell only with + visible type application. Otherwise, it is omitted. + + Example: id :: forall a. a -> a + `a` is a Specified binder, because you can say `id @Int` in source Haskell. + + Example: const :: a -> b -> a + Both `a` and `b` are Specified binders, even though they are not bound + by an explicit forall. + + Printing: a list of Specified binders are put between `forall` and `.`: + const :: forall a b. a -> b -> a + +Visible: + The argument must be given. Visible binders come up only with TypeInType. + + Example: data Proxy k (a :: k) = P + The kind of Proxy is forall k -> k -> *, where k is a Visible binder. + + Printing: As in the example above, Visible binders are put between `forall` + and `->`. This syntax is not parsed (yet), however. + ------------------------------------- Note [PredTy] -} @@ -403,6 +461,23 @@ delBinderVarFV :: TyBinder -> FV -> FV delBinderVarFV (Named tv _) vars fv_cand in_scope acc = delFV tv vars fv_cand in_scope acc delBinderVarFV (Anon {}) vars fv_cand in_scope acc = vars fv_cand in_scope acc +-- | Does this binder bind an invisible argument? +isInvisibleBinder :: TyBinder -> Bool +isInvisibleBinder (Named _ vis) = vis /= Visible +isInvisibleBinder (Anon ty) = isPredTy ty + +-- | Does this binder bind a visible argument? +isVisibleBinder :: TyBinder -> Bool +isVisibleBinder = not . isInvisibleBinder + +isNamedBinder :: TyBinder -> Bool +isNamedBinder (Named {}) = True +isNamedBinder _ = False + +isAnonBinder :: TyBinder -> Bool +isAnonBinder (Anon {}) = True +isAnonBinder _ = False + -- | Create the plain type constructor type which has been applied to no type arguments at all. mkTyConTy :: TyCon -> Type mkTyConTy tycon = TyConApp tycon [] @@ -2063,10 +2138,11 @@ ppr_type _ (CoercionTy co) ppr_forall_type :: TyPrec -> Type -> SDoc ppr_forall_type p ty - = maybeParen p FunPrec $ ppr_sigma_type True ty + = maybeParen p FunPrec $ + sdocWithDynFlags $ \dflags -> + ppr_sigma_type dflags True ty -- True <=> we always print the foralls on *nested* quantifiers -- Opt_PrintExplicitForalls only affects top-level quantifiers - -- False <=> we don't print an extra-constraints wildcard ppr_tvar :: TyVar -> SDoc ppr_tvar tv -- Note [Infix type variables] @@ -2090,13 +2166,27 @@ if_print_coercions yes no else no ------------------- -ppr_sigma_type :: Bool -> Type -> SDoc --- First Bool <=> Show the foralls unconditionally --- Second Bool <=> Show an extra-constraints wildcard -ppr_sigma_type show_foralls_unconditionally ty - = sep [ if show_foralls_unconditionally - then pprForAll bndrs - else pprUserForAll bndrs +ppr_sigma_type :: DynFlags + -> Bool -- ^ True <=> Show the foralls unconditionally + -> Type -> SDoc +-- Suppose we have (forall a. Show a => forall b. a -> b). When we're not +-- printing foralls, we want to drop both the (forall a) and the (forall b). +-- This logic does so. +ppr_sigma_type dflags False orig_ty + | not (gopt Opt_PrintExplicitForalls dflags) + , all (isEmptyVarSet . tyCoVarsOfType . binderType) named + -- See Note [When to print foralls] + = sep [ pprThetaArrowTy (map binderType ctxt) + , pprArrowChain TopPrec (ppr_fun_tail tau) ] + where + (invis_bndrs, tau) = split [] orig_ty + (named, ctxt) = partition isNamedBinder invis_bndrs + + split acc (ForAllTy bndr ty) | isInvisibleBinder bndr = split (bndr:acc) ty + split acc ty = (reverse acc, ty) + +ppr_sigma_type _ _ ty + = sep [ pprForAll bndrs , pprThetaArrowTy ctxt , pprArrowChain TopPrec (ppr_fun_tail tau) ] where @@ -2110,12 +2200,13 @@ ppr_sigma_type show_foralls_unconditionally ty split2 ps ty = (reverse ps, ty) -- We don't want to lose synonyms, so we mustn't use splitFunTys here. - ppr_fun_tail (ForAllTy (Anon ty1) ty2) - | not (isPredTy ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2 - ppr_fun_tail other_ty = [ppr_type TopPrec other_ty] +ppr_fun_tail :: Type -> [SDoc] +ppr_fun_tail (ForAllTy (Anon ty1) ty2) + | not (isPredTy ty1) = ppr_type FunPrec ty1 : ppr_fun_tail ty2 +ppr_fun_tail other_ty = [ppr_type TopPrec other_ty] pprSigmaType :: Type -> SDoc -pprSigmaType ty = ppr_sigma_type False ty +pprSigmaType ty = sdocWithDynFlags $ \dflags -> ppr_sigma_type dflags False ty pprUserForAll :: [TyBinder] -> SDoc -- Print a user-level forall; see Note [When to print foralls] @@ -2128,7 +2219,7 @@ pprUserForAll bndrs = not (isEmptyVarSet (tyCoVarsOfType (binderType bndr))) pprForAllImplicit :: [TyVar] -> SDoc -pprForAllImplicit tvs = pprForAll (zipWith Named tvs (repeat Invisible)) +pprForAllImplicit tvs = pprForAll (zipWith Named tvs (repeat Specified)) -- | Render the "forall ... ." or "forall ... ->" bit of a type. -- Do not pass in anonymous binders! @@ -2140,8 +2231,8 @@ pprForAll bndrs@(Named _ vis : _) (bndrs', doc) = ppr_tv_bndrs bndrs vis add_separator stuff = case vis of - Invisible -> stuff <> dot Visible -> stuff <+> arrow + _inv -> stuff <> dot pprForAll bndrs = pprPanic "pprForAll: anonymous binder" (ppr bndrs) pprTvBndrs :: [TyVar] -> SDoc @@ -2154,8 +2245,14 @@ ppr_tv_bndrs :: [TyBinder] -> VisibilityFlag -- ^ visibility of the first binder in the list -> ([TyBinder], SDoc) ppr_tv_bndrs all_bndrs@(Named tv vis : bndrs) vis1 - | vis == vis1 = let (bndrs', doc) = ppr_tv_bndrs bndrs vis1 in - (bndrs', pprTvBndr tv <+> doc) + | vis `sameVis` vis1 = let (bndrs', doc) = ppr_tv_bndrs bndrs vis1 + pp_tv = sdocWithDynFlags $ \dflags -> + if Invisible == vis && + gopt Opt_PrintExplicitForalls dflags + then braces (pprTvBndrNoParens tv) + else pprTvBndr tv + in + (bndrs', pp_tv <+> doc) | otherwise = (all_bndrs, empty) ppr_tv_bndrs [] _ = ([], empty) ppr_tv_bndrs bndrs _ = pprPanic "ppr_tv_bndrs: anonymous binder" (ppr bndrs) @@ -2167,13 +2264,22 @@ pprTvBndr tv where kind = tyVarKind tv +pprTvBndrNoParens :: TyVar -> SDoc +pprTvBndrNoParens tv + | isLiftedTypeKind kind = ppr_tvar tv + | otherwise = ppr_tvar tv <+> dcolon <+> pprKind kind + where + kind = tyVarKind tv + instance Outputable TyBinder where ppr (Named v Visible) = ppr v + ppr (Named v Specified) = char '@' <> ppr v ppr (Named v Invisible) = braces (ppr v) ppr (Anon ty) = text "[anon]" <+> ppr ty instance Outputable VisibilityFlag where ppr Visible = text "[vis]" + ppr Specified = text "[spec]" ppr Invisible = text "[invis]" ----------------- @@ -2231,7 +2337,7 @@ pprDataConWithArgs :: DataCon -> SDoc pprDataConWithArgs dc = sep [forAllDoc, thetaDoc, ppr dc <+> argsDoc] where (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _res_ty) = dataConFullSig dc - forAllDoc = pprUserForAll $ map (\tv -> Named tv Invisible) $ + forAllDoc = pprUserForAll $ map (\tv -> Named tv Specified) $ ((univ_tvs `minusList` map eqSpecTyVar eq_spec) ++ ex_tvs) thetaDoc = pprThetaArrowTy theta argsDoc = hsep (fmap pprParendType arg_tys) diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs index 685ec830f1..fbb59542f8 100644 --- a/compiler/types/Type.hs +++ b/compiler/types/Type.hs @@ -35,7 +35,8 @@ module Type ( splitListTyConApp_maybe, repSplitTyConApp_maybe, - mkForAllTy, mkForAllTys, mkInvForAllTys, mkVisForAllTys, + mkForAllTy, mkForAllTys, mkInvForAllTys, mkSpecForAllTys, + mkVisForAllTys, mkNamedForAllTy, splitForAllTy_maybe, splitForAllTys, splitForAllTy, splitPiTy_maybe, splitPiTys, splitPiTy, @@ -83,6 +84,7 @@ module Type ( predTypeEqRel, -- ** Binders + sameVis, mkNamedBinder, mkAnonBinder, isNamedBinder, isAnonBinder, isIdLikeBinder, binderVisibility, binderVar_maybe, binderVar, binderRelevantType_maybe, caseBinder, @@ -1187,6 +1189,12 @@ mkInvForAllTys :: [TyVar] -> Type -> Type mkInvForAllTys tvs = ASSERT( all isTyVar tvs ) mkForAllTys (map (flip Named Invisible) tvs) +-- | Like mkForAllTys, but assumes all variables are dependent and specified, +-- a common case +mkSpecForAllTys :: [TyVar] -> Type -> Type +mkSpecForAllTys tvs = ASSERT( all isTyVar tvs ) + mkForAllTys (map (flip Named Specified) tvs) + -- | Like mkForAllTys, but assumes all variables are dependent and visible mkVisForAllTys :: [TyVar] -> Type -> Type mkVisForAllTys tvs = ASSERT( all isTyVar tvs ) @@ -1196,6 +1204,7 @@ mkPiType :: Var -> Type -> Type -- ^ Makes a @(->)@ type or an implicit forall type, depending -- on whether it is given a type variable or a term variable. -- This is used, for example, when producing the type of a lambda. +-- Always uses Invisible binders. mkPiTypes :: [Var] -> Type -> Type -- ^ 'mkPiType' for multiple type or value arguments @@ -1422,14 +1431,6 @@ mkNamedBinder = Named mkAnonBinder :: Type -> TyBinder mkAnonBinder = Anon -isNamedBinder :: TyBinder -> Bool -isNamedBinder (Named {}) = True -isNamedBinder _ = False - -isAnonBinder :: TyBinder -> Bool -isAnonBinder (Anon {}) = True -isAnonBinder _ = False - -- | Does this binder bind a variable that is /not/ erased? Returns -- 'True' for anonymous binders. isIdLikeBinder :: TyBinder -> Bool @@ -1448,15 +1449,6 @@ binderVisibility (Anon ty) | isVisibleType ty = Visible | otherwise = Invisible --- | Does this binder bind an invisible argument? -isInvisibleBinder :: TyBinder -> Bool -isInvisibleBinder (Named _ vis) = vis == Invisible -isInvisibleBinder (Anon ty) = isPredTy ty - --- | Does this binder bind a visible argument? -isVisibleBinder :: TyBinder -> Bool -isVisibleBinder = not . isInvisibleBinder - -- | Extract a bound variable in a binder, if any binderVar_maybe :: TyBinder -> Maybe Var binderVar_maybe (Named v _) = Just v |