{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}

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

-- | Model refinements type as per the
-- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
-- The main export of the module are the functions 'addPhiCtsNablas' for adding
-- facts to the oracle, 'isInhabited' to check if a refinement type is inhabited
-- and 'generateInhabitingPatterns' to turn a 'Nabla' into a concrete pattern
-- for an equation.
--
-- In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6
-- and 3.7. E.g., it represents refinement types directly as a bunch of
-- normalised refinement types 'Nabla'.

module GHC.HsToCore.Pmc.Solver (

        Nabla, Nablas(..), initNablas,

        PhiCt(..), PhiCts,
        addPhiCtNablas,
        addPhiCtsNablas,

        isInhabited,
        generateInhabitingPatterns, GenerateInhabitingPatternsMode(..)

    ) where

import GHC.Prelude

import GHC.HsToCore.Pmc.Types
import GHC.HsToCore.Pmc.Utils (tracePm, traceWhenFailPm, mkPmId)
import GHC.HsToCore.Types (DsGblEnv(..))

import GHC.Driver.DynFlags
import GHC.Driver.Config
import GHC.Utils.Outputable
import GHC.Utils.Misc
import GHC.Utils.Monad (allM)
import GHC.Utils.Panic
import GHC.Data.Bag

import GHC.Types.CompleteMatch
import GHC.Types.Unique.Set
import GHC.Types.Unique.DSet
import GHC.Types.Unique.SDFM
import GHC.Types.Id
import GHC.Types.Name
import GHC.Types.Name.Reader (lookupGRE_Name, GlobalRdrEnv)
import GHC.Types.Var         (EvVar)
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Unique.Supply

import GHC.Tc.Utils.Monad   (getGblEnv)

import GHC.Core
import GHC.Core.FVs         (exprFreeVars)
import GHC.Core.TyCo.Compare( eqType )
import GHC.Core.Map.Expr
import GHC.Core.Predicate (typeDeterminesValue, mkNomEqPred)
import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
import GHC.Core.Utils     (exprType)
import GHC.Core.Make      (mkListExpr, mkCharExpr, mkImpossibleExpr)

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.Core.TyCon.RecWalk
import GHC.Builtin.Names
import GHC.Builtin.Types
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst (elemSubst)
import GHC.Core.Type
import GHC.Tc.Solver   (tcNormalise, tcCheckGivens, tcCheckWanteds)
import GHC.Core.Unify    (tcMatchTy)
import GHC.Core.Coercion
import GHC.Core.Reduction
import GHC.HsToCore.Monad hiding (foldlM)
import GHC.Tc.Instance.Family
import GHC.Core.FamInstEnv

import Control.Applicative ((<|>))
import Control.Monad (foldM, forM, guard, mzero, when, filterM)
import Control.Monad.Trans.Class (lift)
import Control.Monad.Trans.State.Strict
import Data.Coerce
import Data.Foldable (foldlM, minimumBy, toList)
import Data.Monoid   (Any(..))
import Data.List     (sortBy, find)
import qualified Data.List.NonEmpty as NE
import Data.Ord      (comparing)


--
-- * Main exports
--

-- | Add a bunch of 'PhiCt's to all the 'Nabla's.
-- Lifts 'addPhiCts' over many 'Nablas'.
addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas Nablas
nablas PhiCts
cts = (Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla))
-> Nablas -> DsM Nablas
forall (m :: * -> *).
Monad m =>
(Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM (\Nabla
d -> Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
d PhiCts
cts) Nablas
nablas

-- | 'addPmCtsNablas' for a single 'PmCt'.
addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
addPhiCtNablas Nablas
nablas PhiCt
ct = Nablas -> PhiCts -> DsM Nablas
addPhiCtsNablas Nablas
nablas (PhiCt -> PhiCts
forall a. a -> Bag a
unitBag PhiCt
ct)

liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM :: forall (m :: * -> *).
Monad m =>
(Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
liftNablasM Nabla -> m (Maybe Nabla)
f (MkNablas Bag Nabla
ds) = Bag Nabla -> Nablas
MkNablas (Bag Nabla -> Nablas)
-> (Bag (Maybe Nabla) -> Bag Nabla) -> Bag (Maybe Nabla) -> Nablas
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag (Maybe Nabla) -> Bag Nabla
forall a. Bag (Maybe a) -> Bag a
catBagMaybes (Bag (Maybe Nabla) -> Nablas) -> m (Bag (Maybe Nabla)) -> m Nablas
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Nabla -> m (Maybe Nabla)) -> Bag Nabla -> m (Bag (Maybe Nabla))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bag a -> f (Bag b)
traverse Nabla -> m (Maybe Nabla)
f Bag Nabla
ds)

-- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
-- we preserve the invariant that there are no uninhabited 'Nabla's. But that
-- could change in the future, for example by implementing this function in
-- terms of @notNull <$> generateInhabitingPatterns 1 ds@.
isInhabited :: Nablas -> DsM Bool
isInhabited :: Nablas -> DsM Bool
isInhabited (MkNablas Bag Nabla
ds) = Bool -> DsM Bool
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> Bool
not (Bag Nabla -> Bool
forall a. Bag a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Bag Nabla
ds))

-----------------------------------------------
-- * Caching residual COMPLETE sets

-- See Note [Implementation of COMPLETE pragmas]

-- | Update the COMPLETE sets of 'ResidualCompleteMatches', or 'Nothing'
-- if there was no change as per the update function.
updRcm :: (DsCompleteMatch -> (Bool, DsCompleteMatch))
       -> ResidualCompleteMatches -> (Maybe ResidualCompleteMatches)
updRcm :: (DsCompleteMatch -> (Bool, DsCompleteMatch))
-> ResidualCompleteMatches -> Maybe ResidualCompleteMatches
updRcm DsCompleteMatch -> (Bool, DsCompleteMatch)
f (RCM Maybe DsCompleteMatch
vanilla Maybe [DsCompleteMatch]
pragmas)
  | Bool -> Bool
not Bool
any_change = Maybe ResidualCompleteMatches
forall a. Maybe a
Nothing
  | Bool
otherwise      = ResidualCompleteMatches -> Maybe ResidualCompleteMatches
forall a. a -> Maybe a
Just (Maybe DsCompleteMatch
-> Maybe [DsCompleteMatch] -> ResidualCompleteMatches
RCM Maybe DsCompleteMatch
vanilla' Maybe [DsCompleteMatch]
pragmas')
  where
    f' :: DsCompleteMatch -> (Any, DsCompleteMatch)
    f' :: DsCompleteMatch -> (Any, DsCompleteMatch)
f' = (DsCompleteMatch -> (Bool, DsCompleteMatch))
-> DsCompleteMatch -> (Any, DsCompleteMatch)
forall a b. Coercible a b => a -> b
coerce DsCompleteMatch -> (Bool, DsCompleteMatch)
f
    (Any
chgd, Maybe DsCompleteMatch
vanilla')  = (DsCompleteMatch -> (Any, DsCompleteMatch))
-> Maybe DsCompleteMatch -> (Any, Maybe DsCompleteMatch)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse DsCompleteMatch -> (Any, DsCompleteMatch)
f' Maybe DsCompleteMatch
vanilla
    (Any
chgds, Maybe [DsCompleteMatch]
pragmas') = ([DsCompleteMatch] -> (Any, [DsCompleteMatch]))
-> Maybe [DsCompleteMatch] -> (Any, Maybe [DsCompleteMatch])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse ((DsCompleteMatch -> (Any, DsCompleteMatch))
-> [DsCompleteMatch] -> (Any, [DsCompleteMatch])
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse DsCompleteMatch -> (Any, DsCompleteMatch)
f') Maybe [DsCompleteMatch]
pragmas
    any_change :: Bool
any_change        = Any -> Bool
getAny (Any -> Bool) -> Any -> Bool
forall a b. (a -> b) -> a -> b
$ Any
chgd Any -> Any -> Any
forall a. Monoid a => a -> a -> a
`mappend` Any
chgds

-- | A pseudo-'CompleteMatch' for the vanilla complete set of the given data
-- 'TyCon'.
-- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@
vanillaCompleteMatchTC :: TyCon -> Maybe DsCompleteMatch
vanillaCompleteMatchTC :: TyCon -> Maybe DsCompleteMatch
vanillaCompleteMatchTC TyCon
tc =
  let mb_dcs :: Maybe [DataCon]
mb_dcs | -- 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.
               TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon    = [DataCon] -> Maybe [DataCon]
forall a. a -> Maybe a
Just []
             | -- Similarly, treat `type data` declarations as empty data types on
               -- the term level, as `type data` data constructors only exist at
               -- the type level (#22964).  See wrinkle (W2a) in
               -- Note [Type data declarations] in GHC.Rename.Module.
               TyCon -> Bool
isTypeDataTyCon TyCon
tc = [DataCon] -> Maybe [DataCon]
forall a. a -> Maybe a
Just []
             | Bool
otherwise          = TyCon -> Maybe [DataCon]
tyConDataCons_maybe TyCon
tc
  in UniqDSet ConLike -> DsCompleteMatch
forall con. UniqDSet con -> CompleteMatchX con
vanillaCompleteMatch (UniqDSet ConLike -> DsCompleteMatch)
-> ([DataCon] -> UniqDSet ConLike) -> [DataCon] -> DsCompleteMatch
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ConLike] -> UniqDSet ConLike
forall a. Uniquable a => [a] -> UniqDSet a
mkUniqDSet ([ConLike] -> UniqDSet ConLike)
-> ([DataCon] -> [ConLike]) -> [DataCon] -> UniqDSet ConLike
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DataCon -> ConLike) -> [DataCon] -> [ConLike]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> ConLike
RealDataCon ([DataCon] -> DsCompleteMatch)
-> Maybe [DataCon] -> Maybe DsCompleteMatch
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [DataCon]
mb_dcs

-- | Initialise from 'dsGetCompleteMatches' (containing all COMPLETE pragmas)
-- if the given 'ResidualCompleteMatches' were empty.
addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches (RCM Maybe DsCompleteMatch
v Maybe [DsCompleteMatch]
Nothing) = Maybe DsCompleteMatch
-> Maybe [DsCompleteMatch] -> ResidualCompleteMatches
RCM Maybe DsCompleteMatch
v (Maybe [DsCompleteMatch] -> ResidualCompleteMatches)
-> ([DsCompleteMatch] -> Maybe [DsCompleteMatch])
-> [DsCompleteMatch]
-> ResidualCompleteMatches
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DsCompleteMatch] -> Maybe [DsCompleteMatch]
forall a. a -> Maybe a
Just ([DsCompleteMatch] -> ResidualCompleteMatches)
-> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch]
-> DsM ResidualCompleteMatches
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch]
dsGetCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm             = ResidualCompleteMatches -> DsM ResidualCompleteMatches
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ResidualCompleteMatches
rcm

-- | Adds the declared 'CompleteMatches' from COMPLETE pragmas, as well as the
-- vanilla data defn if it is a 'DataCon'.
addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addConLikeMatches (RealDataCon DataCon
dc) ResidualCompleteMatches
rcm = TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches (DataCon -> TyCon
dataConTyCon DataCon
dc) ResidualCompleteMatches
rcm
addConLikeMatches (PatSynCon PatSyn
_)    ResidualCompleteMatches
rcm = ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm

-- | Adds
--    * the 'CompleteMatches' from COMPLETE pragmas
--    * and the /vanilla/ 'CompleteMatch' from the data 'TyCon'
-- to the 'ResidualCompleteMatches', if not already present.
addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches TyCon
tc ResidualCompleteMatches
rcm = ResidualCompleteMatches -> ResidualCompleteMatches
add_tc_match (ResidualCompleteMatches -> ResidualCompleteMatches)
-> DsM ResidualCompleteMatches -> DsM ResidualCompleteMatches
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm
  where
    -- Add the vanilla COMPLETE set from the data defn, if any. But only if
    -- it's not already present.
    add_tc_match :: ResidualCompleteMatches -> ResidualCompleteMatches
add_tc_match ResidualCompleteMatches
rcm
      = ResidualCompleteMatches
rcm{rcm_vanilla = rcm_vanilla rcm <|> vanillaCompleteMatchTC tc}

markMatched :: PmAltCon -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
-- Nothing means the PmAltCon didn't occur in any COMPLETE set.
-- See Note [Shortcutting the inhabitation test] for how this is useful for
-- performance on T17836.
markMatched :: PmAltCon
-> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
markMatched (PmAltLit PmLit
_)      ResidualCompleteMatches
_   = Maybe ResidualCompleteMatches
-> DsM (Maybe ResidualCompleteMatches)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe ResidualCompleteMatches
forall a. Maybe a
Nothing -- lits are never part of a COMPLETE set
markMatched (PmAltConLike ConLike
cl) ResidualCompleteMatches
rcm = do
  rcm' <- ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addConLikeMatches ConLike
cl ResidualCompleteMatches
rcm
  let go DsCompleteMatch
cm = case UniqDSet ConLike -> ConLike -> Maybe ConLike
forall a. Uniquable a => UniqDSet a -> a -> Maybe a
lookupUniqDSet (DsCompleteMatch -> UniqDSet ConLike
forall con. CompleteMatchX con -> UniqDSet con
cmConLikes DsCompleteMatch
cm) ConLike
cl of
        Maybe ConLike
Nothing -> (Bool
False, DsCompleteMatch
cm)
        Just ConLike
_  -> (Bool
True,  DsCompleteMatch
cm { cmConLikes = delOneFromUniqDSet (cmConLikes cm) cl })
  pure $ updRcm go rcm'

{- Note [Implementation of COMPLETE pragmas]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A COMPLETE set represents a set of conlikes (i.e., constructors or
pattern synonyms) such that if they are all pattern-matched against in a
function, it gives rise to a total function. An example is:

  newtype Boolean = Boolean Int
  pattern F, T :: Boolean
  pattern F = Boolean 0
  pattern T = Boolean 1
  {-# COMPLETE F, T #-}

  -- This is a total function
  booleanToInt :: Boolean -> Int
  booleanToInt F = 0
  booleanToInt T = 1

COMPLETE sets are represented internally in GHC as a set of 'ConLike's. For
example, the pragma {-# COMPLETE F, T #-} would be represented as:

  CompleteMatch {F, T} Nothing

What is the Maybe for? Answer: COMPLETE pragmas may optionally specify a
result *type constructor* (cf. T14422):

  class C f where
    foo :: f a -> ()
  pattern P :: C f => f a
  pattern P <- (foo -> ())

  instance C State where
    foo _ = ()
  {-# COMPLETE P :: State #-}

  f :: State a -> ()
  f P = ()
  g :: C f => f a -> ()
  g P = ()

The @:: State@ here means that the types at which the COMPLETE pragma *applies*
is restricted to scrutinee types that are applications of the 'State' TyCon. So
it applies to the match in @f@ but not in @g@ above, resulting in a warning for
the latter but not for the former. The pragma is represented as

  CompleteMatch {P} (Just State)

GHC collects all COMPLETE pragmas from the current module and from imports
into a field in the DsM environment, which can be accessed with
dsGetCompleteMatches from "GHC.HsToCore.Monad".
Currently, COMPLETE pragmas can't be orphans (e.g. at least one ConLike must
also be defined in the module of the pragma) and do not impact recompilation
checking (#18675).

The pattern-match checker will then initialise each variable's 'VarInfo' with
*all* imported COMPLETE sets (in 'GHC.HsToCore.Pmc.Solver.addCompleteMatches'),
well-typed or not, into a 'ResidualCompleteMatches'. The trick is that a
COMPLETE set that is ill-typed for that match variable could never be written by
the user! And we make sure not to report any ill-typed COMPLETE sets when
formatting 'Nabla's for warnings in 'generateInhabitingPatterns'.

A 'ResidualCompleteMatches' is a list of all COMPLETE sets, minus the ConLikes
we know a particular variable can't be (through negative constructor constraints
@x /~ K@ or a failed attempt at instantiating that ConLike during inhabitation
testing). If *any* of the COMPLETE sets become empty, we know that the match
was exhaustive.

We assume that a COMPLETE set does not apply if for one of its
ConLikes we fail to 'matchConLikeResTy' or the
type of the match variable isn't an application of the optional
result type constructor from the pragma. Why don't we simply
prune inapplicable COMPLETE sets from 'ResidualCompleteMatches'?
The answer is that additional type constraints might make more
COMPLETE sets applicable! Example:

  h :: a -> a :~: Boolean -> ()
  h x Refl | T <- x = ()
           | F <- x = ()

If we eagerly prune {F,T} from the residual matches of @x@, then we don't see
that the match in the guards of @h@ is exhaustive, where the COMPLETE set
applies due to refined type information.
-}

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

-- | The return value of 'pmTopNormaliseType'
data TopNormaliseTypeResult
  = 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
  -- 'generateInhabitingPatterns'.
  -- For an example, see Note [Type normalisation].

-- | 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 (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 (NormalisedByConstraints Type
ty)   = String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"NormalisedByConstraints" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> 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
forall doc. IsLine doc => String -> doc
text String
"HadRedexes" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces SDoc
fields
    where
      fields :: SDoc
fields = [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
fsep (SDoc -> [SDoc] -> [SDoc]
forall doc. IsLine doc => doc -> [doc] -> [doc]
punctuate SDoc
forall doc. IsLine doc => doc
comma [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"src_ty =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
src_ty
                                     , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"newtype_dcs =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [(Type, DataCon, Type)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, DataCon, Type)]
ds
                                     , String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"core_ty =" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> 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 Int
_ InertSet
inert) Type
typ = {-# SCC "pmTopNormaliseType" #-} do
  env <- DsM FamInstEnvs
dsGetFamInstEnvs
  tracePm "normalise" (ppr typ)
  -- 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].
  typ' <- initTcDsForSolver $ tcNormalise inert typ
  -- Now we look with topNormaliseTypeX through type and data family
  -- applications and newtypes, which tcNormalise does not do.
  -- See also 'TopNormaliseTypeResult'.
  pure $ case topNormaliseTypeX (stepper env) comb typ' of
    Maybe
  ((ThetaType -> ThetaType,
    [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]),
   Type)
Nothing                -> Type -> TopNormaliseTypeResult
NormalisedByConstraints Type
typ'
    Just ((ThetaType -> ThetaType
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 -> ThetaType -> Type
eq_src_ty Type
ty (Type
typ' Type -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
: ThetaType -> ThetaType
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 -> ThetaType -> Type
eq_src_ty Type
ty ThetaType
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) -> ThetaType -> Maybe Type
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Type -> Bool
is_closed_or_data_family ThetaType
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
     (ThetaType -> ThetaType,
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
stepper FamInstEnvs
env = NormaliseStepper
  (ThetaType -> ThetaType,
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper NormaliseStepper
  (ThetaType -> ThetaType,
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepper
     (ThetaType -> ThetaType,
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepper
     (ThetaType -> ThetaType,
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` FamInstEnvs
-> NormaliseStepper
     (ThetaType -> ThetaType,
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall a.
FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, 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
  (ThetaType -> ThetaType,
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
newTypeStepper RecTcChecker
rec_nts TyCon
tc ThetaType
tys
      | Just (Type
ty', Coercion
_co) <- TyCon -> ThetaType -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc ThetaType
tys
      , let orig_ty :: Type
orig_ty = TyCon -> ThetaType -> Type
TyConApp TyCon
tc ThetaType
tys
      = case RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_nts TyCon
tc of
          Just RecTcChecker
rec_nts' -> let tyf :: ThetaType -> ThetaType
tyf = (Type
orig_tyType -> ThetaType -> ThetaType
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
-> (ThetaType -> ThetaType,
    [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
-> NormaliseStepResult
     (ThetaType -> ThetaType,
      [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' (ThetaType -> ThetaType
tyf, [(Type, DataCon, Type)] -> [(Type, DataCon, Type)]
tmf)
          Maybe RecTcChecker
Nothing       -> NormaliseStepResult
  (ThetaType -> ThetaType,
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. NormaliseStepResult ev
NS_Abort
      | Bool
otherwise
      = NormaliseStepResult
  (ThetaType -> ThetaType,
   [(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
forall ev. NormaliseStepResult ev
NS_Done

    tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
    tyFamStepper :: forall a.
FamInstEnvs -> NormaliseStepper (ThetaType -> ThetaType, a -> a)
tyFamStepper FamInstEnvs
env RecTcChecker
rec_nts TyCon
tc ThetaType
tys  -- Try to step a type/data family
      = case FamInstEnvs -> TyCon -> ThetaType -> Maybe HetReduction
topReduceTyFamApp_maybe FamInstEnvs
env TyCon
tc ThetaType
tys of
          Just (HetReduction (Reduction Coercion
_ Type
rhs) MCoercionN
_)
            -> RecTcChecker
-> Type
-> (ThetaType -> ThetaType, a -> a)
-> NormaliseStepResult (ThetaType -> ThetaType, a -> a)
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
rhs ((Type
rhsType -> ThetaType -> ThetaType
forall a. a -> [a] -> [a]
:), a -> a
forall a. a -> a
id)
          Maybe HetReduction
_ -> NormaliseStepResult (ThetaType -> ThetaType, 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, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty of
      Just (TyCon
tc, ThetaType
ty_args)
             | TyCon -> Bool
is_algebraic_like TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamilyTyCon TyCon
tc)
             -> Bool -> SDoc -> Bool -> Bool
forall a. HasCallStack => Bool -> SDoc -> a -> a
assertPpr (ThetaType
ty_args ThetaType -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` TyCon -> Int
tyConArity TyCon
tc) (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty) Bool
True
      Maybe (TyCon, ThetaType)
_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 underlying 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

-- | Normalise the given source type to WHNF. If it isn't already in WHNF
-- ('isSourceTypeInWHNF') , it will normalise the type and then try to step
-- through type family applications, but not data family applications or
-- newtypes.
--
-- This is a pretty common case of calling 'pmTopNormaliseType' and it should be
-- efficient.
normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type
normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type
normaliseSourceTypeWHNF TyState
_     Type
ty | Type -> Bool
isSourceTypeInWHNF Type
ty = Type -> DsM Type
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
normaliseSourceTypeWHNF TyState
ty_st Type
ty =
  TyState -> Type -> DsM TopNormaliseTypeResult
pmTopNormaliseType TyState
ty_st Type
ty DsM TopNormaliseTypeResult
-> (TopNormaliseTypeResult -> DsM Type) -> DsM Type
forall a b.
IOEnv (Env DsGblEnv DsLclEnv) a
-> (a -> IOEnv (Env DsGblEnv DsLclEnv) b)
-> IOEnv (Env DsGblEnv DsLclEnv) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    NormalisedByConstraints Type
ty -> Type -> DsM Type
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty
    HadRedexes Type
ty [(Type, DataCon, Type)]
_ Type
_          -> Type -> DsM Type
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
ty

-- | Is the source type in WHNF wrt. 'pmTopNormaliseType'?
--
-- Returns False if the given type is not a TyCon application, or if the TyCon
-- app head is a type family TyCon. (But not for data family TyCons!)
isSourceTypeInWHNF :: Type -> Bool
isSourceTypeInWHNF :: Type -> Bool
isSourceTypeInWHNF Type
ty
  | Just (TyCon
tc, ThetaType
_) <- HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty = Bool -> Bool
not (TyCon -> Bool
isTypeFamilyTyCon TyCon
tc)
  | Bool
otherwise                              = Bool
False

{- 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.

Note [Coverage checking Newtype matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Newtypes have quite peculiar match semantics 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. 'isPmAltConMatchStrict' returns False for newtypes, indicating that a
   newtype match is lazy.
2. When we find @x ~ T2 y@, transfer all constraints on @x@ (which involve @⊥@)
   to @y@, similar to what 'equate' does, and don't add a @x ≁ ⊥@ constraint.
   This way, the third clause will still be marked as inaccessible RHS instead
   of redundant. This is ensured by calling 'lookupVarInfoNT'.
3. Immediately reject when we find @x ≁ T2@.
Handling of Newtypes is also described in the Appendix of the Lower Your Guards paper,
where you can find the solution in a perhaps more digestible format.
-}

-------------------------
-- * Adding φ constraints
--
-- Figure 7 in the LYG paper.

-- | A high-level pattern-match constraint. Corresponds to φ from Figure 3 of
-- the LYG paper.
data PhiCt
  = PhiTyCt !PredType
  -- ^ A type constraint "T ~ U".
  | PhiCoreCt    !Id !CoreExpr
  -- ^ @PhiCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@.
  | PhiConCt     !Id !PmAltCon ![TyVar] ![PredType] ![Id]
  -- ^ @PhiConCt x K tvs dicts ys@ encodes @K \@tvs dicts ys <- x@, matching @x@
  -- against the 'PmAltCon' application @K \@tvs dicts ys@, binding @tvs@,
  -- @dicts@ and possibly unlifted fields @ys@ in the process.
  -- See Note [Strict fields and variables of unlifted type].
  | PhiNotConCt  !Id !PmAltCon
  -- ^ @PhiNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed
  -- by @K@.
  | PhiBotCt     !Id
  -- ^ @PhiBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
  -- by @K@.
  | PhiNotBotCt !Id
  -- ^ @PhiNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥.

instance Outputable PhiCt where
  ppr :: PhiCt -> SDoc
ppr (PhiTyCt Type
ty_ct)                 = Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty_ct
  ppr (PhiCoreCt Id
x CoreExpr
e)                 = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'~' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e
  ppr (PhiConCt Id
x PmAltCon
con [Id]
tvs ThetaType
dicts [Id]
args) =
    [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
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_dicts [SDoc] -> [SDoc] -> [SDoc]
forall a. [a] -> [a] -> [a]
++ [SDoc]
pp_args) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"<-" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x
    where
      pp_tvs :: [SDoc]
pp_tvs   = (Id -> SDoc) -> [Id] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ((SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> Char -> SDoc
forall doc. IsLine doc => Char -> doc
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_dicts :: [SDoc]
pp_dicts = (Type -> SDoc) -> ThetaType -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr ThetaType
dicts
      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 (PhiNotConCt Id
x PmAltCon
con)             = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"≁" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> PmAltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmAltCon
con
  ppr (PhiBotCt Id
x)                    = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"~ ⊥"
  ppr (PhiNotBotCt Id
x)                 = Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"≁ ⊥"

type PhiCts = Bag PhiCt

-- | The fuel for the inhabitation test.
-- See Note [Fuel for the inhabitation test].
initFuel :: Int
initFuel :: Int
initFuel = Int
4 -- 4 because it's the smallest number that passes f' in T17977b

-- | Adds new constraints to 'Nabla' and returns 'Nothing' if that leads to a
-- contradiction.
--
-- In terms of the paper, this function models the \(⊕_φ\) function in
-- Figure 7 on batches of φ constraints.
addPhiCts :: Nabla -> PhiCts -> DsM (Maybe Nabla)
-- See Note [TmState invariants].
addPhiCts :: Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
nabla PhiCts
cts = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
 -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
forall a b. (a -> b) -> a -> b
$ do
  let (ThetaType
ty_cts, [PhiCt]
tm_cts) = PhiCts -> (ThetaType, [PhiCt])
partitionPhiCts PhiCts
cts
  nabla' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addTyCts Nabla
nabla (ThetaType -> Bag Type
forall a. [a] -> Bag a
listToBag ThetaType
ty_cts)
  nabla'' <- foldlM addPhiTmCt nabla' (listToBag tm_cts)
  inhabitationTest initFuel (nabla_ty_st nabla) nabla''

partitionPhiCts :: PhiCts -> ([PredType], [PhiCt])
partitionPhiCts :: PhiCts -> (ThetaType, [PhiCt])
partitionPhiCts = (PhiCt -> Either Type PhiCt) -> [PhiCt] -> (ThetaType, [PhiCt])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith PhiCt -> Either Type PhiCt
to_either ([PhiCt] -> (ThetaType, [PhiCt]))
-> (PhiCts -> [PhiCt]) -> PhiCts -> (ThetaType, [PhiCt])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PhiCts -> [PhiCt]
forall a. Bag a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
  where
    to_either :: PhiCt -> Either Type PhiCt
to_either (PhiTyCt Type
pred_ty) = Type -> Either Type PhiCt
forall a b. a -> Either a b
Left Type
pred_ty
    to_either PhiCt
ct                = PhiCt -> Either Type PhiCt
forall a b. b -> Either a b
Right PhiCt
ct

-----------------------------
-- ** Adding type constraints

-- | Adds new type-level constraints by calling out to the type-checker via
-- 'tyOracle'.
addTyCts :: Nabla -> Bag PredType -> MaybeT DsM Nabla
addTyCts :: Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addTyCts nabla :: Nabla
nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState
nabla_ty_st = TyState
ty_st } Bag Type
new_ty_cs = do
  ty_st' <- DsM (Maybe TyState)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TyState
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (TyState -> Bag Type -> DsM (Maybe TyState)
tyOracle TyState
ty_st Bag Type
new_ty_cs)
  pure nabla{ nabla_ty_st = ty_st' }

-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
-- find a contradiction (e.g. @Int ~ Bool@).
--
-- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
tyOracle :: TyState -> Bag Type -> DsM (Maybe TyState)
tyOracle ty_st :: TyState
ty_st@(TySt Int
n InertSet
inert) Bag Type
cts
  | Bag Type -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag Type
cts
  = Maybe TyState -> DsM (Maybe TyState)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyState -> Maybe TyState
forall a. a -> Maybe a
Just TyState
ty_st)
  | Bool
otherwise
  = {-# SCC "tyOracle" #-}
    do { evs <- (Type -> IOEnv (Env DsGblEnv DsLclEnv) 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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Bag a -> f (Bag b)
traverse Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
nameTyCt Bag Type
cts
       ; tracePm "tyOracle" (ppr n $$ ppr cts $$ ppr inert)
       ; mb_new_inert <- initTcDsForSolver $ tcCheckGivens inert evs
         -- return the new inert set and increment the sequence number n
       ; return (TySt (n+1) <$> mb_new_inert) }

-- | Allocates a fresh 'EvVar' name for 'PredTy's.
nameTyCt :: PredType -> DsM EvVar
nameTyCt :: Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
nameTyCt Type
pred_ty = do
  unique <- IOEnv (Env DsGblEnv DsLclEnv) Unique
forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM
  let 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))
  return (mkUserLocalOrCoVar occname unique ManyTy pred_ty noSrcSpan)

-----------------------------
-- ** Adding term constraints

-- | Adds a single higher-level φ constraint by dispatching to the various
-- oracle functions.
--
-- In terms of the paper, this function amounts to the constructor constraint
-- case of \(⊕_φ\) in Figure 7, which "desugars" higher-level φ constraints
-- into lower-level δ constraints. We don't have a data type for δ constraints
-- and call the corresponding oracle function directly instead.
--
-- Precondition: The φ is /not/ a type constraint! These should be handled by
-- 'addTyCts' before, through 'addPhiCts'.
addPhiTmCt :: Nabla -> PhiCt -> MaybeT DsM Nabla
addPhiTmCt :: Nabla -> PhiCt -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addPhiTmCt Nabla
_     (PhiTyCt Type
ct)              = String -> SDoc -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"addPhiCt:TyCt" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ct) -- See the precondition
addPhiTmCt Nabla
nabla (PhiCoreCt Id
x CoreExpr
e)           = Nabla
-> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addCoreCt Nabla
nabla Id
x CoreExpr
e
addPhiTmCt Nabla
nabla (PhiConCt Id
x PmAltCon
con [Id]
tvs ThetaType
dicts [Id]
args) = do
  -- Case (1) of Note [Strict fields and variables of unlifted type]
  -- PhiConCt correspond to the higher-level φ constraints from the paper with
  -- bindings semantics. It disperses into lower-level δ constraints that the
  -- 'add*Ct' functions correspond to.
  nabla' <- Nabla -> Bag Type -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addTyCts Nabla
nabla (ThetaType -> Bag Type
forall a. [a] -> Bag a
listToBag ThetaType
dicts)
  nabla'' <- addConCt nabla' x con tvs args
  foldlM addNotBotCt nabla'' (filterUnliftedFields con args)
addPhiTmCt Nabla
nabla (PhiNotConCt Id
x PmAltCon
con)       = Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
nabla Id
x PmAltCon
con
addPhiTmCt Nabla
nabla (PhiBotCt Id
x)              = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt Nabla
nabla Id
x
addPhiTmCt Nabla
nabla (PhiNotBotCt Id
x)           = Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt Nabla
nabla Id
x

filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
filterUnliftedFields PmAltCon
con [Id]
args =
  [ Id
arg | (Id
arg, HsImplBang
bang) <- String -> [Id] -> [HsImplBang] -> [(Id, HsImplBang)]
forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
zipEqual String
"addPhiCt" [Id]
args (PmAltCon -> [HsImplBang]
pmAltConImplBangs PmAltCon
con)
        , HsImplBang -> Bool
isBanged HsImplBang
bang Bool -> Bool -> Bool
|| Type -> Bool
definitelyUnliftedType (Id -> Type
idType Id
arg) ]

-- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@
-- surely diverges. Quite similar to 'addConCt', only that it only cares about
-- ⊥.
addBotCt :: Nabla -> Id -> MaybeT DsM Nabla
addBotCt :: Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts=UniqSDFM Id VarInfo
env } } Id
x = do
  let (Id
y, vi :: VarInfo
vi@VI { vi_bot :: VarInfo -> BotInfo
vi_bot = BotInfo
bot }) = TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x
  case BotInfo
bot of
    BotInfo
IsNotBot -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero      -- There was x ≁ ⊥. Contradiction!
    BotInfo
IsBot    -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla -- There already is x ~ ⊥. Nothing left to do
    BotInfo
MaybeBot               -- We add x ~ ⊥
      | Type -> Bool
definitelyUnliftedType (Id -> Type
idType Id
x)
      -- Case (3) in Note [Strict fields and variables of unlifted type]
      -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- unlifted vars can never be ⊥
      | Bool
otherwise
      -> do
          let vi' :: VarInfo
vi' = VarInfo
vi{ vi_bot = IsBot }
          Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env y vi' } }

-- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt',
-- but only cares for the ⊥ "constructor".
addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla
addNotBotCt :: Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts=UniqSDFM Id VarInfo
env} } Id
x = do
  let (Id
y, vi :: VarInfo
vi@VI { vi_bot :: VarInfo -> BotInfo
vi_bot = BotInfo
bot }) = TmState -> Id -> (Id, VarInfo)
lookupVarInfoNT (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x
  case BotInfo
bot of
    BotInfo
IsBot    -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero      -- There was x ~ ⊥. Contradiction!
    BotInfo
IsNotBot -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla -- There already is x ≁ ⊥. Nothing left to do
    BotInfo
MaybeBot -> do         -- We add x ≁ ⊥ and test if x is still inhabited
      -- Mark dirty for a delayed inhabitation test
      let vi' :: VarInfo
vi' = VarInfo
vi{ vi_bot = IsNotBot}
      Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a b. (a -> b) -> a -> b
$ Id -> Nabla -> Nabla
markDirty Id
y
           (Nabla -> Nabla) -> Nabla -> Nabla
forall a b. (a -> b) -> a -> b
$ Nabla
nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env y vi' } }

-- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't
-- take the shape of a 'PmAltCon' @K@ in the 'Nabla' and return @Nothing@ if
-- that leads to a contradiction.
-- See Note [TmState invariants].
addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
addNotConCt :: Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
_     Id
_ (PmAltConLike (RealDataCon DataCon
dc))
  | DataCon -> Bool
isNewDataCon DataCon
dc = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero -- (3) in Note [Coverage checking Newtype matches]
addNotConCt Nabla
nabla Id
x PmAltCon
nalt = do
  (mb_mark_dirty, nabla') <- (VarInfo
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo))
-> Nabla
-> Id
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, Nabla)
forall (f :: * -> *) a.
Functor f =>
(VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo)
go Nabla
nabla Id
x
  pure $ case mb_mark_dirty of
    Just Id
x  -> Id -> Nabla -> Nabla
markDirty Id
x Nabla
nabla'
    Maybe Id
Nothing -> Nabla
nabla'
  where
    -- Update `x`'s 'VarInfo' entry. Fail ('MaybeT') if contradiction,
    -- otherwise return updated entry and `Just x'` if `x` should be marked dirty,
    -- where `x'` is the representative of `x`.
    go :: VarInfo -> MaybeT DsM (Maybe Id, VarInfo)
    go :: VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe Id, VarInfo)
go vi :: VarInfo
vi@(VI Id
x' [PmAltConApp]
pos PmAltConSet
neg BotInfo
_ ResidualCompleteMatches
rcm) = do
      -- 1. Bail out quickly when nalt contradicts a solution
      let contradicts :: PmAltCon -> PmAltConApp -> Bool
contradicts PmAltCon
nalt PmAltConApp
sol = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon (PmAltConApp -> PmAltCon
paca_con PmAltConApp
sol) PmAltCon
nalt PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Equal
      Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not ((PmAltConApp -> Bool) -> [PmAltConApp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> PmAltConApp -> Bool
contradicts PmAltCon
nalt) [PmAltConApp]
pos))
      -- 2. Only record the new fact when it's not already implied by one of the
      -- solutions
      let implies :: PmAltCon -> PmAltConApp -> Bool
implies PmAltCon
nalt PmAltConApp
sol = PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon (PmAltConApp -> PmAltCon
paca_con PmAltConApp
sol) PmAltCon
nalt PmEquality -> PmEquality -> Bool
forall a. Eq a => a -> a -> Bool
== PmEquality
Disjoint
      let neg' :: PmAltConSet
neg'
            | (PmAltConApp -> Bool) -> [PmAltConApp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> PmAltConApp -> Bool
implies PmAltCon
nalt) [PmAltConApp]
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
      Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
forall (m :: * -> *). (HasCallStack, Applicative m) => Bool -> m ()
massert (PmAltCon -> Bool
isPmAltConMatchStrict PmAltCon
nalt)
      let vi' :: VarInfo
vi' = VarInfo
vi{ vi_neg = neg', vi_bot = IsNotBot }
      -- 3. Make sure there's at least one other possible constructor
      mb_rcm' <- DsM (Maybe ResidualCompleteMatches)
-> MaybeT
     (IOEnv (Env DsGblEnv DsLclEnv)) (Maybe ResidualCompleteMatches)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (PmAltCon
-> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
markMatched PmAltCon
nalt ResidualCompleteMatches
rcm)
      pure $ case mb_rcm' of
        -- If nalt could be removed from a COMPLETE set, we'll get back Just and
        -- have to mark x dirty, by returning Just x'.
        Just ResidualCompleteMatches
rcm' -> (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
x',  VarInfo
vi'{ vi_rcm = rcm' })
        -- Otherwise, nalt didn't occur in any residual COMPLETE set and we
        -- don't have to mark it dirty. So we return Nothing, which in the case
        -- above would have compromised precision.
        -- See Note [Shortcutting the inhabitation test], grep for T17836.
        Maybe ResidualCompleteMatches
Nothing   -> (Maybe Id
forall a. Maybe a
Nothing, VarInfo
vi')

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

-- | 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 :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla
addConCt :: Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts=UniqSDFM Id VarInfo
env } } Id
x PmAltCon
alt [Id]
tvs [Id]
args = do
  let vi :: VarInfo
vi@(VI Id
_ [PmAltConApp]
pos PmAltConSet
neg BotInfo
bot ResidualCompleteMatches
_) = TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x
  -- First try to refute with a negative fact
  Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) ()
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 (IOEnv (Env DsGblEnv DsLclEnv)) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard ((PmAltConApp -> Bool) -> [PmAltConApp] -> 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)
-> (PmAltConApp -> PmEquality) -> PmAltConApp -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt (PmAltCon -> PmEquality)
-> (PmAltConApp -> PmAltCon) -> PmAltConApp -> PmEquality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltConApp -> PmAltCon
paca_con) [PmAltConApp]
pos)
  -- Now we should be good! Add (alt, tvs, args) as a possible solution, or
  -- refine an existing one
  case (PmAltConApp -> Bool) -> [PmAltConApp] -> Maybe PmAltConApp
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)
-> (PmAltConApp -> PmEquality) -> PmAltConApp -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltCon -> PmAltCon -> PmEquality
eqPmAltCon PmAltCon
alt (PmAltCon -> PmEquality)
-> (PmAltConApp -> PmAltCon) -> PmAltConApp -> PmEquality
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltConApp -> PmAltCon
paca_con) [PmAltConApp]
pos of
    Just (PACA PmAltCon
_con [Id]
other_tvs [Id]
other_args) -> do
      -- We must unify existentially bound ty vars and arguments!
      let ty_cts :: [PhiCt]
ty_cts = ThetaType -> ThetaType -> [PhiCt]
equateTys ((Id -> Type) -> [Id] -> ThetaType
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
tvs) ((Id -> Type) -> [Id] -> ThetaType
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
other_tvs)
      nabla' <- IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a b. (a -> b) -> a -> b
$ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
nabla ([PhiCt] -> PhiCts
forall a. [a] -> Bag a
listToBag [PhiCt]
ty_cts)
      let add_var_ct Nabla
nabla (Id
a, Id
b) = Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt Nabla
nabla Id
a Id
b
      foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args
    Maybe PmAltConApp
Nothing -> do
      let pos' :: [PmAltConApp]
pos' = PmAltCon -> [Id] -> [Id] -> PmAltConApp
PACA PmAltCon
alt [Id]
tvs [Id]
args PmAltConApp -> [PmAltConApp] -> [PmAltConApp]
forall a. a -> [a] -> [a]
: [PmAltConApp]
pos
      let nabla_with :: BotInfo -> Nabla
nabla_with BotInfo
bot' =
            Nabla
nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
      -- Do (2) in Note [Coverage checking Newtype matches]
      case (PmAltCon
alt, [Id]
args) of
        (PmAltConLike (RealDataCon DataCon
dc), [Id
y]) | DataCon -> Bool
isNewDataCon DataCon
dc ->
          case BotInfo
bot of
            BotInfo
MaybeBot -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BotInfo -> Nabla
nabla_with BotInfo
MaybeBot)
            BotInfo
IsBot    -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt (BotInfo -> Nabla
nabla_with BotInfo
MaybeBot) Id
y
            BotInfo
IsNotBot -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt (BotInfo -> Nabla
nabla_with BotInfo
MaybeBot) Id
y
        (PmAltCon, [Id])
_ -> Bool
-> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> Nabla
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. HasCallStack => Bool -> a -> a
assert (PmAltCon -> Bool
isPmAltConMatchStrict PmAltCon
alt )
             Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BotInfo -> Nabla
nabla_with BotInfo
IsNotBot) -- strict match ==> not ⊥

equateTys :: [Type] -> [Type] -> [PhiCt]
equateTys :: ThetaType -> ThetaType -> [PhiCt]
equateTys ThetaType
ts ThetaType
us =
  [ Type -> PhiCt
PhiTyCt (Type -> Type -> Type
mkNomEqPred Type
t Type
u)
  | (Type
t, Type
u) <- String -> ThetaType -> ThetaType -> [(Type, Type)]
forall a b. HasDebugCallStack => String -> [a] -> [b] -> [(a, b)]
zipEqual String
"equateTys" ThetaType
ts ThetaType
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 (HasCallStack => Type -> Type -> Bool
Type -> Type -> Bool
eqType Type
t Type
u)
  ]

-- | Adds a @x ~ y@ constraint by merging the two 'VarInfo's and record the
-- gained knowledge in 'Nabla'.
--
-- Returns @Nothing@ when there's a contradiction while merging. Returns @Just
-- nabla@ when the constraint was compatible with prior facts, in which case
-- @nabla@ has integrated the knowledge from the equality constraint.
--
-- See Note [TmState invariants].
addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
addVarCt :: Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env } } Id
x Id
y =
  case UniqSDFM Id VarInfo
-> Id -> Id -> (Maybe VarInfo, UniqSDFM Id VarInfo)
forall key ele.
Uniquable key =>
UniqSDFM key ele -> key -> key -> (Maybe ele, UniqSDFM key ele)
equateUSDFM UniqSDFM Id VarInfo
env Id
x Id
y of
    (Maybe VarInfo
Nothing,   UniqSDFM Id VarInfo
env') -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nabla
nabla{ nabla_tm_st = ts{ ts_facts = env' } })
    -- Add the constraints we had for x to y
    (Just VarInfo
vi_x, UniqSDFM Id VarInfo
env') -> do
      let nabla_equated :: Nabla
nabla_equated = Nabla
nabla{ nabla_tm_st = ts{ts_facts = env'} }
      -- and then gradually merge every positive fact we have on x into y
      let add_pos :: Nabla
-> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_pos Nabla
nabla (PACA PmAltCon
cl [Id]
tvs [Id]
args) = Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt Nabla
nabla Id
y PmAltCon
cl [Id]
tvs [Id]
args
      nabla_pos <- (Nabla
 -> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> Nabla
-> [PmAltConApp]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM Nabla
-> PmAltConApp -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
add_pos Nabla
nabla_equated (VarInfo -> [PmAltConApp]
vi_pos VarInfo
vi_x)
      -- Do the same for negative info
      let add_neg Nabla
nabla PmAltCon
nalt = Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
nabla Id
y PmAltCon
nalt
      foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x))

-- | 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 :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla
addCoreCt :: Nabla
-> Id -> CoreExpr -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addCoreCt Nabla
nabla Id
x CoreExpr
e = do
  simpl_opts <- DynFlags -> SimpleOpts
initSimpleOpts (DynFlags -> SimpleOpts)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) DynFlags
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) SimpleOpts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  let e' = HasDebugCallStack => SimpleOpts -> CoreExpr -> CoreExpr
SimpleOpts -> CoreExpr -> CoreExpr
simpleOptExpr SimpleOpts
simpl_opts CoreExpr
e
  -- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
  execStateT (core_expr x e') nabla
  where
    -- Takes apart a 'CoreExpr' and tries to extract as much information about
    -- literals and constructor applications as possible.
    core_expr :: Id -> CoreExpr -> StateT Nabla (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 Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x (Cast CoreExpr
e Coercion
_co) = Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
core_expr Id
x CoreExpr
e
    core_expr Id
x (Tick CoreTickish
_t CoreExpr
e) = Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
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 HasCallStack => Type -> Type -> Bool
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 Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
data_con_app Id
x InScopeSet
emptyInScopeSet DataCon
nilDataCon []
          String
s' -> Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
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 Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_lit Id
x PmLit
lit
      | Just (InScopeSet
in_scope, _empty_floats :: [FloatBind]
_empty_floats@[], DataCon
dc, ThetaType
_arg_tys, [CoreExpr]
args)
            <- HasDebugCallStack =>
InScopeEnv
-> CoreExpr
-> Maybe (InScopeSet, [FloatBind], DataCon, ThetaType, [CoreExpr])
InScopeEnv
-> CoreExpr
-> Maybe (InScopeSet, [FloatBind], DataCon, ThetaType, [CoreExpr])
exprIsConApp_maybe InScopeEnv
in_scope_env CoreExpr
e
      = Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
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
      = (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT (\Nabla
nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt Nabla
nabla 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 Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
equate_with_similar_expr Id
x CoreExpr
e
      where
        expr_ty :: Type
expr_ty       = HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e
        expr_in_scope :: InScopeSet
expr_in_scope = VarSet -> InScopeSet
mkInScopeSet (CoreExpr -> VarSet
exprFreeVars CoreExpr
e)
        in_scope_env :: InScopeEnv
in_scope_env  = InScopeSet -> IdUnfoldingFun -> InScopeEnv
ISE InScopeSet
expr_in_scope IdUnfoldingFun
noUnfoldingFun
        -- 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 Nabla (MaybeT DsM) ()
    equate_with_similar_expr :: Id
-> CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
equate_with_similar_expr Id
x CoreExpr
e = do
      rep <- (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla))
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla))
 -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id)
-> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla))
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> DsM (Id, Nabla)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr Nabla
nabla CoreExpr
e)
      -- Note that @rep == x@ if we encountered @e@ for the first time.
      modifyT (\Nabla
nabla -> Nabla -> Id -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addVarCt Nabla
nabla Id
x Id
rep)

    bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id
    bind_expr :: CoreExpr
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
bind_expr CoreExpr
e = do
      x <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) Id
forall (m :: * -> *) a. Monad m => m a -> StateT Nabla m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOEnv (Env DsGblEnv DsLclEnv) Id
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
mkPmId (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e)))
      core_expr x e
      pure x

    -- Look at @let x = K taus theta es@ and generate the following
    -- constraints (assuming universals were dropped from @taus@ before):
    --   1. @x ≁ ⊥@ if 'K' is not a Newtype constructor.
    --   2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@
    --   3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
    --   4. @x ~ K as ys@
    -- This is quite similar to PmCheck.pmConCts.
    data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) ()
    data_con_app :: Id
-> InScopeSet
-> DataCon
-> [CoreExpr]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
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 :: ThetaType
ex_tys                 = (CoreExpr -> Type) -> [CoreExpr] -> ThetaType
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
      uniq_supply <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply
forall (m :: * -> *) a. Monad m => m a -> StateT Nabla m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
 -> StateT
      Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) UniqSupply
forall a b. (a -> b) -> a -> b
$ DsM UniqSupply -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (DsM UniqSupply
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply)
-> DsM UniqSupply
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) UniqSupply
forall a b. (a -> b) -> a -> b
$ DsM UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
      let (_, ex_tvs) = cloneTyVarBndrs (mkEmptySubst in_scope) dc_ex_tvs uniq_supply
          ty_cts      = ThetaType -> ThetaType -> [PhiCt]
equateTys ((Id -> Type) -> [Id] -> ThetaType
forall a b. (a -> b) -> [a] -> [b]
map Id -> Type
mkTyVarTy [Id]
ex_tvs) ThetaType
ex_tys
      -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor (#18341)
      when (not (isNewDataCon dc)) $
        modifyT $ \Nabla
nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt Nabla
nabla Id
x
      -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703
      modifyT $ \Nabla
nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a b. (a -> b) -> a -> b
$ Nabla -> PhiCts -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
addPhiCts Nabla
nabla ([PhiCt] -> PhiCts
forall a. [a] -> Bag a
listToBag [PhiCt]
ty_cts)
      -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
      arg_ids <- traverse bind_expr vis_args
      -- 4. @x ~ K as ys@
      pm_alt_con_app x (PmAltConLike (RealDataCon dc)) ex_tvs arg_ids

    -- Adds a literal constraint, i.e. @x ~ 42@.
    -- Also we assume that literal expressions won't diverge, so this
    -- will add a @x ~/ ⊥@ constraint.
    pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT DsM) ()
    pm_lit :: Id
-> PmLit
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_lit Id
x PmLit
lit = do
      (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
 -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ())
-> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotBotCt Nabla
nabla Id
x
      Id
-> PmAltCon
-> [Id]
-> [Id]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
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 Nabla (MaybeT DsM) ()
    pm_alt_con_app :: Id
-> PmAltCon
-> [Id]
-> [Id]
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
pm_alt_con_app Id
x PmAltCon
con [Id]
tvs [Id]
args = (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall (m :: * -> *) s. Monad m => (s -> m s) -> StateT s m ()
modifyT ((Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
 -> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ())
-> (Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> StateT Nabla (MaybeT (IOEnv (Env DsGblEnv DsLclEnv))) ()
forall a b. (a -> b) -> a -> b
$ \Nabla
nabla -> Nabla
-> Id
-> PmAltCon
-> [Id]
-> [Id]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addConCt Nabla
nabla 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 a b. (a -> b) -> m a -> m b
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

-- | 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 :: Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
representCoreExpr nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_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
key = (Id, Nabla) -> DsM (Id, Nabla)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
rep, Nabla
nabla)
  | Bool
otherwise = do
      rep <- Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
mkPmId (HasDebugCallStack => CoreExpr -> Type
CoreExpr -> Type
exprType CoreExpr
e)
      let reps'  = CoreMap Id -> CoreExpr -> Id -> CoreMap Id
forall a. CoreMap a -> CoreExpr -> a -> CoreMap a
extendCoreMap CoreMap Id
reps CoreExpr
key Id
rep
      let nabla' = Nabla
nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
      pure (rep, nabla')
  where
    key :: CoreExpr
key = CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
e
      -- Use a key in which dictionaries for the same type become equal.
      -- See Note [Unique dictionaries in the TmOracle CoreMap]

-- | Change out 'Id's which are uniquely determined by their type to a
-- common value, so that different names for dictionaries of the same type
-- are considered equal when building a 'CoreMap'.
--
-- See Note [Unique dictionaries in the TmOracle CoreMap]
makeDictsCoherent :: CoreExpr -> CoreExpr
makeDictsCoherent :: CoreExpr -> CoreExpr
makeDictsCoherent var :: CoreExpr
var@(Var Id
v)
  | let ty :: Type
ty = Id -> Type
idType Id
v
  , Type -> Bool
typeDeterminesValue Type
ty
  = Type -> String -> CoreExpr
mkImpossibleExpr Type
ty String
"Solver.makeDictsCoherent"
  | Bool
otherwise
  = CoreExpr
var
makeDictsCoherent lit :: CoreExpr
lit@(Lit {})
  = CoreExpr
lit
makeDictsCoherent (App CoreExpr
f CoreExpr
a)
  = CoreExpr -> CoreExpr -> CoreExpr
forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
f) (CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
a)
makeDictsCoherent (Lam Id
f CoreExpr
body)
  = Id -> CoreExpr -> CoreExpr
forall b. b -> Expr b -> Expr b
Lam Id
f (CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
body)
makeDictsCoherent (Let Bind Id
bndr CoreExpr
body)
  = Bind Id -> CoreExpr -> CoreExpr
forall b. Bind b -> Expr b -> Expr b
Let
      (Bind Id -> Bind Id
go_bndr Bind Id
bndr)
      (CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
body)
  where
    go_bndr :: Bind Id -> Bind Id
go_bndr (NonRec Id
bndr CoreExpr
expr) = Id -> CoreExpr -> Bind Id
forall b. b -> Expr b -> Bind b
NonRec Id
bndr (CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
expr)
    go_bndr (Rec [(Id, CoreExpr)]
bndrs) = [(Id, CoreExpr)] -> Bind Id
forall b. [(b, Expr b)] -> Bind b
Rec (((Id, CoreExpr) -> (Id, CoreExpr))
-> [(Id, CoreExpr)] -> [(Id, CoreExpr)]
forall a b. (a -> b) -> [a] -> [b]
map ( \(Id
b, CoreExpr
expr) -> (Id
b, CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
expr) ) [(Id, CoreExpr)]
bndrs)
makeDictsCoherent (Case CoreExpr
scrut Id
bndr Type
ty [Alt Id]
alts)
  = CoreExpr -> Id -> Type -> [Alt Id] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
scrut Id
bndr Type
ty
      [ AltCon -> [Id] -> CoreExpr -> Alt Id
forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
con [Id]
bndr CoreExpr
expr'
      | Alt AltCon
con [Id]
bndr CoreExpr
expr <- [Alt Id]
alts
      , let expr' :: CoreExpr
expr' = CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
expr ]
makeDictsCoherent (Cast CoreExpr
expr Coercion
co)
  = CoreExpr -> Coercion -> CoreExpr
forall b. Expr b -> Coercion -> Expr b
Cast (CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
expr) Coercion
co
makeDictsCoherent (Tick CoreTickish
tick CoreExpr
expr)
  = CoreTickish -> CoreExpr -> CoreExpr
forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
tick (CoreExpr -> CoreExpr
makeDictsCoherent CoreExpr
expr)
makeDictsCoherent ty :: CoreExpr
ty@(Type {})
  = CoreExpr
ty
makeDictsCoherent co :: CoreExpr
co@(Coercion {})
  = CoreExpr
co

{- Note [Unique dictionaries in the TmOracle CoreMap]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Any two dictionaries for a coherent typeclass should be considered equal
in the TmOracle CoreMap, as this allows us to report better pattern-match
warnings.

Consider for example T21662:

  view_fn :: forall (n :: Nat). KnownNat n => Int -> Bool

  foo :: Int -> Int
  foo (view_fn @12 -> True ) = 0
  foo (view_fn @12 -> False) = 1

In this example, the pattern match is exhaustive because we have covered
the range of the view pattern function. However, we may fail to recognise
the fact that the two cases use the same view function if the KnownNat
dictionaries aren't syntactically equal:

  eqn 1: [let ds_d1p0 = view_fn @12 $dKnownNat_a1ny ds_d1oR,  True <- ds_d1p0]
  eqn 2: [let ds_d1p6 = view_fn @12 $dKnownNat_a1nC ds_d1oR, False <- ds_d1p6]

Note that the uniques of the KnownNat 12 dictionary differ. If we fail to utilise
the coherence of the KnownNat constraint, then we have to pessimistically assume
that we have two function calls with different arguments:

  foo (fn arg1 -> True ) = ...
  foo (fn arg2 -> False) = ...

In this case we can't determine whether the pattern matches are complete, so we
emit a pattern match warning.

Solution: replace all 'Id's whose type uniquely determines its value with
a common value, e.g. in the above example we would replace both
$dKnownNat_a1ny and $dKnownNat_a1nC with error @(KnownNat 12).

Why did we choose this solution? Here are some alternatives that were considered:

  1. Perform CSE first. This would common up the dictionaries before we compare
     using the CoreMap.
     However, this is architecturally difficult as it would require threading
     a CSEnv through to desugarPat.
  2. Directly modify CoreMap so that any two dictionaries of the same type are
     considered equal.
     The problem is that this affects all users of CoreMap. For example, CSE
     would now assume that any two dictionaries of the same type are equal,
     but this isn't necessarily true in the presence of magicDict, which
     violates coherence by design. It seems more prudent to limit the changes
     to the pattern-match checker only, to avoid undesirable consequences.

In the end, replacing dictionaries with an error value in the pattern-match
checker was the most self-contained, although we might want to revisit once
we implement a more robust approach to computing equality in the pattern-match
checker (see #19272).
-}

{- Note [The Pos/Neg invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Invariant applying to each VarInfo: Whenever we have @C @tvs args@ 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 orthogonal.
  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_rcm, which essentially stores positive
information. We make sure that vi_neg and vi_rcm never overlap. This isn't
strictly necessary since vi_rcm is just a cache, so doesn't need to be
accurate: Every suggestion of a possible ConLike from vi_rcm 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 or doing inhabitation testing) contradictory. This implies a few
invariants:
* Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute.
  This is implied by the Note [The Pos/Neg invariant].
* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_rcm 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).

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.

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'.

Note [Strict fields and variables of unlifted type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Binders of unlifted type (and strict fields) are unlifted by construction;
they are conceived with an implicit (but delayed checked) @≁⊥@ constraint to
begin with. Hence, desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned
by strict fields, since the forcing happens *before* pattern matching. And
the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.checkGrd' have
complex binding semantics (binding type constraints and unlifted fields), so
unliftedness semantics are entirely confined to the oracle.

These are the moving parts:

  1.  For each strict (or more generally, unlifted) field @s@ of a 'PhiConCt'
      we have to add a @s ≁ ⊥@ constraint in the corresponding case of
      'addPhiTmCt'. Strict fields are devoid of ⊥ by construction, there's
      nothing that a bang pattern would act on. Example from #18341:

        data T = MkT !Int
        f :: T -> ()
        f (MkT  _) | False = () -- inaccessible
        f (MkT !_) | False = () -- redundant, not only inaccessible!
        f _                = ()

      The second clause desugars to @MkT n <- x, !n@. When coverage checked,
      the 'PmCon' @MkT n <- x@ refines the set of values that reach the bang
      pattern with the φ constraints @MkT n <- x@ (Nothing surprising so far).
      Upon that constraint, it disperses into two lower-level δ constraints
      @x ~ MkT n, n ≁ ⊥@ per Equation (3) in Figure 7 of the paper.

      Checking the 'PmBang' @!n@ will then try to add the
      constraint @n ~ ⊥@ to this set to get the diverging set, which is found
      to be empty. Hence the whole clause is detected as redundant, as
      expected.

  2.  Similarly, when performing the 'inhabitationTest', when instantiating a
      constructor we call 'instCon', which generates a higher-level φ
      constructor constraint.

  3.  The preceding points handle unlifted constructor fields, but there also
      are regular binders of unlifted type. We simply fail in 'addBotCt' for
      any binder of unlifted type.
      It would be enough to check for unliftedness once, when the binder comes
      into scope, but we haven't really a way to track that.

  4.  Why not start an 'emptyVarInfo' of unlifted type with @vi_bot = IsNotBot@?
      Because then we'd need to trigger an inhabitation test, because the var
      might actually be void to begin with. But we can't trigger the test from
      'emptyVarInfo'.
      Historically, that is what we did and not doing the test led to #20631,
      where 'addNotBotCt' trivially succeeded, because the 'VarInfo' already
      said 'IsNotBot', implying that a prior inhabitation test succeeded.
-}

-------------------------
-- * Inhabitation testing
--
-- Figure 8 in the LYG paper.

tyStateRefined :: TyState -> TyState -> Bool
-- Makes use of the fact that the two TyStates we compare will never have the
-- same sequence number. It is invalid to call this function when a is not a
-- refinement of b or vice versa!
tyStateRefined :: TyState -> TyState -> Bool
tyStateRefined TyState
a TyState
b = TyState -> Int
ty_st_n TyState
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= TyState -> Int
ty_st_n TyState
b

markDirty :: Id -> Nabla -> Nabla
markDirty :: Id -> Nabla -> Nabla
markDirty Id
x nabla :: Nabla
nabla@MkNabla{nabla_tm_st :: Nabla -> TmState
nabla_tm_st = ts :: TmState
ts@TmSt{ts_dirty :: TmState -> DIdSet
ts_dirty = DIdSet
dirty} } =
  Nabla
nabla{ nabla_tm_st = ts{ ts_dirty = extendDVarSet dirty x } }

traverseDirty :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
traverseDirty :: forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseDirty VarInfo -> m VarInfo
f ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env, ts_dirty :: TmState -> DIdSet
ts_dirty = DIdSet
dirty} =
  [Id] -> UniqSDFM Id VarInfo -> m TmState
go (DIdSet -> [Id]
forall a. UniqDSet a -> [a]
uniqDSetToList DIdSet
dirty) UniqSDFM Id VarInfo
env
  where
    go :: [Id] -> UniqSDFM Id VarInfo -> m TmState
go []     UniqSDFM Id VarInfo
env  = TmState -> m TmState
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TmState
ts{ts_facts=env}
    go (Id
x:[Id]
xs) !UniqSDFM Id VarInfo
env = do
      vi' <- VarInfo -> m VarInfo
f (TmState -> Id -> VarInfo
lookupVarInfo TmState
ts Id
x)
      go xs (addToUSDFM env x vi')

traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll :: forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll VarInfo -> m VarInfo
f ts :: TmState
ts@TmSt{ts_facts :: TmState -> UniqSDFM Id VarInfo
ts_facts = UniqSDFM Id VarInfo
env} = do
  env' <- (VarInfo -> m VarInfo)
-> UniqSDFM Id VarInfo -> m (UniqSDFM Id VarInfo)
forall key a b (f :: * -> *).
Applicative f =>
(a -> f b) -> UniqSDFM key a -> f (UniqSDFM key b)
traverseUSDFM VarInfo -> m VarInfo
f UniqSDFM Id VarInfo
env
  pure ts{ts_facts = env'}

-- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate
-- all dirty variables (or all variables when the 'TyState' changed) to concrete
-- inhabitants. It returns a 'Nabla' with the *same* inhabitants, but with some
-- amount of work cached (like failed instantiation attempts) from the test.
--
-- The \(∇ ⊢ x inh\) judgment form in Figure 8 of the LYG paper.
inhabitationTest :: Int -> TyState -> Nabla -> MaybeT DsM Nabla
inhabitationTest :: Int
-> TyState -> Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
inhabitationTest Int
0     TyState
_         Nabla
nabla             = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
inhabitationTest Int
fuel  TyState
old_ty_st nabla :: Nabla
nabla@MkNabla{ nabla_tm_st :: Nabla -> TmState
nabla_tm_st = TmState
ts } = {-# SCC "inhabitationTest" #-} do
  -- lift $ tracePm "inhabitation test" $ vcat
  --   [ ppr fuel
  --   , ppr old_ty_st
  --   , ppr nabla
  --   , text "tyStateRefined:" <+> ppr (tyStateRefined old_ty_st (nabla_ty_st nabla))
  --   ]
  -- When type state didn't change, we only need to traverse dirty VarInfos
  ts' <- if TyState -> TyState -> Bool
tyStateRefined TyState
old_ty_st (Nabla -> TyState
nabla_ty_st Nabla
nabla)
            then (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
-> TmState -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TmState
forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseAll   VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
test_one TmState
ts
            else (VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
-> TmState -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) TmState
forall (m :: * -> *).
Monad m =>
(VarInfo -> m VarInfo) -> TmState -> m TmState
traverseDirty VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
test_one TmState
ts
  pure nabla{ nabla_tm_st = ts'{ts_dirty=emptyDVarSet}}
  where
    nabla_not_dirty :: Nabla
nabla_not_dirty = Nabla
nabla{ nabla_tm_st = ts{ts_dirty=emptyDVarSet} }
    test_one :: VarInfo -> MaybeT DsM VarInfo
    test_one :: VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
test_one VarInfo
vi =
      DsM Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TyState -> Nabla -> VarInfo -> DsM Bool
varNeedsTesting TyState
old_ty_st Nabla
nabla VarInfo
vi) MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Bool
-> (Bool -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall a b.
MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
-> (a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Bool
True -> do
          -- lift $ tracePm "test_one" (ppr vi)
          -- No solution yet and needs testing
          -- We have to test with a Nabla where all dirty bits are cleared
          Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instantiate (Int
fuelInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Nabla
nabla_not_dirty VarInfo
vi
        Bool
_ -> VarInfo -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarInfo
vi

-- | Checks whether the given 'VarInfo' needs to be tested for inhabitants.
-- Returns `False` when we can skip the inhabitation test, presuming it would
-- say "yes" anyway. See Note [Shortcutting the inhabitation test].
varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
varNeedsTesting TyState
_         MkNabla{nabla_tm_st :: Nabla -> TmState
nabla_tm_st=TmState
tm_st}     VarInfo
vi
  | Id -> DIdSet -> Bool
elemDVarSet (VarInfo -> Id
vi_id VarInfo
vi) (TmState -> DIdSet
ts_dirty TmState
tm_st) = Bool -> DsM Bool
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
varNeedsTesting TyState
_         Nabla
_                              VarInfo
vi
  | [PmAltConApp] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull (VarInfo -> [PmAltConApp]
vi_pos VarInfo
vi)                     = Bool -> DsM Bool
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
varNeedsTesting TyState
old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState
nabla_ty_st=TyState
new_ty_st} VarInfo
_
  -- Same type state => still inhabited
  | Bool -> Bool
not (TyState -> TyState -> Bool
tyStateRefined TyState
old_ty_st TyState
new_ty_st) = Bool -> DsM Bool
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
varNeedsTesting TyState
old_ty_st MkNabla{nabla_ty_st :: Nabla -> TyState
nabla_ty_st=TyState
new_ty_st} VarInfo
vi = do
  -- These normalisations are relatively expensive, but still better than having
  -- to perform a full inhabitation test
  (_, _, old_norm_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 TyState
old_ty_st (Id -> Type
idType (Id -> Type) -> Id -> Type
forall a b. (a -> b) -> a -> b
$ VarInfo -> Id
vi_id VarInfo
vi)
  (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (idType $ vi_id vi)
  if old_norm_ty `eqType` new_norm_ty
    then pure False
    else pure True

-- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE
-- set satisfies the oracle
--
-- Internally uses and updates the CompleteMatchs in vi_rcm.
--
-- NB: Does /not/ filter each CompleteMatch with the oracle; members may
--     remain that do not satisfy it.  This lazy approach just
--     avoids doing unnecessary work.
instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
instantiate :: Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instantiate Int
fuel Nabla
nabla VarInfo
vi = {-# SCC "instantiate" #-}
  (Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instBot Int
fuel Nabla
nabla VarInfo
vi MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
forall a.
MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instCompleteSets Int
fuel Nabla
nabla VarInfo
vi)

-- | The \(⊢_{Bot}\) rule from the paper
instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
instBot :: Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instBot Int
_fuel Nabla
nabla VarInfo
vi = {-# SCC "instBot" #-} do
  _nabla' <- Nabla -> Id -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addBotCt Nabla
nabla (VarInfo -> Id
vi_id VarInfo
vi)
  pure vi

addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
addNormalisedTypeMatches nabla :: Nabla
nabla@MkNabla{ nabla_ty_st :: Nabla -> TyState
nabla_ty_st = TyState
ty_st } Id
x
  = (VarInfo
 -> IOEnv
      (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo))
-> Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
forall (f :: * -> *) a.
Functor f =>
(VarInfo -> f (a, VarInfo)) -> Nabla -> Id -> f (a, Nabla)
trvVarInfo VarInfo
-> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
add_matches Nabla
nabla Id
x
  where
    add_matches :: VarInfo
-> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
add_matches vi :: VarInfo
vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
rcm }
      -- important common case, shaving down allocations of PmSeriesG by -5%
      | ResidualCompleteMatches -> Bool
isRcmInitialised ResidualCompleteMatches
rcm = (ResidualCompleteMatches, VarInfo)
-> IOEnv (Env DsGblEnv DsLclEnv) (ResidualCompleteMatches, VarInfo)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResidualCompleteMatches
rcm, VarInfo
vi)
    add_matches vi :: VarInfo
vi@VI{ vi_rcm :: VarInfo -> ResidualCompleteMatches
vi_rcm = ResidualCompleteMatches
rcm } = do
      norm_res_ty <- TyState -> Type -> DsM Type
normaliseSourceTypeWHNF TyState
ty_st (Id -> Type
idType Id
x)
      env <- dsGetFamInstEnvs
      rcm' <- case splitReprTyConApp_maybe env norm_res_ty of
        Just (TyCon
rep_tc, ThetaType
_args, Coercion
_co)  -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches TyCon
rep_tc ResidualCompleteMatches
rcm
        Maybe (TyCon, ThetaType, Coercion)
Nothing                    -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches ResidualCompleteMatches
rcm
      pure (rcm', vi{ vi_rcm = rcm' })

-- | Does a 'splitTyConApp_maybe' and then tries to look through a data family
-- application to find the representation TyCon, to which the data constructors
-- are attached. Returns the representation TyCon, the TyCon application args
-- and a representational coercion that will be Refl for non-data family apps.
splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, [Type], Coercion)
splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
splitReprTyConApp_maybe FamInstEnvs
env Type
ty =
  (TyCon -> ThetaType -> (TyCon, ThetaType, Coercion))
-> (TyCon, ThetaType) -> (TyCon, ThetaType, Coercion)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (FamInstEnvs -> TyCon -> ThetaType -> (TyCon, ThetaType, Coercion)
tcLookupDataFamInst FamInstEnvs
env) ((TyCon, ThetaType) -> (TyCon, ThetaType, Coercion))
-> Maybe (TyCon, ThetaType) -> Maybe (TyCon, ThetaType, Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
splitTyConApp_maybe Type
ty

-- | This is the |-Inst rule from the paper (section 4.5). Tries to
-- find an inhabitant in every complete set by instantiating with one their
-- constructors. If there is any complete set where we can't find an
-- inhabitant, the whole thing is uninhabited. It returns the updated 'VarInfo'
-- where all the attempted ConLike instantiations have been purged from the
-- 'ResidualCompleteMatches', which functions as a cache.
instCompleteSets :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
instCompleteSets :: Int
-> Nabla
-> VarInfo
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) VarInfo
instCompleteSets Int
fuel Nabla
nabla VarInfo
vi = {-# SCC "instCompleteSets" #-} do
  let x :: Id
x = VarInfo -> Id
vi_id VarInfo
vi
  (rcm, nabla) <- DsM (ResidualCompleteMatches, Nabla)
-> MaybeT
     (IOEnv (Env DsGblEnv DsLclEnv)) (ResidualCompleteMatches, Nabla)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
addNormalisedTypeMatches Nabla
nabla Id
x)
  nabla <- foldM (\Nabla
nabla DsCompleteMatch
cls -> Int
-> Nabla
-> Id
-> DsCompleteMatch
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCompleteSet Int
fuel Nabla
nabla Id
x DsCompleteMatch
cls) nabla (getRcm rcm)
  pure (lookupVarInfo (nabla_tm_st nabla) x)

anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution ConLike -> Bool
p = (PmAltConApp -> Bool) -> [PmAltConApp] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PmAltCon -> Bool
go (PmAltCon -> Bool)
-> (PmAltConApp -> PmAltCon) -> PmAltConApp -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmAltConApp -> PmAltCon
paca_con)
  where
    go :: PmAltCon -> Bool
go (PmAltConLike ConLike
cl) = ConLike -> Bool
p ConLike
cl
    go PmAltCon
_                 = Bool
False

-- | @instCompleteSet fuel nabla x cls@ iterates over @cls@ until it finds
-- the first inhabited ConLike (as per 'instCon'). Any failed instantiation
-- attempts of a ConLike are recorded as negative information in the returned
-- 'Nabla', so that later calls to this function can skip repeatedly fruitless
-- instantiation of that same constructor.
--
-- Note that the returned Nabla is just a different representation of the
-- original Nabla, not a proper refinement! No positive information will be
-- added, only negative information from failed instantiation attempts,
-- entirely as an optimisation.
instCompleteSet :: Int -> Nabla -> Id -> DsCompleteMatch -> MaybeT DsM Nabla
instCompleteSet :: Int
-> Nabla
-> Id
-> DsCompleteMatch
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCompleteSet Int
fuel Nabla
nabla Id
x DsCompleteMatch
cs
  | (ConLike -> Bool) -> [PmAltConApp] -> Bool
anyConLikeSolution (ConLike -> UniqDSet ConLike -> Bool
forall a. Uniquable a => a -> UniqDSet a -> Bool
`elementOfUniqDSet` (DsCompleteMatch -> UniqDSet ConLike
forall con. CompleteMatchX con -> UniqDSet con
cmConLikes DsCompleteMatch
cs)) (VarInfo -> [PmAltConApp]
vi_pos VarInfo
vi)
  -- No need to instantiate a constructor of this COMPLETE set if we already
  -- have a solution!
  = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
  | Bool -> Bool
not (Type -> DsCompleteMatch -> Bool
forall con. Type -> CompleteMatchX con -> Bool
completeMatchAppliesAtType (Id -> Type
varType Id
x) DsCompleteMatch
cs)
  = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
  | Bool
otherwise
  = {-# SCC "instCompleteSet" #-} Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
go Nabla
nabla (DsCompleteMatch -> [ConLike]
sorted_candidates DsCompleteMatch
cs)
  where
    vi :: VarInfo
vi = TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x

    sorted_candidates :: DsCompleteMatch -> [ConLike]
    sorted_candidates :: DsCompleteMatch -> [ConLike]
sorted_candidates DsCompleteMatch
cm
      -- If there aren't many candidates, we can try to sort them by number of
      -- strict fields, type constraints, etc., so that we are fast in the
      -- common case
      -- (either many simple constructors *or* few "complicated" ones).
      | UniqDSet ConLike -> Int
forall a. UniqDSet a -> Int
sizeUniqDSet UniqDSet ConLike
cs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
5 = (ConLike -> ConLike -> Ordering) -> [ConLike] -> [ConLike]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ConLike -> ConLike -> Ordering
compareConLikeTestability (UniqDSet ConLike -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList UniqDSet ConLike
cs)
      | Bool
otherwise            = UniqDSet ConLike -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList UniqDSet ConLike
cs
      where cs :: UniqDSet ConLike
cs = DsCompleteMatch -> UniqDSet ConLike
forall con. CompleteMatchX con -> UniqDSet con
cmConLikes DsCompleteMatch
cm

    go :: Nabla -> [ConLike] -> MaybeT DsM Nabla
    go :: Nabla -> [ConLike] -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
go Nabla
_     []         = MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    go Nabla
nabla (RealDataCon DataCon
dc:[ConLike]
_)
      -- See Note [DataCons that are definitely inhabitable]
      -- Recall that dc can't be in vi_neg, because then it would be
      -- deleted from the residual COMPLETE set.
      | DataCon -> Bool
isDataConTriviallyInhabited DataCon
dc
      = Nabla -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Nabla
nabla
    go Nabla
nabla (ConLike
con:[ConLike]
cons) = do
      let x :: Id
x = VarInfo -> Id
vi_id VarInfo
vi
      let recur_not_con :: MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
recur_not_con = do
            nabla' <- Nabla
-> Id -> PmAltCon -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
addNotConCt Nabla
nabla Id
x (ConLike -> PmAltCon
PmAltConLike ConLike
con)
            go nabla' cons
      (Nabla
nabla Nabla
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a b.
a
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) b
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Int
-> Nabla
-> Id
-> ConLike
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCon Int
fuel Nabla
nabla Id
x ConLike
con) -- return the original nabla, not the
                                          -- refined one!
            MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a.
MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
recur_not_con -- Assume that x can't be con. Encode that fact
                              -- with addNotConCt and recur.

-- | Is this 'DataCon' trivially inhabited, that is, without needing to perform
-- any inhabitation testing because of strict/unlifted fields or type
-- equalities? See Note [DataCons that are definitely inhabitable]
isDataConTriviallyInhabited :: DataCon -> Bool
isDataConTriviallyInhabited :: DataCon -> Bool
isDataConTriviallyInhabited DataCon
dc
  | TyCon -> Bool
isTyConTriviallyInhabited (DataCon -> TyCon
dataConTyCon DataCon
dc) = Bool
True
isDataConTriviallyInhabited DataCon
dc =
  ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> ThetaType
dataConTheta DataCon
dc) Bool -> Bool -> Bool
&&                -- (1)
  [HsImplBang] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [HsImplBang]
dataConImplBangs DataCon
dc) Bool -> Bool -> Bool
&&            -- (2)
  ThetaType -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> ThetaType
dataConMightBeUnliftedFieldTys DataCon
dc) -- (3)

dataConMightBeUnliftedFieldTys :: DataCon -> [Type]
dataConMightBeUnliftedFieldTys :: DataCon -> ThetaType
dataConMightBeUnliftedFieldTys =
  (Type -> Bool) -> ThetaType -> ThetaType
forall a. (a -> Bool) -> [a] -> [a]
filter Type -> Bool
mightBeUnliftedType (ThetaType -> ThetaType)
-> (DataCon -> ThetaType) -> DataCon -> ThetaType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Scaled Type -> Type) -> [Scaled Type] -> ThetaType
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing ([Scaled Type] -> ThetaType)
-> (DataCon -> [Scaled Type]) -> DataCon -> ThetaType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> [Scaled Type]
dataConOrigArgTys

isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited :: TyCon -> Bool
isTyConTriviallyInhabited TyCon
tc = Unique -> UniqueSet -> Bool
memberUniqueSet (TyCon -> Unique
forall a. Uniquable a => a -> Unique
getUnique TyCon
tc) UniqueSet
triviallyInhabitedTyConKeys

-- | All these types are trivially inhabited
triviallyInhabitedTyConKeys :: UniqueSet
triviallyInhabitedTyConKeys :: UniqueSet
triviallyInhabitedTyConKeys = [Unique] -> UniqueSet
fromListUniqueSet [
    Unique
charTyConKey, Unique
doubleTyConKey, Unique
floatTyConKey,
    Unique
intTyConKey, Unique
int8TyConKey, Unique
int16TyConKey, Unique
int32TyConKey, Unique
int64TyConKey,
    Unique
intPrimTyConKey, Unique
int8PrimTyConKey, Unique
int16PrimTyConKey, Unique
int32PrimTyConKey, Unique
int64PrimTyConKey,
    Unique
wordTyConKey, Unique
word8TyConKey, Unique
word16TyConKey, Unique
word32TyConKey, Unique
word64TyConKey,
    Unique
wordPrimTyConKey, Unique
word8PrimTyConKey, Unique
word16PrimTyConKey, Unique
word32PrimTyConKey, Unique
word64PrimTyConKey,
    Unique
trTyConTyConKey
  ]

compareConLikeTestability :: ConLike -> ConLike -> Ordering
-- We should instantiate DataCons first, because they are likely to occur in
-- multiple COMPLETE sets at once and we might find that multiple COMPLETE sets
-- are inhabited by instantiating only a single DataCon.
compareConLikeTestability :: ConLike -> ConLike -> Ordering
compareConLikeTestability PatSynCon{}     ConLike
_               = Ordering
GT
compareConLikeTestability ConLike
_               PatSynCon{}     = Ordering
GT
compareConLikeTestability (RealDataCon DataCon
a) (RealDataCon DataCon
b) = [DataCon -> DataCon -> Ordering] -> DataCon -> DataCon -> Ordering
forall a. Monoid a => [a] -> a
mconcat
  -- Thetas are most expensive to check, as they might incur a whole new round
  -- of inhabitation testing
  [ (DataCon -> Int) -> DataCon -> DataCon -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (ThetaType -> Int
forall a. [a] -> Int
fast_length (ThetaType -> Int) -> (DataCon -> ThetaType) -> DataCon -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ThetaType
dataConTheta)
  -- Unlifted or strict fields only incur an inhabitation test for that
  -- particular field. Still something to avoid.
  , (DataCon -> Int) -> DataCon -> DataCon -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing DataCon -> Int
unlifted_or_strict_fields
  ] DataCon
a DataCon
b
  where
    fast_length :: [a] -> Int
    fast_length :: forall a. [a] -> Int
fast_length [a]
xs = ([a] -> Int) -> Int -> [a] -> Int -> Int
forall a b. ([a] -> b) -> b -> [a] -> Int -> b
atLength [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Int
6 [a]
xs Int
5 -- @min 6 (length xs)@, but O(1)

    -- An upper bound on the number of strict or unlifted fields. Approximate in
    -- the unlikely bogus case of an unlifted field that has a bang.
    unlifted_or_strict_fields :: DataCon -> Int
    unlifted_or_strict_fields :: DataCon -> Int
unlifted_or_strict_fields DataCon
dc = [HsImplBang] -> Int
forall a. [a] -> Int
fast_length (DataCon -> [HsImplBang]
dataConImplBangs DataCon
dc)
                                 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ThetaType -> Int
forall a. [a] -> Int
fast_length (DataCon -> ThetaType
dataConMightBeUnliftedFieldTys DataCon
dc)

-- | @instCon fuel nabla (x::match_ty) K@ tries to instantiate @x@ to @K@ by
-- adding the proper constructor constraint.
--
-- See Note [Instantiating a ConLike].
instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla
instCon :: Int
-> Nabla
-> Id
-> ConLike
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCon Int
fuel nabla :: Nabla
nabla@MkNabla{nabla_ty_st :: Nabla -> TyState
nabla_ty_st = TyState
ty_st} Id
x ConLike
con = {-# SCC "instCon" #-} IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla)
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
forall a b. (a -> b) -> a -> b
$ do
  let hdr :: String -> String
hdr String
what = String
"instCon " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
fuel String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
what
  env <- DsM FamInstEnvs
dsGetFamInstEnvs
  let match_ty = Id -> Type
idType Id
x
  tracePm (hdr "{") $
    ppr con <+> text "... <-" <+> ppr x <+> dcolon <+> ppr match_ty
  norm_match_ty <- normaliseSourceTypeWHNF ty_st match_ty
  mb_sigma_univ <- matchConLikeResTy env ty_st norm_match_ty con
  case mb_sigma_univ of
    Just Subst
sigma_univ -> do
      let ([Id]
_univ_tvs, [Id]
ex_tvs, [EqSpec]
eq_spec, ThetaType
thetas, ThetaType
_req_theta, [Scaled Type]
field_tys, Type
_con_res_ty)
            = ConLike
-> ([Id], [Id], [EqSpec], ThetaType, ThetaType, [Scaled Type],
    Type)
conLikeFullSig ConLike
con
      -- Following Note [Instantiating a ConLike]:
      -- (1) _req_theta has been tested in 'matchConLikeResTy'
      -- (2) Instantiate fresh existentials
      (sigma_ex, _) <- Subst -> [Id] -> UniqSupply -> (Subst, [Id])
cloneTyVarBndrs Subst
sigma_univ [Id]
ex_tvs (UniqSupply -> (Subst, [Id]))
-> DsM UniqSupply -> IOEnv (Env DsGblEnv DsLclEnv) (Subst, [Id])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DsM UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM
      -- (3) Substitute provided constraints bound by the constructor.
      --     These are added to the type oracle as new facts (in a moment)
      let gammas = HasDebugCallStack => Subst -> ThetaType -> ThetaType
Subst -> ThetaType -> ThetaType
substTheta Subst
sigma_ex ([EqSpec] -> ThetaType
eqSpecPreds [EqSpec]
eq_spec ThetaType -> ThetaType -> ThetaType
forall a. [a] -> [a] -> [a]
++ ThetaType
thetas)
      -- (4) Instantiate fresh term variables as arguments to the constructor
      let field_tys' = HasDebugCallStack => Subst -> ThetaType -> ThetaType
Subst -> ThetaType -> ThetaType
substTys Subst
sigma_ex (ThetaType -> ThetaType) -> ThetaType -> ThetaType
forall a b. (a -> b) -> a -> b
$ (Scaled Type -> Type) -> [Scaled Type] -> ThetaType
forall a b. (a -> b) -> [a] -> [b]
map Scaled Type -> Type
forall a. Scaled a -> a
scaledThing [Scaled Type]
field_tys
      arg_ids <- mapM mkPmId field_tys'
      tracePm (hdr "(cts)") $ vcat
        [ ppr x <+> dcolon <+> ppr match_ty
        , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
        , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
        , ppr (map (\Id
tv -> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'↦' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Subst -> Id -> Type
substTyVar Subst
sigma_univ Id
tv)) _univ_tvs)
        , ppr gammas
        , ppr (map (\Id
x -> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Type
idType Id
x)) arg_ids)
        ]
      -- (5) Finally add the new constructor constraint
      runMaybeT $ do
        -- Case (2) of Note [Strict fields and variables of unlifted type]
        let alt = ConLike -> PmAltCon
PmAltConLike ConLike
con
        let branching_factor = [Id] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Id] -> Int) -> [Id] -> Int
forall a b. (a -> b) -> a -> b
$ PmAltCon -> [Id] -> [Id]
filterUnliftedFields PmAltCon
alt [Id]
arg_ids
        let ct = Id -> PmAltCon -> [Id] -> ThetaType -> [Id] -> PhiCt
PhiConCt Id
x PmAltCon
alt [Id]
ex_tvs ThetaType
gammas [Id]
arg_ids
        nabla1 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $
                  addPhiTmCt nabla ct
        -- See Note [Fuel for the inhabitation test]
        let new_fuel
              | Int
branching_factor Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 = Int
fuel
              | Bool
otherwise             = Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
fuel Int
2
        lift $ tracePm (hdr "(ct satisfiable)") $ vcat
          [ ppr ct
          , ppr x <+> dcolon <+> ppr match_ty
          , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
          , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
          , ppr (map (\Id
tv -> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
tv SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Char -> SDoc
forall doc. IsLine doc => Char -> doc
char Char
'↦' SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Subst -> Id -> Type
substTyVar Subst
sigma_univ Id
tv)) _univ_tvs)
          , ppr gammas
          , ppr (map (\Id
x -> Id -> SDoc
forall a. Outputable a => a -> SDoc
ppr Id
x SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id -> Type
idType Id
x)) arg_ids)
          , ppr branching_factor
          , ppr new_fuel
          ]
        nabla2 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla1) $
                  inhabitationTest new_fuel (nabla_ty_st nabla) nabla1
        lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla2)
        pure nabla2
    Maybe Subst
Nothing -> do
      String -> SDoc -> DsM ()
tracePm (String -> String
hdr String
"(match_ty not instance of res_ty) }") SDoc
forall doc. IsOutput doc => doc
empty
      Maybe Nabla -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Nabla -> Maybe Nabla
forall a. a -> Maybe a
Just Nabla
nabla) -- Matching against match_ty failed. Inhabited!
                        -- See Note [Instantiating a ConLike].

-- | @matchConLikeResTy _ _ ty K@ tries to match @ty@ against the result
-- type of @K@, @res_ty@. It returns a substitution @s@ for @K@'s universal
-- tyvars such that @s(res_ty)@ equals @ty@ if successful.
--
-- Make sure that @ty@ is normalised before.
--
-- See Note [Matching against a ConLike result type].
matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe Subst)
matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe Subst)
matchConLikeResTy FamInstEnvs
env TyState
_              Type
ty (RealDataCon DataCon
dc) = Maybe Subst -> DsM (Maybe Subst)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Subst -> DsM (Maybe Subst))
-> Maybe Subst -> DsM (Maybe Subst)
forall a b. (a -> b) -> a -> b
$ do
  (rep_tc, tc_args, _co) <- FamInstEnvs -> Type -> Maybe (TyCon, ThetaType, Coercion)
splitReprTyConApp_maybe FamInstEnvs
env Type
ty
  if rep_tc == dataConTyCon dc
    then Just (zipTCvSubst (dataConUnivTyVars dc) tc_args)
    else Nothing
matchConLikeResTy FamInstEnvs
_   (TySt Int
_ InertSet
inert) Type
ty (PatSynCon PatSyn
ps) = {-# SCC "matchConLikeResTy" #-} MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst -> DsM (Maybe Subst)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst -> DsM (Maybe Subst))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst
-> DsM (Maybe Subst)
forall a b. (a -> b) -> a -> b
$ do
  let ([Id]
univ_tvs,ThetaType
req_theta,[Id]
_,ThetaType
_,[Scaled Type]
_,Type
con_res_ty) = PatSyn -> ([Id], ThetaType, [Id], ThetaType, [Scaled Type], Type)
patSynSig PatSyn
ps
  subst <- DsM (Maybe Subst) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (DsM (Maybe Subst) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst)
-> DsM (Maybe Subst)
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Subst
forall a b. (a -> b) -> a -> b
$ Maybe Subst -> DsM (Maybe Subst)
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Subst -> DsM (Maybe Subst))
-> Maybe Subst -> DsM (Maybe Subst)
forall a b. (a -> b) -> a -> b
$ Type -> Type -> Maybe Subst
tcMatchTy Type
con_res_ty Type
ty
  guard $ all (`elemSubst` subst) univ_tvs -- See the Note about T11336b
  if null req_theta
    then pure subst
    else do
      let req_theta' = HasDebugCallStack => Subst -> ThetaType -> ThetaType
Subst -> ThetaType -> ThetaType
substTys Subst
subst ThetaType
req_theta
      satisfiable <- lift $ initTcDsForSolver $ tcCheckWanteds inert req_theta'
      if satisfiable
        then pure subst
        else mzero

{- Note [Soundness and Completeness]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Soundness and completeness of the pattern-match checker depend entirely on the
soundness and completeness of the inhabitation test.

Achieving both soundness and completeness at the same time is undecidable.
See also T17977 and Note [Fuel for the inhabitation test].
Losing soundness would make the algorithm pointless; hence we give up on
completeness, but try to get as close as possible (how close is called
the 'precision' of the algorithm).

Soundness means that you
  1. Can remove clauses flagged as redundant without changing program semantics
     (no false positives).
  2. Can be sure that your program is free of incomplete pattern matches
     when the checker doesn't flag any inexhaustive definitions
     (no false negatives).

A complete algorithm would mean that
  1. When a clause can be deleted without changing program semantics, it will
     be flagged as redundant (no false negatives).
  2. A program that is free of incomplete pattern matches will never have a
     definition be flagged as inexhaustive (no false positives).

Via the LYG algorithm, we reduce both these properties to a property on
the inhabitation test of refinement types:
  *Soundness*:    If the inhabitation test says "no" for a given refinement type
                  Nabla, then it provably has no inhabitant.
  *Completeness*: If the inhabitation test says "yes" for a given refinement type
                  Nabla, then it provably has an inhabitant.
Our test is sound, but incomplete, so there are instances where we say
"yes" but in fact the Nabla is empty. Which entails false positive exhaustivity
and false negative redundancy warnings, as above.

In summary, we have the following correspondence:

Property     | Exhaustiveness warnings | Redundancy warnings | Inhabitation test |
-------------|-------------------------|---------------------|-------------------|
Soundness    | No false negatives      | No false positives  | Only says "no"    |
             |                         |                     | if there is no    |
             |                         |                     | inhabitant        |
Completeness | No false positives      | No false negatives  | Only says "yes"   |
             |                         |                     | if there is an    |
             |                         |                     | inhabitant        |

Note [Shortcutting the inhabitation test]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Generally, we have to re-test a refinement type for inhabitants whenever we
add a new constraint. Often, we can say "no" early, upon trying to add a
contradicting constraint, see Note [The Pos/Neg invariant]. Still, COMPLETE
sets and type evidence are best handled in a delayed fashion, because of
the recursive nature of the test and our fuel-based approach.
But even then there are some cases in which we can skip the full test,
because we are sure that the refinement type is still inhabited. These
conditions are monitored by 'varNeedsTesting'. It returns

- `True` whenever a full inhabitation test is needed
- `False` whenever the test can be skipped, amounting to an inhabitation test
  that says "yes".

According to Note [Soundness and Completeness], this test will never compromise
soundness: The `True` case just forwards to the actual inhabitation test and the
`False` case amounts to an inhabitation test that is trivially sound, because it
never says "no".

Of course, if the returns says `False`, Completeness (and thus Precision) of the
algorithm is affected, but we get to skip costly inhabitation tests. We try to
trade as little Precision as possible against as much Performance as possible.
Here are the tests, in order:

  1. If a variable is dirty (because of a newly added negative term constraint),
     we have to test.
  2. If a variable has positive information, we don't have to test: The
     positive information acts as constructive proof for inhabitation.
  3. If the type state didn't change, there is no need to test.
  4. If the variable's normalised type didn't change, there is no need to test.
  5. Otherwise, we have to test.

Why (1) before (2)?
-------------------
Consider the reverse for (T18960):
  pattern P x = x
  {-# COMPLETE P :: () #-}
  foo = case () of x@(P _) -> ()
This should be exhaustive. But if we say "We know `x` has solution `()`, so it's
inhabited", then we'll get a warning saying that `()` wasn't matched.
But the match on `P` added the new negative information to the uncovered set,
in the process of which we marked `x` as dirty. By giving the dirty flag a
higher priority than positive info, we get to test again and see that `x` is
uninhabited and the match is exhaustive.

But suppose that `P` wasn't mentioned in any COMPLETE set. Then we simply
don't mark `x` as dirty and will emit a warning again (which we would anyway),
without running a superfluous inhabitation test. That speeds up T17836
considerably.

Why (2) before (3) and (4)?
---------------------------
Simply because (2) is more efficient to test than (3) (not by a lot), which
is more efficient to test than (4), which is still more efficient than running
the full inhabitation test (5).

Note [Fuel for the inhabitation test]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Whether or not a type is inhabited is undecidable in general, see also
Note [Soundness and Completeness]. As a result, we can run into infinite
loops in `inhabitationTest`. 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. But this can't be proven by mere
instantiation and requires an inductive argument, which `inhabitationTest`
currently isn't equipped to do.

In order to prevent endless instantiation attempts in @inhabitationTest@, we
use the fuel as an upper bound on such attempts.

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
`inhabitationTest` can run in exponential time in the amount of fuel. Consider
the following data type:

  data T = MkT !T !T !T

If we try to instantiate 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 initial fuel is, say,
100, then the inhabitation test will effectively take forever.

To mitigate this, we check the branching factor every time we are about to do
inhabitation testing in 'instCon'. 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 fuel to 4, 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 [DataCons 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
'instCon' on it, since it's "obvious" that it is inhabitable. To make this
intuition formal, we say that a DataCon C is definitely inhabitable (DI) if:

  1. C has no equality constraints (since they might be unsatisfiable)
  2. C has no strict arguments (since they might be uninhabitable)
  3. C has no unlifted argument types (since they might be uninhabitable)

It's relatively cheap to check if a DataCon is DI, so before we call 'instCon'
on a constructor of a COMPLETE set, we filter out all of the DI ones.

This fast path shaves down -7% allocations for PmSeriesG, for example.

Note [Matching against a ConLike result type]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given a ConLike

> C :: forall us. R => ... -> res_ty

is a pattern `C ...` compatible with the type `ty`? Clearly that is the case if
`res_ty` /subsumes/ `ty` and the required constraints `R` (strictly a feature of
pattern synonyms) are satisfiable. In that case, 'matchConLikeResTy' returns a
substitution σ over `us` such that `σ(res_ty) == ty`.

It's surprisingly tricky to implement correctly, and works quite different for
DataCons and PatSynCons:

  * For data cons, we look at `ty` and see if it's a TyCon app `T t1 ... tn`.
    If that is the case, we make sure that `C` is a DataCon of `T` and return
    a substitution mapping `C`'s universal tyvars `us` to `t1`...`tn`.

    Wrinkle: Since `T` might be a data family TyCon, we have to look up its
    representation TyCon before we compare to `C`'s TyCon.
    So we use 'splitReprTyConApp_maybe' instead of 'splitTyConApp_maybe'.

  * For pattern synonyms, we directly match `ty` against `res_ty` to get the
    substitution σ. See Note [Pattern synonym result type] in "GHC.Core.PatSyn".

    Fortunately, we don't have to treat data family TyCons specially:
    Pattern synonyms /never/ apply to a data family representation TyCon.
    We do have to consider the required constraints `σ(R)`, though, as we have
    seen in #19475. That is done by solving them as Wanted constraints given the
    inert set of the current type state (which is part of a Nabla's TySt). Since
    spinning up a constraint solver session is costly, we only do so in the rare
    cases that a pattern synonym actually carries any required constraints.

    We can get into the strange situation that not all universal type variables
    `us` occur in `res_ty`. Example from T11336b:

      instance C Proxy where ...                      -- impl uninteresting
      pattern P :: forall f a. C f => f a -> Proxy a  -- impl uninteresting

      fun :: Proxy a -> ()
      fun (P Proxy) = ()
      fun (P Proxy) = () -- ideally detected as redundant

    `f` is a universal type variable and `C f` the required constraint of
    pattern synonym `P`. But `f` doesn't occur in the result type `Proxy a` of
    `P`, so σ will not even have `f` in its in-scope set. It's a bit unclear
    what to do here; we might want to freshen `f` to `f'` and see if we can
    solve `C f'` as a Wanted constraint, which we most likely can't.
    Hence, we simply skip the freshening and declare the match as failed when
    there is a variable like `f`. For the definition of `fun`, that
    means we will not remember that we matched on `P` and thus will
    not detect its second clause as redundant.

    See Note [Pattern synonym result type] in "GHC.Core.PatSyn" for similar
    oddities.

Note [Instantiating a ConLike]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
`instCon` implements the \(Inst\) function from Figure 8 of the LYG paper.

Given the following type of ConLike `K`

> K :: forall us. R => forall es. P => t1 -> ... -> tn -> res_ty

and a variable `x::match_ty`, it tries to find an instantiation
`K ex_tvs gammas arg_ids :: match_ty` (for fresh `arg_ids`) and ultimately adds
a constructor constraint `K ex_tvs gammas arg_ids <- x` to the given Nabla.

As a first step, it tries (via 'matchConLikeResTy') to match `match_ty` against
`res_ty` and checks that that the required constraints @R@ are satisfiable.
See Note [Matching against a ConLike result type].

If matching /fails/, it trivially (and conservatively) reports "inhabited" by
returning the unrefined input Nabla. After all, the match might have failed due
to incomplete type information in Nabla.
(Later type refinement from unpacking GADT constructors might monomorphise
`match_ty` so much that `res_ty` ultimately subsumes it.)

If matching /succeeds/, we get a substitution σ for the (universal)
tyvars `us`. After applying σ, we get

> K @σ(us) :: σ(R) => forall σ(es). σ(P) => σ(t1) -> ... -> σ(tn) -> match_ty

The existentials `es` might still occur in argument types `σ(tn)`, though.
Now 'instCon' performs the following steps:

 1. It drops the required constraints `σ(R)`, as they have already been
    discharged by 'matchConLikeResTy'.
 2. It instantiates fresh binders `es'` for the other type variables `es`
    bound by `K` and adds the mapping to σ to get σ', so that we have

    > K @σ(us) @es' :: σ'(P) => σ'(t1) -> ... -> σ'(tn) -> match_ty

 3. It adds new type constraints from the substituted
    provided constraints @σ'(P)@.
 4. It substitutes and conjures new binders @arg_ids@ for the argument types
    @σ'(t1) ... σ'(tn)@.
 5. It adds a term constraint @K es' σ'(P) arg_ids <- x@, which handles
    the details regarding type constraints and unlifted fields.

And finally the extended 'Nabla' is returned if all the constraints were
compatible.
-}

--------------------------------------
-- * Generating inhabitants of a Nabla
--
-- This is important for warnings. Roughly corresponds to G in Figure 6 of the
-- LYG paper, with a few tweaks for better warning messages.

-- | See Note [Case split inhabiting patterns]
data GenerateInhabitingPatternsMode
  = CaseSplitTopLevel
  | MinimalCover
  deriving (GenerateInhabitingPatternsMode
-> GenerateInhabitingPatternsMode -> Bool
(GenerateInhabitingPatternsMode
 -> GenerateInhabitingPatternsMode -> Bool)
-> (GenerateInhabitingPatternsMode
    -> GenerateInhabitingPatternsMode -> Bool)
-> Eq GenerateInhabitingPatternsMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GenerateInhabitingPatternsMode
-> GenerateInhabitingPatternsMode -> Bool
== :: GenerateInhabitingPatternsMode
-> GenerateInhabitingPatternsMode -> Bool
$c/= :: GenerateInhabitingPatternsMode
-> GenerateInhabitingPatternsMode -> Bool
/= :: GenerateInhabitingPatternsMode
-> GenerateInhabitingPatternsMode -> Bool
Eq, Int -> GenerateInhabitingPatternsMode -> String -> String
[GenerateInhabitingPatternsMode] -> String -> String
GenerateInhabitingPatternsMode -> String
(Int -> GenerateInhabitingPatternsMode -> String -> String)
-> (GenerateInhabitingPatternsMode -> String)
-> ([GenerateInhabitingPatternsMode] -> String -> String)
-> Show GenerateInhabitingPatternsMode
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> GenerateInhabitingPatternsMode -> String -> String
showsPrec :: Int -> GenerateInhabitingPatternsMode -> String -> String
$cshow :: GenerateInhabitingPatternsMode -> String
show :: GenerateInhabitingPatternsMode -> String
$cshowList :: [GenerateInhabitingPatternsMode] -> String -> String
showList :: [GenerateInhabitingPatternsMode] -> String -> String
Show)

instance Outputable GenerateInhabitingPatternsMode where
  ppr :: GenerateInhabitingPatternsMode -> SDoc
ppr = String -> SDoc
forall doc. IsLine doc => String -> doc
text (String -> SDoc)
-> (GenerateInhabitingPatternsMode -> String)
-> GenerateInhabitingPatternsMode
-> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenerateInhabitingPatternsMode -> String
forall a. Show a => a -> String
show

-- | @generateInhabitingPatterns vs n nabla@ returns a list of at most @n@ (but
-- perhaps empty) refinements of @nabla@ that represent inhabited patterns.
-- Negative information is only retained if literals are involved or for
-- recursive GADTs.
generateInhabitingPatterns :: GenerateInhabitingPatternsMode -> [Id] -> Int -> Nabla -> DsM [Nabla]
-- See Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
generateInhabitingPatterns :: GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
_    [Id]
_      Int
0 Nabla
_     = [Nabla] -> DsM [Nabla]
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
generateInhabitingPatterns GenerateInhabitingPatternsMode
_    []     Int
_ Nabla
nabla = [Nabla] -> DsM [Nabla]
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Nabla
nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode (Id
x:[Id]
xs) Int
n Nabla
nabla = do
  String -> SDoc -> DsM ()
tracePm String
"generateInhabitingPatterns" (GenerateInhabitingPatternsMode -> SDoc
forall a. Outputable a => a -> SDoc
ppr GenerateInhabitingPatternsMode
mode SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [Id] -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Id
xId -> [Id] -> [Id]
forall a. a -> [a] -> [a]
:[Id]
xs) SDoc -> SDoc -> SDoc
forall doc. IsDoc doc => doc -> doc -> doc
$$ Nabla -> SDoc
forall a. Outputable a => a -> SDoc
ppr Nabla
nabla)
  let VI Id
_ [PmAltConApp]
pos PmAltConSet
neg BotInfo
_ ResidualCompleteMatches
_ = TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
nabla) Id
x
  case [PmAltConApp]
pos of
    PmAltConApp
_:[PmAltConApp]
_ -> do
      -- Example for multiple solutions (must involve a PatSyn):
      --   f x@(Just _) True | SomePatSyn _ <- x = ...
      -- within the RHS, we know that
      --   * @x ~ Just y@ for some @y@
      --   * @x ~ SomePatSyn z@ for some @z@
      -- and both conditions have to hold /at the same time/. Hence 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 = (PmAltConApp -> [Id]) -> [PmAltConApp] -> [Id]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PmAltConApp -> [Id]
paca_ids [PmAltConApp]
pos
      GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode ([Id]
arg_vas [Id] -> [Id] -> [Id]
forall a. [a] -> [a] -> [a]
++ [Id]
xs) Int
n Nabla
nabla
    []
      -- When there are literals involved, just print negative info
      -- instead of listing missed constructors
      | [PmLit] -> Bool
forall (f :: * -> *) a. Foldable f => f a -> Bool
notNull [ PmLit
l | PmAltLit PmLit
l <- PmAltConSet -> [PmAltCon]
pmAltConSetElems PmAltConSet
neg ]
      -> GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode [Id]
xs Int
n Nabla
nabla
      -- When some constructors are impossible or when we don't care for a
      -- minimal cover (Note [Case split inhabiting patterns]), do a case split.
      | Bool -> Bool
not (PmAltConSet -> Bool
isEmptyPmAltConSet PmAltConSet
neg) Bool -> Bool -> Bool
|| GenerateInhabitingPatternsMode
mode GenerateInhabitingPatternsMode
-> GenerateInhabitingPatternsMode -> Bool
forall a. Eq a => a -> a -> Bool
== GenerateInhabitingPatternsMode
CaseSplitTopLevel
      -> Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
try_instantiate Id
x [Id]
xs Int
n Nabla
nabla
      -- Else don't do a case split on this var, just print a wildcard.
      -- But try splitting for the remaining vars, of course
      | Bool
otherwise
      -> GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode [Id]
xs Int
n Nabla
nabla
  where
    -- 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 -> Nabla -> DsM [Nabla]
    -- Convention: x binds the outer constructor in the chain, y the inner one.
    try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
try_instantiate Id
x [Id]
xs Int
n Nabla
nabla = do
      (_src_ty, dcs, rep_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 (Nabla -> TyState
nabla_ty_st Nabla
nabla) (Id -> Type
idType Id
x)
      mb_stuff <- runMaybeT $ instantiate_newtype_chain x nabla dcs
      case mb_stuff of
        Maybe (Id, Nabla)
Nothing -> [Nabla] -> DsM [Nabla]
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
        Just (Id
y, Nabla
newty_nabla) -> do
          let vi :: VarInfo
vi = TmState -> Id -> VarInfo
lookupVarInfo (Nabla -> TmState
nabla_tm_st Nabla
newty_nabla) Id
y
          env <- DsM FamInstEnvs
dsGetFamInstEnvs
          rcm <- case splitReprTyConApp_maybe env rep_ty of
            Just (TyCon
tc, ThetaType
_, Coercion
_) -> TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addTyConMatches TyCon
tc (VarInfo -> ResidualCompleteMatches
vi_rcm VarInfo
vi)
            Maybe (TyCon, ThetaType, Coercion)
Nothing         -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
addCompleteMatches (VarInfo -> ResidualCompleteMatches
vi_rcm VarInfo
vi)

          -- Test all COMPLETE sets for inhabitants (n inhs at max). Take care of ⊥.
          clss <- pickApplicableCompleteSets (nabla_ty_st nabla) rep_ty rcm
          case NE.nonEmpty (uniqDSetToList . cmConLikes <$> clss) of
            Maybe (NonEmpty [ConLike])
Nothing ->
              -- No COMPLETE sets ==> inhabited
              GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode [Id]
xs Int
n Nabla
newty_nabla
            Just NonEmpty [ConLike]
clss -> do
              -- Try each COMPLETE set.
              nablass' <- NonEmpty [ConLike]
-> ([ConLike]
    -> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)])
-> IOEnv
     (Env DsGblEnv DsLclEnv) (NonEmpty [(Maybe ConLike, Nabla)])
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM NonEmpty [ConLike]
clss (Id
-> Type
-> [Id]
-> Int
-> Nabla
-> [ConLike]
-> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)]
instantiate_cons Id
y Type
rep_ty [Id]
xs Int
n Nabla
newty_nabla)
              if any null nablass' && vi_bot vi /= IsNotBot
              then generateInhabitingPatterns mode xs n newty_nabla -- bot is still possible. Display a wildcard!
              else do
                -- Pick the residual COMPLETE set with the smallest cost (see 'completeSetCost').
                -- See Note [Prefer in-scope COMPLETE matches].
                DsGblEnv { ds_gbl_rdr_env = rdr_env } <- getGblEnv
                let bestSet = ((Maybe ConLike, Nabla) -> Nabla)
-> [(Maybe ConLike, Nabla)] -> [Nabla]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe ConLike, Nabla) -> Nabla
forall a b. (a, b) -> b
snd ([(Maybe ConLike, Nabla)] -> [Nabla])
-> [(Maybe ConLike, Nabla)] -> [Nabla]
forall a b. (a -> b) -> a -> b
$ ([(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)] -> Ordering)
-> NonEmpty [(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)]
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy (([(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int))
-> [(Maybe ConLike, Nabla)] -> [(Maybe ConLike, Nabla)] -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (([(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int))
 -> [(Maybe ConLike, Nabla)]
 -> [(Maybe ConLike, Nabla)]
 -> Ordering)
-> ([(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int))
-> [(Maybe ConLike, Nabla)]
-> [(Maybe ConLike, Nabla)]
-> Ordering
forall a b. (a -> b) -> a -> b
$ GlobalRdrEnv -> [(Maybe ConLike, Nabla)] -> (Bool, Int, Int, Int)
forall a.
GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int)
completeSetCost GlobalRdrEnv
rdr_env) NonEmpty [(Maybe ConLike, Nabla)]
nablass'
                pure bestSet

    -- Instantiates a chain of newtypes, beginning at @x@.
    -- Turns @x nabla [T,U,V]@ to @(y, nabla')@, where @nabla'@ we has the fact
    -- @x ~ T (U (V y))@.
    instantiate_newtype_chain :: Id -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (Id, Nabla)
    instantiate_newtype_chain :: Id
-> Nabla
-> [(Type, DataCon, Type)]
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
instantiate_newtype_chain Id
x Nabla
nabla []                      = (Id, Nabla) -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) (Id, Nabla)
forall a. a -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id
x, Nabla
nabla)
    instantiate_newtype_chain Id
x Nabla
nabla ((Type
_ty, DataCon
dc, Type
arg_ty):[(Type, DataCon, Type)]
dcs) = do
      y <- IOEnv (Env DsGblEnv DsLclEnv) Id
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IOEnv (Env DsGblEnv DsLclEnv) Id
 -> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id)
-> IOEnv (Env DsGblEnv DsLclEnv) Id
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Id
forall a b. (a -> b) -> a -> b
$ Type -> IOEnv (Env DsGblEnv DsLclEnv) Id
mkPmId Type
arg_ty
      -- Newtypes don't have existentials (yet?!), so passing an empty
      -- list as ex_tvs.
      nabla' <- addConCt nabla x (PmAltConLike (RealDataCon dc)) [] [y]
      instantiate_newtype_chain y nabla' dcs

    instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [(Maybe ConLike, Nabla)]
    instantiate_cons :: Id
-> Type
-> [Id]
-> Int
-> Nabla
-> [ConLike]
-> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)]
instantiate_cons Id
_ Type
_  [Id]
_  Int
_ Nabla
_     []       = [(Maybe ConLike, Nabla)]
-> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)]
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    instantiate_cons Id
_ Type
_  [Id]
_  Int
0 Nabla
_     [ConLike]
_        = [(Maybe ConLike, Nabla)]
-> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)]
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
    instantiate_cons Id
_ Type
ty [Id]
xs Int
n Nabla
nabla [ConLike]
_
      -- We don't want to expose users to GHC-specific constructors for Int etc.
      | ((TyCon, ThetaType) -> Bool)
-> Maybe (TyCon, ThetaType) -> Maybe Bool
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TyCon -> Bool
isTyConTriviallyInhabited (TyCon -> Bool)
-> ((TyCon, ThetaType) -> TyCon) -> (TyCon, ThetaType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TyCon, ThetaType) -> TyCon
forall a b. (a, b) -> a
fst) (HasDebugCallStack => Type -> Maybe (TyCon, ThetaType)
Type -> Maybe (TyCon, ThetaType)
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
      = (Nabla -> (Maybe ConLike, Nabla))
-> [Nabla] -> [(Maybe ConLike, Nabla)]
forall a b. (a -> b) -> [a] -> [b]
map (Maybe ConLike
forall a. Maybe a
Nothing,) ([Nabla] -> [(Maybe ConLike, Nabla)])
-> DsM [Nabla]
-> IOEnv (Env DsGblEnv DsLclEnv) [(Maybe ConLike, Nabla)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode [Id]
xs Int
n Nabla
nabla
    instantiate_cons Id
x Type
ty [Id]
xs Int
n Nabla
nabla (ConLike
cl:[ConLike]
cls) = do
      -- The following line is where we call out to the inhabitationTest!
      mb_nabla <- MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
 -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla))
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
-> IOEnv (Env DsGblEnv DsLclEnv) (Maybe Nabla)
forall a b. (a -> b) -> a -> b
$ Int
-> Nabla
-> Id
-> ConLike
-> MaybeT (IOEnv (Env DsGblEnv DsLclEnv)) Nabla
instCon Int
4 Nabla
nabla Id
x ConLike
cl
      tracePm "instantiate_cons" (vcat [ ppr x <+> dcolon <+> ppr (idType x)
                                       , ppr ty
                                       , ppr cl
                                       , ppr nabla
                                       , ppr mb_nabla
                                       , ppr n ])
      con_nablas <- case mb_nabla of
        Maybe Nabla
Nothing     -> [Nabla] -> DsM [Nabla]
forall a. a -> IOEnv (Env DsGblEnv DsLclEnv) a
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 the inhabitation test would have refuted.
        Just Nabla
nabla' -> GenerateInhabitingPatternsMode
-> [Id] -> Int -> Nabla -> DsM [Nabla]
generateInhabitingPatterns GenerateInhabitingPatternsMode
mode [Id]
xs Int
n Nabla
nabla'
      other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls
      pure (map (Just cl,) con_nablas ++ other_cons_nablas)

-- | If multiple residual COMPLETE sets apply, pick one as follows:
--
--  - prefer COMPLETE sets in which all constructors are in scope,
--    as per Note [Prefer in-scope COMPLETE matches],
--  - if there are ties, pick the one with the fewest (residual) ConLikes,
--  - if there are ties, pick the one with the fewest "trivially inhabited" types,
--  - if there are ties, pick the one with the fewest PatSyns,
--  - if there are still ties, pick the one that comes first in the list of
--    COMPLETE pragmas, which means the one that was brought into scope first.
completeSetCost :: GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int)
completeSetCost :: forall a.
GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int)
completeSetCost GlobalRdrEnv
_ [] = (Bool
False, Int
0, Int
0, Int
0)
completeSetCost GlobalRdrEnv
rdr_env ((Maybe ConLike
mb_con, a
_) : [(Maybe ConLike, a)]
cons) =
  let con_out_of_scope :: Bool
con_out_of_scope
        | Just ConLike
con <- Maybe ConLike
mb_con
        = Maybe (GlobalRdrEltX GREInfo) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (GlobalRdrEltX GREInfo) -> Bool)
-> Maybe (GlobalRdrEltX GREInfo) -> Bool
forall a b. (a -> b) -> a -> b
$ GlobalRdrEnv -> Name -> Maybe (GlobalRdrEltX GREInfo)
forall info.
Outputable info =>
GlobalRdrEnvX info -> Name -> Maybe (GlobalRdrEltX info)
lookupGRE_Name GlobalRdrEnv
rdr_env (ConLike -> Name
conLikeName ConLike
con)
        | Bool
otherwise
        = Bool
False
      (Bool
any_out_of_scope, Int
nb_cons, Int
nb_triv, Int
nb_ps) = GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int)
forall a.
GlobalRdrEnv -> [(Maybe ConLike, a)] -> (Bool, Int, Int, Int)
completeSetCost GlobalRdrEnv
rdr_env [(Maybe ConLike, a)]
cons
  in ( Bool
any_out_of_scope Bool -> Bool -> Bool
|| Bool
con_out_of_scope
     , Int
nb_cons Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
     , Int
nb_triv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ case Maybe ConLike
mb_con of { Maybe ConLike
Nothing -> Int
1; Maybe ConLike
_ -> Int
0 }
     , Int
nb_ps   Int -> Int -> Int
forall a. Num a => a -> a -> a
+ case Maybe ConLike
mb_con of { Just (PatSynCon {}) -> Int
1; Maybe ConLike
_ -> Int
0 }
     )

{- Note [Prefer in-scope COMPLETE matches]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We prefer using COMPLETE pragmas in which all ConLikes are in scope, as this
improves error messages. See for example T25115:

  - T25115a defines pattern Foo :: a with {-# COMPLETE Foo #-}
  - T25115 imports T25115a, but not Foo.
    (This means it imports the COMPLETE pragma, which behaves like an instance.)

    Then, for the following incomplete pattern match in T25115:

      baz :: Ordering -> Int
      baz = \case
        EQ -> 5

    we would prefer reporting that 'LT' and 'GT' are not matched, rather than
    saying that 'T25115a.Foo' is not matched.

    However, if ALL ConLikes are out of scope, then we should still report
    something, so we don't want to outright filter out all COMPLETE sets
    with an out-of-scope ConLike.
-}

pickApplicableCompleteSets :: TyState -> Type -> ResidualCompleteMatches -> DsM DsCompleteMatches
-- See Note [Implementation of COMPLETE pragmas] on what "applicable" means
pickApplicableCompleteSets :: TyState
-> Type
-> ResidualCompleteMatches
-> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch]
pickApplicableCompleteSets TyState
ty_st Type
ty ResidualCompleteMatches
rcm = do
  let cl_res_ty_ok :: ConLike -> DsM Bool
      cl_res_ty_ok :: ConLike -> DsM Bool
cl_res_ty_ok ConLike
cl = do
        env <- DsM FamInstEnvs
dsGetFamInstEnvs
        isJust <$> matchConLikeResTy env ty_st ty cl
  let cm_applicable :: DsCompleteMatch -> DsM Bool
      cm_applicable :: DsCompleteMatch -> DsM Bool
cm_applicable DsCompleteMatch
cm = do
        cls_ok <- (ConLike -> DsM Bool) -> [ConLike] -> DsM Bool
forall (m :: * -> *) (f :: * -> *) a.
(Monad m, Foldable f) =>
(a -> m Bool) -> f a -> m Bool
allM ConLike -> DsM Bool
cl_res_ty_ok (UniqDSet ConLike -> [ConLike]
forall a. UniqDSet a -> [a]
uniqDSetToList (DsCompleteMatch -> UniqDSet ConLike
forall con. CompleteMatchX con -> UniqDSet con
cmConLikes DsCompleteMatch
cm))
        let match_ty_ok = Type -> DsCompleteMatch -> Bool
forall con. Type -> CompleteMatchX con -> Bool
completeMatchAppliesAtType Type
ty DsCompleteMatch
cm
        pure (cls_ok && match_ty_ok)
  applicable_cms <- (DsCompleteMatch -> DsM Bool)
-> [DsCompleteMatch]
-> IOEnv (Env DsGblEnv DsLclEnv) [DsCompleteMatch]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterM DsCompleteMatch -> DsM Bool
cm_applicable (ResidualCompleteMatches -> [DsCompleteMatch]
getRcm ResidualCompleteMatches
rcm)
  tracePm "pickApplicableCompleteSets:" $
    vcat
      [ ppr ty
      , ppr rcm
      , ppr applicable_cms
      ]
  return applicable_cms

{- Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Why can't we define `inhabitationTest` (IT) in terms of
`generateInhabitingPatterns` (GIP) as

  inhabitationTest nabla = do
    nablas <- lift $ generateInhabitingPatterns all_variables 1 nabla
    guard (notNull nablas)

There are a few technical reasons, like the lack of a fuel-tracking approach
to stay decidable, that could be overcome. But the nail in the coffin is
performance: In order to provide good warning messages, GIP commits to *one*
COMPLETE set, and goes through some hoops to find the minimal one. This implies
it has to look at *all* constructors in the residual COMPLETE matches and see if
they match, if only to filter out ill-typed COMPLETE sets
(see Note [Implementation of COMPLETE pragmas]). That is untractable for an
efficient IT on huge enumerations.

But we still need GIP to produce the Nablas as proxies for
uncovered patterns that we display warnings for. It's fine to pay this price
once at the end, but IT is called far more often than that.

Note [Case split inhabiting patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we have an -XEmptyCase,
```hs
f :: Maybe a -> ()
f x = case x of {}
```
we want to show the different missing patterns {'Just _', 'Nothing'} to the user
instead of an uninformative wildcard pattern '_'.

But when we have a match as part of a function definition, such as
```hs
g :: (Bool, [a]) -> ()
g (_, []) = ()
```
we established in #20642 that we *do not* want to report P1={'(False, (_:_))',
'(True, (_:_))'} when we could just give the singleton set P2={'(_, (_:_))'}!
The latter set M is a "minimal cover" of the space of missing patterns S, in
that

1. The union of M is *exactly* S
2. The size of M is minimal under all such candidates.

In terms of 'g', P2 satisfies both (1) and (2). While P1 satisfies (1), it does
not satisfy (2). The set {'_'} satisfies (2), but it does not satisfy (1) as
it also covers the pattern '(_,[])' which is not part of the space of missing
patterns of 'g', so it would be a bad (too conservative) suggestion.

Note that for -XEmptyCase, we don't want to emit a minimal cover. We arrange
that by passing 'CaseSplitTopLevel' to 'generateInhabitingPatterns'. We detect
the -XEmptyCase case in 'reportWarnings' by looking for 'ReportEmptyCase'.
-}