[Git][ghc/ghc][wip/sand-witch/bidir-ki-check] Merge tc_infer_hs_type and tc_hs_type into one function using ExpType philosophy (#24299, #23639)
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Thu Mar 21 10:09:56 UTC 2024
Andrei Borzenkov pushed to branch wip/sand-witch/bidir-ki-check at Glasgow Haskell Compiler / GHC
Commits:
1420cc46 by Andrei Borzenkov at 2024-03-21T13:54:09+04:00
Merge tc_infer_hs_type and tc_hs_type into one function using ExpType philosophy (#24299, #23639)
This patch implements refactoring which is a prerequisite to
updating kind checking of type patterns. This is a huge simplification
of the main worker that checks kind of HsType.
It also fixes the issues caused by previous code duplication, e.g.
that we didn't add module finalizers from splices in inference mode.
- - - - -
9 changed files:
- compiler/GHC/Rename/Splice.hs
- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- compiler/Language/Haskell/Syntax/Type.hs
- testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout
- + testsuite/tests/th/T24299.hs
- + testsuite/tests/th/T24299.stderr
- testsuite/tests/th/all.T
Changes:
=====================================
compiler/GHC/Rename/Splice.hs
=====================================
@@ -677,7 +677,7 @@ References:
[2] 'rnSpliceExpr'
[3] 'GHC.Tc.Gen.Splice.qAddModFinalizer'
[4] 'GHC.Tc.Gen.Expr.tcExpr' ('HsSpliceE' ('HsSpliced' ...))
-[5] 'GHC.Tc.Gen.HsType.tc_hs_type' ('HsSpliceTy' ('HsSpliced' ...))
+[5] 'GHC.Tc.Gen.HsType.tc_check_hs_type' ('HsSpliceTy' ('HsSpliced' ...))
[6] 'GHC.Tc.Gen.Pat.tc_pat' ('SplicePat' ('HsSpliced' ...))
-}
=====================================
compiler/GHC/Tc/Gen/HsType.hs
=====================================
@@ -609,7 +609,7 @@ tc_top_lhs_type tyki ctxt (L loc sig_ty@(HsSig { sig_bndrs = hs_outer_bndrs
<- pushLevelAndSolveEqualitiesX "tc_top_lhs_type" $
tcOuterTKBndrs skol_info hs_outer_bndrs $
do { kind <- newExpectedKind (expectedKindInCtxt ctxt)
- ; tc_lhs_type (mkMode tyki) body kind }
+ ; tc_check_lhs_type (mkMode tyki) body kind }
; outer_bndrs <- scopedSortOuter outer_bndrs
; let outer_tv_bndrs = outerTyVarBndrs outer_bndrs
@@ -704,7 +704,7 @@ tcHsTypeApp wc_ty kind
-- We are looking at a user-written type, very like a
-- signature so we want to solve its equalities right now
bindNamedWildCardBinders sig_wcs $ \ _ ->
- tc_lhs_type mode hs_ty kind
+ tc_check_lhs_type mode hs_ty kind
-- We do not kind-generalize type applications: we just
-- instantiate with exactly what the user says.
@@ -854,7 +854,7 @@ tcInferLHsTypeUnsaturated :: LHsType GhcRn -> TcM (TcType, TcKind)
tcInferLHsTypeUnsaturated hs_ty
= addTypeCtxt hs_ty $
do { mode <- mkHoleMode TypeLevel HM_Sig -- Allow and report holes
- ; case splitHsAppTys (unLoc hs_ty) of
+ ; case splitHsAppTys_maybe (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 }
@@ -1002,15 +1002,6 @@ that *can* be kind-polymorphic, we implement just the "up" (functions with
"infer" in their name) version, as we gain nothing by also implementing the
"down" version.
-Note [Future-proofing the type checker]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As discussed in Note [Bidirectional type checking], each HsType form is
-handled in *either* tc_infer_hs_type *or* tc_hs_type. These functions
-are mutually recursive, so that either one can work for any type former.
-But, we want to make sure that our pattern-matches are complete. So,
-we have a bunch of repetitive code just so that we get warnings if we're
-missing any patterns.
-
-}
------------------------------------------
@@ -1022,74 +1013,13 @@ tc_infer_lhs_type mode (L span ty)
= setSrcSpanA span $
tc_infer_hs_type mode ty
----------------------------
--- | Call 'tc_infer_hs_type' and check its result against an expected kind.
-tc_infer_hs_type_ek :: HasDebugCallStack => TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
-tc_infer_hs_type_ek mode hs_ty ek
- = do { (ty, k) <- tc_infer_hs_type mode hs_ty
- ; checkExpectedKind hs_ty ty k ek }
-
---------------------------
-- | Infer the kind of a type and desugar. This is the "up" type-checker,
-- as described in Note [Bidirectional type checking]
tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)
-tc_infer_hs_type mode (HsParTy _ t)
- = tc_infer_lhs_type mode t
-
-tc_infer_hs_type mode ty
- | Just (hs_fun_ty, hs_args) <- splitHsAppTys 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)
- = do { let mode' = mode { mode_tyki = KindLevel }
- ; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig
- -- We must typecheck the kind signature, and solve all
- -- its equalities etc; from this point on we may do
- -- things like instantiate its foralls, so it needs
- -- to be fully determined (#14904)
- ; traceTc "tc_infer_hs_type:sig" (ppr ty $$ ppr sig')
- ; ty' <- tcAddKindSigPlaceholders sig $
- tc_lhs_type mode ty sig'
- ; return (ty', sig') }
-
--- HsSpliced is an annotation produced by 'GHC.Rename.Splice.rnSpliceType' to communicate
--- the splice location to the typechecker. Here we skip over it in order to have
--- the same kind inferred for a given expression whether it was produced from
--- splices or not.
---
--- See Note [Delaying modFinalizers in untyped splices].
-tc_infer_hs_type mode (HsSpliceTy (HsUntypedSpliceTop _ ty) _)
- = tc_infer_lhs_type mode ty
-
-tc_infer_hs_type _ (HsSpliceTy (HsUntypedSpliceNested n) s) = pprPanic "tc_infer_hs_type: invalid nested splice" (pprUntypedSplice True (Just n) s)
-
-tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
-
--- See Note [Typechecking HsCoreTys]
-tc_infer_hs_type _ (XHsType ty)
- = do env <- getLclEnv
- -- Raw uniques since we go from NameEnv to TvSubstEnv.
- let subst_prs :: [(Unique, TcTyVar)]
- subst_prs = [ (getUnique nm, tv)
- | ATyVar nm tv <- nonDetNameEnvElts (getLclEnvTypeEnv env) ]
- subst = mkTvSubst
- (mkInScopeSetList $ map snd subst_prs)
- (listToUFM_Directly $ map (fmap mkTyVarTy) subst_prs)
- ty' = substTy subst ty
- return (ty', typeKind ty')
-
-tc_infer_hs_type _ (HsExplicitListTy _ _ tys)
- | null tys -- this is so that we can use visible kind application with '[]
- -- e.g ... '[] @Bool
- = return (mkTyConTy promotedNilDataCon,
- mkSpecForAllTys [alphaTyVar] $ mkListTy alphaTy)
-
-tc_infer_hs_type mode other_ty
- = do { kv <- newMetaKindVar
- ; ty' <- tc_hs_type mode other_ty kv
- ; return (ty', kv) }
+tc_infer_hs_type mode rn_ty
+ = tcInfer $ \exp_kind -> tc_hs_type mode rn_ty exp_kind
{-
Note [Typechecking HsCoreTys]
@@ -1135,14 +1065,24 @@ substitution to each HsCoreTy and all is well:
------------------------------------------
tcLHsType :: LHsType GhcRn -> TcKind -> TcM TcType
tcLHsType hs_ty exp_kind
- = tc_lhs_type typeLevelMode hs_ty exp_kind
+ = tc_check_lhs_type typeLevelMode hs_ty exp_kind
+
+tc_check_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
+tc_check_lhs_type mode (L span ty) exp_kind
+ = setSrcSpanA span $
+ tc_check_hs_type mode ty exp_kind
+
+tc_check_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
+-- See Note [Bidirectional type checking]
+tc_check_hs_type mode ty ek = tc_hs_type mode ty (Check ek)
-tc_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
+tc_lhs_type :: TcTyMode -> LHsType GhcRn -> ExpKind -> TcM TcType
tc_lhs_type mode (L span ty) exp_kind
= setSrcSpanA span $
tc_hs_type mode ty exp_kind
-tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
+tc_hs_type :: TcTyMode -> HsType GhcRn -> ExpKind -> TcM TcType
+-- The main workhorse for type kind checking
-- See Note [Bidirectional type checking]
tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
@@ -1187,8 +1127,8 @@ tc_hs_type mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
| HsForAllVis{} <- tele
= do { ek <- newOpenTypeKind
- ; r <- tc_hs_forall_ty tele ty ek
- ; checkExpectedKind t r ek exp_kind }
+ ; r <- tc_hs_forall_ty tele ty (Check ek)
+ ; checkExpKind t r ek exp_kind }
-- For a visible forall, we require that the body is of kind TYPE r.
-- See Note [Body kind of a HsForAllTy]
@@ -1206,84 +1146,63 @@ tc_hs_type mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
tc_hs_type mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
| null (unLoc ctxt)
= tc_lhs_type mode rn_ty exp_kind
-
- -- See Note [Body kind of a HsQualTy]
- | isConstraintLikeKind exp_kind
+ -- See Note [Body kind of a HsQualTy]
+ | Check kind <- exp_kind, isConstraintLikeKind kind
= do { ctxt' <- tc_hs_context mode ctxt
- ; ty' <- tc_lhs_type mode rn_ty constraintKind
- ; return (tcMkDFunPhiTy ctxt' ty') }
+ ; ty' <- tc_check_lhs_type mode rn_ty constraintKind
+ ; return (tcMkDFunPhiTy ctxt' ty') }
| otherwise
= do { ctxt' <- tc_hs_context mode ctxt
- ; ek <- newOpenTypeKind -- The body kind (result of the function) can
+ ; ek <- newOpenTypeKind -- The body kind (result of the function) can
-- be TYPE r, for any r, hence newOpenTypeKind
- ; ty' <- tc_lhs_type mode rn_ty ek
- ; checkExpectedKind (unLoc rn_ty) (tcMkPhiTy ctxt' ty')
- liftedTypeKind exp_kind }
+ ; ty' <- tc_check_lhs_type mode rn_ty ek
+ ; let res_ty = tcMkPhiTy ctxt' ty'
+ ; checkExpKind (unLoc rn_ty) res_ty
+ liftedTypeKind exp_kind }
--------- Lists, arrays, and tuples
tc_hs_type mode rn_ty@(HsListTy _ elt_ty) exp_kind
- = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
+ = do { tau_ty <- tc_check_lhs_type mode elt_ty liftedTypeKind
; checkWiredInTyCon listTyCon
- ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
-
--- See Note [Distinguishing tuple kinds] in Language.Haskell.Syntax.Type
--- See Note [Inferring tuple kinds]
-tc_hs_type mode rn_ty@(HsTupleTy _ HsBoxedOrConstraintTuple hs_tys) exp_kind
- -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
- | Just tup_sort <- tupKindSort_maybe exp_kind
- = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
- tc_tuple rn_ty mode tup_sort hs_tys exp_kind
- | otherwise
- = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
- ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
- ; kinds <- liftZonkM $ mapM zonkTcType kinds
- -- Infer each arg type separately, because errors can be
- -- confusing if we give them a shared kind. Eg #7410
- -- (Either Int, Int), we do not want to get an error saying
- -- "the second argument of a tuple should have kind *->*"
+ ; checkExpKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
- ; let (arg_kind, tup_sort)
- = case [ (k,s) | k <- kinds
- , Just s <- [tupKindSort_maybe k] ] of
- ((k,s) : _) -> (k,s)
- [] -> (liftedTypeKind, BoxedTuple)
- -- In the [] case, it's not clear what the kind is, so guess *
-
- ; tys' <- sequence [ setSrcSpanA loc $
- checkExpectedKind hs_ty ty kind arg_kind
- | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
-
- ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
-
-
-tc_hs_type mode rn_ty@(HsTupleTy _ HsUnboxedTuple tys) exp_kind
- = tc_tuple rn_ty mode UnboxedTuple tys exp_kind
+tc_hs_type mode rn_ty@(HsTupleTy _ tup_sort tys) exp_kind
+ = do k <- expTypeToType exp_kind
+ tc_hs_tuple_ty rn_ty mode tup_sort tys k
tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
= do { let arity = length hs_tys
; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
- ; tau_tys <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
+ ; tau_tys <- zipWithM (tc_check_lhs_type mode) hs_tys arg_kinds
; let arg_reps = map kindRep arg_kinds
arg_tys = arg_reps ++ tau_tys
sum_ty = mkTyConApp (sumTyCon arity) arg_tys
sum_kind = unboxedSumKind arg_reps
- ; checkExpectedKind rn_ty sum_ty sum_kind exp_kind
+ ; checkExpKind rn_ty sum_ty sum_kind exp_kind
}
--------- Promoted lists and tuples
tc_hs_type mode rn_ty@(HsExplicitListTy _ _ tys) exp_kind
- -- The '[] case is handled in tc_infer_hs_type.
- -- See Note [Future-proofing the type checker].
+ -- for empty list create a `forall a. [a]` kind
+ -- so it is not instantiated too early
+ --
+ -- See Note [Bidirectional type checking]
| null tys
- = tc_infer_hs_type_ek mode rn_ty exp_kind
-
+ = do let ty = mkTyConTy promotedNilDataCon
+ let kind = mkSpecForAllTys [alphaTyVar] $ mkListTy alphaTy
+ checkExpKind rn_ty ty kind exp_kind
+
+ -- for non-empty lists [t1, t2] unify all `t`'s kinds with
+ -- kappa, create a type of form
+ -- (:) @kappa t1 ((:) @kappa t2 ([] @kappa))
+ -- and assign kind [kappa] to it
| otherwise
= do { tks <- mapM (tc_infer_lhs_type mode) tys
; (taus', kind) <- unifyKinds tys tks
; let ty = (foldr (mk_cons kind) (mk_nil kind) taus')
- ; checkExpectedKind rn_ty ty (mkListTy kind) exp_kind }
+ ; checkExpKind rn_ty ty (mkListTy kind) exp_kind }
where
mk_cons k a b = mkTyConApp (promoteDataCon consDataCon) [k, a, b]
mk_nil k = mkTyConApp (promoteDataCon nilDataCon) [k]
@@ -1292,54 +1211,114 @@ tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
-- using newMetaKindVar means that we force instantiations of any polykinded
-- types. At first, I just used tc_infer_lhs_type, but that led to #11255.
= do { ks <- replicateM arity newMetaKindVar
- ; taus <- zipWithM (tc_lhs_type mode) tys ks
+ ; taus <- zipWithM (tc_check_lhs_type mode) tys ks
; let kind_con = tupleTyCon Boxed arity
ty_con = promotedTupleDataCon Boxed arity
tup_k = mkTyConApp kind_con ks
; checkTupSize arity
- ; checkExpectedKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
+ ; checkExpKind rn_ty (mkTyConApp ty_con (ks ++ taus)) tup_k exp_kind }
where
arity = length tys
--------- Constraint types
tc_hs_type mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
= do { massert (isTypeLevel (mode_tyki mode))
- ; ty' <- tc_lhs_type mode ty liftedTypeKind
+ ; ty' <- tc_check_lhs_type mode ty liftedTypeKind
; let n' = mkStrLitTy $ hsIPNameFS n
; ipClass <- tcLookupClass ipClassName
- ; checkExpectedKind rn_ty (mkClassPred ipClass [n',ty'])
+ ; checkExpKind rn_ty (mkClassPred ipClass [n',ty'])
constraintKind exp_kind }
tc_hs_type _ rn_ty@(HsStarTy _ _) exp_kind
-- Desugaring 'HsStarTy' to 'Data.Kind.Type' here means that we don't
-- have to handle it in 'coreView'
- = checkExpectedKind rn_ty liftedTypeKind liftedTypeKind exp_kind
+ = checkExpKind rn_ty liftedTypeKind liftedTypeKind exp_kind
--------- Literals
tc_hs_type _ rn_ty@(HsTyLit _ (HsNumTy _ n)) exp_kind
= do { checkWiredInTyCon naturalTyCon
- ; checkExpectedKind rn_ty (mkNumLitTy n) naturalTy exp_kind }
+ ; checkExpKind rn_ty (mkNumLitTy n) naturalTy exp_kind }
tc_hs_type _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
= do { checkWiredInTyCon typeSymbolKindCon
- ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
+ ; checkExpKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
tc_hs_type _ rn_ty@(HsTyLit _ (HsCharTy _ c)) exp_kind
= do { checkWiredInTyCon charTyCon
- ; checkExpectedKind rn_ty (mkCharLitTy c) charTy exp_kind }
+ ; checkExpKind rn_ty (mkCharLitTy c) charTy exp_kind }
--------- Wildcards
-tc_hs_type mode ty@(HsWildCardTy _) ek
- = tcAnonWildCardOcc NoExtraConstraint mode ty ek
+tc_hs_type mode ty@(HsWildCardTy _) ek
+ = do k <- expTypeToType ek
+ tcAnonWildCardOcc NoExtraConstraint mode ty k
+
+--------- Infer
+tc_hs_type mode rn_ty@(HsTyVar{}) exp_kind = tc_app_ty mode rn_ty exp_kind
+tc_hs_type mode rn_ty@(HsAppTy{}) exp_kind = tc_app_ty mode rn_ty exp_kind
+tc_hs_type mode rn_ty@(HsAppKindTy{}) exp_kind = tc_app_ty mode rn_ty exp_kind
+tc_hs_type mode rn_ty@(HsOpTy{}) exp_kind = tc_app_ty mode rn_ty exp_kind
---------- Potentially kind-polymorphic types: call the "up" checker
--- See Note [Future-proofing the type checker]
-tc_hs_type mode ty@(HsTyVar {}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsAppTy {}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsAppKindTy{}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsOpTy {}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(HsKindSig {}) ek = tc_infer_hs_type_ek mode ty ek
-tc_hs_type mode ty@(XHsType {}) ek = tc_infer_hs_type_ek mode ty ek
+tc_hs_type mode rn_ty@(HsKindSig _ ty sig) exp_kind
+ = do { let mode' = mode { mode_tyki = KindLevel }
+ ; sig' <- tc_lhs_kind_sig mode' KindSigCtxt sig
+ -- We must typecheck the kind signature, and solve all
+ -- its equalities etc; from this point on we may do
+ -- things like instantiate its foralls, so it needs
+ -- to be fully determined (#14904)
+ ; traceTc "tc_hs_type:sig" (ppr ty $$ ppr sig')
+ ; ty' <- tcAddKindSigPlaceholders sig $
+ tc_check_lhs_type mode ty sig'
+ ; checkExpKind rn_ty ty' sig' exp_kind }
+
+-- See Note [Typechecking HsCoreTys]
+tc_hs_type _ rn_ty@(XHsType ty) exp_kind
+ = do env <- getLclEnv
+ -- Raw uniques since we go from NameEnv to TvSubstEnv.
+ let subst_prs :: [(Unique, TcTyVar)]
+ subst_prs = [ (getUnique nm, tv)
+ | ATyVar nm tv <- nonDetNameEnvElts (getLclEnvTypeEnv env) ]
+ subst = mkTvSubst
+ (mkInScopeSetList $ map snd subst_prs)
+ (listToUFM_Directly $ map (fmap mkTyVarTy) subst_prs)
+ ty' = substTy subst ty
+ checkExpKind rn_ty ty' (typeKind ty') exp_kind
+
+tc_hs_tuple_ty :: HsType GhcRn
+ -> TcTyMode
+ -> HsTupleSort
+ -> [LHsType GhcRn]
+ -> TcKind
+ -> TcM TcType
+-- See Note [Distinguishing tuple kinds] in GHC.Hs.Type
+-- See Note [Inferring tuple kinds]
+tc_hs_tuple_ty rn_ty mode HsBoxedOrConstraintTuple hs_tys exp_kind
+ -- (NB: not zonking before looking at exp_k, to avoid left-right bias)
+ | Just tup_sort <- tupKindSort_maybe exp_kind
+ = traceTc "tc_hs_type tuple" (ppr hs_tys) >>
+ tc_tuple rn_ty mode tup_sort hs_tys exp_kind
+ | otherwise
+ = do { traceTc "tc_hs_type tuple 2" (ppr hs_tys)
+ ; (tys, kinds) <- mapAndUnzipM (tc_infer_lhs_type mode) hs_tys
+ ; kinds <- liftZonkM $ mapM zonkTcType kinds
+ -- Infer each arg type separately, because errors can be
+ -- confusing if we give them a shared kind. Eg #7410
+ -- (Either Int, Int), we do not want to get an error saying
+ -- "the second argument of a tuple should have kind *->*"
+
+ ; let (arg_kind, tup_sort)
+ = case [ (k,s) | k <- kinds
+ , Just s <- [tupKindSort_maybe k] ] of
+ ((k,s) : _) -> (k,s)
+ [] -> (liftedTypeKind, BoxedTuple)
+ -- In the [] case, it's not clear what the kind is, so guess *
+
+ ; tys' <- sequence [ setSrcSpanA loc $
+ checkExpectedKind hs_ty ty kind arg_kind
+ | ((L loc hs_ty),ty,kind) <- zip3 hs_tys tys kinds ]
+
+ ; finish_tuple rn_ty tup_sort tys' (map (const arg_kind) tys') exp_kind }
+tc_hs_tuple_ty rn_ty mode HsUnboxedTuple tys exp_kind =
+ tc_tuple rn_ty mode UnboxedTuple tys exp_kind
{-
Note [Variable Specificity and Forall Visibility]
@@ -1366,28 +1345,28 @@ Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo
------------------------------------------
tc_mult :: TcTyMode -> HsArrow GhcRn -> TcM Mult
-tc_mult mode ty = tc_lhs_type mode (arrowToHsType ty) multiplicityTy
+tc_mult mode ty = tc_check_lhs_type mode (arrowToHsType ty) multiplicityTy
------------------------------------------
-tc_fun_type :: TcTyMode -> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> TcKind
+tc_fun_type :: TcTyMode -> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> ExpKind
-> TcM TcType
tc_fun_type mode mult ty1 ty2 exp_kind = case mode_tyki mode of
TypeLevel ->
do { traceTc "tc_fun_type" (ppr ty1 $$ ppr ty2)
; arg_k <- newOpenTypeKind
; res_k <- newOpenTypeKind
- ; ty1' <- tc_lhs_type mode ty1 arg_k
- ; ty2' <- tc_lhs_type mode ty2 res_k
+ ; ty1' <- tc_check_lhs_type mode ty1 arg_k
+ ; ty2' <- tc_check_lhs_type mode ty2 res_k
; mult' <- tc_mult mode mult
- ; checkExpectedKind (HsFunTy noExtField mult ty1 ty2)
- (tcMkVisFunTy mult' ty1' ty2')
- liftedTypeKind exp_kind }
+ ; checkExpKind (HsFunTy noExtField mult ty1 ty2)
+ (tcMkVisFunTy mult' ty1' ty2')
+ liftedTypeKind exp_kind }
KindLevel -> -- no representation polymorphism in kinds. yet.
- do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
- ; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
+ do { ty1' <- tc_check_lhs_type mode ty1 liftedTypeKind
+ ; ty2' <- tc_check_lhs_type mode ty2 liftedTypeKind
; mult' <- tc_mult mode mult
- ; checkExpectedKind (HsFunTy noExtField mult ty1 ty2)
- (tcMkVisFunTy mult' ty1' ty2')
- liftedTypeKind exp_kind }
+ ; checkExpKind (HsFunTy noExtField mult ty1 ty2)
+ (tcMkVisFunTy mult' ty1' ty2')
+ liftedTypeKind exp_kind }
{- Note [Skolem escape and forall-types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1442,7 +1421,7 @@ tc_tuple rn_ty mode tup_sort tys exp_kind
BoxedTuple -> return (replicate arity liftedTypeKind)
UnboxedTuple -> replicateM arity newOpenTypeKind
ConstraintTuple -> return (replicate arity constraintKind)
- ; tau_tys <- zipWithM (tc_lhs_type mode) tys arg_kinds
+ ; tau_tys <- zipWithM (tc_check_lhs_type mode) tys arg_kinds
; finish_tuple rn_ty tup_sort tau_tys arg_kinds exp_kind }
where
arity = length tys
@@ -1530,9 +1509,9 @@ since the two constraints should be semantically equivalent.
* *
********************************************************************* -}
-splitHsAppTys :: HsType GhcRn -> Maybe (LHsType GhcRn, [LHsTypeArg GhcRn])
-splitHsAppTys hs_ty
- | is_app hs_ty = Just (go (noLocA hs_ty) [])
+splitHsAppTys_maybe :: HsType GhcRn -> Maybe (LHsType GhcRn, [LHsTypeArg GhcRn])
+splitHsAppTys_maybe hs_ty
+ | is_app hs_ty = Just (splitHsAppTys hs_ty)
| otherwise = Nothing
where
is_app :: HsType GhcRn -> Bool
@@ -1547,6 +1526,10 @@ splitHsAppTys hs_ty
is_app (HsParTy _ (L _ ty)) = is_app ty
is_app _ = False
+splitHsAppTys :: HsType GhcRn -> (LHsType GhcRn, [LHsTypeArg GhcRn])
+
+splitHsAppTys hs_ty = go (noLocA hs_ty) []
+ where
go :: LHsType GhcRn
-> [HsArg GhcRn (LHsType GhcRn) (LHsKind GhcRn)]
-> (LHsType GhcRn,
@@ -1570,6 +1553,14 @@ tcInferTyAppHead _ (L _ (HsTyVar _ _ (L _ tv)))
tcInferTyAppHead mode ty
= tc_infer_lhs_type mode ty
+tc_app_ty :: TcTyMode -> HsType GhcRn -> ExpKind -> TcM TcType
+tc_app_ty mode rn_ty exp_kind
+ = do { (fun_ty, _ki) <- tcInferTyAppHead mode hs_fun_ty
+ ; (ty, infered_kind) <- tcInferTyApps mode hs_fun_ty fun_ty hs_args
+ ; checkExpKind rn_ty ty infered_kind exp_kind }
+ where
+ (hs_fun_ty, hs_args) = splitHsAppTys rn_ty
+
---------------------------
-- | Apply a type of a given kind to a list of arguments. This instantiates
-- invisible parameters as necessary. Always consumes all the arguments,
@@ -1656,7 +1647,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
; 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
+ tc_check_lhs_type arg_mode hs_ki_arg exp_kind
; traceTc "tcInferTyApps (vis kind app)" (ppr exp_kind)
; (subst', fun') <- mkAppTyM subst fun ki_binder ki_arg
@@ -1687,7 +1678,7 @@ tcInferTyApps_nosat mode orig_hs_ty fun orig_hs_args
, ppr subst ])
; let exp_kind = substTy subst $ piTyBinderType ki_binder
; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
- tc_lhs_type mode arg exp_kind
+ tc_check_lhs_type mode arg exp_kind
; traceTc "tcInferTyApps (vis normal app) 2" (ppr exp_kind)
; (subst', fun') <- mkAppTyM subst fun ki_binder arg'
; go (n+1) fun' subst' inner_ki args }
@@ -1975,6 +1966,19 @@ checkExpectedKind hs_ty ty act_kind exp_kind
n_act_invis_bndrs = invisibleTyBndrCount act_kind
n_to_inst = n_act_invis_bndrs - n_exp_invis_bndrs
+
+-- tyr <- checkExpKind hs_ty ty (act_ki :: Kind) (exp_ki :: ExpKind)
+-- requires that `ty` has kind `act_ki`
+-- It checks that the actual kind `act_ki` matches the expected kind `exp_ki`
+-- and returns `tyr`, a possibly-casted form of `ty`, that has precisely kind `exp_ki`
+-- `hs_ty` is purely for error messages
+checkExpKind :: HsType GhcRn -> TcType -> TcKind -> ExpKind -> TcM TcType
+checkExpKind rn_ty ty ki (Check ki') =
+ checkExpectedKind rn_ty ty ki ki'
+checkExpKind _rn_ty ty ki (Infer cell) = do
+ co <- fillInferResult ki cell
+ pure (ty `mkCastTy` co)
+
---------------------------
tcHsContext :: Maybe (LHsContext GhcRn) -> TcM [PredType]
@@ -1988,7 +1992,7 @@ tc_hs_context :: TcTyMode -> LHsContext GhcRn -> TcM [PredType]
tc_hs_context mode ctxt = mapM (tc_lhs_pred mode) (unLoc ctxt)
tc_lhs_pred :: TcTyMode -> LHsType GhcRn -> TcM PredType
-tc_lhs_pred mode pred = tc_lhs_type mode pred constraintKind
+tc_lhs_pred mode pred = tc_check_lhs_type mode pred constraintKind
---------------------------
tcTyVar :: Name -> TcM (TcType, TcKind)
@@ -4045,7 +4049,7 @@ tcHsPartialSigType ctxt sig_ty
; tau <- -- Don't do (addTypeCtxt hs_tau) here else we get
-- In the type <blah>
-- In the type signature: foo :: <blah>
- tc_lhs_type mode hs_tau ek
+ tc_check_lhs_type mode hs_tau ek
; return (wcs, wcx, theta, tau) }
@@ -4355,8 +4359,8 @@ tc_type_in_pat ctxt hole_mode hs_ty wcs ns ctxt_kind
-- and c.f #16033
bindNamedWildCardBinders wcs $ \ wcs ->
tcExtendNameTyVarEnv tkv_prs $
- do { ek <- newExpectedKind ctxt_kind
- ; ty <- tc_lhs_type mode hs_ty ek
+ do { ek <- newExpectedKind ctxt_kind
+ ; ty <- tc_check_lhs_type mode hs_ty ek
; return (wcs, ty) }
; mapM_ emitNamedTypeHole wcs
@@ -4532,7 +4536,7 @@ tc_lhs_kind_sig mode ctxt hs_kind
-- Result is zonked
= do { kind <- addErrCtxt (text "In the kind" <+> quotes (ppr hs_kind)) $
solveEqualities "tcLHsKindSig" $
- tc_lhs_type mode hs_kind liftedTypeKind
+ tc_check_lhs_type mode hs_kind liftedTypeKind
; traceTc "tcLHsKindSig" (ppr hs_kind $$ ppr kind)
-- No generalization:
; kindGeneralizeNone kind
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -27,7 +27,7 @@ module GHC.Tc.Utils.TcType (
TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcInvisTVBinder, TcReqTVBinder,
TcTyCon, MonoTcTyCon, PolyTcTyCon, TcTyConBinder, KnotTied,
- ExpType(..), InferResult(..),
+ ExpType(..), ExpKind, InferResult(..),
ExpTypeFRR, ExpSigmaType, ExpSigmaTypeFRR,
ExpRhoType,
mkCheckExpType,
@@ -433,6 +433,9 @@ type ExpSigmaTypeFRR = ExpTypeFRR
type ExpRhoType = ExpType
+-- | Like 'ExpType', but on kind level
+type ExpKind = ExpType
+
instance Outputable ExpType where
ppr (Check ty) = text "Check" <> braces (ppr ty)
ppr (Infer ir) = ppr ir
=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -43,6 +43,8 @@ module GHC.Tc.Utils.Unify (
PuResult(..), failCheckWith, okCheckRefl, mapCheck,
TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
famAppArgFlags, simpleUnifyCheck, checkPromoteFreeVars,
+
+ fillInferResult,
) where
import GHC.Prelude
=====================================
compiler/Language/Haskell/Syntax/Type.hs
=====================================
@@ -1006,7 +1006,7 @@ would mean that when we pretty-print it back, we don't know whether the user
wrote '*' or 'Type', and lose the parse/ppr roundtrip property.
As a workaround, we parse '*' as HsStarTy (if it stands for 'Data.Kind.Type')
-and then desugar it to 'Data.Kind.Type' in the typechecker (see tc_hs_type).
+and then desugar it to 'Data.Kind.Type' in the typechecker (see tc_check_hs_type).
When '*' is a regular type operator (StarIsType is disabled), HsStarTy is not
involved.
=====================================
testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout
=====================================
@@ -1,2 +1,2 @@
-_ :: k
+_ :: p
Maybe _ :: *
=====================================
testsuite/tests/th/T24299.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module T24299 where
+import Language.Haskell.TH.Syntax (addModFinalizer, runIO)
+import GHC.Types (Type)
+import System.IO
+
+type Proxy :: forall a. a -> Type
+data Proxy a = MkProxy
+
+check :: ($(addModFinalizer (runIO (do putStrLn "check"; hFlush stdout)) >>
+ [t| Proxy |]) :: Type -> Type) Int -- There is kind signature, we are in check mode
+check = MkProxy
+
+infer :: ($(addModFinalizer (runIO (do putStrLn "infer"; hFlush stdout)) >>
+ [t| Proxy |]) ) Int -- no kind signature, inference mode is enabled
+infer = MkProxy
=====================================
testsuite/tests/th/T24299.stderr
=====================================
@@ -0,0 +1,2 @@
+check
+infer
=====================================
testsuite/tests/th/all.T
=====================================
@@ -604,3 +604,4 @@ test('T24308', normal, compile_and_run, [''])
test('T14032a', normal, compile, [''])
test('T14032e', normal, compile_fail, ['-dsuppress-uniques'])
test('ListTuplePunsTH', [only_ways(['ghci']), extra_files(['ListTuplePunsTH.hs', 'T15843a.hs'])], ghci_script, ['ListTuplePunsTH.script'])
+test('T24299', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1420cc46a84086fbe762f3c173240ec1630ce653
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1420cc46a84086fbe762f3c173240ec1630ce653
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/20240321/56bc7a0a/attachment-0001.html>
More information about the ghc-commits
mailing list