[Git][ghc/ghc][wip/sand-witch/lazy-skol] Almost done

Simon Peyton Jones (@simonpj) gitlab at gitlab.haskell.org
Fri Jan 26 23:21:38 UTC 2024



Simon Peyton Jones pushed to branch wip/sand-witch/lazy-skol at Glasgow Haskell Compiler / GHC


Commits:
ac379222 by Simon Peyton Jones at 2024-01-26T23:21:11+00:00
Almost done

- - - - -


13 changed files:

- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Tc/Errors/Ppr.hs
- compiler/GHC/Tc/Gen/Expr.hs
- compiler/GHC/Tc/Gen/Match.hs
- compiler/GHC/Tc/Gen/Pat.hs
- compiler/GHC/Tc/Types/Origin.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Tc/Utils/Unify.hs
- testsuite/tests/typecheck/should_fail/FD1.stderr
- testsuite/tests/typecheck/should_fail/T2714.stderr
- testsuite/tests/typecheck/should_fail/tcfail001.stderr
- testsuite/tests/typecheck/should_fail/tcfail175.stderr
- testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr


Changes:

=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -809,7 +809,7 @@ tcMkVisFunTy mult arg res
           , ft_arg = arg, ft_res = res }
 
 tcMkInvisFunTy :: TypeOrConstraint -> Type -> Type -> Type
--- Always TypeLike, invisible argument
+-- Always invisible (constraint) argument, result specified by res_torc
 -- Does not have the assert-checking in mkFunTy: used by the typechecker
 -- to avoid looking at the result kind, which may not be zonked
 tcMkInvisFunTy res_torc arg res


=====================================
compiler/GHC/Tc/Errors/Ppr.hs
=====================================
@@ -4991,9 +4991,9 @@ tidySigSkol env cx ty tv_prs
       where
         (env', tv') = tidy_tv_bndr env tv
 
-    tidy_ty env ty@(FunTy af w arg res) -- Look under  c => t
-      | isInvisibleFunArg af
-      = ty { ft_mult = tidy_ty env w
+    tidy_ty env ty@(FunTy { ft_mult = w, ft_arg = arg, ft_res = res })
+      = -- Look under  c => t and t1 -> t2
+        ty { ft_mult = tidy_ty env w
            , ft_arg  = tidyType env arg
            , ft_res  = tidy_ty env res }
 


=====================================
compiler/GHC/Tc/Gen/Expr.hs
=====================================
@@ -192,8 +192,7 @@ tcPolyExprCheck expr res_ty
                     -> ([ExpPatType] -> TcRhoType -> TcM (HsExpr GhcTc))
                     -> TcM (HsExpr GhcTc)
     outer_skolemise (Left ty) thing_inside
-      = do { (wrap, expr') <- tcSkolemiseGeneral Shallow GenSigCtxt ty $ \tv_prs rho_ty ->
-                              thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty
+      = do { (wrap, expr') <- tcSkolemiseExpectedType ty thing_inside
            ; return (mkHsWrap wrap expr') }
     outer_skolemise (Right sig) thing_inside
       = do { (wrap, expr') <- tcSkolemiseCompleteSig sig thing_inside


=====================================
compiler/GHC/Tc/Gen/Match.hs
=====================================
@@ -277,10 +277,12 @@ tcMatch ctxt pat_tys rhs_ty match
              match@(Match { m_pats = pats, m_grhss = grhss })
       = add_match_ctxt match $
         do { (pats', (wrapper, grhss')) <- tcMatchPats (mc_what ctxt) pats pat_tys $
-                                tcGRHSs ctxt grhss rhs_ty
+                                           tcGRHSs ctxt grhss rhs_ty
+             -- NB: pats' are just the /value/ patterns
+             -- See Note [tcMatchPats] in GHC.Tc.Gen.Pat
            ; return (wrapper, Match { m_ext = noAnn
                                     , m_ctxt = mc_what ctxt
-                                    , m_pats = filter_out_type_pats pats'
+                                    , m_pats = pats'
                                     , m_grhss = grhss' }) }
 
         -- For (\x -> e), tcExpr has already said "In the expression \x->e"
@@ -292,13 +294,6 @@ tcMatch ctxt pat_tys rhs_ty match
             LamAlt LamSingle -> thing_inside
             _                -> addErrCtxt (pprMatchInCtxt match) thing_inside
 
-    -- We filter out type patterns because we have no use for them in HsToCore.
-    -- Type variable bindings have already been converted to HsWrappers.
-    filter_out_type_pats :: [LPat GhcTc] -> [LPat GhcTc]
-    filter_out_type_pats = filterByList (map isExpFunPatType vis_pat_tys)
-      where
-        vis_pat_tys = filter isVisibleExpPatType pat_tys
-
 -------------
 tcGRHSs :: AnnoBody body
         => TcMatchCtxt body -> GRHSs GhcRn (LocatedA (body GhcRn)) -> ExpRhoType
@@ -1219,4 +1214,5 @@ checkArgCounts matchContext (MG { mg_alts = L _ (match1:matches) })
 
     reqd_args_in_match :: LocatedA (Match GhcRn body1) -> Arity
     -- Counts the number of /required/ args in the match
+    -- IMPORTANT: THIS WILL NEED TO CHANGE WHEN @ty BECOMES A PATTERN
     reqd_args_in_match (L _ (Match { m_pats = pats })) = length pats


=====================================
compiler/GHC/Tc/Gen/Pat.hs
=====================================
@@ -128,24 +128,16 @@ tcMatchPats :: forall a.
             -> [ExpPatType]             -- ^ types of the patterns
             -> TcM a                    -- ^ checker for the body
             -> TcM ([LPat GhcTc], a)
-
--- This is the externally-callable wrapper function for
---   function definitions  f p1 .. pn = rhs
---   lambdas               \p1 .. pn -> body
--- Typecheck the patterns, extend the environment to bind the variables,
--- do the thing inside, use any existentially-bound dictionaries to
--- discharge parts of the returning LIE, and deal with pattern type
--- signatures
-
+-- See Note [tcMatchPats]
+--
 -- PRECONDITION:
---    number of visible Pats in pats (@a is invisible)
---         =
---    number of visible ExpPatTypes in pat_tys (ExpForAllPatTy v is visible iff b is Required)
-
---   1. Initialise the PatState
---   2. Check the patterns
---   3. Check the body
---   4. Check that no existentials escape
+--    number of visible Pats in pats
+--      (@a is invisible)
+--  = number of visible ExpPatTypes in pat_tys
+--      (ExpForAllPatTy v is visible iff b is Required)
+--
+-- POSTCONDITION:
+--   Returns only the /value/ patterns; see Note [tcMatchPats]
 
 tcMatchPats match_ctxt pats pat_tys thing_inside
   = assertPpr (count isVisibleExpPatType pat_tys == length pats)
@@ -155,7 +147,7 @@ tcMatchPats match_ctxt pats pat_tys thing_inside
     do { err_ctxt <- getErrCtxt
        ; let loop :: [LPat GhcRn] -> [ExpPatType] -> TcM ([LPat GhcTc], a)
 
-             -- No more patterns; discard excess type patterns;
+             -- No more patterns.  Discard excess pat_tys;
              -- they should all be invisible.  Example:
              --    f :: Int -> forall a b. blah
              --    f x @p = rhs
@@ -178,8 +170,9 @@ tcMatchPats match_ctxt pats pat_tys thing_inside
              loop (pat : pats) (ExpForAllPatTy bndr : pat_tys)
                | Bndr tv vis <- bndr
                , isVisibleForAllTyFlag vis
-               = do { (p, (ps, res)) <- tc_forall_lpat tv penv pat $
+               = do { (_p, (ps, res)) <- tc_forall_lpat tv penv pat $
                                         loop pats pat_tys
+
                     ; return (ps, res) }
 
                -- Invisible forall in type, and an @a type pattern
@@ -228,7 +221,26 @@ tcCheckPat_O ctxt orig pat (Scaled pat_mult pat_ty) thing_inside
     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = orig }
 
 
-{-
+{- Note [tcMatchPats]
+~~~~~~~~~~~~~~~~~~~~~
+tcMatchPats is the externally-callable wrapper function for
+  function definitions  f p1 .. pn = rhs
+  lambdas               \p1 .. pn -> body
+Typecheck the patterns, extend the environment to bind the variables, do the
+thing inside, use any existentially-bound dictionaries to discharge parts of
+the returning LIE, and deal with pattern type signatures
+
+It takes the list of patterns writen by the user, but it returns only the
+/value/ patterns.  For example:
+     f :: forall a. forall b -> a -> Mabye b -> blah
+     f @a w x (Just y) = ....
+tcMatchPats returns only the /value/ patterns [x, Just y].  Why?  The
+desugarer expects only value patterns.  (We could change that, but we would
+have to do so carefullly.)  However, distinguishing value patterns from type
+patterns is a bit tiricky; e.g. the `w` in this example.  So it's very
+convenient to filter them out right here.
+
+
 ************************************************************************
 *                                                                      *
                 PatEnv, PatCtxt, LetBndrSpec


=====================================
compiler/GHC/Tc/Types/Origin.hs
=====================================
@@ -440,7 +440,7 @@ in the right place.  So we proceed as follows:
   whatever it tidies to, say a''; and then we walk over the type
   replacing the binder a by the tidied version a'', to give
        forall a''. Eq a'' => forall b''. b'' -> a''
-  We need to do this under (=>) arrows, to match what topSkolemise
+  We need to do this under (=>) arrows and (->), to match what skolemisation
   does.
 
 * Typically a'' will have a nice pretty name like "a", but the point is


=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -81,7 +81,7 @@ module GHC.Tc.Utils.TcType (
   ---------------------------------
   -- Predicates.
   -- Again, newtypes are opaque
-  isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy, isDeepRhoTy,
+  isSigmaTy, isRhoTy, isRhoExpTy, isOverloadedTy,
   isFloatingPrimTy, isDoubleTy, isFloatTy, isIntTy, isWordTy, isStringTy,
   isIntegerTy, isNaturalTy,
   isBoolTy, isUnitTy, isCharTy,
@@ -1908,18 +1908,6 @@ isRhoTy (FunTy { ft_af = af })       = isVisibleFunArg af
 isRhoTy ty | Just ty' <- coreView ty = isRhoTy ty'
 isRhoTy _                            = True
 
-isDeepRhoTy :: TcType -> Bool
--- Same as isRhoTy but for DeepSubsumption
--- Are there any invisible binders, possibly underneath visible ones
-isDeepRhoTy (ForAllTy (Bndr _ af) body)
-  | isVisibleForAllTyFlag af = isDeepRhoTy body
-  | otherwise                = False
-isDeepRhoTy (FunTy { ft_af = af, ft_res = res })
-  | isVisibleFunArg af = isDeepRhoTy res
-  | otherwise          = False
-isDeepRhoTy ty | Just ty' <- coreView ty = isRhoTy ty'
-isDeepRhoTy _                            = True
-
 -- | Like 'isRhoTy', but also says 'True' for 'Infer' types
 isRhoExpTy :: ExpType -> Bool
 isRhoExpTy (Check ty) = isRhoTy ty


=====================================
compiler/GHC/Tc/Utils/Unify.hs
=====================================
@@ -20,7 +20,7 @@ module GHC.Tc.Utils.Unify (
 
   -- Skolemisation
   DeepSubsumptionFlag(..), getDeepSubsumptionFlag,
-  tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseGeneral,
+  tcSkolemise, tcSkolemiseCompleteSig, tcSkolemiseExpectedType,
 
   -- Various unifications
   unifyType, unifyKind, unifyInvisibleType, unifyExpectedType,
@@ -318,11 +318,10 @@ Both ultimately handled by matchExpectedFunTys.
   The outer skolemisation in tcPolyExprCheck is done using
     * tcSkolemiseCompleteSig when there is a user-written signature
     * tcSkolemiseGeneral when the polytpe just comes from the context e.g. (f e)
-  The two cases differ only slightly:
+  The former just calls the latter, so the two cases differ only slightly:
     * Both do shallow skolemisation
-    * Both always call checkConstraints, even if there are no skolem
-      variables at all.  Reason: there might be nested deferred errors
-      that must not be allowed to float to top level.
+    * Both go via tcSkolemiseGeneral, which uses implicationNeeded to decide whether
+      to build an implication constraint even if there /are/ no skolems.
       See Note [When to build an implication] below.
 
   The difference between the two cases is that `tcSkolemiseCompleteSig`
@@ -388,10 +387,14 @@ Some examples:
 tcSkolemiseGeneral
   :: DeepSubsumptionFlag
   -> UserTypeCtxt
-  -> TcType
+  -> TcType -> TcType   -- top_ty and expected_ty
+        -- * top_ty is the type we started to skolemise; it is used only in SigSkol
+        -- * expected_ty is the type we are actually  skolemising
+        -- matchExpectedFunTys walks down the type, skolemising as it goes,
+        -- keeping the same top_ty, but successively smaller expected_tys
   -> ([(Name, TcInvisTVBinder)] -> TcType -> TcM result)
   -> TcM (HsWrapper, result)
-tcSkolemiseGeneral ds_flag ctxt expected_ty thing_inside
+tcSkolemiseGeneral ds_flag ctxt top_ty expected_ty thing_inside
   = do { implication_needed <- implicationNeeded ds_flag ctxt expected_ty
        ; if not implication_needed
               -- Fast path.  We check every function argument with tcCheckPolyExpr,
@@ -407,7 +410,7 @@ tcSkolemiseGeneral ds_flag ctxt expected_ty thing_inside
        ; rec { (wrap, tv_prs, given, rho_ty) <- case ds_flag of
                     Deep    -> deeplySkolemise skol_info expected_ty
                     Shallow -> topSkolemise skol_info expected_ty
-             ; skol_info <- mkSkolemInfo (SigSkol ctxt expected_ty (map (fmap binderVar) tv_prs)) }
+             ; skol_info <- mkSkolemInfo (SigSkol ctxt top_ty (map (fmap binderVar) tv_prs)) }
 
        ; let skol_tvs = map (binderVar . snd) tv_prs
        ; (ev_binds, result) <- checkConstraints (getSkolemInfo skol_info) skol_tvs given $
@@ -427,17 +430,30 @@ tcSkolemiseCompleteSig :: TcCompleteSig
 tcSkolemiseCompleteSig (CSig { sig_bndr = poly_id, sig_ctxt = ctxt, sig_loc = loc })
                        thing_inside
   = do { cur_loc <- getSrcSpanM
+       ; let poly_ty = idType poly_id
        ; setSrcSpan loc $   -- Sets the location for the implication constraint
-         tcSkolemiseGeneral Shallow ctxt (idType poly_id) $ \tv_prs rho_ty ->
+         tcSkolemiseGeneral Shallow ctxt poly_ty poly_ty $ \tv_prs rho_ty ->
          setSrcSpan cur_loc $ -- Revert to the original location
          tcExtendNameTyVarEnv (map (fmap binderVar) tv_prs) $
          thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty }
 
+tcSkolemiseExpectedType :: TcSigmaType
+                        -> ([ExpPatType] -> TcRhoType -> TcM result)
+                        -> TcM (HsWrapper, result)
+-- Just ike tcSkolemiseCompleteSig, except that don't have a user-written
+-- type signature, we only have a type comimg from the context.
+-- Eg. f :: (forall a. blah) -> blah
+--     In the call (f e) we will call tcSkolemiseExpectedType on (forall a.blah)
+--     before typececking `e`
+tcSkolemiseExpectedType exp_ty thing_inside
+  = tcSkolemiseGeneral Shallow GenSigCtxt exp_ty exp_ty $ \tv_prs rho_ty ->
+    thing_inside (map (mkInvisExpPatType . snd) tv_prs) rho_ty
+
 tcSkolemise :: DeepSubsumptionFlag -> UserTypeCtxt -> TcSigmaType
             -> (TcRhoType -> TcM result)
             -> TcM (HsWrapper, result)
 tcSkolemise ds_flag ctxt expected_ty thing_inside
-  = tcSkolemiseGeneral ds_flag ctxt expected_ty $ \_ rho_ty ->
+  = tcSkolemiseGeneral ds_flag ctxt expected_ty expected_ty $ \_ rho_ty ->
     thing_inside rho_ty
 
 checkConstraints :: SkolemInfoAnon
@@ -502,9 +518,7 @@ buildTvImplication skol_info skol_tvs tclvl wanted
 implicationNeeded :: DeepSubsumptionFlag -> UserTypeCtxt -> TcType -> TcM Bool
 -- See Note [When to build an implication]
 implicationNeeded ds_flag ctxt expected_ty
-  | case ds_flag of          -- Check for no invisible quantifiers
-       Shallow -> isRhoTy expected_ty
-       Deep    -> isDeepRhoTy expected_ty
+  | definitely_mono ds_flag expected_ty   -- Check for no invisible quantifiers
   , not (alwaysBuildImplication ctxt)
   = -- Empty skolems and givens
     -- Build an implication if any of the "defer" flags is on
@@ -738,8 +752,8 @@ matchExpectedFunTys herald _ arity (Infer inf_res) thing_inside
        ; co <- fillInferResult (mkScaledFunTys arg_tys res_ty) inf_res
        ; return (mkWpCastN co, result) }
 
-matchExpectedFunTys herald ctx arity (Check ty) thing_inside
-  = check 0 [] ty
+matchExpectedFunTys herald ctx arity (Check top_ty) thing_inside
+  = check 0 [] top_ty
   where
     check :: Arity -> [ExpPatType] -> TcSigmaType -> TcM (HsWrapper, a)
     -- `check` is called only in the Check{} case
@@ -751,7 +765,7 @@ matchExpectedFunTys herald ctx arity (Check ty) thing_inside
     check n_so_far rev_pat_tys ty
       | isSigmaTy ty  -- Type has invisible quantifiers
       = do { (wrap_gen, (wrap_res, result))
-                 <- tcSkolemiseGeneral Shallow ctx ty $ \tv_bndrs ty' ->
+                 <- tcSkolemiseGeneral Shallow ctx top_ty ty $ \tv_bndrs ty' ->
                     let rev_pat_tys' = reverse (map (mkInvisExpPatType . snd) tv_bndrs)
                                        ++ rev_pat_tys
                     in check n_so_far rev_pat_tys' ty'
@@ -767,7 +781,7 @@ matchExpectedFunTys herald ctx arity (Check ty) thing_inside
            ; case ds_flag of
                Shallow -> do { res <- thing_inside pat_tys (mkCheckExpType rho_ty)
                              ; return (idHsWrapper, res) }
-               Deep    -> tcSkolemiseGeneral Deep ctx rho_ty $ \_ rho_ty ->
+               Deep    -> tcSkolemiseGeneral Deep ctx top_ty rho_ty $ \_ rho_ty ->
                           -- "_" drop the /deeply/-skolemise binders
                           -- They do not line up with binders in the Match
                           thing_inside pat_tys (mkCheckExpType rho_ty) }
@@ -784,11 +798,15 @@ matchExpectedFunTys herald ctx arity (Check ty) thing_inside
     -- See Note [Visible type application and abstraction] in GHC.Tc.Gen.App
     check n_so_far rev_pat_tys ty
       | Just (Bndr tv vis, body_ty) <- splitForAllForAllTyBinder_maybe ty
-      , Required <- vis
-      = do { let init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
+      = assertPpr (isVisibleForAllTyFlag vis) (ppr ty) $
+        -- isSigmaTy case above has dealt with /invisible/ quantifiers,
+        -- so this one must be /visible/ (= Required)
+        do { let init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
+             -- rec {..}: see Note [Keeping SkolemInfo inside a SkolemTv]
+             --           in GHC.Tc.Utils.TcType
            ; rec { (subst', [tv']) <- tcInstSkolTyVarsX skol_info init_subst [tv]
                  ; let tv_prs = [(tyVarName tv, tv')]
-                 ; skol_info <- mkSkolemInfo (SigSkol ctx ty tv_prs) }
+                 ; skol_info <- mkSkolemInfo (SigSkol ctx top_ty tv_prs) }
            ; let body_ty' = substTy subst' body_ty
                  pat_ty   = ExpForAllPatTy (mkForAllTyBinder Required tv')
            ; (ev_binds, (wrap_res, result)) <- checkConstraints (getSkolemInfo skol_info) [tv'] [] $
@@ -1437,14 +1455,10 @@ tc_sub_type_ds ds_flag unify inst_orig ctxt ty_actual ty_expected
 
 ----------------------
 definitely_mono :: DeepSubsumptionFlag -> TcType -> Bool
-definitely_mono Shallow ty
-  = isRhoTy ty    -- isRhoTy: no top level forall or (=>)
-definitely_mono Deep ty
-  = go ty
-  where  -- Look deeply for foralls
-    go ty | not (isRhoTy ty)                       = False
-          | Just (_, res) <- tcSplitFunTy_maybe ty = go res
-          | otherwise                              = True
+definitely_mono ds_flag ty
+  = case ds_flag of
+      Shallow -> isRhoTy ty      -- isRhoTy: no top level forall or (=>)
+      Deep    -> isDeepRhoTy ty  -- "deep" version: no nested forall or (=>)
 
 definitely_poly :: TcType -> Bool
 -- A very conservative test:
@@ -1748,7 +1762,7 @@ deeplySkolemise skol_info ty
     init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
 
     go subst ty
-      | Just (arg_tys, bndrs, theta, ty') <- tcDeepSplitSigmaTyBndr_maybe ty
+      | Just (arg_tys, bndrs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
       = do { let arg_tys' = substScaledTys subst arg_tys
            ; ids1             <- newSysLocalIds (fsLit "dk") arg_tys'
            ; (subst', bndrs1) <- tcInstSkolTyVarBndrsX skol_info subst bndrs
@@ -1775,8 +1789,9 @@ deeplyInstantiate orig ty
     init_subst = mkEmptySubst (mkInScopeSet (tyCoVarsOfType ty))
 
     go subst ty
-      | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
-      = do { (subst', tvs') <- newMetaTyVarsX subst tvs
+      | Just (arg_tys, bndrs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
+      = do { let tvs = binderVars bndrs
+           ; (subst', tvs') <- newMetaTyVarsX subst tvs
            ; let arg_tys' = substScaledTys   subst' arg_tys
                  theta'   = substTheta subst' theta
            ; ids1  <- newSysLocalIds (fsLit "di") arg_tys'
@@ -1789,32 +1804,34 @@ deeplyInstantiate orig ty
       = do { let ty' = substTy subst ty
            ; return (idHsWrapper, ty') }
 
-
-
-tcDeepSplit_maybe :: (Type -> ([a], ThetaType, Type)) -> TcSigmaType -> Maybe ([Scaled TcType], [a], ThetaType, TcSigmaType)
--- Looks for a *non-trivial* quantified type, under zero or more function arrows
--- By "non-trivial" we mean either tyvars or constraints are non-empty
-
-tcDeepSplit_maybe splitter = go where
-  go ty
-    | Just (arg_ty, res_ty)           <- tcSplitFunTy_maybe ty
-    , Just (arg_tys, tvs, theta, rho) <- go res_ty
-    = Just (arg_ty:arg_tys, tvs, theta, rho)
-
-    | (tvs, theta, rho) <- splitter ty
-    , not (null tvs && null theta)
-    = Just ([], tvs, theta, rho)
-
-    | otherwise = Nothing
-
 tcDeepSplitSigmaTy_maybe
-  :: TcSigmaType -> Maybe ([Scaled TcType], [TyVar], ThetaType, TcSigmaType)
-tcDeepSplitSigmaTy_maybe = tcDeepSplit_maybe tcSplitSigmaTy
-
-tcDeepSplitSigmaTyBndr_maybe
   :: TcSigmaType -> Maybe ([Scaled TcType], [TcInvisTVBinder], ThetaType, TcSigmaType)
-tcDeepSplitSigmaTyBndr_maybe = tcDeepSplit_maybe tcSplitSigmaTyBndrs
-
+-- Looks for a *non-trivial* quantified type, under zero or more function arrows
+-- By "non-trivial" we mean either tyvars or constraints are non-empty
+tcDeepSplitSigmaTy_maybe ty
+  = go ty
+  where
+  go ty | Just (arg_ty, res_ty)           <- tcSplitFunTy_maybe ty
+        , Just (arg_tys, tvs, theta, rho) <- go res_ty
+        = Just (arg_ty:arg_tys, tvs, theta, rho)
+
+        | (tvs, theta, rho) <- tcSplitSigmaTyBndrs ty
+        , not (null tvs && null theta)
+        = Just ([], tvs, theta, rho)
+
+        | otherwise = Nothing
+
+isDeepRhoTy :: TcType -> Bool
+-- True if there are no foralls or (=>) at the top, or nested under
+-- arrows to the right.  e.g
+--    forall a. a                  False
+--    Int -> forall a. a           False
+--    (forall a. a) -> Int         True
+-- Returns True iff tcDeepSplitSigmaTy_maybe returns Nothing
+isDeepRhoTy ty
+  | not (isRhoTy ty)                       = False  -- Foralls or (=>) at top
+  | Just (_, res) <- tcSplitFunTy_maybe ty = isDeepRhoTy res
+  | otherwise                              = True   -- No forall, (=>), or (->) at top
 
 {-
 ************************************************************************


=====================================
testsuite/tests/typecheck/should_fail/FD1.stderr
=====================================
@@ -7,3 +7,4 @@ FD1.hs:16:1: error: [GHC-25897]
         at FD1.hs:15:1-38
     • The equation for ‘plus’ has two value arguments,
         but its type ‘Int -> a’ has only one
+    • Relevant bindings include plus :: Int -> a (bound at FD1.hs:16:1)


=====================================
testsuite/tests/typecheck/should_fail/T2714.stderr
=====================================
@@ -5,10 +5,10 @@ T2714.hs:8:7: error: [GHC-25897]
         Actual: f0 (a -> b) -> f0 b
       ‘c’ is a rigid type variable bound by
         the type signature for:
-          f :: forall c. c -> a
+          f :: ((a -> b) -> b) -> forall c. c -> a
         at T2714.hs:8:1-13
     • In the expression: ffmap x
       In an equation for ‘f’: f x = ffmap x
     • Relevant bindings include
         x :: (a -> b) -> b (bound at T2714.hs:8:3)
-        f :: ((a -> b) -> b) -> c -> a (bound at T2714.hs:8:1)
+        f :: ((a -> b) -> b) -> forall c. c -> a (bound at T2714.hs:8:1)


=====================================
testsuite/tests/typecheck/should_fail/tcfail001.stderr
=====================================
@@ -5,3 +5,4 @@ tcfail001.hs:9:2: error: [GHC-83865]
     • The equation for ‘op’ has one value argument,
         but its type ‘[a]’ has none
       In the instance declaration for ‘A [a]’
+    • Relevant bindings include op :: [a] (bound at tcfail001.hs:9:2)


=====================================
testsuite/tests/typecheck/should_fail/tcfail175.stderr
=====================================
@@ -8,3 +8,5 @@ tcfail175.hs:11:1: error: [GHC-25897]
         at tcfail175.hs:10:1-19
     • The equation for ‘evalRHS’ has three value arguments,
         but its type ‘Int -> a’ has only one
+    • Relevant bindings include
+        evalRHS :: Int -> a (bound at tcfail175.hs:11:1)


=====================================
testsuite/tests/vdq-rta/should_fail/T22326_fail_n_args.stderr
=====================================
@@ -3,7 +3,7 @@ T22326_fail_n_args.hs:6:1: error: [GHC-25897]
     • Couldn't match expected type ‘b’ with actual type ‘t0 -> t1’
       ‘b’ is a rigid type variable bound by
         the type signature for:
-          f :: forall b -> b
+          f :: a -> forall b -> b
         at T22326_fail_n_args.hs:6:1-26
     • The equation for ‘f’ has three value arguments,
         but its type ‘a -> forall b -> b’ has only two



View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ac3792224030e7a08357f5fad7621b1af7459411

-- 
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ac3792224030e7a08357f5fad7621b1af7459411
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/20240126/55d83a49/attachment-0001.html>


More information about the ghc-commits mailing list