{-
Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
         Sebastian Graf <sgraf1337@gmail.com>
         Ryan Scott <ryan.gl.scott@gmail.com>
-}

{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-}

-- | The pattern match oracle. The main export of the module are the functions
-- 'addPmCts' for adding facts to the oracle, and 'provideEvidence' to turn a
-- 'Delta' into a concrete evidence for an equation.
module GHC.HsToCore.PmCheck.Oracle (

        DsM, tracePm, mkPmId,
        Delta, initDeltas, lookupRefuts, lookupSolution,

        PmCt(PmTyCt), PmCts, pattern PmVarCt, pattern PmCoreCt,
        pattern PmConCt, pattern PmNotConCt, pattern PmBotCt,
        pattern PmNotBotCt,

        addPmCts,           -- Add a constraint to the oracle.
        canDiverge,         -- Try to add the term equality x ~ ⊥
        provideEvidence
    ) where

#include "HsVersions.h"

import GHC.Prelude

import GHC.HsToCore.PmCheck.Types

import GHC.Driver.Session
import GHC.Utils.Outputable
import GHC.Utils.Error
import GHC.Utils.Misc
import GHC.Data.Bag
import GHC.Types.Unique.Set
import GHC.Types.Unique.DSet
import GHC.Types.Unique
import GHC.Types.Id
import GHC.Types.Var.Env
import GHC.Types.Unique.DFM
import GHC.Types.Var      (EvVar)
import GHC.Types.Name
import GHC.Core
import GHC.Core.FVs       (exprFreeVars)
import GHC.Core.Map
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils     (exprType)
import GHC.Core.Make      (mkListExpr, mkCharExpr)
import GHC.Types.Unique.Supply
import GHC.Data.FastString
import GHC.Types.SrcLoc
import GHC.Data.Maybe
import GHC.Core.ConLike
import GHC.Core.DataCon
import GHC.Core.PatSyn
import GHC.Core.TyCon
import GHC.Builtin.Types
import GHC.Builtin.Types.Prim (tYPETyCon)
import GHC.Core.TyCo.Rep
import GHC.Core.Type
import GHC.Tc.Solver   (tcNormalise, tcCheckSatisfiability)
import GHC.Core.Unify    (tcMatchTy)
import GHC.Tc.Types      (completeMatchConLikes)
import GHC.Core.Coercion
import GHC.Utils.Monad hiding (foldlM)
import GHC.HsToCore.Monad hiding (foldlM)
import GHC.Tc.Instance.Family
import GHC.Core.FamInstEnv

import Control.Monad (guard, mzero, when)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict
import Data.Bifunctor (second)
import Data.Either   (partitionEithers)
import Data.Foldable (foldlM, minimumBy, toList)
import Data.List     (find)
import qualified Data.List.NonEmpty as NonEmpty
import Data.Ord      (comparing)
import qualified Data.Semigroup as Semigroup
import Data.Tuple    (swap)

-- Debugging Infrastructure

tracePm :: String -> SDoc -> DsM ()
tracePm :: String -> SDoc -> DsM ()
tracePm String
herald SDoc
doc = do
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  PrintUnqualified
printer <- DsM PrintUnqualified
mkPrintUnqualifiedDs
  IO () -> DsM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> DsM ()) -> IO () -> DsM ()
forall a b. (a -> b) -> a -> b
$ PrintUnqualified
-> DynFlags -> DumpFlag -> String -> DumpFormat -> SDoc -> IO ()
dumpIfSet_dyn_printer PrintUnqualified
printer DynFlags
dflags
            DumpFlag
Opt_D_dump_ec_trace String
"" DumpFormat
FormatText (String -> SDoc
text String
herald SDoc -> SDoc -> SDoc
$$ (Int -> SDoc -> SDoc
nest Int
2 SDoc
doc))
{-# INLINE tracePm #-}  -- see Note [INLINE conditional tracing utilities]

-- | Generate a fresh `Id` of a given type
mkPmId :: Type -> DsM Id
mkPmId :: Type -> DsM Id
mkPmId Type
ty = IOEnv (Env DsGblEnv DsLclEnv) Unique
forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM IOEnv (Env DsGblEnv DsLclEnv) Unique
-> (Unique -> DsM Id) -> DsM Id
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Unique
unique ->
  let occname :: OccName
occname = FastString -> OccName
mkVarOccFS (FastString -> OccName) -> FastString -> OccName
forall a b. (a -> b) -> a -> b
$ String -> FastString
fsLit String
"pm"
      name :: Name
name    = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
unique OccName
occname SrcSpan
noSrcSpan
  in  Id -> DsM Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> Type -> Id
mkLocalIdOrCoVar Name
name Type
Many Type
ty)

-----------------------------------------------
-- * Caching possible matches of a COMPLETE set

markMatched :: ConLike -> PossibleMatches -> PossibleMatches
markMatched :: ConLike -> PossibleMatches -> PossibleMatches
markMatched ConLike
_   PossibleMatches
NoPM    = PossibleMatches
NoPM
markMatched ConLike
con (PM NonEmpty ConLikeSet
ms) = NonEmpty ConLikeSet -> PossibleMatches
PM (ConLike -> ConLikeSet -> ConLikeSet
del_one_con ConLike
con (ConLikeSet -> ConLikeSet)
-> NonEmpty ConLikeSet -> NonEmpty ConLikeSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty ConLikeSet
ms)
  where
    del_one_con :: ConLike -> ConLikeSet -> ConLikeSet
del_one_con = (ConLikeSet -> ConLike -> ConLikeSet)
-> ConLike -> ConLikeSet -> ConLikeSet
forall a b c. (a -> b -> c) -> b -> a -> c
flip ConLikeSet -> ConLike -> ConLikeSet
forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
delOneFromUniqDSet

---------------------------------------------------
-- * Instantiating constructors, types and evidence

-- | Instantiate a 'ConLike' given its universal type arguments. Instantiates
-- existential and term binders with fresh variables of appropriate type.
-- Returns instantiated type and term variables from the match, type evidence
-- and the types of strict constructor fields.
mkOneConFull :: [Type] -> ConLike -> DsM ([TyVar], [Id], Bag TyCt, [Type])
--  * 'con' K is a ConLike
--       - In the case of DataCons and most PatSynCons, these
--         are associated with a particular TyCon T
--       - But there are PatSynCons for this is not the case! See #11336, #17112
--
--  * 'arg_tys' tys are the types K's universally quantified type
--     variables should be instantiated to.
--       - For DataCons and most PatSyns these are the arguments of their TyCon
--       - For cases like the PatSyns in #11336, #17112, we can't easily guess
--         these, so don't call this function.
--
-- After instantiating the universal tyvars of K to tys we get
--          K @tys :: forall bs. Q => s1 .. sn -> T tys
-- Note that if K is a PatSynCon, depending on arg_tys, T might not necessarily
-- be a concrete TyCon.
--
-- Suppose y1 is a strict field. Then we get
-- Results: bs
--          [y1,..,yn]
--          Q
--          [s1]
mkOneConFull :: [Type] -> ConLike -> DsM ([Id], [Id], Bag Type, [Type])
mkOneConFull [Type]
arg_tys ConLike
con = do
  let ([Id]
univ_tvs, [Id]
ex_tvs, [EqSpec]
eq_spec, [Type]
thetas, [Type]
_req_theta, [Scaled Type]
field_tys, Type
_con_res_ty)
        = ConLike
-> ([Id], [Id], [EqSpec], [Type], [Type], [Scaled Type], Type)
conLikeFullSig ConLike
con
  -- pprTrace "mkOneConFull" (ppr con $$ ppr arg_tys $$ ppr univ_tvs $$ ppr _con_res_ty) (return ())
  -- Substitute universals for type arguments
  let subst_univ :: TCvSubst
subst_univ = [Id] -> [Type] -> TCvSubst
HasDebugCallStack => [Id] -> [Type] -> TCvSubst
zipTvSubst [Id]
univ_tvs [Type]
arg_tys
  -- Instantiate fresh existentials as arguments to the constructor. This is
  -- important for instantiating the Thetas and field types.
  (TCvSubst
subst, [Id]
_) <- TCvSubst -> [Id] -> UniqSupply -> (TCvSubst, [Id])
cloneTyVarBndrs TCvSubst
subst_univ [Id]
ex_tvs (UniqSupply -> (TCvSubst, [Id]))
-> IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
-> IOEnv (Env DsGblEnv DsLclEnv) (TCvSubst, [Id])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
  let field_tys' :: [Type]
field_tys' = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$ (Scaled Type -> Type) -> [Scaled Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
field_tys
  -- Instantiate fresh term variables (VAs) as arguments to the constructor
  [Id]
vars <- (Type -> DsM Id) -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [Id]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> DsM Id
mkPmId [Type]
field_tys'
  -- All constraints bound by the constructor (alpha-renamed), these are added
  -- to the type oracle
  let ty_cs :: [Type]
ty_cs = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTheta TCvSubst
subst ([EqSpec] -> [Type]
eqSpecPreds [EqSpec]
eq_spec [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
thetas)
  -- Figure out the types of strict constructor fields
  let arg_is_strict :: [Bool]
arg_is_strict
        | RealDataCon DataCon
dc <- ConLike
con
        , TyCon -> Bool
isNewTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc)
        = [Bool
True] -- See Note [Divergence of Newtype matches]
        | Bool
otherwise
        = (HsImplBang -> Bool) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map HsImplBang -> Bool
isBanged ([HsImplBang] -> [Bool]) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> a -> b
$ ConLike -> [HsImplBang]
conLikeImplBangs ConLike
con
      strict_arg_tys :: [Type]
strict_arg_tys = [Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
arg_is_strict [Type]
field_tys'
  ([Id], [Id], Bag Type, [Type])
-> DsM ([Id], [Id], Bag Type, [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Id]
ex_tvs, [Id]
vars, [Type] -> Bag Type
forall a. [a] -> Bag a
listToBag [Type]
ty_cs, [Type]
strict_arg_tys)

-------------------------
-- * Pattern match oracle


{- Note [Recovering from unsatisfiable pattern-matching constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the following code (see #12957 and #15450):

  f :: Int ~ Bool => ()
  f = case True of { False -> () }

We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC
used not to do this; in fact, it would warn that the match was /redundant/!
This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the
coverage checker deems any matches with unsatisfiable constraint sets to be
unreachable.

We decide to better than this. When beginning coverage checking, we first
check if the constraints in scope are unsatisfiable, and if so, we start
afresh with an empty set of constraints. This way, we'll get the warnings
that we expect.
-}

-------------------------------------
-- * Composable satisfiability checks

-- | Given a 'Delta', check if it is compatible with new facts encoded in this
-- this check. If so, return 'Just' a potentially extended 'Delta'. Return
-- 'Nothing' if unsatisfiable.
--
-- There are three essential SatisfiabilityChecks:
--   1. 'tmIsSatisfiable', adding term oracle facts
--   2. 'tyIsSatisfiable', adding type oracle facts
--   3. 'tysAreNonVoid', checks if the given types have an inhabitant
-- Functions like 'pmIsSatisfiable', 'nonVoid' and 'testInhabited' plug these
-- together as they see fit.
newtype SatisfiabilityCheck = SC (Delta -> DsM (Maybe Delta))

-- | Check the given 'Delta' for satisfiability by the given
-- 'SatisfiabilityCheck'. Return 'Just' a new, potentially extended, 'Delta' if
-- successful, and 'Nothing' otherwise.
runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
delta (SC Delta -> DsM (Maybe Delta)
chk) = Delta -> DsM (Maybe Delta)
chk Delta
delta

-- | Allowing easy composition of 'SatisfiabilityCheck's.
instance Semigroup SatisfiabilityCheck where
  -- This is @a >=> b@ from MaybeT DsM
  SC Delta -> DsM (Maybe Delta)
a <> :: SatisfiabilityCheck -> SatisfiabilityCheck -> SatisfiabilityCheck
<> SC Delta -> DsM (Maybe Delta)
b = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC Delta -> DsM (Maybe Delta)
c
    where
      c :: Delta -> DsM (Maybe Delta)
c Delta
delta = Delta -> DsM (Maybe Delta)
a Delta
delta DsM (Maybe Delta)
-> (Maybe Delta -> DsM (Maybe Delta)) -> DsM (Maybe Delta)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe Delta
Nothing     -> Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Delta
forall a. Maybe a
Nothing
        Just Delta
delta' -> Delta -> DsM (Maybe Delta)
b Delta
delta'

instance Monoid SatisfiabilityCheck where
  -- We only need this because of mconcat (which we use in place of sconcat,
  -- which requires NonEmpty lists as argument, making all call sites ugly)
  mempty :: SatisfiabilityCheck
mempty = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC (Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Delta -> DsM (Maybe Delta))
-> (Delta -> Maybe Delta) -> Delta -> DsM (Maybe Delta)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Delta -> Maybe Delta
forall a. a -> Maybe a
Just)

-------------------------------
-- * Oracle transition function

-- | Given a conlike's term constraints, type constraints, and strict argument
-- types, check if they are satisfiable.
-- (In other words, this is the ⊢_Sat oracle judgment from the GADTs Meet
-- Their Match paper.)
--
-- Taking strict argument types into account is something which was not
-- discussed in GADTs Meet Their Match. For an explanation of what role they
-- serve, see @Note [Strict argument type constraints]@.
pmIsSatisfiable
  :: Delta       -- ^ The ambient term and type constraints
                 --   (known to be satisfiable).
  -> Bag TyCt    -- ^ The new type constraints.
  -> Bag TmCt    -- ^ The new term constraints.
  -> [Type]      -- ^ The strict argument types.
  -> DsM (Maybe Delta)
                 -- ^ @'Just' delta@ if the constraints (@delta@) are
                 -- satisfiable, and each strict argument type is inhabitable.
                 -- 'Nothing' otherwise.
pmIsSatisfiable :: Delta -> Bag Type -> Bag TmCt -> [Type] -> DsM (Maybe Delta)
pmIsSatisfiable Delta
amb_cs Bag Type
new_ty_cs Bag TmCt
new_tm_cs [Type]
strict_arg_tys =
  -- The order is important here! Check the new type constraints before we check
  -- whether strict argument types are inhabited given those constraints.
  Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
amb_cs (SatisfiabilityCheck -> DsM (Maybe Delta))
-> SatisfiabilityCheck -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ [SatisfiabilityCheck] -> SatisfiabilityCheck
forall a. Monoid a => [a] -> a
mconcat
    [ Bool -> Bag Type -> SatisfiabilityCheck
tyIsSatisfiable Bool
True Bag Type
new_ty_cs
    , Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable Bag TmCt
new_tm_cs
    , RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
initRecTc [Type]
strict_arg_tys
    ]

-----------------------
-- * Type normalisation

-- | The return value of 'pmTopNormaliseType'
data TopNormaliseTypeResult
  = NoChange Type
  -- ^ 'tcNormalise' failed to simplify the type and 'topNormaliseTypeX' was
  -- unable to reduce the outermost type application, so the type came out
  -- unchanged.
  | NormalisedByConstraints Type
  -- ^ 'tcNormalise' was able to simplify the type with some local constraint
  -- from the type oracle, but 'topNormaliseTypeX' couldn't identify a type
  -- redex.
  | HadRedexes Type [(Type, DataCon, Type)] Type
  -- ^ 'tcNormalise' may or may not been able to simplify the type, but
  -- 'topNormaliseTypeX' made progress either way and got rid of at least one
  -- outermost type or data family redex or newtype.
  -- The first field is the last type that was reduced solely through type
  -- family applications (possibly just the 'tcNormalise'd type). This is the
  -- one that is equal (in source Haskell) to the initial type.
  -- The third field is the type that we get when also looking through data
  -- family applications and newtypes. This would be the representation type in
  -- Core (modulo casts).
  -- The second field is the list of Newtype 'DataCon's that we looked through
  -- in the chain of reduction steps between the Source type and the Core type.
  -- We also keep the type of the DataCon application and its field, so that we
  -- don't have to reconstruct it in 'inhabitationCandidates' and
  -- 'provideEvidence'.
  -- For an example, see Note [Type normalisation].

-- | Just give me the potentially normalised source type, unchanged or not!
normalisedSourceType :: TopNormaliseTypeResult -> Type
normalisedSourceType :: TopNormaliseTypeResult -> Type
normalisedSourceType (NoChange Type
ty)                = Type
ty
normalisedSourceType (NormalisedByConstraints Type
ty) = Type
ty
normalisedSourceType (HadRedexes Type
ty [(Type, DataCon, Type)]
_ Type
_)          = Type
ty

-- | Return the fields of 'HadRedexes'. Returns appropriate defaults in the
-- other cases.
tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts (NoChange Type
ty)                  = (Type
ty,     [],      Type
ty)
tntrGuts (NormalisedByConstraints Type
ty)   = (Type
ty,     [],      Type
ty)
tntrGuts (HadRedexes Type
src_ty [(Type, DataCon, Type)]
ds Type
core_ty) = (Type
src_ty, [(Type, DataCon, Type)]
ds, Type
core_ty)

instance Outputable TopNormaliseTypeResult where
  ppr :: TopNormaliseTypeResult -> SDoc
ppr (NoChange Type
ty)                  = String -> SDoc
text String
"NoChange" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
  ppr (NormalisedByConstraints Type
ty)   = String -> SDoc
text String
"NormalisedByConstraints" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
  ppr (HadRedexes Type
src_ty [(Type, DataCon, Type)]
ds Type
core_ty) = String -> SDoc
text String
"HadRedexes" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces SDoc
fields
    where
      fields :: SDoc
fields = [SDoc] -> SDoc
fsep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma [ String -> SDoc
text String
"src_ty =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
src_ty
                                     , String -> SDoc
text String
"newtype_dcs =" SDoc -> SDoc -> SDoc
<+> [(Type, DataCon, Type)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, DataCon, Type)]
ds
                                     , String -> SDoc
text String
"core_ty =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
core_ty ])

pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
-- ^ Get rid of *outermost* (or toplevel)
--      * type function redex
--      * data family redex
--      * newtypes
--
-- Behaves like `topNormaliseType_maybe`, but instead of returning a
-- coercion, it returns useful information for issuing pattern matching
-- warnings. See Note [Type normalisation] for details.
-- It also initially 'tcNormalise's the type with the bag of local constraints.
--
-- See 'TopNormaliseTypeResult' for the meaning of the return value.
--
-- NB: Normalisation can potentially change kinds, if the head of the type
-- is a type family with a variable result kind. I (Richard E) can't think
-- of a way to cause trouble here, though.
pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType (TySt Bag Id
inert) Type
typ
  = do FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
       -- Before proceeding, we chuck typ into the constraint solver, in case
       -- solving for given equalities may reduce typ some. See
       -- "Wrinkle: local equalities" in Note [Type normalisation].
       (Messages
_, Maybe Type
mb_typ') <- TcM Type -> DsM (Messages, Maybe Type)
forall a. TcM a -> DsM (Messages, Maybe a)
initTcDsForSolver (TcM Type -> DsM (Messages, Maybe Type))
-> TcM Type -> DsM (Messages, Maybe Type)
forall a b. (a -> b) -> a -> b
$ Bag Id -> Type -> TcM Type
tcNormalise Bag Id
inert Type
typ
       -- If tcNormalise didn't manage to simplify the type, continue anyway.
       -- We might be able to reduce type applications nonetheless!
       let typ' :: Type
typ' = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
typ Maybe Type
mb_typ'
       -- Now we look with topNormaliseTypeX through type and data family
       -- applications and newtypes, which tcNormalise does not do.
       -- See also 'TopNormaliseTypeResult'.
       TopNormaliseTypeResult -> DsM TopNormaliseTypeResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TopNormaliseTypeResult -> DsM TopNormaliseTypeResult)
-> TopNormaliseTypeResult -> DsM TopNormaliseTypeResult
forall a b. (a -> b) -> a -> b
$ case NormaliseStepper
  ([Type] -> [Type],
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> (([Type] -> [Type],
     [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    -> ([Type] -> [Type],
        [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    -> ([Type] -> [Type],
        [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]))
-> Type
-> Maybe
     (([Type] -> [Type],
       [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]),
      Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX (FamInstEnvs
-> NormaliseStepper
     ([Type] -> [Type],
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
stepper FamInstEnvs
env) ([Type] -> [Type],
 [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> ([Type] -> [Type],
    [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> ([Type] -> [Type],
    [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall {b} {c} {b} {c} {a} {a}.
(b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
comb Type
typ' of
         Maybe
  (([Type] -> [Type],
    [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]),
   Type)
Nothing
           | Maybe Type
Nothing <- Maybe Type
mb_typ' -> Type -> TopNormaliseTypeResult
NoChange Type
typ
           | Bool
otherwise          -> Type -> TopNormaliseTypeResult
NormalisedByConstraints Type
typ'
         Just (([Type] -> [Type]
ty_f,[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tm_f), Type
ty) -> Type -> [(Type, DataCon, Type)] -> Type -> TopNormaliseTypeResult
HadRedexes Type
src_ty [(Type, DataCon, Type)]
newtype_dcs Type
core_ty
           where
             src_ty :: Type
src_ty = Type -> [Type] -> Type
eq_src_ty Type
ty (Type
typ' Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type] -> [Type]
ty_f [Type
ty])
             newtype_dcs :: [(Type, DataCon, Type)]
newtype_dcs = [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tm_f []
             core_ty :: Type
core_ty = Type
ty
  where
    -- Find the first type in the sequence of rewrites that is a data type,
    -- newtype, or a data family application (not the representation tycon!).
    -- This is the one that is equal (in source Haskell) to the initial type.
    -- If none is found in the list, then all of them are type family
    -- applications, so we simply return the last one, which is the *simplest*.
    eq_src_ty :: Type -> [Type] -> Type
    eq_src_ty :: Type -> [Type] -> Type
eq_src_ty Type
ty [Type]
tys = Type -> (Type -> Type) -> Maybe Type -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type
ty Type -> Type
forall a. a -> a
id ((Type -> Bool) -> [Type] -> Maybe Type
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Type -> Bool
is_closed_or_data_family [Type]
tys)

    is_closed_or_data_family :: Type -> Bool
    is_closed_or_data_family :: Type -> Bool
is_closed_or_data_family Type
ty = Type -> Bool
pmIsClosedType Type
ty Bool -> Bool -> Bool
|| Type -> Bool
isDataFamilyAppType Type
ty

    -- For efficiency, represent both lists as difference lists.
    -- comb performs the concatenation, for both lists.
    comb :: (b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
comb (b -> c
tyf1, b -> c
tmf1) (a -> b
tyf2, a -> b
tmf2) = (b -> c
tyf1 (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
tyf2, b -> c
tmf1 (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
tmf2)

    stepper :: FamInstEnvs
-> NormaliseStepper
     ([Type] -> [Type],
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
stepper FamInstEnvs
env = NormaliseStepper
  ([Type] -> [Type],
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper NormaliseStepper
  ([Type] -> [Type],
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepper
     ([Type] -> [Type],
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepper
     ([Type] -> [Type],
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` FamInstEnvs
-> NormaliseStepper
     ([Type] -> [Type],
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall a.
FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
tyFamStepper FamInstEnvs
env

    -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
    -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
    newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
    newTypeStepper :: NormaliseStepper
  ([Type] -> [Type],
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys
      | Just (Type
ty', Coercion
_co) <- TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc [Type]
tys
      , let orig_ty :: Type
orig_ty = TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys
      = case RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_nts TyCon
tc of
          Just RecTcChecker
rec_nts' -> let tyf :: [Type] -> [Type]
tyf = (Type
orig_tyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:)
                               tmf :: [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tmf = ((Type
orig_ty, TyCon -> DataCon
tyConSingleDataCon TyCon
tc, Type
ty')(Type, DataCon, Type)
-> [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
forall a. a -> [a] -> [a]
:)
                           in  RecTcChecker
-> Type
-> ([Type] -> [Type],
    [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepResult
     ([Type] -> [Type],
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' ([Type] -> [Type]
tyf, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tmf)
          Maybe RecTcChecker
Nothing       -> NormaliseStepResult
  ([Type] -> [Type],
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. NormaliseStepResult ev
NS_Abort
      | Bool
otherwise
      = NormaliseStepResult
  ([Type] -> [Type],
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. NormaliseStepResult ev
NS_Done

    tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
    tyFamStepper :: forall a.
FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
tyFamStepper FamInstEnvs
env RecTcChecker
rec_nts TyCon
tc [Type]
tys  -- Try to step a type/data family
      = case FamInstEnvs -> TyCon -> [Type] -> Maybe (Coercion, Type, Coercion)
topReduceTyFamApp_maybe FamInstEnvs
env TyCon
tc [Type]
tys of
          Just (Coercion
_, Type
rhs, Coercion
_) -> RecTcChecker
-> Type
-> ([Type] -> [Type], a -> a)
-> NormaliseStepResult ([Type] -> [Type], a -> a)
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
rhs ((Type
rhsType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:), a -> a
forall a. a -> a
id)
          Maybe (Coercion, Type, Coercion)
_                -> NormaliseStepResult ([Type] -> [Type], a -> a)
forall ev. NormaliseStepResult ev
NS_Done

-- | Returns 'True' if the argument 'Type' is a fully saturated application of
-- a closed type constructor.
--
-- Closed type constructors are those with a fixed right hand side, as
-- opposed to e.g. associated types. These are of particular interest for
-- pattern-match coverage checking, because GHC can exhaustively consider all
-- possible forms that values of a closed type can take on.
--
-- Note that this function is intended to be used to check types of value-level
-- patterns, so as a consequence, the 'Type' supplied as an argument to this
-- function should be of kind @Type@.
pmIsClosedType :: Type -> Bool
pmIsClosedType :: Type -> Bool
pmIsClosedType Type
ty
  = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
      Just (TyCon
tc, [Type]
ty_args)
             | TyCon -> Bool
is_algebraic_like TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamilyTyCon TyCon
tc)
             -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
      Maybe (TyCon, [Type])
_other -> Bool
False
  where
    -- This returns True for TyCons which /act like/ algebraic types.
    -- (See "Type#type_classification" for what an algebraic type is.)
    --
    -- This is qualified with \"like\" because of a particular special
    -- case: TYPE (the underlyind kind behind Type, among others). TYPE
    -- is conceptually a datatype (and thus algebraic), but in practice it is
    -- a primitive builtin type, so we must check for it specially.
    --
    -- NB: it makes sense to think of TYPE as a closed type in a value-level,
    -- pattern-matching context. However, at the kind level, TYPE is certainly
    -- not closed! Since this function is specifically tailored towards pattern
    -- matching, however, it's OK to label TYPE as closed.
    is_algebraic_like :: TyCon -> Bool
    is_algebraic_like :: TyCon -> Bool
is_algebraic_like TyCon
tc = TyCon -> Bool
isAlgTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon

{- Note [Type normalisation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Constructs like -XEmptyCase or a previous unsuccessful pattern match on a data
constructor place a non-void constraint on the matched thing. This means that it
boils down to checking whether the type of the scrutinee is inhabited. Function
pmTopNormaliseType gets rid of the outermost type function/data family redex and
newtypes, in search of an algebraic type constructor, which is easier to check
for inhabitation.

It returns 3 results instead of one, because there are 2 subtle points:
1. Newtypes are isomorphic to the underlying type in core but not in the source
   language,
2. The representational data family tycon is used internally but should not be
   shown to the user

Hence, if pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty),
then
  (a) src_ty is the rewritten type which we can show to the user. That is, the
      type we get if we rewrite type families but not data families or
      newtypes.
  (b) dcs is the list of newtype constructors "skipped", every time we normalise
      a newtype to its core representation, we keep track of the source data
      constructor. For convenience, we also track the type we unwrap and the
      type of its field. Example: @Down 42@ => @[(Down @Int, Down, Int)]
  (c) core_ty is the rewritten type. That is,
        pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty)
      implies
        topNormaliseType_maybe env ty = Just (co, core_ty)
      for some coercion co.

To see how all cases come into play, consider the following example:

  data family T a :: *
  data instance T Int = T1 | T2 Bool
  -- Which gives rise to FC:
  --   data T a
  --   data R:TInt = T1 | T2 Bool
  --   axiom ax_ti : T Int ~R R:TInt

  newtype G1 = MkG1 (T Int)
  newtype G2 = MkG2 G1

  type instance F Int  = F Char
  type instance F Char = G2

In this case pmTopNormaliseType env ty_cs (F Int) results in

  Just (G2, [(G2,MkG2,G1),(G1,MkG1,T Int)], R:TInt)

Which means that in source Haskell:
  - G2 is equivalent to F Int (in contrast, G1 isn't).
  - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).

-----
-- Wrinkle: Local equalities
-----

Given the following type family:

  type family F a
  type instance F Int = Void

Should the following program (from #14813) be considered exhaustive?

  f :: (i ~ Int) => F i -> a
  f x = case x of {}

You might think "of course, since `x` is obviously of type Void". But the
idType of `x` is technically F i, not Void, so if we pass F i to
inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive.
In order to avoid this pitfall, we need to normalise the type passed to
pmTopNormaliseType, using the constraint solver to solve for any local
equalities (such as i ~ Int) that may be in scope.
-}

----------------
-- * Type oracle

-- | Allocates a fresh 'EvVar' name for 'PredTy's.
nameTyCt :: PredType -> DsM EvVar
nameTyCt :: Type -> DsM Id
nameTyCt Type
pred_ty = do
  Unique
unique <- IOEnv (Env DsGblEnv DsLclEnv) Unique
forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM
  let occname :: OccName
occname = FastString -> OccName
mkVarOccFS (String -> FastString
fsLit (String
"pm_"String -> String -> String
forall a. [a] -> [a] -> [a]
++Unique -> String
forall a. Show a => a -> String
show Unique
unique))
      idname :: Name
idname  = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
unique OccName
occname SrcSpan
noSrcSpan
  Id -> DsM Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> Type -> Id
mkLocalIdOrCoVar Name
idname Type
Many Type
pred_ty)

-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle :: TyState -> Bag Type -> DsM (Maybe TyState)
tyOracle (TySt Bag Id
inert) Bag Type
cts
  = do { Bag Id
evs <- (Type -> DsM Id)
-> Bag Type -> IOEnv (Env DsGblEnv DsLclEnv) (Bag Id)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Type -> DsM Id
nameTyCt Bag Type
cts
       ; let new_inert :: Bag Id
new_inert = Bag Id
inert Bag Id -> Bag Id -> Bag Id
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag Id
evs
       ; String -> SDoc -> DsM ()
tracePm String
"tyOracle" (Bag Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Type
cts)
       ; ((WarningMessages
_warns, WarningMessages
errs), Maybe Bool
res) <- TcM Bool -> DsM (Messages, Maybe Bool)
forall a. TcM a -> DsM (Messages, Maybe a)
initTcDsForSolver (TcM Bool -> DsM (Messages, Maybe Bool))
-> TcM Bool -> DsM (Messages, Maybe Bool)
forall a b. (a -> b) -> a -> b
$ Bag Id -> TcM Bool
tcCheckSatisfiability Bag Id
new_inert
       ; case Maybe Bool
res of
            Just Bool
True  -> Maybe TyState -> DsM (Maybe TyState)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyState -> Maybe TyState
forall a. a -> Maybe a
Just (Bag Id -> TyState
TySt Bag Id
new_inert))
            Just Bool
False -> Maybe TyState -> DsM (Maybe TyState)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe TyState
forall a. Maybe a
Nothing
            Maybe Bool
Nothing    -> String -> SDoc -> DsM (Maybe TyState)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"tyOracle" ([SDoc] -> SDoc
vcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ WarningMessages -> [SDoc]
pprErrMsgBagWithLoc WarningMessages
errs) }

-- | A 'SatisfiabilityCheck' based on new type-level constraints.
-- Returns a new 'Delta' if the new constraints are compatible with existing
-- ones. Doesn't bother calling out to the type oracle if the bag of new type
-- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle
-- for emptiness if the first argument is 'True'.
tyIsSatisfiable :: Bool -> Bag PredType -> SatisfiabilityCheck
tyIsSatisfiable :: Bool -> Bag Type -> SatisfiabilityCheck
tyIsSatisfiable Bool
recheck_complete_sets Bag Type
new_ty_cs = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC ((Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck)
-> (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
forall a b. (a -> b) -> a -> b
$ \Delta
delta ->
  if Bag Type -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Type
new_ty_cs
    then Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta)
    else TyState -> Bag Type -> DsM (Maybe TyState)
tyOracle (Delta -> TyState
delta_ty_st Delta
delta) Bag Type
new_ty_cs DsM (Maybe TyState)
-> (Maybe TyState -> DsM (Maybe Delta)) -> DsM (Maybe Delta)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Maybe TyState
Nothing                   -> Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Delta
forall a. Maybe a
Nothing
      Just TyState
ty_st'               -> do
        let delta' :: Delta
delta' = Delta
delta{ delta_ty_st :: TyState
delta_ty_st = TyState
ty_st' }
        if Bool
recheck_complete_sets
          then Delta -> DsM (Maybe Delta)
ensureAllPossibleMatchesInhabited Delta
delta'
          else Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta')


{- *********************************************************************
*                                                                      *
              DIdEnv with sharing
*                                                                      *
********************************************************************* -}


{- *********************************************************************
*                                                                      *
                 TmState
          What we know about terms
*                                                                      *
********************************************************************* -}

{- Note [The Pos/Neg invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos',
any entry in 'vi_neg' must be incomparable to C (return Nothing) according to
'eqPmAltCons'. Those entries that are comparable either lead to a refutation
or are redundant. Examples:
* @x ~ Just y@, @x /~ [Just]@. 'eqPmAltCon' returns @Equal@, so refute.
* @x ~ Nothing@, @x /~ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative
  info is redundant and should be discarded.
* @x ~ I# y@, @x /~ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal.
  We keep this info in order to be able to refute a redundant match on i.e. 4
  later on.

This carries over to pattern synonyms and overloaded literals. Say, we have
    pattern Just42 = Just 42
    case Just42 of x
      Nothing -> ()
      Just _  -> ()
Even though we had a solution for the value abstraction called x here in form
of a PatSynCon (Just42,[]), this solution is incomparable to both Nothing and
Just. Hence we retain the info in vi_neg, which eventually allows us to detect
the complete pattern match.

The Pos/Neg invariant extends to vi_cache, which stores essentially positive
information. We make sure that vi_neg and vi_cache never overlap. This isn't
strictly necessary since vi_cache is just a cache, so doesn't need to be
accurate: Every suggestion of a possible ConLike from vi_cache might be
refutable by the type oracle anyway. But it helps to maintain sanity while
debugging traces.

Note [Why record both positive and negative info?]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
You might think that knowing positive info (like x ~ Just y) would render
negative info irrelevant, but not so because of pattern synonyms.  E.g we might
know that x cannot match (Foo 4), where pattern Foo p = Just p

Also overloaded literals themselves behave like pattern synonyms. E.g if
postively we know that (x ~ I# y), we might also negatively want to record that
x does not match 45 f 45       = e2 f (I# 22#) = e3 f 45       = e4  --
Overlapped

Note [TmState invariants]
~~~~~~~~~~~~~~~~~~~~~~~~~
The term oracle state is never obviously (i.e., without consulting the type
oracle) contradictory. This implies a few invariants:
* Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute.
  This is implied by the Note [Pos/Neg invariant].
* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_cache to
  detect this, but we could just compare whole COMPLETE sets to vi_neg every
  time, if it weren't for performance.

Maintaining these invariants in 'addVarCt' (the core of the term oracle) and
'addNotConCt' is subtle.
* Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate').
  - (COMPLETE) If we had @x /~ True@ and @y /~ False@, then we get
    @x /~ [True,False]@. This is vacuous by matter of comparing to the built-in
    COMPLETE set, so should refute.
  - (Pos/Neg) If we had @x /~ True@ and @y ~ True@, we have to refute.
* Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addConCt')
  - (Neg) If we had @x /~ K@, refute.
  - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to
    'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute.
  - (Refine) If we had @x /~ K zs@, unify each y with each z in turn.
* Adding negative information. Example: Add the fact @x /~ Nothing@ (see 'addNotConCt')
  - (Refut) If we have @x ~ K ys@, refute.
  - (COMPLETE) If K=Nothing and we had @x /~ Just@, then we get
    @x /~ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in
    COMPLETE set, so should refute.

Note that merging VarInfo in equate can be done by calling out to 'addConCt' and
'addNotConCt' for each of the facts individually.

Note [Representation of Strings in TmState]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Instead of treating regular String literals as a PmLits, we treat it as a list
of characters in the oracle for better overlap reasoning. The following example
shows why:

  f :: String -> ()
  f ('f':_) = ()
  f "foo"   = ()
  f _       = ()

The second case is redundant, and we like to warn about it. Therefore either
the oracle will have to do some smart conversion between the list and literal
representation or treat is as the list it really is at runtime.

The "smart conversion" has the advantage of leveraging the more compact literal
representation wherever possible, but is really nasty to get right with negative
equalities: Just think of how to encode @x /= "foo"@.
The "list" option is far simpler, but incurs some overhead in representation and
warning messages (which can be alleviated by someone with enough dedication).
-}

-- | A 'SatisfiabilityCheck' based on new term-level constraints.
-- Returns a new 'Delta' if the new constraints are compatible with existing
-- ones.
tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable Bag TmCt
new_tm_cs = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC ((Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck)
-> (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> MaybeT DsM Delta -> DsM (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT DsM Delta -> DsM (Maybe Delta))
-> MaybeT DsM Delta -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ (Delta -> TmCt -> MaybeT DsM Delta)
-> Delta -> Bag TmCt -> MaybeT DsM Delta
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Delta -> TmCt -> MaybeT DsM Delta
addTmCt Delta
delta Bag TmCt
new_tm_cs

-----------------------
-- * Looking up VarInfo

emptyVarInfo :: Id -> VarInfo
emptyVarInfo :: Id -> VarInfo
emptyVarInfo Id
x = Type
-> [(PmAltCon, [Id], [Id])]
-> PmAltConSet
-> PossibleMatches
-> VarInfo
VI (Id -> Type
idType Id
x) [] PmAltConSet
emptyPmAltConSet PossibleMatches
NoPM

lookupVarInfo :: TmState -> Id -> VarInfo
-- (lookupVarInfo tms x) tells what we know about 'x'
lookupVarInfo :: TmState -> Id -> VarInfo
lookupVarInfo (TmSt SharedDIdEnv VarInfo
env CoreMap Id
_) Id
x = VarInfo -> Maybe VarInfo -> VarInfo
forall a. a -> Maybe a -> a
fromMaybe (Id -> VarInfo
emptyVarInfo Id
x) (SharedDIdEnv VarInfo -> Id -> Maybe VarInfo
forall a. SharedDIdEnv a -> Id -> Maybe a
lookupSDIE SharedDIdEnv VarInfo
env Id
x)

initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo
initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo
initPossibleMatches TyState
ty_st vi :: VarInfo
vi@VI{ vi_ty :: VarInfo -> Type
vi_ty = Type
ty, vi_cache :: VarInfo -> PossibleMatches
vi_cache = PossibleMatches
NoPM } = do
  -- New evidence might lead to refined info on ty, in turn leading to discovery
  -- of a COMPLETE set.
  TopNormaliseTypeResult
res <- TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty
  let ty' :: Type
ty' = TopNormaliseTypeResult -> Type
normalisedSourceType TopNormaliseTypeResult
res
  case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty' of
    Maybe (TyCon, [Type])
Nothing -> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty' }
    Just (TyCon
tc, [Type
_])
      | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon
      -- TYPE acts like an empty data type on the term-level (#14086), but
      -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
      -- special case.
      -> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty', vi_cache :: PossibleMatches
vi_cache = NonEmpty ConLikeSet -> PossibleMatches
PM (ConLikeSet -> NonEmpty ConLikeSet
forall (f :: * -> *) a. Applicative f => a -> f a
pure ConLikeSet
forall a. UniqDSet a
emptyUniqDSet) }
    Just (TyCon
tc, [Type]
tc_args) -> do
      -- See Note [COMPLETE sets on data families]
      (TyCon
tc_rep, TyCon
tc_fam) <- case TyCon -> Maybe (TyCon, [Type])
tyConFamInst_maybe TyCon
tc of
        Just (TyCon
tc_fam, [Type]
_) -> (TyCon, TyCon) -> IOEnv (Env DsGblEnv DsLclEnv) (TyCon, TyCon)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon
tc, TyCon
tc_fam)
        Maybe (TyCon, [Type])
Nothing -> do
          FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
          let (TyCon
tc_rep, [Type]
_tc_rep_args, Coercion
_co) = FamInstEnvs -> TyCon -> [Type] -> (TyCon, [Type], Coercion)
tcLookupDataFamInst FamInstEnvs
env TyCon
tc [Type]
tc_args
          (TyCon, TyCon) -> IOEnv (Env DsGblEnv DsLclEnv) (TyCon, TyCon)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyCon
tc_rep, TyCon
tc)
      -- Note that the common case here is tc_rep == tc_fam
      let mb_rdcs :: Maybe [ConLike]
mb_rdcs = (DataCon -> ConLike) -> [DataCon] -> [ConLike]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> ConLike
RealDataCon ([DataCon] -> [ConLike]) -> Maybe [DataCon] -> Maybe [ConLike]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> Maybe [DataCon]
tyConDataCons_maybe TyCon
tc_rep
      let rdcs :: [[ConLike]]
rdcs = Maybe [ConLike] -> [[ConLike]]
forall a. Maybe a -> [a]
maybeToList Maybe [ConLike]
mb_rdcs
      -- NB: tc_fam, because COMPLETE sets are associated with the parent data
      -- family TyCon
      [CompleteMatch]
pragmas <- TyCon -> DsM [CompleteMatch]
dsGetCompleteMatches TyCon
tc_fam
      let fams :: CompleteMatch -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
fams = (Name -> IOEnv (Env DsGblEnv DsLclEnv) ConLike)
-> [Name] -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> IOEnv (Env DsGblEnv DsLclEnv) ConLike
dsLookupConLike ([Name] -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike])
-> (CompleteMatch -> [Name])
-> CompleteMatch
-> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CompleteMatch -> [Name]
completeMatchConLikes
      [[ConLike]]
pscs <- (CompleteMatch -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike])
-> [CompleteMatch] -> IOEnv (Env DsGblEnv DsLclEnv) [[ConLike]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CompleteMatch -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
fams [CompleteMatch]
pragmas
      -- pprTrace "initPossibleMatches" (ppr ty $$ ppr ty' $$ ppr tc_rep <+> ppr tc_fam <+> ppr tc_args $$ ppr (rdcs ++ pscs)) (return ())
      case [[ConLike]] -> Maybe (NonEmpty [ConLike])
forall a. [a] -> Maybe (NonEmpty a)
NonEmpty.nonEmpty ([[ConLike]]
rdcs [[ConLike]] -> [[ConLike]] -> [[ConLike]]
forall a. [a] -> [a] -> [a]
++ [[ConLike]]
pscs) of
        Maybe (NonEmpty [ConLike])
Nothing -> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty' } -- Didn't find any COMPLETE sets
        Just NonEmpty [ConLike]
cs -> VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi{ vi_ty :: Type
vi_ty = Type
ty', vi_cache :: PossibleMatches
vi_cache = NonEmpty ConLikeSet -> PossibleMatches
PM ([ConLike] -> ConLikeSet
forall a. Uniquable a => [a] -> UniqDSet a
mkUniqDSet ([ConLike] -> ConLikeSet)
-> NonEmpty [ConLike] -> NonEmpty ConLikeSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty [ConLike]
cs) }
initPossibleMatches TyState
_     VarInfo
vi                                   = VarInfo -> DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi

-- | @initLookupVarInfo ts x@ looks up the 'VarInfo' for @x@ in @ts@ and tries
-- to initialise the 'vi_cache' component if it was 'NoPM' through
-- 'initPossibleMatches'.
initLookupVarInfo :: Delta -> Id -> DsM VarInfo
initLookupVarInfo :: Delta -> Id -> DsM VarInfo
initLookupVarInfo MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmState
ts, delta_ty_st :: Delta -> TyState
delta_ty_st = TyState
ty_st } Id
x
  = TyState -> VarInfo -> DsM VarInfo
initPossibleMatches TyState
ty_st (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x)

{- Note [COMPLETE sets on data families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
User-defined COMPLETE sets involving data families are attached to the family
TyCon, whereas the built-in COMPLETE set is attached to a data family instance's
representation TyCon. This matters for COMPLETE sets involving both DataCons
and PatSyns (from #17207):

  data family T a
  data family instance T () = A | B
  pattern C = B
  {-# COMPLETE A, C #-}
  f :: T () -> ()
  f A = ()
  f C = ()

The match on A is actually wrapped in a CoPat, matching impedance between T ()
and its representation TyCon, which we translate as
@x | let y = x |> co, A <- y@ in PmCheck.

Which TyCon should we use for looking up the COMPLETE set? The representation
TyCon from the match on A would only reveal the built-in COMPLETE set, while the
data family TyCon would only give the user-defined one. But when initialising
the PossibleMatches for a given Type, we want to do so only once, because
merging different COMPLETE sets after the fact is very complicated and possibly
inefficient.

So in fact, we just *drop* the coercion arising from the CoPat when handling
handling the constraint @y ~ x |> co@ in addCoreCt, just equating @y ~ x@.
We then handle the fallout in initPossibleMatches, which has to get a hand at
both the representation TyCon tc_rep and the parent data family TyCon tc_fam.
It considers three cases after having established that the Type is a TyConApp:

1. The TyCon is a vanilla data type constructor
2. The TyCon is tc_rep
3. The TyCon is tc_fam

1. is simple and subsumed by the handling of the other two.
We check for case 2. by 'tyConFamInst_maybe' and get the tc_fam out.
Otherwise (3.), we try to lookup the data family instance at that particular
type to get out the tc_rep. In case 1., this will just return the original
TyCon, so tc_rep = tc_fam afterwards.
-}

------------------------------------------------
-- * Exported utility functions querying 'Delta'

-- | Check whether adding a constraint @x ~ BOT@ to 'Delta' succeeds.
canDiverge :: Delta -> Id -> Bool
canDiverge :: Delta -> Id -> Bool
canDiverge delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmState
ts } Id
x
  | VI Type
_ [(PmAltCon, [Id], [Id])]
pos PmAltConSet
neg PossibleMatches
_ <- TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x
  = PmAltConSet -> Bool
isEmptyPmAltConSet PmAltConSet
neg Bool -> Bool -> Bool
&& ((PmAltCon, [Id], [Id]) -> Bool)
-> [(PmAltCon, [Id], [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PmAltCon, [Id], [Id]) -> Bool
forall {b}. (PmAltCon, b, [Id]) -> Bool
pos_can_diverge [(PmAltCon, [Id], [Id])]
pos
  where
    pos_can_diverge :: (PmAltCon, b, [Id]) -> Bool
pos_can_diverge (PmAltConLike (RealDataCon DataCon
dc), b
_, [Id
y])
      -- See Note [Divergence of Newtype matches]
      | TyCon -> Bool
isNewTyCon (DataCon -> TyCon
dataConTyCon DataCon
dc) = Delta -> Id -> Bool
canDiverge Delta
delta Id
y
    pos_can_diverge (PmAltCon, b, [Id])
_ = Bool
False

{- Note [Divergence of Newtype matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Newtypes behave rather strangely when compared to ordinary DataCons. In a
pattern-match, they behave like a irrefutable (lazy) match, but for inhabitation
testing purposes (e.g. at construction sites), they behave rather like a DataCon
with a *strict* field, because they don't contribute their own bottom and are
inhabited iff the wrapped type is inhabited.

This distinction becomes apparent in #17248:

  newtype T2 a = T2 a
  g _      True = ()
  g (T2 _) True = ()
  g !_     True = ()

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 compiling the PmCon guard in 'pmCompileTree', don't add a @DivergeIf@,
   because the match will never diverge.
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.
3. When testing for inhabitants ('mkOneConFull'), we regard the newtype field as
   strict, so that the newtype is inhabited iff its field is inhabited.
-}

lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon]
-- Unfortunately we need the extra bit of polymorphism and the unfortunate
-- duplication of lookupVarInfo here.
lookupRefuts :: forall k. Uniquable k => Delta -> k -> [PmAltCon]
lookupRefuts MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = ts :: TmState
ts@(TmSt (SDIE DIdEnv (Shared VarInfo)
env) CoreMap Id
_) } k
k =
  case DIdEnv (Shared VarInfo) -> Unique -> Maybe (Shared VarInfo)
forall key elt. UniqDFM key elt -> Unique -> Maybe elt
lookupUDFM_Directly DIdEnv (Shared VarInfo)
env (k -> Unique
forall a. Uniquable a => a -> Unique
getUnique k
k) of
    Maybe (Shared VarInfo)
Nothing -> []
    Just (Indirect Id
y) -> PmAltConSet -> [PmAltCon]
pmAltConSetElems (VarInfo -> PmAltConSet
vi_neg (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
y))
    Just (Entry VarInfo
vi)   -> PmAltConSet -> [PmAltCon]
pmAltConSetElems (VarInfo -> PmAltConSet
vi_neg VarInfo
vi)

isDataConSolution :: (PmAltCon, [TyVar], [Id]) -> Bool
isDataConSolution :: (PmAltCon, [Id], [Id]) -> Bool
isDataConSolution (PmAltConLike (RealDataCon DataCon
_), [Id]
_, [Id]
_) = Bool
True
isDataConSolution (PmAltCon, [Id], [Id])
_                                    = Bool
False

-- @lookupSolution delta x@ picks a single solution ('vi_pos') of @x@ from
-- possibly many, preferring 'RealDataCon' solutions whenever possible.
lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [TyVar], [Id])
lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id], [Id])
lookupSolution Delta
delta Id
x = case VarInfo -> [(PmAltCon, [Id], [Id])]
vi_pos (TmState -> Id -> VarInfo
lookupVarInfo (Delta -> TmState
delta_tm_st Delta
delta) Id
x) of
  []                                         -> Maybe (PmAltCon, [Id], [Id])
forall a. Maybe a
Nothing
  [(PmAltCon, [Id], [Id])]
pos
    | Just (PmAltCon, [Id], [Id])
sol <- ((PmAltCon, [Id], [Id]) -> Bool)
-> [(PmAltCon, [Id], [Id])] -> Maybe (PmAltCon, [Id], [Id])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (PmAltCon, [Id], [Id]) -> Bool
isDataConSolution [(PmAltCon, [Id], [Id])]
pos -> (PmAltCon, [Id], [Id]) -> Maybe (PmAltCon, [Id], [Id])
forall a. a -> Maybe a
Just (PmAltCon, [Id], [Id])
sol
    | Bool
otherwise                              -> (PmAltCon, [Id], [Id]) -> Maybe (PmAltCon, [Id], [Id])
forall a. a -> Maybe a
Just ([(PmAltCon, [Id], [Id])] -> (PmAltCon, [Id], [Id])
forall a. [a] -> a
head [(PmAltCon, [Id], [Id])]
pos)

-------------------------------
-- * Adding facts to the oracle

-- | A term constraint.
data TmCt
  = TmVarCt     !Id !Id
  -- ^ @TmVarCt x y@ encodes "x ~ y", equating @x@ and @y@.
  | TmCoreCt    !Id !CoreExpr
  -- ^ @TmCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@.
  | TmConCt     !Id !PmAltCon ![TyVar] ![Id]
  -- ^ @TmConCt x K tvs ys@ encodes "x ~ K @tvs ys", equating @x@ with the 'PmAltCon'
  -- application @K @tvs ys@.
  | TmNotConCt  !Id !PmAltCon
  -- ^ @TmNotConCt x K@ encodes "x /~ K", asserting that @x@ can't be headed
  -- by @K@.
  | TmBotCt     !Id
  -- ^ @TmBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
  -- by @K@.
  | TmNotBotCt !Id
  -- ^ @TmNotBotCt x y@ encodes "x /~ ⊥", asserting that @x@ can't be ⊥.

instance Outputable TmCt where
  ppr :: TmCt -> SDoc
ppr (TmVarCt Id
x Id
y)            = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
y
  ppr (TmCoreCt Id
x CoreExpr
e)           = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e
  ppr (TmConCt Id
x PmAltCon
con [Id]
tvs [Id]
args) = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> Char -> SDoc
char Char
'~' SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
hsep (PmAltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltCon
con SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: [SDoc]
pp_tvs [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc]
pp_args)
    where
      pp_tvs :: [SDoc]
pp_tvs  = (Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ((SDoc -> SDoc -> SDoc
<> Char -> SDoc
char Char
'@') (SDoc -> SDoc) -> (Id -> SDoc) -> Id -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr) [Id]
tvs
      pp_args :: [SDoc]
pp_args = (Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
args
  ppr (TmNotConCt Id
x PmAltCon
con)       = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"/~" SDoc -> SDoc -> SDoc
<+> PmAltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltCon
con
  ppr (TmBotCt Id
x)              = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"~ ⊥"
  ppr (TmNotBotCt Id
x)           = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"/~ ⊥"

type TyCt = PredType

-- | An oracle constraint.
data PmCt
  = PmTyCt !TyCt
  -- ^ @PmTy pred_ty@ carries 'PredType's, for example equality constraints.
  | PmTmCt !TmCt
  -- ^ A term constraint.

type PmCts = Bag PmCt

pattern PmVarCt :: Id -> Id -> PmCt
pattern $mPmVarCt :: forall {r}. PmCt -> (Id -> Id -> r) -> (Void# -> r) -> r
$bPmVarCt :: Id -> Id -> PmCt
PmVarCt x y            = PmTmCt (TmVarCt x y)
pattern PmCoreCt :: Id -> CoreExpr -> PmCt
pattern $mPmCoreCt :: forall {r}. PmCt -> (Id -> CoreExpr -> r) -> (Void# -> r) -> r
$bPmCoreCt :: Id -> CoreExpr -> PmCt
PmCoreCt x e           = PmTmCt (TmCoreCt x e)
pattern PmConCt :: Id -> PmAltCon -> [TyVar] -> [Id] -> PmCt
pattern $mPmConCt :: forall {r}.
PmCt -> (Id -> PmAltCon -> [Id] -> [Id] -> r) -> (Void# -> r) -> r
$bPmConCt :: Id -> PmAltCon -> [Id] -> [Id] -> PmCt
PmConCt x con tvs args = PmTmCt (TmConCt x con tvs args)
pattern PmNotConCt :: Id -> PmAltCon -> PmCt
pattern $mPmNotConCt :: forall {r}. PmCt -> (Id -> PmAltCon -> r) -> (Void# -> r) -> r
$bPmNotConCt :: Id -> PmAltCon -> PmCt
PmNotConCt x con       = PmTmCt (TmNotConCt x con)
pattern PmBotCt :: Id -> PmCt
pattern $mPmBotCt :: forall {r}. PmCt -> (Id -> r) -> (Void# -> r) -> r
$bPmBotCt :: Id -> PmCt
PmBotCt x              = PmTmCt (TmBotCt x)
pattern PmNotBotCt :: Id -> PmCt
pattern $mPmNotBotCt :: forall {r}. PmCt -> (Id -> r) -> (Void# -> r) -> r
$bPmNotBotCt :: Id -> PmCt
PmNotBotCt x           = PmTmCt (TmNotBotCt x)
{-# COMPLETE PmTyCt, PmVarCt, PmCoreCt, PmConCt, PmNotConCt, PmBotCt, PmNotBotCt #-}

instance Outputable PmCt where
  ppr :: PmCt -> SDoc
ppr (PmTyCt Type
pred_ty) = Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
pred_ty
  ppr (PmTmCt TmCt
tm_ct)   = TmCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr TmCt
tm_ct

-- | Adds new constraints to 'Delta' and returns 'Nothing' if that leads to a
-- contradiction.
addPmCts :: Delta -> PmCts -> DsM (Maybe Delta)
-- See Note [TmState invariants].
addPmCts :: Delta -> PmCts -> DsM (Maybe Delta)
addPmCts Delta
delta PmCts
cts = do
  let ([Type]
ty_cts, [TmCt]
tm_cts) = PmCts -> ([Type], [TmCt])
partitionTyTmCts PmCts
cts
  Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
delta (SatisfiabilityCheck -> DsM (Maybe Delta))
-> SatisfiabilityCheck -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ [SatisfiabilityCheck] -> SatisfiabilityCheck
forall a. Monoid a => [a] -> a
mconcat
    [ Bool -> Bag Type -> SatisfiabilityCheck
tyIsSatisfiable Bool
True ([Type] -> Bag Type
forall a. [a] -> Bag a
listToBag [Type]
ty_cts)
    , Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable ([TmCt] -> Bag TmCt
forall a. [a] -> Bag a
listToBag [TmCt]
tm_cts)
    ]

partitionTyTmCts :: PmCts -> ([TyCt], [TmCt])
partitionTyTmCts :: PmCts -> ([Type], [TmCt])
partitionTyTmCts = [Either Type TmCt] -> ([Type], [TmCt])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either Type TmCt] -> ([Type], [TmCt]))
-> (PmCts -> [Either Type TmCt]) -> PmCts -> ([Type], [TmCt])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PmCt -> Either Type TmCt) -> [PmCt] -> [Either Type TmCt]
forall a b. (a -> b) -> [a] -> [b]
map PmCt -> Either Type TmCt
to_either ([PmCt] -> [Either Type TmCt])
-> (PmCts -> [PmCt]) -> PmCts -> [Either Type TmCt]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmCts -> [PmCt]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
  where
    to_either :: PmCt -> Either Type TmCt
to_either (PmTyCt Type
pred_ty) = Type -> Either Type TmCt
forall a b. a -> Either a b
Left Type
pred_ty
    to_either (PmTmCt TmCt
tm_ct)   = TmCt -> Either Type TmCt
forall a b. b -> Either a b
Right TmCt
tm_ct

-- | Adds a single term constraint by dispatching to the various term oracle
-- functions.
addTmCt :: Delta -> TmCt -> MaybeT DsM Delta
addTmCt :: Delta -> TmCt -> MaybeT DsM Delta
addTmCt Delta
delta (TmVarCt Id
x Id
y)            = Delta -> Id -> Id -> MaybeT DsM Delta
addVarCt Delta
delta Id
x Id
y
addTmCt Delta
delta (TmCoreCt Id
x CoreExpr
e)           = Delta -> Id -> CoreExpr -> MaybeT DsM Delta
addCoreCt Delta
delta Id
x CoreExpr
e
addTmCt Delta
delta (TmConCt Id
x PmAltCon
con [Id]
tvs [Id]
args) = Delta -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT DsM Delta
addConCt Delta
delta Id
x PmAltCon
con [Id]
tvs [Id]
args
addTmCt Delta
delta (TmNotConCt Id
x PmAltCon
con)       = Delta -> Id -> PmAltCon -> MaybeT DsM Delta
addNotConCt Delta
delta Id
x PmAltCon
con
addTmCt Delta
delta (TmBotCt Id
x)              = Delta -> Id -> MaybeT DsM Delta
addBotCt Delta
delta Id
x
addTmCt Delta
delta (TmNotBotCt Id
x)           = Delta -> Id -> MaybeT DsM Delta
addNotBotCt Delta
delta Id
x

-- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@
-- surely diverges.
--
-- Only that's a lie, because we don't currently preserve the fact in 'Delta'
-- after we checked compatibility. See Note [Preserving TmBotCt]
addBotCt :: Delta -> Id -> MaybeT DsM Delta
addBotCt :: Delta -> Id -> MaybeT DsM Delta
addBotCt Delta
delta Id
x
  | Delta -> Id -> Bool
canDiverge Delta
delta Id
x = Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta
  | Bool
otherwise          = MaybeT DsM Delta
forall (m :: * -> *) a. MonadPlus m => m a
mzero

{- Note [Preserving TmBotCt]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Whenever we add a new constraint to 'Delta' via 'addTmCt', we want to check it
for compatibility with existing constraints in the modeled indert set and then
add it the constraint itself to the inert set.
For a 'TmBotCt' @x ~ ⊥@ we don't actually add it to the inert set after checking
it for compatibility with 'Delta'.
And that is fine in the context of the patter-match checking algorithm!
Whenever we add a 'TmBotCt' (we only do so for checking divergence of bang
patterns and strict constructor matches), we don't add any more constraints to
the inert set afterwards, so we don't need to preserve it.
-}

-- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't
-- take the shape of a 'PmAltCon' @K@ in the 'Delta' and return @Nothing@ if
-- that leads to a contradiction.
-- See Note [TmState invariants].
addNotConCt :: Delta -> Id -> PmAltCon -> MaybeT DsM Delta
addNotConCt :: Delta -> Id -> PmAltCon -> MaybeT DsM Delta
addNotConCt delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x PmAltCon
nalt = do
  vi :: VarInfo
vi@(VI Type
_ [(PmAltCon, [Id], [Id])]
pos PmAltConSet
neg PossibleMatches
pm) <- DsM VarInfo -> MaybeT DsM VarInfo
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x)
  -- 1. Bail out quickly when nalt contradicts a solution
  let contradicts :: PmAltCon -> (PmAltCon, b, c) -> Bool
contradicts PmAltCon
nalt (PmAltCon
cl, b
_tvs, c
_args) = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
cl PmAltCon
nalt PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Equal
  Bool -> MaybeT DsM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (((PmAltCon, [Id], [Id]) -> Bool)
-> [(PmAltCon, [Id], [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> (PmAltCon, [Id], [Id]) -> Bool
forall {b} {c}. PmAltCon -> (PmAltCon, b, c) -> Bool
contradicts PmAltCon
nalt) [(PmAltCon, [Id], [Id])]
pos))
  -- 2. Only record the new fact when it's not already implied by one of the
  -- solutions
  let implies :: PmAltCon -> (PmAltCon, b, c) -> Bool
implies PmAltCon
nalt (PmAltCon
cl, b
_tvs, c
_args) = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
cl PmAltCon
nalt PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Disjoint
  let neg' :: PmAltConSet
neg'
        | ((PmAltCon, [Id], [Id]) -> Bool)
-> [(PmAltCon, [Id], [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> (PmAltCon, [Id], [Id]) -> Bool
forall {b} {c}. PmAltCon -> (PmAltCon, b, c) -> Bool
implies PmAltCon
nalt) [(PmAltCon, [Id], [Id])]
pos = PmAltConSet
neg
        -- See Note [Completeness checking with required Thetas]
        | PmAltCon -> Bool
hasRequiredTheta PmAltCon
nalt  = PmAltConSet
neg
        | Bool
otherwise              = PmAltConSet -> PmAltCon -> PmAltConSet
extendPmAltConSet PmAltConSet
neg PmAltCon
nalt
  let vi_ext :: VarInfo
vi_ext = VarInfo
vi{ vi_neg :: PmAltConSet
vi_neg = PmAltConSet
neg' }
  -- 3. Make sure there's at least one other possible constructor
  VarInfo
vi' <- case PmAltCon
nalt of
    PmAltConLike ConLike
cl
      -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo) -> MaybeT DsM VarInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi_ext{ vi_cache :: PossibleMatches
vi_cache = ConLike -> PossibleMatches -> PossibleMatches
markMatched ConLike
cl PossibleMatches
pm })
    PmAltCon
_ -> VarInfo -> MaybeT DsM VarInfo
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi_ext
  Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env Id
x VarInfo
vi') CoreMap Id
reps }

hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta :: PmAltCon -> Bool
hasRequiredTheta (PmAltConLike ConLike
cl) = [Type] -> Bool
forall a. [a] -> Bool
notNull [Type]
req_theta
  where
    ([Id]
_,[Id]
_,[EqSpec]
_,[Type]
_,[Type]
req_theta,[Scaled Type]
_,Type
_) = ConLike
-> ([Id], [Id], [EqSpec], [Type], [Type], [Scaled Type], Type)
conLikeFullSig ConLike
cl
hasRequiredTheta PmAltCon
_                 = Bool
False

{- Note [Completeness checking with required Thetas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the situation in #11224

    import Text.Read (readMaybe)
    pattern PRead :: Read a => () => a -> String
    pattern PRead x <- (readMaybe -> Just x)
    f :: String -> Int
    f (PRead x)  = x
    f (PRead xs) = length xs
    f _          = 0

Is the first match exhaustive on the PRead synonym? Should the second line thus
deemed redundant? The answer is, of course, No! The required theta is like a
hidden parameter which must be supplied at the pattern match site, so PRead
is much more like a view pattern (where behavior depends on the particular value
passed in).
The simple solution here is to forget in 'addNotConCt' that we matched
on synonyms with a required Theta like @PRead@, so that subsequent matches on
the same constructor are never flagged as redundant. The consequence is that
we no longer detect the actually redundant match in

    g :: String -> Int
    g (PRead x) = x
    g (PRead y) = y -- redundant!
    g _         = 0

But that's a small price to pay, compared to the proper solution here involving
storing required arguments along with the PmAltConLike in 'vi_neg'.
-}

-- | Guess the universal argument types of a ConLike from an instantiation of
-- its result type. Rather easy for DataCons, but not so much for PatSynCons.
-- See Note [Pattern synonym result type] in "GHC.Core.PatSyn".
guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy FamInstEnvs
env Type
res_ty (RealDataCon DataCon
_) = do
  (TyCon
tc, [Type]
tc_args) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
res_ty
  -- Consider data families: In case of a DataCon, we need to translate to
  -- the representation TyCon. For PatSyns, they are relative to the data
  -- family TyCon, so we don't need to translate them.
  let (TyCon
_, [Type]
tc_args', Coercion
_) = FamInstEnvs -> TyCon -> [Type] -> (TyCon, [Type], Coercion)
tcLookupDataFamInst FamInstEnvs
env TyCon
tc [Type]
tc_args
  [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
tc_args'
guessConLikeUnivTyArgsFromResTy FamInstEnvs
_   Type
res_ty (PatSynCon PatSyn
ps)  = do
  -- We are successful if we managed to instantiate *every* univ_tv of con.
  -- This is difficult and bound to fail in some cases, see
  -- Note [Pattern synonym result type] in GHC.Core.PatSyn. So we just try our best
  -- here and be sure to return an instantiation when we can substitute every
  -- universally quantified type variable.
  -- We *could* instantiate all the other univ_tvs just to fresh variables, I
  -- suppose, but that means we get weird field types for which we don't know
  -- anything. So we prefer to keep it simple here.
  let ([Id]
univ_tvs,[Type]
_,[Id]
_,[Type]
_,[Scaled Type]
_,Type
con_res_ty) = PatSyn -> ([Id], [Type], [Id], [Type], [Scaled Type], Type)
patSynSig PatSyn
ps
  TCvSubst
subst <- Type -> Type -> Maybe TCvSubst
tcMatchTy Type
con_res_ty Type
res_ty
  (Id -> Maybe Type) -> [Id] -> Maybe [Type]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TCvSubst -> Id -> Maybe Type
lookupTyVar TCvSubst
subst) [Id]
univ_tvs

-- | Adds the constraint @x ~/ ⊥@ to 'Delta'.
--
-- But doesn't really commit to upholding that constraint in the future. This
-- will be rectified in a follow-up patch. The status quo should work good
-- enough for now.
addNotBotCt :: Delta -> Id -> MaybeT DsM Delta
addNotBotCt :: Delta -> Id -> MaybeT DsM Delta
addNotBotCt delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x = do
  VarInfo
vi  <- DsM VarInfo -> MaybeT DsM VarInfo
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM VarInfo -> MaybeT DsM VarInfo)
-> DsM VarInfo -> MaybeT DsM VarInfo
forall a b. (a -> b) -> a -> b
$ Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x
  VarInfo
vi' <- IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo) -> MaybeT DsM VarInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
 -> MaybeT DsM VarInfo)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
-> MaybeT DsM VarInfo
forall a b. (a -> b) -> a -> b
$ Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi
  -- vi' has probably constructed and then thinned out some PossibleMatches.
  -- We want to cache that work
  Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env Id
x VarInfo
vi') CoreMap Id
reps}

ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo)
   -- Returns (Just vi) if at least one member of each ConLike in the COMPLETE
   -- set satisfies the oracle
   --
   -- Internally uses and updates the ConLikeSets in vi_cache.
   --
   -- NB: Does /not/ filter each ConLikeSet with the oracle; members may
   --     remain that do not statisfy it.  This lazy approach just
   --     avoids doing unnecessary work.
ensureInhabited :: Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi = (PossibleMatches -> VarInfo)
-> Maybe PossibleMatches -> Maybe VarInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VarInfo -> PossibleMatches -> VarInfo
set_cache VarInfo
vi) (Maybe PossibleMatches -> Maybe VarInfo)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
test (VarInfo -> PossibleMatches
vi_cache VarInfo
vi) -- This would be much less tedious with lenses
  where
    set_cache :: VarInfo -> PossibleMatches -> VarInfo
set_cache VarInfo
vi PossibleMatches
cache = VarInfo
vi { vi_cache :: PossibleMatches
vi_cache = PossibleMatches
cache }

    test :: PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
test PossibleMatches
NoPM    = Maybe PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PossibleMatches -> Maybe PossibleMatches
forall a. a -> Maybe a
Just PossibleMatches
NoPM)
    test (PM NonEmpty ConLikeSet
ms) = MaybeT DsM PossibleMatches
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe PossibleMatches)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (NonEmpty ConLikeSet -> PossibleMatches
PM (NonEmpty ConLikeSet -> PossibleMatches)
-> MaybeT DsM (NonEmpty ConLikeSet) -> MaybeT DsM PossibleMatches
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ConLikeSet -> MaybeT DsM ConLikeSet)
-> NonEmpty ConLikeSet -> MaybeT DsM (NonEmpty ConLikeSet)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ConLikeSet -> MaybeT DsM ConLikeSet
one_set NonEmpty ConLikeSet
ms)

    one_set :: ConLikeSet -> MaybeT DsM ConLikeSet
one_set ConLikeSet
cs = ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
find_one_inh ConLikeSet
cs (ConLikeSet -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList ConLikeSet
cs)

    find_one_inh :: ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
    -- (find_one_inh cs cls) iterates over cls, deleting from cs
    -- any uninhabited elements of cls.  Stop (returning Just cs)
    -- when you see an inhabited element; return Nothing if all
    -- are uninhabited
    find_one_inh :: ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
find_one_inh ConLikeSet
_  [] = MaybeT DsM ConLikeSet
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    find_one_inh ConLikeSet
cs (ConLike
con:[ConLike]
cons) = IOEnv (Env DsGblEnv DsLclEnv) Bool -> MaybeT DsM Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (ConLike -> IOEnv (Env DsGblEnv DsLclEnv) Bool
inh_test ConLike
con) MaybeT DsM Bool
-> (Bool -> MaybeT DsM ConLikeSet) -> MaybeT DsM ConLikeSet
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True  -> ConLikeSet -> MaybeT DsM ConLikeSet
forall (f :: * -> *) a. Applicative f => a -> f a
pure ConLikeSet
cs
      Bool
False -> ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet
find_one_inh (ConLikeSet -> ConLike -> ConLikeSet
forall a. Uniquable a => UniqDSet a -> a -> UniqDSet a
delOneFromUniqDSet ConLikeSet
cs ConLike
con) [ConLike]
cons

    inh_test :: ConLike -> DsM Bool
    -- @inh_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly
    -- be of form @K _ _ _@. Returning True is always sound.
    --
    -- It's like 'DataCon.dataConCannotMatch', but more clever because it takes
    -- the facts in Delta into account.
    inh_test :: ConLike -> IOEnv (Env DsGblEnv DsLclEnv) Bool
inh_test ConLike
con = do
      FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
      case FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy FamInstEnvs
env (VarInfo -> Type
vi_ty VarInfo
vi) ConLike
con of
        Maybe [Type]
Nothing -> Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True -- be conservative about this
        Just [Type]
arg_tys -> do
          ([Id]
_tvs, [Id]
_vars, Bag Type
ty_cs, [Type]
strict_arg_tys) <- [Type] -> ConLike -> DsM ([Id], [Id], Bag Type, [Type])
mkOneConFull [Type]
arg_tys ConLike
con
          String -> SDoc -> DsM ()
tracePm String
"inh_test" (ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
con SDoc -> SDoc -> SDoc
$$ Bag Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Type
ty_cs)
          -- No need to run the term oracle compared to pmIsSatisfiable
          (Maybe Delta -> Bool)
-> DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe Delta -> Bool
forall a. Maybe a -> Bool
isJust (DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> (SatisfiabilityCheck -> DsM (Maybe Delta))
-> SatisfiabilityCheck
-> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
delta (SatisfiabilityCheck -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> SatisfiabilityCheck -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall a b. (a -> b) -> a -> b
$ [SatisfiabilityCheck] -> SatisfiabilityCheck
forall a. Monoid a => [a] -> a
mconcat
            -- Important to pass False to tyIsSatisfiable here, so that we won't
            -- recursively call ensureAllPossibleMatchesInhabited, leading to an
            -- endless recursion.
            [ Bool -> Bag Type -> SatisfiabilityCheck
tyIsSatisfiable Bool
False Bag Type
ty_cs
            , RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
initRecTc [Type]
strict_arg_tys
            ]

-- | Checks if every 'VarInfo' in the term oracle has still an inhabited
-- 'vi_cache', considering the current type information in 'Delta'.
-- This check is necessary after having matched on a GADT con to weed out
-- impossible matches.
ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta)
ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta)
ensureAllPossibleMatchesInhabited delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps }
  = MaybeT DsM Delta -> DsM (Maybe Delta)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (Delta -> SharedDIdEnv VarInfo -> Delta
set_tm_cs_env Delta
delta (SharedDIdEnv VarInfo -> Delta)
-> MaybeT DsM (SharedDIdEnv VarInfo) -> MaybeT DsM Delta
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarInfo -> MaybeT DsM VarInfo)
-> SharedDIdEnv VarInfo -> MaybeT DsM (SharedDIdEnv VarInfo)
forall a b (f :: * -> *).
Applicative f =>
(a -> f b) -> SharedDIdEnv a -> f (SharedDIdEnv b)
traverseSDIE VarInfo -> MaybeT DsM VarInfo
go SharedDIdEnv VarInfo
env)
  where
    set_tm_cs_env :: Delta -> SharedDIdEnv VarInfo -> Delta
set_tm_cs_env Delta
delta SharedDIdEnv VarInfo
env = Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps }
    go :: VarInfo -> MaybeT DsM VarInfo
go VarInfo
vi = IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo) -> MaybeT DsM VarInfo
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Delta -> VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe VarInfo)
ensureInhabited Delta
delta VarInfo
vi)

--------------------------------------
-- * Term oracle unification procedure

-- | Adds a @x ~ y@ constraint by trying to unify two 'Id's and record the
-- gained knowledge in 'Delta'.
--
-- Returns @Nothing@ when there's a contradiction. Returns @Just delta@
-- when the constraint was compatible with prior facts, in which case @delta@
-- has integrated the knowledge from the equality constraint.
--
-- See Note [TmState invariants].
addVarCt :: Delta -> Id -> Id -> MaybeT DsM Delta
addVarCt :: Delta -> Id -> Id -> MaybeT DsM Delta
addVarCt delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
_ } Id
x Id
y
  -- It's important that we never @equate@ two variables of the same equivalence
  -- class, otherwise we might get cyclic substitutions.
  -- Cf. 'extendSubstAndSolve' and
  -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@.
  | SharedDIdEnv VarInfo -> Id -> Id -> Bool
forall a. SharedDIdEnv a -> Id -> Id -> Bool
sameRepresentativeSDIE SharedDIdEnv VarInfo
env Id
x Id
y = Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta
  | Bool
otherwise                      = Delta -> Id -> Id -> MaybeT DsM Delta
equate Delta
delta Id
x Id
y

-- | @equate ts@(TmSt env) x y@ merges the equivalence classes of @x@ and @y@ by
-- adding an indirection to the environment.
-- Makes sure that the positive and negative facts of @x@ and @y@ are
-- compatible.
-- Preconditions: @not (sameRepresentativeSDIE env x y)@
--
-- See Note [TmState invariants].
equate :: Delta -> Id -> Id -> MaybeT DsM Delta
equate :: Delta -> Id -> Id -> MaybeT DsM Delta
equate delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x Id
y
  = ASSERT( not (sameRepresentativeSDIE env x y) )
    case (SharedDIdEnv VarInfo -> Id -> Maybe VarInfo
forall a. SharedDIdEnv a -> Id -> Maybe a
lookupSDIE SharedDIdEnv VarInfo
env Id
x, SharedDIdEnv VarInfo -> Id -> Maybe VarInfo
forall a. SharedDIdEnv a -> Id -> Maybe a
lookupSDIE SharedDIdEnv VarInfo
env Id
y) of
      (Maybe VarInfo
Nothing, Maybe VarInfo
_) -> Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> Id -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE SharedDIdEnv VarInfo
env Id
x Id
y) CoreMap Id
reps })
      (Maybe VarInfo
_, Maybe VarInfo
Nothing) -> Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> Id -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE SharedDIdEnv VarInfo
env Id
y Id
x) CoreMap Id
reps })
      -- Merge the info we have for x into the info for y
      (Just VarInfo
vi_x, Just VarInfo
vi_y) -> do
        -- This assert will probably trigger at some point...
        -- We should decide how to break the tie
        MASSERT2( vi_ty vi_x `eqType` vi_ty vi_y, text "Not same type" )
        -- First assume that x and y are in the same equivalence class
        let env_ind :: SharedDIdEnv VarInfo
env_ind = SharedDIdEnv VarInfo -> Id -> Id -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> Id -> SharedDIdEnv a
setIndirectSDIE SharedDIdEnv VarInfo
env Id
x Id
y
        -- Then sum up the refinement counters
        let env_refs :: SharedDIdEnv VarInfo
env_refs = SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env_ind Id
y VarInfo
vi_y
        let delta_refs :: Delta
delta_refs = Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt SharedDIdEnv VarInfo
env_refs CoreMap Id
reps }
        -- and then gradually merge every positive fact we have on x into y
        let add_fact :: Delta -> (PmAltCon, [Id], [Id]) -> MaybeT DsM Delta
add_fact Delta
delta (PmAltCon
cl, [Id]
tvs, [Id]
args) = Delta -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT DsM Delta
addConCt Delta
delta Id
y PmAltCon
cl [Id]
tvs [Id]
args
        Delta
delta_pos <- (Delta -> (PmAltCon, [Id], [Id]) -> MaybeT DsM Delta)
-> Delta -> [(PmAltCon, [Id], [Id])] -> MaybeT DsM Delta
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Delta -> (PmAltCon, [Id], [Id]) -> MaybeT DsM Delta
add_fact Delta
delta_refs (VarInfo -> [(PmAltCon, [Id], [Id])]
vi_pos VarInfo
vi_x)
        -- Do the same for negative info
        let add_refut :: Delta -> PmAltCon -> MaybeT DsM Delta
add_refut Delta
delta PmAltCon
nalt = Delta -> Id -> PmAltCon -> MaybeT DsM Delta
addNotConCt Delta
delta Id
y PmAltCon
nalt
        Delta
delta_neg <- (Delta -> PmAltCon -> MaybeT DsM Delta)
-> Delta -> [PmAltCon] -> MaybeT DsM Delta
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Delta -> PmAltCon -> MaybeT DsM Delta
add_refut Delta
delta_pos (PmAltConSet -> [PmAltCon]
pmAltConSetElems (VarInfo -> PmAltConSet
vi_neg VarInfo
vi_x))
        -- vi_cache will be updated in addNotConCt, so we are good to
        -- go!
        Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta_neg

-- | Add a @x ~ K tvs args ts@ constraint.
-- @addConCt x K tvs args ts@ extends the substitution with a solution
-- @x :-> (K, tvs, args)@ if compatible with the negative and positive info we
-- have on @x@, reject (@Nothing@) otherwise.
--
-- See Note [TmState invariants].
addConCt :: Delta -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Delta
addConCt :: Delta -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT DsM Delta
addConCt delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = TmSt SharedDIdEnv VarInfo
env CoreMap Id
reps } Id
x PmAltCon
alt [Id]
tvs [Id]
args = do
  VI Type
ty [(PmAltCon, [Id], [Id])]
pos PmAltConSet
neg PossibleMatches
cache <- DsM VarInfo -> MaybeT DsM VarInfo
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x)
  -- First try to refute with a negative fact
  Bool -> MaybeT DsM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (PmAltCon -> PmAltConSet -> Bool
elemPmAltConSet PmAltCon
alt PmAltConSet
neg))
  -- Then see if any of the other solutions (remember: each of them is an
  -- additional refinement of the possible values x could take) indicate a
  -- contradiction
  Bool -> MaybeT DsM ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (((PmAltCon, [Id], [Id]) -> Bool)
-> [(PmAltCon, [Id], [Id])] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
/= PmEquality
Disjoint) (PmEquality -> Bool)
-> ((PmAltCon, [Id], [Id]) -> PmEquality)
-> (PmAltCon, [Id], [Id])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt (PmAltCon -> PmEquality)
-> ((PmAltCon, [Id], [Id]) -> PmAltCon)
-> (PmAltCon, [Id], [Id])
-> PmEquality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PmAltCon, [Id], [Id]) -> PmAltCon
forall a b c. (a, b, c) -> a
fstOf3) [(PmAltCon, [Id], [Id])]
pos)
  -- Now we should be good! Add (alt, tvs, args) as a possible solution, or
  -- refine an existing one
  case ((PmAltCon, [Id], [Id]) -> Bool)
-> [(PmAltCon, [Id], [Id])] -> Maybe (PmAltCon, [Id], [Id])
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Equal) (PmEquality -> Bool)
-> ((PmAltCon, [Id], [Id]) -> PmEquality)
-> (PmAltCon, [Id], [Id])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt (PmAltCon -> PmEquality)
-> ((PmAltCon, [Id], [Id]) -> PmAltCon)
-> (PmAltCon, [Id], [Id])
-> PmEquality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PmAltCon, [Id], [Id]) -> PmAltCon
forall a b c. (a, b, c) -> a
fstOf3) [(PmAltCon, [Id], [Id])]
pos of
    Just (PmAltCon
_con, [Id]
other_tvs, [Id]
other_args) -> do
      -- We must unify existentially bound ty vars and arguments!
      let ty_cts :: [PmCt]
ty_cts = [Type] -> [Type] -> [PmCt]
equateTys ((Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
tvs) ((Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
other_tvs)
      Bool -> MaybeT DsM () -> MaybeT DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
other_args) (MaybeT DsM () -> MaybeT DsM ()) -> MaybeT DsM () -> MaybeT DsM ()
forall a b. (a -> b) -> a -> b
$
        DsM () -> MaybeT DsM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM () -> MaybeT DsM ()) -> DsM () -> MaybeT DsM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> DsM ()
tracePm String
"error" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
<+> PmAltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltCon
alt SDoc -> SDoc -> SDoc
<+> [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
args SDoc -> SDoc -> SDoc
<+> [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
other_args)
      let tm_cts :: [PmCt]
tm_cts = String -> (Id -> Id -> PmCt) -> [Id] -> [Id] -> [PmCt]
forall a b c. String -> (a -> b -> c) -> [a] -> [b] -> [c]
zipWithEqual String
"addConCt" Id -> Id -> PmCt
PmVarCt [Id]
args [Id]
other_args
      DsM (Maybe Delta) -> MaybeT DsM Delta
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (DsM (Maybe Delta) -> MaybeT DsM Delta)
-> DsM (Maybe Delta) -> MaybeT DsM Delta
forall a b. (a -> b) -> a -> b
$ Delta -> PmCts -> DsM (Maybe Delta)
addPmCts Delta
delta ([PmCt] -> PmCts
forall a. [a] -> Bag a
listToBag [PmCt]
ty_cts PmCts -> PmCts -> PmCts
forall a. Bag a -> Bag a -> Bag a
`unionBags` [PmCt] -> PmCts
forall a. [a] -> Bag a
listToBag [PmCt]
tm_cts)
    Maybe (PmAltCon, [Id], [Id])
Nothing -> do
      let pos' :: [(PmAltCon, [Id], [Id])]
pos' = (PmAltCon
alt, [Id]
tvs, [Id]
args)(PmAltCon, [Id], [Id])
-> [(PmAltCon, [Id], [Id])] -> [(PmAltCon, [Id], [Id])]
forall a. a -> [a] -> [a]
:[(PmAltCon, [Id], [Id])]
pos
      Delta -> MaybeT DsM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure Delta
delta{ delta_tm_st :: TmState
delta_tm_st = SharedDIdEnv VarInfo -> CoreMap Id -> TmState
TmSt (SharedDIdEnv VarInfo -> Id -> VarInfo -> SharedDIdEnv VarInfo
forall a. SharedDIdEnv a -> Id -> a -> SharedDIdEnv a
setEntrySDIE SharedDIdEnv VarInfo
env Id
x (Type
-> [(PmAltCon, [Id], [Id])]
-> PmAltConSet
-> PossibleMatches
-> VarInfo
VI Type
ty [(PmAltCon, [Id], [Id])]
pos' PmAltConSet
neg PossibleMatches
cache)) CoreMap Id
reps}

equateTys :: [Type] -> [Type] -> [PmCt]
equateTys :: [Type] -> [Type] -> [PmCt]
equateTys [Type]
ts [Type]
us =
  [ Type -> PmCt
PmTyCt (Type -> Type -> Type
mkPrimEqPred Type
t Type
u)
  | (Type
t, Type
u) <- String -> [Type] -> [Type] -> [(Type, Type)]
forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"equateTys" [Type]
ts [Type]
us
  -- The following line filters out trivial Refl constraints, so that we don't
  -- need to initialise the type oracle that often
  , Bool -> Bool
not (Type -> Type -> Bool
eqType Type
t Type
u)
  ]

----------------------------------------
-- * Enumerating inhabitation candidates

-- | Information about a conlike that is relevant to coverage checking.
-- It is called an \"inhabitation candidate\" since it is a value which may
-- possibly inhabit some type, but only if its term constraints ('ic_tm_cs')
-- and type constraints ('ic_ty_cs') are permitting, and if all of its strict
-- argument types ('ic_strict_arg_tys') are inhabitable.
-- See @Note [Strict argument type constraints]@.
data InhabitationCandidate =
  InhabitationCandidate
  { InhabitationCandidate -> PmCts
ic_cs             :: PmCts
  , InhabitationCandidate -> [Type]
ic_strict_arg_tys :: [Type]
  }

instance Outputable InhabitationCandidate where
  ppr :: InhabitationCandidate -> SDoc
ppr (InhabitationCandidate PmCts
cs [Type]
strict_arg_tys) =
    String -> SDoc
text String
"InhabitationCandidate" SDoc -> SDoc -> SDoc
<+>
      [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"ic_cs             =" SDoc -> SDoc -> SDoc
<+> PmCts -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmCts
cs
           , String -> SDoc
text String
"ic_strict_arg_tys =" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
strict_arg_tys ]

mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
-- Precondition: idType x is a TyConApp, so that tyConAppArgs in here is safe.
mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate
mkInhabitationCandidate Id
x DataCon
dc = do
  let cl :: ConLike
cl = DataCon -> ConLike
RealDataCon DataCon
dc
  let tc_args :: [Type]
tc_args = Type -> [Type]
tyConAppArgs (Id -> Type
idType Id
x)
  ([Id]
ty_vars, [Id]
arg_vars, Bag Type
ty_cs, [Type]
strict_arg_tys) <- [Type] -> ConLike -> DsM ([Id], [Id], Bag Type, [Type])
mkOneConFull [Type]
tc_args ConLike
cl
  InhabitationCandidate -> DsM InhabitationCandidate
forall (f :: * -> *) a. Applicative f => a -> f a
pure InhabitationCandidate :: PmCts -> [Type] -> InhabitationCandidate
InhabitationCandidate
        { ic_cs :: PmCts
ic_cs = Type -> PmCt
PmTyCt (Type -> PmCt) -> Bag Type -> PmCts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bag Type
ty_cs PmCts -> PmCt -> PmCts
forall a. Bag a -> a -> Bag a
`snocBag` Id -> PmAltCon -> [Id] -> [Id] -> PmCt
PmConCt Id
x (ConLike -> PmAltCon
PmAltConLike ConLike
cl) [Id]
ty_vars [Id]
arg_vars
        , ic_strict_arg_tys :: [Type]
ic_strict_arg_tys = [Type]
strict_arg_tys
        }

-- | Generate all 'InhabitationCandidate's for a given type. The result is
-- either @'Left' ty@, if the type cannot be reduced to a closed algebraic type
-- (or if it's one trivially inhabited, like 'Int'), or @'Right' candidates@,
-- if it can. In this case, the candidates are the signature of the tycon, each
-- one accompanied by the term- and type- constraints it gives rise to.
-- See also Note [Checking EmptyCase Expressions]
inhabitationCandidates :: Delta -> Type
                       -> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
inhabitationCandidates :: Delta
-> Type -> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
inhabitationCandidates MkDelta{ delta_ty_st :: Delta -> TyState
delta_ty_st = TyState
ty_st } Type
ty = do
  TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty DsM TopNormaliseTypeResult
-> (TopNormaliseTypeResult
    -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])))
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    NoChange Type
_                    -> Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
ty     Type
ty      []
    NormalisedByConstraints Type
ty'   -> Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
ty'    Type
ty'     []
    HadRedexes Type
src_ty [(Type, DataCon, Type)]
dcs Type
core_ty -> Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
src_ty Type
core_ty [(Type, DataCon, Type)]
dcs
  where
    build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, PmCt)
    build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, PmCt)
build_newtype (Type
ty, DataCon
dc, Type
_arg_ty) Id
x = do
      -- ty is the type of @dc x@. It's a @dataConTyCon dc@ application.
      Id
y <- Type -> DsM Id
mkPmId Type
ty
      -- Newtypes don't have existentials (yet?!), so passing an empty list as
      -- ex_tvs.
      (Id, PmCt) -> DsM (Id, PmCt)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
y, Id -> PmAltCon -> [Id] -> [Id] -> PmCt
PmConCt Id
y (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [] [Id
x])

    build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt])
    build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt])
build_newtypes Id
x = ((Type, DataCon, Type) -> (Id, [PmCt]) -> DsM (Id, [PmCt]))
-> (Id, [PmCt]) -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt])
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM (\(Type, DataCon, Type)
dc (Id
x, [PmCt]
cts) -> (Type, DataCon, Type) -> Id -> [PmCt] -> DsM (Id, [PmCt])
go (Type, DataCon, Type)
dc Id
x [PmCt]
cts) (Id
x, [])
      where
        go :: (Type, DataCon, Type) -> Id -> [PmCt] -> DsM (Id, [PmCt])
go (Type, DataCon, Type)
dc Id
x [PmCt]
cts = (PmCt -> [PmCt]) -> (Id, PmCt) -> (Id, [PmCt])
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (PmCt -> [PmCt] -> [PmCt]
forall a. a -> [a] -> [a]
:[PmCt]
cts) ((Id, PmCt) -> (Id, [PmCt])) -> DsM (Id, PmCt) -> DsM (Id, [PmCt])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type, DataCon, Type) -> Id -> DsM (Id, PmCt)
build_newtype (Type, DataCon, Type)
dc Id
x

    -- Inhabitation candidates, using the result of pmTopNormaliseType
    alts_to_check :: Type -> Type -> [(Type, DataCon, Type)]
                  -> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
    alts_to_check :: Type
-> Type
-> [(Type, DataCon, Type)]
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
alts_to_check Type
src_ty Type
core_ty [(Type, DataCon, Type)]
dcs = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
core_ty of
      Just (TyCon
tc, [Type]
_)
        |  TyCon -> Bool
isTyConTriviallyInhabited TyCon
tc
        -> case [(Type, DataCon, Type)]
dcs of
             []    -> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. a -> Either a b
Left Type
src_ty)
             ((Type, DataCon, Type)
_:[(Type, DataCon, Type)]
_) -> do Id
inner <- Type -> DsM Id
mkPmId Type
core_ty
                         (Id
outer, [PmCt]
new_tm_cts) <- Id -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt])
build_newtypes Id
inner [(Type, DataCon, Type)]
dcs
                         Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Type (TyCon, Id, [InhabitationCandidate])
 -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])))
-> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall a b. (a -> b) -> a -> b
$ (TyCon, Id, [InhabitationCandidate])
-> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. b -> Either a b
Right (TyCon
tc, Id
outer, [InhabitationCandidate :: PmCts -> [Type] -> InhabitationCandidate
InhabitationCandidate
                           { ic_cs :: PmCts
ic_cs = [PmCt] -> PmCts
forall a. [a] -> Bag a
listToBag [PmCt]
new_tm_cts
                           , ic_strict_arg_tys :: [Type]
ic_strict_arg_tys = [] }])

        |  Type -> Bool
pmIsClosedType Type
core_ty Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isAbstractTyCon TyCon
tc)
           -- Don't consider abstract tycons since we don't know what their
           -- constructors are, which makes the results of coverage checking
           -- them extremely misleading.
        -> do
             Id
inner <- Type -> DsM Id
mkPmId Type
core_ty -- it would be wrong to unify inner
             [InhabitationCandidate]
alts <- (DataCon -> DsM InhabitationCandidate)
-> [DataCon]
-> IOEnv (Env DsGblEnv DsLclEnv) [InhabitationCandidate]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Id -> DataCon -> DsM InhabitationCandidate
mkInhabitationCandidate Id
inner) (TyCon -> [DataCon]
tyConDataCons TyCon
tc)
             (Id
outer, [PmCt]
new_cts) <- Id -> [(Type, DataCon, Type)] -> DsM (Id, [PmCt])
build_newtypes Id
inner [(Type, DataCon, Type)]
dcs
             let wrap_dcs :: InhabitationCandidate -> InhabitationCandidate
wrap_dcs InhabitationCandidate
alt = InhabitationCandidate
alt{ ic_cs :: PmCts
ic_cs = [PmCt] -> PmCts
forall a. [a] -> Bag a
listToBag [PmCt]
new_cts PmCts -> PmCts -> PmCts
forall a. Bag a -> Bag a -> Bag a
`unionBags` InhabitationCandidate -> PmCts
ic_cs InhabitationCandidate
alt}
             Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Type (TyCon, Id, [InhabitationCandidate])
 -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])))
-> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall a b. (a -> b) -> a -> b
$ (TyCon, Id, [InhabitationCandidate])
-> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. b -> Either a b
Right (TyCon
tc, Id
outer, (InhabitationCandidate -> InhabitationCandidate)
-> [InhabitationCandidate] -> [InhabitationCandidate]
forall a b. (a -> b) -> [a] -> [b]
map InhabitationCandidate -> InhabitationCandidate
wrap_dcs [InhabitationCandidate]
alts)
      -- For other types conservatively assume that they are inhabited.
      Maybe (TyCon, [Type])
_other -> Either Type (TyCon, Id, [InhabitationCandidate])
-> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either Type (TyCon, Id, [InhabitationCandidate])
forall a b. a -> Either a b
Left Type
src_ty)

-- | All these types are trivially inhabited
triviallyInhabitedTyCons :: UniqSet TyCon
triviallyInhabitedTyCons :: UniqSet TyCon
triviallyInhabitedTyCons = [TyCon] -> UniqSet TyCon
forall a. Uniquable a => [a] -> UniqSet a
mkUniqSet [
    TyCon
charTyCon, TyCon
doubleTyCon, TyCon
floatTyCon, TyCon
intTyCon, TyCon
wordTyCon, TyCon
word8TyCon
  ]

isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited TyCon
tc = TyCon -> UniqSet TyCon -> Bool
forall a. Uniquable a => a -> UniqSet a -> Bool
elementOfUniqSet TyCon
tc UniqSet TyCon
triviallyInhabitedTyCons

----------------------------
-- * Detecting vacuous types

{- Note [Checking EmptyCase Expressions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Empty case expressions are strict on the scrutinee. That is, `case x of {}`
will force argument `x`. Hence, `checkMatches` is not sufficient for checking
empty cases, because it assumes that the match is not strict (which is true
for all other cases, apart from EmptyCase). This gave rise to #10746. Instead,
we do the following:

1. We normalise the outermost type family redex, data family redex or newtype,
   using pmTopNormaliseType (in "GHC.Core.FamInstEnv"). This computes 3
   things:
   (a) A normalised type src_ty, which is equal to the type of the scrutinee in
       source Haskell (does not normalise newtypes or data families)
   (b) The actual normalised type core_ty, which coincides with the result
       topNormaliseType_maybe. This type is not necessarily equal to the input
       type in source Haskell. And this is precicely the reason we compute (a)
       and (c): the reasoning happens with the underlying types, but both the
       patterns and types we print should respect newtypes and also show the
       family type constructors and not the representation constructors.

   (c) A list of all newtype data constructors dcs, each one corresponding to a
       newtype rewrite performed in (b).

   For an example see also Note [Type normalisation]
   in "GHC.Core.FamInstEnv".

2. Function Check.checkEmptyCase' performs the check:
   - If core_ty is not an algebraic type, then we cannot check for
     inhabitation, so we emit (_ :: src_ty) as missing, conservatively assuming
     that the type is inhabited.
   - If core_ty is an algebraic type, then we unfold the scrutinee to all
     possible constructor patterns, using inhabitationCandidates, and then
     check each one for constraint satisfiability, same as we do for normal
     pattern match checking.
-}

-- | A 'SatisfiabilityCheck' based on "NonVoid ty" constraints, e.g. Will
-- check if the @strict_arg_tys@ are actually all inhabited.
-- Returns the old 'Delta' if all the types are non-void according to 'Delta'.
tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
rec_env [Type]
strict_arg_tys = (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
SC ((Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck)
-> (Delta -> DsM (Maybe Delta)) -> SatisfiabilityCheck
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> do
  Bool
all_non_void <- RecTcChecker
-> Delta -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
checkAllNonVoid RecTcChecker
rec_env Delta
delta [Type]
strict_arg_tys
  -- Check if each strict argument type is inhabitable
  Maybe Delta -> DsM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Delta -> DsM (Maybe Delta))
-> Maybe Delta -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ if Bool
all_non_void
            then Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta
            else Maybe Delta
forall a. Maybe a
Nothing

-- | Implements two performance optimizations, as described in
-- @Note [Strict argument type constraints]@.
checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> DsM Bool
checkAllNonVoid :: RecTcChecker
-> Delta -> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
checkAllNonVoid RecTcChecker
rec_ts Delta
amb_cs [Type]
strict_arg_tys = do
  let definitely_inhabited :: Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitely_inhabited = TyState -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitelyInhabitedType (Delta -> TyState
delta_ty_st Delta
amb_cs)
  [Type]
tys_to_check <- (Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [Type]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterOutM Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitely_inhabited [Type]
strict_arg_tys
  -- See Note [Fuel for the inhabitation test]
  let rec_max_bound :: Int
rec_max_bound | [Type]
tys_to_check [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
1
                    = Int
1
                    | Bool
otherwise
                    = Int
3
      rec_ts' :: RecTcChecker
rec_ts' = Int -> RecTcChecker -> RecTcChecker
setRecTcMaxBound Int
rec_max_bound RecTcChecker
rec_ts
  (Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM (RecTcChecker -> Delta -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
nonVoid RecTcChecker
rec_ts' Delta
amb_cs) [Type]
tys_to_check

-- | Checks if a strict argument type of a conlike is inhabitable by a
-- terminating value (i.e, an 'InhabitationCandidate').
-- See @Note [Strict argument type constraints]@.
nonVoid
  :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit.
  -> Delta        -- ^ The ambient term/type constraints (known to be
                  --   satisfiable).
  -> Type         -- ^ The strict argument type.
  -> DsM Bool     -- ^ 'True' if the strict argument type might be inhabited by
                  --   a terminating value (i.e., an 'InhabitationCandidate').
                  --   'False' if it is definitely uninhabitable by anything
                  --   (except bottom).
nonVoid :: RecTcChecker -> Delta -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
nonVoid RecTcChecker
rec_ts Delta
amb_cs Type
strict_arg_ty = do
  Either Type (TyCon, Id, [InhabitationCandidate])
mb_cands <- Delta
-> Type -> DsM (Either Type (TyCon, Id, [InhabitationCandidate]))
inhabitationCandidates Delta
amb_cs Type
strict_arg_ty
  case Either Type (TyCon, Id, [InhabitationCandidate])
mb_cands of
    Right (TyCon
tc, Id
_, [InhabitationCandidate]
cands)
      -- See Note [Fuel for the inhabitation test]
      |  Just RecTcChecker
rec_ts' <- RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_ts TyCon
tc
      -> (InhabitationCandidate -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> [InhabitationCandidate] -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM (RecTcChecker
-> Delta
-> InhabitationCandidate
-> IOEnv (Env DsGblEnv DsLclEnv) Bool
cand_is_inhabitable RecTcChecker
rec_ts' Delta
amb_cs) [InhabitationCandidate]
cands
           -- A strict argument type is inhabitable by a terminating value if
           -- at least one InhabitationCandidate is inhabitable.
    Either Type (TyCon, Id, [InhabitationCandidate])
_ -> Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
           -- Either the type is trivially inhabited or we have exceeded the
           -- recursion depth for some TyCon (so bail out and conservatively
           -- claim the type is inhabited).
  where
    -- Checks if an InhabitationCandidate for a strict argument type:
    --
    -- (1) Has satisfiable term and type constraints.
    -- (2) Has 'nonVoid' strict argument types (we bail out of this
    --     check if recursion is detected).
    --
    -- See Note [Strict argument type constraints]
    cand_is_inhabitable :: RecTcChecker -> Delta
                        -> InhabitationCandidate -> DsM Bool
    cand_is_inhabitable :: RecTcChecker
-> Delta
-> InhabitationCandidate
-> IOEnv (Env DsGblEnv DsLclEnv) Bool
cand_is_inhabitable RecTcChecker
rec_ts Delta
amb_cs
      (InhabitationCandidate{ ic_cs :: InhabitationCandidate -> PmCts
ic_cs             = PmCts
new_cs
                            , ic_strict_arg_tys :: InhabitationCandidate -> [Type]
ic_strict_arg_tys = [Type]
new_strict_arg_tys }) = do
        let ([Type]
new_ty_cs, [TmCt]
new_tm_cs) = PmCts -> ([Type], [TmCt])
partitionTyTmCts PmCts
new_cs
        (Maybe Delta -> Bool)
-> DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Maybe Delta -> Bool
forall a. Maybe a -> Bool
isJust (DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> DsM (Maybe Delta) -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall a b. (a -> b) -> a -> b
$ Delta -> SatisfiabilityCheck -> DsM (Maybe Delta)
runSatisfiabilityCheck Delta
amb_cs (SatisfiabilityCheck -> DsM (Maybe Delta))
-> SatisfiabilityCheck -> DsM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ [SatisfiabilityCheck] -> SatisfiabilityCheck
forall a. Monoid a => [a] -> a
mconcat
          [ Bool -> Bag Type -> SatisfiabilityCheck
tyIsSatisfiable Bool
False ([Type] -> Bag Type
forall a. [a] -> Bag a
listToBag [Type]
new_ty_cs)
          , Bag TmCt -> SatisfiabilityCheck
tmIsSatisfiable ([TmCt] -> Bag TmCt
forall a. [a] -> Bag a
listToBag [TmCt]
new_tm_cs)
          , RecTcChecker -> [Type] -> SatisfiabilityCheck
tysAreNonVoid RecTcChecker
rec_ts [Type]
new_strict_arg_tys
          ]

-- | @'definitelyInhabitedType' ty@ returns 'True' if @ty@ has at least one
-- constructor @C@ such that:
--
-- 1. @C@ has no equality constraints.
-- 2. @C@ has no strict argument types.
--
-- See the @Note [Strict argument type constraints]@.
definitelyInhabitedType :: TyState -> Type -> DsM Bool
definitelyInhabitedType :: TyState -> Type -> IOEnv (Env DsGblEnv DsLclEnv) Bool
definitelyInhabitedType TyState
ty_st Type
ty = do
  TopNormaliseTypeResult
res <- TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty
  Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool)
-> Bool -> IOEnv (Env DsGblEnv DsLclEnv) Bool
forall a b. (a -> b) -> a -> b
$ case TopNormaliseTypeResult
res of
           HadRedexes Type
_ [(Type, DataCon, Type)]
cons Type
_ -> ((Type, DataCon, Type) -> Bool) -> [(Type, DataCon, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Type, DataCon, Type) -> Bool
meets_criteria [(Type, DataCon, Type)]
cons
           TopNormaliseTypeResult
_                   -> Bool
False
  where
    meets_criteria :: (Type, DataCon, Type) -> Bool
    meets_criteria :: (Type, DataCon, Type) -> Bool
meets_criteria (Type
_, DataCon
con, Type
_) =
      [EqSpec] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [EqSpec]
dataConEqSpec DataCon
con) Bool -> Bool -> Bool
&& -- (1)
      [HsImplBang] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [HsImplBang]
dataConImplBangs DataCon
con) -- (2)

{- Note [Strict argument type constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the ConVar case of clause processing, each conlike K traditionally
generates two different forms of constraints:

* A term constraint (e.g., x ~ K y1 ... yn)
* Type constraints from the conlike's context (e.g., if K has type
  forall bs. Q => s1 .. sn -> T tys, then Q would be its type constraints)

As it turns out, these alone are not enough to detect a certain class of
unreachable code. Consider the following example (adapted from #15305):

  data K = K1 | K2 !Void

  f :: K -> ()
  f K1 = ()

Even though `f` doesn't match on `K2`, `f` is exhaustive in its patterns. Why?
Because it's impossible to construct a terminating value of type `K` using the
`K2` constructor, and thus it's impossible for `f` to ever successfully match
on `K2`.

The reason is because `K2`'s field of type `Void` is //strict//. Because there
are no terminating values of type `Void`, any attempt to construct something
using `K2` will immediately loop infinitely or throw an exception due to the
strictness annotation. (If the field were not strict, then `f` could match on,
say, `K2 undefined` or `K2 (let x = x in x)`.)

Since neither the term nor type constraints mentioned above take strict
argument types into account, we make use of the `nonVoid` function to
determine whether a strict type is inhabitable by a terminating value or not.
We call this the "inhabitation test".

`nonVoid ty` returns True when either:
1. `ty` has at least one InhabitationCandidate for which both its term and type
   constraints are satisfiable, and `nonVoid` returns `True` for all of the
   strict argument types in that InhabitationCandidate.
2. We're unsure if it's inhabited by a terminating value.

`nonVoid ty` returns False when `ty` is definitely uninhabited by anything
(except bottom). Some examples:

* `nonVoid Void` returns False, since Void has no InhabitationCandidates.
  (This is what lets us discard the `K2` constructor in the earlier example.)
* `nonVoid (Int :~: Int)` returns True, since it has an InhabitationCandidate
  (through the Refl constructor), and its term constraint (x ~ Refl) and
  type constraint (Int ~ Int) are satisfiable.
* `nonVoid (Int :~: Bool)` returns False. Although it has an
  InhabitationCandidate (by way of Refl), its type constraint (Int ~ Bool) is
  not satisfiable.
* Given the following definition of `MyVoid`:

    data MyVoid = MkMyVoid !Void

  `nonVoid MyVoid` returns False. The InhabitationCandidate for the MkMyVoid
  constructor contains Void as a strict argument type, and since `nonVoid Void`
  returns False, that InhabitationCandidate is discarded, leaving no others.
* Whether or not a type is inhabited is undecidable in general.
  See Note [Fuel for the inhabitation test].
* For some types, inhabitation is evident immediately and we don't need to
  perform expensive tests. See Note [Types that are definitely inhabitable].

Note [Fuel for the inhabitation test]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Whether or not a type is inhabited is undecidable in general. As a result, we
can run into infinite loops in `nonVoid`. Therefore, we adopt a fuel-based
approach to prevent that.

Consider the following example:

  data Abyss = MkAbyss !Abyss
  stareIntoTheAbyss :: Abyss -> a
  stareIntoTheAbyss x = case x of {}

In principle, stareIntoTheAbyss is exhaustive, since there is no way to
construct a terminating value using MkAbyss. However, both the term and type
constraints for MkAbyss are satisfiable, so the only way one could determine
that MkAbyss is unreachable is to check if `nonVoid Abyss` returns False.
There is only one InhabitationCandidate for Abyss—MkAbyss—and both its term
and type constraints are satisfiable, so we'd need to check if `nonVoid Abyss`
returns False... and now we've entered an infinite loop!

To avoid this sort of conundrum, `nonVoid` uses a simple test to detect the
presence of recursive types (through `checkRecTc`), and if recursion is
detected, we bail out and conservatively assume that the type is inhabited by
some terminating value. This avoids infinite loops at the expense of making
the coverage checker incomplete with respect to functions like
stareIntoTheAbyss above. Then again, the same problem occurs with recursive
newtypes, like in the following code:

  newtype Chasm = MkChasm Chasm
  gazeIntoTheChasm :: Chasm -> a
  gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive

So this limitation is somewhat understandable.

Note that even with this recursion detection, there is still a possibility that
`nonVoid` can run in exponential time. Consider the following data type:

  data T = MkT !T !T !T

If we call `nonVoid` on each of its fields, that will require us to once again
check if `MkT` is inhabitable in each of those three fields, which in turn will
require us to check if `MkT` is inhabitable again... As you can see, the
branching factor adds up quickly, and if the recursion depth limit is, say,
100, then `nonVoid T` will effectively take forever.

To mitigate this, we check the branching factor every time we are about to call
`nonVoid` on a list of strict argument types. If the branching factor exceeds 1
(i.e., if there is potential for exponential runtime), then we limit the
maximum recursion depth to 1 to mitigate the problem. If the branching factor
is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay
to stick with a larger maximum recursion depth.

In #17977 we saw that the defaultRecTcMaxBound (100 at the time of writing) was
too large and had detrimental effect on performance of the coverage checker.
Given that we only commit to a best effort anyway, we decided to substantially
decrement the recursion depth to 3, at the cost of precision in some edge cases
like

  data Nat = Z | S Nat
  data Down :: Nat -> Type where
    Down :: !(Down n) -> Down (S n)
  f :: Down (S (S (S (S (S Z))))) -> ()
  f x = case x of {}

Since the coverage won't bother to instantiate Down 4 levels deep to see that it
is in fact uninhabited, it will emit a inexhaustivity warning for the case.

Note [Types that are definitely inhabitable]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Another microoptimization applies to data types like this one:

  data S a = S ![a] !T

Even though there is a strict field of type [a], it's quite silly to call
nonVoid on it, since it's "obvious" that it is inhabitable. To make this
intuition formal, we say that a type is definitely inhabitable (DI) if:

  * It has at least one constructor C such that:
    1. C has no equality constraints (since they might be unsatisfiable)
    2. C has no strict argument types (since they might be uninhabitable)

It's relatively cheap to check if a type is DI, so before we call `nonVoid`
on a list of strict argument types, we filter out all of the DI ones.
-}

--------------------------------------------
-- * Providing positive evidence for a Delta

-- | @provideEvidence vs n delta@ returns a list of
-- at most @n@ (but perhaps empty) refinements of @delta@ that instantiate
-- @vs@ to compatible constructor applications or wildcards.
-- Negative information is only retained if literals are involved or when
-- for recursive GADTs.
provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta]
provideEvidence = [Id] -> Int -> Delta -> DsM [Delta]
go
  where
    go :: [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
_      Int
0 Delta
_     = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    go []     Int
_ Delta
delta = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Delta
delta]
    go (Id
x:[Id]
xs) Int
n Delta
delta = do
      String -> SDoc -> DsM ()
tracePm String
"provideEvidence" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
$$ [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Id]
xs SDoc -> SDoc -> SDoc
$$ Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta SDoc -> SDoc -> SDoc
$$ Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n)
      VI Type
_ [(PmAltCon, [Id], [Id])]
pos PmAltConSet
neg PossibleMatches
_ <- Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
delta Id
x
      case [(PmAltCon, [Id], [Id])]
pos of
        (PmAltCon, [Id], [Id])
_:[(PmAltCon, [Id], [Id])]
_ -> do
          -- All solutions must be valid at once. Try to find candidates for their
          -- fields. Example:
          --   f x@(Just _) True = case x of SomePatSyn _ -> ()
          -- after this clause, we want to report that
          --   * @f Nothing _@ is uncovered
          --   * @f x False@ is uncovered
          -- where @x@ will have two possibly compatible solutions, @Just y@ for
          -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@
          -- and @z@ that is valid at the same time. These constitute arg_vas below.
          let arg_vas :: [Id]
arg_vas = ((PmAltCon, [Id], [Id]) -> [Id])
-> [(PmAltCon, [Id], [Id])] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(PmAltCon
_cl, [Id]
_tvs, [Id]
args) -> [Id]
args) [(PmAltCon, [Id], [Id])]
pos
          [Id] -> Int -> Delta -> DsM [Delta]
go ([Id]
arg_vas [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id]
xs) Int
n Delta
delta
        []
          -- When there are literals involved, just print negative info
          -- instead of listing missed constructors
          | [PmLit] -> Bool
forall a. [a] -> Bool
notNull [ PmLit
l | PmAltLit PmLit
l <- PmAltConSet -> [PmAltCon]
pmAltConSetElems PmAltConSet
neg ]
          -> [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
delta
        [] -> Id -> [Id] -> Int -> Delta -> DsM [Delta]
try_instantiate Id
x [Id]
xs Int
n Delta
delta

    -- | Tries to instantiate a variable by possibly following the chain of
    -- newtypes and then instantiating to all ConLikes of the wrapped type's
    -- minimal residual COMPLETE set.
    try_instantiate :: Id -> [Id] -> Int -> Delta -> DsM [Delta]
    -- Convention: x binds the outer constructor in the chain, y the inner one.
    try_instantiate :: Id -> [Id] -> Int -> Delta -> DsM [Delta]
try_instantiate Id
x [Id]
xs Int
n Delta
delta = do
      (Type
_src_ty, [(Type, DataCon, Type)]
dcs, Type
core_ty) <- TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
tntrGuts (TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type))
-> DsM TopNormaliseTypeResult
-> IOEnv
     (Env DsGblEnv DsLclEnv) (Type, [(Type, DataCon, Type)], Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType (Delta -> TyState
delta_ty_st Delta
delta) (Id -> Type
idType Id
x)
      let build_newtype :: (Id, Delta) -> (a, DataCon, Type) -> MaybeT DsM (Id, Delta)
build_newtype (Id
x, Delta
delta) (a
_ty, DataCon
dc, Type
arg_ty) = do
            Id
y <- DsM Id -> MaybeT DsM Id
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM Id -> MaybeT DsM Id) -> DsM Id -> MaybeT DsM Id
forall a b. (a -> b) -> a -> b
$ Type -> DsM Id
mkPmId Type
arg_ty
            -- Newtypes don't have existentials (yet?!), so passing an empty
            -- list as ex_tvs.
            Delta
delta' <- Delta -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT DsM Delta
addConCt Delta
delta Id
x (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [] [Id
y]
            (Id, Delta) -> MaybeT DsM (Id, Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
y, Delta
delta')
      MaybeT DsM (Id, Delta)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe (Id, Delta))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (((Id, Delta) -> (Type, DataCon, Type) -> MaybeT DsM (Id, Delta))
-> (Id, Delta) -> [(Type, DataCon, Type)] -> MaybeT DsM (Id, Delta)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (Id, Delta) -> (Type, DataCon, Type) -> MaybeT DsM (Id, Delta)
forall {a}.
(Id, Delta) -> (a, DataCon, Type) -> MaybeT DsM (Id, Delta)
build_newtype (Id
x, Delta
delta) [(Type, DataCon, Type)]
dcs) IOEnv (Env DsGblEnv DsLclEnv) (Maybe (Id, Delta))
-> (Maybe (Id, Delta) -> DsM [Delta]) -> DsM [Delta]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe (Id, Delta)
Nothing -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        Just (Id
y, Delta
newty_delta) -> do
          -- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥.
          PossibleMatches
pm     <- VarInfo -> PossibleMatches
vi_cache (VarInfo -> PossibleMatches)
-> DsM VarInfo -> IOEnv (Env DsGblEnv DsLclEnv) PossibleMatches
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Delta -> Id -> DsM VarInfo
initLookupVarInfo Delta
newty_delta Id
y
          Maybe ConLikeSet
mb_cls <- Delta -> PossibleMatches -> DsM (Maybe ConLikeSet)
pickMinimalCompleteSet Delta
newty_delta PossibleMatches
pm
          case ConLikeSet -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList (ConLikeSet -> [ConLike]) -> Maybe ConLikeSet -> Maybe [ConLike]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe ConLikeSet
mb_cls of
            Just cls :: [ConLike]
cls@(ConLike
_:[ConLike]
_) -> Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
instantiate_cons Id
y Type
core_ty [Id]
xs Int
n Delta
newty_delta [ConLike]
cls
            Just [] | Bool -> Bool
not (Delta -> Id -> Bool
canDiverge Delta
newty_delta Id
y) -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
            -- Either ⊥ is still possible (think Void) or there are no COMPLETE
            -- sets available, so we can assume it's inhabited
            Maybe [ConLike]
_ -> [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
newty_delta

    instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
    instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
instantiate_cons Id
_ Type
_  [Id]
_  Int
_ Delta
_     []       = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    instantiate_cons Id
_ Type
_  [Id]
_  Int
0 Delta
_     [ConLike]
_        = [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    instantiate_cons Id
_ Type
ty [Id]
xs Int
n Delta
delta [ConLike]
_
      -- We don't want to expose users to GHC-specific constructors for Int etc.
      | ((TyCon, [Type]) -> Bool) -> Maybe (TyCon, [Type]) -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TyCon -> Bool
isTyConTriviallyInhabited (TyCon -> Bool)
-> ((TyCon, [Type]) -> TyCon) -> (TyCon, [Type]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, [Type]) -> TyCon
forall a b. (a, b) -> a
fst) (HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty) Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
      = [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
delta
    instantiate_cons Id
x Type
ty [Id]
xs Int
n Delta
delta (ConLike
cl:[ConLike]
cls) = do
      FamInstEnvs
env <- DsM FamInstEnvs
dsGetFamInstEnvs
      case FamInstEnvs -> Type -> ConLike -> Maybe [Type]
guessConLikeUnivTyArgsFromResTy FamInstEnvs
env Type
ty ConLike
cl of
        Maybe [Type]
Nothing -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Delta
delta] -- No idea how to refine this one, so just finish off with a wildcard
        Just [Type]
arg_tys -> do
          ([Id]
tvs, [Id]
arg_vars, Bag Type
new_ty_cs, [Type]
strict_arg_tys) <- [Type] -> ConLike -> DsM ([Id], [Id], Bag Type, [Type])
mkOneConFull [Type]
arg_tys ConLike
cl
          let new_tm_cs :: Bag TmCt
new_tm_cs = TmCt -> Bag TmCt
forall a. a -> Bag a
unitBag (Id -> PmAltCon -> [Id] -> [Id] -> TmCt
TmConCt Id
x (ConLike -> PmAltCon
PmAltConLike ConLike
cl) [Id]
tvs [Id]
arg_vars)
          -- Now check satifiability
          Maybe Delta
mb_delta <- Delta -> Bag Type -> Bag TmCt -> [Type] -> DsM (Maybe Delta)
pmIsSatisfiable Delta
delta Bag Type
new_ty_cs Bag TmCt
new_tm_cs [Type]
strict_arg_tys
          String -> SDoc -> DsM ()
tracePm String
"instantiate_cons" ([SDoc] -> SDoc
vcat [ Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x
                                           , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Type
idType Id
x)
                                           , Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
                                           , ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
cl
                                           , [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
arg_tys
                                           , Bag TmCt -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TmCt
new_tm_cs
                                           , Bag Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag Type
new_ty_cs
                                           , [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
strict_arg_tys
                                           , Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Delta
delta
                                           , Maybe Delta -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe Delta
mb_delta
                                           , Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n ])
          [Delta]
con_deltas <- case Maybe Delta
mb_delta of
            Maybe Delta
Nothing     -> [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
            -- NB: We don't prepend arg_vars as we don't have any evidence on
            -- them and we only want to split once on a data type. They are
            -- inhabited, otherwise pmIsSatisfiable would have refuted.
            Just Delta
delta' -> [Id] -> Int -> Delta -> DsM [Delta]
go [Id]
xs Int
n Delta
delta'
          [Delta]
other_cons_deltas <- Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta]
instantiate_cons Id
x Type
ty [Id]
xs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Delta] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Delta]
con_deltas) Delta
delta [ConLike]
cls
          [Delta] -> DsM [Delta]
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Delta]
con_deltas [Delta] -> [Delta] -> [Delta]
forall a. [a] -> [a] -> [a]
++ [Delta]
other_cons_deltas)

pickMinimalCompleteSet :: Delta -> PossibleMatches -> DsM (Maybe ConLikeSet)
pickMinimalCompleteSet :: Delta -> PossibleMatches -> DsM (Maybe ConLikeSet)
pickMinimalCompleteSet Delta
_ PossibleMatches
NoPM      = Maybe ConLikeSet -> DsM (Maybe ConLikeSet)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ConLikeSet
forall a. Maybe a
Nothing
-- TODO: First prune sets with type info in delta. But this is good enough for
-- now and less costly. See #17386.
pickMinimalCompleteSet Delta
_ (PM NonEmpty ConLikeSet
clss) = do
  String -> SDoc -> DsM ()
tracePm String
"pickMinimalCompleteSet" ([ConLikeSet] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([ConLikeSet] -> SDoc) -> [ConLikeSet] -> SDoc
forall a b. (a -> b) -> a -> b
$ NonEmpty ConLikeSet -> [ConLikeSet]
forall a. NonEmpty a -> [a]
NonEmpty.toList NonEmpty ConLikeSet
clss)
  Maybe ConLikeSet -> DsM (Maybe ConLikeSet)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ConLikeSet -> Maybe ConLikeSet
forall a. a -> Maybe a
Just ((ConLikeSet -> ConLikeSet -> Ordering)
-> NonEmpty ConLikeSet -> ConLikeSet
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy ((ConLikeSet -> Int) -> ConLikeSet -> ConLikeSet -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ConLikeSet -> Int
forall a. UniqDSet a -> Int
sizeUniqDSet) NonEmpty ConLikeSet
clss))

-- | Finds a representant of the semantic equality class of the given @e@.
-- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
-- equivalent to @e'@) we encountered earlier, or a fresh identifier if
-- there weren't any such constraints.
representCoreExpr :: Delta -> CoreExpr -> DsM (Delta, Id)
representCoreExpr :: Delta -> CoreExpr -> DsM (Delta, Id)
representCoreExpr delta :: Delta
delta@MkDelta{ delta_tm_st :: Delta -> TmState
delta_tm_st = ts :: TmState
ts@TmSt{ ts_reps :: TmState -> CoreMap Id
ts_reps = CoreMap Id
reps } } CoreExpr
e
  | Just Id
rep <- CoreMap Id -> CoreExpr -> Maybe Id
forall a. CoreMap a -> CoreExpr -> Maybe a
lookupCoreMap CoreMap Id
reps CoreExpr
e = (Delta, Id) -> DsM (Delta, Id)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta, Id
rep)
  | Bool
otherwise = do
      Id
rep <- Type -> DsM Id
mkPmId (CoreExpr -> Type
exprType CoreExpr
e)
      let reps' :: CoreMap Id
reps'  = CoreMap Id -> CoreExpr -> Id -> CoreMap Id
forall a. CoreMap a -> CoreExpr -> a -> CoreMap a
extendCoreMap CoreMap Id
reps CoreExpr
e Id
rep
      let delta' :: Delta
delta' = Delta
delta{ delta_tm_st :: TmState
delta_tm_st = TmState
ts{ ts_reps :: CoreMap Id
ts_reps = CoreMap Id
reps' } }
      (Delta, Id) -> DsM (Delta, Id)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta
delta', Id
rep)

-- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
-- on the shape of the 'CoreExpr' @e@. Examples:
--
--   * For @let x = Just (42, 'z')@ we want to record the
--     constraints @x ~ Just a, a ~ (b, c), b ~ 42, c ~ 'z'@.
--     See 'data_con_app'.
--   * For @let x = unpackCString# "tmp"@ we want to record the literal
--     constraint @x ~ "tmp"@.
--   * For @let x = I# 42@ we want the literal constraint @x ~ 42@. Similar
--     for other literals. See 'coreExprAsPmLit'.
--   * Finally, if we have @let x = e@ and we already have seen @let y = e@, we
--     want to record @x ~ y@.
addCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta
addCoreCt :: Delta -> Id -> CoreExpr -> MaybeT DsM Delta
addCoreCt Delta
delta Id
x CoreExpr
e = do
  DynFlags
dflags <- MaybeT DsM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  let e' :: CoreExpr
e' = HasDebugCallStack => DynFlags -> CoreExpr -> CoreExpr
DynFlags -> CoreExpr -> CoreExpr
simpleOptExpr DynFlags
dflags CoreExpr
e
  DsM () -> MaybeT DsM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM () -> MaybeT DsM ()) -> DsM () -> MaybeT DsM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> DsM ()
tracePm String
"addCoreCt" (Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
$$ CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e SDoc -> SDoc -> SDoc
$$ CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e')
  StateT Delta (MaybeT DsM) () -> Delta -> MaybeT DsM Delta
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT (Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
core_expr Id
x CoreExpr
e') Delta
delta
  where
    -- | Takes apart a 'CoreExpr' and tries to extract as much information about
    -- literals and constructor applications as possible.
    core_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
    -- TODO: Handle newtypes properly, by wrapping the expression in a DataCon
    -- This is the right thing for casts involving data family instances and
    -- their representation TyCon, though (which are not visible in source
    -- syntax). See Note [COMPLETE sets on data families]
    -- core_expr x e | pprTrace "core_expr" (ppr x $$ ppr e) False = undefined
    core_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
core_expr Id
x (Cast CoreExpr
e Coercion
_co) = Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
core_expr Id
x CoreExpr
e
    core_expr Id
x (Tick Tickish Id
_t CoreExpr
e) = Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
core_expr Id
x CoreExpr
e
    core_expr Id
x CoreExpr
e
      | Just (PmLit -> Maybe FastString
pmLitAsStringLit -> Just FastString
s) <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
      , Type
expr_ty Type -> Type -> Bool
`eqType` Type
stringTy
      -- See Note [Representation of Strings in TmState]
      = case FastString -> String
unpackFS FastString
s of
          -- We need this special case to break a loop with coreExprAsPmLit
          -- Otherwise we alternate endlessly between [] and ""
          [] -> Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Delta (MaybeT DsM) ()
data_con_app Id
x InScopeSet
emptyInScopeSet DataCon
nilDataCon []
          String
s' -> Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
core_expr Id
x (Type -> [CoreExpr] -> CoreExpr
mkListExpr Type
charTy ((Char -> CoreExpr) -> String -> [CoreExpr]
forall a b. (a -> b) -> [a] -> [b]
map Char -> CoreExpr
mkCharExpr String
s'))
      | Just PmLit
lit <- CoreExpr -> Maybe PmLit
coreExprAsPmLit CoreExpr
e
      = Id -> PmLit -> StateT Delta (MaybeT DsM) ()
pm_lit Id
x PmLit
lit
      | Just (InScopeSet
in_scope, _empty_floats :: [FloatBind]
_empty_floats@[], DataCon
dc, [Type]
_arg_tys, [CoreExpr]
args)
            <- InScopeEnv
-> CoreExpr
-> Maybe (InScopeSet, [FloatBind], DataCon, [Type], [CoreExpr])
HasDebugCallStack =>
InScopeEnv
-> CoreExpr
-> Maybe (InScopeSet, [FloatBind], DataCon, [Type], [CoreExpr])
exprIsConApp_maybe InScopeEnv
forall {b}. (InScopeSet, b -> Unfolding)
in_scope_env CoreExpr
e
      = Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Delta (MaybeT DsM) ()
data_con_app Id
x InScopeSet
in_scope DataCon
dc [CoreExpr]
args
      -- See Note [Detecting pattern synonym applications in expressions]
      | Var Id
y <- CoreExpr
e, Maybe DataCon
Nothing <- Id -> Maybe DataCon
isDataConId_maybe Id
x
      -- We don't consider DataCons flexible variables
      = (Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT (\Delta
delta -> Delta -> Id -> Id -> MaybeT DsM Delta
addVarCt Delta
delta Id
x Id
y)
      | Bool
otherwise
      -- Any other expression. Try to find other uses of a semantically
      -- equivalent expression and represent them by the same variable!
      = Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
equate_with_similar_expr Id
x CoreExpr
e
      where
        expr_ty :: Type
expr_ty       = CoreExpr -> Type
exprType CoreExpr
e
        expr_in_scope :: InScopeSet
expr_in_scope = VarSet -> InScopeSet
mkInScopeSet (CoreExpr -> VarSet
exprFreeVars CoreExpr
e)
        in_scope_env :: (InScopeSet, b -> Unfolding)
in_scope_env  = (InScopeSet
expr_in_scope, Unfolding -> b -> Unfolding
forall a b. a -> b -> a
const Unfolding
NoUnfolding)
        -- It's inconvenient to get hold of a global in-scope set
        -- here, but it'll only be needed if exprIsConApp_maybe ends
        -- up substituting inside a forall or lambda (i.e. seldom)
        -- so using exprFreeVars seems fine.   See MR !1647.

    -- | The @e@ in @let x = e@ had no familiar form. But we can still see if
    -- see if we already encountered a constraint @let y = e'@ with @e'@
    -- semantically equivalent to @e@, in which case we may add the constraint
    -- @x ~ y@.
    equate_with_similar_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
    equate_with_similar_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
equate_with_similar_expr Id
x CoreExpr
e = do
      Id
rep <- (Delta -> MaybeT DsM (Id, Delta)) -> StateT Delta (MaybeT DsM) Id
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Delta -> MaybeT DsM (Id, Delta)) -> StateT Delta (MaybeT DsM) Id)
-> (Delta -> MaybeT DsM (Id, Delta))
-> StateT Delta (MaybeT DsM) Id
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> (Delta, Id) -> (Id, Delta)
forall a b. (a, b) -> (b, a)
swap ((Delta, Id) -> (Id, Delta))
-> MaybeT DsM (Delta, Id) -> MaybeT DsM (Id, Delta)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DsM (Delta, Id) -> MaybeT DsM (Delta, Id)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Delta -> CoreExpr -> DsM (Delta, Id)
representCoreExpr Delta
delta CoreExpr
e)
      -- Note that @rep == x@ if we encountered @e@ for the first time.
      (Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT (\Delta
delta -> Delta -> Id -> Id -> MaybeT DsM Delta
addVarCt Delta
delta Id
x Id
rep)

    bind_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id
    bind_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id
bind_expr CoreExpr
e = do
      Id
x <- MaybeT DsM Id -> StateT Delta (MaybeT DsM) Id
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM Id -> MaybeT DsM Id
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Type -> DsM Id
mkPmId (CoreExpr -> Type
exprType CoreExpr
e)))
      Id -> CoreExpr -> StateT Delta (MaybeT DsM) ()
core_expr Id
x CoreExpr
e
      Id -> StateT Delta (MaybeT DsM) Id
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
x

    -- | Look at @let x = K taus theta es@ and generate the following
    -- constraints (assuming universals were dropped from @taus@ before):
    --   1. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@
    --   2. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
    --   3. @x ~ K as ys@
    data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Delta (MaybeT DsM) ()
    data_con_app :: Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Delta (MaybeT DsM) ()
data_con_app Id
x InScopeSet
in_scope DataCon
dc [CoreExpr]
args = do
      let dc_ex_tvs :: [Id]
dc_ex_tvs              = DataCon -> [Id]
dataConExTyCoVars DataCon
dc
          arty :: Int
arty                   = DataCon -> Int
dataConSourceArity DataCon
dc
          ([CoreExpr]
ex_ty_args, [CoreExpr]
val_args) = [Id] -> [CoreExpr] -> ([CoreExpr], [CoreExpr])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [Id]
dc_ex_tvs [CoreExpr]
args
          ex_tys :: [Type]
ex_tys                 = (CoreExpr -> Type) -> [CoreExpr] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map CoreExpr -> Type
exprToType [CoreExpr]
ex_ty_args
          vis_args :: [CoreExpr]
vis_args               = [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a]
reverse ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
forall a b. (a -> b) -> a -> b
$ Int -> [CoreExpr] -> [CoreExpr]
forall a. Int -> [a] -> [a]
take Int
arty ([CoreExpr] -> [CoreExpr]) -> [CoreExpr] -> [CoreExpr]
forall a b. (a -> b) -> a -> b
$ [CoreExpr] -> [CoreExpr]
forall a. [a] -> [a]
reverse [CoreExpr]
val_args
      UniqSupply
uniq_supply <- MaybeT DsM UniqSupply -> StateT Delta (MaybeT DsM) UniqSupply
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (MaybeT DsM UniqSupply -> StateT Delta (MaybeT DsM) UniqSupply)
-> MaybeT DsM UniqSupply -> StateT Delta (MaybeT DsM) UniqSupply
forall a b. (a -> b) -> a -> b
$ IOEnv (Env DsGblEnv DsLclEnv) UniqSupply -> MaybeT DsM UniqSupply
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOEnv (Env DsGblEnv DsLclEnv) UniqSupply -> MaybeT DsM UniqSupply)
-> IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
-> MaybeT DsM UniqSupply
forall a b. (a -> b) -> a -> b
$ IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
      let (TCvSubst
_, [Id]
ex_tvs) = TCvSubst -> [Id] -> UniqSupply -> (TCvSubst, [Id])
cloneTyVarBndrs (InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope) [Id]
dc_ex_tvs UniqSupply
uniq_supply
          ty_cts :: [PmCt]
ty_cts      = [Type] -> [Type] -> [PmCt]
equateTys ((Id -> Type) -> [Id] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
ex_tvs) [Type]
ex_tys
      -- 1. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703
      (Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT ((Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ())
-> (Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ()
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> DsM (Maybe Delta) -> MaybeT DsM Delta
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (DsM (Maybe Delta) -> MaybeT DsM Delta)
-> DsM (Maybe Delta) -> MaybeT DsM Delta
forall a b. (a -> b) -> a -> b
$ Delta -> PmCts -> DsM (Maybe Delta)
addPmCts Delta
delta ([PmCt] -> PmCts
forall a. [a] -> Bag a
listToBag [PmCt]
ty_cts)
      -- 2. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
      [Id]
arg_ids <- (CoreExpr -> StateT Delta (MaybeT DsM) Id)
-> [CoreExpr] -> StateT Delta (MaybeT DsM) [Id]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse CoreExpr -> StateT Delta (MaybeT DsM) Id
bind_expr [CoreExpr]
vis_args
      -- 3. @x ~ K as ys@
      Id -> PmAltCon -> [Id] -> [Id] -> StateT Delta (MaybeT DsM) ()
pm_alt_con_app Id
x (ConLike -> PmAltCon
PmAltConLike (DataCon -> ConLike
RealDataCon DataCon
dc)) [Id]
ex_tvs [Id]
arg_ids

    -- | Adds a literal constraint, i.e. @x ~ 42@.
    pm_lit :: Id -> PmLit -> StateT Delta (MaybeT DsM) ()
    pm_lit :: Id -> PmLit -> StateT Delta (MaybeT DsM) ()
pm_lit Id
x PmLit
lit = Id -> PmAltCon -> [Id] -> [Id] -> StateT Delta (MaybeT DsM) ()
pm_alt_con_app Id
x (PmLit -> PmAltCon
PmAltLit PmLit
lit) [] []

    -- | Adds the given constructor application as a solution for @x@.
    pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Delta (MaybeT DsM) ()
    pm_alt_con_app :: Id -> PmAltCon -> [Id] -> [Id] -> StateT Delta (MaybeT DsM) ()
pm_alt_con_app Id
x PmAltCon
con [Id]
tvs [Id]
args = (Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT ((Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ())
-> (Delta -> MaybeT DsM Delta) -> StateT Delta (MaybeT DsM) ()
forall a b. (a -> b) -> a -> b
$ \Delta
delta -> Delta -> Id -> PmAltCon -> [Id] -> [Id] -> MaybeT DsM Delta
addConCt Delta
delta Id
x PmAltCon
con [Id]
tvs [Id]
args

-- | Like 'modify', but with an effectful modifier action
modifyT :: Monad m => (s -> m s) -> StateT s m ()
modifyT :: forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT s -> m s
f = (s -> m ((), s)) -> StateT s m ()
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((s -> m ((), s)) -> StateT s m ())
-> (s -> m ((), s)) -> StateT s m ()
forall a b. (a -> b) -> a -> b
$ (s -> ((), s)) -> m s -> m ((), s)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((,) ()) (m s -> m ((), s)) -> (s -> m s) -> s -> m ((), s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> m s
f

{- Note [Detecting pattern synonym applications in expressions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
At the moment we fail to detect pattern synonyms in scrutinees and RHS of
guards. This could be alleviated with considerable effort and complexity, but
the returns are meager. Consider:

    pattern P
    pattern Q
    case P 15 of
      Q _  -> ...
      P 15 ->

Compared to the situation where P and Q are DataCons, the lack of generativity
means we could never flag Q as redundant. (also see Note [Undecidable Equality
for PmAltCons] in PmTypes.) On the other hand, if we fail to recognise the
pattern synonym, we flag the pattern match as inexhaustive. That wouldn't happen
if we had knowledge about the scrutinee, in which case the oracle basically
knows "If it's a P, then its field is 15".

This is a pretty narrow use case and I don't think we should to try to fix it
until a user complains energetically.
-}