[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 13 14:02:07 UTC 2024



Andrei Borzenkov pushed to branch wip/sand-witch/bidir-ki-check at Glasgow Haskell Compiler / GHC


Commits:
1eb6c06e by Andrei Borzenkov at 2024-03-13T18:01:48+04:00
Merge tc_infer_hs_type and tc_hs_type into one function using ExpType philosophy

- - - - -


6 changed files:

- compiler/GHC/Tc/Gen/HsType.hs
- compiler/GHC/Tc/Utils/Unify.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/Tc/Gen/HsType.hs
=====================================
@@ -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 }
@@ -1022,74 +1022,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_exp mode rn_ty exp_kind
 
 {-
 Note [Typechecking HsCoreTys]
@@ -1144,15 +1083,33 @@ tc_lhs_type mode (L span ty) exp_kind
 
 tc_hs_type :: TcTyMode -> HsType GhcRn -> TcKind -> TcM TcType
 -- See Note [Bidirectional type checking]
+tc_hs_type mode ty ek = tc_hs_type_exp mode ty (Check ek)
+
+type ExpKind = ExpType
+
+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)
+
+tc_lhs_type_exp :: TcTyMode -> LHsType GhcRn -> ExpKind -> TcM TcType
+tc_lhs_type_exp mode (L span ty) exp_kind
+  = setSrcSpanA span $
+    tc_hs_type_exp mode ty exp_kind
+
+tc_hs_type_exp :: 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
-tc_hs_type mode (HsDocTy _ ty _) exp_kind = tc_lhs_type mode ty exp_kind
-tc_hs_type _ ty@(HsBangTy _ bang _) _
+tc_hs_type_exp mode (HsParTy _ ty)   exp_kind = tc_lhs_type_exp mode ty exp_kind
+tc_hs_type_exp mode (HsDocTy _ ty _) exp_kind = tc_lhs_type_exp mode ty exp_kind
+tc_hs_type_exp _ ty@(HsBangTy _ bang _) _
     -- While top-level bangs at this point are eliminated (eg !(Maybe Int)),
     -- other kinds of bangs are not (eg ((!Maybe) Int)). These kinds of
     -- bangs are invalid, so fail. (#7210, #14761)
     = failWith $ TcRnUnexpectedAnnotation ty bang
-tc_hs_type _ ty@(HsRecTy {})      _
+tc_hs_type_exp _ ty@(HsRecTy {})      _
       -- Record types (which only show up temporarily in constructor
       -- signatures) should have been removed by now
     = failWithTc $ TcRnIllegalRecordSyntax (Right ty)
@@ -1162,23 +1119,25 @@ tc_hs_type _ ty@(HsRecTy {})      _
 -- while capturing the local environment.
 --
 -- See Note [Delaying modFinalizers in untyped splices].
-tc_hs_type mode (HsSpliceTy (HsUntypedSpliceTop mod_finalizers ty) _)
+tc_hs_type_exp mode (HsSpliceTy (HsUntypedSpliceTop mod_finalizers ty) _)
            exp_kind
   = do addModFinalizersWithLclEnv mod_finalizers
-       tc_lhs_type mode ty exp_kind
+       tc_lhs_type_exp mode ty exp_kind
 
-tc_hs_type _ (HsSpliceTy (HsUntypedSpliceNested n) s) _ = pprPanic "tc_hs_type: invalid nested splice" (pprUntypedSplice True (Just n) s)
+tc_hs_type_exp _ (HsSpliceTy (HsUntypedSpliceNested n) s) _ = pprPanic "tc_hs_type_exp: invalid nested splice" (pprUntypedSplice True (Just n) s)
 
 ---------- Functions and applications
-tc_hs_type mode (HsFunTy _ mult ty1 ty2) exp_kind
-  = tc_fun_type mode mult ty1 ty2 exp_kind
+tc_hs_type_exp mode (HsFunTy _ mult ty1 ty2) exp_kind
+  = do k <- expTypeToType exp_kind
+       tc_fun_type mode mult ty1 ty2 k
 
-tc_hs_type mode (HsOpTy _ _ ty1 (L _ op) ty2) exp_kind
+tc_hs_type_exp mode (HsOpTy _ _ ty1 (L _ op) ty2) exp_kind
   | op `hasKey` unrestrictedFunTyConKey
-  = tc_fun_type mode (HsUnrestrictedArrow noExtField) ty1 ty2 exp_kind
+  = do k <- expTypeToType exp_kind
+       tc_fun_type mode (HsUnrestrictedArrow noExtField) ty1 ty2 k
 
 --------- Foralls
-tc_hs_type mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
+tc_hs_type_exp mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
   | HsForAllInvis{} <- tele
   = tc_hs_forall_ty tele ty exp_kind
                  -- For an invisible forall, we allow the body to have
@@ -1187,15 +1146,15 @@ 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]
 
   where
     tc_hs_forall_ty tele ty ek
       = do { (tv_bndrs, ty') <- tcTKTelescope mode tele $
-                                tc_lhs_type mode ty ek
+                                tc_lhs_type_exp mode ty ek
                  -- Pass on the mode from the type, to any wildcards
                  -- in kind signatures on the forall'd variables
                  -- e.g.      f :: _ -> Int -> forall (a :: _). blah
@@ -1203,65 +1162,40 @@ tc_hs_type mode t@(HsForAllTy { hst_tele = tele, hst_body = ty }) exp_kind
              -- Do not kind-generalise here!  See Note [Kind generalisation]
            ; 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') }
+tc_hs_type_exp mode (HsQualTy { hst_ctxt = ctxt, hst_body = rn_ty }) exp_kind
+  = do k <- expTypeToType exp_kind
+       tc_hs_qual_ty k
+  where
+    tc_hs_qual_ty kind
+      | null (unLoc ctxt)
+      = tc_lhs_type mode rn_ty kind
 
-  | 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_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_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_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
+tc_hs_type_exp mode rn_ty@(HsListTy _ elt_ty) exp_kind
   = do { tau_ty <- tc_lhs_type mode elt_ty liftedTypeKind
        ; checkWiredInTyCon listTyCon
-       ; checkExpectedKind rn_ty (mkListTy tau_ty) liftedTypeKind exp_kind }
+       ; checkExpKind 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 *->*"
+tc_hs_type_exp 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
 
-       ; 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@(HsSumTy _ hs_tys) exp_kind
+tc_hs_type_exp 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
@@ -1269,26 +1203,28 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
              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
+tc_hs_type_exp 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]
 
-tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
+tc_hs_type_exp 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
@@ -1297,49 +1233,117 @@ tc_hs_type mode rn_ty@(HsExplicitTupleTy _ tys) exp_kind
              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
+tc_hs_type_exp mode rn_ty@(HsIParamTy _ (L _ n) ty) exp_kind
   = do { massert (isTypeLevel (mode_tyki mode))
        ; ty' <- tc_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
+tc_hs_type_exp _ 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
+tc_hs_type_exp _ 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
+tc_hs_type_exp _ rn_ty@(HsTyLit _ (HsStrTy _ s)) exp_kind
   = do { checkWiredInTyCon typeSymbolKindCon
-       ; checkExpectedKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
-tc_hs_type _ rn_ty@(HsTyLit _ (HsCharTy _ c)) exp_kind
+       ; checkExpKind rn_ty (mkStrLitTy s) typeSymbolKind exp_kind }
+tc_hs_type_exp _ 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_exp 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_exp mode rn_ty@(HsTyVar{})     exp_kind = tc_app_ty mode rn_ty exp_kind
+tc_hs_type_exp mode rn_ty@(HsAppTy{})     exp_kind = tc_app_ty mode rn_ty exp_kind
+tc_hs_type_exp mode rn_ty@(HsAppKindTy{}) exp_kind = tc_app_ty mode rn_ty exp_kind
+tc_hs_type_exp mode rn_ty@(HsOpTy{})      exp_kind = tc_app_ty mode rn_ty exp_kind
+
+tc_hs_type_exp 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_exp:sig" (ppr ty $$ ppr sig')
+       ; ty' <- tcAddKindSigPlaceholders sig $
+                tc_lhs_type mode ty sig'
+       ; checkExpKind rn_ty ty' sig' exp_kind }
+
+-- See Note [Typechecking HsCoreTys]
+tc_hs_type_exp _ 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_exp tuple" (ppr hs_tys) >>
+    tc_tuple rn_ty mode tup_sort hs_tys exp_kind
+  | otherwise
+  = do { traceTc "tc_hs_type_exp 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]
@@ -1530,9 +1534,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 +1551,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,
@@ -4355,7 +4363,7 @@ 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
+               do { ek <- newExpectedKind ctxt_kind
                   ; ty <- tc_lhs_type mode hs_ty ek
                   ; return (wcs, ty) }
 


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -43,6 +43,9 @@ module GHC.Tc.Utils.Unify (
   PuResult(..), failCheckWith, okCheckRefl, mapCheck,
   TyEqFlags(..), TyEqFamApp(..), AreUnifying(..), LevelCheck(..), FamAppBreaker,
   famAppArgFlags, simpleUnifyCheck, checkPromoteFreeVars,
+
+  -- Is that safe?
+  fillInferResult,
   ) where
 
 import GHC.Prelude


=====================================
testsuite/tests/partial-sigs/should_run/GHCiWildcardKind.stdout
=====================================
@@ -1,2 +1,2 @@
-_ :: k
+_ :: p
 Maybe _ :: *


=====================================
testsuite/tests/th/T24299.hs
=====================================
@@ -0,0 +1,16 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module T24299 where
+import Language.Haskell.TH.Syntax (addModFinalizer, runIO)
+import GHC.Types (Type)
+
+type Proxy :: forall a. a -> Type
+data Proxy a = MkProxy
+
+check :: ($(addModFinalizer (runIO (putStrLn "check")) >>
+  [t| Proxy |]) :: Type -> Type) Int -- There is kind signature, we are in check mode
+check = MkProxy
+
+infer :: ($(addModFinalizer (runIO (putStrLn "infer")) >>
+  [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/1eb6c06e63f0faa03d7c7a1f6c9eb5aa97967153

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/1eb6c06e63f0faa03d7c7a1f6c9eb5aa97967153
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/20240313/8040249c/attachment-0001.html>


More information about the ghc-commits mailing list