[Git][ghc/ghc][wip/sand-witch/bidir-ki-check] Merge tc_infer_hs_type and tc_hs_type into one function using ExpType philosophy
Andrei Borzenkov (@sand-witch)
gitlab at gitlab.haskell.org
Wed Mar 20 12:51:48 UTC 2024
Andrei Borzenkov pushed to branch wip/sand-witch/bidir-ki-check at Glasgow Haskell Compiler / GHC
Commits:
68888e40 by Andrei Borzenkov at 2024-03-20T16:51:31+04:00
Merge tc_infer_hs_type and tc_hs_type into one function using ExpType philosophy
- - - - -
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,23 @@ 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_lhs_type :: TcTyMode -> LHsType GhcRn -> TcKind -> TcM TcType
+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 -> 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
-- See Note [Bidirectional type checking]
tc_hs_type mode (HsParTy _ ty) exp_kind = tc_lhs_type mode ty exp_kind
@@ -1187,8 +1126,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]
@@ -1204,72 +1143,47 @@ tc_hs_type mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
; return (mkForAllTys tv_bndrs ty') }
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
- = do { ctxt' <- tc_hs_context mode ctxt
- ; ty' <- tc_lhs_type mode rn_ty constraintKind
- ; return (tcMkDFunPhiTy ctxt' ty') }
-
- | otherwise
- = do { ctxt' <- tc_hs_context mode ctxt
+ = do k <- expTypeToType exp_kind
+ tc_hs_qual_ty k
+ where
+ tc_hs_qual_ty kind
+ | null (unLoc ctxt)
+ = tc_check_lhs_type mode rn_ty kind
- ; 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 }
+ -- See Note [Body kind of a HsQualTy]
+ | isConstraintLikeKind kind
+ = do { ctxt' <- tc_hs_context mode ctxt
+ ; 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
+ -- be TYPE r, for any r, hence newOpenTypeKind
+ ; ty' <- tc_check_lhs_type mode rn_ty ek
+ ; let res_ty = tcMkPhiTy ctxt' ty'
+ ; checkExpectedKind (unLoc rn_ty) res_ty
+ liftedTypeKind 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 *->*"
-
- ; 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 }
+ ; checkExpKind rn_ty (mkListTy tau_ty) liftedTypeKind 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
@@ -1277,13 +1191,15 @@ 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].
| 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
| 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 +1208,122 @@ 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
---------- 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
+--------- 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
+
+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
+
+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
{-
Note [Variable Specificity and Forall Visibility]
@@ -1366,28 +1350,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 +1426,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 +1514,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 +1531,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,
@@ -1656,7 +1644,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 +1675,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 +1963,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 +1989,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 +4046,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 +4356,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 +4533,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/68888e40e011c66d3165b3d2fbf652f6f6163e94
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/68888e40e011c66d3165b3d2fbf652f6f6163e94
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/20240320/1232908c/attachment-0001.html>
More information about the ghc-commits
mailing list