[Git][ghc/ghc][wip/27627] Make isTerminatingType look through unary classes
Zubin pushed to branch wip/27627 at Glasgow Haskell Compiler / GHC Commits: 5d8c2279 by Zubin Duggal at 2026-08-14T14:17:42+05:30 Make isTerminatingType look through unary classes A unary class is represented by its field, so it can be bottom precisely when its field can be bottom. Also add a core lint check to ensure there are no bindings whose type is `isTerminatingType` but their rhs is bottom Fixes #27627 - - - - - 14 changed files: - + changelog.d/27627 - compiler/GHC/Core.hs - compiler/GHC/Core/DataCon.hs-boot - compiler/GHC/Core/Lint.hs - compiler/GHC/Core/Opt/WorkWrap/Utils.hs - compiler/GHC/Core/TyCon.hs - compiler/GHC/Core/Type.hs - compiler/GHC/Core/Utils.hs - compiler/GHC/Types/RepType.hs - + testsuite/tests/core-to-stg/T27627/Callee.hs - + testsuite/tests/core-to-stg/T27627/Caller.hs - + testsuite/tests/core-to-stg/T27627/Main.hs - + testsuite/tests/core-to-stg/T27627/T27627.stdout - + testsuite/tests/core-to-stg/T27627/all.T Changes: ===================================== changelog.d/27627 ===================================== @@ -0,0 +1,5 @@ +section: compiler +synopsis: Fix a bug where an absent dictionary argument of a unary class could + be replaced by an error thunk, which GHC then evaluated, crashing the program. +mrs: !16519 +issues: #27627 ===================================== compiler/GHC/Core.hs ===================================== @@ -644,21 +644,20 @@ parts of the compilation pipeline. Note [NON-BOTTOM-DICTS invariant] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -It is a global invariant (not checkable by Lint) that +It is a global invariant that - every non-newtype dictionary-typed expression is non-bottom. + a dictionary-typed expression is never bottom, -These conditions are captured by GHC.Core.Type.isTerminatingType. +The exception is unary classes; see (1) below. +GHC.Core.Type.isTerminatingType says which types the invariant covers. -How are we so sure about this? Dictionaries are built by GHC in only two ways: +How are we so sure about this? GHC builds a dictionary in only two ways: * A dictionary function (DFun), arising from an instance declaration. DFuns do no computation: they always return a data constructor immediately. See DFunUnfolding in GHC.Core. So the result of a call to a DFun is always non-bottom. - Exception: newtype dictionaries. - Plus: see the Very Nasty Wrinkle in Note [Speculative evaluation] in GHC.CoreToStg.Prep @@ -666,20 +665,89 @@ How are we so sure about this? Dictionaries are built by GHC in only two ways: see Note [Recursive superclasses] and Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance. -A bad Core-to-Core pass could invalidate this reasoning, but that's too bad. -It's still an invariant of Core programs generated by GHC from Haskell, and -Core-to-Core passes maintain it. +(1) Unary classes + +The dictionary of a unary class is not a data constructor application at all: +it *is* its single field. See Note [Unary class magic] in GHC.Core.TyCon. +So for + + class Eq a => C1 a where { op :: a -> a } -- Two fields: not unary + class Eq a => C2 a -- One field: unary + class D a where { meth :: a -> a } -- One field: unary + +a (C1 a) dictionary is a data constructor application, so it cannot be bottom. +A (C2 a) dictionary is precisely the (Eq a) dictionary it wraps, which cannot +be bottom either. But a (D a) dictionary is precisely the function `meth`, and +the programmer can write + + instance D Int where meth = undefined + +so it can perfectly well bottom. + +`isTerminatingType` therefore looks through unary classes, one field at a time, +until it reaches a type that is not a unary class: + + isTerminatingType (C1 a) = True -- Stops at once: C1 is not unary + isTerminatingType (C2 a) = True -- Looks through C2, reaches (Eq a) + isTerminatingType (D a) = False -- Looks through D, reaches (a -> a) + +(2) Two kinds of callers, pulling in opposite directions + +Some code __relies__ on a dictionary being non-bottom, and evaluates one eagerly +on the basis of that: + + * -fdicts-strict makes dictionary arguments strict. + See GHC.Types.Demand.strictifyDictDmd + + * exprOkForSpeculation says that (eq_sel d) terminates, so that + case (eq_sel d) of _ -> blah + can be discarded (exprOkToDiscard), or evaluated ahead of time. See + Note [exprOkForSpeculation and type classes] in GHC.Core.Utils and + Note [Speculative evaluation] in GHC.CoreToStg.Prep + +Other code would otherwise __create__ a bottom value at a dictionary type, and +it must not: + + * Worker/wrapper replaces an absent argument with an error thunk or a + rubbish literal. See Note [Don't make fillers for terminating types] + in GHC.Core.Opt.WorkWrap.Utils + +isTerminatingType is the condition used by both, so we the latter +kind of caller doesn't put bottoms in places where the former kind of +caller requires them to be absent. + +The result of `isTerminatingType` depnds only on the type at the end of the +chain of fields, so `isTerminatingType` returns the same thing for a unary class +and its field: if it says False for (C2 a) then it also says False for (Eq a). +#27627 is an example of how we got it wrong before. `isTerminatingType` used +to stop at the unary class C2 rather than look through it, so worker/wrapper +made an error thunk for a (C2 a) dictionary, while exprOkForSpeculation +evaluated that very same value as a (Eq a) dictionary. + +(3) Cyclic superclasses + +With UndecidableSuperClasses the chain of fields can loop back on itself: + + class D2 a => D1 a + class D1 a => D2 a + +`isTerminatingType` returns false as soon as it detects a cycle + +(4) Keeping the invariant true + +We can check the invariant in core lint: `lintLetBind` rejects a binding +whose type is terminating and whose right hand side is bottom. It checks +bindings only, which is where the absent-filler machinery of worker/wrapper and +Specialise puts such values. -Why is it useful to know that dictionaries are non-bottom? +However, there is a complication. With -fdefer-type-errors (and +-fdefer-typed-holes, and friends) GHC binds a dictionary it could not solve to +`typeError`, which is bottom: -1. It justifies the use of `-XDictsStrict`; - see `GHC.Core.Types.Demand.strictifyDictDmd` + $dEq :: Eq T + $dEq = case typeError "No instance for (Eq T) ..."# of {} -2. It means that (eq_sel d) is ok-for-speculation and thus - case (eq_sel d) of _ -> blah - can be discarded by the Simplifier. See these Notes: - Note [exprOkForSpeculation and type classes] in GHC.Core.Utils - Note[Speculative evaluation] in GHC.CoreToStg.Prep +`GHC.Core.Lint.isDeferredTypeError` handles this. Note [Case expression invariants] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ===================================== compiler/GHC/Core/DataCon.hs-boot ===================================== @@ -22,6 +22,7 @@ dataConUserTyVars :: DataCon -> [TyVar] dataConUserTyVarBinders :: DataCon -> [TyVarBinder] dataConSourceArity :: DataCon -> Arity dataConFieldLabels :: DataCon -> [FieldLabel] +dataConInstArgTys :: DataCon -> [Type] -> [Scaled Type] dataConInstOrigArgTys :: DataCon -> [Type] -> [Scaled Type] dataConStupidTheta :: DataCon -> ThetaType dataConFullSig :: DataCon ===================================== compiler/GHC/Core/Lint.hs ===================================== @@ -563,6 +563,15 @@ lintLetBind top_lvl rec_flag binder rhs rhs_ty || exprIsTickedString rhs) (mkTopNonLitStrMsg binder) + -- 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) + || not (exprIsDeadEnd rhs) + || isDeferredTypeError rhs) + (mkBottomTerminatingTyMsg binder) + ; flags <- getLintFlags -- Check that a join-point binder has a valid type @@ -3814,6 +3823,28 @@ mkTopNonLitStrMsg :: Id -> SDoc mkTopNonLitStrMsg binder = hsep [text "Top-level Addr# binder has a non-literal rhs:", ppr binder] +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 +isDeferredTypeError = go + where + go (Case scrut _ _ []) = go scrut + go (App fun _) = go fun + go (Cast expr _) = go expr + go (Tick _ expr) = go expr + go (Var v) = v `hasKey` typeErrorIdKey + go _ = False + +mkBottomTerminatingTyMsg :: Id -> SDoc +-- See (4) 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)) + , text "A value of this type is assumed never to be bottom," + , text "so GHC may evaluate this binding without being asked to." ] + mkKindErrMsg :: TyVar -> Type -> SDoc mkKindErrMsg tyvar arg_ty = vcat [text "Kinds don't match in type application:", ===================================== compiler/GHC/Core/Opt/WorkWrap/Utils.hs ===================================== @@ -1326,8 +1326,8 @@ fragile Note [Don't make fillers for terminating types] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ We never make an absent filler, error thunk or rubbish literal, for a terminating -type (isTerminatingType): a non-unary class dictionary, a boxed equality, or a -constraint tuple. +type (isTerminatingType): a non-unary class dictionary, a unary class dictionary +that wraps a non-unary class dictionary, a boxed equality, or a constraint tuple. GHC relies on a dictionary value never being bottom (see Note [NON-BOTTOM-DICTS invariant] in GHC.Core). GHC uses "speculation" to @@ -1338,6 +1338,7 @@ rise to a succession of bugs including: * #24934: we evaluated an absent dictionary * #25924: we selected a superclass from an absent dictionary + * #27627: we selected a superclass from an absent dictionary of a unary class A terminating type is exactly what speculation will force: see Note [exprOkForSpeculation and type classes] in GHC.Core.Utils. So we refuse to ===================================== compiler/GHC/Core/TyCon.hs ===================================== @@ -1503,8 +1503,15 @@ There are a number of wrinkles Rather, it has its own AlgTyConRhs, namely `UnaryClassTyCon` (UCM3) Unlike non-unary classes, a value of type (C ty), where `C` is a unary - class, might be bottom, because it is represented by the method type alone. - See GHC.Core.Type.isTerminatingType. + class, might be bottom, because it is represented by its single field alone. + It is bottom exactly when a value of that field's type can be bottom, so + GHC.Core.Type.isTerminatingType looks through unary classes to decide. For + + class Eq a => C2 a -- Field: an (Eq a) dictionary + class D a where { meth :: a -> a } -- Field: a function + + a (C2 a) dictionary cannot be bottom but a (D a) dictionary can. + See Note [NON-BOTTOM-DICTS invariant] in GHC.Core. Similarly in exprOkForSpeculation/exprOkToDiscard/exprOkForSpecEval, in GHC.Core.Utils. In the utility funcion `app_ok` we need a special ===================================== compiler/GHC/Core/Type.hs ===================================== @@ -133,6 +133,7 @@ module GHC.Core.Type ( definitelyLiftedType, definitelyUnliftedType, isAlgType, isDataFamilyApp, isSatTyFamApp, isPrimitiveType, isStrictType, isTerminatingType, + unwrapUnaryClasses, isLevityTy, isLevityVar, isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy, dropRuntimeRepArgs, @@ -235,8 +236,11 @@ import GHC.Types.Var.Env import GHC.Types.Var.Set import GHC.Core.TyCon +import GHC.Core.TyCon.Set( TyConSet, emptyTyConSet, elemTyConSet, extendTyConSet ) import GHC.Builtin.Types.Prim +import {-# SOURCE #-} GHC.Core.DataCon( dataConInstArgTys ) + import {-# SOURCE #-} GHC.Builtin.Types ( charTy, naturalTy , typeSymbolKind, liftedTypeKind, unliftedTypeKind @@ -2460,12 +2464,50 @@ isTerminatingType :: HasDebugCallStack => Type -> Bool -- 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 ty of +isTerminatingType ty = case tyConAppTyCon_maybe (unwrapUnaryClasses id ty) of Just tc -> isClassTyCon tc && not (isUnaryClassTyCon tc) - -- A non-unary class TyCon is terminating - -- See (UCM3) in Note [Unary class magic] in GHC.Core.TyCon + -- 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 +-- | Look through unary classes, and return the first type +-- that is not a unary class. For +-- +-- class Eq a => C2 a -- Unary +-- class D a where { meth :: a -> a } -- Unary +-- class Eq a => C1 a where { op :: a -> a } -- Not unary +-- +-- this returns (Eq a) for (C2 a), (a -> a) for (D a), and (C1 a) unchanged. +-- +-- With UndecidableSuperClasses we can have a cycle: +-- +-- class D2 a => D1 a +-- class D1 a => D2 a +-- +-- so we stop and return when we detect a cycle. +-- See Note [Unary class magic] in GHC.Core.TyCon +unwrapUnaryClasses :: (Type -> Type) -- ^ Normalise a type before each step. + -- Pass 'id' to leave it alone, or + -- 'GHC.Types.RepType.unwrapType' to see + -- through newtypes, casts and foralls + -> Type -> Type +unwrapUnaryClasses norm = go emptyTyConSet + where + go :: TyConSet -> Type -> Type + go seen ty + | Just (tc, tys) <- splitTyConApp_maybe (norm ty) + , Just (_cls, dict_con) <- isUnaryClassTyCon_maybe tc + , [fld_ty] <- map scaledThing (dataConInstArgTys dict_con tys) + , not (tc `elemTyConSet` seen) + = go (seen `extendTyConSet` tc) fld_ty + | otherwise + = ty + isPrimitiveType :: Type -> Bool -- ^ Returns true of types that are opaque to Haskell. isPrimitiveType ty = case splitTyConApp_maybe ty of ===================================== compiler/GHC/Core/Utils.hs ===================================== @@ -2383,8 +2383,10 @@ a) That the function is a class-op, with IdDetails of ClassOpId b) That the result type of the class-op is terminating or unlifted. E.g. for class C a => D a where ... class C a where { op :: a -> a } - Since C is represented by a newtype, (sc_sel (d :: D a)) might - not be terminating. + C is a unary class whose one field is the method `op`, so a (C a) dictionary + **is** that function and can be bottom. Hence + (sc_sel (d :: D a)) might not be terminating. + See (1) in Note [NON-BOTTOM-DICTS invariant] in GHC.Core. Rather than repeatedly test if the result of the class-op is a terminating/unlifted type, we cache it as a field of ClassOpId. See ===================================== compiler/GHC/Types/RepType.hs ===================================== @@ -32,7 +32,6 @@ import GHC.Types.Basic (Arity, RepArity) import GHC.Core.DataCon import GHC.Core.Coercion import GHC.Core.TyCon -import GHC.Core.TyCon.Set import GHC.Core.TyCon.RecWalk import GHC.Core.TyCo.Rep import GHC.Core.Type @@ -734,26 +733,13 @@ mightBeFunTy ty -- definitely not a function type. | definitelyUnliftedType ty = False - | Just tc <- tyConAppTyCon_maybe (unwrap_type ty) + -- Use 'unwrapType' to look through casts, newtypes and foralls, and + -- 'unwrapUnaryClasses' to look through unary classes (which are transparent + -- as per Note [Unary class magic] in GHC.Core.TyCon). We don't try to + -- reduce type family applications, as we don't have a FamInstEnv to hand. + | Just tc <- tyConAppTyCon_maybe (unwrapUnaryClasses unwrapType ty) -- A proper datatype (such as 'Int' or 'Maybe Bool') is definitely not -- a function type. (This does not include newtypes nor type families.) = not $ isBoxedDataTyCon tc | otherwise = True - - where - -- Use 'unwrapType' to look through casts, newtypes and foralls. - -- Separately, look through unary classes (supposed to be transparent as per - -- Note [Unary class magic] in GHC.Core.TyCon). We don't try to reduce type - -- family applications, as we don't have a FamInstEnv to hand. - unwrap_type = go emptyTyConSet - where - go seen_tcs ty - | Just (tc, tys) <- splitTyConApp_maybe (unwrapType ty) - , Just (_cls, unary_dc) <- isUnaryClassTyCon_maybe tc - , [inst_meth_ty] <- map scaledThing (dataConInstArgTys unary_dc tys) - = if tc `elemTyConSet` seen_tcs - then ty -- cycle detected: bail out - else go (seen_tcs `extendTyConSet` tc) inst_meth_ty - | otherwise - = ty ===================================== testsuite/tests/core-to-stg/T27627/Callee.hs ===================================== @@ -0,0 +1,34 @@ +{-# LANGUAGE GADTs, ConstraintKinds, ScopedTypeVariables #-} +{-# OPTIONS_GHC -fno-worker-wrapper #-} +module Callee where + +-- TC is not unary: it has a superclass field and a method field. So $p1TC is +-- an ordinary selector, ($p1TC d) is not a trivial expression, and CorePrep +-- gives it a binding of its own. +class Eq a => TC a where + tcDummy :: a -> Int + +-- UC is unary: a single superclass field. Its dictionary is precisely the +-- (TC a) dictionary it wraps, so it cannot be bottom either. +class TC a => UC a where {} + +instance TC Int where tcDummy _ = 0 +instance UC Int + +data Dict c where + Dict :: c => Dict c + +-- Ignores its argument, so the Dict below is absent-demanded, and hence so is +-- the UC dictionary that Dict carries. +{-# NOINLINE discard #-} +discard :: Dict c -> Int +discard _ = 42 + +-- The Core of the body is +-- discard (Dict @(Eq a) ($p1TC ($p1UC d))) +-- The constructor application is a value, so CorePrep floats the selection +-- out of the argument and evaluates it at the head of b. -fno-worker-wrapper +-- keeps the dictionary parameter, so the caller has to pass one. +{-# NOINLINE b #-} +b :: forall a. UC a => a -> Int +b _ = discard (Dict :: Dict (Eq a)) ===================================== testsuite/tests/core-to-stg/T27627/Caller.hs ===================================== @@ -0,0 +1,11 @@ +module Caller where + +import Callee + +-- b does not use its dictionary, so a's dictionary is absent. Worker/wrapper +-- used to drop it and pass an error thunk to b in its place, which b then +-- evaluated. Now isTerminatingType looks through the unary class UC, sees the +-- (TC a) dictionary underneath, and refuses to make a filler. +{-# NOINLINE a #-} +a :: UC t => t -> Int +a x = b x + 1 ===================================== testsuite/tests/core-to-stg/T27627/Main.hs ===================================== @@ -0,0 +1,4 @@ +module Main where +import Caller +main :: IO () +main = print (a (1 :: Int)) ===================================== testsuite/tests/core-to-stg/T27627/T27627.stdout ===================================== @@ -0,0 +1 @@ +43 ===================================== testsuite/tests/core-to-stg/T27627/all.T ===================================== @@ -0,0 +1,4 @@ +test('T27627', + [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/5d8c22799b5de5296a12df78cb02b191... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/5d8c22799b5de5296a12df78cb02b191... 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
participants (1)
-
Zubin (@wz1000)