Add `vi_bot` and use it in `canDiverge`

3 files changed, 36 insertions, 24 deletions

diff --git a/compiler/GHC/HsToCore/PmCheck.hs b/compiler/GHC/HsToCore/PmCheck.hs
index c8e42dd248..3a96fcdce7 100644
--- a/compiler/GHC/HsToCore/PmCheck.hs
+++ b/compiler/GHC/HsToCore/PmCheck.hs
@@ -42,7 +42,6 @@ import SrcLoc
 import Util
 import Outputable
 import DataCon
-import TyCon
 import Var (EvVar)
 import Coercion
 import TcEvidence
@@ -1104,9 +1103,9 @@ forceIfCanDiverge delta x
 -- | 'forceIfCanDiverge' if the 'PmAltCon' was not a Newtype.
 -- See Note [Divergence of Newtype matches].
 addConMatchStrictness :: Delta -> Id -> PmAltCon -> PartialResult -> PartialResult
-addConMatchStrictness _     _ (PmAltConLike (RealDataCon dc)) res
-  | isNewTyCon (dataConTyCon dc) = res
-addConMatchStrictness delta x _ res = forceIfCanDiverge delta x res
+addConMatchStrictness _     _ alt res
+  | isNewtypeAltCon alt = res
+addConMatchStrictness delta x _   res = forceIfCanDiverge delta x res
 
 -- ----------------------------------------------------------------------------
 -- * Propagation of term constraints inwards when checking nested matches
diff --git a/compiler/GHC/HsToCore/PmCheck/Oracle.hs b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
index 1b5c5b24c8..0f8950e1b2 100644
--- a/compiler/GHC/HsToCore/PmCheck/Oracle.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Oracle.hs
@@ -153,8 +153,7 @@ mkOneConFull arg_tys con = do
   let ty_cs = map TyCt (substTheta subst (eqSpecPreds eq_spec ++ thetas))
   -- Figure out the types of strict constructor fields
   let arg_is_strict
-        | RealDataCon dc <- con
-        , isNewTyCon (dataConTyCon dc)
+        | RealDataCon dc <- con, isNewTyCon (dataConTyCon dc)
         = [True] -- See Note [Divergence of Newtype matches]
         | otherwise
         = map isBanged $ conLikeImplBangs con
@@ -666,7 +665,11 @@ tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM go delta new_tm_cs
 -- * Looking up VarInfo
 
 emptyVarInfo :: Id -> VarInfo
-emptyVarInfo x = VI (idType x) [] [] NoPM
+emptyVarInfo x = VI ty bot [] [] NoPM
+  where
+    ty = idType x
+    bot | Just False <- isLiftedType_maybe ty = False
+        | otherwise                           = True
 
 lookupVarInfo :: TmState -> Id -> VarInfo
 -- (lookupVarInfo tms x) tells what we know about 'x'
@@ -763,14 +766,7 @@ TyCon, so tc_rep = tc_fam afterwards.
 
 -- | Check whether adding a constraint @x ~ BOT@ to 'Delta' succeeds.
 canDiverge :: Delta -> Id -> Bool
-canDiverge delta@MkDelta{ delta_tm_st = ts } x
-  | VI _ pos neg _ <- lookupVarInfo ts x
-  = null neg && all pos_can_diverge pos
-  where
-    pos_can_diverge (PmAltConLike (RealDataCon dc), [y])
-      -- See Note [Divergence of Newtype matches]
-      | isNewTyCon (dataConTyCon dc) = canDiverge delta y
-    pos_can_diverge _ = False
+canDiverge MkDelta{ delta_tm_st = ts } x = vi_bot (lookupVarInfo ts x)
 
 {- Note [Divergence of Newtype matches]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -791,9 +787,9 @@ If we treat Newtypes like we treat regular DataCons, we would mark the third
 clause as redundant, which clearly is unsound. The solution:
 1. When checking the PmCon in 'pmCheck', never mark the result as Divergent if
    it's a Newtype match.
-2. Regard @T2 x@ as 'canDiverge' iff @x@ 'canDiverge'. E.g. @T2 x ~ _|_@ <=>
-   @x ~ _|_@. This way, the third clause will still be marked as inaccessible
-   RHS instead of redundant.
+2. Contrary to data types, a constraint @x ~ T2 y@ will not imply @x /~ ⊥@,
+   while a constraint @x /~ T2@ will still imply @x /~ ⊥@. This way, the third
+   clause will still be marked as inaccessible RHS instead of redundant.
 3. When testing for inhabitants ('mkOneConFull'), we regard the newtype field as
    strict, so that the newtype is inhabited iff its field is inhabited.
 -}
@@ -853,7 +849,7 @@ addTmCt delta ct = runMaybeT $ case ct of
 -- See Note [TmState invariants].
 addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta)
 addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = runMaybeT $ do
-  vi@(VI _ pos neg pm) <- lift (initLookupVarInfo delta x)
+  vi@(VI _ _ pos neg pm) <- lift (initLookupVarInfo delta x)
   -- 1. Bail out quickly when nalt contradicts a solution
   let contradicts nalt (cl, _args) = eqPmAltCon cl nalt == Equal
   guard (not (any (contradicts nalt) pos))
@@ -865,7 +861,9 @@ addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = runMayb
         -- See Note [Completeness checking with required Thetas]
         | hasRequiredTheta nalt  = neg
         | otherwise              = unionLists neg [nalt]
-  let vi_ext = vi{ vi_neg = neg' }
+  -- See Note [Divergence of Newtype matches]
+  let bot' = False
+  let vi_ext = vi{ vi_bot = bot', vi_neg = neg' }
   -- 3. Make sure there's at least one other possible constructor
   vi' <- case nalt of
     PmAltConLike cl
@@ -1065,7 +1063,7 @@ equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y
 -- See Note [TmState invariants].
 addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta
 addVarConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt args = do
-  VI ty pos neg cache <- lift (initLookupVarInfo delta x)
+  VI ty bot pos neg cache <- lift (initLookupVarInfo delta x)
   -- First try to refute with a negative fact
   guard (all ((/= Equal) . eqPmAltCon alt) neg)
   -- Then see if any of the other solutions (remember: each of them is an
@@ -1082,7 +1080,11 @@ addVarConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt args = do
       -- the new solution)
       let neg' = filter ((== PossiblyOverlap) . eqPmAltCon alt) neg
       let pos' = (alt,args):pos
-      pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg' cache)) reps}
+      -- Can only be ⊥ if it was before and this was a newtype AltCon
+      -- See Note [Divergence of Newtype matches]
+      let bot' = bot && isNewtypeAltCon alt
+      -- Really bot = False here? I don't think that works for newtypes
+      pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty bot' pos' neg' cache)) reps}
 
 ----------------------------------------
 -- * Enumerating inhabitation candidates
diff --git a/compiler/GHC/HsToCore/PmCheck/Types.hs b/compiler/GHC/HsToCore/PmCheck/Types.hs
index 10f172a430..1cdfb508f4 100644
--- a/compiler/GHC/HsToCore/PmCheck/Types.hs
+++ b/compiler/GHC/HsToCore/PmCheck/Types.hs
@@ -13,6 +13,7 @@ Author: George Karachalias <george.karachalias@cs.kuleuven.be>
 module GHC.HsToCore.PmCheck.Types (
         -- * Representations for Literals and AltCons
         PmLit(..), PmLitValue(..), PmAltCon(..), pmLitType, pmAltConType,
+        isNewtypeAltCon,
 
         -- ** Equality on 'PmAltCon's
         PmEquality(..), eqPmAltCon,
@@ -189,6 +190,10 @@ pmAltConType :: PmAltCon -> [Type] -> Type
 pmAltConType (PmAltLit lit)     _arg_tys = ASSERT( null _arg_tys ) pmLitType lit
 pmAltConType (PmAltConLike con) arg_tys  = conLikeResTy con arg_tys
 
+isNewtypeAltCon :: PmAltCon -> Bool
+isNewtypeAltCon (PmAltConLike (RealDataCon dc)) = isNewTyCon (dataConTyCon dc)
+isNewtypeAltCon _                               = False
+
 {- Note [Undecidable Equality for PmAltCons]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Equality on overloaded literals is undecidable in the general case. Consider
@@ -465,6 +470,10 @@ data VarInfo
   -- ^ The type of the variable. Important for rejecting possible GADT
   -- constructors or incompatible pattern synonyms (@Just42 :: Maybe Int@).
 
+  , vi_bot :: Bool
+  -- ^ Whether evaluation of this variable can still diverge. Initially @True@
+  -- for lifted types.
+
   , vi_pos :: ![(PmAltCon, [Id])]
   -- ^ Positive info: 'PmAltCon' apps it is (i.e. @x ~ [Just y, PatSyn z]@), all
   -- at the same time (i.e. conjunctive).  We need a list because of nested
@@ -501,8 +510,10 @@ instance Outputable TmState where
 
 -- | Not user-facing.
 instance Outputable VarInfo where
-  ppr (VI ty pos neg cache)
-    = braces (hcat (punctuate comma [ppr ty, ppr pos, ppr neg, ppr cache]))
+  ppr (VI ty bot pos neg cache)
+    = braces (hcat (punctuate comma [ppr ty, ppr mark, ppr pos, ppr neg, ppr cache]))
+    where
+      mark = if bot then char '~' else char '!'
 
 -- | Initial state of the term oracle.
 initTmState :: TmState