Improve exprOkForSpeculation for classopswip/T22745

This patch fixes #22745 and #15205, which are about GHC's
failure to discard unnecessary superclass selections that
yield coercions.  See
  GHC.Core.Utils Note [exprOkForSpeculation and type classes]

The main changes are:

* Write new Note [NON-BOTTOM_DICTS invariant] in GHC.Core, and
  refer to it

* Define new function isTerminatingType, to identify those
  guaranteed-terminating dictionary types.

* exprOkForSpeculation has a new (very simple) case for ClassOpId

* ClassOpId has a new field that says if the return type is
  an unlifted type, or a terminating type.

This was surprisingly tricky to get right.  In particular note
that unlifted types are not terminating types; you can write an
expression of unlifted type, that diverges.  Not so for dictionaries
(or, more precisely, for the dictionaries that GHC constructs).

Metric Decrease:
    LargeRecord

21 files changed, 228 insertions, 80 deletions

diff --git a/compiler/GHC/Core.hs b/compiler/GHC/Core.hs
index b18ec7acda..809332d395 100644
--- a/compiler/GHC/Core.hs
+++ b/compiler/GHC/Core.hs
@@ -292,7 +292,7 @@ data AltCon
 -- This instance is a bit shady. It can only be used to compare AltCons for
 -- a single type constructor. Fortunately, it seems quite unlikely that we'll
 -- ever need to compare AltCons for different type constructors.
--- The instance adheres to the order described in [Core case invariants]
+-- The instance adheres to the order described in Note [Case expression invariants]
 instance Ord AltCon where
   compare (DataAlt con1) (DataAlt con2) =
     assert (dataConTyCon con1 == dataConTyCon con2) $
@@ -466,6 +466,45 @@ we need to allow lots of things in the arguments of a call.
 
 TL;DR: we relaxed the let/app invariant to become the let-can-float invariant.
 
+Note [NON-BOTTOM-DICTS invariant]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is a global invariant (not checkable by Lint) that
+
+     every non-newtype dictionary-typed expression is non-bottom.
+
+These conditions are captured by GHC.Core.Type.isTerminatingType.
+
+How are we so sure about this?  Dictionaries are built by GHC 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
+
+* A superclass selection from some other dictionary. This is harder to guarantee:
+  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.
+
+Why is it useful to know that dictionaries are non-bottom?
+
+1. It justifies the use of `-XDictsStrict`;
+   see `GHC.Core.Types.Demand.strictifyDictDmd`
+
+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
+
 Note [Case expression invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Case expressions are one of the more complicated elements of the Core
@@ -556,10 +595,6 @@ substitutions until the next run of the simplifier.
   Note [Equality superclasses in quantified constraints]
   in GHC.Tc.Solver.Canonical
 
-Note [Core case invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See Note [Case expression invariants]
-
 Note [Representation polymorphism invariants]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 GHC allows us to abstract over calling conventions using **representation polymorphism**.
@@ -627,12 +662,6 @@ representation: we check whether bound variables and function arguments have a
 See Note [Representation polymorphism checking] in GHC.Tc.Utils.Concrete
 for an overview of how we enforce these invariants in the typechecker.
 
-Note [Core let goal]
-~~~~~~~~~~~~~~~~~~~~
-* The simplifier tries to ensure that if the RHS of a let is a constructor
-  application, its arguments are trivial, so that the constructor can be
-  inlined vigorously.
-
 Note [Empty case alternatives]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The alternatives of a case expression should be exhaustive.  But
diff --git a/compiler/GHC/Core/Opt/DmdAnal.hs b/compiler/GHC/Core/Opt/DmdAnal.hs
index fbe843cff8..0bcabf55d3 100644
--- a/compiler/GHC/Core/Opt/DmdAnal.hs
+++ b/compiler/GHC/Core/Opt/DmdAnal.hs
@@ -395,7 +395,7 @@ dmdAnalBindLetDown top_lvl env dmd bind anal_body = case bind of
 anticipateANF :: CoreExpr -> Card -> Card
 anticipateANF e n
   | exprIsTrivial e                               = n -- trivial expr won't have a binding
-  | Just Unlifted <- typeLevity_maybe (exprType e)
+  | definitelyUnliftedType (exprType e)
   , not (isAbs n && exprOkForSpeculation e)       = case_bind n
   | otherwise                                     = let_bind  n
   where
diff --git a/compiler/GHC/Core/Opt/FloatIn.hs b/compiler/GHC/Core/Opt/FloatIn.hs
index 2feef8a617..b35e655a87 100644
--- a/compiler/GHC/Core/Opt/FloatIn.hs
+++ b/compiler/GHC/Core/Opt/FloatIn.hs
@@ -28,7 +28,7 @@ import GHC.Core.Utils
 import GHC.Core.FVs
 import GHC.Core.Type
 
-import GHC.Types.Basic      ( RecFlag(..), isRec, Levity(Unlifted) )
+import GHC.Types.Basic      ( RecFlag(..), isRec )
 import GHC.Types.Id         ( idType, isJoinId, isJoinId_maybe )
 import GHC.Types.Tickish
 import GHC.Types.Var
@@ -618,7 +618,7 @@ noFloatIntoRhs is_rec bndr rhs
   | isJoinId bndr
   = isRec is_rec -- Joins are one-shot iff non-recursive
 
-  | Just Unlifted <- typeLevity_maybe (idType bndr)
+  | definitelyUnliftedType (idType bndr)
   = True  -- Preserve let-can-float invariant, see Note [noFloatInto considerations]
 
   | otherwise
diff --git a/compiler/GHC/Core/Opt/Simplify/Utils.hs b/compiler/GHC/Core/Opt/Simplify/Utils.hs
index dfca4bc0ce..39263455c0 100644
--- a/compiler/GHC/Core/Opt/Simplify/Utils.hs
+++ b/compiler/GHC/Core/Opt/Simplify/Utils.hs
@@ -685,7 +685,7 @@ mkArgInfo env rule_base fun cont
       | Just (_, _, arg_ty, fun_ty') <- splitFunTy_maybe fun_ty        -- Add strict-type info
       , dmd : rest_dmds <- dmds
       , let dmd'
-             | Just Unlifted <- typeLevity_maybe arg_ty
+             | definitelyUnliftedType arg_ty
              = strictifyDmd dmd
              | otherwise
              -- Something that's not definitely unlifted.
diff --git a/compiler/GHC/Core/Predicate.hs b/compiler/GHC/Core/Predicate.hs
index 9751724d56..c8d280259a 100644
--- a/compiler/GHC/Core/Predicate.hs
+++ b/compiler/GHC/Core/Predicate.hs
@@ -224,11 +224,12 @@ isEqPredClass :: Class -> Bool
 isEqPredClass cls =  cls `hasKey` eqTyConKey
                   || cls `hasKey` heqTyConKey
 
-isClassPred, isEqPred, isEqPrimPred :: PredType -> Bool
+isClassPred :: PredType -> Bool
 isClassPred ty = case tyConAppTyCon_maybe ty of
-    Just tyCon | isClassTyCon tyCon -> True
-    _                               -> False
+    Just tc -> isClassTyCon tc
+    _       -> False
 
+isEqPred :: PredType -> Bool
 isEqPred ty  -- True of (a ~ b) and (a ~~ b)
              -- ToDo: should we check saturation?
   | Just tc <- tyConAppTyCon_maybe ty
@@ -237,6 +238,7 @@ isEqPred ty  -- True of (a ~ b) and (a ~~ b)
   | otherwise
   = False
 
+isEqPrimPred :: PredType -> Bool
 isEqPrimPred ty = isCoVarType ty
   -- True of (a ~# b) (a ~R# b)
 
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 9e0d95b0d9..8bab8462be 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -132,8 +132,9 @@ module GHC.Core.Type (
         isUnliftedType, isBoxedType, isUnboxedTupleType, isUnboxedSumType,
         kindBoxedRepLevity_maybe,
         mightBeLiftedType, mightBeUnliftedType,
+        definitelyLiftedType, definitelyUnliftedType,
         isAlgType, isDataFamilyAppType,
-        isPrimitiveType, isStrictType,
+        isPrimitiveType, isStrictType, isTerminatingType,
         isLevityTy, isLevityVar,
         isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
         dropRuntimeRepArgs,
@@ -2198,18 +2199,6 @@ isFamFreeTy (ForAllTy _ ty)   = isFamFreeTy ty
 isFamFreeTy (CastTy ty _)     = isFamFreeTy ty
 isFamFreeTy (CoercionTy _)    = False  -- Not sure about this
 
--- | Does this type classify a core (unlifted) Coercion?
--- At either role nominal or representational
---    (t1 ~# t2) or (t1 ~R# t2)
--- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep"
-isCoVarType :: Type -> Bool
-  -- ToDo: should we check saturation?
-isCoVarType ty
-  | Just tc <- tyConAppTyCon_maybe ty
-  = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
-  | otherwise
-  = False
-
 buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind   -- ^ /result/ kind
               -> [Role] -> KnotTied Type -> TyCon
 -- This function is here because here is where we have
@@ -2256,8 +2245,7 @@ isUnliftedType ty =
   case typeLevity_maybe ty of
     Just Lifted   -> False
     Just Unlifted -> True
-    Nothing       ->
-      pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty))
+    Nothing       -> pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty))
 
 -- | Returns:
 --
@@ -2267,6 +2255,9 @@ isUnliftedType ty =
 mightBeLiftedType :: Type -> Bool
 mightBeLiftedType = mightBeLifted . typeLevity_maybe
 
+definitelyLiftedType :: Type -> Bool
+definitelyLiftedType = not . mightBeUnliftedType
+
 -- | Returns:
 --
 -- * 'False' if the type is /guaranteed/ lifted or
@@ -2275,6 +2266,9 @@ mightBeLiftedType = mightBeLifted . typeLevity_maybe
 mightBeUnliftedType :: Type -> Bool
 mightBeUnliftedType = mightBeUnlifted . typeLevity_maybe
 
+definitelyUnliftedType :: Type -> Bool
+definitelyUnliftedType = not . mightBeLiftedType
+
 -- | See "Type#type_classification" for what a boxed type is.
 -- Panics on representation-polymorphic types; See 'mightBeUnliftedType' for
 -- a more approximate predicate that behaves better in the presence of
@@ -2371,6 +2365,28 @@ isDataFamilyAppType ty = case tyConAppTyCon_maybe ty of
 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
+-- 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
+    Just tc -> isClassTyCon tc && not (isNewTyCon tc)
+    _       -> False
+
+-- | Does this type classify a core (unlifted) Coercion?
+-- At either role nominal or representational
+--    (t1 ~# t2) or (t1 ~R# t2)
+-- See Note [Types for coercions, predicates, and evidence] in "GHC.Core.TyCo.Rep"
+isCoVarType :: Type -> Bool
+  -- ToDo: should we check saturation?
+isCoVarType ty
+  | Just tc <- tyConAppTyCon_maybe ty
+  = tc `hasKey` eqPrimTyConKey || tc `hasKey` eqReprPrimTyConKey
+  | otherwise
+  = False
+
 isPrimitiveType :: Type -> Bool
 -- ^ Returns true of types that are opaque to Haskell.
 isPrimitiveType ty = case splitTyConApp_maybe ty of
diff --git a/compiler/GHC/Core/Unfold.hs b/compiler/GHC/Core/Unfold.hs
index 48a7e5e82f..3663e50bf1 100644
--- a/compiler/GHC/Core/Unfold.hs
+++ b/compiler/GHC/Core/Unfold.hs
@@ -593,7 +593,7 @@ sizeExpr opts !bOMB_OUT_SIZE top_args expr
            FCallId _        -> sizeN (callSize (length val_args) voids)
            DataConWorkId dc -> conSize    dc (length val_args)
            PrimOpId op _    -> primOpSize op (length val_args)
-           ClassOpId _      -> classOpSize opts top_args val_args
+           ClassOpId {}     -> classOpSize opts top_args val_args
            _                -> funSize opts top_args fun (length val_args) voids
 
     ------------
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index a0d3bc9c44..35023c6576 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -91,8 +91,7 @@ import GHC.Types.Literal
 import GHC.Types.Tickish
 import GHC.Types.Id
 import GHC.Types.Id.Info
-import GHC.Types.Basic( Arity, Levity(..)
-                       )
+import GHC.Types.Basic( Arity )
 import GHC.Types.Unique
 import GHC.Types.Unique.Set
 import GHC.Types.Demand
@@ -1574,6 +1573,13 @@ app_ok fun_ok primop_ok fun args
                 -- been expressed by its "wrapper", so we don't need
                 -- to take the arguments into account
 
+      ClassOpId _ is_terminating_result
+        | is_terminating_result -- See Note [exprOkForSpeculation and type classes]
+        -> assertPpr (n_val_args == 1) (ppr fun $$ ppr args) $
+           True
+           -- assert: terminating result type => can't be applied;
+           -- c.f the _other case below
+
       PrimOpId op _
         | primOpIsDiv op
         , [arg1, Lit lit] <- args
@@ -1596,14 +1602,16 @@ app_ok fun_ok primop_ok fun args
         -> primop_ok op  -- Check the primop itself
         && and (zipWith arg_ok arg_tys args)  -- Check the arguments
 
-      _  -- Unlifted types
-         -- c.f. the Var case of exprIsHNF
-         | Just Unlifted <- typeLevity_maybe (idType fun)
+      _other  -- Unlifted and terminating types;
+              -- Also c.f. the Var case of exprIsHNF
+         |  isTerminatingType fun_ty  -- See Note [exprOkForSpeculation and type classes]
+         || definitelyUnliftedType fun_ty
          -> assertPpr (n_val_args == 0) (ppr fun $$ ppr args)
-            True  -- Our only unlifted types are Int# etc, so will have
-                  -- no value args.  The assert is just to check this.
-                  -- If we added unlifted function types this would change,
-                  -- and we'd need to actually test n_val_args == 0.
+            True  -- Both terminating types (e.g. Eq a), and unlifted types (e.g. Int#)
+                  -- are non-functions and so will have no value args.  The assert is
+                  -- just to check this.
+                  -- (If we added unlifted function types this would change,
+                  -- and we'd need to actually test n_val_args == 0.)
 
          -- Partial applications
          | idArity fun > n_val_args ->
@@ -1618,14 +1626,15 @@ app_ok fun_ok primop_ok fun args
              --     for evaluated-ness of the fun;
              --     see Note [exprOkForSpeculation and evaluated variables]
   where
+    fun_ty       = idType fun
     n_val_args   = valArgCount args
-    (arg_tys, _) = splitPiTys (idType fun)
+    (arg_tys, _) = splitPiTys fun_ty
 
     -- Used for arguments to primops and to partial applications
     arg_ok :: PiTyVarBinder -> CoreExpr -> Bool
     arg_ok (Named _) _ = True   -- A type argument
     arg_ok (Anon ty _) arg      -- A term argument
-       | Just Lifted <- typeLevity_maybe (scaledThing ty)
+       | definitelyLiftedType (scaledThing ty)
        = True -- See Note [Primops with lifted arguments]
        | otherwise
        = expr_ok fun_ok primop_ok arg
@@ -1655,8 +1664,36 @@ etaExpansionTick id t
   = hasNoBinding id &&
     ( tickishFloatable t || isProfTick t )
 
-{- Note [exprOkForSpeculation: case expressions]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [exprOkForSpeculation and type classes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider (#22745, #15205)
+
+  \(d :: C a b). case eq_sel (sc_sel d) of
+                   (co :: t1 ~# t2) [Dead] ->  blah
+
+We know that
+* eq_sel's argument (sc_sel d) has dictionary type, so it definitely terminates
+  (again Note [NON-BOTTOM-DICTS invariant] in GHC.Core)
+* eq_sel is simply a superclass selector, and hence is fast
+* The field that eq_sel picks is of unlifted type, and hence can't be bottom
+  (remember the dictionary argument itself is non-bottom)
+
+So we can treat (eq_sel (sc_sel d)) as ok-for-speculation.  We must check
+
+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.
+
+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
+GHC.Types.Id.Make.mkDictSelId for where this field is initialised.
+
+Note [exprOkForSpeculation: case expressions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 exprOkForSpeculation accepts very special case expressions.
 Reason: (a ==# b) is ok-for-speculation, but the litEq rules
 in GHC.Core.Opt.ConstantFold convert it (a ==# 3#) to
@@ -1881,7 +1918,8 @@ exprIsHNFlike is_con is_con_unf = is_hnf_like
         -- We don't look through loop breakers here, which is a bit conservative
         -- but otherwise I worry that if an Id's unfolding is just itself,
         -- we could get an infinite loop
-      || ( typeLevity_maybe (idType v) == Just Unlifted )
+
+      || definitelyUnliftedType (idType v)
         -- Unlifted binders are always evaluated (#20140)
 
     is_hnf_like (Lit l)          = not (isLitRubbish l)
diff --git a/compiler/GHC/CoreToStg/Prep.hs b/compiler/GHC/CoreToStg/Prep.hs
index 78ce8e16f1..c0b72cefed 100644
--- a/compiler/GHC/CoreToStg/Prep.hs
+++ b/compiler/GHC/CoreToStg/Prep.hs
@@ -1648,12 +1648,16 @@ long as the callee might evaluate it. And if it is evaluated on
 most code paths anyway, we get to turn the unknown eval in the
 callee into a known call at the call site.
 
-However, we must be very careful not to speculate recursive calls!
-Doing so might well change termination behavior.
+Very Nasty Wrinkle
+
+We must be very careful not to speculate recursive calls!  Doing so
+might well change termination behavior.
 
 That comes up in practice for DFuns, which are considered ok-for-spec,
 because they always immediately return a constructor.
-Not so if you speculate the recursive call, as #20836 shows:
+See Note [NON-BOTTOM-DICTS invariant] in GHC.Core.
+
+But not so if you speculate the recursive call, as #20836 shows:
 
   class Foo m => Foo m where
     runFoo :: m a -> m a
diff --git a/compiler/GHC/HsToCore/Pmc/Solver.hs b/compiler/GHC/HsToCore/Pmc/Solver.hs
index 07176b87cc..cfc98273e3 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver.hs
@@ -46,7 +46,6 @@ import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 import GHC.Data.Bag
 
-import GHC.Types.Basic (Levity(..))
 import GHC.Types.CompleteMatch
 import GHC.Types.Unique.Set
 import GHC.Types.Unique.DSet
@@ -675,7 +674,7 @@ addPhiTmCt nabla (PhiNotBotCt x)           = addNotBotCt nabla x
 filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
 filterUnliftedFields con args =
   [ arg | (arg, bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con)
-        , isBanged bang || typeLevity_maybe (idType arg) == Just Unlifted ]
+        , isBanged bang || definitelyUnliftedType (idType arg) ]
 
 -- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@
 -- surely diverges. Quite similar to 'addConCt', only that it only cares about
@@ -687,7 +686,7 @@ addBotCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x = do
     IsNotBot -> mzero      -- There was x ≁ ⊥. Contradiction!
     IsBot    -> pure nabla -- There already is x ~ ⊥. Nothing left to do
     MaybeBot               -- We add x ~ ⊥
-      | Just Unlifted <- typeLevity_maybe (idType x)
+      | definitelyUnliftedType (idType x)
       -- Case (3) in Note [Strict fields and variables of unlifted type]
       -> mzero -- unlifted vars can never be ⊥
       | otherwise
diff --git a/compiler/GHC/Stg/InferTags/Rewrite.hs b/compiler/GHC/Stg/InferTags/Rewrite.hs
index 171de2da91..fac784d5fc 100644
--- a/compiler/GHC/Stg/InferTags/Rewrite.hs
+++ b/compiler/GHC/Stg/InferTags/Rewrite.hs
@@ -22,8 +22,7 @@ import GHC.Prelude
 
 import GHC.Builtin.PrimOps ( PrimOp(..) )
 import GHC.Types.Basic     ( CbvMark (..), isMarkedCbv
-                           , TopLevelFlag(..), isTopLevel
-                           , Levity(..) )
+                           , TopLevelFlag(..), isTopLevel )
 import GHC.Types.Id
 import GHC.Types.Name
 import GHC.Types.Unique.Supply
@@ -257,7 +256,7 @@ isTagged v = do
                                     (TagSig TagDunno)
     case nameIsLocalOrFrom this_mod (idName v) of
         True
-            | Just Unlifted <- typeLevity_maybe (idType v)
+            | definitelyUnliftedType (idType v)
               -- NB: v might be the Id of a representation-polymorphic join point,
               -- so we shouldn't use isUnliftedType here. See T22212.
             -> return True
diff --git a/compiler/GHC/StgToJS/Expr.hs b/compiler/GHC/StgToJS/Expr.hs
index fd6d09585f..b398cdf501 100644
--- a/compiler/GHC/StgToJS/Expr.hs
+++ b/compiler/GHC/StgToJS/Expr.hs
@@ -51,7 +51,6 @@ import GHC.StgToJS.Utils
 import GHC.StgToJS.Stack
 import GHC.StgToJS.Ids
 
-import GHC.Types.Basic
 import GHC.Types.CostCentre
 import GHC.Types.Tickish
 import GHC.Types.Var.Set
@@ -484,7 +483,7 @@ genStaticRefs lv
   | otherwise         = do
       unfloated <- State.gets gsUnfloated
       let xs = filter (\x -> not (elemUFM x unfloated ||
-                                  typeLevity_maybe (idType x) == Just Unlifted))
+                                  definitelyUnliftedType (idType x)))
                       (dVarSetElems sv)
       CIStaticRefs . catMaybes <$> mapM getStaticRef xs
   where
diff --git a/compiler/GHC/Tc/Gen/Splice.hs b/compiler/GHC/Tc/Gen/Splice.hs
index e1a91ad495..c12ab7a1aa 100644
--- a/compiler/GHC/Tc/Gen/Splice.hs
+++ b/compiler/GHC/Tc/Gen/Splice.hs
@@ -2057,7 +2057,7 @@ reifyThing (AGlobal (AnId id))
   = do  { ty <- reifyType (idType id)
         ; let v = reifyName id
         ; case idDetails id of
-            ClassOpId cls -> return (TH.ClassOpI v ty (reifyName cls))
+            ClassOpId cls _ -> return (TH.ClassOpI v ty (reifyName cls))
             RecSelId{sel_tycon=RecSelData tc}
                           -> return (TH.VarI (reifySelector id tc) ty Nothing)
             _             -> return (TH.VarI     v ty Nothing)
diff --git a/compiler/GHC/Types/Demand.hs b/compiler/GHC/Types/Demand.hs
index 9890b55dee..09b08b7f36 100644
--- a/compiler/GHC/Types/Demand.hs
+++ b/compiler/GHC/Types/Demand.hs
@@ -92,8 +92,7 @@ import GHC.Types.Unique.FM
 import GHC.Types.Basic
 import GHC.Data.Maybe   ( orElse )
 
-import GHC.Core.Type    ( Type )
-import GHC.Core.TyCon   ( isNewTyCon, isClassTyCon )
+import GHC.Core.Type    ( Type, isTerminatingType )
 import GHC.Core.DataCon ( splitDataProductType_maybe, StrictnessMark, isMarkedStrict )
 import GHC.Core.Multiplicity    ( scaledThing )
 
@@ -988,7 +987,10 @@ oneifyDmd (n :* sd) = oneifyCard n :* sd
 strictifyDmd :: Demand -> Demand
 strictifyDmd = plusDmd seqDmd
 
--- | If the argument is a used non-newtype dictionary, give it strict demand.
+-- | If the argument is a guaranteed-terminating type
+--   (i.e. a non-newtype dictionary) give it strict demand.
+--   This is sound because terminating types can't be bottom:
+--         See GHC.Core Note [NON-BOTTOM-DICTS invariant]
 -- Also split the product type & demand and recur in order to similarly
 -- strictify the argument's contained used non-newtype superclass dictionaries.
 -- We use the demand as our recursive measure to guarantee termination.
@@ -1002,11 +1004,9 @@ strictifyDictDmd ty (n :* Prod b ds)
     -- Return a TyCon and a list of field types if the given
     -- type is a non-newtype dictionary type
     as_non_newtype_dict ty
-      | Just (tycon, _arg_tys, _data_con, map scaledThing -> inst_con_arg_tys)
-          <- splitDataProductType_maybe ty
-      , not (isNewTyCon tycon)
-      , isClassTyCon tycon
-      = Just inst_con_arg_tys
+      | isTerminatingType ty
+      , Just (_tc, _arg_tys, _data_con, field_tys) <- splitDataProductType_maybe ty
+      = Just (map scaledThing field_tys)
       | otherwise
       = Nothing
 strictifyDictDmd _  dmd = dmd
diff --git a/compiler/GHC/Types/Id.hs b/compiler/GHC/Types/Id.hs
index 5131307a00..cdcb89ef3e 100644
--- a/compiler/GHC/Types/Id.hs
+++ b/compiler/GHC/Types/Id.hs
@@ -491,12 +491,12 @@ isNaughtyRecordSelector id = case Var.idDetails id of
                         _                               -> False
 
 isClassOpId id = case Var.idDetails id of
-                        ClassOpId _   -> True
-                        _other        -> False
+                        ClassOpId {} -> True
+                        _other       -> False
 
 isClassOpId_maybe id = case Var.idDetails id of
-                        ClassOpId cls -> Just cls
-                        _other        -> Nothing
+                        ClassOpId cls _ -> Just cls
+                        _other          -> Nothing
 
 isPrimOpId id = case Var.idDetails id of
                         PrimOpId {} -> True
diff --git a/compiler/GHC/Types/Id/Info.hs b/compiler/GHC/Types/Id/Info.hs
index ea7636bea4..2b6785117d 100644
--- a/compiler/GHC/Types/Id/Info.hs
+++ b/compiler/GHC/Types/Id/Info.hs
@@ -150,8 +150,13 @@ data IdDetails
                                 --  a) to support isImplicitId
                                 --  b) when desugaring a RecordCon we can get
                                 --     from the Id back to the data con]
-  | ClassOpId Class             -- ^ The 'Id' is a superclass selector,
-                                -- or class operation of a class
+
+  | ClassOpId                   -- ^ The 'Id' is a superclass selector or class operation
+      Class                     --    for this class
+      Bool                      --   True <=> given a non-bottom dictionary, the class op will
+                                --            definitely return a non-bottom result
+                                --   and Note [exprOkForSpeculation and type classes]
+                                --       in GHC.Core.Utils
 
   | PrimOpId PrimOp Bool        -- ^ The 'Id' is for a primitive operator
                                 -- True <=> is representation-polymorphic,
diff --git a/compiler/GHC/Types/Id/Make.hs b/compiler/GHC/Types/Id/Make.hs
index 4baa335db1..fec1b6c2be 100644
--- a/compiler/GHC/Types/Id/Make.hs
+++ b/compiler/GHC/Types/Id/Make.hs
@@ -465,7 +465,7 @@ mkDictSelId :: Name          -- Name of one of the *value* selectors
                              -- (dictionary superclass or method)
             -> Class -> Id
 mkDictSelId name clas
-  = mkGlobalId (ClassOpId clas) name sel_ty info
+  = mkGlobalId (ClassOpId clas terminating) name sel_ty info
   where
     tycon          = classTyCon clas
     sel_names      = map idName (classAllSelIds clas)
@@ -476,10 +476,15 @@ mkDictSelId name clas
     arg_tys        = dataConRepArgTys data_con  -- Includes the dictionary superclasses
     val_index      = assoc "MkId.mkDictSelId" (sel_names `zip` [0..]) name
 
-    sel_ty = mkInvisForAllTys tyvars $
-             mkFunctionType ManyTy (mkClassPred clas (mkTyVarTys (binderVars tyvars))) $
-             scaledThing (getNth arg_tys val_index)
-               -- See Note [Type classes and linear types]
+    pred_ty = mkClassPred clas (mkTyVarTys (binderVars tyvars))
+    res_ty  = scaledThing (getNth arg_tys val_index)
+    sel_ty  = mkInvisForAllTys tyvars $
+              mkFunctionType ManyTy pred_ty res_ty
+             -- See Note [Type classes and linear types]
+
+    terminating = isTerminatingType res_ty || definitelyUnliftedType res_ty
+                  -- If the field is unlifted, it can't be bottom
+                  -- Ditto if it's a terminating type
 
     base_info = noCafIdInfo
                 `setArityInfo`  1
diff --git a/compiler/GHC/Types/TyThing.hs b/compiler/GHC/Types/TyThing.hs
index 08d13b1257..ab400204d5 100644
--- a/compiler/GHC/Types/TyThing.hs
+++ b/compiler/GHC/Types/TyThing.hs
@@ -257,7 +257,7 @@ tyThingParent_maybe (AnId id)     = case idDetails id of
                                           Just (ATyCon tc)
                                       RecSelId { sel_tycon = RecSelPatSyn ps } ->
                                           Just (AConLike (PatSynCon ps))
-                                      ClassOpId cls               ->
+                                      ClassOpId cls _             ->
                                           Just (ATyCon (classTyCon cls))
                                       _other                      -> Nothing
 tyThingParent_maybe _other = Nothing
diff --git a/testsuite/tests/simplCore/should_compile/T15205.hs b/testsuite/tests/simplCore/should_compile/T15205.hs
new file mode 100644
index 0000000000..64eb1f51d6
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T15205.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE MultiParamTypeClasses, GADTs, TypeOperators #-}
+module Foo where
+
+class (a ~ b) => C a b where
+  op :: a -> a -> b
+
+f :: C a b => a -> b
+f x = op x x
diff --git a/testsuite/tests/simplCore/should_compile/T15205.stderr b/testsuite/tests/simplCore/should_compile/T15205.stderr
new file mode 100644
index 0000000000..c5336a8a6e
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T15205.stderr
@@ -0,0 +1,43 @@
+
+==================== Tidy Core ====================
+Result size of Tidy Core
+  = {terms: 25, types: 62, coercions: 0, joins: 0/0}
+
+-- RHS size: {terms: 7, types: 15, coercions: 0, joins: 0/0}
+Foo.$p1C [InlPrag=[~]] :: forall a b. C a b => a ~ b
+[GblId[ClassOp],
+ Arity=1,
+ Str=<S!P(SL,A)>,
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=1,unsat_ok=False,boring_ok=False)
+         Tmpl= \ (@a) (@b) (v [Occ=Once1!] :: C a b) ->
+                 case v of { Foo.C:C v2 [Occ=Once1] _ [Occ=Dead] -> v2 }}]
+Foo.$p1C
+  = \ (@a) (@b) (v :: C a b) -> case v of v1 { Foo.C:C v2 v3 -> v2 }
+
+-- RHS size: {terms: 7, types: 15, coercions: 0, joins: 0/0}
+op [InlPrag=[~]] :: forall a b. C a b => a -> a -> b
+[GblId[ClassOp],
+ Arity=1,
+ Str=<S!P(A,SL)>,
+ Unf=Unf{Src=StableSystem, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=ALWAYS_IF(arity=1,unsat_ok=False,boring_ok=False)
+         Tmpl= \ (@a) (@b) (v [Occ=Once1!] :: C a b) ->
+                 case v of { Foo.C:C _ [Occ=Dead] v3 [Occ=Once1] -> v3 }}]
+op
+  = \ (@a) (@b) (v :: C a b) -> case v of v1 { Foo.C:C v2 v3 -> v3 }
+
+-- RHS size: {terms: 8, types: 8, coercions: 0, joins: 0/0}
+f :: forall a b. C a b => a -> b
+[GblId,
+ Arity=2,
+ Str=<1P(A,1C(1,C(1,L)))><L>,
+ Unf=Unf{Src=<vanilla>, TopLvl=True,
+         Value=True, ConLike=True, WorkFree=True, Expandable=True,
+         Guidance=IF_ARGS [30 0] 40 0}]
+f = \ (@a) (@b) ($dC :: C a b) (x :: a) -> op @a @b $dC x x
+
+
+
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index 745bb22cd9..927ac191f6 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -471,3 +471,4 @@ test('T22502', normal, compile, ['-O'])
 test('T22611', [when(wordsize(32), skip), grep_errmsg(r'\$salterF') ], compile, ['-O -ddump-simpl -dsuppress-uniques -dsuppress-all'])
 test('T22715_2', normal, multimod_compile, ['T22715_2', '-v0 -O -fspecialise-aggressively'])
 test('T22802', normal, compile, ['-O'])
+test('T15205', normal, compile, ['-O -ddump-simpl -dno-typeable-binds -dsuppress-uniques'])