[Git][ghc/ghc][wip/T17775] More wibbles
Simon Peyton Jones
gitlab at gitlab.haskell.org
Mon Apr 27 23:52:42 UTC 2020
Simon Peyton Jones pushed to branch wip/T17775 at Glasgow Haskell Compiler / GHC
Commits:
c73bb2ec by Simon Peyton Jones at 2020-04-28T00:52:10+01:00
More wibbles
- - - - -
17 changed files:
- compiler/GHC/Rename/HsType.hs
- compiler/GHC/Tc/Errors.hs
- compiler/GHC/Tc/Gen/Default.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Gen/Sig.hs
- compiler/GHC/Tc/Gen/Splice.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/Types/Constraint.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/dependent/should_fail/T16326_Fail10.stderr
- testsuite/tests/typecheck/should_compile/T10072.stderr
- testsuite/tests/typecheck/should_fail/tcfail206.stderr
Changes:
=====================================
compiler/GHC/Rename/HsType.hs
=====================================
@@ -972,12 +972,12 @@ bindLHsTyVarBndr _doc mb_assoc (L loc
bindLHsTyVarBndr doc mb_assoc (L loc (KindedTyVar x lrdr@(L lv _) kind))
thing_inside
= do { sig_ok <- xoptM LangExt.KindSignatures
- ; unless sig_ok (badKindSigErr doc kind)
- ; (kind', fvs1) <- rnLHsKind doc kind
- ; tv_nm <- newTyVarNameRn mb_assoc lrdr
- ; (b, fvs2) <- bindLocalNamesFV [tv_nm]
- $ thing_inside (L loc (KindedTyVar x (L lv tv_nm) kind'))
- ; return (b, fvs1 `plusFV` fvs2) }
+ ; unless sig_ok (badKindSigErr doc kind)
+ ; (kind', fvs1) <- rnLHsKind doc kind
+ ; tv_nm <- newTyVarNameRn mb_assoc lrdr
+ ; (b, fvs2) <- bindLocalNamesFV [tv_nm]
+ $ thing_inside (L loc (KindedTyVar x (L lv tv_nm) kind'))
+ ; return (b, fvs1 `plusFV` fvs2) }
newTyVarNameRn :: Maybe a -> Located RdrName -> RnM Name
newTyVarNameRn mb_assoc (L loc rdr)
=====================================
compiler/GHC/Tc/Errors.hs
=====================================
@@ -422,10 +422,12 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs
| otherwise
= do { traceTc "reportImplic" (ppr implic')
+ ; when bad_telescope $ reportBadTelescope ctxt tcl_env info tvs
+ -- Do /not/ use the tidied tvs because then are in the
+ -- wrong order, so tidying will rename things wrongly
; reportWanteds ctxt' tc_lvl wanted
; when (cec_warn_redundant ctxt) $
- warnRedundantConstraints ctxt' tcl_env info' dead_givens
- ; when bad_telescope $ reportBadTelescope ctxt' tcl_env info' tvs' }
+ warnRedundantConstraints ctxt' tcl_env info' dead_givens }
where
tcl_env = ic_env implic
insoluble = isInsolubleStatus status
=====================================
compiler/GHC/Tc/Gen/Default.hs
=====================================
@@ -70,8 +70,8 @@ tcDefaults decls@(L locn (DefaultDecl _ _) : _)
tc_default_ty :: [Class] -> LHsType GhcRn -> TcM Type
tc_default_ty deflt_clss hs_ty
- = do { (ty, _kind) <- solveEqualities $
- tcInferLHsType hs_ty
+ = do { ty <- solveEqualities $
+ tcInferLHsType hs_ty
; ty <- zonkTcTypeToType ty -- establish Type invariants
; checkValidType DefaultDeclCtxt ty
=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -436,11 +436,11 @@ tcExpr expr@(SectionR x op arg2) res_ty
= do { (op', op_ty) <- tcInferRhoNC op
; (wrap_fun, [arg1_ty, arg2_ty], op_res_ty)
<- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op)) 2 op_ty
- ; wrap_res <- tcSubTypeHR SectionOrigin expr
- (mkVisFunTy arg1_ty op_res_ty) res_ty
; arg2' <- tcArg (unLoc op) arg2 arg2_ty 2
- ; return ( mkHsWrap wrap_res $
- SectionR x (mkLHsWrap wrap_fun op') arg2' ) }
+ ; let expr' = SectionR x (mkLHsWrap wrap_fun op') arg2'
+ act_res_ty = mkVisFunTy arg1_ty op_res_ty
+ ; tcWrapResultMono expr expr' act_res_ty res_ty }
+
where
fn_orig = lexprCtOrigin op
-- It's important to use the origin of 'op', so that call-stacks
@@ -456,11 +456,10 @@ tcExpr expr@(SectionL x arg1 op) res_ty
; (wrap_fn, (arg1_ty:arg_tys), op_res_ty)
<- matchActualFunTys (mk_op_msg op) fn_orig (Just (unLoc op))
n_reqd_args op_ty
- ; wrap_res <- tcSubTypeHR SectionOrigin expr
- (mkVisFunTys arg_tys op_res_ty) res_ty
; arg1' <- tcArg (unLoc op) arg1 arg1_ty 1
- ; return ( mkHsWrap wrap_res $
- SectionL x arg1' (mkLHsWrap wrap_fn op') ) }
+ ; let expr' = SectionL x arg1' (mkLHsWrap wrap_fn op')
+ act_res_ty = mkVisFunTys arg_tys op_res_ty
+ ; tcWrapResultMono expr expr' act_res_ty res_ty }
where
fn_orig = lexprCtOrigin op
-- It's important to use the origin of 'op', so that call-stacks
@@ -490,18 +489,17 @@ tcExpr expr@(ExplicitTuple x tup_args boxity) res_ty
; arg_tys <- case boxity of
{ Boxed -> newFlexiTyVarTys arity liftedTypeKind
; Unboxed -> replicateM arity newOpenFlexiTyVarTy }
- ; let actual_res_ty
- = mkVisFunTys [ty | (ty, (L _ (Missing _))) <- arg_tys `zip` tup_args]
- (mkTupleTy1 boxity arg_tys)
- -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
-
- ; wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "ExpTuple") expr
- actual_res_ty res_ty
-- Handle tuple sections where
; tup_args1 <- tcTupArgs tup_args arg_tys
- ; return $ mkHsWrap wrap (ExplicitTuple x tup_args1 boxity) }
+ ; let expr' = ExplicitTuple x tup_args1 boxity
+ act_res_ty = mkVisFunTys [ty | (ty, (L _ (Missing _)))
+ <- arg_tys `zip` tup_args]
+ (mkTupleTy1 boxity arg_tys)
+ -- See Note [Don't flatten tuples from HsSyn] in GHC.Core.Make
+
+ ; tcWrapResultMono expr expr' act_res_ty res_ty }
tcExpr (ExplicitSum _ alt arity expr) res_ty
= do { let sum_tc = sumTyCon arity
@@ -673,25 +671,26 @@ tcExpr expr@(RecordCon { rcon_con_name = L loc con_name
; checkMissingFields con_like rbinds
; (con_expr, con_sigma) <- tcInferId con_name
- ; (con_wrap, con_tau) <-
- topInstantiate (OccurrenceOf con_name) con_sigma
+ ; (con_wrap, con_tau) <- topInstantiate orig con_sigma
-- a shallow instantiation should really be enough for
-- a data constructor.
; let arity = conLikeArity con_like
Right (arg_tys, actual_res_ty) = tcSplitFunTysN arity con_tau
- ; case conLikeWrapId_maybe con_like of
- Nothing -> nonBidirectionalErr (conLikeName con_like)
- Just con_id -> do {
- res_wrap <- tcSubTypeHR (Shouldn'tHappenOrigin "RecordCon")
- expr actual_res_ty res_ty
- ; rbinds' <- tcRecordBinds con_like arg_tys rbinds
- ; return $
- mkHsWrap res_wrap $
- RecordCon { rcon_ext = RecordConTc
- { rcon_con_like = con_like
- , rcon_con_expr = mkHsWrap con_wrap con_expr }
- , rcon_con_name = L loc con_id
- , rcon_flds = rbinds' } } }
+ ; case conLikeWrapId_maybe con_like of {
+ Nothing -> nonBidirectionalErr (conLikeName con_like) ;
+ Just con_id ->
+
+ do { rbinds' <- tcRecordBinds con_like arg_tys rbinds
+ ; let rcon_tc = RecordConTc
+ { rcon_con_like = con_like
+ , rcon_con_expr = mkHsWrap con_wrap con_expr }
+ expr' = RecordCon { rcon_ext = rcon_tc
+ , rcon_con_name = L loc con_id
+ , rcon_flds = rbinds' }
+
+ ; tcWrapResultMono expr expr' actual_res_ty res_ty } } }
+ where
+ orig = OccurrenceOf con_name
{-
Note [Type of a record update]
@@ -942,8 +941,6 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
scrut_ty = TcType.substTy scrut_subst con1_res_ty
con1_arg_tys' = map (TcType.substTy result_subst) con1_arg_tys
- ; wrap_res <- tcSubTypeHR (exprCtOrigin expr) expr
- rec_res_ty res_ty
; co_scrut <- unifyType (Just (unLoc record_expr)) record_rho scrut_ty
-- NB: normal unification is OK here (as opposed to subsumption),
-- because for this to work out, both record_rho and scrut_ty have
@@ -973,16 +970,16 @@ tcExpr expr@(RecordUpd { rupd_expr = record_expr, rupd_flds = rbnds }) res_ty
; req_wrap <- instCallConstraints RecordUpdOrigin req_theta'
-- Phew!
- ; return $
- mkHsWrap wrap_res $
- RecordUpd { rupd_expr
- = mkLHsWrap fam_co (mkLHsWrapCo co_scrut record_expr')
- , rupd_flds = rbinds'
- , rupd_ext = RecordUpdTc
- { rupd_cons = relevant_cons
- , rupd_in_tys = scrut_inst_tys
- , rupd_out_tys = result_inst_tys
- , rupd_wrap = req_wrap }} }
+ ; let upd_tc = RecordUpdTc { rupd_cons = relevant_cons
+ , rupd_in_tys = scrut_inst_tys
+ , rupd_out_tys = result_inst_tys
+ , rupd_wrap = req_wrap }
+ expr' = RecordUpd { rupd_expr = mkLHsWrap fam_co $
+ mkLHsWrapCo co_scrut record_expr'
+ , rupd_flds = rbinds'
+ , rupd_ext = upd_tc }
+
+ ; tcWrapResult expr expr' rec_res_ty res_ty }
tcExpr e@(HsRecFld _ f) res_ty
= tcCheckRecSelId e f res_ty
@@ -1401,9 +1398,9 @@ tcArgs fun orig_fun_ty orig_args
_ -> ty_app_err upsilon_ty hs_ty_arg }
go n so_far fun_ty (HsEValArg loc arg : args)
- = do { (wrap, [arg_ty], res_ty)
- <- matchActualFunTysPart herald fun_orig (Just fun)
- n_val_args so_far 1 fun_ty
+ = do { (wrap, arg_ty, res_ty)
+ <- matchActualFunTy herald fun_orig (Just fun)
+ (n_val_args, so_far) fun_ty
; arg' <- tcArg fun arg arg_ty n
; (args', inner_res_ty) <- go (n+1) (arg_ty:so_far) res_ty args
; return ( addArgWrap wrap $ HsEValArg loc arg' : args'
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -419,7 +419,7 @@ tcStandaloneKindSig (L _ kisig) = case kisig of
StandaloneKindSig _ (L _ name) ksig ->
let ctxt = StandaloneKindSigCtxt name in
addSigCtxt ctxt (hsSigType ksig) $
- do { mode <- mkTcTyMode KindLevel
+ do { let mode = mkMode KindLevel
; kind <- tc_top_lhs_type mode ksig (expectedKindInCtxt ctxt)
; checkValidType ctxt kind
; return (name, kind) }
@@ -427,8 +427,7 @@ tcStandaloneKindSig (L _ kisig) = case kisig of
tcTopLHsType :: LHsSigType GhcRn -> ContextKind -> TcM Type
tcTopLHsType hs_ty ctxt_kind
- = do { mode <- mkTcTyMode TypeLevel
- ; tc_top_lhs_type mode hs_ty ctxt_kind }
+ = tc_top_lhs_type (mkMode TypeLevel) hs_ty ctxt_kind
tc_top_lhs_type :: TcTyMode -> LHsSigType GhcRn -> ContextKind -> TcM Type
-- tcTopLHsType is used for kind-checking top-level HsType where
@@ -522,7 +521,7 @@ tcHsTypeApp :: LHsWcType GhcRn -> Kind -> TcM Type
-- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
tcHsTypeApp wc_ty kind
| HsWC { hswc_ext = sig_wcs, hswc_body = hs_ty } <- wc_ty
- = do { mode <- mkMode TypeLevel HM_VTA
+ = do { mode <- mkHoleMode TypeLevel HM_VTA
-- HM_VTA: See Note [Wildcards in visible type application]
; ty <- addTypeCtxt hs_ty $
solveLocalEqualities "tcHsTypeApp" $
@@ -584,7 +583,7 @@ tcFamTyPats fam_tc hs_pats
= do { traceTc "tcFamTyPats {" $
vcat [ ppr fam_tc, text "arity:" <+> ppr fam_arity ]
- ; mode <- mkMode TypeLevel HM_FamPat
+ ; mode <- mkHoleMode TypeLevel HM_FamPat
-- HM_FamPat: See Note [Wildcards in family instances] in
-- GHC.Rename.Module
; let fun_ty = mkTyConApp fam_tc []
@@ -626,27 +625,28 @@ tcCheckLHsType hs_ty exp_kind
do { ek <- newExpectedKind exp_kind
; tcLHsType hs_ty ek }
-tcInferLHsType :: LHsType GhcRn -> TcM (TcType, TcKind)
+tcInferLHsType :: LHsType GhcRn -> TcM TcType
-- Called from outside: set the context
-tcInferLHsType hs_ty = addTypeCtxt hs_ty $
- do { mode <- mkTcTyMode TypeLevel
- ; tc_infer_lhs_type mode hs_ty }
+tcInferLHsType hs_ty
+ = addTypeCtxt hs_ty $
+ do { (ty, _kind) <- tc_infer_lhs_type (mkMode TypeLevel) hs_ty
+ ; return ty }
--- Like tcInferLHsType, but use it in a context where type synonyms and type families
--- do not need to be saturated, like in a GHCi :kind call
+-- Used to check the argument of GHCi :kind
+-- Allow and report wildcards, e.g. :kind T _
+-- Do not saturate family applications: see Note [Dealing with :kind]
tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcInferLHsTypeUnsaturated hs_ty
- | Just (hs_fun_ty, hs_args) <- splitHsAppTys (unLoc hs_ty)
= addTypeCtxt hs_ty $
- do { mode <- mkTcTyMode TypeLevel
- ; (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
- ; tcInferTyApps_nosat mode hs_fun_ty fun_ty hs_args }
- -- Notice the 'nosat'; do not instantiate trailing
- -- invisible arguments of a type family.
- -- See Note [Dealing with :kind]
-
- | otherwise
- = tcInferLHsType hs_ty
+ do { mode <- mkHoleMode TypeLevel HM_Sig -- Allow and report holes
+ ; case splitHsAppTys (unLoc hs_ty) of
+ Just (hs_fun_ty, hs_args)
+ -> do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
+ ; tcInferTyApps_nosat mode hs_fun_ty fun_ty hs_args }
+ -- Notice the 'nosat'; do not instantiate trailing
+ -- invisible arguments of a type family.
+ -- See Note [Dealing with :kind]
+ Nothing -> tc_infer_lhs_type mode hs_ty }
{- Note [Dealing with :kind]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -695,46 +695,39 @@ data TcTyMode
= TcTyMode { mode_tyki :: TypeOrKind
-- See Note [Levels for wildcards]
- , mode_lvl :: TcLevel
- , mode_holes :: HoleMode
+ -- Nothing <=> no wildcards expected
+ , mode_holes :: Maybe (TcLevel, HoleMode)
}
-- HoleMode says how to treat the occurrences
-- of anonymous wildcards; see tcAnonWildCardOcc
-data HoleMode = HM_NoHoles -- No wildcard expected
- | HM_Sig -- Partial type signatures: f :: _ -> Int
+data HoleMode = HM_Sig -- Partial type signatures: f :: _ -> Int
| HM_FamPat -- Family instances: F _ Int = Bool
| HM_VTA -- Visible type and kind application:
-- f @(Maybe _)
-- Maybe @(_ -> _)
-holesOK :: HoleMode -> Bool
--- True <=> it's ok to encounter a hole
--- Should have been checked by the renamer
-holesOK HM_NoHoles = False
-holesOK _ = True
+mkMode :: TypeOrKind -> TcTyMode
+mkMode tyki = TcTyMode { mode_tyki = tyki, mode_holes = Nothing }
-mkTcTyMode :: TypeOrKind -> TcM TcTyMode
-mkTcTyMode tyki = mkMode tyki HM_NoHoles
-
-mkMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
-mkMode tyki hm
+mkHoleMode :: TypeOrKind -> HoleMode -> TcM TcTyMode
+mkHoleMode tyki hm
= do { lvl <- getTcLevel
; return (TcTyMode { mode_tyki = tyki
- , mode_lvl = lvl
- , mode_holes = hm }) }
+ , mode_holes = Just (lvl,hm) }) }
+
+kindLevel :: TcTyMode -> TcTyMode
+kindLevel mode = mode { mode_tyki = KindLevel }
instance Outputable HoleMode where
- ppr HM_NoHoles = text "HM_NoHoles"
ppr HM_Sig = text "HM_Sig"
ppr HM_FamPat = text "HM_FamPat"
ppr HM_VTA = text "HM_VTA"
instance Outputable TcTyMode where
- ppr (TcTyMode { mode_tyki = tyki, mode_lvl = lvl, mode_holes = hm })
+ ppr (TcTyMode { mode_tyki = tyki, mode_holes = hm })
= text "TcTyMode" <+> braces (sep [ ppr tyki <> comma
- , ppr hm <> comma
- , text "lvl:" <> ppr lvl ])
+ , ppr hm ])
{-
Note [Bidirectional type checking]
@@ -809,7 +802,7 @@ tc_infer_hs_type mode (HsParTy _ t)
tc_infer_hs_type mode ty
| Just (hs_fun_ty, hs_args) <- splitHsAppTys ty
- = do { (fun_ty, _ki) <- tcInferAppHead mode hs_fun_ty
+ = do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
; tcInferTyApps mode hs_fun_ty fun_ty hs_args }
tc_infer_hs_type mode (HsKindSig _ ty sig)
@@ -850,8 +843,7 @@ tc_infer_hs_type mode other_ty
------------------------------------------
tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
tcLHsType hs_ty exp_kind
- = do { mode <- mkTcTyMode TypeLevel
- ; tc_lhs_type mode hs_ty exp_kind }
+ = tc_lhs_type (mkMode TypeLevel) hs_ty exp_kind
tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
tc_lhs_type mode (L span ty) exp_kind
@@ -906,9 +898,13 @@ tc_hs_type mode (HsOpTy _ ty1 (L _ op) ty2) exp_kind
tc_hs_type mode forall@(HsForAllTy { hst_fvf = fvf, hst_bndrs = hs_tvs
, hst_body = ty }) exp_kind
= do { (tclvl, wanted, (tvs', ty'))
- <- pushLevelAndCaptureConstraints $
- bindExplicitTKBndrs_Skol hs_tvs $
+ <- pushLevelAndCaptureConstraints $
+ bindExplicitTKBndrs_Skol_M mode hs_tvs $
+ -- The _M variant passes on the mode from the type, to
+ -- any wildards in kind signatures on the forall'd variables
+ -- e.g. f :: _ -> Int -> forall (a :: _). blah
tc_lhs_type mode ty exp_kind
+
-- Do not kind-generalise here! See Note [Kind generalisation]
-- Why exp_kind? See Note [Body kind of HsForAllTy]
; let argf = case fvf of
@@ -1243,14 +1239,14 @@ splitHsAppTys hs_ty
go f as = (f, as)
---------------------------
-tcInferAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
+tcInferTyAppHead :: TcTyMode -> LHsType GhcRn -> TcM (TcType, TcKind)
-- Version of tc_infer_lhs_type specialised for the head of an
-- application. In particular, for a HsTyVar (which includes type
-- constructors, it does not zoom off into tcInferTyApps and family
-- saturation
-tcInferAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
+tcInferTyAppHead mode (L _ (HsTyVar _ _ (L _ tv)))
= tcTyVar mode tv
-tcInferAppHead mode ty
+tcInferTyAppHead mode ty
= tc_infer_lhs_type mode ty
---------------------------
@@ -1337,8 +1333,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
, ppr subst ])
; let exp_kind = substTy subst $ tyBinderType ki_binder
- arg_mode = mode { mode_tyki = KindLevel
- , mode_holes = HM_VTA }
+ ; arg_mode <- mkHoleMode KindLevel HM_VTA
-- HM_VKA: see Note [Wildcards in visible kind application]
; ki_arg <- addErrCtxt (funAppCtxt orig_hs_ty hs_ki_arg n) $
tc_lhs_type arg_mode hs_ki_arg exp_kind
@@ -1654,12 +1649,10 @@ tcHsMbContext Nothing = return []
tcHsMbContext (Just cxt) = tcHsContext cxt
tcHsContext :: LHsContext GhcRn -> TcM [PredType]
-tcHsContext cxt = do { mode <- mkTcTyMode TypeLevel
- ; tc_hs_context mode cxt }
+tcHsContext cxt = tc_hs_context (mkMode TypeLevel) cxt
tcLHsPredType :: LHsType GhcRn -> TcM PredType
-tcLHsPredType pred = do { mode <- mkTcTyMode TypeLevel
- ; tc_lhs_pred mode pred }
+tcLHsPredType pred = tc_lhs_pred (mkMode TypeLevel) pred
tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
@@ -1899,20 +1892,19 @@ newNamedWildTyVar _name -- Currently ignoring the "_x" wildcard name used in t
---------------------------
tcAnonWildCardOcc :: TcTyMode -> HsType GhcRn -> Kind -> TcM TcType
-tcAnonWildCardOcc (TcTyMode { mode_lvl = lvl, mode_holes = hole_mode })
+tcAnonWildCardOcc (TcTyMode { mode_holes = Just (hole_lvl, hole_mode) })
ty exp_kind
- -- mode_lvl field: see Note [Checking partial type signatures]
- -- esp the bullet on nested forall types
- = ASSERT2( holesOK hole_mode, ppr ty )
- do { kv_details <- newTauTvDetailsAtLevel lvl
+ -- hole_lvl: see Note [Checking partial type signatures]
+ -- esp the bullet on nested forall types
+ = do { kv_details <- newTauTvDetailsAtLevel hole_lvl
; kv_name <- newMetaTyVarName (fsLit "k")
- ; wc_details <- newTauTvDetailsAtLevel lvl
+ ; wc_details <- newTauTvDetailsAtLevel hole_lvl
; wc_name <- newMetaTyVarName (fsLit wc_nm)
; let kv = mkTcTyVar kv_name liftedTypeKind kv_details
wc_kind = mkTyVarTy kv
wc_tv = mkTcTyVar wc_name wc_kind wc_details
- ; traceTc "tcAnonWildCardOcc" (ppr lvl <+> ppr emit_holes)
+ ; traceTc "tcAnonWildCardOcc" (ppr hole_lvl <+> ppr emit_holes)
; when emit_holes $
emitAnonWildCardHoleConstraint wc_tv
-- Why the 'when' guard?
@@ -1926,14 +1918,19 @@ tcAnonWildCardOcc (TcTyMode { mode_lvl = lvl, mode_holes = hole_mode })
where
-- See Note [Wildcard names]
wc_nm = case hole_mode of
- HM_Sig -> "w"
- HM_FamPat -> "_"
- HM_VTA -> "w"
+ HM_Sig -> "w"
+ HM_FamPat -> "_"
+ HM_VTA -> "w"
emit_holes = case hole_mode of
- HM_Sig -> True
- HM_FamPat -> False
- HM_VTA -> False
+ HM_Sig -> True
+ HM_FamPat -> False
+ HM_VTA -> False
+
+tcAnonWildCardOcc mode ty _
+-- mode_holes is Nothing. Should not happen, because renamer
+-- should already have rejected holes in unexpected places
+ = pprPanic "tcWildCardOcc" (ppr mode $$ ppr ty)
{- Note [Wildcard names]
~~~~~~~~~~~~~~~~~~~~~~~~
@@ -2822,9 +2819,16 @@ bindExplicitTKBndrs_Skol, bindExplicitTKBndrs_Tv
:: [LHsTyVarBndr GhcRn]
-> TcM a
-> TcM ([TcTyVar], a)
+bindExplicitTKBndrs_Skol_M, bindExplicitTKBndrs_Tv_M
+ :: TcTyMode
+ -> [LHsTyVarBndr GhcRn]
+ -> TcM a
+ -> TcM ([TcTyVar], a)
-bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr newSkolemTyVar)
-bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr cloneTyVarTyVar)
+bindExplicitTKBndrs_Skol = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) newSkolemTyVar)
+bindExplicitTKBndrs_Skol_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) newSkolemTyVar)
+bindExplicitTKBndrs_Tv = bindExplicitTKBndrsX (tcHsTyVarBndr (mkMode KindLevel) cloneTyVarTyVar)
+bindExplicitTKBndrs_Tv_M mode = bindExplicitTKBndrsX (tcHsTyVarBndr (kindLevel mode) cloneTyVarTyVar)
-- newSkolemTyVar: see Note [Non-cloning for tyvar binders]
-- cloneTyVarTyVar: see Note [Cloning for tyvar binders]
@@ -2863,13 +2867,13 @@ bindExplicitTKBndrsX tc_tv hs_tvs thing_inside
; return (tv:tvs, res) }
-----------------
-tcHsTyVarBndr :: (Name -> Kind -> TcM TyVar)
+tcHsTyVarBndr :: TcTyMode -> (Name -> Kind -> TcM TyVar)
-> HsTyVarBndr GhcRn -> TcM TcTyVar
-tcHsTyVarBndr new_tv (UserTyVar _ (L _ tv_nm))
+tcHsTyVarBndr _ new_tv (UserTyVar _ (L _ tv_nm))
= do { kind <- newMetaKindVar
; new_tv tv_nm kind }
-tcHsTyVarBndr new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
- = do { kind <- tcLHsKindSig (TyVarBndrKindCtxt tv_nm) lhs_kind
+tcHsTyVarBndr mode new_tv (KindedTyVar _ (L _ tv_nm) lhs_kind)
+ = do { kind <- tc_lhs_kind_sig mode (TyVarBndrKindCtxt tv_nm) lhs_kind
; new_tv tv_nm kind }
-----------------
@@ -3322,12 +3326,12 @@ tcHsPartialSigType ctxt sig_ty
, hsib_body = hs_ty } <- ib_ty
, (explicit_hs_tvs, L _ hs_ctxt, hs_tau) <- splitLHsSigmaTyInvis hs_ty
= addSigCtxt ctxt hs_ty $
- do { mode <- mkMode TypeLevel HM_Sig
+ do { mode <- mkHoleMode TypeLevel HM_Sig
; (implicit_tvs, (explicit_tvs, (wcs, wcx, theta, tau)))
<- solveLocalEqualities "tcHsPartialSigType" $
tcNamedWildCardBinders sig_wcs $ \ wcs ->
- bindImplicitTKBndrs_Tv implicit_hs_tvs $
- bindExplicitTKBndrs_Tv explicit_hs_tvs $
+ bindImplicitTKBndrs_Tv implicit_hs_tvs $
+ bindExplicitTKBndrs_Tv_M mode explicit_hs_tvs $
do { -- Instantiate the type-class context; but if there
-- is an extra-constraints wildcard, just discard it here
(theta, wcx) <- tcPartialContext mode hs_ctxt
@@ -3457,12 +3461,13 @@ We achieve this as follows:
can't unify with skolem 'a'.
- For /anonymous/ wildcards, such as 'f' above, we carry the ambient
- level of the signature to the hole in the mode_lvl field of
- TcTyMode. Then, in tcAnonWildCardOcc we us that level (and /not/
- the level ambient at the occurrence of "_") to create the
- unificaiton variable for the wildcard. That is the sole
- purpose of the mode_lvl field: to transport the ambient level
- of the signature down to the anonymous wildcard occurrences.
+ level of the signature to the hole in the TcLevel part of the
+ mode_holes field of TcTyMode. Then, in tcAnonWildCardOcc we us that
+ level (and /not/ the level ambient at the occurrence of "_") to
+ create the unification variable for the wildcard. That is the sole
+ purpose of the TcLevel in the mode_holes field: to transport the
+ ambient level of the signature down to the anonymous wildcard
+ occurrences.
Note [Extra-constraint holes in partial type signatures]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3523,19 +3528,21 @@ tcHsPatSigType :: UserTypeCtxt
-- This may emit constraints
-- See Note [Recipe for checking a signature]
tcHsPatSigType ctxt sig_ty
- | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
- , HsIB { hsib_ext = sig_ns
- , hsib_body = hs_ty } <- ib_ty
+ | HsWC { hswc_ext = sig_wcs, hswc_body = ib_ty } <- sig_ty
+ , HsIB { hsib_ext = sig_ns, hsib_body = hs_ty } <- ib_ty
= addSigCtxt ctxt hs_ty $
do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
+ ; mode <- mkHoleMode TypeLevel HM_Sig
; (wcs, sig_ty)
- <- solveLocalEqualities "tcHsPatSigType" $
+ <- addTypeCtxt hs_ty $
+ solveLocalEqualities "tcHsPatSigType" $
-- Always solve local equalities if possible,
-- else casts get in the way of deep skolemisation
-- (#16033)
tcNamedWildCardBinders sig_wcs $ \ wcs ->
tcExtendNameTyVarEnv sig_tkv_prs $
- do { sig_ty <- tcHsOpenType hs_ty
+ do { ek <- newOpenTypeKind
+ ; sig_ty <- tc_lhs_type mode hs_ty ek
; return (wcs, sig_ty) }
; emitNamedWildCardHoleConstraints wcs
@@ -3638,8 +3645,7 @@ It does sort checking and desugaring at the same time, in one single pass.
tcLHsKindSig :: UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tcLHsKindSig ctxt hs_kind
- = do { mode <- mkTcTyMode KindLevel
- ; tc_lhs_kind_sig mode ctxt hs_kind }
+ = tc_lhs_kind_sig (mkMode KindLevel) ctxt hs_kind
tc_lhs_kind_sig :: TcTyMode -> UserTypeCtxt -> LHsKind GhcRn -> TcM Kind
tc_lhs_kind_sig mode ctxt hs_kind
=====================================
compiler/GHC/Tc/Gen/Sig.hs
=====================================
@@ -376,13 +376,13 @@ tcPatSynSig name sig_ty
, hsib_body = hs_ty } <- sig_ty
, (univ_hs_tvs, hs_req, hs_ty1) <- splitLHsSigmaTyInvis hs_ty
, (ex_hs_tvs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
- = do { traceTc "tcPatSynSig 1" (ppr sig_ty)
+ = do { traceTc "tcPatSynSig 1" (ppr sig_ty)
; (implicit_tvs, (univ_tvs, (ex_tvs, (req, prov, body_ty))))
<- pushTcLevelM_ $
solveEqualities $ -- See Note [solveEqualities in tcPatSynSig]
- bindImplicitTKBndrs_Skol implicit_hs_tvs $
- bindExplicitTKBndrs_Skol univ_hs_tvs $
- bindExplicitTKBndrs_Skol ex_hs_tvs $
+ bindImplicitTKBndrs_Skol implicit_hs_tvs $
+ bindExplicitTKBndrs_Skol univ_hs_tvs $
+ bindExplicitTKBndrs_Skol ex_hs_tvs $
do { req <- tcHsContext hs_req
; prov <- tcHsContext hs_prov
; body_ty <- tcHsOpenType hs_body_ty
=====================================
compiler/GHC/Tc/Gen/Splice.hs
=====================================
@@ -1430,7 +1430,7 @@ reifyInstances th_nm th_tys
<- pushTcLevelM_ $
solveEqualities $ -- Avoid error cascade if there are unsolved
bindImplicitTKBndrs_Skol tv_names $
- fst <$> tcInferLHsType rn_ty
+ tcInferLHsType rn_ty
; ty <- zonkTcTypeToType ty
-- Substitute out the meta type variables
-- In particular, the type might have kind
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -920,11 +920,11 @@ It is conceivable to do a better job at tracking whether or not a type
is flattened, but this is left as future work. (Mar '15)
-Note [FunTy and decomposing tycon applications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked.
-This means that we may very well have a FunTy containing a type of some unknown
-kind. For instance, we may have,
+Note [Decomposing FunTy]
+~~~~~~~~~~~~~~~~~~~~~~~~
+can_eq_nc' may attempt to decompose a FunTy that is un-zonked. This
+means that we may very well have a FunTy containing a type of some
+unknown kind. For instance, we may have,
FunTy (a :: k) Int
@@ -1020,24 +1020,26 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
= do { setEvBindIfWanted ev (evCoercion $ mkReflCo (eqRelRole eq_rel) ty1)
; stopWith ev "Equal LitTy" }
--- Try to decompose type constructor applications
--- Including FunTy (s -> t)
-can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
- --- See Note [FunTy and decomposing type constructor applications]
- | FunTy { ft_af = af1, ft_arg = ty1a, ft_res = ty1b } <- ty1
- , FunTy { ft_af = af2, ft_arg = ty2a, ft_res = ty2b } <- ty2
- , af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah)
- , Just ty1a_rep <- getRuntimeRep_maybe ty1a
- , Just ty1b_rep <- getRuntimeRep_maybe ty1b
+-- Decompose FunTy: (s -> t) and (c => t)
+-- NB: don't decompose (Int -> blah) ~ (Show a => blah)
+can_eq_nc' _flat _rdr_env _envs ev eq_rel
+ (FunTy { ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _
+ (FunTy { ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _
+ | af1 == af2 -- Don't decompose (Int -> blah) ~ (Show a => blah)
+ , Just ty1a_rep <- getRuntimeRep_maybe ty1a -- getRutimeRep_maybe:
+ , Just ty1b_rep <- getRuntimeRep_maybe ty1b -- see Note [Decomposing FunTy]
, Just ty2a_rep <- getRuntimeRep_maybe ty2a
, Just ty2b_rep <- getRuntimeRep_maybe ty2b
= canDecomposableTyConAppOK ev eq_rel funTyCon
[ty1a_rep, ty1b_rep, ty1a, ty1b]
[ty2a_rep, ty2b_rep, ty2a, ty2b]
- | TyConApp tc1 tys1 <- ty1
- , TyConApp tc2 tys2 <- ty2
- , not (isTypeFamilyTyCon tc1)
+-- Decompose type constructor applications
+-- NB: e have expanded type synonyms already
+can_eq_nc' _flat _rdr_env _envs ev eq_rel
+ (TyConApp tc1 tys1) _
+ (TyConApp tc2 tys2) _
+ | not (isTypeFamilyTyCon tc1)
, not (isTypeFamilyTyCon tc2)
= canTyConApp ev eq_rel tc1 tys1 tc2 tys2
@@ -1505,7 +1507,6 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
-- the wrong thing (from a pretty printing point of view)
-- for functions, because we've lost the AnonArgFlag; but
-- in fact we never call canTyConApp on a saturated FunTyCon
- -- Note [FunTy and decomposing type constructor applications]
ty1 = mkTyConApp tc1 tys1
ty2 = mkTyConApp tc2 tys2
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -2315,18 +2315,18 @@ newtype instance T [a] :: <kind> where ... -- See Point 5
2. Where these kinds come from: Return kinds are processed through several
different code paths:
- data/newtypes: The return kind is part of the TyCon kind, gotten either
+ Data/newtypes: The return kind is part of the TyCon kind, gotten either
by checkInitialKind (standalone kind signature / CUSK) or
inferInitialKind. It is extracted by bindTyClTyVars in tcTyClDecl1. It is
then passed to tcDataDefn.
- families: The return kind is either written in a standalone signature
+ Families: The return kind is either written in a standalone signature
or extracted from a family declaration in getInitialKind.
If a family declaration is missing a result kind, it is assumed to be
Type. This assumption is in getInitialKind for CUSKs or
get_fam_decl_initial_kind for non-signature & non-CUSK cases.
- instances: The data family already has a known kind. The return kind
+ Instances: The data family already has a known kind. The return kind
of an instance is then calculated by applying the data family tycon
to the patterns provided, as computed by the typeKind lhs_ty in the
end of tcDataFamInstHeader. In the case of an instance written in GADT
@@ -2362,7 +2362,7 @@ newtype instance T [a] :: <kind> where ... -- See Point 5
data T5 :: Bool -- bad
data T6 :: Type -> Bool -- bad
- Exactly the same applies to data instance (but not data famlily)
+ Exactly the same applies to data instance (but not data family)
declarations. Examples
data instance D1 :: Type -- good
data instance D2 :: Boool -> Type -- good
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -852,7 +852,7 @@ tcDataFamInstHeader mb_clsinfo fam_tc imp_vars mb_bndrs fixity
; when (isJust m_ksig) $
checkDataKindSig (DataInstanceSort new_or_data) $
snd $ tcSplitPiTys res_kind
- -- See Note [Datatype return kinds], end of point (4)
+ -- See Note [Datatype return kinds], point (4a)
-- Check that type patterns match the class instance head
-- The call to splitTyConApp_maybe here is just an inlining of
=====================================
compiler/GHC/Tc/Types/Constraint.hs
=====================================
@@ -26,7 +26,7 @@ module GHC.Tc.Types.Constraint (
tyCoVarsOfCt, tyCoVarsOfCts,
tyCoVarsOfCtList, tyCoVarsOfCtsList,
- WantedConstraints(..), insolubleWC, insolubleOrImplicWC,
+ WantedConstraints(..), insolubleWC,
emptyWC, isEmptyWC,
isSolvedWC, andWC, unionsWC, mkSimpleWC, mkImplicWC,
addInsols, dropMisleading, addSimples, addImplics,
@@ -934,7 +934,8 @@ addInsols wc cts
= wc { wc_simple = wc_simple wc `unionBags` cts }
dropMisleading :: WantedConstraints -> WantedConstraints
--- Drop misleading constraints
+-- Drop misleading constraints; really just class constraints
+-- See Note [Constraints and errors] in GHC.Tc.Utils.Monad
dropMisleading (WC { wc_simple = simples, wc_impl = implics })
= WC { wc_simple = filterBag keep_ct simples
, wc_impl = mapBag drop_implic implics }
@@ -943,7 +944,6 @@ dropMisleading (WC { wc_simple = simples, wc_impl = implics })
= implic { ic_wanted = dropMisleading (ic_wanted implic) }
keep_ct ct
| isHoleCt ct = isOutOfScopeCt ct
- | insolubleEqCt ct = True
| otherwise = case classifyPredType (ctPred ct) of
ClassPred {} -> False
_ -> True
@@ -965,17 +965,6 @@ insolubleWC (WC { wc_impl = implics, wc_simple = simples })
= anyBag insolubleCt simples
|| anyBag insolubleImplic implics
-insolubleOrImplicWC :: WantedConstraints -> Bool
--- Any insoluble simple constraints, or any (non-empty) implications
--- The latter are almost certainly skolem-escape violations
-insolubleOrImplicWC (WC { wc_impl = implics, wc_simple = simples })
- = anyBag insolubleCt simples
- || non_empty_implics implics
- where
- non_empty_implics = anyBag (non_empty_wc . ic_wanted)
- non_empty_wc (WC { wc_impl = implics, wc_simple = simples })
- = not (isEmptyBag simples) || non_empty_implics implics
-
insolubleCt :: Ct -> Bool
-- Definitely insoluble, in particular /excluding/ type-hole constraints
-- Namely: a) an equality constraint
=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -125,7 +125,7 @@ data UserTypeCtxt
pprUserTypeCtxt :: UserTypeCtxt -> SDoc
pprUserTypeCtxt (FunSigCtxt n _) = text "the type signature for" <+> quotes (ppr n)
pprUserTypeCtxt (InfSigCtxt n) = text "the inferred type for" <+> quotes (ppr n)
-pprUserTypeCtxt (RuleSigCtxt n) = text "a RULE for" <+> quotes (ppr n)
+pprUserTypeCtxt (RuleSigCtxt n) = text "the type signature for" <+> quotes (ppr n)
pprUserTypeCtxt ExprSigCtxt = text "an expression type signature"
pprUserTypeCtxt KindSigCtxt = text "a kind signature"
pprUserTypeCtxt (StandaloneKindSigCtxt n) = text "a standalone kind signature for" <+> quotes (ppr n)
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -429,11 +429,12 @@ mkSynFunTys arg_tys res_ty = foldr SynFun (SynType res_ty) arg_tys
{-
Note [TcRhoType]
~~~~~~~~~~~~~~~~
-A TcRhoType has no foralls or contexts at the top, or to the right of an arrow
- YES (forall a. a->a) -> Int
+A TcRhoType has no foralls or contexts at the top
NO forall a. a -> Int
NO Eq a => a -> a
- NO Int -> forall a. a -> Int
+ YES a -> a
+ YES (forall a. a->a) -> Int
+ YES Int -> forall a. a -> Int
************************************************************************
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -13,8 +13,9 @@
-- | Type subsumption and unification
module GHC.Tc.Utils.Unify (
-- Full-blown subsumption
- tcWrapResult, tcWrapResultO, tcSkolemise, tcSkolemiseET,
- tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeHR,
+ tcWrapResult, tcWrapResultO, tcWrapResultMono,
+ tcSkolemise, tcSkolemiseET,
+ tcSubType, tcSubTypeSigma, tcSubTypePat,
checkConstraints, checkTvConstraints,
buildImplicationFor, buildTvImplication, emitResidualTvConstraint,
@@ -30,7 +31,7 @@ module GHC.Tc.Utils.Unify (
matchExpectedTyConApp,
matchExpectedAppTy,
matchExpectedFunTys,
- matchActualFunTys, matchActualFunTysPart,
+ matchActualFunTys, matchActualFunTy,
matchExpectedFunKind,
metaTyVarUpdateOK, occCheckForErrors, MetaTyVarUpdateResult(..)
@@ -216,7 +217,7 @@ matchExpectedFunTys herald ctx arity orig_ty thing_inside
; more_arg_tys <- mapM readExpType more_arg_tys
; res_ty <- readExpType res_ty
; let unif_fun_ty = mkVisFunTys more_arg_tys res_ty
- ; wrap <- tcSubType AppOrigin GenSigCtxt unif_fun_ty fun_ty
+ ; wrap <- tcSubType AppOrigin ctx unif_fun_ty fun_ty
-- Not a good origin at all :-(
; return (wrap, result) }
@@ -237,31 +238,45 @@ matchActualFunTys :: SDoc -- See Note [Herald for matchExpectedFunTys]
-> Maybe (HsExpr GhcRn) -- the thing with type TcSigmaType
-> Arity
-> TcSigmaType
- -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
--- If matchActualFunTys n ty = (wrap, [t1,..,tn], ty_r)
--- then wrap : ty ~> (t1 -> ... -> tn -> ty_r)
+ -> TcM (HsWrapper, [TcSigmaType], TcRhoType)
+-- If matchActualFunTys n ty = (wrap, [t1,..,tn], res_ty)
+-- then wrap : ty ~> (t1 -> ... -> tn -> res_ty)
+-- and res_ty is a RhoType
matchActualFunTys herald ct_orig mb_thing n_val_args_wanted fun_ty
- = matchActualFunTysPart herald ct_orig mb_thing
- n_val_args_wanted []
- n_val_args_wanted fun_ty
+ = go n_val_args_wanted [] fun_ty
+ where
+ go 0 _ fun_ty
+ = do { (wrap, rho) <- topInstantiate ct_orig fun_ty
+ ; return (wrap, [], rho) }
+ go n so_far fun_ty
+ = do { (wrap_fun1, arg_ty1, res_ty1) <- matchActualFunTy herald ct_orig mb_thing
+ (n_val_args_wanted, so_far)
+ fun_ty
+ ; (wrap_res, arg_tys, res_ty) <- go (n-1) (arg_ty1:so_far) res_ty1
+ ; let wrap_fun2 = mkWpFun idHsWrapper wrap_res arg_ty1 res_ty doc
+ ; return (wrap_fun2 <.> wrap_fun1, arg_ty1:arg_tys, res_ty) }
+ where
+ doc = text "When inferring the argument type of a function with type" <+>
+ quotes (ppr fun_ty)
-- | Variant of 'matchActualFunTys' that works when supplied only part
-- (that is, to the right of some arrows) of the full function type
-matchActualFunTysPart
+matchActualFunTy
:: SDoc -- See Note [Herald for matchExpectedFunTys]
-> CtOrigin
- -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType
- -> Arity -- Total number of value args in the call
- -> [TcSigmaType] -- Types of values args to which function has
- -- been applied already (reversed)
- -> Arity -- Number of new value args wanted
+ -> Maybe (HsExpr GhcRn) -- The thing with type TcSigmaType
+ -> (Arity, [TcSigmaType]) -- Total number of value args in the call, and
+ -- types of values args to which function has
+ -- been applied already (reversed)
+ -- Both are used only for error messages)
-> TcSigmaType -- Type to analyse
- -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
+ -> TcM (HsWrapper, TcSigmaType, TcSigmaType)
-- See Note [matchActualFunTys error handling] for all these arguments
-matchActualFunTysPart herald ct_orig mb_thing
- n_val_args_in_call arg_tys_so_far
- n_val_args_wanted fun_ty
- = go n_val_args_wanted arg_tys_so_far fun_ty
+-- If (wrap, arg_ty, res_ty) = matchActualFunTy ... fun_ty
+-- then wrap :: fun_ty ~> (arg_ty -> res_ty)
+-- and NB: res_ty is an (uninstantiated) SigmaType
+matchActualFunTy herald ct_orig mb_thing err_info fun_ty
+ = go fun_ty
-- Does not allocate unnecessary meta variables: if the input already is
-- a function, we just take it apart. Not only is this efficient,
-- it's important for higher rank: the argument might be of form
@@ -288,40 +303,28 @@ matchActualFunTysPart herald ct_orig mb_thing
-- bizarre to build the HsWrapper but not the arg_tys.
--
-- Refactoring is welcome.
- go :: Arity
- -> [TcSigmaType] -- Types of value args to which the function has
- -- been applied so far (reversed)
- -- Used only for error messages
- -> TcSigmaType -- the remainder of the type as we're processing
- -> TcM (HsWrapper, [TcSigmaType], TcSigmaType)
- go 0 _ ty = return (idHsWrapper, [], ty)
-
- go n so_far ty
- | Just ty' <- tcView ty = go n so_far ty'
-
- go n so_far ty
+ go :: TcSigmaType -- the remainder of the type as we're processing
+ -> TcM (HsWrapper, TcSigmaType, TcSigmaType)
+ go ty | Just ty' <- tcView ty = go ty'
+
+ go ty
| not (null tvs && null theta)
= do { (wrap1, rho) <- topInstantiate ct_orig ty
- ; (wrap2, arg_tys, res_ty) <- go n so_far rho
- ; return (wrap2 <.> wrap1, arg_tys, res_ty) }
+ ; (wrap2, arg_ty, res_ty) <- go rho
+ ; return (wrap2 <.> wrap1, arg_ty, res_ty) }
where
(tvs, theta, _) = tcSplitSigmaTy ty
- go n so_far (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
+ go (FunTy { ft_af = af, ft_arg = arg_ty, ft_res = res_ty })
= ASSERT( af == VisArg )
- do { (wrap_res, tys, ty_r) <- go (n-1) (arg_ty:so_far) res_ty
- ; return ( mkWpFun idHsWrapper wrap_res arg_ty ty_r doc
- , arg_ty : tys, ty_r ) }
- where
- doc = text "When inferring the argument type of a function with type" <+>
- quotes (ppr fun_ty)
+ return (idHsWrapper, arg_ty, res_ty)
- go n so_far ty@(TyVarTy tv)
+ go ty@(TyVarTy tv)
| isMetaTyVar tv
= do { cts <- readMetaTyVar tv
; case cts of
- Indirect ty' -> go n so_far ty'
- Flexi -> defer n ty }
+ Indirect ty' -> go ty'
+ Flexi -> defer ty }
-- In all other cases we bale out into ordinary unification
-- However unlike the meta-tyvar case, we are sure that the
@@ -338,22 +341,23 @@ matchActualFunTysPart herald ct_orig mb_thing
--
-- But in that case we add specialized type into error context
-- anyway, because it may be useful. See also #9605.
- go n so_far ty = addErrCtxtM (mk_ctxt so_far ty) (defer n ty)
+ go ty = addErrCtxtM (mk_ctxt ty) (defer ty)
------------
- defer n fun_ty
- = do { arg_tys <- replicateM n newOpenFlexiTyVarTy
- ; res_ty <- newOpenFlexiTyVarTy
- ; let unif_fun_ty = mkVisFunTys arg_tys res_ty
+ defer fun_ty
+ = do { arg_ty <- newOpenFlexiTyVarTy
+ ; res_ty <- newOpenFlexiTyVarTy
+ ; let unif_fun_ty = mkVisFunTy arg_ty res_ty
; co <- unifyType mb_thing fun_ty unif_fun_ty
- ; return (mkWpCastN co, arg_tys, res_ty) }
+ ; return (mkWpCastN co, arg_ty, res_ty) }
------------
- mk_ctxt :: [TcType] -> TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
- mk_ctxt arg_tys res_ty env
+ mk_ctxt :: TcType -> TidyEnv -> TcM (TidyEnv, MsgDoc)
+ mk_ctxt res_ty env
= do { (env', ty) <- zonkTidyTcType env $
- mkVisFunTys (reverse arg_tys) res_ty
+ mkVisFunTys (reverse arg_tys_so_far) res_ty
; return (env', mk_fun_tys_msg herald ty n_val_args_in_call) }
+ (n_val_args_in_call, arg_tys_so_far) = err_info
mk_fun_tys_msg :: SDoc -> TcType -> Arity -> SDoc
mk_fun_tys_msg herald ty n_args_in_call
@@ -510,6 +514,35 @@ expected_ty.
-}
+-----------------
+-- tcWrapResult needs both un-type-checked (for origins and error messages)
+-- and type-checked (for wrapping) expressions
+tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+ -> TcM (HsExpr GhcTcId)
+tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
+
+tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
+ -> TcM (HsExpr GhcTcId)
+tcWrapResultO orig rn_expr expr actual_ty res_ty
+ = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty
+ , text "Expected:" <+> ppr res_ty ])
+ ; wrap <- tcSubTypeNC orig GenSigCtxt (Just rn_expr) actual_ty res_ty
+ ; return (mkHsWrap wrap expr) }
+
+tcWrapResultMono :: HsExpr GhcRn -> HsExpr GhcTcId
+ -> TcRhoType -- Actual -- a rho-type not a sigma-type
+ -> ExpRhoType -- Expected
+ -> TcM (HsExpr GhcTcId)
+-- A version of tcWrapResult to use when the actual type is a
+-- rho-type, so nothing to instantiate; just go straight to unify.
+-- It means we don't need to pass in a CtOrigin
+tcWrapResultMono rn_expr expr act_ty res_ty
+ = ASSERT2( isRhoTy act_ty, ppr act_ty $$ ppr rn_expr )
+ do { co <- case res_ty of
+ Infer inf_res -> fillInferResult act_ty inf_res
+ Check exp_ty -> unifyType (Just rn_expr) act_ty exp_ty
+ ; return (mkHsWrapCo co expr) }
+
------------------------
tcSubTypePat :: CtOrigin -> UserTypeCtxt
-> ExpSigmaType -> TcSigmaType -> TcM HsWrapper
@@ -527,17 +560,16 @@ tcSubTypePat _ _ (Infer inf_res) ty_expected
; return (mkWpCastN (mkTcSymCo co)) }
---------------
-tcSubType :: CtOrigin -> UserTypeCtxt -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
+tcSubType :: CtOrigin -> UserTypeCtxt
+ -> TcSigmaType -- Actual
+ -> ExpRhoType -- Expected
+ -> TcM HsWrapper
+-- Checks that 'actual' is more polymorphic than 'expected'
tcSubType orig ctxt ty_actual ty_expected
= addSubTypeCtxt ty_actual ty_expected $
do { traceTc "tcSubType" (vcat [pprUserTypeCtxt ctxt, ppr ty_actual, ppr ty_expected])
; tcSubTypeNC orig ctxt Nothing ty_actual ty_expected }
--- | Call this variant when you are in a higher-rank situation
-tcSubTypeHR :: CtOrigin -> HsExpr GhcRn -> TcSigmaType -> ExpRhoType -> TcM HsWrapper
-tcSubTypeHR orig expr
- = tcSubTypeNC orig GenSigCtxt (Just expr)
-
tcSubTypeNC :: CtOrigin -- origin used for instantiation only
-> UserTypeCtxt
-> Maybe (HsExpr GhcRn) -- The expression that has type 'actual' (if known)
@@ -699,24 +731,6 @@ to a UserTypeCtxt of GenSigCtxt. Why?
See Note [When to build an implication]
-}
------------------
--- needs both un-type-checked (for origins) and type-checked (for wrapping)
--- expressions
-tcWrapResult :: HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
- -> TcM (HsExpr GhcTcId)
-tcWrapResult rn_expr = tcWrapResultO (exprCtOrigin rn_expr) rn_expr
-
--- | Sometimes we don't have a @HsExpr Name@ to hand, and this is more
--- convenient.
-tcWrapResultO :: CtOrigin -> HsExpr GhcRn -> HsExpr GhcTcId -> TcSigmaType -> ExpRhoType
- -> TcM (HsExpr GhcTcId)
-tcWrapResultO orig rn_expr expr actual_ty res_ty
- = do { traceTc "tcWrapResult" (vcat [ text "Actual: " <+> ppr actual_ty
- , text "Expected:" <+> ppr res_ty ])
- ; cow <- tcSubTypeNC orig GenSigCtxt (Just rn_expr)
- actual_ty res_ty
- ; return (mkHsWrap cow expr) }
-
{- **********************************************************************
%* *
@@ -1550,7 +1564,7 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
swapOverTyVars :: Bool -> TcTyVar -> TcTyVar -> Bool
swapOverTyVars is_given tv1 tv2
- -- See Note [Get unification variables on the left]
+ -- See Note [Unification variables on the left]
| not is_given, pri1 == 0, pri2 > 0 = True
| not is_given, pri2 == 0, pri1 > 0 = False
=====================================
testsuite/tests/dependent/should_fail/T16326_Fail10.stderr
=====================================
@@ -3,5 +3,5 @@ T16326_Fail10.hs:12:18: error:
• Illegal visible, dependent quantification in the type of a term:
forall a -> a -> a
(GHC does not yet support this)
- • In a RULE for ‘x’: forall a -> a -> a
+ • In the type signature for ‘x’: forall a -> a -> a
When checking the transformation rule "flurmp"
=====================================
testsuite/tests/typecheck/should_compile/T10072.stderr
=====================================
@@ -6,5 +6,5 @@ T10072.hs:3:31: error:
at T10072.hs:3:1-47
To use the inferred type, enable PartialTypeSignatures
• In the type ‘a -> _’
- In a RULE for ‘f’: a -> _
+ In the type signature for ‘f’: a -> _
When checking the transformation rule "map/empty"
=====================================
testsuite/tests/typecheck/should_fail/tcfail206.stderr
=====================================
@@ -17,7 +17,7 @@ tcfail206.hs:8:5: error:
tcfail206.hs:11:5: error:
• Couldn't match type ‘a’ with ‘Bool’
Expected: a -> (a, Bool)
- Actual: a -> (a, a)
+ Actual: a -> (Bool, a)
‘a’ is a rigid type variable bound by
the type signature for:
c :: forall a. a -> (a, Bool)
@@ -45,7 +45,7 @@ tcfail206.hs:17:5: error:
tcfail206.hs:20:5: error:
• Couldn't match type ‘a’ with ‘Bool’
Expected: a -> (# a, Bool #)
- Actual: a -> (# a, a #)
+ Actual: a -> (# Bool, a #)
‘a’ is a rigid type variable bound by
the type signature for:
f :: forall a. a -> (# a, Bool #)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c73bb2ecfa4aec49a915777adc698bc8839e9e71
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c73bb2ecfa4aec49a915777adc698bc8839e9e71
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200427/590ab62b/attachment-0001.html>
More information about the ghc-commits
mailing list