Zubin pushed to branch wip/27627 at Glasgow Haskell Compiler / GHC Commits: 226d0699 by Zubin Duggal at 2026-08-14T16:33:12+05:30 Make isTerminatingType 3 valued We only introduce a bottom if it is SurelyNotTerminating We only speculate if it is SurelyTerminating - - - - - 17 changed files: - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/Make.hs - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Utils.hs - compiler/GHC/Types/Demand.hs - compiler/GHC/Types/Id/Make.hs - + testsuite/tests/core-to-stg/T27627a/Callee.hs - + testsuite/tests/core-to-stg/T27627a/Caller.hs - + testsuite/tests/core-to-stg/T27627a/Main.hs - + testsuite/tests/core-to-stg/T27627a/T27627a.stdout - + testsuite/tests/core-to-stg/T27627a/all.T - + testsuite/tests/core-to-stg/T27627b/Callee.hs - + testsuite/tests/core-to-stg/T27627b/Caller.hs - + testsuite/tests/core-to-stg/T27627b/Main.hs - + testsuite/tests/core-to-stg/T27627b/T27627b.stdout - + testsuite/tests/core-to-stg/T27627b/all.T Changes: ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -566,8 +566,8 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty -- Check that we have not bound bottom at a type whose values are -- assumed to be non-bottom, such as a dictionary. (See #24934, #25924, #27627). -- A deferred type error is an exception. - -- See (4) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core - ; checkL (not (isTerminatingType binder_ty) + -- See (5) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core + ; checkL (not (mightBeTerminatingType binder_ty) || not (exprIsDeadEnd rhs) || isDeferredTypeError rhs) (mkBottomTerminatingTyMsg binder) @@ -3827,7 +3827,7 @@ isDeferredTypeError :: CoreExpr -> Bool -- ^ True if it contains a call to `typeError` like -fdefer-type-errors and its -- relatives insert, such as -- case typeError @LiftedRep @() "No instance for ..."# of {} --- See (4) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core +-- See (5) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core isDeferredTypeError = go where go (Case scrut _ _ []) = go scrut @@ -3838,7 +3838,7 @@ isDeferredTypeError = go go _ = False mkBottomTerminatingTyMsg :: Id -> SDoc --- See (4) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core +-- See (5) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core mkBottomTerminatingTyMsg binder = vcat [ text "Binder of a terminating type is bound to bottom:" , nest 2 (ppr binder <+> dcolon <+> ppr (idType binder)) ===================================== compiler/GHC/Core/Make.hs ===================================== @@ -227,7 +227,7 @@ mkLitRubbish :: Type -> Maybe CoreExpr -- Fail (returning Nothing) if -- * the RuntimeRep of the Type is not monomorphic; -- * the type is (a ~# b), the type of coercion --- * the type is terminating (isTerminatingType), e.g. a dictionary +-- * the type might be terminating (mightBeTerminatingType), e.g. a dictionary -- See INVARIANT 1, 2 and 3 of item (2) in Note [Rubbish literals] -- in GHC.Types.Literal mkLitRubbish ty @@ -235,7 +235,7 @@ mkLitRubbish ty = Nothing -- Satisfy INVARIANT 1 | isEqPred ty = Nothing -- Satisfy INVARIANT 2 - | isTerminatingType ty + | mightBeTerminatingType ty = Nothing -- Satisfy INVARIANT 3 | otherwise = Just (Lit (LitRubbish torc rep) `mkTyApps` [ty]) ===================================== compiler/GHC/Core/Opt/WorkWrap/Utils.hs ===================================== @@ -1068,11 +1068,11 @@ unbox_one_arg opts arg_var -- same type as @id@. Otherwise, no suitable filler could be found. mkAbsentFiller :: Module -> Id -> StrictnessMark -> Maybe CoreExpr mkAbsentFiller mod arg str - -- We never make a filler for a terminating type: it might be speculatively - -- evaluated or have a field projected out of it. + -- We never make a filler for a type that might be terminating: it might be + -- speculatively evaluated or have a field projected out of it. -- See (AF4) in Note [Absent fillers], and -- Note [Don't make fillers for terminating types]. - | isTerminatingType arg_ty + | mightBeTerminatingType arg_ty = Nothing -- The lifted case: bind 'absentError'. See (AF1) in Note [Absent fillers] ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -132,7 +132,9 @@ module GHC.Core.Type ( mightBeLiftedType, mightBeUnliftedType, definitelyLiftedType, definitelyUnliftedType, isAlgType, isDataFamilyApp, isSatTyFamApp, - isPrimitiveType, isStrictType, isTerminatingType, + isPrimitiveType, isStrictType, + IsTerminating(..), typeTerminating, + definitelyTerminatingType, mightBeTerminatingType, unwrapUnaryClasses, isLevityTy, isLevityVar, isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy, @@ -2458,22 +2460,46 @@ isAlgType ty isStrictType :: HasDebugCallStack => Type -> Bool isStrictType = isUnliftedType -isTerminatingType :: HasDebugCallStack => Type -> Bool --- ^ True <=> a term of this type cannot be bottom --- This identifies the types described by --- Note [NON-BOTTOM-DICTS invariant] in GHC.Core +-- | Returned by 'typeTerminating'. +-- See Note [NON-BOTTOM-DICTS invariant] in GHC.Core +data IsTerminating + = SurelyTerminating -- ^ A term of this type is never bottom + | SurelyNotTerminating -- ^ A term of this type may well be bottom + | MaybeTerminating -- ^ We cannot tell; see (4) in the Note + deriving (Eq, Show) + +instance Outputable IsTerminating where + ppr = text . show + +typeTerminating :: HasDebugCallStack => Type -> IsTerminating +-- ^ Says whether a term of this type can be bottom. +-- See Note [NON-BOTTOM-DICTS invariant] in GHC.Core -- NB: unlifted types are not terminating types! -- e.g. you can write a term (loop 1)::Int# that diverges. -isTerminatingType ty = case tyConAppTyCon_maybe (unwrapUnaryClasses id ty) of - Just tc -> isClassTyCon tc && not (isUnaryClassTyCon tc) - -- We ask about the type that represents the dictionary, not the - -- type we were handed, because a unary class dictionary **is** the - -- field it wraps. A non-unary class TyCon is terminating; a - -- unary one is left here only when there is a cylce, - -- and then the dictionary really can be bottom. - -- See (1) and (3) in Note [NON-BOTTOM-DICTS invariant] in - -- GHC.Core, and (UCM3) in Note [Unary class magic] - _ -> False +typeTerminating ty + | Just tc <- tyConAppTyCon_maybe unwrapped + , isClassTyCon tc + = if isUnaryClassTyCon tc + then SurelyNotTerminating -- Only left here by a cycle; see (3) + else SurelyTerminating + + | ConstraintLike <- typeTypeOrConstraint unwrapped + = MaybeTerminating -- See (4) + + | otherwise + = SurelyNotTerminating + where + unwrapped = dropForAlls (unwrapUnaryClasses dropForAlls ty) + +definitelyTerminatingType :: HasDebugCallStack => Type -> Bool +-- ^ For callers that will evaluate a term of this type. +-- See (2) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core +definitelyTerminatingType ty = typeTerminating ty == SurelyTerminating + +mightBeTerminatingType :: HasDebugCallStack => Type -> Bool +-- ^ For callers that will put a bottoming term at this type. +-- See (2) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core +mightBeTerminatingType ty = typeTerminating ty /= SurelyNotTerminating -- | Look through unary classes, and return the first type -- that is not a unary class. For ===================================== compiler/GHC/Core/Utils.hs ===================================== @@ -2275,7 +2275,7 @@ app_ok fun_ok primop_ok fun args _other -- Unlifted and terminating types; -- Also c.f. the Var case of exprIsHNF - | isTerminatingType fun_ty -- See Note [exprOkForSpeculation and type classes] + | definitelyTerminatingType fun_ty -- See Note [exprOkForSpeculation and type classes] || definitelyUnliftedType fun_ty -> assertPpr (n_val_args == 0) (ppr fun $$ ppr args) True -- Both terminating types (e.g. Eq a), and unlifted types (e.g. Int#) ===================================== compiler/GHC/Types/Demand.hs ===================================== @@ -91,7 +91,7 @@ import GHC.Types.Unique.FM import GHC.Types.Basic import GHC.Data.Maybe ( orElse ) -import GHC.Core.Type ( Type, isTerminatingType ) +import GHC.Core.Type ( Type, definitelyTerminatingType ) import GHC.Core.DataCon ( splitDataProductType_maybe, StrictnessMark, isMarkedStrict ) import GHC.Core.Multiplicity ( scaledThing ) @@ -1064,7 +1064,7 @@ strictifyDmd = plusDmd seqDmd strictifyDictDmd :: Type -> Demand -> Demand strictifyDictDmd ty (n :* Prod b ds) | not (isAbs n) - , isTerminatingType ty + , definitelyTerminatingType ty , Just (_tc, _arg_tys, _data_con, field_tys) <- splitDataProductType_maybe ty = C_1N :* mkProd b (zipWith strictifyDictDmd (map scaledThing field_tys) ds) -- main idea: ensure it's strict ===================================== compiler/GHC/Types/Id/Make.hs ===================================== @@ -498,7 +498,7 @@ mkDictSelId name clas mkFunctionType ManyTy pred_ty res_ty -- See Note [Type classes and linear types] - terminating = isTerminatingType res_ty || definitelyUnliftedType res_ty + terminating = definitelyTerminatingType res_ty || definitelyUnliftedType res_ty -- If the field is unlifted, it can't be bottom -- Ditto if it's a terminating type ===================================== testsuite/tests/core-to-stg/T27627a/Callee.hs ===================================== @@ -0,0 +1,34 @@ +{-# LANGUAGE GADTs, ConstraintKinds, ScopedTypeVariables, TypeFamilies #-} +{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses, FlexibleInstances #-} +{-# OPTIONS_GHC -fno-worker-wrapper #-} +module Callee where + +import Data.Kind (Constraint) + +-- A Constraint-kinded type family. It always reduces to (TC a), but +-- unwrapUnaryClasses does not reduce type families, so it cannot walk +-- through this field. See (4) in Note [NON-BOTTOM-DICTS invariant]. +type family F a :: Constraint +type instance F a = TC a + +-- Not unary: a superclass field and a method field. +class Eq a => TC a where + tcDummy :: a -> Int + +-- Unary: a single superclass field, whose type is the unreduced family +-- application (F a). +class F a => UC a + +instance TC Int where tcDummy _ = 0 +instance UC Int + +data Dict c where + Dict :: c => Dict c + +{-# NOINLINE discard #-} +discard :: Dict c -> Int +discard _ = 42 + +{-# NOINLINE b #-} +b :: forall a. UC a => a -> Int +b _ = discard (Dict :: Dict (Eq a)) ===================================== testsuite/tests/core-to-stg/T27627a/Caller.hs ===================================== @@ -0,0 +1,10 @@ +module Caller where + +import Callee + +-- b does not use its dictionary, so a's dictionary is absent. Worker/wrapper +-- must not replace it with an error thunk: at runtime a (UC t) dictionary is a +-- (TC t) dictionary, and Callee speculates a superclass selection out of it. +{-# NOINLINE a #-} +a :: UC t => t -> Int +a x = b x + 1 ===================================== testsuite/tests/core-to-stg/T27627a/Main.hs ===================================== @@ -0,0 +1,6 @@ +module Main where + +import Caller + +main :: IO () +main = print (a (3 :: Int)) ===================================== testsuite/tests/core-to-stg/T27627a/T27627a.stdout ===================================== @@ -0,0 +1 @@ +43 ===================================== testsuite/tests/core-to-stg/T27627a/all.T ===================================== @@ -0,0 +1,4 @@ +test('T27627a', + [extra_files(['Main.hs', 'Caller.hs', 'Callee.hs'])], + multimod_compile_and_run, + ['Main', '-O']) ===================================== testsuite/tests/core-to-stg/T27627b/Callee.hs ===================================== @@ -0,0 +1,29 @@ +{-# LANGUAGE GADTs, ConstraintKinds, ScopedTypeVariables, QuantifiedConstraints #-} +{-# LANGUAGE UndecidableInstances, FlexibleInstances, RankNTypes #-} +{-# OPTIONS_GHC -fno-worker-wrapper #-} +module Callee where + +-- Not unary: a superclass field and a method field, so (TC a) is terminating. +class Eq a => TC a where + tcDummy :: a -> Int + +-- Unary: one superclass field, of type (forall a. TC (f a)). +-- unwrapUnaryClasses cannot walk through a forall, so it cannot reach the +-- class underneath. See (4) in Note [NON-BOTTOM-DICTS invariant]. +class (forall a. TC (f a)) => UQ f + +newtype Id a = MkId a +instance Eq (Id a) where _ == _ = True +instance TC (Id a) where tcDummy _ = 0 +instance UQ Id + +data Dict c where + Dict :: c => Dict c + +{-# NOINLINE discard #-} +discard :: Dict c -> Int +discard _ = 42 + +{-# NOINLINE b #-} +b :: forall f. UQ f => f Int -> Int +b _ = discard (Dict :: Dict (Eq (f Int))) ===================================== testsuite/tests/core-to-stg/T27627b/Caller.hs ===================================== @@ -0,0 +1,10 @@ +module Caller where + +import Callee + +-- b does not use its dictionary, so a's dictionary is absent. Worker/wrapper +-- must not replace it with an error thunk: Callee speculates a superclass +-- selection out of it. +{-# NOINLINE a #-} +a :: UQ f => f Int -> Int +a x = b x + 1 ===================================== testsuite/tests/core-to-stg/T27627b/Main.hs ===================================== @@ -0,0 +1,7 @@ +module Main where + +import Callee +import Caller + +main :: IO () +main = print (a (MkId 3 :: Id Int)) ===================================== testsuite/tests/core-to-stg/T27627b/T27627b.stdout ===================================== @@ -0,0 +1 @@ +43 ===================================== testsuite/tests/core-to-stg/T27627b/all.T ===================================== @@ -0,0 +1,4 @@ +test('T27627b', + [extra_files(['Main.hs', 'Caller.hs', 'Callee.hs'])], + multimod_compile_and_run, + ['Main', '-O']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/226d0699fd676e8f54163519d35d50df... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/226d0699fd676e8f54163519d35d50df... You're receiving this email because of your account on gitlab.haskell.org. Manage all notifications: https://gitlab.haskell.org/-/profile/notifications | Help: https://gitlab.haskell.org/help