{-
Author: George Karachalias <george.karachalias@cs.kuleuven.be>

Pattern Matching Coverage Checking.
-}

{-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE ViewPatterns  #-}

module Check (
        -- Checking and printing
        checkSingle, checkMatches, checkGuardMatches, isAnyPmCheckEnabled,

        -- See Note [Type and Term Equality Propagation]
        genCaseTmCs1, genCaseTmCs2
    ) where

#include "HsVersions.h"

import GhcPrelude

import TmOracle
import Unify( tcMatchTy )
import DynFlags
import HsSyn
import TcHsSyn
import Id
import ConLike
import Name
import FamInstEnv
import TysPrim (tYPETyCon)
import TysWiredIn
import TyCon
import SrcLoc
import Util
import Outputable
import FastString
import DataCon
import PatSyn
import HscTypes (CompleteMatch(..))
import BasicTypes (Boxity(..))

import DsMonad
import TcSimplify    (tcCheckSatisfiability)
import TcType        (isStringTy)
import Bag
import ErrUtils
import Var           (EvVar)
import TyCoRep
import Type
import UniqSupply
import DsUtils       (isTrueLHsExpr)
import Maybes        (expectJust)
import qualified GHC.LanguageExtensions as LangExt

import Data.List     (find)
import Data.Maybe    (catMaybes, isJust, fromMaybe)
import Control.Monad (forM, when, forM_, zipWithM)
import Coercion
import TcEvidence
import TcSimplify    (tcNormalise)
import IOEnv
import qualified Data.Semigroup as Semi

import ListT (ListT(..), fold, select)

{-
This module checks pattern matches for:
\begin{enumerate}
  \item Equations that are redundant
  \item Equations with inaccessible right-hand-side
  \item Exhaustiveness
\end{enumerate}

The algorithm is based on the paper:

  "GADTs Meet Their Match:
     Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"

    http://people.cs.kuleuven.be/~george.karachalias/papers/p424-karachalias.pdf

%************************************************************************
%*                                                                      *
                     Pattern Match Check Types
%*                                                                      *
%************************************************************************
-}

-- We use the non-determinism monad to apply the algorithm to several
-- possible sets of constructors. Users can specify complete sets of
-- constructors by using COMPLETE pragmas.
-- The algorithm only picks out constructor
-- sets deep in the bowels which makes a simpler `mapM` more difficult to
-- implement. The non-determinism is only used in one place, see the ConVar
-- case in `pmCheckHd`.

type PmM a = ListT DsM a

liftD :: DsM a -> PmM a
liftD :: DsM a -> PmM a
liftD m :: DsM a
m = (forall r. (a -> DsM r -> DsM r) -> DsM r -> DsM r) -> PmM a
forall (m :: * -> *) a.
(forall r. (a -> m r -> m r) -> m r -> m r) -> ListT m a
ListT ((forall r. (a -> DsM r -> DsM r) -> DsM r -> DsM r) -> PmM a)
-> (forall r. (a -> DsM r -> DsM r) -> DsM r -> DsM r) -> PmM a
forall a b. (a -> b) -> a -> b
$ \sk :: a -> DsM r -> DsM r
sk fk :: DsM r
fk -> DsM a
m DsM a -> (a -> DsM r) -> DsM r
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: a
a -> a -> DsM r -> DsM r
sk a
a DsM r
fk

-- Pick the first match complete covered match or otherwise the "best" match.
-- The best match is the one with the least uncovered clauses, ties broken
-- by the number of inaccessible clauses followed by number of redundant
-- clauses.
--
-- This is specified in the
-- "Disambiguating between multiple ``COMPLETE`` pragmas" section of the
-- users' guide. If you update the implementation of this function, make sure
-- to update that section of the users' guide as well.
getResult :: PmM PmResult -> DsM PmResult
getResult :: PmM PmResult -> DsM PmResult
getResult ls :: PmM PmResult
ls
  = do { Maybe PmResult
res <- PmM PmResult
-> (PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult))
-> DsM (Maybe PmResult)
-> DsM (Maybe PmResult)
forall (m :: * -> *) a r.
ListT m a -> (a -> m r -> m r) -> m r -> m r
fold PmM PmResult
ls PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
goM (Maybe PmResult -> DsM (Maybe PmResult)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe PmResult
forall a. Maybe a
Nothing)
       ; case Maybe PmResult
res of
            Nothing -> String -> DsM PmResult
forall a. String -> a
panic "getResult is empty"
            Just a :: PmResult
a  -> PmResult -> DsM PmResult
forall (m :: * -> *) a. Monad m => a -> m a
return PmResult
a }
  where
    goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
    goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
goM mpm :: PmResult
mpm dpm :: DsM (Maybe PmResult)
dpm = do { Maybe PmResult
pmr <- DsM (Maybe PmResult)
dpm
                     ; Maybe PmResult -> DsM (Maybe PmResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe PmResult -> DsM (Maybe PmResult))
-> Maybe PmResult -> DsM (Maybe PmResult)
forall a b. (a -> b) -> a -> b
$ PmResult -> Maybe PmResult
forall a. a -> Maybe a
Just (PmResult -> Maybe PmResult) -> PmResult -> Maybe PmResult
forall a b. (a -> b) -> a -> b
$ Maybe PmResult -> PmResult -> PmResult
go Maybe PmResult
pmr PmResult
mpm }

    -- Careful not to force unecessary results
    go :: Maybe PmResult -> PmResult -> PmResult
    go :: Maybe PmResult -> PmResult -> PmResult
go Nothing rs :: PmResult
rs = PmResult
rs
    go (Just old :: PmResult
old@(PmResult prov :: Provenance
prov rs :: [Located [LPat GhcTc]]
rs (UncoveredPatterns us :: Uncovered
us) is :: [Located [LPat GhcTc]]
is)) new :: PmResult
new
      | Uncovered -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Uncovered
us Bool -> Bool -> Bool
&& [Located [LPat GhcTc]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Located [LPat GhcTc]]
rs Bool -> Bool -> Bool
&& [Located [LPat GhcTc]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Located [LPat GhcTc]]
is = PmResult
old
      | Bool
otherwise =
        let PmResult prov' :: Provenance
prov' rs' :: [Located [LPat GhcTc]]
rs' (UncoveredPatterns us' :: Uncovered
us') is' :: [Located [LPat GhcTc]]
is' = PmResult
new
        in case Uncovered -> Uncovered -> Ordering
forall a b. [a] -> [b] -> Ordering
compareLength Uncovered
us Uncovered
us'
                Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` ([Located [LPat GhcTc]] -> [Located [LPat GhcTc]] -> Ordering
forall a b. [a] -> [b] -> Ordering
compareLength [Located [LPat GhcTc]]
is [Located [LPat GhcTc]]
is')
                Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` ([Located [LPat GhcTc]] -> [Located [LPat GhcTc]] -> Ordering
forall a b. [a] -> [b] -> Ordering
compareLength [Located [LPat GhcTc]]
rs [Located [LPat GhcTc]]
rs')
                Ordering -> Ordering -> Ordering
forall a. Monoid a => a -> a -> a
`mappend` (Provenance -> Provenance -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Provenance
prov Provenance
prov') of
              GT  -> PmResult
new
              EQ  -> PmResult
new
              LT  -> PmResult
old
    go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new :: PmResult
_new
      = String -> PmResult
forall a. String -> a
panic "getResult: No inhabitation candidates"

data PatTy = PAT | VA -- Used only as a kind, to index PmPat

-- The *arity* of a PatVec [p1,..,pn] is
-- the number of p1..pn that are not Guards

data PmPat :: PatTy -> * where
  PmCon  :: { PmPat t -> ConLike
pm_con_con     :: ConLike
            , PmPat t -> [Type]
pm_con_arg_tys :: [Type]
            , PmPat t -> [TyVar]
pm_con_tvs     :: [TyVar]
            , PmPat t -> [TyVar]
pm_con_dicts   :: [EvVar]
            , PmPat t -> [PmPat t]
pm_con_args    :: [PmPat t] } -> PmPat t
            -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
  PmVar  :: { PmPat t -> TyVar
pm_var_id   :: Id } -> PmPat t
  PmLit  :: { PmPat t -> PmLit
pm_lit_lit  :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
  PmNLit :: { PmPat 'VA -> TyVar
pm_lit_id   :: Id
            , PmPat 'VA -> [PmLit]
pm_lit_not  :: [PmLit] } -> PmPat 'VA
  PmGrd  :: { PmPat 'PAT -> PatVec
pm_grd_pv   :: PatVec
            , PmPat 'PAT -> PmExpr
pm_grd_expr :: PmExpr  } -> PmPat 'PAT

instance Outputable (PmPat a) where
  ppr :: PmPat a -> SDoc
ppr = PmPat a -> SDoc
forall (a :: PatTy). PmPat a -> SDoc
pprPmPatDebug

-- data T a where
--     MkT :: forall p q. (Eq p, Ord q) => p -> q -> T [p]
-- or  MkT :: forall p q r. (Eq p, Ord q, [p] ~ r) => p -> q -> T r

type Pattern = PmPat 'PAT -- ^ Patterns
type ValAbs  = PmPat 'VA  -- ^ Value Abstractions

type PatVec = [Pattern]             -- ^ Pattern Vectors
data ValVec = ValVec [ValAbs] Delta -- ^ Value Vector Abstractions

-- | Term and type constraints to accompany each value vector abstraction.
-- For efficiency, we store the term oracle state instead of the term
-- constraints. TODO: Do the same for the type constraints?
data Delta = MkDelta { Delta -> Bag TyVar
delta_ty_cs :: Bag EvVar
                     , Delta -> TmState
delta_tm_cs :: TmState }

type ValSetAbs = [ValVec]  -- ^ Value Set Abstractions
type Uncovered = ValSetAbs

-- Instead of keeping the whole sets in memory, we keep a boolean for both the
-- covered and the divergent set (we store the uncovered set though, since we
-- want to print it). For both the covered and the divergent we have:
--
--   True <=> The set is non-empty
--
-- hence:
--  C = True             ==> Useful clause (no warning)
--  C = False, D = True  ==> Clause with inaccessible RHS
--  C = False, D = False ==> Redundant clause

data Covered = Covered | NotCovered
  deriving Int -> Covered -> ShowS
[Covered] -> ShowS
Covered -> String
(Int -> Covered -> ShowS)
-> (Covered -> String) -> ([Covered] -> ShowS) -> Show Covered
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Covered] -> ShowS
$cshowList :: [Covered] -> ShowS
show :: Covered -> String
$cshow :: Covered -> String
showsPrec :: Int -> Covered -> ShowS
$cshowsPrec :: Int -> Covered -> ShowS
Show

instance Outputable Covered where
  ppr :: Covered -> SDoc
ppr (Covered
Covered) = String -> SDoc
text "Covered"
  ppr (Covered
NotCovered) = String -> SDoc
text "NotCovered"

-- Like the or monoid for booleans
-- Covered = True, Uncovered = False
instance Semi.Semigroup Covered where
  Covered <> :: Covered -> Covered -> Covered
<> _ = Covered
Covered
  _ <> Covered = Covered
Covered
  NotCovered <> NotCovered = Covered
NotCovered

instance Monoid Covered where
  mempty :: Covered
mempty = Covered
NotCovered
  mappend :: Covered -> Covered -> Covered
mappend = Covered -> Covered -> Covered
forall a. Semigroup a => a -> a -> a
(Semi.<>)

data Diverged = Diverged | NotDiverged
  deriving Int -> Diverged -> ShowS
[Diverged] -> ShowS
Diverged -> String
(Int -> Diverged -> ShowS)
-> (Diverged -> String) -> ([Diverged] -> ShowS) -> Show Diverged
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Diverged] -> ShowS
$cshowList :: [Diverged] -> ShowS
show :: Diverged -> String
$cshow :: Diverged -> String
showsPrec :: Int -> Diverged -> ShowS
$cshowsPrec :: Int -> Diverged -> ShowS
Show

instance Outputable Diverged where
  ppr :: Diverged -> SDoc
ppr Diverged = String -> SDoc
text "Diverged"
  ppr NotDiverged = String -> SDoc
text "NotDiverged"

instance Semi.Semigroup Diverged where
  Diverged <> :: Diverged -> Diverged -> Diverged
<> _ = Diverged
Diverged
  _ <> Diverged = Diverged
Diverged
  NotDiverged <> NotDiverged = Diverged
NotDiverged

instance Monoid Diverged where
  mempty :: Diverged
mempty = Diverged
NotDiverged
  mappend :: Diverged -> Diverged -> Diverged
mappend = Diverged -> Diverged -> Diverged
forall a. Semigroup a => a -> a -> a
(Semi.<>)

-- | When we learned that a given match group is complete
data Provenance =
                  FromBuiltin -- ^  From the original definition of the type
                              --    constructor.
                | FromComplete -- ^ From a user-provided @COMPLETE@ pragma
  deriving (Int -> Provenance -> ShowS
[Provenance] -> ShowS
Provenance -> String
(Int -> Provenance -> ShowS)
-> (Provenance -> String)
-> ([Provenance] -> ShowS)
-> Show Provenance
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Provenance] -> ShowS
$cshowList :: [Provenance] -> ShowS
show :: Provenance -> String
$cshow :: Provenance -> String
showsPrec :: Int -> Provenance -> ShowS
$cshowsPrec :: Int -> Provenance -> ShowS
Show, Provenance -> Provenance -> Bool
(Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool) -> Eq Provenance
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Provenance -> Provenance -> Bool
$c/= :: Provenance -> Provenance -> Bool
== :: Provenance -> Provenance -> Bool
$c== :: Provenance -> Provenance -> Bool
Eq, Eq Provenance
Eq Provenance =>
(Provenance -> Provenance -> Ordering)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Bool)
-> (Provenance -> Provenance -> Provenance)
-> (Provenance -> Provenance -> Provenance)
-> Ord Provenance
Provenance -> Provenance -> Bool
Provenance -> Provenance -> Ordering
Provenance -> Provenance -> Provenance
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Provenance -> Provenance -> Provenance
$cmin :: Provenance -> Provenance -> Provenance
max :: Provenance -> Provenance -> Provenance
$cmax :: Provenance -> Provenance -> Provenance
>= :: Provenance -> Provenance -> Bool
$c>= :: Provenance -> Provenance -> Bool
> :: Provenance -> Provenance -> Bool
$c> :: Provenance -> Provenance -> Bool
<= :: Provenance -> Provenance -> Bool
$c<= :: Provenance -> Provenance -> Bool
< :: Provenance -> Provenance -> Bool
$c< :: Provenance -> Provenance -> Bool
compare :: Provenance -> Provenance -> Ordering
$ccompare :: Provenance -> Provenance -> Ordering
$cp1Ord :: Eq Provenance
Ord)

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

instance Semi.Semigroup Provenance where
  FromComplete <> :: Provenance -> Provenance -> Provenance
<> _ = Provenance
FromComplete
  _ <> FromComplete = Provenance
FromComplete
  _ <> _ = Provenance
FromBuiltin

instance Monoid Provenance where
  mempty :: Provenance
mempty = Provenance
FromBuiltin
  mappend :: Provenance -> Provenance -> Provenance
mappend = Provenance -> Provenance -> Provenance
forall a. Semigroup a => a -> a -> a
(Semi.<>)

data PartialResult = PartialResult {
                        PartialResult -> Provenance
presultProvenance :: Provenance
                         -- keep track of provenance because we don't want
                         -- to warn about redundant matches if the result
                         -- is contaminated with a COMPLETE pragma
                      , PartialResult -> Covered
presultCovered :: Covered
                      , PartialResult -> Uncovered
presultUncovered :: Uncovered
                      , PartialResult -> Diverged
presultDivergent :: Diverged }

instance Outputable PartialResult where
  ppr :: PartialResult -> SDoc
ppr (PartialResult prov :: Provenance
prov c :: Covered
c vsa :: Uncovered
vsa d :: Diverged
d)
           = String -> SDoc
text "PartialResult" SDoc -> SDoc -> SDoc
<+> Provenance -> SDoc
forall a. Outputable a => a -> SDoc
ppr Provenance
prov SDoc -> SDoc -> SDoc
<+> Covered -> SDoc
forall a. Outputable a => a -> SDoc
ppr Covered
c
                                  SDoc -> SDoc -> SDoc
<+> Diverged -> SDoc
forall a. Outputable a => a -> SDoc
ppr Diverged
d SDoc -> SDoc -> SDoc
<+> Uncovered -> SDoc
forall a. Outputable a => a -> SDoc
ppr Uncovered
vsa


instance Semi.Semigroup PartialResult where
  (PartialResult prov1 :: Provenance
prov1 cs1 :: Covered
cs1 vsa1 :: Uncovered
vsa1 ds1 :: Diverged
ds1)
    <> :: PartialResult -> PartialResult -> PartialResult
<> (PartialResult prov2 :: Provenance
prov2 cs2 :: Covered
cs2 vsa2 :: Uncovered
vsa2 ds2 :: Diverged
ds2)
      = Provenance -> Covered -> Uncovered -> Diverged -> PartialResult
PartialResult (Provenance
prov1 Provenance -> Provenance -> Provenance
forall a. Semigroup a => a -> a -> a
Semi.<> Provenance
prov2)
                      (Covered
cs1 Covered -> Covered -> Covered
forall a. Semigroup a => a -> a -> a
Semi.<> Covered
cs2)
                      (Uncovered
vsa1 Uncovered -> Uncovered -> Uncovered
forall a. Semigroup a => a -> a -> a
Semi.<> Uncovered
vsa2)
                      (Diverged
ds1 Diverged -> Diverged -> Diverged
forall a. Semigroup a => a -> a -> a
Semi.<> Diverged
ds2)


instance Monoid PartialResult where
  mempty :: PartialResult
mempty = Provenance -> Covered -> Uncovered -> Diverged -> PartialResult
PartialResult Provenance
forall a. Monoid a => a
mempty Covered
forall a. Monoid a => a
mempty [] Diverged
forall a. Monoid a => a
mempty
  mappend :: PartialResult -> PartialResult -> PartialResult
mappend = PartialResult -> PartialResult -> PartialResult
forall a. Semigroup a => a -> a -> a
(Semi.<>)

-- newtype ChoiceOf a = ChoiceOf [a]

-- | Pattern check result
--
-- * Redundant clauses
-- * Not-covered clauses (or their type, if no pattern is available)
-- * Clauses with inaccessible RHS
--
-- More details about the classification of clauses into useful, redundant
-- and with inaccessible right hand side can be found here:
--
--     https://ghc.haskell.org/trac/ghc/wiki/PatternMatchCheck
--
data PmResult =
  PmResult {
      PmResult -> Provenance
pmresultProvenance   :: Provenance
    , PmResult -> [Located [LPat GhcTc]]
pmresultRedundant    :: [Located [LPat GhcTc]]
    , PmResult -> UncoveredCandidates
pmresultUncovered    :: UncoveredCandidates
    , PmResult -> [Located [LPat GhcTc]]
pmresultInaccessible :: [Located [LPat GhcTc]] }

-- | Either a list of patterns that are not covered, or their type, in case we
-- have no patterns at hand. Not having patterns at hand can arise when
-- handling EmptyCase expressions, in two cases:
--
-- * The type of the scrutinee is a trivially inhabited type (like Int or Char)
-- * The type of the scrutinee cannot be reduced to WHNF.
--
-- In both these cases we have no inhabitation candidates for the type at hand,
-- but we don't want to issue just a wildcard as missing. Instead, we print a
-- type annotated wildcard, so that the user knows what kind of patterns is
-- expected (e.g. (_ :: Int), or (_ :: F Int), where F Int does not reduce).
data UncoveredCandidates = UncoveredPatterns Uncovered
                         | TypeOfUncovered Type

-- | The empty pattern check result
emptyPmResult :: PmResult
emptyPmResult :: PmResult
emptyPmResult = Provenance
-> [Located [LPat GhcTc]]
-> UncoveredCandidates
-> [Located [LPat GhcTc]]
-> PmResult
PmResult Provenance
FromBuiltin [] (Uncovered -> UncoveredCandidates
UncoveredPatterns []) []

-- | Non-exhaustive empty case with unknown/trivial inhabitants
uncoveredWithTy :: Type -> PmResult
uncoveredWithTy :: Type -> PmResult
uncoveredWithTy ty :: Type
ty = Provenance
-> [Located [LPat GhcTc]]
-> UncoveredCandidates
-> [Located [LPat GhcTc]]
-> PmResult
PmResult Provenance
FromBuiltin [] (Type -> UncoveredCandidates
TypeOfUncovered Type
ty) []

{-
%************************************************************************
%*                                                                      *
       Entry points to the checker: checkSingle and checkMatches
%*                                                                      *
%************************************************************************
-}

-- | Check a single pattern binding (let)
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
checkSingle :: DynFlags -> DsMatchContext -> TyVar -> LPat GhcTc -> DsM ()
checkSingle dflags :: DynFlags
dflags ctxt :: DsMatchContext
ctxt@(DsMatchContext _ locn :: SrcSpan
locn) var :: TyVar
var p :: LPat GhcTc
p = do
  String -> SDoc -> DsM ()
tracePmD "checkSingle" ([SDoc] -> SDoc
vcat [DsMatchContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr DsMatchContext
ctxt, TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
var, LPat GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr LPat GhcTc
p])
  Either IOEnvFailure PmResult
mb_pm_res <- DsM PmResult
-> IOEnv (Env DsGblEnv DsLclEnv) (Either IOEnvFailure PmResult)
forall env r. IOEnv env r -> IOEnv env (Either IOEnvFailure r)
tryM (PmM PmResult -> DsM PmResult
getResult (SrcSpan -> TyVar -> LPat GhcTc -> PmM PmResult
checkSingle' SrcSpan
locn TyVar
var LPat GhcTc
p))
  case Either IOEnvFailure PmResult
mb_pm_res of
    Left  _   -> DynFlags -> DsMatchContext -> DsM ()
warnPmIters DynFlags
dflags DsMatchContext
ctxt
    Right res :: PmResult
res -> DynFlags -> DsMatchContext -> PmResult -> DsM ()
dsPmWarn DynFlags
dflags DsMatchContext
ctxt PmResult
res

-- | Check a single pattern binding (let)
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
checkSingle' :: SrcSpan -> TyVar -> LPat GhcTc -> PmM PmResult
checkSingle' locn :: SrcSpan
locn var :: TyVar
var p :: LPat GhcTc
p = do
  DsM () -> PmM ()
forall a. DsM a -> PmM a
liftD DsM ()
resetPmIterDs -- set the iter-no to zero
  FamInstEnvs
fam_insts <- DsM FamInstEnvs -> PmM FamInstEnvs
forall a. DsM a -> PmM a
liftD DsM FamInstEnvs
dsGetFamInstEnvs
  PatVec
clause    <- DsM PatVec -> PmM PatVec
forall a. DsM a -> PmM a
liftD (DsM PatVec -> PmM PatVec) -> DsM PatVec -> PmM PatVec
forall a b. (a -> b) -> a -> b
$ FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts LPat GhcTc
p
  Uncovered
missing   <- [TyVar] -> PmM Uncovered
mkInitialUncovered [TyVar
var]
  String -> SDoc -> PmM ()
tracePm "checkSingle: missing" ([SDoc] -> SDoc
vcat ((ValVec -> SDoc) -> Uncovered -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ValVec -> SDoc
pprValVecDebug Uncovered
missing))
                                 -- no guards
  PartialResult prov :: Provenance
prov cs :: Covered
cs us :: Uncovered
us ds :: Diverged
ds <- (ValVec -> PmM PartialResult) -> Uncovered -> PmM PartialResult
runMany (PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI PatVec
clause []) Uncovered
missing
  let us' :: UncoveredCandidates
us' = Uncovered -> UncoveredCandidates
UncoveredPatterns Uncovered
us
  PmResult -> PmM PmResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PmResult -> PmM PmResult) -> PmResult -> PmM PmResult
forall a b. (a -> b) -> a -> b
$ case (Covered
cs,Diverged
ds) of
    (Covered,  _    )         -> Provenance
-> [Located [LPat GhcTc]]
-> UncoveredCandidates
-> [Located [LPat GhcTc]]
-> PmResult
PmResult Provenance
prov [] UncoveredCandidates
us' [] -- useful
    (NotCovered, NotDiverged) -> Provenance
-> [Located [LPat GhcTc]]
-> UncoveredCandidates
-> [Located [LPat GhcTc]]
-> PmResult
PmResult Provenance
prov [Located [LPat GhcTc]]
m  UncoveredCandidates
us' [] -- redundant
    (NotCovered, Diverged )   -> Provenance
-> [Located [LPat GhcTc]]
-> UncoveredCandidates
-> [Located [LPat GhcTc]]
-> PmResult
PmResult Provenance
prov [] UncoveredCandidates
us' [Located [LPat GhcTc]]
m  -- inaccessible rhs
  where m :: [Located [LPat GhcTc]]
m = [SrcSpan
-> SrcSpanLess (Located [LPat GhcTc]) -> Located [LPat GhcTc]
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
locn [SrcSpan -> SrcSpanLess (LPat GhcTc) -> LPat GhcTc
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
locn SrcSpanLess (LPat GhcTc)
LPat GhcTc
p]]

-- | Exhaustive for guard matches, is used for guards in pattern bindings and
-- in @MultiIf@ expressions.
checkGuardMatches :: HsMatchContext Name          -- Match context
                  -> GRHSs GhcTc (LHsExpr GhcTc)  -- Guarded RHSs
                  -> DsM ()
checkGuardMatches :: HsMatchContext Name -> GRHSs GhcTc (LHsExpr GhcTc) -> DsM ()
checkGuardMatches hs_ctx :: HsMatchContext Name
hs_ctx guards :: GRHSs GhcTc (LHsExpr GhcTc)
guards@(GRHSs _ grhss :: [LGRHS GhcTc (LHsExpr GhcTc)]
grhss _) = do
    DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
    let combinedLoc :: SrcSpan
combinedLoc = (SrcSpan -> SrcSpan -> SrcSpan) -> [SrcSpan] -> SrcSpan
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 SrcSpan -> SrcSpan -> SrcSpan
combineSrcSpans ((LGRHS GhcTc (LHsExpr GhcTc) -> SrcSpan)
-> [LGRHS GhcTc (LHsExpr GhcTc)] -> [SrcSpan]
forall a b. (a -> b) -> [a] -> [b]
map LGRHS GhcTc (LHsExpr GhcTc) -> SrcSpan
forall a. HasSrcSpan a => a -> SrcSpan
getLoc [LGRHS GhcTc (LHsExpr GhcTc)]
grhss)
        dsMatchContext :: DsMatchContext
dsMatchContext = HsMatchContext Name -> SrcSpan -> DsMatchContext
DsMatchContext HsMatchContext Name
hs_ctx SrcSpan
combinedLoc
        match :: LMatch GhcTc (LHsExpr GhcTc)
match = SrcSpan
-> SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc))
-> LMatch GhcTc (LHsExpr GhcTc)
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
combinedLoc (SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc))
 -> LMatch GhcTc (LHsExpr GhcTc))
-> SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc))
-> LMatch GhcTc (LHsExpr GhcTc)
forall a b. (a -> b) -> a -> b
$
                  Match :: forall p body.
XCMatch p body
-> HsMatchContext (NameOrRdrName (IdP p))
-> [LPat p]
-> GRHSs p body
-> Match p body
Match { m_ext :: XCMatch GhcTc (LHsExpr GhcTc)
m_ext = XCMatch GhcTc (LHsExpr GhcTc)
NoExt
noExt
                        , m_ctxt :: HsMatchContext (NameOrRdrName (IdP GhcTc))
m_ctxt = HsMatchContext Name
HsMatchContext (NameOrRdrName (IdP GhcTc))
hs_ctx
                        , m_pats :: [LPat GhcTc]
m_pats = []
                        , m_grhss :: GRHSs GhcTc (LHsExpr GhcTc)
m_grhss = GRHSs GhcTc (LHsExpr GhcTc)
guards }
    DynFlags
-> DsMatchContext
-> [TyVar]
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> DsM ()
checkMatches DynFlags
dflags DsMatchContext
dsMatchContext [] [LMatch GhcTc (LHsExpr GhcTc)
match]
checkGuardMatches _ (XGRHSs _) = String -> DsM ()
forall a. String -> a
panic "checkGuardMatches"

-- | Check a matchgroup (case, functions, etc.)
checkMatches :: DynFlags -> DsMatchContext
             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
checkMatches :: DynFlags
-> DsMatchContext
-> [TyVar]
-> [LMatch GhcTc (LHsExpr GhcTc)]
-> DsM ()
checkMatches dflags :: DynFlags
dflags ctxt :: DsMatchContext
ctxt vars :: [TyVar]
vars matches :: [LMatch GhcTc (LHsExpr GhcTc)]
matches = do
  String -> SDoc -> DsM ()
tracePmD "checkMatches" (SDoc -> Int -> SDoc -> SDoc
hang ([SDoc] -> SDoc
vcat [DsMatchContext -> SDoc
forall a. Outputable a => a -> SDoc
ppr DsMatchContext
ctxt
                               , [TyVar] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [TyVar]
vars
                               , String -> SDoc
text "Matches:"])
                               2
                               ([SDoc] -> SDoc
vcat ((LMatch GhcTc (LHsExpr GhcTc) -> SDoc)
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map LMatch GhcTc (LHsExpr GhcTc) -> SDoc
forall a. Outputable a => a -> SDoc
ppr [LMatch GhcTc (LHsExpr GhcTc)]
matches)))
  Either IOEnvFailure PmResult
mb_pm_res <- DsM PmResult
-> IOEnv (Env DsGblEnv DsLclEnv) (Either IOEnvFailure PmResult)
forall env r. IOEnv env r -> IOEnv env (Either IOEnvFailure r)
tryM (DsM PmResult
 -> IOEnv (Env DsGblEnv DsLclEnv) (Either IOEnvFailure PmResult))
-> DsM PmResult
-> IOEnv (Env DsGblEnv DsLclEnv) (Either IOEnvFailure PmResult)
forall a b. (a -> b) -> a -> b
$ PmM PmResult -> DsM PmResult
getResult (PmM PmResult -> DsM PmResult) -> PmM PmResult -> DsM PmResult
forall a b. (a -> b) -> a -> b
$ case [LMatch GhcTc (LHsExpr GhcTc)]
matches of
    -- Check EmptyCase separately
    -- See Note [Checking EmptyCase Expressions]
    [] | [var :: TyVar
var] <- [TyVar]
vars -> TyVar -> PmM PmResult
checkEmptyCase' TyVar
var
    _normal_match :: [LMatch GhcTc (LHsExpr GhcTc)]
_normal_match      -> [TyVar] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
checkMatches' [TyVar]
vars [LMatch GhcTc (LHsExpr GhcTc)]
matches
  case Either IOEnvFailure PmResult
mb_pm_res of
    Left  _   -> DynFlags -> DsMatchContext -> DsM ()
warnPmIters DynFlags
dflags DsMatchContext
ctxt
    Right res :: PmResult
res -> DynFlags -> DsMatchContext -> PmResult -> DsM ()
dsPmWarn DynFlags
dflags DsMatchContext
ctxt PmResult
res

-- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
-- list of matches. For empty case expressions, use checkEmptyCase' instead.
checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
checkMatches' :: [TyVar] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
checkMatches' vars :: [TyVar]
vars matches :: [LMatch GhcTc (LHsExpr GhcTc)]
matches
  | [LMatch GhcTc (LHsExpr GhcTc)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LMatch GhcTc (LHsExpr GhcTc)]
matches = String -> PmM PmResult
forall a. String -> a
panic "checkMatches': EmptyCase"
  | Bool
otherwise = do
      DsM () -> PmM ()
forall a. DsM a -> PmM a
liftD DsM ()
resetPmIterDs -- set the iter-no to zero
      Uncovered
missing    <- [TyVar] -> PmM Uncovered
mkInitialUncovered [TyVar]
vars
      String -> SDoc -> PmM ()
tracePm "checkMatches': missing" ([SDoc] -> SDoc
vcat ((ValVec -> SDoc) -> Uncovered -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ValVec -> SDoc
pprValVecDebug Uncovered
missing))
      (prov :: Provenance
prov, rs :: [LMatch GhcTc (LHsExpr GhcTc)]
rs,us :: Uncovered
us,ds :: [LMatch GhcTc (LHsExpr GhcTc)]
ds) <- [LMatch GhcTc (LHsExpr GhcTc)]
-> Uncovered
-> PmM
     (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)])
go [LMatch GhcTc (LHsExpr GhcTc)]
matches Uncovered
missing
      PmResult -> PmM PmResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PmResult -> PmM PmResult) -> PmResult -> PmM PmResult
forall a b. (a -> b) -> a -> b
$ PmResult :: Provenance
-> [Located [LPat GhcTc]]
-> UncoveredCandidates
-> [Located [LPat GhcTc]]
-> PmResult
PmResult {
                   pmresultProvenance :: Provenance
pmresultProvenance   = Provenance
prov
                 , pmresultRedundant :: [Located [LPat GhcTc]]
pmresultRedundant    = (LMatch GhcTc (LHsExpr GhcTc) -> Located [LPat GhcTc])
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [Located [LPat GhcTc]]
forall a b. (a -> b) -> [a] -> [b]
map LMatch GhcTc (LHsExpr GhcTc) -> Located [LPat GhcTc]
forall id body. LMatch id body -> Located [LPat id]
hsLMatchToLPats [LMatch GhcTc (LHsExpr GhcTc)]
rs
                 , pmresultUncovered :: UncoveredCandidates
pmresultUncovered    = Uncovered -> UncoveredCandidates
UncoveredPatterns Uncovered
us
                 , pmresultInaccessible :: [Located [LPat GhcTc]]
pmresultInaccessible = (LMatch GhcTc (LHsExpr GhcTc) -> Located [LPat GhcTc])
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [Located [LPat GhcTc]]
forall a b. (a -> b) -> [a] -> [b]
map LMatch GhcTc (LHsExpr GhcTc) -> Located [LPat GhcTc]
forall id body. LMatch id body -> Located [LPat id]
hsLMatchToLPats [LMatch GhcTc (LHsExpr GhcTc)]
ds }
  where
    go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
       -> PmM (Provenance
              , [LMatch GhcTc (LHsExpr GhcTc)]
              , Uncovered
              , [LMatch GhcTc (LHsExpr GhcTc)])
    go :: [LMatch GhcTc (LHsExpr GhcTc)]
-> Uncovered
-> PmM
     (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)])
go []     missing :: Uncovered
missing = (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
 [LMatch GhcTc (LHsExpr GhcTc)])
-> PmM
     (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Provenance
forall a. Monoid a => a
mempty, [], Uncovered
missing, [])
    go (m :: LMatch GhcTc (LHsExpr GhcTc)
m:ms :: [LMatch GhcTc (LHsExpr GhcTc)]
ms) missing :: Uncovered
missing = do
      String -> SDoc -> PmM ()
tracePm "checMatches': go" (LMatch GhcTc (LHsExpr GhcTc) -> SDoc
forall a. Outputable a => a -> SDoc
ppr LMatch GhcTc (LHsExpr GhcTc)
m SDoc -> SDoc -> SDoc
$$ Uncovered -> SDoc
forall a. Outputable a => a -> SDoc
ppr Uncovered
missing)
      FamInstEnvs
fam_insts          <- DsM FamInstEnvs -> PmM FamInstEnvs
forall a. DsM a -> PmM a
liftD DsM FamInstEnvs
dsGetFamInstEnvs
      (clause :: PatVec
clause, guards :: [PatVec]
guards)   <- DsM (PatVec, [PatVec]) -> PmM (PatVec, [PatVec])
forall a. DsM a -> PmM a
liftD (DsM (PatVec, [PatVec]) -> PmM (PatVec, [PatVec]))
-> DsM (PatVec, [PatVec]) -> PmM (PatVec, [PatVec])
forall a b. (a -> b) -> a -> b
$ FamInstEnvs
-> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PatVec, [PatVec])
translateMatch FamInstEnvs
fam_insts LMatch GhcTc (LHsExpr GhcTc)
m
      r :: PartialResult
r@(PartialResult prov :: Provenance
prov cs :: Covered
cs missing' :: Uncovered
missing' ds :: Diverged
ds)
        <- (ValVec -> PmM PartialResult) -> Uncovered -> PmM PartialResult
runMany (PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI PatVec
clause [PatVec]
guards) Uncovered
missing
      String -> SDoc -> PmM ()
tracePm "checMatches': go: res" (PartialResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr PartialResult
r)
      (ms_prov :: Provenance
ms_prov, rs :: [LMatch GhcTc (LHsExpr GhcTc)]
rs, final_u :: Uncovered
final_u, is :: [LMatch GhcTc (LHsExpr GhcTc)]
is)  <- [LMatch GhcTc (LHsExpr GhcTc)]
-> Uncovered
-> PmM
     (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)])
go [LMatch GhcTc (LHsExpr GhcTc)]
ms Uncovered
missing'
      let final_prov :: Provenance
final_prov = Provenance
prov Provenance -> Provenance -> Provenance
forall a. Monoid a => a -> a -> a
`mappend` Provenance
ms_prov
      (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
 [LMatch GhcTc (LHsExpr GhcTc)])
-> PmM
     (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
  [LMatch GhcTc (LHsExpr GhcTc)])
 -> PmM
      (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
       [LMatch GhcTc (LHsExpr GhcTc)]))
-> (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
    [LMatch GhcTc (LHsExpr GhcTc)])
-> PmM
     (Provenance, [LMatch GhcTc (LHsExpr GhcTc)], Uncovered,
      [LMatch GhcTc (LHsExpr GhcTc)])
forall a b. (a -> b) -> a -> b
$ case (Covered
cs, Diverged
ds) of
        -- useful
        (Covered,  _    )        -> (Provenance
final_prov,  [LMatch GhcTc (LHsExpr GhcTc)]
rs, Uncovered
final_u,   [LMatch GhcTc (LHsExpr GhcTc)]
is)
        -- redundant
        (NotCovered, NotDiverged) -> (Provenance
final_prov, LMatch GhcTc (LHsExpr GhcTc)
mLMatch GhcTc (LHsExpr GhcTc)
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [LMatch GhcTc (LHsExpr GhcTc)]
forall a. a -> [a] -> [a]
:[LMatch GhcTc (LHsExpr GhcTc)]
rs, Uncovered
final_u,[LMatch GhcTc (LHsExpr GhcTc)]
is)
        -- inaccessible
        (NotCovered, Diverged )   -> (Provenance
final_prov,  [LMatch GhcTc (LHsExpr GhcTc)]
rs, Uncovered
final_u, LMatch GhcTc (LHsExpr GhcTc)
mLMatch GhcTc (LHsExpr GhcTc)
-> [LMatch GhcTc (LHsExpr GhcTc)] -> [LMatch GhcTc (LHsExpr GhcTc)]
forall a. a -> [a] -> [a]
:[LMatch GhcTc (LHsExpr GhcTc)]
is)

    hsLMatchToLPats :: LMatch id body -> Located [LPat id]
    hsLMatchToLPats :: LMatch id body -> Located [LPat id]
hsLMatchToLPats (LMatch id body -> Located (SrcSpanLess (LMatch id body))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L l :: SrcSpan
l (Match { m_pats = pats })) = SrcSpan -> SrcSpanLess (Located [LPat id]) -> Located [LPat id]
forall a. HasSrcSpan a => SrcSpan -> SrcSpanLess a -> a
cL SrcSpan
l [LPat id]
SrcSpanLess (Located [LPat id])
pats
    hsLMatchToLPats _                                   = String -> Located [LPat id]
forall a. String -> a
panic "checMatches'"

-- | Check an empty case expression. Since there are no clauses to process, we
--   only compute the uncovered set. See Note [Checking EmptyCase Expressions]
--   for details.
checkEmptyCase' :: Id -> PmM PmResult
checkEmptyCase' :: TyVar -> PmM PmResult
checkEmptyCase' var :: TyVar
var = do
  Delta
tm_ty_css     <- PmM Delta
pmInitialTmTyCs
  Either Type (TyCon, [InhabitationCandidate])
mb_candidates <- Bag TyVar
-> Type -> PmM (Either Type (TyCon, [InhabitationCandidate]))
inhabitationCandidates (Delta -> Bag TyVar
delta_ty_cs Delta
tm_ty_css) (TyVar -> Type
idType TyVar
var)
  case Either Type (TyCon, [InhabitationCandidate])
mb_candidates of
    -- Inhabitation checking failed / the type is trivially inhabited
    Left ty :: Type
ty -> PmResult -> PmM PmResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> PmResult
uncoveredWithTy Type
ty)

    -- A list of inhabitant candidates is available: Check for each
    -- one for the satisfiability of the constraints it gives rise to.
    Right (_, candidates :: [InhabitationCandidate]
candidates) -> do
      Uncovered
missing_m <- ((InhabitationCandidate -> ListT DsM (Maybe ValVec))
 -> [InhabitationCandidate] -> PmM Uncovered)
-> [InhabitationCandidate]
-> (InhabitationCandidate -> ListT DsM (Maybe ValVec))
-> PmM Uncovered
forall a b c. (a -> b -> c) -> b -> a -> c
flip (InhabitationCandidate -> ListT DsM (Maybe ValVec))
-> [InhabitationCandidate] -> PmM Uncovered
forall (m :: * -> *) a b.
Applicative m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM [InhabitationCandidate]
candidates ((InhabitationCandidate -> ListT DsM (Maybe ValVec))
 -> PmM Uncovered)
-> (InhabitationCandidate -> ListT DsM (Maybe ValVec))
-> PmM Uncovered
forall a b. (a -> b) -> a -> b
$
          \InhabitationCandidate{ ic_val_abs :: InhabitationCandidate -> PmPat 'VA
ic_val_abs = PmPat 'VA
va, ic_tm_ct :: InhabitationCandidate -> ComplexEq
ic_tm_ct = ComplexEq
tm_ct
                                , ic_ty_cs :: InhabitationCandidate -> Bag TyVar
ic_ty_cs = Bag TyVar
ty_cs
                                , ic_strict_arg_tys :: InhabitationCandidate -> [Type]
ic_strict_arg_tys = [Type]
strict_arg_tys } -> do
        Maybe Delta
mb_sat <- Delta -> ComplexEq -> Bag TyVar -> [Type] -> PmM (Maybe Delta)
pmIsSatisfiable Delta
tm_ty_css ComplexEq
tm_ct Bag TyVar
ty_cs [Type]
strict_arg_tys
        Maybe ValVec -> ListT DsM (Maybe ValVec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ValVec -> ListT DsM (Maybe ValVec))
-> Maybe ValVec -> ListT DsM (Maybe ValVec)
forall a b. (a -> b) -> a -> b
$ (Delta -> ValVec) -> Maybe Delta -> Maybe ValVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA
va]) Maybe Delta
mb_sat
      PmResult -> PmM PmResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PmResult -> PmM PmResult) -> PmResult -> PmM PmResult
forall a b. (a -> b) -> a -> b
$ if Uncovered -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Uncovered
missing_m
        then PmResult
emptyPmResult
        else Provenance
-> [Located [LPat GhcTc]]
-> UncoveredCandidates
-> [Located [LPat GhcTc]]
-> PmResult
PmResult Provenance
FromBuiltin [] (Uncovered -> UncoveredCandidates
UncoveredPatterns Uncovered
missing_m) []

-- | 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 ty :: Type
ty
  = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
      Just (tc :: TyCon
tc, ty_args :: [Type]
ty_args)
             | TyCon -> Bool
is_algebraic_like TyCon
tc Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isFamilyTyCon TyCon
tc)
             -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
      _other :: Maybe (TyCon, [Type])
_other -> Bool
False
  where
    -- This returns True for TyCons which /act like/ algebraic types.
    -- (See "Type#type_classification" for what an algebraic type is.)
    --
    -- This is qualified with \"like\" because of a particular special
    -- case: TYPE (the underlyind kind behind Type, among others). TYPE
    -- is conceptually a datatype (and thus algebraic), but in practice it is
    -- a primitive builtin type, so we must check for it specially.
    --
    -- NB: it makes sense to think of TYPE as a closed type in a value-level,
    -- pattern-matching context. However, at the kind level, TYPE is certainly
    -- not closed! Since this function is specifically tailored towards pattern
    -- matching, however, it's OK to label TYPE as closed.
    is_algebraic_like :: TyCon -> Bool
    is_algebraic_like :: TyCon -> Bool
is_algebraic_like tc :: TyCon
tc = TyCon -> Bool
isAlgTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tYPETyCon

pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
                         -> PmM (Maybe (Type, [DataCon], Type))
-- ^ Get rid of *outermost* (or toplevel)
--      * type function redex
--      * data family redex
--      * newtypes
--
-- Behaves exactly like `topNormaliseType_maybe`, but instead of returning a
-- coercion, it returns useful information for issuing pattern matching
-- warnings. See Note [Type normalisation for EmptyCase] for details.
--
-- 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_maybe :: FamInstEnvs
-> Bag TyVar -> Type -> PmM (Maybe (Type, [DataCon], Type))
pmTopNormaliseType_maybe env :: FamInstEnvs
env ty_cs :: Bag TyVar
ty_cs typ :: Type
typ
  = do (_, mb_typ' :: Maybe Type
mb_typ') <- DsM (Messages, Maybe Type) -> PmM (Messages, Maybe Type)
forall a. DsM a -> PmM a
liftD (DsM (Messages, Maybe Type) -> PmM (Messages, Maybe Type))
-> DsM (Messages, Maybe Type) -> PmM (Messages, Maybe Type)
forall a b. (a -> b) -> a -> b
$ TcM Type -> DsM (Messages, Maybe Type)
forall a. TcM a -> DsM (Messages, Maybe a)
initTcDsForSolver (TcM Type -> DsM (Messages, Maybe Type))
-> TcM Type -> DsM (Messages, Maybe Type)
forall a b. (a -> b) -> a -> b
$ Bag TyVar -> Type -> TcM Type
tcNormalise Bag TyVar
ty_cs Type
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 for EmptyCase].
       Maybe (Type, [DataCon], Type)
-> PmM (Maybe (Type, [DataCon], Type))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (Type, [DataCon], Type)
 -> PmM (Maybe (Type, [DataCon], Type)))
-> Maybe (Type, [DataCon], Type)
-> PmM (Maybe (Type, [DataCon], Type))
forall a b. (a -> b) -> a -> b
$ do Type
typ' <- Maybe Type
mb_typ'
                 ((ty_f :: [Type] -> [Type]
ty_f,tm_f :: [DataCon] -> [DataCon]
tm_f), ty :: Type
ty) <- NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
-> (([Type] -> [Type], [DataCon] -> [DataCon])
    -> ([Type] -> [Type], [DataCon] -> [DataCon])
    -> ([Type] -> [Type], [DataCon] -> [DataCon]))
-> Type
-> Maybe (([Type] -> [Type], [DataCon] -> [DataCon]), Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
stepper ([Type] -> [Type], [DataCon] -> [DataCon])
-> ([Type] -> [Type], [DataCon] -> [DataCon])
-> ([Type] -> [Type], [DataCon] -> [DataCon])
forall b c b c a a.
(b -> c, b -> c) -> (a -> b, a -> b) -> (a -> c, a -> c)
comb Type
typ'
                 -- We need to do topNormaliseTypeX in addition to tcNormalise,
                 -- since topNormaliseX looks through newtypes, which
                 -- tcNormalise does not do.
                 (Type, [DataCon], Type) -> Maybe (Type, [DataCon], Type)
forall a. a -> Maybe a
Just (Type -> [Type] -> Type
eq_src_ty Type
ty (Type
typ' Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type] -> [Type]
ty_f [Type
ty]), [DataCon] -> [DataCon]
tm_f [], Type
ty)
  where
    -- Find the first type in the sequence of rewrites that is a data type,
    -- newtype, or a data family application (not the representation tycon!).
    -- This is the one that is equal (in source Haskell) to the initial type.
    -- If none is found in the list, then all of them are type family
    -- applications, so we simply return the last one, which is the *simplest*.
    eq_src_ty :: Type -> [Type] -> Type
    eq_src_ty :: Type -> [Type] -> Type
eq_src_ty ty :: Type
ty tys :: [Type]
tys = Type -> (Type -> Type) -> Maybe Type -> Type
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type
ty Type -> Type
forall a. a -> a
id ((Type -> Bool) -> [Type] -> Maybe Type
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Type -> Bool
is_closed_or_data_family [Type]
tys)

    is_closed_or_data_family :: Type -> Bool
    is_closed_or_data_family :: Type -> Bool
is_closed_or_data_family ty :: 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 (tyf1 :: b -> c
tyf1, tmf1 :: b -> c
tmf1) (tyf2 :: a -> b
tyf2, tmf2 :: 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 :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
stepper = NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
newTypeStepper NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
-> NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
-> NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
forall ev.
NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
`composeSteppers` NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
tyFamStepper

    -- 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],[DataCon] -> [DataCon])
    newTypeStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
newTypeStepper rec_nts :: RecTcChecker
rec_nts tc :: TyCon
tc tys :: [Type]
tys
      | Just (ty' :: Type
ty', _co :: Coercion
_co) <- TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc [Type]
tys
      = case RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_nts TyCon
tc of
          Just rec_nts' :: RecTcChecker
rec_nts' -> let tyf :: [Type] -> [Type]
tyf = ((TyCon -> [Type] -> Type
TyConApp TyCon
tc [Type]
tys)Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:)
                               tmf :: [DataCon] -> [DataCon]
tmf = ((TyCon -> DataCon
tyConSingleDataCon TyCon
tc)DataCon -> [DataCon] -> [DataCon]
forall a. a -> [a] -> [a]
:)
                           in  RecTcChecker
-> Type
-> ([Type] -> [Type], [DataCon] -> [DataCon])
-> NormaliseStepResult ([Type] -> [Type], [DataCon] -> [DataCon])
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' ([Type] -> [Type]
tyf, [DataCon] -> [DataCon]
tmf)
          Nothing       -> NormaliseStepResult ([Type] -> [Type], [DataCon] -> [DataCon])
forall ev. NormaliseStepResult ev
NS_Abort
      | Bool
otherwise
      = NormaliseStepResult ([Type] -> [Type], [DataCon] -> [DataCon])
forall ev. NormaliseStepResult ev
NS_Done

    tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
    tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
tyFamStepper rec_nts :: RecTcChecker
rec_nts tc :: TyCon
tc tys :: [Type]
tys  -- Try to step a type/data family
      = let (_args_co :: Coercion
_args_co, ntys :: [Type]
ntys, _res_co :: Coercion
_res_co) = FamInstEnvs
-> Role -> TyCon -> [Type] -> (Coercion, [Type], Coercion)
normaliseTcArgs FamInstEnvs
env Role
Representational TyCon
tc [Type]
tys in
          -- NB: It's OK to use normaliseTcArgs here instead of
          -- normalise_tc_args (which takes the LiftingContext described
          -- in Note [Normalising types]) because the reduceTyFamApp below
          -- works only at top level. We'll never recur in this function
          -- after reducing the kind of a bound tyvar.

        case FamInstEnvs -> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
reduceTyFamApp_maybe FamInstEnvs
env Role
Representational TyCon
tc [Type]
ntys of
          Just (_co :: Coercion
_co, rhs :: Type
rhs) -> RecTcChecker
-> Type
-> ([Type] -> [Type], [DataCon] -> [DataCon])
-> NormaliseStepResult ([Type] -> [Type], [DataCon] -> [DataCon])
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
rhs ((Type
rhsType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:), [DataCon] -> [DataCon]
forall a. a -> a
id)
          _               -> NormaliseStepResult ([Type] -> [Type], [DataCon] -> [DataCon])
forall ev. NormaliseStepResult ev
NS_Done

-- | Determine suitable constraints to use at the beginning of pattern-match
-- coverage checking by consulting the sets of term and type constraints
-- currently in scope. If one of these sets of constraints is unsatisfiable,
-- use an empty set in its place. (See
-- @Note [Recovering from unsatisfiable pattern-matching constraints]@
-- for why this is done.)
pmInitialTmTyCs :: PmM Delta
pmInitialTmTyCs :: PmM Delta
pmInitialTmTyCs = do
  Bag TyVar
ty_cs  <- DsM (Bag TyVar) -> PmM (Bag TyVar)
forall a. DsM a -> PmM a
liftD DsM (Bag TyVar)
getDictsDs
  [ComplexEq]
tm_cs  <- (SimpleEq -> ComplexEq) -> [SimpleEq] -> [ComplexEq]
forall a b. (a -> b) -> [a] -> [b]
map SimpleEq -> ComplexEq
toComplex ([SimpleEq] -> [ComplexEq])
-> (Bag SimpleEq -> [SimpleEq]) -> Bag SimpleEq -> [ComplexEq]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bag SimpleEq -> [SimpleEq]
forall a. Bag a -> [a]
bagToList (Bag SimpleEq -> [ComplexEq])
-> ListT DsM (Bag SimpleEq) -> ListT DsM [ComplexEq]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DsM (Bag SimpleEq) -> ListT DsM (Bag SimpleEq)
forall a. DsM a -> PmM a
liftD DsM (Bag SimpleEq)
getTmCsDs
  Bool
sat_ty <- Bag TyVar -> PmM Bool
tyOracle Bag TyVar
ty_cs
  let initTyCs :: Bag TyVar
initTyCs = if Bool
sat_ty then Bag TyVar
ty_cs else Bag TyVar
forall a. Bag a
emptyBag
      initTmState :: TmState
initTmState = TmState -> Maybe TmState -> TmState
forall a. a -> Maybe a -> a
fromMaybe TmState
initialTmState (TmState -> [ComplexEq] -> Maybe TmState
tmOracle TmState
initialTmState [ComplexEq]
tm_cs)
  Delta -> PmM Delta
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Delta -> PmM Delta) -> Delta -> PmM Delta
forall a b. (a -> b) -> a -> b
$ MkDelta :: Bag TyVar -> TmState -> Delta
MkDelta{ delta_tm_cs :: TmState
delta_tm_cs = TmState
initTmState, delta_ty_cs :: Bag TyVar
delta_ty_cs = Bag TyVar
initTyCs }

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

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

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

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

-- | Given a conlike's term constraints, type constraints, and strict argument
-- types, check if they are satisfiable.
-- (In other words, this is the ⊢_Sat oracle judgment from the GADTs Meet
-- Their Match paper.)
--
-- For the purposes of efficiency, this takes as separate arguments the
-- ambient term and type constraints (which are known beforehand to be
-- satisfiable), as well as the new term and type constraints (which may not
-- be satisfiable). This lets us implement two mini-optimizations:
--
-- * If there are no new type constraints, then don't bother initializing
--   the type oracle, since it's redundant to do so.
-- * Since the new term constraint is a separate argument, we only need to
--   execute one iteration of the term oracle (instead of traversing the
--   entire set of term constraints).
--
-- Taking strict argument types into account is something which was not
-- discussed in GADTs Meet Their Match. For an explanation of what role they
-- serve, see @Note [Extensions to GADTs Meet Their Match]@.
pmIsSatisfiable
  :: Delta     -- ^ The ambient term and type constraints
               --   (known to be satisfiable).
  -> ComplexEq -- ^ The new term constraint.
  -> Bag EvVar -- ^ The new type constraints.
  -> [Type]    -- ^ The strict argument types.
  -> PmM (Maybe Delta)
               -- ^ @'Just' delta@ if the constraints (@delta@) are
               -- satisfiable, and each strict argument type is inhabitable.
               -- 'Nothing' otherwise.
pmIsSatisfiable :: Delta -> ComplexEq -> Bag TyVar -> [Type] -> PmM (Maybe Delta)
pmIsSatisfiable amb_cs :: Delta
amb_cs new_tm_c :: ComplexEq
new_tm_c new_ty_cs :: Bag TyVar
new_ty_cs strict_arg_tys :: [Type]
strict_arg_tys = do
  Maybe Delta
mb_sat <- Delta -> ComplexEq -> Bag TyVar -> PmM (Maybe Delta)
tmTyCsAreSatisfiable Delta
amb_cs ComplexEq
new_tm_c Bag TyVar
new_ty_cs
  case Maybe Delta
mb_sat of
    Nothing -> Maybe Delta -> PmM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Delta
forall a. Maybe a
Nothing
    Just delta :: Delta
delta -> do
      -- We know that the term and type constraints are inhabitable, so now
      -- check if each strict argument type is inhabitable.
      Bool
all_non_void <- RecTcChecker -> Delta -> [Type] -> PmM Bool
checkAllNonVoid RecTcChecker
initRecTc Delta
delta [Type]
strict_arg_tys
      Maybe Delta -> PmM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Delta -> PmM (Maybe Delta))
-> Maybe Delta -> PmM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ if Bool
all_non_void -- Check if each strict argument type
                             -- is inhabitable
                then Delta -> Maybe Delta
forall a. a -> Maybe a
Just Delta
delta
                else Maybe Delta
forall a. Maybe a
Nothing

-- | Like 'pmIsSatisfiable', but only checks if term and type constraints are
-- satisfiable, and doesn't bother checking anything related to strict argument
-- types.
tmTyCsAreSatisfiable
  :: Delta     -- ^ The ambient term and type constraints
               --   (known to be satisfiable).
  -> ComplexEq -- ^ The new term constraint.
  -> Bag EvVar -- ^ The new type constraints.
  -> PmM (Maybe Delta)
       -- ^ @'Just' delta@ if the constraints (@delta@) are
       -- satisfiable. 'Nothing' otherwise.
tmTyCsAreSatisfiable :: Delta -> ComplexEq -> Bag TyVar -> PmM (Maybe Delta)
tmTyCsAreSatisfiable
    (MkDelta{ delta_tm_cs :: Delta -> TmState
delta_tm_cs = TmState
amb_tm_cs, delta_ty_cs :: Delta -> Bag TyVar
delta_ty_cs = Bag TyVar
amb_ty_cs })
    new_tm_c :: ComplexEq
new_tm_c new_ty_cs :: Bag TyVar
new_ty_cs = do
  let ty_cs :: Bag TyVar
ty_cs = Bag TyVar
new_ty_cs Bag TyVar -> Bag TyVar -> Bag TyVar
forall a. Bag a -> Bag a -> Bag a
`unionBags` Bag TyVar
amb_ty_cs
  Bool
sat_ty <- if Bag TyVar -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag TyVar
new_ty_cs
               then Bool -> PmM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
               else Bag TyVar -> PmM Bool
tyOracle Bag TyVar
ty_cs
  Maybe Delta -> PmM (Maybe Delta)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Delta -> PmM (Maybe Delta))
-> Maybe Delta -> PmM (Maybe Delta)
forall a b. (a -> b) -> a -> b
$ case (Bool
sat_ty, TmState -> ComplexEq -> Maybe TmState
solveOneEq TmState
amb_tm_cs ComplexEq
new_tm_c) of
           (True, Just term_cs :: TmState
term_cs) -> Delta -> Maybe Delta
forall a. a -> Maybe a
Just (Delta -> Maybe Delta) -> Delta -> Maybe Delta
forall a b. (a -> b) -> a -> b
$ MkDelta :: Bag TyVar -> TmState -> Delta
MkDelta{ delta_ty_cs :: Bag TyVar
delta_ty_cs = Bag TyVar
ty_cs
                                                 , delta_tm_cs :: TmState
delta_tm_cs = TmState
term_cs }
           _unsat :: (Bool, Maybe TmState)
_unsat               -> Maybe Delta
forall a. Maybe a
Nothing

-- | Implements two performance optimizations, as described in the
-- \"Strict argument type constraints\" section of
-- @Note [Extensions to GADTs Meet Their Match]@.
checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> PmM Bool
checkAllNonVoid rec_ts :: RecTcChecker
rec_ts amb_cs :: Delta
amb_cs strict_arg_tys :: [Type]
strict_arg_tys = do
  FamInstEnvs
fam_insts <- DsM FamInstEnvs -> PmM FamInstEnvs
forall a. DsM a -> PmM a
liftD DsM FamInstEnvs
dsGetFamInstEnvs
  let definitely_inhabited :: Type -> PmM Bool
definitely_inhabited =
        FamInstEnvs -> Bag TyVar -> Type -> PmM Bool
definitelyInhabitedType FamInstEnvs
fam_insts (Delta -> Bag TyVar
delta_ty_cs Delta
amb_cs)
  [Type]
tys_to_check <- (Type -> PmM Bool) -> [Type] -> ListT DsM [Type]
forall (m :: * -> *) a.
Applicative m =>
(a -> m Bool) -> [a] -> m [a]
filterOutM Type -> PmM Bool
definitely_inhabited [Type]
strict_arg_tys
  let rec_max_bound :: Int
rec_max_bound | [Type]
tys_to_check [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` 1
                    = 1
                    | Bool
otherwise
                    = Int
defaultRecTcMaxBound
      rec_ts' :: RecTcChecker
rec_ts' = Int -> RecTcChecker -> RecTcChecker
setRecTcMaxBound Int
rec_max_bound RecTcChecker
rec_ts
  (Type -> PmM Bool) -> [Type] -> PmM Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
allM (RecTcChecker -> Delta -> Type -> PmM Bool
nonVoid RecTcChecker
rec_ts' Delta
amb_cs) [Type]
tys_to_check

-- | Checks if a strict argument type of a conlike is inhabitable by a
-- terminating value (i.e, an 'InhabitationCandidate').
-- See @Note [Extensions to GADTs Meet Their Match]@.
nonVoid
  :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit.
  -> Delta        -- ^ The ambient term/type constraints (known to be
                  --   satisfiable).
  -> Type         -- ^ The strict argument type.
  -> PmM Bool     -- ^ 'True' if the strict argument type might be inhabited by
                  --   a terminating value (i.e., an 'InhabitationCandidate').
                  --   'False' if it is definitely uninhabitable by anything
                  --   (except bottom).
nonVoid :: RecTcChecker -> Delta -> Type -> PmM Bool
nonVoid rec_ts :: RecTcChecker
rec_ts amb_cs :: Delta
amb_cs strict_arg_ty :: Type
strict_arg_ty = do
  Either Type (TyCon, [InhabitationCandidate])
mb_cands <- Bag TyVar
-> Type -> PmM (Either Type (TyCon, [InhabitationCandidate]))
inhabitationCandidates (Delta -> Bag TyVar
delta_ty_cs Delta
amb_cs) Type
strict_arg_ty
  case Either Type (TyCon, [InhabitationCandidate])
mb_cands of
    Right (tc :: TyCon
tc, cands :: [InhabitationCandidate]
cands)
      |  Just rec_ts' :: RecTcChecker
rec_ts' <- RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_ts TyCon
tc
      -> (InhabitationCandidate -> PmM Bool)
-> [InhabitationCandidate] -> PmM Bool
forall (m :: * -> *) a. Monad m => (a -> m Bool) -> [a] -> m Bool
anyM (RecTcChecker -> Delta -> InhabitationCandidate -> PmM Bool
cand_is_inhabitable RecTcChecker
rec_ts' Delta
amb_cs) [InhabitationCandidate]
cands
           -- A strict argument type is inhabitable by a terminating value if
           -- at least one InhabitationCandidate is inhabitable.
    _ -> Bool -> PmM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
           -- Either the type is trivially inhabited or we have exceeded the
           -- recursion depth for some TyCon (so bail out and conservatively
           -- claim the type is inhabited).
  where
    -- Checks if an InhabitationCandidate for a strict argument type:
    --
    -- (1) Has satisfiable term and type constraints.
    -- (2) Has 'nonVoid' strict argument types (we bail out of this
    --     check if recursion is detected).
    --
    -- See Note [Extensions to GADTs Meet Their Match]
    cand_is_inhabitable :: RecTcChecker -> Delta
                        -> InhabitationCandidate -> PmM Bool
    cand_is_inhabitable :: RecTcChecker -> Delta -> InhabitationCandidate -> PmM Bool
cand_is_inhabitable rec_ts :: RecTcChecker
rec_ts amb_cs :: Delta
amb_cs
      (InhabitationCandidate{ ic_tm_ct :: InhabitationCandidate -> ComplexEq
ic_tm_ct          = ComplexEq
new_term_c
                            , ic_ty_cs :: InhabitationCandidate -> Bag TyVar
ic_ty_cs          = Bag TyVar
new_ty_cs
                            , ic_strict_arg_tys :: InhabitationCandidate -> [Type]
ic_strict_arg_tys = [Type]
new_strict_arg_tys }) = do
        Maybe Delta
mb_sat <- Delta -> ComplexEq -> Bag TyVar -> PmM (Maybe Delta)
tmTyCsAreSatisfiable Delta
amb_cs ComplexEq
new_term_c Bag TyVar
new_ty_cs
        case Maybe Delta
mb_sat of
          Nothing -> Bool -> PmM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
          Just new_delta :: Delta
new_delta -> do
            RecTcChecker -> Delta -> [Type] -> PmM Bool
checkAllNonVoid RecTcChecker
rec_ts Delta
new_delta [Type]
new_strict_arg_tys

-- | @'definitelyInhabitedType' ty@ returns 'True' if @ty@ has at least one
-- constructor @C@ such that:
--
-- 1. @C@ has no equality constraints.
-- 2. @C@ has no strict argument types.
--
-- See the \"Strict argument type constraints\" section of
-- @Note [Extensions to GADTs Meet Their Match]@.
definitelyInhabitedType :: FamInstEnvs -> Bag EvVar -> Type -> PmM Bool
definitelyInhabitedType :: FamInstEnvs -> Bag TyVar -> Type -> PmM Bool
definitelyInhabitedType env :: FamInstEnvs
env ty_cs :: Bag TyVar
ty_cs ty :: Type
ty = do
  Maybe (Type, [DataCon], Type)
mb_res <- FamInstEnvs
-> Bag TyVar -> Type -> PmM (Maybe (Type, [DataCon], Type))
pmTopNormaliseType_maybe FamInstEnvs
env Bag TyVar
ty_cs Type
ty
  Bool -> PmM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> PmM Bool) -> Bool -> PmM Bool
forall a b. (a -> b) -> a -> b
$ case Maybe (Type, [DataCon], Type)
mb_res of
           Just (_, cons :: [DataCon]
cons, _) -> (DataCon -> Bool) -> [DataCon] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any DataCon -> Bool
meets_criteria [DataCon]
cons
           Nothing           -> Bool
False
  where
    meets_criteria :: DataCon -> Bool
    meets_criteria :: DataCon -> Bool
meets_criteria con :: DataCon
con =
      [EqSpec] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [EqSpec]
dataConEqSpec DataCon
con) Bool -> Bool -> Bool
&& -- (1)
      [HsImplBang] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (DataCon -> [HsImplBang]
dataConImplBangs DataCon
con) -- (2)

{- Note [Type normalisation for EmptyCase]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
EmptyCase is an exception for pattern matching, since it is strict. This means
that it boils down to checking whether the type of the scrutinee is inhabited.
Function pmTopNormaliseType_maybe 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_maybe 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 data constructors "skipped", every time we normalise a
      newtype to its core representation, we keep track of the source data
      constructor.
  (c) core_ty is the rewritten type. That is,
        pmTopNormaliseType_maybe 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_maybe env ty_cs (F Int) results in

  Just (G2, [MkG2,MkG1], 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_maybe, using the constraint solver to solve for any local
equalities (such as i ~ Int) that may be in scope.
-}

-- | Generate all 'InhabitationCandidate's for a given type. The result is
-- either @'Left' ty@, if the type cannot be reduced to a closed algebraic type
-- (or if it's one trivially inhabited, like 'Int'), or @'Right' candidates@,
-- if it can. In this case, the candidates are the signature of the tycon, each
-- one accompanied by the term- and type- constraints it gives rise to.
-- See also Note [Checking EmptyCase Expressions]
inhabitationCandidates :: Bag EvVar -> Type
                       -> PmM (Either Type (TyCon, [InhabitationCandidate]))
inhabitationCandidates :: Bag TyVar
-> Type -> PmM (Either Type (TyCon, [InhabitationCandidate]))
inhabitationCandidates ty_cs :: Bag TyVar
ty_cs ty :: Type
ty = do
  FamInstEnvs
fam_insts   <- DsM FamInstEnvs -> PmM FamInstEnvs
forall a. DsM a -> PmM a
liftD DsM FamInstEnvs
dsGetFamInstEnvs
  Maybe (Type, [DataCon], Type)
mb_norm_res <- FamInstEnvs
-> Bag TyVar -> Type -> PmM (Maybe (Type, [DataCon], Type))
pmTopNormaliseType_maybe FamInstEnvs
fam_insts Bag TyVar
ty_cs Type
ty
  case Maybe (Type, [DataCon], Type)
mb_norm_res of
    Just (src_ty :: Type
src_ty, dcs :: [DataCon]
dcs, core_ty :: Type
core_ty) -> Type
-> Type
-> [DataCon]
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
alts_to_check Type
src_ty Type
core_ty [DataCon]
dcs
    Nothing                     -> Type
-> Type
-> [DataCon]
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
alts_to_check Type
ty     Type
ty      []
  where
    -- All these types are trivially inhabited
    trivially_inhabited :: [TyCon]
trivially_inhabited = [ TyCon
charTyCon, TyCon
doubleTyCon, TyCon
floatTyCon
                          , TyCon
intTyCon, TyCon
wordTyCon, TyCon
word8TyCon ]

    -- Note: At the moment we leave all the typing and constraint fields of
    -- PmCon empty, since we know that they are not gonna be used. Is the
    -- right-thing-to-do to actually create them, even if they are never used?
    build_tm :: ValAbs -> [DataCon] -> ValAbs
    build_tm :: PmPat 'VA -> [DataCon] -> PmPat 'VA
build_tm = (DataCon -> PmPat 'VA -> PmPat 'VA)
-> PmPat 'VA -> [DataCon] -> PmPat 'VA
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\dc :: DataCon
dc e :: PmPat 'VA
e -> ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat 'VA] -> PmPat 'VA
forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon (DataCon -> ConLike
RealDataCon DataCon
dc) [] [] [] [PmPat 'VA
e])

    -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
    alts_to_check :: Type -> Type -> [DataCon]
                  -> PmM (Either Type (TyCon, [InhabitationCandidate]))
    alts_to_check :: Type
-> Type
-> [DataCon]
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
alts_to_check src_ty :: Type
src_ty core_ty :: Type
core_ty dcs :: [DataCon]
dcs = case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
core_ty of
      Just (tc :: TyCon
tc, _)
        |  TyCon
tc TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TyCon]
trivially_inhabited
        -> case [DataCon]
dcs of
             []    -> Either Type (TyCon, [InhabitationCandidate])
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either Type (TyCon, [InhabitationCandidate])
forall a b. a -> Either a b
Left Type
src_ty)
             (_:_) -> do TyVar
var <- DsM TyVar -> PmM TyVar
forall a. DsM a -> PmM a
liftD (DsM TyVar -> PmM TyVar) -> DsM TyVar -> PmM TyVar
forall a b. (a -> b) -> a -> b
$ Type -> DsM TyVar
mkPmId Type
core_ty
                         let va :: PmPat 'VA
va = PmPat 'VA -> [DataCon] -> PmPat 'VA
build_tm (TyVar -> PmPat 'VA
forall (t :: PatTy). TyVar -> PmPat t
PmVar TyVar
var) [DataCon]
dcs
                         Either Type (TyCon, [InhabitationCandidate])
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Type (TyCon, [InhabitationCandidate])
 -> PmM (Either Type (TyCon, [InhabitationCandidate])))
-> Either Type (TyCon, [InhabitationCandidate])
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
forall a b. (a -> b) -> a -> b
$ (TyCon, [InhabitationCandidate])
-> Either Type (TyCon, [InhabitationCandidate])
forall a b. b -> Either a b
Right (TyCon
tc, [InhabitationCandidate :: PmPat 'VA
-> ComplexEq -> Bag TyVar -> [Type] -> InhabitationCandidate
InhabitationCandidate
                           { ic_val_abs :: PmPat 'VA
ic_val_abs = PmPat 'VA
va, ic_tm_ct :: ComplexEq
ic_tm_ct = TyVar -> ComplexEq
mkIdEq TyVar
var
                           , ic_ty_cs :: Bag TyVar
ic_ty_cs = Bag TyVar
forall a. Bag a
emptyBag, ic_strict_arg_tys :: [Type]
ic_strict_arg_tys = [] }])

        |  Type -> Bool
pmIsClosedType Type
core_ty Bool -> Bool -> Bool
&& Bool -> Bool
not (TyCon -> Bool
isAbstractTyCon TyCon
tc)
           -- Don't consider abstract tycons since we don't know what their
           -- constructors are, which makes the results of coverage checking
           -- them extremely misleading.
        -> DsM (Either Type (TyCon, [InhabitationCandidate]))
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
forall a. DsM a -> PmM a
liftD (DsM (Either Type (TyCon, [InhabitationCandidate]))
 -> PmM (Either Type (TyCon, [InhabitationCandidate])))
-> DsM (Either Type (TyCon, [InhabitationCandidate]))
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
forall a b. (a -> b) -> a -> b
$ do
             TyVar
var  <- Type -> DsM TyVar
mkPmId Type
core_ty -- it would be wrong to unify x
             [InhabitationCandidate]
alts <- (DataCon -> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate)
-> [DataCon]
-> IOEnv (Env DsGblEnv DsLclEnv) [InhabitationCandidate]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (TyVar
-> ConLike -> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
mkOneConFull TyVar
var (ConLike -> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate)
-> (DataCon -> ConLike)
-> DataCon
-> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataCon -> ConLike
RealDataCon) (TyCon -> [DataCon]
tyConDataCons TyCon
tc)
             Either Type (TyCon, [InhabitationCandidate])
-> DsM (Either Type (TyCon, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either Type (TyCon, [InhabitationCandidate])
 -> DsM (Either Type (TyCon, [InhabitationCandidate])))
-> Either Type (TyCon, [InhabitationCandidate])
-> DsM (Either Type (TyCon, [InhabitationCandidate]))
forall a b. (a -> b) -> a -> b
$ (TyCon, [InhabitationCandidate])
-> Either Type (TyCon, [InhabitationCandidate])
forall a b. b -> Either a b
Right
               (TyCon
tc, [ InhabitationCandidate
alt{ic_val_abs :: PmPat 'VA
ic_val_abs = PmPat 'VA -> [DataCon] -> PmPat 'VA
build_tm (InhabitationCandidate -> PmPat 'VA
ic_val_abs InhabitationCandidate
alt) [DataCon]
dcs}
                    | InhabitationCandidate
alt <- [InhabitationCandidate]
alts ])
      -- For other types conservatively assume that they are inhabited.
      _other :: Maybe (TyCon, [Type])
_other -> Either Type (TyCon, [InhabitationCandidate])
-> PmM (Either Type (TyCon, [InhabitationCandidate]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> Either Type (TyCon, [InhabitationCandidate])
forall a b. a -> Either a b
Left Type
src_ty)

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

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

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

   For an example see also Note [Type normalisation for EmptyCase]
   in types/FamInstEnv.hs.

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

%************************************************************************
%*                                                                      *
              Transform source syntax to *our* syntax
%*                                                                      *
%************************************************************************
-}

-- -----------------------------------------------------------------------
-- * Utilities

nullaryConPattern :: ConLike -> Pattern
-- Nullary data constructor and nullary type constructor
nullaryConPattern :: ConLike -> PmPat 'PAT
nullaryConPattern con :: ConLike
con =
  PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con = ConLike
con, pm_con_arg_tys :: [Type]
pm_con_arg_tys = []
        , pm_con_tvs :: [TyVar]
pm_con_tvs = [], pm_con_dicts :: [TyVar]
pm_con_dicts = [], pm_con_args :: PatVec
pm_con_args = [] }
{-# INLINE nullaryConPattern #-}

truePattern :: Pattern
truePattern :: PmPat 'PAT
truePattern = ConLike -> PmPat 'PAT
nullaryConPattern (DataCon -> ConLike
RealDataCon DataCon
trueDataCon)
{-# INLINE truePattern #-}

-- | A fake guard pattern (True <- _) used to represent cases we cannot handle
fake_pat :: Pattern
fake_pat :: PmPat 'PAT
fake_pat = $WPmGrd :: PatVec -> PmExpr -> PmPat 'PAT
PmGrd { pm_grd_pv :: PatVec
pm_grd_pv   = [PmPat 'PAT
truePattern]
                 , pm_grd_expr :: PmExpr
pm_grd_expr = HsExpr GhcTc -> PmExpr
PmExprOther (XEWildPat GhcTc -> HsExpr GhcTc
forall p. XEWildPat p -> HsExpr p
EWildPat XEWildPat GhcTc
NoExt
noExt) }
{-# INLINE fake_pat #-}

-- | Check whether a guard pattern is generated by the checker (unhandled)
isFakeGuard :: [Pattern] -> PmExpr -> Bool
isFakeGuard :: PatVec -> PmExpr -> Bool
isFakeGuard [PmCon { pm_con_con :: forall (t :: PatTy). PmPat t -> ConLike
pm_con_con = RealDataCon c :: DataCon
c }] (PmExprOther (EWildPat _))
  | DataCon
c DataCon -> DataCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon
trueDataCon = Bool
True
  | Bool
otherwise        = Bool
False
isFakeGuard _pats :: PatVec
_pats _e :: PmExpr
_e = Bool
False

-- | Generate a `canFail` pattern vector of a specific type
mkCanFailPmPat :: Type -> DsM PatVec
mkCanFailPmPat :: Type -> DsM PatVec
mkCanFailPmPat ty :: Type
ty = do
  PmPat 'PAT
var <- Type -> DsM (PmPat 'PAT)
forall (p :: PatTy). Type -> DsM (PmPat p)
mkPmVar Type
ty
  PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [PmPat 'PAT
var, PmPat 'PAT
fake_pat]

vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
-- ADT constructor pattern => no existentials, no local constraints
vanillaConPattern :: ConLike -> [Type] -> PatVec -> PmPat 'PAT
vanillaConPattern con :: ConLike
con arg_tys :: [Type]
arg_tys args :: PatVec
args =
  PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con = ConLike
con, pm_con_arg_tys :: [Type]
pm_con_arg_tys = [Type]
arg_tys
        , pm_con_tvs :: [TyVar]
pm_con_tvs = [], pm_con_dicts :: [TyVar]
pm_con_dicts = [], pm_con_args :: PatVec
pm_con_args = PatVec
args }
{-# INLINE vanillaConPattern #-}

-- | Create an empty list pattern of a given type
nilPattern :: Type -> Pattern
nilPattern :: Type -> PmPat 'PAT
nilPattern ty :: Type
ty =
  PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con = DataCon -> ConLike
RealDataCon DataCon
nilDataCon, pm_con_arg_tys :: [Type]
pm_con_arg_tys = [Type
ty]
        , pm_con_tvs :: [TyVar]
pm_con_tvs = [], pm_con_dicts :: [TyVar]
pm_con_dicts = []
        , pm_con_args :: PatVec
pm_con_args = [] }
{-# INLINE nilPattern #-}

mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
mkListPatVec ty :: Type
ty xs :: PatVec
xs ys :: PatVec
ys = [PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con = DataCon -> ConLike
RealDataCon DataCon
consDataCon
                               , pm_con_arg_tys :: [Type]
pm_con_arg_tys = [Type
ty]
                               , pm_con_tvs :: [TyVar]
pm_con_tvs = [], pm_con_dicts :: [TyVar]
pm_con_dicts = []
                               , pm_con_args :: PatVec
pm_con_args = PatVec
xsPatVec -> PatVec -> PatVec
forall a. [a] -> [a] -> [a]
++PatVec
ys }]
{-# INLINE mkListPatVec #-}

-- | Create a (non-overloaded) literal pattern
mkLitPattern :: HsLit GhcTc -> Pattern
mkLitPattern :: HsLit GhcTc -> PmPat 'PAT
mkLitPattern lit :: HsLit GhcTc
lit = PmLit :: forall (t :: PatTy). PmLit -> PmPat t
PmLit { pm_lit_lit :: PmLit
pm_lit_lit = HsLit GhcTc -> PmLit
PmSLit HsLit GhcTc
lit }
{-# INLINE mkLitPattern #-}

-- -----------------------------------------------------------------------
-- * Transform (Pat Id) into of (PmPat Id)

translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
translatePat :: FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat fam_insts :: FamInstEnvs
fam_insts pat :: LPat GhcTc
pat = case LPat GhcTc
pat of
  WildPat  ty :: XWildPat GhcTc
ty  -> [Type] -> DsM PatVec
mkPmVars [Type
XWildPat GhcTc
ty]
  VarPat _ id :: Located (IdP GhcTc)
id  -> PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [TyVar -> PmPat 'PAT
forall (t :: PatTy). TyVar -> PmPat t
PmVar (Located TyVar -> SrcSpanLess (Located TyVar)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Located TyVar
Located (IdP GhcTc)
id)]
  ParPat _ p :: LPat GhcTc
p   -> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts (LPat GhcTc -> SrcSpanLess (LPat GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LPat GhcTc
p)
  LazyPat _ _  -> [Type] -> DsM PatVec
mkPmVars [LPat GhcTc -> Type
hsPatType LPat GhcTc
pat] -- like a variable

  -- ignore strictness annotations for now
  BangPat _ p :: LPat GhcTc
p  -> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts (LPat GhcTc -> SrcSpanLess (LPat GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LPat GhcTc
p)

  AsPat _ lid :: Located (IdP GhcTc)
lid p :: LPat GhcTc
p -> do
     -- Note [Translating As Patterns]
    PatVec
ps <- FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts (LPat GhcTc -> SrcSpanLess (LPat GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LPat GhcTc
p)
    let [e :: PmExpr
e] = (PmPat 'VA -> PmExpr) -> [PmPat 'VA] -> [PmExpr]
forall a b. (a -> b) -> [a] -> [b]
map PmPat 'VA -> PmExpr
vaToPmExpr (PatVec -> [PmPat 'VA]
coercePatVec PatVec
ps)
        g :: PmPat 'PAT
g   = PatVec -> PmExpr -> PmPat 'PAT
PmGrd [TyVar -> PmPat 'PAT
forall (t :: PatTy). TyVar -> PmPat t
PmVar (Located TyVar -> SrcSpanLess (Located TyVar)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc Located TyVar
Located (IdP GhcTc)
lid)] PmExpr
e
    PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return (PatVec
ps PatVec -> PatVec -> PatVec
forall a. [a] -> [a] -> [a]
++ [PmPat 'PAT
g])

  SigPat _ p :: LPat GhcTc
p _ty :: LHsSigWcType (NoGhcTc GhcTc)
_ty -> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts (LPat GhcTc -> SrcSpanLess (LPat GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LPat GhcTc
p)

  -- See Note [Translate CoPats]
  CoPat _ wrapper :: HsWrapper
wrapper p :: LPat GhcTc
p ty :: Type
ty
    | HsWrapper -> Bool
isIdHsWrapper HsWrapper
wrapper                   -> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts LPat GhcTc
p
    | WpCast co :: Coercion
co <-  HsWrapper
wrapper, Coercion -> Bool
isReflexiveCo Coercion
co -> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts LPat GhcTc
p
    | Bool
otherwise -> do
        PatVec
ps      <- FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts LPat GhcTc
p
        (xp :: PmPat 'PAT
xp,xe :: LHsExpr GhcTc
xe) <- Type -> DsM (PmPat 'PAT, LHsExpr GhcTc)
mkPmId2Forms Type
ty
        let g :: PmPat 'PAT
g = PatVec -> HsExpr GhcTc -> PmPat 'PAT
mkGuard PatVec
ps (HsWrapper -> HsExpr GhcTc -> HsExpr GhcTc
forall (id :: Pass).
HsWrapper -> HsExpr (GhcPass id) -> HsExpr (GhcPass id)
mkHsWrap HsWrapper
wrapper (LHsExpr GhcTc -> SrcSpanLess (LHsExpr GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcTc
xe))
        PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [PmPat 'PAT
xp,PmPat 'PAT
g]

  -- (n + k)  ===>   x (True <- x >= k) (n <- x-k)
  NPlusKPat ty :: XNPlusKPat GhcTc
ty (Located (IdP GhcTc) -> Located (SrcSpanLess (Located TyVar))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ _n :: SrcSpanLess (Located TyVar)
_n) _k1 :: Located (HsOverLit GhcTc)
_k1 _k2 :: HsOverLit GhcTc
_k2 _ge :: SyntaxExpr GhcTc
_ge _minus :: SyntaxExpr GhcTc
_minus -> Type -> DsM PatVec
mkCanFailPmPat Type
XNPlusKPat GhcTc
ty

  -- (fun -> pat)   ===>   x (pat <- fun x)
  ViewPat arg_ty :: XViewPat GhcTc
arg_ty lexpr :: LHsExpr GhcTc
lexpr lpat :: LPat GhcTc
lpat -> do
    PatVec
ps <- FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts (LPat GhcTc -> SrcSpanLess (LPat GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LPat GhcTc
lpat)
    -- See Note [Guards and Approximation]
    case (PmPat 'PAT -> Bool) -> PatVec -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PmPat 'PAT -> Bool
cantFailPattern PatVec
ps of
      True  -> do
        (xp :: PmPat 'PAT
xp,xe :: LHsExpr GhcTc
xe) <- Type -> DsM (PmPat 'PAT, LHsExpr GhcTc)
mkPmId2Forms Type
XViewPat GhcTc
arg_ty
        let g :: PmPat 'PAT
g = PatVec -> HsExpr GhcTc -> PmPat 'PAT
mkGuard PatVec
ps (XApp GhcTc -> LHsExpr GhcTc -> LHsExpr GhcTc -> HsExpr GhcTc
forall p. XApp p -> LHsExpr p -> LHsExpr p -> HsExpr p
HsApp XApp GhcTc
NoExt
noExt LHsExpr GhcTc
lexpr LHsExpr GhcTc
xe)
        PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [PmPat 'PAT
xp,PmPat 'PAT
g]
      False -> Type -> DsM PatVec
mkCanFailPmPat Type
XViewPat GhcTc
arg_ty

  -- list
  ListPat (ListPatTc ty Nothing) ps :: [LPat GhcTc]
ps -> do
    (PatVec -> PatVec -> PatVec) -> PatVec -> [PatVec] -> PatVec
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> PatVec -> PatVec -> PatVec
mkListPatVec Type
ty) [Type -> PmPat 'PAT
nilPattern Type
ty]
      ([PatVec] -> PatVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [PatVec] -> DsM PatVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec FamInstEnvs
fam_insts ((LPat GhcTc -> LPat GhcTc) -> [LPat GhcTc] -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map LPat GhcTc -> LPat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LPat GhcTc]
ps)

  -- overloaded list
  ListPat (ListPatTc _elem_ty (Just (pat_ty, _to_list))) lpats :: [LPat GhcTc]
lpats -> do
    DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
    if Extension -> DynFlags -> Bool
xopt Extension
LangExt.RebindableSyntax DynFlags
dflags
       then Type -> DsM PatVec
mkCanFailPmPat Type
pat_ty
       else case Type -> Maybe Type
splitListTyConApp_maybe Type
pat_ty of
              Just e_ty :: Type
e_ty -> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts
                                        (XListPat GhcTc -> [LPat GhcTc] -> LPat GhcTc
forall p. XListPat p -> [LPat p] -> LPat p
ListPat (Type -> Maybe (Type, SyntaxExpr GhcTc) -> ListPatTc
ListPatTc Type
e_ty Maybe (Type, SyntaxExpr GhcTc)
forall a. Maybe a
Nothing) [LPat GhcTc]
lpats)
              Nothing   -> Type -> DsM PatVec
mkCanFailPmPat Type
pat_ty
    -- (a) In the presence of RebindableSyntax, we don't know anything about
    --     `toList`, we should treat `ListPat` as any other view pattern.
    --
    -- (b) In the absence of RebindableSyntax,
    --     - If the pat_ty is `[a]`, then we treat the overloaded list pattern
    --       as ordinary list pattern. Although we can give an instance
    --       `IsList [Int]` (more specific than the default `IsList [a]`), in
    --       practice, we almost never do that. We assume the `_to_list` is
    --       the `toList` from `instance IsList [a]`.
    --
    --     - Otherwise, we treat the `ListPat` as ordinary view pattern.
    --
    -- See Trac #14547, especially comment#9 and comment#10.
    --
    -- Here we construct CanFailPmPat directly, rather can construct a view
    -- pattern and do further translation as an optimization, for the reason,
    -- see Note [Guards and Approximation].

  ConPatOut { pat_con :: forall p. LPat p -> Located ConLike
pat_con     = (Located ConLike -> Located (SrcSpanLess (Located ConLike))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ con :: SrcSpanLess (Located ConLike)
con)
            , pat_arg_tys :: forall p. LPat p -> [Type]
pat_arg_tys = [Type]
arg_tys
            , pat_tvs :: forall p. LPat p -> [TyVar]
pat_tvs     = [TyVar]
ex_tvs
            , pat_dicts :: forall p. LPat p -> [TyVar]
pat_dicts   = [TyVar]
dicts
            , pat_args :: forall p. LPat p -> HsConPatDetails p
pat_args    = HsConPatDetails GhcTc
ps } -> do
    [(Provenance, [ConLike])]
groups <- ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
allCompleteMatches SrcSpanLess (Located ConLike)
ConLike
con [Type]
arg_tys
    case [(Provenance, [ConLike])]
groups of
      [] -> Type -> DsM PatVec
mkCanFailPmPat (ConLike -> [Type] -> Type
conLikeResTy SrcSpanLess (Located ConLike)
ConLike
con [Type]
arg_tys)
      _  -> do
        PatVec
args <- FamInstEnvs
-> [Type]
-> [TyVar]
-> ConLike
-> HsConPatDetails GhcTc
-> DsM PatVec
translateConPatVec FamInstEnvs
fam_insts [Type]
arg_tys [TyVar]
ex_tvs SrcSpanLess (Located ConLike)
ConLike
con HsConPatDetails GhcTc
ps
        PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con     = SrcSpanLess (Located ConLike)
ConLike
con
                      , pm_con_arg_tys :: [Type]
pm_con_arg_tys = [Type]
arg_tys
                      , pm_con_tvs :: [TyVar]
pm_con_tvs     = [TyVar]
ex_tvs
                      , pm_con_dicts :: [TyVar]
pm_con_dicts   = [TyVar]
dicts
                      , pm_con_args :: PatVec
pm_con_args    = PatVec
args }]

  -- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
  NPat _ (Located (HsOverLit GhcTc)
-> Located (SrcSpanLess (Located (HsOverLit GhcTc)))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ olit :: SrcSpanLess (Located (HsOverLit GhcTc))
olit) mb_neg :: Maybe (SyntaxExpr GhcTc)
mb_neg _
    | OverLit (OverLitTc False ty) (HsIsString src s) _ <- SrcSpanLess (Located (HsOverLit GhcTc))
olit
    , Type -> Bool
isStringTy Type
ty ->
        (PatVec -> PatVec -> PatVec) -> PatVec -> [PatVec] -> PatVec
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> PatVec -> PatVec -> PatVec
mkListPatVec Type
charTy) [Type -> PmPat 'PAT
nilPattern Type
charTy] ([PatVec] -> PatVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [PatVec] -> DsM PatVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec FamInstEnvs
fam_insts
            ((Char -> LPat GhcTc) -> String -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map (XLitPat GhcTc -> HsLit GhcTc -> LPat GhcTc
forall p. XLitPat p -> HsLit p -> LPat p
LitPat XLitPat GhcTc
NoExt
noExt (HsLit GhcTc -> LPat GhcTc)
-> (Char -> HsLit GhcTc) -> Char -> LPat GhcTc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XHsChar GhcTc -> Char -> HsLit GhcTc
forall x. XHsChar x -> Char -> HsLit x
HsChar SourceText
XHsChar GhcTc
src) (FastString -> String
unpackFS FastString
s))
    | Bool
otherwise -> PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [PmLit :: forall (t :: PatTy). PmLit -> PmPat t
PmLit { pm_lit_lit :: PmLit
pm_lit_lit = Bool -> HsOverLit GhcTc -> PmLit
PmOLit (Maybe (SyntaxExpr GhcTc) -> Bool
forall a. Maybe a -> Bool
isJust Maybe (SyntaxExpr GhcTc)
mb_neg) SrcSpanLess (Located (HsOverLit GhcTc))
HsOverLit GhcTc
olit }]

  -- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
  LitPat _ lit :: HsLit GhcTc
lit
    | HsString src :: XHsString GhcTc
src s :: FastString
s <- HsLit GhcTc
lit ->
        (PatVec -> PatVec -> PatVec) -> PatVec -> [PatVec] -> PatVec
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Type -> PatVec -> PatVec -> PatVec
mkListPatVec Type
charTy) [Type -> PmPat 'PAT
nilPattern Type
charTy] ([PatVec] -> PatVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [PatVec] -> DsM PatVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec FamInstEnvs
fam_insts
            ((Char -> LPat GhcTc) -> String -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map (XLitPat GhcTc -> HsLit GhcTc -> LPat GhcTc
forall p. XLitPat p -> HsLit p -> LPat p
LitPat XLitPat GhcTc
NoExt
noExt (HsLit GhcTc -> LPat GhcTc)
-> (Char -> HsLit GhcTc) -> Char -> LPat GhcTc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. XHsChar GhcTc -> Char -> HsLit GhcTc
forall x. XHsChar x -> Char -> HsLit x
HsChar XHsString GhcTc
XHsChar GhcTc
src) (FastString -> String
unpackFS FastString
s))
    | Bool
otherwise -> PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [HsLit GhcTc -> PmPat 'PAT
mkLitPattern HsLit GhcTc
lit]

  TuplePat tys :: XTuplePat GhcTc
tys ps :: [LPat GhcTc]
ps boxity :: Boxity
boxity -> do
    [PatVec]
tidy_ps <- FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec FamInstEnvs
fam_insts ((LPat GhcTc -> LPat GhcTc) -> [LPat GhcTc] -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map LPat GhcTc -> LPat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LPat GhcTc]
ps)
    let tuple_con :: ConLike
tuple_con = DataCon -> ConLike
RealDataCon (Boxity -> Int -> DataCon
tupleDataCon Boxity
boxity ([LPat GhcTc] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LPat GhcTc]
ps))
        tys' :: [Type]
tys' = case Boxity
boxity of
                 Boxed -> [Type]
XTuplePat GhcTc
tys
                 -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
                 Unboxed -> (Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => Type -> Type
Type -> Type
getRuntimeRep [Type]
XTuplePat GhcTc
tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
XTuplePat GhcTc
tys
    PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [ConLike -> [Type] -> PatVec -> PmPat 'PAT
vanillaConPattern ConLike
tuple_con [Type]
tys' ([PatVec] -> PatVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [PatVec]
tidy_ps)]

  SumPat ty :: XSumPat GhcTc
ty p :: LPat GhcTc
p alt :: Int
alt arity :: Int
arity -> do
    PatVec
tidy_p <- FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts (LPat GhcTc -> SrcSpanLess (LPat GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LPat GhcTc
p)
    let sum_con :: ConLike
sum_con = DataCon -> ConLike
RealDataCon (Int -> Int -> DataCon
sumDataCon Int
alt Int
arity)
    -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
    PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [ConLike -> [Type] -> PatVec -> PmPat 'PAT
vanillaConPattern ConLike
sum_con ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map HasDebugCallStack => Type -> Type
Type -> Type
getRuntimeRep [Type]
XSumPat GhcTc
ty [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
XSumPat GhcTc
ty) PatVec
tidy_p]

  -- --------------------------------------------------------------------------
  -- Not supposed to happen
  ConPatIn  {} -> String -> DsM PatVec
forall a. String -> a
panic "Check.translatePat: ConPatIn"
  SplicePat {} -> String -> DsM PatVec
forall a. String -> a
panic "Check.translatePat: SplicePat"
  XPat      {} -> String -> DsM PatVec
forall a. String -> a
panic "Check.translatePat: XPat"

{- Note [Translate Overloaded Literal for Exhaustiveness Checking]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The translation of @NPat@ in exhaustiveness checker is a bit different
from translation in pattern matcher.

  * In pattern matcher (see `tidyNPat' in deSugar/MatchLit.hs), we
    translate integral literals to HsIntPrim or HsWordPrim and translate
    overloaded strings to HsString.

  * In exhaustiveness checker, in `genCaseTmCs1/genCaseTmCs2`, we use
    `lhsExprToPmExpr` to generate uncovered set. In `hsExprToPmExpr`,
    however we generate `PmOLit` for HsOverLit, rather than refine
    `HsOverLit` inside `NPat` to HsIntPrim/HsWordPrim. If we do
    the same thing in `translatePat` as in `tidyNPat`, the exhaustiveness
    checker will fail to match the literals patterns correctly. See
    Trac #14546.

  In Note [Undecidable Equality for Overloaded Literals], we say: "treat
  overloaded literals that look different as different", but previously we
  didn't do such things.

  Now, we translate the literal value to match and the literal patterns
  consistently:

  * For integral literals, we parse both the integral literal value and
    the patterns as OverLit HsIntegral. For example:

      case 0::Int of
          0 -> putStrLn "A"
          1 -> putStrLn "B"
          _ -> putStrLn "C"

    When checking the exhaustiveness of pattern matching, we translate the 0
    in value position as PmOLit, but translate the 0 and 1 in pattern position
    as PmSLit. The inconsistency leads to the failure of eqPmLit to detect the
    equality and report warning of "Pattern match is redundant" on pattern 0,
    as reported in Trac #14546. In this patch we remove the specialization of
    OverLit patterns, and keep the overloaded number literal in pattern as it
    is to maintain the consistency. We know nothing about the `fromInteger`
    method (see Note [Undecidable Equality for Overloaded Literals]). Now we
    can capture the exhaustiveness of pattern 0 and the redundancy of pattern
    1 and _.

  * For string literals, we parse the string literals as HsString. When
    OverloadedStrings is enabled, it further be turned as HsOverLit HsIsString.
    For example:

      case "foo" of
          "foo" -> putStrLn "A"
          "bar" -> putStrLn "B"
          "baz" -> putStrLn "C"

    Previously, the overloaded string values are translated to PmOLit and the
    non-overloaded string values are translated to PmSLit. However the string
    patterns, both overloaded and non-overloaded, are translated to list of
    characters. The inconsistency leads to wrong warnings about redundant and
    non-exhaustive pattern matching warnings, as reported in Trac #14546.

    In order to catch the redundant pattern in following case:

      case "foo" of
          ('f':_) -> putStrLn "A"
          "bar" -> putStrLn "B"

    in this patch, we translate non-overloaded string literals, both in value
    position and pattern position, as list of characters. For overloaded string
    literals, we only translate it to list of characters only when it's type
    is stringTy, since we know nothing about the toString methods. But we know
    that if two overloaded strings are syntax equal, then they are equal. Then
    if it's type is not stringTy, we just translate it to PmOLit. We can still
    capture the exhaustiveness of pattern "foo" and the redundancy of pattern
    "bar" and "baz" in the following code:

      {-# LANGUAGE OverloadedStrings #-}
      main = do
        case "foo" of
            "foo" -> putStrLn "A"
            "bar" -> putStrLn "B"
            "baz" -> putStrLn "C"

  We must ensure that doing the same translation to literal values and patterns
  in `translatePat` and `hsExprToPmExpr`. The previous inconsistent work led to
  Trac #14546.
-}

-- | Translate a list of patterns (Note: each pattern is translated
-- to a pattern vector but we do not concatenate the results).
translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
translatePatVec :: FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec fam_insts :: FamInstEnvs
fam_insts pats :: [LPat GhcTc]
pats = (LPat GhcTc -> DsM PatVec)
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts) [LPat GhcTc]
pats

-- | Translate a constructor pattern
translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
                   -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
translateConPatVec :: FamInstEnvs
-> [Type]
-> [TyVar]
-> ConLike
-> HsConPatDetails GhcTc
-> DsM PatVec
translateConPatVec fam_insts :: FamInstEnvs
fam_insts _univ_tys :: [Type]
_univ_tys _ex_tvs :: [TyVar]
_ex_tvs _ (PrefixCon ps :: [LPat GhcTc]
ps)
  = [PatVec] -> PatVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([PatVec] -> PatVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [PatVec] -> DsM PatVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec FamInstEnvs
fam_insts ((LPat GhcTc -> LPat GhcTc) -> [LPat GhcTc] -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map LPat GhcTc -> LPat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LPat GhcTc]
ps)
translateConPatVec fam_insts :: FamInstEnvs
fam_insts _univ_tys :: [Type]
_univ_tys _ex_tvs :: [TyVar]
_ex_tvs _ (InfixCon p1 :: LPat GhcTc
p1 p2 :: LPat GhcTc
p2)
  = [PatVec] -> PatVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([PatVec] -> PatVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [PatVec] -> DsM PatVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec FamInstEnvs
fam_insts ((LPat GhcTc -> LPat GhcTc) -> [LPat GhcTc] -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map LPat GhcTc -> LPat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LPat GhcTc
p1,LPat GhcTc
p2])
translateConPatVec fam_insts :: FamInstEnvs
fam_insts  univ_tys :: [Type]
univ_tys  ex_tvs :: [TyVar]
ex_tvs c :: ConLike
c (RecCon (HsRecFields fs :: [LHsRecField GhcTc (LPat GhcTc)]
fs _))
    -- Nothing matched. Make up some fresh term variables
  | [LHsRecField GhcTc (LPat GhcTc)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LHsRecField GhcTc (LPat GhcTc)]
fs        = [Type] -> DsM PatVec
mkPmVars [Type]
arg_tys
    -- The data constructor was not defined using record syntax. For the
    -- pattern to be in record syntax it should be empty (e.g. Just {}).
    -- So just like the previous case.
  | [Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Name]
orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
    -- Some of the fields appear, in the original order (there may be holes).
    -- Generate a simple constructor pattern and make up fresh variables for
    -- the rest of the fields
  | [Name]
matched_lbls [Name] -> [Name] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`subsetOf` [Name]
orig_lbls
  = ASSERT(orig_lbls `equalLength` arg_tys)
      let translateOne :: (Name, Type) -> DsM PatVec
translateOne (lbl :: Name
lbl, ty :: Type
ty) = case Name -> [(Name, LPat GhcTc)] -> Maybe (LPat GhcTc)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
lbl [(Name, LPat GhcTc)]
matched_pats of
            Just p :: LPat GhcTc
p  -> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts LPat GhcTc
p
            Nothing -> [Type] -> DsM PatVec
mkPmVars [Type
ty]
      in  ((Name, Type) -> DsM PatVec) -> [(Name, Type)] -> DsM PatVec
forall (m :: * -> *) a b. Monad m => (a -> m [b]) -> [a] -> m [b]
concatMapM (Name, Type) -> DsM PatVec
translateOne ([Name] -> [Type] -> [(Name, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
orig_lbls [Type]
arg_tys)
    -- The fields that appear are not in the correct order. Make up fresh
    -- variables for all fields and add guards after matching, to force the
    -- evaluation in the correct order.
  | Bool
otherwise = do
      PatVec
arg_var_pats    <- [Type] -> DsM PatVec
mkPmVars [Type]
arg_tys
      [(Name, PatVec)]
translated_pats <- [(Name, LPat GhcTc)]
-> ((Name, LPat GhcTc)
    -> IOEnv (Env DsGblEnv DsLclEnv) (Name, PatVec))
-> IOEnv (Env DsGblEnv DsLclEnv) [(Name, PatVec)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, LPat GhcTc)]
matched_pats (((Name, LPat GhcTc)
  -> IOEnv (Env DsGblEnv DsLclEnv) (Name, PatVec))
 -> IOEnv (Env DsGblEnv DsLclEnv) [(Name, PatVec)])
-> ((Name, LPat GhcTc)
    -> IOEnv (Env DsGblEnv DsLclEnv) (Name, PatVec))
-> IOEnv (Env DsGblEnv DsLclEnv) [(Name, PatVec)]
forall a b. (a -> b) -> a -> b
$ \(x :: Name
x,pat :: LPat GhcTc
pat) -> do
        PatVec
pvec <- FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts LPat GhcTc
pat
        (Name, PatVec) -> IOEnv (Env DsGblEnv DsLclEnv) (Name, PatVec)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
x, PatVec
pvec)

      let zipped :: [(Name, TyVar)]
zipped = [Name] -> [TyVar] -> [(Name, TyVar)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
orig_lbls [ TyVar
x | PmVar x :: TyVar
x <- PatVec
arg_var_pats ]
          guards :: PatVec
guards = ((Name, PatVec) -> PmPat 'PAT) -> [(Name, PatVec)] -> PatVec
forall a b. (a -> b) -> [a] -> [b]
map (\(name :: Name
name,pvec :: PatVec
pvec) -> case Name -> [(Name, TyVar)] -> Maybe TyVar
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
name [(Name, TyVar)]
zipped of
                            Just x :: TyVar
x  -> PatVec -> PmExpr -> PmPat 'PAT
PmGrd PatVec
pvec (Name -> PmExpr
PmExprVar (TyVar -> Name
idName TyVar
x))
                            Nothing -> String -> PmPat 'PAT
forall a. String -> a
panic "translateConPatVec: lookup")
                       [(Name, PatVec)]
translated_pats

      PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return (PatVec
arg_var_pats PatVec -> PatVec -> PatVec
forall a. [a] -> [a] -> [a]
++ PatVec
guards)
  where
    -- The actual argument types (instantiated)
    arg_tys :: [Type]
arg_tys = ConLike -> [Type] -> [Type]
conLikeInstOrigArgTys ConLike
c ([Type]
univ_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [TyVar] -> [Type]
mkTyVarTys [TyVar]
ex_tvs)

    -- Some label information
    orig_lbls :: [Name]
orig_lbls    = (FieldLbl Name -> Name) -> [FieldLbl Name] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map FieldLbl Name -> Name
forall a. FieldLbl a -> a
flSelector ([FieldLbl Name] -> [Name]) -> [FieldLbl Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ ConLike -> [FieldLbl Name]
conLikeFieldLabels ConLike
c
    matched_pats :: [(Name, LPat GhcTc)]
matched_pats = [ (TyVar -> Name
forall a. NamedThing a => a -> Name
getName (Located TyVar -> SrcSpanLess (Located TyVar)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc (HsRecField GhcTc (LPat GhcTc) -> Located TyVar
forall arg. HsRecField GhcTc arg -> Located TyVar
hsRecFieldId SrcSpanLess (LHsRecField GhcTc (LPat GhcTc))
HsRecField GhcTc (LPat GhcTc)
x)), LPat GhcTc -> SrcSpanLess (LPat GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc (HsRecField GhcTc (LPat GhcTc) -> LPat GhcTc
forall id arg. HsRecField' id arg -> arg
hsRecFieldArg SrcSpanLess (LHsRecField GhcTc (LPat GhcTc))
HsRecField GhcTc (LPat GhcTc)
x))
                   | (LHsRecField GhcTc (LPat GhcTc)
-> Located (SrcSpanLess (LHsRecField GhcTc (LPat GhcTc)))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ x :: SrcSpanLess (LHsRecField GhcTc (LPat GhcTc))
x) <- [LHsRecField GhcTc (LPat GhcTc)]
fs]
    matched_lbls :: [Name]
matched_lbls = [ Name
name | (name :: Name
name, _pat :: LPat GhcTc
_pat) <- [(Name, LPat GhcTc)]
matched_pats ]

    subsetOf :: Eq a => [a] -> [a] -> Bool
    subsetOf :: [a] -> [a] -> Bool
subsetOf []     _  = Bool
True
    subsetOf (_:_)  [] = Bool
False
    subsetOf (x :: a
x:xs :: [a]
xs) (y :: a
y:ys :: [a]
ys)
      | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y    = [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
subsetOf    [a]
xs  [a]
ys
      | Bool
otherwise = [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
subsetOf (a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
xs) [a]
ys

-- Translate a single match
translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
               -> DsM (PatVec,[PatVec])
translateMatch :: FamInstEnvs
-> LMatch GhcTc (LHsExpr GhcTc) -> DsM (PatVec, [PatVec])
translateMatch fam_insts :: FamInstEnvs
fam_insts (LMatch GhcTc (LHsExpr GhcTc)
-> Located (SrcSpanLess (LMatch GhcTc (LHsExpr GhcTc)))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ (Match { m_pats = lpats, m_grhss = grhss })) =
  do
  PatVec
pats'   <- [PatVec] -> PatVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([PatVec] -> PatVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [PatVec] -> DsM PatVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs
-> [LPat GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
translatePatVec FamInstEnvs
fam_insts [LPat GhcTc]
pats
  [PatVec]
guards' <- ([GuardStmt GhcTc] -> DsM PatVec)
-> [[GuardStmt GhcTc]] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
translateGuards FamInstEnvs
fam_insts) [[GuardStmt GhcTc]]
guards
  (PatVec, [PatVec]) -> DsM (PatVec, [PatVec])
forall (m :: * -> *) a. Monad m => a -> m a
return (PatVec
pats', [PatVec]
guards')
  where
    extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
    extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
extractGuards (LGRHS GhcTc (LHsExpr GhcTc)
-> Located (SrcSpanLess (LGRHS GhcTc (LHsExpr GhcTc)))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ (GRHS _ gs _)) = (GuardLStmt GhcTc -> GuardStmt GhcTc)
-> [GuardLStmt GhcTc] -> [GuardStmt GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map GuardLStmt GhcTc -> GuardStmt GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [GuardLStmt GhcTc]
gs
    extractGuards _                       = String -> [GuardStmt GhcTc]
forall a. String -> a
panic "translateMatch"

    pats :: [LPat GhcTc]
pats   = (LPat GhcTc -> LPat GhcTc) -> [LPat GhcTc] -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map LPat GhcTc -> LPat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LPat GhcTc]
lpats
    guards :: [[GuardStmt GhcTc]]
guards = (LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc])
-> [LGRHS GhcTc (LHsExpr GhcTc)] -> [[GuardStmt GhcTc]]
forall a b. (a -> b) -> [a] -> [b]
map LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
extractGuards (GRHSs GhcTc (LHsExpr GhcTc) -> [LGRHS GhcTc (LHsExpr GhcTc)]
forall p body. GRHSs p body -> [LGRHS p body]
grhssGRHSs GRHSs GhcTc (LHsExpr GhcTc)
grhss)
translateMatch _ _ = String -> DsM (PatVec, [PatVec])
forall a. String -> a
panic "translateMatch"

-- -----------------------------------------------------------------------
-- * Transform source guards (GuardStmt Id) to PmPats (Pattern)

-- | Translate a list of guard statements to a pattern vector
translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
translateGuards fam_insts :: FamInstEnvs
fam_insts guards :: [GuardStmt GhcTc]
guards = do
  PatVec
all_guards <- [PatVec] -> PatVec
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([PatVec] -> PatVec)
-> IOEnv (Env DsGblEnv DsLclEnv) [PatVec] -> DsM PatVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (GuardStmt GhcTc -> DsM PatVec)
-> [GuardStmt GhcTc] -> IOEnv (Env DsGblEnv DsLclEnv) [PatVec]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
translateGuard FamInstEnvs
fam_insts) [GuardStmt GhcTc]
guards
  PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return (PatVec -> PatVec
replace_unhandled PatVec
all_guards)
  -- It should have been (return all_guards) but it is too expressive.
  -- Since the term oracle does not handle all constraints we generate,
  -- we (hackily) replace all constraints the oracle cannot handle with a
  -- single one (we need to know if there is a possibility of falure).
  -- See Note [Guards and Approximation] for all guard-related approximations
  -- we implement.
  where
    replace_unhandled :: PatVec -> PatVec
    replace_unhandled :: PatVec -> PatVec
replace_unhandled gv :: PatVec
gv
      | PatVec -> Bool
any_unhandled PatVec
gv = PmPat 'PAT
fake_pat PmPat 'PAT -> PatVec -> PatVec
forall a. a -> [a] -> [a]
: [ PmPat 'PAT
p | PmPat 'PAT
p <- PatVec
gv, PmPat 'PAT -> Bool
shouldKeep PmPat 'PAT
p ]
      | Bool
otherwise        = PatVec
gv

    any_unhandled :: PatVec -> Bool
    any_unhandled :: PatVec -> Bool
any_unhandled gv :: PatVec
gv = (PmPat 'PAT -> Bool) -> PatVec -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> (PmPat 'PAT -> Bool) -> PmPat 'PAT -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmPat 'PAT -> Bool
shouldKeep) PatVec
gv

    shouldKeep :: Pattern -> Bool
    shouldKeep :: PmPat 'PAT -> Bool
shouldKeep p :: PmPat 'PAT
p
      | PmVar {} <- PmPat 'PAT
p      = Bool
True
      | PmCon {} <- PmPat 'PAT
p      = ConLike -> Bool
singleConstructor (PmPat 'PAT -> ConLike
forall (t :: PatTy). PmPat t -> ConLike
pm_con_con PmPat 'PAT
p)
                             Bool -> Bool -> Bool
&& (PmPat 'PAT -> Bool) -> PatVec -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PmPat 'PAT -> Bool
shouldKeep (PmPat 'PAT -> PatVec
forall (t :: PatTy). PmPat t -> [PmPat t]
pm_con_args PmPat 'PAT
p)
    shouldKeep (PmGrd pv :: PatVec
pv e :: PmExpr
e)
      | (PmPat 'PAT -> Bool) -> PatVec -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PmPat 'PAT -> Bool
shouldKeep PatVec
pv  = Bool
True
      | PmExpr -> Bool
isNotPmExprOther PmExpr
e = Bool
True  -- expensive but we want it
    shouldKeep _other_pat :: PmPat 'PAT
_other_pat  = Bool
False -- let the rest..

-- | Check whether a pattern can fail to match
cantFailPattern :: Pattern -> Bool
cantFailPattern :: PmPat 'PAT -> Bool
cantFailPattern p :: PmPat 'PAT
p
  | PmVar {} <- PmPat 'PAT
p = Bool
True
  | PmCon {} <- PmPat 'PAT
p = ConLike -> Bool
singleConstructor (PmPat 'PAT -> ConLike
forall (t :: PatTy). PmPat t -> ConLike
pm_con_con PmPat 'PAT
p)
                    Bool -> Bool -> Bool
&& (PmPat 'PAT -> Bool) -> PatVec -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PmPat 'PAT -> Bool
cantFailPattern (PmPat 'PAT -> PatVec
forall (t :: PatTy). PmPat t -> [PmPat t]
pm_con_args PmPat 'PAT
p)
cantFailPattern (PmGrd pv :: PatVec
pv _e :: PmExpr
_e)
                  = (PmPat 'PAT -> Bool) -> PatVec -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PmPat 'PAT -> Bool
cantFailPattern PatVec
pv
cantFailPattern _ = Bool
False

-- | Translate a guard statement to Pattern
translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
translateGuard :: FamInstEnvs -> GuardStmt GhcTc -> DsM PatVec
translateGuard fam_insts :: FamInstEnvs
fam_insts guard :: GuardStmt GhcTc
guard = case GuardStmt GhcTc
guard of
  BodyStmt _   e :: LHsExpr GhcTc
e _ _ -> LHsExpr GhcTc -> DsM PatVec
translateBoolGuard LHsExpr GhcTc
e
  LetStmt  _   binds :: LHsLocalBindsLR GhcTc GhcTc
binds -> HsLocalBinds GhcTc -> DsM PatVec
translateLet (LHsLocalBindsLR GhcTc GhcTc
-> SrcSpanLess (LHsLocalBindsLR GhcTc GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsLocalBindsLR GhcTc GhcTc
binds)
  BindStmt _ p :: LPat GhcTc
p e :: LHsExpr GhcTc
e _ _ -> FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
translateBind FamInstEnvs
fam_insts LPat GhcTc
p LHsExpr GhcTc
e
  LastStmt        {} -> String -> DsM PatVec
forall a. String -> a
panic "translateGuard LastStmt"
  ParStmt         {} -> String -> DsM PatVec
forall a. String -> a
panic "translateGuard ParStmt"
  TransStmt       {} -> String -> DsM PatVec
forall a. String -> a
panic "translateGuard TransStmt"
  RecStmt         {} -> String -> DsM PatVec
forall a. String -> a
panic "translateGuard RecStmt"
  ApplicativeStmt {} -> String -> DsM PatVec
forall a. String -> a
panic "translateGuard ApplicativeLastStmt"
  XStmtLR         {} -> String -> DsM PatVec
forall a. String -> a
panic "translateGuard RecStmt"

-- | Translate let-bindings
translateLet :: HsLocalBinds GhcTc -> DsM PatVec
translateLet :: HsLocalBinds GhcTc -> DsM PatVec
translateLet _binds :: HsLocalBinds GhcTc
_binds = PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- | Translate a pattern guard
translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
translateBind :: FamInstEnvs -> LPat GhcTc -> LHsExpr GhcTc -> DsM PatVec
translateBind fam_insts :: FamInstEnvs
fam_insts (LPat GhcTc -> Located (SrcSpanLess (LPat GhcTc))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ p :: SrcSpanLess (LPat GhcTc)
p) e :: LHsExpr GhcTc
e = do
  PatVec
ps <- FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts SrcSpanLess (LPat GhcTc)
LPat GhcTc
p
  PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [PatVec -> HsExpr GhcTc -> PmPat 'PAT
mkGuard PatVec
ps (LHsExpr GhcTc -> SrcSpanLess (LHsExpr GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcTc
e)]

-- | Translate a boolean guard
translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
translateBoolGuard :: LHsExpr GhcTc -> DsM PatVec
translateBoolGuard e :: LHsExpr GhcTc
e
  | Maybe (CoreExpr -> DsM CoreExpr) -> Bool
forall a. Maybe a -> Bool
isJust (LHsExpr GhcTc -> Maybe (CoreExpr -> DsM CoreExpr)
isTrueLHsExpr LHsExpr GhcTc
e) = PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return []
    -- The formal thing to do would be to generate (True <- True)
    -- but it is trivial to solve so instead we give back an empty
    -- PatVec for efficiency
  | Bool
otherwise = PatVec -> DsM PatVec
forall (m :: * -> *) a. Monad m => a -> m a
return [PatVec -> HsExpr GhcTc -> PmPat 'PAT
mkGuard [PmPat 'PAT
truePattern] (LHsExpr GhcTc -> SrcSpanLess (LHsExpr GhcTc)
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc LHsExpr GhcTc
e)]

{- Note [Guards and Approximation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Even if the algorithm is really expressive, the term oracle we use is not.
Hence, several features are not translated *properly* but we approximate.
The list includes:

1. View Patterns
----------------
A view pattern @(f -> p)@ should be translated to @x (p <- f x)@. The term
oracle does not handle function applications so we know that the generated
constraints will not be handled at the end. Hence, we distinguish between two
cases:
  a) Pattern @p@ cannot fail. Then this is just a binding and we do the *right
     thing*.
  b) Pattern @p@ can fail. This means that when checking the guard, we will
     generate several cases, with no useful information. E.g.:

       h (f -> [a,b]) = ...
       h x ([a,b] <- f x) = ...

       uncovered set = { [x |> { False ~ (f x ~ [])            }]
                       , [x |> { False ~ (f x ~ (t1:[]))       }]
                       , [x |> { False ~ (f x ~ (t1:t2:t3:t4)) }] }

     So we have two problems:
       1) Since we do not print the constraints in the general case (they may
          be too many), the warning will look like this:

            Pattern match(es) are non-exhaustive
            In an equation for `h':
                Patterns not matched:
                    _
                    _
                    _
          Which is not short and not more useful than a single underscore.
       2) The size of the uncovered set increases a lot, without gaining more
          expressivity in our warnings.

     Hence, in this case, we replace the guard @([a,b] <- f x)@ with a *dummy*
     @fake_pat@: @True <- _@. That is, we record that there is a possibility
     of failure but we minimize it to a True/False. This generates a single
     warning and much smaller uncovered sets.

2. Overloaded Lists
-------------------
An overloaded list @[...]@ should be translated to @x ([...] <- toList x)@. The
problem is exactly like above, as its solution. For future reference, the code
below is the *right thing to do*:

   ListPat (ListPatTc elem_ty (Just (pat_ty, _to_list))) lpats
     otherwise -> do
       (xp, xe) <- mkPmId2Forms pat_ty
       ps       <- translatePatVec (map unLoc lpats)
       let pats = foldr (mkListPatVec elem_ty) [nilPattern elem_ty] ps
           g    = mkGuard pats (HsApp (noLoc to_list) xe)
       return [xp,g]

3. Overloaded Literals
----------------------
The case with literals is a bit different. a literal @l@ should be translated
to @x (True <- x == from l)@. Since we want to have better warnings for
overloaded literals as it is a very common feature, we treat them differently.
They are mainly covered in Note [Undecidable Equality for Overloaded Literals]
in PmExpr.

4. N+K Patterns & Pattern Synonyms
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
An n+k pattern (n+k) should be translated to @x (True <- x >= k) (n <- x-k)@.
Since the only pattern of the three that causes failure is guard @(n <- x-k)@,
and has two possible outcomes. Hence, there is no benefit in using a dummy and
we implement the proper thing. Pattern synonyms are simply not implemented yet.
Hence, to be conservative, we generate a dummy pattern, assuming that the
pattern can fail.

5. Actual Guards
----------------
During translation, boolean guards and pattern guards are translated properly.
Let bindings though are omitted by function @translateLet@. Since they are lazy
bindings, we do not actually want to generate a (strict) equality (like we do
in the pattern bind case). Hence, we safely drop them.

Additionally, top-level guard translation (performed by @translateGuards@)
replaces guards that cannot be reasoned about (like the ones we described in
1-4) with a single @fake_pat@ to record the possibility of failure to match.

Note [Translate CoPats]
~~~~~~~~~~~~~~~~~~~~~~~
The pattern match checker did not know how to handle coerced patterns `CoPat`
efficiently, which gave rise to #11276. The original approach translated
`CoPat`s:

    pat |> co    ===>    x (pat <- (e |> co))

Instead, we now check whether the coercion is a hole or if it is just refl, in
which case we can drop it. Unfortunately, data families generate useful
coercions so guards are still generated in these cases and checking data
families is not really efficient.

%************************************************************************
%*                                                                      *
                 Utilities for Pattern Match Checking
%*                                                                      *
%************************************************************************
-}

-- ----------------------------------------------------------------------------
-- * Basic utilities

-- | Get the type out of a PmPat. For guard patterns (ps <- e) we use the type
-- of the first (or the single -WHEREVER IT IS- valid to use?) pattern
pmPatType :: PmPat p -> Type
pmPatType :: PmPat p -> Type
pmPatType (PmCon { pm_con_con :: forall (t :: PatTy). PmPat t -> ConLike
pm_con_con = ConLike
con, pm_con_arg_tys :: forall (t :: PatTy). PmPat t -> [Type]
pm_con_arg_tys = [Type]
tys })
  = ConLike -> [Type] -> Type
conLikeResTy ConLike
con [Type]
tys
pmPatType (PmVar  { pm_var_id :: forall (t :: PatTy). PmPat t -> TyVar
pm_var_id  = TyVar
x }) = TyVar -> Type
idType TyVar
x
pmPatType (PmLit  { pm_lit_lit :: forall (t :: PatTy). PmPat t -> PmLit
pm_lit_lit = PmLit
l }) = PmLit -> Type
pmLitType PmLit
l
pmPatType (PmNLit { pm_lit_id :: PmPat 'VA -> TyVar
pm_lit_id  = TyVar
x }) = TyVar -> Type
idType TyVar
x
pmPatType (PmGrd  { pm_grd_pv :: PmPat 'PAT -> PatVec
pm_grd_pv  = PatVec
pv })
  = ASSERT(patVecArity pv == 1) (pmPatType p)
  where Just p :: PmPat 'PAT
p = (PmPat 'PAT -> Bool) -> PatVec -> Maybe (PmPat 'PAT)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==1) (Int -> Bool) -> (PmPat 'PAT -> Int) -> PmPat 'PAT -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmPat 'PAT -> Int
patternArity) PatVec
pv

-- | Information about a conlike that is relevant to coverage checking.
-- It is called an \"inhabitation candidate\" since it is a value which may
-- possibly inhabit some type, but only if its term constraint ('ic_tm_ct')
-- and type constraints ('ic_ty_cs') are permitting, and if all of its strict
-- argument types ('ic_strict_arg_tys') are inhabitable.
-- See @Note [Extensions to GADTs Meet Their Match]@.
data InhabitationCandidate =
  InhabitationCandidate
  { InhabitationCandidate -> PmPat 'VA
ic_val_abs        :: ValAbs
  , InhabitationCandidate -> ComplexEq
ic_tm_ct          :: ComplexEq
  , InhabitationCandidate -> Bag TyVar
ic_ty_cs          :: Bag EvVar
  , InhabitationCandidate -> [Type]
ic_strict_arg_tys :: [Type]
  }

{-
Note [Extensions to GADTs Meet Their Match]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The GADTs Meet Their Match paper presents the formalism that GHC's coverage
checker adheres to. Since the paper's publication, there have been some
additional features added to the coverage checker which are not described in
the paper. This Note serves as a reference for these new features.

-----
-- Strict argument type constraints
-----

In the ConVar case of clause processing, each conlike K traditionally
generates two different forms of constraints:

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

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

  data K = K1 | K2 !Void

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

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

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

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

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

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

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

    data MyVoid = MkMyVoid !Void

  `nonVoid MyVoid` returns False. The InhabitationCandidate for the MkMyVoid
  constructor contains Void as a strict argument type, and since `nonVoid Void`
  returns False, that InhabitationCandidate is discarded, leaving no others.

* Performance considerations

We must be careful when recursively calling `nonVoid` on the strict argument
types of an InhabitationCandidate, because doing so naïvely can cause GHC to
fall into an infinite loop. Consider the following example:

  data Abyss = MkAbyss !Abyss

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

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

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

  newtype Chasm = MkChasm Chasm

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

So this limitation is somewhat understandable.

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

  data T = MkT !T !T !T

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

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

Another microoptimization applies to data types like this one:

  data S a = ![a] !T

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

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

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

instance Outputable InhabitationCandidate where
  ppr :: InhabitationCandidate -> SDoc
ppr (InhabitationCandidate { ic_val_abs :: InhabitationCandidate -> PmPat 'VA
ic_val_abs = PmPat 'VA
va, ic_tm_ct :: InhabitationCandidate -> ComplexEq
ic_tm_ct = ComplexEq
tm_ct
                             , ic_ty_cs :: InhabitationCandidate -> Bag TyVar
ic_ty_cs = Bag TyVar
ty_cs
                             , ic_strict_arg_tys :: InhabitationCandidate -> [Type]
ic_strict_arg_tys = [Type]
strict_arg_tys }) =
    String -> SDoc
text "InhabitationCandidate" SDoc -> SDoc -> SDoc
<+>
      [SDoc] -> SDoc
vcat [ String -> SDoc
text "ic_val_abs        =" SDoc -> SDoc -> SDoc
<+> PmPat 'VA -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmPat 'VA
va
           , String -> SDoc
text "ic_tm_ct          =" SDoc -> SDoc -> SDoc
<+> ComplexEq -> SDoc
forall a. Outputable a => a -> SDoc
ppr ComplexEq
tm_ct
           , String -> SDoc
text "ic_ty_cs          =" SDoc -> SDoc -> SDoc
<+> Bag TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr Bag TyVar
ty_cs
           , String -> SDoc
text "ic_strict_arg_tys =" SDoc -> SDoc -> SDoc
<+> [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Type]
strict_arg_tys ]

-- | Generate an 'InhabitationCandidate' for a given conlike (generate
-- fresh variables of the appropriate type for arguments)
mkOneConFull :: Id -> ConLike -> DsM InhabitationCandidate
--  *  x :: T tys, where T is an algebraic data type
--     NB: in the case of a data family, T is the *representation* TyCon
--     e.g.   data instance T (a,b) = T1 a b
--       leads to
--            data TPair a b = T1 a b  -- The "representation" type
--       It is TPair, not T, that is given to mkOneConFull
--
--  * 'con' K is a conlike of data type T
--
-- After instantiating the universal tyvars of K we get
--          K tys :: forall bs. Q => s1 .. sn -> T tys
--
-- Suppose y1 is a strict field. Then we get
-- Results: ic_val_abs:        K (y1::s1) .. (yn::sn)
--          ic_tm_ct:          x ~ K y1..yn
--          ic_ty_cs:          Q
--          ic_strict_arg_tys: [s1]
mkOneConFull :: TyVar
-> ConLike -> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
mkOneConFull x :: TyVar
x con :: ConLike
con = do
  let res_ty :: Type
res_ty  = TyVar -> Type
idType TyVar
x
      (univ_tvs :: [TyVar]
univ_tvs, ex_tvs :: [TyVar]
ex_tvs, eq_spec :: [EqSpec]
eq_spec, thetas :: [Type]
thetas, _req_theta :: [Type]
_req_theta , arg_tys :: [Type]
arg_tys, con_res_ty :: Type
con_res_ty)
        = ConLike
-> ([TyVar], [TyVar], [EqSpec], [Type], [Type], [Type], Type)
conLikeFullSig ConLike
con
      arg_is_banged :: [Bool]
arg_is_banged = (HsImplBang -> Bool) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map HsImplBang -> Bool
isBanged ([HsImplBang] -> [Bool]) -> [HsImplBang] -> [Bool]
forall a b. (a -> b) -> a -> b
$ ConLike -> [HsImplBang]
conLikeImplBangs ConLike
con
      tc_args :: [Type]
tc_args = Type -> [Type]
tyConAppArgs Type
res_ty
      subst1 :: TCvSubst
subst1  = case ConLike
con of
                  RealDataCon {} -> [TyVar] -> [Type] -> TCvSubst
HasDebugCallStack => [TyVar] -> [Type] -> TCvSubst
zipTvSubst [TyVar]
univ_tvs [Type]
tc_args
                  PatSynCon {}   -> String -> Maybe TCvSubst -> TCvSubst
forall a. HasCallStack => String -> Maybe a -> a
expectJust "mkOneConFull" (Type -> Type -> Maybe TCvSubst
tcMatchTy Type
con_res_ty Type
res_ty)
                                    -- See Note [Pattern synonym result type] in PatSyn

  (subst :: TCvSubst
subst, ex_tvs' :: [TyVar]
ex_tvs') <- TCvSubst -> [TyVar] -> UniqSupply -> (TCvSubst, [TyVar])
cloneTyVarBndrs TCvSubst
subst1 [TyVar]
ex_tvs (UniqSupply -> (TCvSubst, [TyVar]))
-> IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
-> IOEnv (Env DsGblEnv DsLclEnv) (TCvSubst, [TyVar])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env DsGblEnv DsLclEnv) UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM

  let arg_tys' :: [Type]
arg_tys' = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst [Type]
arg_tys
  -- Fresh term variables (VAs) as arguments to the constructor
  [PmPat 'VA]
arguments <-  (Type -> IOEnv (Env DsGblEnv DsLclEnv) (PmPat 'VA))
-> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [PmPat 'VA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> IOEnv (Env DsGblEnv DsLclEnv) (PmPat 'VA)
forall (p :: PatTy). Type -> DsM (PmPat p)
mkPmVar [Type]
arg_tys'
  -- All constraints bound by the constructor (alpha-renamed)
  let theta_cs :: [Type]
theta_cs = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTheta TCvSubst
subst ([EqSpec] -> [Type]
eqSpecPreds [EqSpec]
eq_spec [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
thetas)
  [TyVar]
evvars <- (Type -> DsM TyVar)
-> [Type] -> IOEnv (Env DsGblEnv DsLclEnv) [TyVar]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String -> Type -> DsM TyVar
nameType "pm") [Type]
theta_cs
  let con_abs :: PmPat 'VA
con_abs  = PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con     = ConLike
con
                       , pm_con_arg_tys :: [Type]
pm_con_arg_tys = [Type]
tc_args
                       , pm_con_tvs :: [TyVar]
pm_con_tvs     = [TyVar]
ex_tvs'
                       , pm_con_dicts :: [TyVar]
pm_con_dicts   = [TyVar]
evvars
                       , pm_con_args :: [PmPat 'VA]
pm_con_args    = [PmPat 'VA]
arguments }
      strict_arg_tys :: [Type]
strict_arg_tys = [Bool] -> [Type] -> [Type]
forall a. [Bool] -> [a] -> [a]
filterByList [Bool]
arg_is_banged [Type]
arg_tys'
  InhabitationCandidate
-> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
forall (m :: * -> *) a. Monad m => a -> m a
return (InhabitationCandidate
 -> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate)
-> InhabitationCandidate
-> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
forall a b. (a -> b) -> a -> b
$ InhabitationCandidate :: PmPat 'VA
-> ComplexEq -> Bag TyVar -> [Type] -> InhabitationCandidate
InhabitationCandidate
           { ic_val_abs :: PmPat 'VA
ic_val_abs        = PmPat 'VA
con_abs
           , ic_tm_ct :: ComplexEq
ic_tm_ct          = (Name -> PmExpr
PmExprVar (TyVar -> Name
idName TyVar
x), PmPat 'VA -> PmExpr
vaToPmExpr PmPat 'VA
con_abs)
           , ic_ty_cs :: Bag TyVar
ic_ty_cs          = [TyVar] -> Bag TyVar
forall a. [a] -> Bag a
listToBag [TyVar]
evvars
           , ic_strict_arg_tys :: [Type]
ic_strict_arg_tys = [Type]
strict_arg_tys
           }

-- ----------------------------------------------------------------------------
-- * More smart constructors and fresh variable generation

-- | Create a guard pattern
mkGuard :: PatVec -> HsExpr GhcTc -> Pattern
mkGuard :: PatVec -> HsExpr GhcTc -> PmPat 'PAT
mkGuard pv :: PatVec
pv e :: HsExpr GhcTc
e
  | (PmPat 'PAT -> Bool) -> PatVec -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all PmPat 'PAT -> Bool
cantFailPattern PatVec
pv = PatVec -> PmExpr -> PmPat 'PAT
PmGrd PatVec
pv PmExpr
expr
  | PmExprOther {} <- PmExpr
expr = PmPat 'PAT
fake_pat
  | Bool
otherwise              = PatVec -> PmExpr -> PmPat 'PAT
PmGrd PatVec
pv PmExpr
expr
  where
    expr :: PmExpr
expr = HsExpr GhcTc -> PmExpr
hsExprToPmExpr HsExpr GhcTc
e

-- | Create a term equality of the form: `(False ~ (x ~ lit))`
mkNegEq :: Id -> PmLit -> ComplexEq
mkNegEq :: TyVar -> PmLit -> ComplexEq
mkNegEq x :: TyVar
x l :: PmLit
l = (PmExpr
falsePmExpr, Name -> PmExpr
PmExprVar (TyVar -> Name
idName TyVar
x) PmExpr -> PmExpr -> PmExpr
`PmExprEq` PmLit -> PmExpr
PmExprLit PmLit
l)
{-# INLINE mkNegEq #-}

-- | Create a term equality of the form: `(x ~ lit)`
mkPosEq :: Id -> PmLit -> ComplexEq
mkPosEq :: TyVar -> PmLit -> ComplexEq
mkPosEq x :: TyVar
x l :: PmLit
l = (Name -> PmExpr
PmExprVar (TyVar -> Name
idName TyVar
x), PmLit -> PmExpr
PmExprLit PmLit
l)
{-# INLINE mkPosEq #-}

-- | Create a term equality of the form: `(x ~ x)`
-- (always discharged by the term oracle)
mkIdEq :: Id -> ComplexEq
mkIdEq :: TyVar -> ComplexEq
mkIdEq x :: TyVar
x = (Name -> PmExpr
PmExprVar Name
name, Name -> PmExpr
PmExprVar Name
name)
  where name :: Name
name = TyVar -> Name
idName TyVar
x
{-# INLINE mkIdEq #-}

-- | Generate a variable pattern of a given type
mkPmVar :: Type -> DsM (PmPat p)
mkPmVar :: Type -> DsM (PmPat p)
mkPmVar ty :: Type
ty = TyVar -> PmPat p
forall (t :: PatTy). TyVar -> PmPat t
PmVar (TyVar -> PmPat p) -> DsM TyVar -> DsM (PmPat p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> DsM TyVar
mkPmId Type
ty
{-# INLINE mkPmVar #-}

-- | Generate many variable patterns, given a list of types
mkPmVars :: [Type] -> DsM PatVec
mkPmVars :: [Type] -> DsM PatVec
mkPmVars tys :: [Type]
tys = (Type -> DsM (PmPat 'PAT)) -> [Type] -> DsM PatVec
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> DsM (PmPat 'PAT)
forall (p :: PatTy). Type -> DsM (PmPat p)
mkPmVar [Type]
tys
{-# INLINE mkPmVars #-}

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

-- | Generate a fresh term variable of a given and return it in two forms:
-- * A variable pattern
-- * A variable expression
mkPmId2Forms :: Type -> DsM (Pattern, LHsExpr GhcTc)
mkPmId2Forms :: Type -> DsM (PmPat 'PAT, LHsExpr GhcTc)
mkPmId2Forms ty :: Type
ty = do
  TyVar
x <- Type -> DsM TyVar
mkPmId Type
ty
  (PmPat 'PAT, LHsExpr GhcTc) -> DsM (PmPat 'PAT, LHsExpr GhcTc)
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar -> PmPat 'PAT
forall (t :: PatTy). TyVar -> PmPat t
PmVar TyVar
x, SrcSpanLess (LHsExpr GhcTc) -> LHsExpr GhcTc
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc (XVar GhcTc -> Located (IdP GhcTc) -> HsExpr GhcTc
forall p. XVar p -> Located (IdP p) -> HsExpr p
HsVar XVar GhcTc
NoExt
noExt (SrcSpanLess (Located TyVar) -> Located TyVar
forall a. HasSrcSpan a => SrcSpanLess a -> a
noLoc SrcSpanLess (Located TyVar)
TyVar
x)))

-- ----------------------------------------------------------------------------
-- * Converting between Value Abstractions, Patterns and PmExpr

-- | Convert a value abstraction an expression
vaToPmExpr :: ValAbs -> PmExpr
vaToPmExpr :: PmPat 'VA -> PmExpr
vaToPmExpr (PmCon  { pm_con_con :: forall (t :: PatTy). PmPat t -> ConLike
pm_con_con = ConLike
c, pm_con_args :: forall (t :: PatTy). PmPat t -> [PmPat t]
pm_con_args = [PmPat 'VA]
ps })
  = ConLike -> [PmExpr] -> PmExpr
PmExprCon ConLike
c ((PmPat 'VA -> PmExpr) -> [PmPat 'VA] -> [PmExpr]
forall a b. (a -> b) -> [a] -> [b]
map PmPat 'VA -> PmExpr
vaToPmExpr [PmPat 'VA]
ps)
vaToPmExpr (PmVar  { pm_var_id :: forall (t :: PatTy). PmPat t -> TyVar
pm_var_id  = TyVar
x }) = Name -> PmExpr
PmExprVar (TyVar -> Name
idName TyVar
x)
vaToPmExpr (PmLit  { pm_lit_lit :: forall (t :: PatTy). PmPat t -> PmLit
pm_lit_lit = PmLit
l }) = PmLit -> PmExpr
PmExprLit PmLit
l
vaToPmExpr (PmNLit { pm_lit_id :: PmPat 'VA -> TyVar
pm_lit_id  = TyVar
x }) = Name -> PmExpr
PmExprVar (TyVar -> Name
idName TyVar
x)

-- | Convert a pattern vector to a list of value abstractions by dropping the
-- guards (See Note [Translating As Patterns])
coercePatVec :: PatVec -> [ValAbs]
coercePatVec :: PatVec -> [PmPat 'VA]
coercePatVec pv :: PatVec
pv = (PmPat 'PAT -> [PmPat 'VA]) -> PatVec -> [PmPat 'VA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap PmPat 'PAT -> [PmPat 'VA]
coercePmPat PatVec
pv

-- | Convert a pattern to a list of value abstractions (will be either an empty
-- list if the pattern is a guard pattern, or a singleton list in all other
-- cases) by dropping the guards (See Note [Translating As Patterns])
coercePmPat :: Pattern -> [ValAbs]
coercePmPat :: PmPat 'PAT -> [PmPat 'VA]
coercePmPat (PmVar { pm_var_id :: forall (t :: PatTy). PmPat t -> TyVar
pm_var_id  = TyVar
x }) = [PmVar :: forall (t :: PatTy). TyVar -> PmPat t
PmVar { pm_var_id :: TyVar
pm_var_id  = TyVar
x }]
coercePmPat (PmLit { pm_lit_lit :: forall (t :: PatTy). PmPat t -> PmLit
pm_lit_lit = PmLit
l }) = [PmLit :: forall (t :: PatTy). PmLit -> PmPat t
PmLit { pm_lit_lit :: PmLit
pm_lit_lit = PmLit
l }]
coercePmPat (PmCon { pm_con_con :: forall (t :: PatTy). PmPat t -> ConLike
pm_con_con = ConLike
con, pm_con_arg_tys :: forall (t :: PatTy). PmPat t -> [Type]
pm_con_arg_tys = [Type]
arg_tys
                   , pm_con_tvs :: forall (t :: PatTy). PmPat t -> [TyVar]
pm_con_tvs = [TyVar]
tvs, pm_con_dicts :: forall (t :: PatTy). PmPat t -> [TyVar]
pm_con_dicts = [TyVar]
dicts
                   , pm_con_args :: forall (t :: PatTy). PmPat t -> [PmPat t]
pm_con_args = PatVec
args })
  = [PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con  = ConLike
con, pm_con_arg_tys :: [Type]
pm_con_arg_tys = [Type]
arg_tys
           , pm_con_tvs :: [TyVar]
pm_con_tvs  = [TyVar]
tvs, pm_con_dicts :: [TyVar]
pm_con_dicts = [TyVar]
dicts
           , pm_con_args :: [PmPat 'VA]
pm_con_args = PatVec -> [PmPat 'VA]
coercePatVec PatVec
args }]
coercePmPat (PmGrd {}) = [] -- drop the guards

-- | Check whether a data constructor is the only way to construct
-- a data type.
singleConstructor :: ConLike -> Bool
singleConstructor :: ConLike -> Bool
singleConstructor (RealDataCon dc :: DataCon
dc) =
  case TyCon -> [DataCon]
tyConDataCons (DataCon -> TyCon
dataConTyCon DataCon
dc) of
    [_] -> Bool
True
    _   -> Bool
False
singleConstructor _ = Bool
False

-- | For a given conlike, finds all the sets of patterns which could
-- be relevant to that conlike by consulting the result type.
--
-- These come from two places.
--  1. From data constructors defined with the result type constructor.
--  2. From `COMPLETE` pragmas which have the same type as the result
--     type constructor. Note that we only use `COMPLETE` pragmas
--     *all* of whose pattern types match. See #14135
allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
allCompleteMatches :: ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
allCompleteMatches cl :: ConLike
cl tys :: [Type]
tys = do
  let fam :: [(Provenance, [ConLike])]
fam = case ConLike
cl of
           RealDataCon dc :: DataCon
dc ->
            [(Provenance
FromBuiltin, (DataCon -> ConLike) -> [DataCon] -> [ConLike]
forall a b. (a -> b) -> [a] -> [b]
map DataCon -> ConLike
RealDataCon (TyCon -> [DataCon]
tyConDataCons (DataCon -> TyCon
dataConTyCon DataCon
dc)))]
           PatSynCon _    -> []
      ty :: Type
ty  = ConLike -> [Type] -> Type
conLikeResTy ConLike
cl [Type]
tys
  [CompleteMatch]
pragmas <- case HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty of
               Just (tc :: TyCon
tc, _) -> TyCon -> DsM [CompleteMatch]
dsGetCompleteMatches TyCon
tc
               Nothing      -> [CompleteMatch] -> DsM [CompleteMatch]
forall (m :: * -> *) a. Monad m => a -> m a
return []
  let fams :: CompleteMatch
-> IOEnv (Env DsGblEnv DsLclEnv) (Provenance, [ConLike])
fams cm :: CompleteMatch
cm = (Provenance
FromComplete,) ([ConLike] -> (Provenance, [ConLike]))
-> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
-> IOEnv (Env DsGblEnv DsLclEnv) (Provenance, [ConLike])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                (Name -> IOEnv (Env DsGblEnv DsLclEnv) ConLike)
-> [Name] -> IOEnv (Env DsGblEnv DsLclEnv) [ConLike]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Name -> IOEnv (Env DsGblEnv DsLclEnv) ConLike
dsLookupConLike (CompleteMatch -> [Name]
completeMatchConLikes CompleteMatch
cm)
  [(Provenance, [ConLike])]
from_pragma <- ((Provenance, [ConLike]) -> Bool)
-> [(Provenance, [ConLike])] -> [(Provenance, [ConLike])]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(_,m :: [ConLike]
m) -> Type -> [ConLike] -> Bool
isValidCompleteMatch Type
ty [ConLike]
m) ([(Provenance, [ConLike])] -> [(Provenance, [ConLike])])
-> DsM [(Provenance, [ConLike])] -> DsM [(Provenance, [ConLike])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                (CompleteMatch
 -> IOEnv (Env DsGblEnv DsLclEnv) (Provenance, [ConLike]))
-> [CompleteMatch] -> DsM [(Provenance, [ConLike])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CompleteMatch
-> IOEnv (Env DsGblEnv DsLclEnv) (Provenance, [ConLike])
fams [CompleteMatch]
pragmas
  let final_groups :: [(Provenance, [ConLike])]
final_groups = [(Provenance, [ConLike])]
fam [(Provenance, [ConLike])]
-> [(Provenance, [ConLike])] -> [(Provenance, [ConLike])]
forall a. [a] -> [a] -> [a]
++ [(Provenance, [ConLike])]
from_pragma
  [(Provenance, [ConLike])] -> DsM [(Provenance, [ConLike])]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Provenance, [ConLike])]
final_groups
    where
      -- Check that all the pattern synonym return types in a `COMPLETE`
      -- pragma subsume the type we're matching.
      -- See Note [Filtering out non-matching COMPLETE sets]
      isValidCompleteMatch :: Type -> [ConLike] -> Bool
      isValidCompleteMatch :: Type -> [ConLike] -> Bool
isValidCompleteMatch ty :: Type
ty = (ConLike -> Bool) -> [ConLike] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ConLike -> Bool
go
        where
          go :: ConLike -> Bool
go (RealDataCon {}) = Bool
True
          go (PatSynCon psc :: PatSyn
psc)  = Maybe TCvSubst -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TCvSubst -> Bool) -> Maybe TCvSubst -> Bool
forall a b. (a -> b) -> a -> b
$ (Type -> Type -> Maybe TCvSubst) -> Type -> Type -> Maybe TCvSubst
forall a b c. (a -> b -> c) -> b -> a -> c
flip Type -> Type -> Maybe TCvSubst
tcMatchTy Type
ty (Type -> Maybe TCvSubst) -> Type -> Maybe TCvSubst
forall a b. (a -> b) -> a -> b
$ ([TyVar], [Type], [TyVar], [Type], [Type], Type) -> Type
forall a b c d e f. (a, b, c, d, e, f) -> f
patSynResTy
                                       (([TyVar], [Type], [TyVar], [Type], [Type], Type) -> Type)
-> ([TyVar], [Type], [TyVar], [Type], [Type], Type) -> Type
forall a b. (a -> b) -> a -> b
$ PatSyn -> ([TyVar], [Type], [TyVar], [Type], [Type], Type)
patSynSig PatSyn
psc

          patSynResTy :: (a, b, c, d, e, f) -> f
patSynResTy (_, _, _, _, _, res_ty :: f
res_ty) = f
res_ty

{-
Note [Filtering out non-matching COMPLETE sets]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Currently, conlikes in a COMPLETE set are simply grouped by the
type constructor heading the return type. This is nice and simple, but it does
mean that there are scenarios when a COMPLETE set might be incompatible with
the type of a scrutinee. For instance, consider (from #14135):

  data Foo a = Foo1 a | Foo2 a

  pattern MyFoo2 :: Int -> Foo Int
  pattern MyFoo2 i = Foo2 i

  {-# COMPLETE Foo1, MyFoo2 #-}

  f :: Foo a -> a
  f (Foo1 x) = x

`f` has an incomplete pattern-match, so when choosing which constructors to
report as unmatched in a warning, GHC must choose between the original set of
data constructors {Foo1, Foo2} and the COMPLETE set {Foo1, MyFoo2}. But observe
that GHC shouldn't even consider the COMPLETE set as a possibility: the return
type of MyFoo2, Foo Int, does not match the type of the scrutinee, Foo a, since
there's no substitution `s` such that s(Foo Int) = Foo a.

To ensure that GHC doesn't pick this COMPLETE set, it checks each pattern
synonym constructor's return type matches the type of the scrutinee, and if one
doesn't, then we remove the whole COMPLETE set from consideration.

One might wonder why GHC only checks /pattern synonym/ constructors, and not
/data/ constructors as well. The reason is because that the type of a
GADT constructor very well may not match the type of a scrutinee, and that's
OK. Consider this example (from #14059):

  data SBool (z :: Bool) where
    SFalse :: SBool False
    STrue  :: SBool True

  pattern STooGoodToBeTrue :: forall (z :: Bool). ()
                           => z ~ True
                           => SBool z
  pattern STooGoodToBeTrue = STrue
  {-# COMPLETE SFalse, STooGoodToBeTrue #-}

  wobble :: SBool z -> Bool
  wobble STooGoodToBeTrue = True

In the incomplete pattern match for `wobble`, we /do/ want to warn that SFalse
should be matched against, even though its type, SBool False, does not match
the scrutinee type, SBool z.
-}

-- -----------------------------------------------------------------------
-- * Types and constraints

newEvVar :: Name -> Type -> EvVar
newEvVar :: Name -> Type -> TyVar
newEvVar name :: Name
name ty :: Type
ty = Name -> Type -> TyVar
mkLocalId Name
name Type
ty

nameType :: String -> Type -> DsM EvVar
nameType :: String -> Type -> DsM TyVar
nameType name :: String
name ty :: Type
ty = do
  Unique
unique <- IOEnv (Env DsGblEnv DsLclEnv) Unique
forall (m :: * -> *). MonadUnique m => m Unique
getUniqueM
  let occname :: OccName
occname = FastString -> OccName
mkVarOccFS (String -> FastString
fsLit (String
nameString -> ShowS
forall a. [a] -> [a] -> [a]
++"_"String -> ShowS
forall a. [a] -> [a] -> [a]
++Unique -> String
forall a. Show a => a -> String
show Unique
unique))
      idname :: Name
idname  = Unique -> OccName -> SrcSpan -> Name
mkInternalName Unique
unique OccName
occname SrcSpan
noSrcSpan
  TyVar -> DsM TyVar
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type -> TyVar
newEvVar Name
idname Type
ty)

{-
%************************************************************************
%*                                                                      *
                              The type oracle
%*                                                                      *
%************************************************************************
-}

-- | Check whether a set of type constraints is satisfiable.
tyOracle :: Bag EvVar -> PmM Bool
tyOracle :: Bag TyVar -> PmM Bool
tyOracle evs :: Bag TyVar
evs
  = DsM Bool -> PmM Bool
forall a. DsM a -> PmM a
liftD (DsM Bool -> PmM Bool) -> DsM Bool -> PmM Bool
forall a b. (a -> b) -> a -> b
$
    do { ((_warns :: WarningMessages
_warns, errs :: WarningMessages
errs), res :: Maybe Bool
res) <- TcM Bool -> DsM (Messages, Maybe Bool)
forall a. TcM a -> DsM (Messages, Maybe a)
initTcDsForSolver (TcM Bool -> DsM (Messages, Maybe Bool))
-> TcM Bool -> DsM (Messages, Maybe Bool)
forall a b. (a -> b) -> a -> b
$ Bag TyVar -> TcM Bool
tcCheckSatisfiability Bag TyVar
evs
       ; case Maybe Bool
res of
            Just sat :: Bool
sat -> Bool -> DsM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
sat
            Nothing  -> String -> SDoc -> DsM Bool
forall a. HasCallStack => String -> SDoc -> a
pprPanic "tyOracle" ([SDoc] -> SDoc
vcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ WarningMessages -> [SDoc]
pprErrMsgBagWithLoc WarningMessages
errs) }

{-
%************************************************************************
%*                                                                      *
                             Sanity Checks
%*                                                                      *
%************************************************************************
-}

-- | The arity of a pattern/pattern vector is the
-- number of top-level patterns that are not guards
type PmArity = Int

-- | Compute the arity of a pattern vector
patVecArity :: PatVec -> PmArity
patVecArity :: PatVec -> Int
patVecArity = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> (PatVec -> [Int]) -> PatVec -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PmPat 'PAT -> Int) -> PatVec -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map PmPat 'PAT -> Int
patternArity

-- | Compute the arity of a pattern
patternArity :: Pattern -> PmArity
patternArity :: PmPat 'PAT -> Int
patternArity (PmGrd {}) = 0
patternArity _other_pat :: PmPat 'PAT
_other_pat = 1

{-
%************************************************************************
%*                                                                      *
            Heart of the algorithm: Function pmcheck
%*                                                                      *
%************************************************************************

Main functions are:

* mkInitialUncovered :: [Id] -> PmM Uncovered

  Generates the initial uncovered set. Term and type constraints in scope
  are checked, if they are inconsistent, the set is empty, otherwise, the
  set contains only a vector of variables with the constraints in scope.

* pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult

  Checks redundancy, coverage and inaccessibility, using auxilary functions
  `pmcheckGuards` and `pmcheckHd`. Mainly handles the guard case which is
  common in all three checks (see paper) and calls `pmcheckGuards` when the
  whole clause is checked, or `pmcheckHd` when the pattern vector does not
  start with a guard.

* pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult

  Processes the guards.

* pmcheckHd :: Pattern -> PatVec -> [PatVec]
          -> ValAbs -> ValVec -> PmM PartialResult

  Worker: This function implements functions `covered`, `uncovered` and
  `divergent` from the paper at once. Slightly different from the paper because
  it does not even produce the covered and uncovered sets. Since we only care
  about whether a clause covers SOMETHING or if it may forces ANY argument, we
  only store a boolean in both cases, for efficiency.
-}

-- | Lift a pattern matching action from a single value vector abstration to a
-- value set abstraction, but calling it on every vector and the combining the
-- results.
runMany :: (ValVec -> PmM PartialResult) -> (Uncovered -> PmM PartialResult)
runMany :: (ValVec -> PmM PartialResult) -> Uncovered -> PmM PartialResult
runMany _ [] = PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return PartialResult
forall a. Monoid a => a
mempty
runMany pm :: ValVec -> PmM PartialResult
pm (m :: ValVec
m:ms :: Uncovered
ms) = PartialResult -> PartialResult -> PartialResult
forall a. Monoid a => a -> a -> a
mappend (PartialResult -> PartialResult -> PartialResult)
-> PmM PartialResult -> ListT DsM (PartialResult -> PartialResult)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ValVec -> PmM PartialResult
pm ValVec
m ListT DsM (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (ValVec -> PmM PartialResult) -> Uncovered -> PmM PartialResult
runMany ValVec -> PmM PartialResult
pm Uncovered
ms

-- | Generate the initial uncovered set. It initializes the
-- delta with all term and type constraints in scope.
mkInitialUncovered :: [Id] -> PmM Uncovered
mkInitialUncovered :: [TyVar] -> PmM Uncovered
mkInitialUncovered vars :: [TyVar]
vars = do
  Delta
delta <- PmM Delta
pmInitialTmTyCs
  let patterns :: [PmPat 'VA]
patterns = (TyVar -> PmPat 'VA) -> [TyVar] -> [PmPat 'VA]
forall a b. (a -> b) -> [a] -> [b]
map TyVar -> PmPat 'VA
forall (t :: PatTy). TyVar -> PmPat t
PmVar [TyVar]
vars
  Uncovered -> PmM Uncovered
forall (m :: * -> *) a. Monad m => a -> m a
return [[PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
patterns Delta
delta]

-- | Increase the counter for elapsed algorithm iterations, check that the
-- limit is not exceeded and call `pmcheck`
pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI ps :: PatVec
ps guards :: [PatVec]
guards vva :: ValVec
vva = do
  Int
n <- DsM Int -> PmM Int
forall a. DsM a -> PmM a
liftD DsM Int
incrCheckPmIterDs
  String -> SDoc -> PmM ()
tracePm "pmCheck" (Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> PatVec -> SDoc
pprPatVec PatVec
ps
                        SDoc -> SDoc -> SDoc
$$ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "guards:") 2 ([SDoc] -> SDoc
vcat ((PatVec -> SDoc) -> [PatVec] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map PatVec -> SDoc
pprPatVec [PatVec]
guards))
                        SDoc -> SDoc -> SDoc
$$ ValVec -> SDoc
pprValVecDebug ValVec
vva)
  PartialResult
res <- PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheck PatVec
ps [PatVec]
guards ValVec
vva
  String -> SDoc -> PmM ()
tracePm "pmCheckResult:" (PartialResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr PartialResult
res)
  PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return PartialResult
res
{-# INLINE pmcheckI #-}

-- | Increase the counter for elapsed algorithm iterations, check that the
-- limit is not exceeded and call `pmcheckGuards`
pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
pmcheckGuardsI :: [PatVec] -> ValVec -> PmM PartialResult
pmcheckGuardsI gvs :: [PatVec]
gvs vva :: ValVec
vva = DsM Int -> PmM Int
forall a. DsM a -> PmM a
liftD DsM Int
incrCheckPmIterDs PmM Int -> PmM PartialResult -> PmM PartialResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [PatVec] -> ValVec -> PmM PartialResult
pmcheckGuards [PatVec]
gvs ValVec
vva
{-# INLINE pmcheckGuardsI #-}

-- | Increase the counter for elapsed algorithm iterations, check that the
-- limit is not exceeded and call `pmcheckHd`
pmcheckHdI :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
           -> PmM PartialResult
pmcheckHdI :: PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHdI p :: PmPat 'PAT
p ps :: PatVec
ps guards :: [PatVec]
guards va :: PmPat 'VA
va vva :: ValVec
vva = do
  Int
n <- DsM Int -> PmM Int
forall a. DsM a -> PmM a
liftD DsM Int
incrCheckPmIterDs
  String -> SDoc -> PmM ()
tracePm "pmCheckHdI" (Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> PmPat 'PAT -> SDoc
forall (a :: PatTy). PmPat a -> SDoc
pprPmPatDebug PmPat 'PAT
p
                        SDoc -> SDoc -> SDoc
$$ PatVec -> SDoc
pprPatVec PatVec
ps
                        SDoc -> SDoc -> SDoc
$$ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "guards:") 2 ([SDoc] -> SDoc
vcat ((PatVec -> SDoc) -> [PatVec] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map PatVec -> SDoc
pprPatVec [PatVec]
guards))
                        SDoc -> SDoc -> SDoc
$$ PmPat 'VA -> SDoc
forall (a :: PatTy). PmPat a -> SDoc
pprPmPatDebug PmPat 'VA
va
                        SDoc -> SDoc -> SDoc
$$ ValVec -> SDoc
pprValVecDebug ValVec
vva)

  PartialResult
res <- PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHd PmPat 'PAT
p PatVec
ps [PatVec]
guards PmPat 'VA
va ValVec
vva
  String -> SDoc -> PmM ()
tracePm "pmCheckHdI: res" (PartialResult -> SDoc
forall a. Outputable a => a -> SDoc
ppr PartialResult
res)
  PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return PartialResult
res
{-# INLINE pmcheckHdI #-}

-- | Matching function: Check simultaneously a clause (takes separately the
-- patterns and the list of guards) for exhaustiveness, redundancy and
-- inaccessibility.
pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheck :: PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheck [] guards :: [PatVec]
guards vva :: ValVec
vva@(ValVec [] _)
  | [PatVec] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PatVec]
guards = PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PartialResult -> PmM PartialResult)
-> PartialResult -> PmM PartialResult
forall a b. (a -> b) -> a -> b
$ PartialResult
forall a. Monoid a => a
mempty { presultCovered :: Covered
presultCovered = Covered
Covered }
  | Bool
otherwise   = [PatVec] -> ValVec -> PmM PartialResult
pmcheckGuardsI [PatVec]
guards ValVec
vva

-- Guard
pmcheck (p :: PmPat 'PAT
p@(PmGrd pv :: PatVec
pv e :: PmExpr
e) : ps :: PatVec
ps) guards :: [PatVec]
guards vva :: ValVec
vva@(ValVec vas :: [PmPat 'VA]
vas delta :: Delta
delta)
    -- short-circuit if the guard pattern is useless.
    -- we just have two possible outcomes: fail here or match and recurse
    -- none of the two contains any useful information about the failure
    -- though. So just have these two cases but do not do all the boilerplate
  | PatVec -> PmExpr -> Bool
isFakeGuard PatVec
pv PmExpr
e = PartialResult -> PartialResult
forces (PartialResult -> PartialResult)
-> (PartialResult -> PartialResult)
-> PartialResult
-> PartialResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValVec -> PartialResult -> PartialResult
mkCons ValVec
vva (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI PatVec
ps [PatVec]
guards ValVec
vva
  | Bool
otherwise = do
      TyVar
y <- DsM TyVar -> PmM TyVar
forall a. DsM a -> PmM a
liftD (DsM TyVar -> PmM TyVar) -> DsM TyVar -> PmM TyVar
forall a b. (a -> b) -> a -> b
$ Type -> DsM TyVar
mkPmId (PmPat 'PAT -> Type
forall (p :: PatTy). PmPat p -> Type
pmPatType PmPat 'PAT
p)
      let tm_state :: TmState
tm_state = TyVar -> PmExpr -> TmState -> TmState
extendSubst TyVar
y PmExpr
e (Delta -> TmState
delta_tm_cs Delta
delta)
          delta' :: Delta
delta'   = Delta
delta { delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state }
      PartialResult -> PartialResult
utail (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI (PatVec
pv PatVec -> PatVec -> PatVec
forall a. [a] -> [a] -> [a]
++ PatVec
ps) [PatVec]
guards ([PmPat 'VA] -> Delta -> ValVec
ValVec (TyVar -> PmPat 'VA
forall (t :: PatTy). TyVar -> PmPat t
PmVar TyVar
y PmPat 'VA -> [PmPat 'VA] -> [PmPat 'VA]
forall a. a -> [a] -> [a]
: [PmPat 'VA]
vas) Delta
delta')

pmcheck [] _ (ValVec (_:_) _) = String -> PmM PartialResult
forall a. String -> a
panic "pmcheck: nil-cons"
pmcheck (_:_) _ (ValVec [] _) = String -> PmM PartialResult
forall a. String -> a
panic "pmcheck: cons-nil"

pmcheck (p :: PmPat 'PAT
p:ps :: PatVec
ps) guards :: [PatVec]
guards (ValVec (va :: PmPat 'VA
va:vva :: [PmPat 'VA]
vva) delta :: Delta
delta)
  = PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHdI PmPat 'PAT
p PatVec
ps [PatVec]
guards PmPat 'VA
va ([PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
vva Delta
delta)

-- | Check the list of guards
pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
pmcheckGuards :: [PatVec] -> ValVec -> PmM PartialResult
pmcheckGuards []       vva :: ValVec
vva = PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Uncovered -> PartialResult
usimple [ValVec
vva])
pmcheckGuards (gv :: PatVec
gv:gvs :: [PatVec]
gvs) vva :: ValVec
vva = do
  (PartialResult prov1 :: Provenance
prov1 cs :: Covered
cs vsa :: Uncovered
vsa ds :: Diverged
ds) <- PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI PatVec
gv [] ValVec
vva
  (PartialResult prov2 :: Provenance
prov2 css :: Covered
css vsas :: Uncovered
vsas dss :: Diverged
dss) <- (ValVec -> PmM PartialResult) -> Uncovered -> PmM PartialResult
runMany ([PatVec] -> ValVec -> PmM PartialResult
pmcheckGuardsI [PatVec]
gvs) Uncovered
vsa
  PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PartialResult -> PmM PartialResult)
-> PartialResult -> PmM PartialResult
forall a b. (a -> b) -> a -> b
$ Provenance -> Covered -> Uncovered -> Diverged -> PartialResult
PartialResult (Provenance
prov1 Provenance -> Provenance -> Provenance
forall a. Monoid a => a -> a -> a
`mappend` Provenance
prov2)
                         (Covered
cs Covered -> Covered -> Covered
forall a. Monoid a => a -> a -> a
`mappend` Covered
css)
                         Uncovered
vsas
                         (Diverged
ds Diverged -> Diverged -> Diverged
forall a. Monoid a => a -> a -> a
`mappend` Diverged
dss)

-- | Worker function: Implements all cases described in the paper for all three
-- functions (`covered`, `uncovered` and `divergent`) apart from the `Guard`
-- cases which are handled by `pmcheck`
pmcheckHd :: Pattern -> PatVec -> [PatVec] -> ValAbs -> ValVec
          -> PmM PartialResult

-- Var
pmcheckHd :: PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHd (PmVar x :: TyVar
x) ps :: PatVec
ps guards :: [PatVec]
guards va :: PmPat 'VA
va (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta)
  | Just tm_state :: TmState
tm_state <- TmState -> ComplexEq -> Maybe TmState
solveOneEq (Delta -> TmState
delta_tm_cs Delta
delta)
                                (Name -> PmExpr
PmExprVar (TyVar -> Name
idName TyVar
x), PmPat 'VA -> PmExpr
vaToPmExpr PmPat 'VA
va)
  = PmPat 'VA -> PartialResult -> PartialResult
ucon PmPat 'VA
va (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI PatVec
ps [PatVec]
guards ([PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
vva (Delta
delta {delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state}))
  | Bool
otherwise = PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return PartialResult
forall a. Monoid a => a
mempty

-- ConCon
pmcheckHd ( p :: PmPat 'PAT
p@(PmCon { pm_con_con :: forall (t :: PatTy). PmPat t -> ConLike
pm_con_con = ConLike
c1, pm_con_tvs :: forall (t :: PatTy). PmPat t -> [TyVar]
pm_con_tvs = [TyVar]
ex_tvs1
                     , pm_con_args :: forall (t :: PatTy). PmPat t -> [PmPat t]
pm_con_args = PatVec
args1})) ps :: PatVec
ps guards :: [PatVec]
guards
          (va :: PmPat 'VA
va@(PmCon { pm_con_con :: forall (t :: PatTy). PmPat t -> ConLike
pm_con_con = ConLike
c2, pm_con_tvs :: forall (t :: PatTy). PmPat t -> [TyVar]
pm_con_tvs = [TyVar]
ex_tvs2
                     , pm_con_args :: forall (t :: PatTy). PmPat t -> [PmPat t]
pm_con_args = [PmPat 'VA]
args2})) (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta)
  | ConLike
c1 ConLike -> ConLike -> Bool
forall a. Eq a => a -> a -> Bool
/= ConLike
c2  =
    PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (Uncovered -> PartialResult
usimple [[PmPat 'VA] -> Delta -> ValVec
ValVec (PmPat 'VA
vaPmPat 'VA -> [PmPat 'VA] -> [PmPat 'VA]
forall a. a -> [a] -> [a]
:[PmPat 'VA]
vva) Delta
delta])
  | Bool
otherwise = do
    let to_evvar :: TyVar -> TyVar -> DsM TyVar
to_evvar tv1 :: TyVar
tv1 tv2 :: TyVar
tv2 = String -> Type -> DsM TyVar
nameType "pmConCon" (Type -> DsM TyVar) -> Type -> DsM TyVar
forall a b. (a -> b) -> a -> b
$
                           Type -> Type -> Type
mkPrimEqPred (TyVar -> Type
mkTyVarTy TyVar
tv1) (TyVar -> Type
mkTyVarTy TyVar
tv2)
        mb_to_evvar :: TyVar -> TyVar -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe TyVar)
mb_to_evvar tv1 :: TyVar
tv1 tv2 :: TyVar
tv2
            -- If we have identical constructors but different existential
            -- tyvars, then generate extra equality constraints to ensure the
            -- existential tyvars.
            -- See Note [Coverage checking and existential tyvars].
          | TyVar
tv1 TyVar -> TyVar -> Bool
forall a. Eq a => a -> a -> Bool
== TyVar
tv2 = Maybe TyVar -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe TyVar)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe TyVar
forall a. Maybe a
Nothing
          | Bool
otherwise  = TyVar -> Maybe TyVar
forall a. a -> Maybe a
Just (TyVar -> Maybe TyVar)
-> DsM TyVar -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyVar -> TyVar -> DsM TyVar
to_evvar TyVar
tv1 TyVar
tv2
    Bag TyVar
evvars <- ([TyVar] -> Bag TyVar
forall a. [a] -> Bag a
listToBag ([TyVar] -> Bag TyVar)
-> ([Maybe TyVar] -> [TyVar]) -> [Maybe TyVar] -> Bag TyVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe TyVar] -> [TyVar]
forall a. [Maybe a] -> [a]
catMaybes) ([Maybe TyVar] -> Bag TyVar)
-> ListT DsM [Maybe TyVar] -> PmM (Bag TyVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
              ASSERT(ex_tvs1 `equalLength` ex_tvs2)
              DsM [Maybe TyVar] -> ListT DsM [Maybe TyVar]
forall a. DsM a -> PmM a
liftD ((TyVar -> TyVar -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe TyVar))
-> [TyVar] -> [TyVar] -> DsM [Maybe TyVar]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TyVar -> TyVar -> IOEnv (Env DsGblEnv DsLclEnv) (Maybe TyVar)
mb_to_evvar [TyVar]
ex_tvs1 [TyVar]
ex_tvs2)
    let delta' :: Delta
delta' = Delta
delta { delta_ty_cs :: Bag TyVar
delta_ty_cs = Bag TyVar
evvars Bag TyVar -> Bag TyVar -> Bag TyVar
forall a. Bag a -> Bag a -> Bag a
`unionBags` Delta -> Bag TyVar
delta_ty_cs Delta
delta }
    ConLike
-> [Type] -> [TyVar] -> [TyVar] -> PartialResult -> PartialResult
kcon ConLike
c1 (PmPat 'PAT -> [Type]
forall (t :: PatTy). PmPat t -> [Type]
pm_con_arg_tys PmPat 'PAT
p) (PmPat 'PAT -> [TyVar]
forall (t :: PatTy). PmPat t -> [TyVar]
pm_con_tvs PmPat 'PAT
p) (PmPat 'PAT -> [TyVar]
forall (t :: PatTy). PmPat t -> [TyVar]
pm_con_dicts PmPat 'PAT
p)
      (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI (PatVec
args1 PatVec -> PatVec -> PatVec
forall a. [a] -> [a] -> [a]
++ PatVec
ps) [PatVec]
guards ([PmPat 'VA] -> Delta -> ValVec
ValVec ([PmPat 'VA]
args2 [PmPat 'VA] -> [PmPat 'VA] -> [PmPat 'VA]
forall a. [a] -> [a] -> [a]
++ [PmPat 'VA]
vva) Delta
delta')

-- LitLit
pmcheckHd (PmLit l1 :: PmLit
l1) ps :: PatVec
ps guards :: [PatVec]
guards (va :: PmPat 'VA
va@(PmLit l2 :: PmLit
l2)) vva :: ValVec
vva =
  case PmLit -> PmLit -> Bool
eqPmLit PmLit
l1 PmLit
l2 of
    True  -> PmPat 'VA -> PartialResult -> PartialResult
ucon PmPat 'VA
va (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI PatVec
ps [PatVec]
guards ValVec
vva
    False -> PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return (PartialResult -> PmM PartialResult)
-> PartialResult -> PmM PartialResult
forall a b. (a -> b) -> a -> b
$ PmPat 'VA -> PartialResult -> PartialResult
ucon PmPat 'VA
va (Uncovered -> PartialResult
usimple [ValVec
vva])

-- ConVar
pmcheckHd (p :: PmPat 'PAT
p@(PmCon { pm_con_con :: forall (t :: PatTy). PmPat t -> ConLike
pm_con_con = ConLike
con, pm_con_arg_tys :: forall (t :: PatTy). PmPat t -> [Type]
pm_con_arg_tys = [Type]
tys }))
          ps :: PatVec
ps guards :: [PatVec]
guards
          (PmVar x :: TyVar
x) (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta) = do
  (prov :: Provenance
prov, complete_match :: [ConLike]
complete_match) <- [(Provenance, [ConLike])] -> ListT DsM (Provenance, [ConLike])
forall (m :: * -> *) a. Monad m => [a] -> ListT m a
select ([(Provenance, [ConLike])] -> ListT DsM (Provenance, [ConLike]))
-> ListT DsM [(Provenance, [ConLike])]
-> ListT DsM (Provenance, [ConLike])
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< DsM [(Provenance, [ConLike])]
-> ListT DsM [(Provenance, [ConLike])]
forall a. DsM a -> PmM a
liftD (ConLike -> [Type] -> DsM [(Provenance, [ConLike])]
allCompleteMatches ConLike
con [Type]
tys)

  [InhabitationCandidate]
cons_cs <- (ConLike -> ListT DsM InhabitationCandidate)
-> [ConLike] -> ListT DsM [InhabitationCandidate]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
-> ListT DsM InhabitationCandidate
forall a. DsM a -> PmM a
liftD (IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
 -> ListT DsM InhabitationCandidate)
-> (ConLike -> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate)
-> ConLike
-> ListT DsM InhabitationCandidate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVar
-> ConLike -> IOEnv (Env DsGblEnv DsLclEnv) InhabitationCandidate
mkOneConFull TyVar
x) [ConLike]
complete_match

  Uncovered
inst_vsa <- ((InhabitationCandidate -> ListT DsM (Maybe ValVec))
 -> [InhabitationCandidate] -> PmM Uncovered)
-> [InhabitationCandidate]
-> (InhabitationCandidate -> ListT DsM (Maybe ValVec))
-> PmM Uncovered
forall a b c. (a -> b -> c) -> b -> a -> c
flip (InhabitationCandidate -> ListT DsM (Maybe ValVec))
-> [InhabitationCandidate] -> PmM Uncovered
forall (m :: * -> *) a b.
Applicative m =>
(a -> m (Maybe b)) -> [a] -> m [b]
mapMaybeM [InhabitationCandidate]
cons_cs ((InhabitationCandidate -> ListT DsM (Maybe ValVec))
 -> PmM Uncovered)
-> (InhabitationCandidate -> ListT DsM (Maybe ValVec))
-> PmM Uncovered
forall a b. (a -> b) -> a -> b
$
      \InhabitationCandidate{ ic_val_abs :: InhabitationCandidate -> PmPat 'VA
ic_val_abs = PmPat 'VA
va, ic_tm_ct :: InhabitationCandidate -> ComplexEq
ic_tm_ct = ComplexEq
tm_ct
                            , ic_ty_cs :: InhabitationCandidate -> Bag TyVar
ic_ty_cs = Bag TyVar
ty_cs
                            , ic_strict_arg_tys :: InhabitationCandidate -> [Type]
ic_strict_arg_tys = [Type]
strict_arg_tys } -> do
    Maybe Delta
mb_sat <- Delta -> ComplexEq -> Bag TyVar -> [Type] -> PmM (Maybe Delta)
pmIsSatisfiable Delta
delta ComplexEq
tm_ct Bag TyVar
ty_cs [Type]
strict_arg_tys
    Maybe ValVec -> ListT DsM (Maybe ValVec)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe ValVec -> ListT DsM (Maybe ValVec))
-> Maybe ValVec -> ListT DsM (Maybe ValVec)
forall a b. (a -> b) -> a -> b
$ (Delta -> ValVec) -> Maybe Delta -> Maybe ValVec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([PmPat 'VA] -> Delta -> ValVec
ValVec (PmPat 'VA
vaPmPat 'VA -> [PmPat 'VA] -> [PmPat 'VA]
forall a. a -> [a] -> [a]
:[PmPat 'VA]
vva)) Maybe Delta
mb_sat

  Provenance -> PartialResult -> PartialResult
set_provenance Provenance
prov (PartialResult -> PartialResult)
-> (PartialResult -> PartialResult)
-> PartialResult
-> PartialResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Bool -> PartialResult -> PartialResult
force_if (Name -> TmState -> Bool
canDiverge (TyVar -> Name
idName TyVar
x) (Delta -> TmState
delta_tm_cs Delta
delta)) (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      (ValVec -> PmM PartialResult) -> Uncovered -> PmM PartialResult
runMany (PatVec -> [PatVec] -> ValVec -> PmM PartialResult
pmcheckI (PmPat 'PAT
pPmPat 'PAT -> PatVec -> PatVec
forall a. a -> [a] -> [a]
:PatVec
ps) [PatVec]
guards) Uncovered
inst_vsa

-- LitVar
pmcheckHd (p :: PmPat 'PAT
p@(PmLit l :: PmLit
l)) ps :: PatVec
ps guards :: [PatVec]
guards (PmVar x :: TyVar
x) (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta)
  = Bool -> PartialResult -> PartialResult
force_if (Name -> TmState -> Bool
canDiverge (TyVar -> Name
idName TyVar
x) (Delta -> TmState
delta_tm_cs Delta
delta)) (PartialResult -> PartialResult)
-> (PartialResult -> PartialResult)
-> PartialResult
-> PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      PartialResult -> PartialResult -> PartialResult
mkUnion PartialResult
non_matched (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        case TmState -> ComplexEq -> Maybe TmState
solveOneEq (Delta -> TmState
delta_tm_cs Delta
delta) (TyVar -> PmLit -> ComplexEq
mkPosEq TyVar
x PmLit
l) of
          Just tm_state :: TmState
tm_state -> PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHdI PmPat 'PAT
p PatVec
ps [PatVec]
guards (PmLit -> PmPat 'VA
forall (t :: PatTy). PmLit -> PmPat t
PmLit PmLit
l) (ValVec -> PmM PartialResult) -> ValVec -> PmM PartialResult
forall a b. (a -> b) -> a -> b
$
                             [PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
vva (Delta
delta {delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state})
          Nothing       -> PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return PartialResult
forall a. Monoid a => a
mempty
  where
    us :: Uncovered
us | Just tm_state :: TmState
tm_state <- TmState -> ComplexEq -> Maybe TmState
solveOneEq (Delta -> TmState
delta_tm_cs Delta
delta) (TyVar -> PmLit -> ComplexEq
mkNegEq TyVar
x PmLit
l)
       = [[PmPat 'VA] -> Delta -> ValVec
ValVec (TyVar -> [PmLit] -> PmPat 'VA
PmNLit TyVar
x [PmLit
l] PmPat 'VA -> [PmPat 'VA] -> [PmPat 'VA]
forall a. a -> [a] -> [a]
: [PmPat 'VA]
vva) (Delta
delta { delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state })]
       | Bool
otherwise = []

    non_matched :: PartialResult
non_matched = Uncovered -> PartialResult
usimple Uncovered
us

-- LitNLit
pmcheckHd (p :: PmPat 'PAT
p@(PmLit l :: PmLit
l)) ps :: PatVec
ps guards :: [PatVec]
guards
          (PmNLit { pm_lit_id :: PmPat 'VA -> TyVar
pm_lit_id = TyVar
x, pm_lit_not :: PmPat 'VA -> [PmLit]
pm_lit_not = [PmLit]
lits }) (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta)
  | (PmLit -> Bool) -> [PmLit] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (PmLit -> Bool) -> PmLit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmLit -> PmLit -> Bool
eqPmLit PmLit
l) [PmLit]
lits
  , Just tm_state :: TmState
tm_state <- TmState -> ComplexEq -> Maybe TmState
solveOneEq (Delta -> TmState
delta_tm_cs Delta
delta) (TyVar -> PmLit -> ComplexEq
mkPosEq TyVar
x PmLit
l)
    -- Both guards check the same so it would be sufficient to have only
    -- the second one. Nevertheless, it is much cheaper to check whether
    -- the literal is in the list so we check it first, to avoid calling
    -- the term oracle (`solveOneEq`) if possible
  = PartialResult -> PartialResult -> PartialResult
mkUnion PartialResult
non_matched (PartialResult -> PartialResult)
-> PmM PartialResult -> PmM PartialResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHdI PmPat 'PAT
p PatVec
ps [PatVec]
guards (PmLit -> PmPat 'VA
forall (t :: PatTy). PmLit -> PmPat t
PmLit PmLit
l)
                ([PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
vva (Delta
delta { delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state }))
  | Bool
otherwise = PartialResult -> PmM PartialResult
forall (m :: * -> *) a. Monad m => a -> m a
return PartialResult
non_matched
  where
    us :: Uncovered
us | Just tm_state :: TmState
tm_state <- TmState -> ComplexEq -> Maybe TmState
solveOneEq (Delta -> TmState
delta_tm_cs Delta
delta) (TyVar -> PmLit -> ComplexEq
mkNegEq TyVar
x PmLit
l)
       = [[PmPat 'VA] -> Delta -> ValVec
ValVec (TyVar -> [PmLit] -> PmPat 'VA
PmNLit TyVar
x (PmLit
lPmLit -> [PmLit] -> [PmLit]
forall a. a -> [a] -> [a]
:[PmLit]
lits) PmPat 'VA -> [PmPat 'VA] -> [PmPat 'VA]
forall a. a -> [a] -> [a]
: [PmPat 'VA]
vva) (Delta
delta { delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state })]
       | Bool
otherwise = []

    non_matched :: PartialResult
non_matched = Uncovered -> PartialResult
usimple Uncovered
us

-- ----------------------------------------------------------------------------
-- The following three can happen only in cases like #322 where constructors
-- and overloaded literals appear in the same match. The general strategy is
-- to replace the literal (positive/negative) by a variable and recurse. The
-- fact that the variable is equal to the literal is recorded in `delta` so
-- no information is lost

-- LitCon
pmcheckHd (PmLit l :: PmLit
l) ps :: PatVec
ps guards :: [PatVec]
guards (va :: PmPat 'VA
va@(PmCon {})) (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta)
  = do TyVar
y <- DsM TyVar -> PmM TyVar
forall a. DsM a -> PmM a
liftD (DsM TyVar -> PmM TyVar) -> DsM TyVar -> PmM TyVar
forall a b. (a -> b) -> a -> b
$ Type -> DsM TyVar
mkPmId (PmPat 'VA -> Type
forall (p :: PatTy). PmPat p -> Type
pmPatType PmPat 'VA
va)
       let tm_state :: TmState
tm_state = TyVar -> PmExpr -> TmState -> TmState
extendSubst TyVar
y (PmLit -> PmExpr
PmExprLit PmLit
l) (Delta -> TmState
delta_tm_cs Delta
delta)
           delta' :: Delta
delta'   = Delta
delta { delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state }
       PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHdI (TyVar -> PmPat 'PAT
forall (t :: PatTy). TyVar -> PmPat t
PmVar TyVar
y) PatVec
ps [PatVec]
guards PmPat 'VA
va ([PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
vva Delta
delta')

-- ConLit
pmcheckHd (p :: PmPat 'PAT
p@(PmCon {})) ps :: PatVec
ps guards :: [PatVec]
guards (PmLit l :: PmLit
l) (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta)
  = do TyVar
y <- DsM TyVar -> PmM TyVar
forall a. DsM a -> PmM a
liftD (DsM TyVar -> PmM TyVar) -> DsM TyVar -> PmM TyVar
forall a b. (a -> b) -> a -> b
$ Type -> DsM TyVar
mkPmId (PmPat 'PAT -> Type
forall (p :: PatTy). PmPat p -> Type
pmPatType PmPat 'PAT
p)
       let tm_state :: TmState
tm_state = TyVar -> PmExpr -> TmState -> TmState
extendSubst TyVar
y (PmLit -> PmExpr
PmExprLit PmLit
l) (Delta -> TmState
delta_tm_cs Delta
delta)
           delta' :: Delta
delta'   = Delta
delta { delta_tm_cs :: TmState
delta_tm_cs = TmState
tm_state }
       PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHdI PmPat 'PAT
p PatVec
ps [PatVec]
guards (TyVar -> PmPat 'VA
forall (t :: PatTy). TyVar -> PmPat t
PmVar TyVar
y) ([PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
vva Delta
delta')

-- ConNLit
pmcheckHd (p :: PmPat 'PAT
p@(PmCon {})) ps :: PatVec
ps guards :: [PatVec]
guards (PmNLit { pm_lit_id :: PmPat 'VA -> TyVar
pm_lit_id = TyVar
x }) vva :: ValVec
vva
  = PmPat 'PAT
-> PatVec -> [PatVec] -> PmPat 'VA -> ValVec -> PmM PartialResult
pmcheckHdI PmPat 'PAT
p PatVec
ps [PatVec]
guards (TyVar -> PmPat 'VA
forall (t :: PatTy). TyVar -> PmPat t
PmVar TyVar
x) ValVec
vva

-- Impossible: handled by pmcheck
pmcheckHd (PmGrd {}) _ _ _ _ = String -> PmM PartialResult
forall a. String -> a
panic "pmcheckHd: Guard"

{-
Note [Coverage checking and existential tyvars]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
GHC's implementation of the pattern-match coverage algorithm (as described in
the GADTs Meet Their Match paper) must take some care to emit enough type
constraints when handling data constructors with exisentially quantified type
variables. To better explain what the challenge is, consider a constructor K
of the form:

  K @e_1 ... @e_m ev_1 ... ev_v ty_1 ... ty_n :: T u_1 ... u_p

Where:

* e_1, ..., e_m are the existentially bound type variables.
* ev_1, ..., ev_v are evidence variables, which may inhabit a dictionary type
  (e.g., Eq) or an equality constraint (e.g., e_1 ~ Int).
* ty_1, ..., ty_n are the types of K's fields.
* T u_1 ... u_p is the return type, where T is the data type constructor, and
  u_1, ..., u_p are the universally quantified type variables.

In the ConVar case, the coverage algorithm will have in hand the constructor
K as well as a pattern variable (pv :: T PV_1 ... PV_p), where PV_1, ..., PV_p
are some types that instantiate u_1, ... u_p. The idea is that we should
substitute PV_1 for u_1, ..., and PV_p for u_p when forming a PmCon (the
mkOneConFull function accomplishes this) and then hand this PmCon off to the
ConCon case.

The presence of existentially quantified type variables adds a significant
wrinkle. We always grab e_1, ..., e_m from the definition of K to begin with,
but we don't want them to appear in the final PmCon, because then
calling (mkOneConFull K) for other pattern variables might reuse the same
existential tyvars, which is certainly wrong.

Previously, GHC's solution to this wrinkle was to always create fresh names
for the existential tyvars and put them into the PmCon. This works well for
many cases, but it can break down if you nest GADT pattern matches in just
the right way. For instance, consider the following program:

    data App f a where
      App :: f a -> App f (Maybe a)

    data Ty a where
      TBool :: Ty Bool
      TInt  :: Ty Int

    data T f a where
      C :: T Ty (Maybe Bool)

    foo :: T f a -> App f a -> ()
    foo C (App TBool) = ()

foo is a total program, but with the previous approach to handling existential
tyvars, GHC would mark foo's patterns as non-exhaustive.

When foo is desugared to Core, it looks roughly like so:

    foo @f @a (C co1 _co2) (App @a1 _co3 (TBool |> co1)) = ()

(Where `a1` is an existential tyvar.)

That, in turn, is processed by the coverage checker to become:

    foo @f @a (C co1 _co2) (App @a1 _co3 (pmvar123 :: f a1))
      | TBool <- pmvar123 |> co1
      = ()

Note that the type of pmvar123 is `f a1`—this will be important later.

Now, we proceed with coverage-checking as usual. When we come to the
ConVar case for App, we create a fresh variable `a2` to represent its
existential tyvar. At this point, we have the equality constraints
`(a ~ Maybe a2, a ~ Maybe Bool, f ~ Ty)` in scope.

However, when we check the guard, it will use the type of pmvar123, which is
`f a1`. Thus, when considering if pmvar123 can match the constructor TInt,
it will generate the constraint `a1 ~ Int`. This means our final set of
equality constraints would be:

    f  ~ Ty
    a  ~ Maybe Bool
    a  ~ Maybe a2
    a1 ~ Int

Which is satisfiable! Freshening the existential tyvar `a` to `a2` doomed us,
because GHC is unable to relate `a2` to `a1`, which really should be the same
tyvar.

Luckily, we can avoid this pitfall. Recall that the ConVar case was where we
generated a PmCon with too-fresh existentials. But after ConVar, we have the
ConCon case, which considers whether each constructor of a particular data type
can be matched on in a particular spot.

In the case of App, when we get to the ConCon case, we will compare our
original App PmCon (from the source program) to the App PmCon created from the
ConVar case. In the former PmCon, we have `a1` in hand, which is exactly the
existential tyvar we want! Thus, we can force `a1` to be the same as `a2` here
by emitting an additional `a1 ~ a2` constraint. Now our final set of equality
constraints will be:

    f  ~ Ty
    a  ~ Maybe Bool
    a  ~ Maybe a2
    a1 ~ Int
    a1 ~ a2

Which is unsatisfiable, as we desired, since we now have that
Int ~ a1 ~ a2 ~ Bool.

In general, App might have more than one constructor, in which case we
couldn't reuse the existential tyvar for App for a different constructor. This
means that we can only use this trick in ConCon when the constructors are the
same. But this is fine, since this is the only scenario where this situation
arises in the first place!
-}

-- ----------------------------------------------------------------------------
-- * Utilities for main checking

updateVsa :: (ValSetAbs -> ValSetAbs) -> (PartialResult -> PartialResult)
updateVsa :: (Uncovered -> Uncovered) -> PartialResult -> PartialResult
updateVsa f :: Uncovered -> Uncovered
f p :: PartialResult
p@(PartialResult { presultUncovered :: PartialResult -> Uncovered
presultUncovered = Uncovered
old })
  = PartialResult
p { presultUncovered :: Uncovered
presultUncovered = Uncovered -> Uncovered
f Uncovered
old }


-- | Initialise with default values for covering and divergent information.
usimple :: ValSetAbs -> PartialResult
usimple :: Uncovered -> PartialResult
usimple vsa :: Uncovered
vsa = PartialResult
forall a. Monoid a => a
mempty { presultUncovered :: Uncovered
presultUncovered = Uncovered
vsa }

-- | Take the tail of all value vector abstractions in the uncovered set
utail :: PartialResult -> PartialResult
utail :: PartialResult -> PartialResult
utail = (Uncovered -> Uncovered) -> PartialResult -> PartialResult
updateVsa Uncovered -> Uncovered
upd
  where upd :: Uncovered -> Uncovered
upd vsa :: Uncovered
vsa = [ [PmPat 'VA] -> Delta -> ValVec
ValVec [PmPat 'VA]
vva Delta
delta | ValVec (_:vva :: [PmPat 'VA]
vva) delta :: Delta
delta <- Uncovered
vsa ]

-- | Prepend a value abstraction to all value vector abstractions in the
-- uncovered set
ucon :: ValAbs -> PartialResult -> PartialResult
ucon :: PmPat 'VA -> PartialResult -> PartialResult
ucon va :: PmPat 'VA
va = (Uncovered -> Uncovered) -> PartialResult -> PartialResult
updateVsa Uncovered -> Uncovered
upd
  where
    upd :: Uncovered -> Uncovered
upd vsa :: Uncovered
vsa = [ [PmPat 'VA] -> Delta -> ValVec
ValVec (PmPat 'VA
vaPmPat 'VA -> [PmPat 'VA] -> [PmPat 'VA]
forall a. a -> [a] -> [a]
:[PmPat 'VA]
vva) Delta
delta | ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta <- Uncovered
vsa ]

-- | Given a data constructor of arity `a` and an uncovered set containing
-- value vector abstractions of length `(a+n)`, pass the first `n` value
-- abstractions to the constructor (Hence, the resulting value vector
-- abstractions will have length `n+1`)
kcon :: ConLike -> [Type] -> [TyVar] -> [EvVar]
     -> PartialResult -> PartialResult
kcon :: ConLike
-> [Type] -> [TyVar] -> [TyVar] -> PartialResult -> PartialResult
kcon con :: ConLike
con arg_tys :: [Type]
arg_tys ex_tvs :: [TyVar]
ex_tvs dicts :: [TyVar]
dicts
  = let n :: Int
n = ConLike -> Int
conLikeArity ConLike
con
        upd :: Uncovered -> Uncovered
upd vsa :: Uncovered
vsa =
          [ [PmPat 'VA] -> Delta -> ValVec
ValVec (PmPat 'VA
vaPmPat 'VA -> [PmPat 'VA] -> [PmPat 'VA]
forall a. a -> [a] -> [a]
:[PmPat 'VA]
vva) Delta
delta
          | ValVec vva' :: [PmPat 'VA]
vva' delta :: Delta
delta <- Uncovered
vsa
          , let (args :: [PmPat 'VA]
args, vva :: [PmPat 'VA]
vva) = Int -> [PmPat 'VA] -> ([PmPat 'VA], [PmPat 'VA])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
n [PmPat 'VA]
vva'
          , let va :: PmPat 'VA
va = PmCon :: forall (t :: PatTy).
ConLike -> [Type] -> [TyVar] -> [TyVar] -> [PmPat t] -> PmPat t
PmCon { pm_con_con :: ConLike
pm_con_con     = ConLike
con
                            , pm_con_arg_tys :: [Type]
pm_con_arg_tys = [Type]
arg_tys
                            , pm_con_tvs :: [TyVar]
pm_con_tvs     = [TyVar]
ex_tvs
                            , pm_con_dicts :: [TyVar]
pm_con_dicts   = [TyVar]
dicts
                            , pm_con_args :: [PmPat 'VA]
pm_con_args    = [PmPat 'VA]
args } ]
    in (Uncovered -> Uncovered) -> PartialResult -> PartialResult
updateVsa Uncovered -> Uncovered
upd

-- | Get the union of two covered, uncovered and divergent value set
-- abstractions. Since the covered and divergent sets are represented by a
-- boolean, union means computing the logical or (at least one of the two is
-- non-empty).

mkUnion :: PartialResult -> PartialResult -> PartialResult
mkUnion :: PartialResult -> PartialResult -> PartialResult
mkUnion = PartialResult -> PartialResult -> PartialResult
forall a. Monoid a => a -> a -> a
mappend

-- | Add a value vector abstraction to a value set abstraction (uncovered).
mkCons :: ValVec -> PartialResult -> PartialResult
mkCons :: ValVec -> PartialResult -> PartialResult
mkCons vva :: ValVec
vva = (Uncovered -> Uncovered) -> PartialResult -> PartialResult
updateVsa (ValVec
vvaValVec -> Uncovered -> Uncovered
forall a. a -> [a] -> [a]
:)

-- | Set the divergent set to not empty
forces :: PartialResult -> PartialResult
forces :: PartialResult -> PartialResult
forces pres :: PartialResult
pres = PartialResult
pres { presultDivergent :: Diverged
presultDivergent = Diverged
Diverged }

-- | Set the divergent set to non-empty if the flag is `True`
force_if :: Bool -> PartialResult -> PartialResult
force_if :: Bool -> PartialResult -> PartialResult
force_if True  pres :: PartialResult
pres = PartialResult -> PartialResult
forces PartialResult
pres
force_if False pres :: PartialResult
pres = PartialResult
pres

set_provenance :: Provenance -> PartialResult -> PartialResult
set_provenance :: Provenance -> PartialResult -> PartialResult
set_provenance prov :: Provenance
prov pr :: PartialResult
pr = PartialResult
pr { presultProvenance :: Provenance
presultProvenance = Provenance
prov }

-- ----------------------------------------------------------------------------
-- * Propagation of term constraints inwards when checking nested matches

{- Note [Type and Term Equality Propagation]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking a match it would be great to have all type and term information
available so we can get more precise results. For this reason we have functions
`addDictsDs' and `addTmCsDs' in PmMonad that store in the environment type and
term constraints (respectively) as we go deeper.

The type constraints we propagate inwards are collected by `collectEvVarsPats'
in HsPat.hs. This handles bug #4139 ( see example
  https://ghc.haskell.org/trac/ghc/attachment/ticket/4139/GADTbug.hs )
where this is needed.

For term equalities we do less, we just generate equalities for HsCase. For
example we accurately give 2 redundancy warnings for the marked cases:

f :: [a] -> Bool
f x = case x of

  []    -> case x of        -- brings (x ~ []) in scope
             []    -> True
             (_:_) -> False -- can't happen

  (_:_) -> case x of        -- brings (x ~ (_:_)) in scope
             (_:_) -> True
             []    -> False -- can't happen

Functions `genCaseTmCs1' and `genCaseTmCs2' are responsible for generating
these constraints.
-}

-- | Generate equalities when checking a case expression:
--     case x of { p1 -> e1; ... pn -> en }
-- When we go deeper to check e.g. e1 we record two equalities:
-- (x ~ y), where y is the initial uncovered when checking (p1; .. ; pn)
-- and (x ~ p1).
genCaseTmCs2 :: Maybe (LHsExpr GhcTc) -- Scrutinee
             -> [Pat GhcTc]           -- LHS       (should have length 1)
             -> [Id]                  -- MatchVars (should have length 1)
             -> DsM (Bag SimpleEq)
genCaseTmCs2 :: Maybe (LHsExpr GhcTc)
-> [LPat GhcTc] -> [TyVar] -> DsM (Bag SimpleEq)
genCaseTmCs2 Nothing _ _ = Bag SimpleEq -> DsM (Bag SimpleEq)
forall (m :: * -> *) a. Monad m => a -> m a
return Bag SimpleEq
forall a. Bag a
emptyBag
genCaseTmCs2 (Just scr :: LHsExpr GhcTc
scr) [p :: LPat GhcTc
p] [var :: TyVar
var] = do
  FamInstEnvs
fam_insts <- DsM FamInstEnvs
dsGetFamInstEnvs
  [e :: PmExpr
e] <- (PmPat 'VA -> PmExpr) -> [PmPat 'VA] -> [PmExpr]
forall a b. (a -> b) -> [a] -> [b]
map PmPat 'VA -> PmExpr
vaToPmExpr ([PmPat 'VA] -> [PmExpr])
-> (PatVec -> [PmPat 'VA]) -> PatVec -> [PmExpr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PatVec -> [PmPat 'VA]
coercePatVec (PatVec -> [PmExpr])
-> DsM PatVec -> IOEnv (Env DsGblEnv DsLclEnv) [PmExpr]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FamInstEnvs -> LPat GhcTc -> DsM PatVec
translatePat FamInstEnvs
fam_insts LPat GhcTc
p
  let scr_e :: PmExpr
scr_e = LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
scr
  Bag SimpleEq -> DsM (Bag SimpleEq)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bag SimpleEq -> DsM (Bag SimpleEq))
-> Bag SimpleEq -> DsM (Bag SimpleEq)
forall a b. (a -> b) -> a -> b
$ [SimpleEq] -> Bag SimpleEq
forall a. [a] -> Bag a
listToBag [(TyVar
var, PmExpr
e), (TyVar
var, PmExpr
scr_e)]
genCaseTmCs2 _ _ _ = String -> DsM (Bag SimpleEq)
forall a. String -> a
panic "genCaseTmCs2: HsCase"

-- | Generate a simple equality when checking a case expression:
--     case x of { matches }
-- When checking matches we record that (x ~ y) where y is the initial
-- uncovered. All matches will have to satisfy this equality.
genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [Id] -> Bag SimpleEq
genCaseTmCs1 :: Maybe (LHsExpr GhcTc) -> [TyVar] -> Bag SimpleEq
genCaseTmCs1 Nothing     _    = Bag SimpleEq
forall a. Bag a
emptyBag
genCaseTmCs1 (Just scr :: LHsExpr GhcTc
scr) [var :: TyVar
var] = SimpleEq -> Bag SimpleEq
forall a. a -> Bag a
unitBag (TyVar
var, LHsExpr GhcTc -> PmExpr
lhsExprToPmExpr LHsExpr GhcTc
scr)
genCaseTmCs1 _ _              = String -> Bag SimpleEq
forall a. String -> a
panic "genCaseTmCs1: HsCase"

{- Note [Literals in PmPat]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
Instead of translating a literal to a variable accompanied with a guard, we
treat them like constructor patterns. The following example from
"./libraries/base/GHC/IO/Encoding.hs" shows why:

mkTextEncoding' :: CodingFailureMode -> String -> IO TextEncoding
mkTextEncoding' cfm enc = case [toUpper c | c <- enc, c /= '-'] of
    "UTF8"    -> return $ UTF8.mkUTF8 cfm
    "UTF16"   -> return $ UTF16.mkUTF16 cfm
    "UTF16LE" -> return $ UTF16.mkUTF16le cfm
    ...

Each clause gets translated to a list of variables with an equal number of
guards. For every guard we generate two cases (equals True/equals False) which
means that we generate 2^n cases to feed the oracle with, where n is the sum of
the length of all strings that appear in the patterns. For this particular
example this means over 2^40 cases. Instead, by representing them like with
constructor we get the following:
  1. We exploit the common prefix with our representation of VSAs
  2. We prune immediately non-reachable cases
     (e.g. False == (x == "U"), True == (x == "U"))

Note [Translating As Patterns]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Instead of translating x@p as:  x (p <- x)
we instead translate it as:     p (x <- coercePattern p)
for performance reasons. For example:

  f x@True  = 1
  f y@False = 2

Gives the following with the first translation:

  x |> {x == False, x == y, y == True}

If we use the second translation we get an empty set, independently of the
oracle. Since the pattern `p' may contain guard patterns though, it cannot be
used as an expression. That's why we call `coercePatVec' to drop the guard and
`vaToPmExpr' to transform the value abstraction to an expression in the
guard pattern (value abstractions are a subset of expressions). We keep the
guards in the first pattern `p' though.


%************************************************************************
%*                                                                      *
      Pretty printing of exhaustiveness/redundancy check warnings
%*                                                                      *
%************************************************************************
-}

-- | Check whether any part of pattern match checking is enabled (does not
-- matter whether it is the redundancy check or the exhaustiveness check).
isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
isAnyPmCheckEnabled :: DynFlags -> DsMatchContext -> Bool
isAnyPmCheckEnabled dflags :: DynFlags
dflags (DsMatchContext kind :: HsMatchContext Name
kind _loc :: SrcSpan
_loc)
  = WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnOverlappingPatterns DynFlags
dflags Bool -> Bool -> Bool
|| DynFlags -> HsMatchContext Name -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext Name
kind

instance Outputable ValVec where
  ppr :: ValVec -> SDoc
ppr (ValVec vva :: [PmPat 'VA]
vva delta :: Delta
delta)
    = let (residual_eqs :: [ComplexEq]
residual_eqs, subst :: PmVarEnv
subst) = TmState -> ([ComplexEq], PmVarEnv)
wrapUpTmState (Delta -> TmState
delta_tm_cs Delta
delta)
          vector :: [PmExpr]
vector                = PmVarEnv -> [PmPat 'VA] -> [PmExpr]
substInValAbs PmVarEnv
subst [PmPat 'VA]
vva
      in  ([PmExpr], [ComplexEq]) -> SDoc
ppr_uncovered ([PmExpr]
vector, [ComplexEq]
residual_eqs)

-- | Apply a term substitution to a value vector abstraction. All VAs are
-- transformed to PmExpr (used only before pretty printing).
substInValAbs :: PmVarEnv -> [ValAbs] -> [PmExpr]
substInValAbs :: PmVarEnv -> [PmPat 'VA] -> [PmExpr]
substInValAbs subst :: PmVarEnv
subst = (PmPat 'VA -> PmExpr) -> [PmPat 'VA] -> [PmExpr]
forall a b. (a -> b) -> [a] -> [b]
map (PmVarEnv -> PmExpr -> PmExpr
exprDeepLookup PmVarEnv
subst (PmExpr -> PmExpr) -> (PmPat 'VA -> PmExpr) -> PmPat 'VA -> PmExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PmPat 'VA -> PmExpr
vaToPmExpr)

-- | Wrap up the term oracle's state once solving is complete. Drop any
-- information about unhandled constraints (involving HsExprs) and flatten
-- (height 1) the substitution.
wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
wrapUpTmState :: TmState -> ([ComplexEq], PmVarEnv)
wrapUpTmState (residual :: [ComplexEq]
residual, (_, subst :: PmVarEnv
subst)) = ([ComplexEq]
residual, PmVarEnv -> PmVarEnv
flattenPmVarEnv PmVarEnv
subst)

-- | Issue all the warnings (coverage, exhaustiveness, inaccessibility)
dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
dsPmWarn :: DynFlags -> DsMatchContext -> PmResult -> DsM ()
dsPmWarn dflags :: DynFlags
dflags ctx :: DsMatchContext
ctx@(DsMatchContext kind :: HsMatchContext Name
kind loc :: SrcSpan
loc) pm_result :: PmResult
pm_result
  = Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
flag_i Bool -> Bool -> Bool
|| Bool
flag_u) (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ do
      let exists_r :: Bool
exists_r = Bool
flag_i Bool -> Bool -> Bool
&& [Located [LPat GhcTc]] -> Bool
forall a. [a] -> Bool
notNull [Located [LPat GhcTc]]
redundant Bool -> Bool -> Bool
&& Bool
onlyBuiltin
          exists_i :: Bool
exists_i = Bool
flag_i Bool -> Bool -> Bool
&& [Located [LPat GhcTc]] -> Bool
forall a. [a] -> Bool
notNull [Located [LPat GhcTc]]
inaccessible Bool -> Bool -> Bool
&& Bool
onlyBuiltin Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
is_rec_upd
          exists_u :: Bool
exists_u = Bool
flag_u Bool -> Bool -> Bool
&& (case UncoveredCandidates
uncovered of
                                  TypeOfUncovered   _ -> Bool
True
                                  UncoveredPatterns u :: Uncovered
u -> Uncovered -> Bool
forall a. [a] -> Bool
notNull Uncovered
u)

      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_r (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ [Located [LPat GhcTc]]
-> (Located [LPat GhcTc] -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Located [LPat GhcTc]]
redundant ((Located [LPat GhcTc] -> DsM ()) -> DsM ())
-> (Located [LPat GhcTc] -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(Located [LPat GhcTc]
-> Located (SrcSpanLess (Located [LPat GhcTc]))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L l :: SrcSpan
l q :: SrcSpanLess (Located [LPat GhcTc])
q) -> do
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (WarnReason -> SDoc -> DsM ()
warnDs (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnOverlappingPatterns)
                               ([LPat GhcTc] -> String -> SDoc
pprEqn [LPat GhcTc]
SrcSpanLess (Located [LPat GhcTc])
q "is redundant"))
      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_i (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ [Located [LPat GhcTc]]
-> (Located [LPat GhcTc] -> DsM ()) -> DsM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Located [LPat GhcTc]]
inaccessible ((Located [LPat GhcTc] -> DsM ()) -> DsM ())
-> (Located [LPat GhcTc] -> DsM ()) -> DsM ()
forall a b. (a -> b) -> a -> b
$ \(Located [LPat GhcTc]
-> Located (SrcSpanLess (Located [LPat GhcTc]))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L l :: SrcSpan
l q :: SrcSpanLess (Located [LPat GhcTc])
q) -> do
        SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
l (WarnReason -> SDoc -> DsM ()
warnDs (WarningFlag -> WarnReason
Reason WarningFlag
Opt_WarnOverlappingPatterns)
                               ([LPat GhcTc] -> String -> SDoc
pprEqn [LPat GhcTc]
SrcSpanLess (Located [LPat GhcTc])
q "has inaccessible right hand side"))
      Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
exists_u (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
loc (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ WarnReason -> SDoc -> DsM ()
warnDs WarnReason
flag_u_reason (SDoc -> DsM ()) -> SDoc -> DsM ()
forall a b. (a -> b) -> a -> b
$
        case UncoveredCandidates
uncovered of
          TypeOfUncovered ty :: Type
ty           -> Type -> SDoc
warnEmptyCase Type
ty
          UncoveredPatterns candidates :: Uncovered
candidates -> Uncovered -> SDoc
pprEqns Uncovered
candidates
  where
    PmResult
      { pmresultProvenance :: PmResult -> Provenance
pmresultProvenance = Provenance
prov
      , pmresultRedundant :: PmResult -> [Located [LPat GhcTc]]
pmresultRedundant = [Located [LPat GhcTc]]
redundant
      , pmresultUncovered :: PmResult -> UncoveredCandidates
pmresultUncovered = UncoveredCandidates
uncovered
      , pmresultInaccessible :: PmResult -> [Located [LPat GhcTc]]
pmresultInaccessible = [Located [LPat GhcTc]]
inaccessible } = PmResult
pm_result

    flag_i :: Bool
flag_i = WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnOverlappingPatterns DynFlags
dflags
    flag_u :: Bool
flag_u = DynFlags -> HsMatchContext Name -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext Name
kind
    flag_u_reason :: WarnReason
flag_u_reason = WarnReason
-> (WarningFlag -> WarnReason) -> Maybe WarningFlag -> WarnReason
forall b a. b -> (a -> b) -> Maybe a -> b
maybe WarnReason
NoReason WarningFlag -> WarnReason
Reason (HsMatchContext Name -> Maybe WarningFlag
forall id. HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag HsMatchContext Name
kind)

    is_rec_upd :: Bool
is_rec_upd = case HsMatchContext Name
kind of { RecUpd -> Bool
True; _ -> Bool
False }
       -- See Note [Inaccessible warnings for record updates]

    onlyBuiltin :: Bool
onlyBuiltin = Provenance
prov Provenance -> Provenance -> Bool
forall a. Eq a => a -> a -> Bool
== Provenance
FromBuiltin

    maxPatterns :: Int
maxPatterns = DynFlags -> Int
maxUncoveredPatterns DynFlags
dflags

    -- Print a single clause (for redundant/with-inaccessible-rhs)
    pprEqn :: [LPat GhcTc] -> String -> SDoc
pprEqn q :: [LPat GhcTc]
q txt :: String
txt = Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pp_context Bool
True DsMatchContext
ctx (String -> SDoc
text String
txt) (((SDoc -> SDoc) -> SDoc) -> SDoc)
-> ((SDoc -> SDoc) -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \f :: SDoc -> SDoc
f -> (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
ppr_eqn SDoc -> SDoc
f HsMatchContext Name
kind [LPat GhcTc]
q

    -- Print several clauses (for uncovered clauses)
    pprEqns :: Uncovered -> SDoc
pprEqns qs :: Uncovered
qs = Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pp_context Bool
False DsMatchContext
ctx (String -> SDoc
text "are non-exhaustive") (((SDoc -> SDoc) -> SDoc) -> SDoc)
-> ((SDoc -> SDoc) -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \_ ->
      case Uncovered
qs of -- See #11245
           [ValVec [] _]
                    -> String -> SDoc
text "Guards do not cover entire pattern space"
           _missing :: Uncovered
_missing -> let us :: [SDoc]
us = (ValVec -> SDoc) -> Uncovered -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map ValVec -> SDoc
forall a. Outputable a => a -> SDoc
ppr Uncovered
qs
                       in  SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Patterns not matched:") 4
                                ([SDoc] -> SDoc
vcat (Int -> [SDoc] -> [SDoc]
forall a. Int -> [a] -> [a]
take Int
maxPatterns [SDoc]
us)
                                 SDoc -> SDoc -> SDoc
$$ Int -> [SDoc] -> SDoc
forall a. Int -> [a] -> SDoc
dots Int
maxPatterns [SDoc]
us)

    -- Print a type-annotated wildcard (for non-exhaustive `EmptyCase`s for
    -- which we only know the type and have no inhabitants at hand)
    warnEmptyCase :: Type -> SDoc
warnEmptyCase ty :: Type
ty = Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pp_context Bool
False DsMatchContext
ctx (String -> SDoc
text "are non-exhaustive") (((SDoc -> SDoc) -> SDoc) -> SDoc)
-> ((SDoc -> SDoc) -> SDoc) -> SDoc
forall a b. (a -> b) -> a -> b
$ \_ ->
      SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Patterns not matched:") 4 (SDoc
underscore SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)

{- Note [Inaccessible warnings for record updates]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (Trac #12957)
  data T a where
    T1 :: { x :: Int } -> T Bool
    T2 :: { x :: Int } -> T a
    T3 :: T a

  f :: T Char -> T a
  f r = r { x = 3 }

The desugarer will (conservatively generate a case for T1 even though
it's impossible:
  f r = case r of
          T1 x -> T1 3   -- Inaccessible branch
          T2 x -> T2 3
          _    -> error "Missing"

We don't want to warn about the inaccessible branch because the programmer
didn't put it there!  So we filter out the warning here.
-}

-- | Issue a warning when the predefined number of iterations is exceeded
-- for the pattern match checker
warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
warnPmIters :: DynFlags -> DsMatchContext -> DsM ()
warnPmIters dflags :: DynFlags
dflags (DsMatchContext kind :: HsMatchContext Name
kind loc :: SrcSpan
loc)
  = Bool -> DsM () -> DsM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
flag_i Bool -> Bool -> Bool
|| Bool
flag_u) (DsM () -> DsM ()) -> DsM () -> DsM ()
forall a b. (a -> b) -> a -> b
$ do
      Int
iters <- DynFlags -> Int
maxPmCheckIterations (DynFlags -> Int)
-> IOEnv (Env DsGblEnv DsLclEnv) DynFlags -> DsM Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
      SrcSpan -> DsM () -> DsM ()
forall a. SrcSpan -> DsM a -> DsM a
putSrcSpanDs SrcSpan
loc (WarnReason -> SDoc -> DsM ()
warnDs WarnReason
NoReason (Int -> SDoc
msg Int
iters))
  where
    ctxt :: SDoc
ctxt   = HsMatchContext Name -> SDoc
forall id.
(Outputable (NameOrRdrName id), Outputable id) =>
HsMatchContext id -> SDoc
pprMatchContext HsMatchContext Name
kind
    msg :: Int -> SDoc
msg is :: Int
is = [SDoc] -> SDoc
fsep [ String -> SDoc
text "Pattern match checker exceeded"
                  , SDoc -> SDoc
parens (Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
is), String -> SDoc
text "iterations in", SDoc
ctxt SDoc -> SDoc -> SDoc
<> SDoc
dot
                  , String -> SDoc
text "(Use -fmax-pmcheck-iterations=n"
                  , String -> SDoc
text "to set the maximum number of iterations to n)" ]

    flag_i :: Bool
flag_i = WarningFlag -> DynFlags -> Bool
wopt WarningFlag
Opt_WarnOverlappingPatterns DynFlags
dflags
    flag_u :: Bool
flag_u = DynFlags -> HsMatchContext Name -> Bool
forall id. DynFlags -> HsMatchContext id -> Bool
exhaustive DynFlags
dflags HsMatchContext Name
kind

dots :: Int -> [a] -> SDoc
dots :: Int -> [a] -> SDoc
dots maxPatterns :: Int
maxPatterns qs :: [a]
qs
    | [a]
qs [a] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
maxPatterns = String -> SDoc
text "..."
    | Bool
otherwise                      = SDoc
empty

-- | Check whether the exhaustiveness checker should run (exhaustiveness only)
exhaustive :: DynFlags -> HsMatchContext id -> Bool
exhaustive :: DynFlags -> HsMatchContext id -> Bool
exhaustive  dflags :: DynFlags
dflags = Bool -> (WarningFlag -> Bool) -> Maybe WarningFlag -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (WarningFlag -> DynFlags -> Bool
`wopt` DynFlags
dflags) (Maybe WarningFlag -> Bool)
-> (HsMatchContext id -> Maybe WarningFlag)
-> HsMatchContext id
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsMatchContext id -> Maybe WarningFlag
forall id. HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag

-- | Denotes whether an exhaustiveness check is supported, and if so,
-- via which 'WarningFlag' it's controlled.
-- Returns 'Nothing' if check is not supported.
exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag :: HsMatchContext id -> Maybe WarningFlag
exhaustiveWarningFlag (FunRhs {})   = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag CaseAlt       = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag IfAlt         = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag LambdaExpr    = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompleteUniPatterns
exhaustiveWarningFlag PatBindRhs    = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompleteUniPatterns
exhaustiveWarningFlag PatBindGuards = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatterns
exhaustiveWarningFlag ProcExpr      = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompleteUniPatterns
exhaustiveWarningFlag RecUpd        = WarningFlag -> Maybe WarningFlag
forall a. a -> Maybe a
Just WarningFlag
Opt_WarnIncompletePatternsRecUpd
exhaustiveWarningFlag ThPatSplice   = Maybe WarningFlag
forall a. Maybe a
Nothing
exhaustiveWarningFlag PatSyn        = Maybe WarningFlag
forall a. Maybe a
Nothing
exhaustiveWarningFlag ThPatQuote    = Maybe WarningFlag
forall a. Maybe a
Nothing
exhaustiveWarningFlag (StmtCtxt {}) = Maybe WarningFlag
forall a. Maybe a
Nothing -- Don't warn about incomplete patterns
                                       -- in list comprehensions, pattern guards
                                       -- etc. They are often *supposed* to be
                                       -- incomplete

-- True <==> singular
pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pp_context :: Bool -> DsMatchContext -> SDoc -> ((SDoc -> SDoc) -> SDoc) -> SDoc
pp_context singular :: Bool
singular (DsMatchContext kind :: HsMatchContext Name
kind _loc :: SrcSpan
_loc) msg :: SDoc
msg rest_of_msg_fun :: (SDoc -> SDoc) -> SDoc
rest_of_msg_fun
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
txt SDoc -> SDoc -> SDoc
<+> SDoc
msg,
          [SDoc] -> SDoc
sep [ String -> SDoc
text "In" SDoc -> SDoc -> SDoc
<+> SDoc
ppr_match SDoc -> SDoc -> SDoc
<> Char -> SDoc
char ':'
              , Int -> SDoc -> SDoc
nest 4 ((SDoc -> SDoc) -> SDoc
rest_of_msg_fun SDoc -> SDoc
pref)]]
  where
    txt :: String
txt | Bool
singular  = "Pattern match"
        | Bool
otherwise = "Pattern match(es)"

    (ppr_match :: SDoc
ppr_match, pref :: SDoc -> SDoc
pref)
        = case HsMatchContext Name
kind of
             FunRhs { mc_fun :: forall id. HsMatchContext id -> Located id
mc_fun = (Located Name -> Located (SrcSpanLess (Located Name))
forall a. HasSrcSpan a => a -> Located (SrcSpanLess a)
dL->L _ fun :: SrcSpanLess (Located Name)
fun) }
                  -> (HsMatchContext Name -> SDoc
forall id.
(Outputable (NameOrRdrName id), Outputable id) =>
HsMatchContext id -> SDoc
pprMatchContext HsMatchContext Name
kind, \ pp :: SDoc
pp -> Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr Name
SrcSpanLess (Located Name)
fun SDoc -> SDoc -> SDoc
<+> SDoc
pp)
             _    -> (HsMatchContext Name -> SDoc
forall id.
(Outputable (NameOrRdrName id), Outputable id) =>
HsMatchContext id -> SDoc
pprMatchContext HsMatchContext Name
kind, \ pp :: SDoc
pp -> SDoc
pp)

ppr_pats :: HsMatchContext Name -> [Pat GhcTc] -> SDoc
ppr_pats :: HsMatchContext Name -> [LPat GhcTc] -> SDoc
ppr_pats kind :: HsMatchContext Name
kind pats :: [LPat GhcTc]
pats
  = [SDoc] -> SDoc
sep [[SDoc] -> SDoc
sep ((LPat GhcTc -> SDoc) -> [LPat GhcTc] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map LPat GhcTc -> SDoc
forall a. Outputable a => a -> SDoc
ppr [LPat GhcTc]
pats), HsMatchContext Name -> SDoc
forall id. HsMatchContext id -> SDoc
matchSeparator HsMatchContext Name
kind, String -> SDoc
text "..."]

ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
ppr_eqn :: (SDoc -> SDoc) -> HsMatchContext Name -> [LPat GhcTc] -> SDoc
ppr_eqn prefixF :: SDoc -> SDoc
prefixF kind :: HsMatchContext Name
kind eqn :: [LPat GhcTc]
eqn = SDoc -> SDoc
prefixF (HsMatchContext Name -> [LPat GhcTc] -> SDoc
ppr_pats HsMatchContext Name
kind ((LPat GhcTc -> LPat GhcTc) -> [LPat GhcTc] -> [LPat GhcTc]
forall a b. (a -> b) -> [a] -> [b]
map LPat GhcTc -> LPat GhcTc
forall a. HasSrcSpan a => a -> SrcSpanLess a
unLoc [LPat GhcTc]
eqn))

ppr_constraint :: (SDoc,[PmLit]) -> SDoc
ppr_constraint :: (SDoc, [PmLit]) -> SDoc
ppr_constraint (var :: SDoc
var, lits :: [PmLit]
lits) = SDoc
var SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "is not one of"
                                 SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
braces ((PmLit -> SDoc) -> [PmLit] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas PmLit -> SDoc
forall a. Outputable a => a -> SDoc
ppr [PmLit]
lits)

ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
ppr_uncovered :: ([PmExpr], [ComplexEq]) -> SDoc
ppr_uncovered (expr_vec :: [PmExpr]
expr_vec, complex :: [ComplexEq]
complex)
  | [(SDoc, [PmLit])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(SDoc, [PmLit])]
cs   = [SDoc] -> SDoc
fsep [SDoc]
vec -- there are no literal constraints
  | Bool
otherwise = SDoc -> Int -> SDoc -> SDoc
hang ([SDoc] -> SDoc
fsep [SDoc]
vec) 4 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
                  String -> SDoc
text "where" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat (((SDoc, [PmLit]) -> SDoc) -> [(SDoc, [PmLit])] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (SDoc, [PmLit]) -> SDoc
ppr_constraint [(SDoc, [PmLit])]
cs)
  where
    sdoc_vec :: StateT ([PmNegLitCt], NameSet) Identity [SDoc]
sdoc_vec = (PmExpr -> StateT ([PmNegLitCt], NameSet) Identity SDoc)
-> [PmExpr] -> StateT ([PmNegLitCt], NameSet) Identity [SDoc]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM PmExpr -> StateT ([PmNegLitCt], NameSet) Identity SDoc
pprPmExprWithParens [PmExpr]
expr_vec
    (vec :: [SDoc]
vec,cs :: [(SDoc, [PmLit])]
cs) = StateT ([PmNegLitCt], NameSet) Identity [SDoc]
-> [PmNegLitCt] -> ([SDoc], [(SDoc, [PmLit])])
forall a. PmPprM a -> [PmNegLitCt] -> (a, [(SDoc, [PmLit])])
runPmPprM StateT ([PmNegLitCt], NameSet) Identity [SDoc]
sdoc_vec ([ComplexEq] -> [PmNegLitCt]
filterComplex [ComplexEq]
complex)

{- Note [Representation of Term Equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In the paper, term constraints always take the form (x ~ e). Of course, a more
general constraint of the form (e1 ~ e1) can always be transformed to an
equivalent set of the former constraints, by introducing a fresh, intermediate
variable: { y ~ e1, y ~ e1 }. Yet, implementing this representation gave rise
to #11160 (incredibly bad performance for literal pattern matching). Two are
the main sources of this problem (the actual problem is how these two interact
with each other):

1. Pattern matching on literals generates twice as many constraints as needed.
   Consider the following (tests/ghci/should_run/ghcirun004):

    foo :: Int -> Int
    foo 1    = 0
    ...
    foo 5000 = 4999

   The covered and uncovered set *should* look like:
     U0 = { x |> {} }

     C1  = { 1  |> { x ~ 1 } }
     U1  = { x  |> { False ~ (x ~ 1) } }
     ...
     C10 = { 10 |> { False ~ (x ~ 1), .., False ~ (x ~ 9), x ~ 10 } }
     U10 = { x  |> { False ~ (x ~ 1), .., False ~ (x ~ 9), False ~ (x ~ 10) } }
     ...

     If we replace { False ~ (x ~ 1) } with { y ~ False, y ~ (x ~ 1) }
     we get twice as many constraints. Also note that half of them are just the
     substitution [x |-> False].

2. The term oracle (`tmOracle` in deSugar/TmOracle) uses equalities of the form
   (x ~ e) as substitutions [x |-> e]. More specifically, function
   `extendSubstAndSolve` applies such substitutions in the residual constraints
   and partitions them in the affected and non-affected ones, which are the new
   worklist. Essentially, this gives quadradic behaviour on the number of the
   residual constraints. (This would not be the case if the term oracle used
   mutable variables but, since we use it to handle disjunctions on value set
   abstractions (`Union` case), we chose a pure, incremental interface).

Now the problem becomes apparent (e.g. for clause 300):
  * Set U300 contains 300 substituting constraints [y_i |-> False] and 300
    constraints that we know that will not reduce (stay in the worklist).
  * To check for consistency, we apply the substituting constraints ONE BY ONE
    (since `tmOracle` is called incrementally, it does not have all of them
    available at once). Hence, we go through the (non-progressing) constraints
    over and over, achieving over-quadradic behaviour.

If instead we allow constraints of the form (e ~ e),
  * All uncovered sets Ui contain no substituting constraints and i
    non-progressing constraints of the form (False ~ (x ~ lit)) so the oracle
    behaves linearly.
  * All covered sets Ci contain exactly (i-1) non-progressing constraints and
    a single substituting constraint. So the term oracle goes through the
    constraints only once.

The performance improvement becomes even more important when more arguments are
involved.
-}

-- Debugging Infrastructre

tracePm :: String -> SDoc -> PmM ()
tracePm :: String -> SDoc -> PmM ()
tracePm herald :: String
herald doc :: SDoc
doc = DsM () -> PmM ()
forall a. DsM a -> PmM a
liftD (DsM () -> PmM ()) -> DsM () -> PmM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> DsM ()
tracePmD String
herald SDoc
doc


tracePmD :: String -> SDoc -> DsM ()
tracePmD :: String -> SDoc -> DsM ()
tracePmD herald :: String
herald doc :: SDoc
doc = do
  DynFlags
dflags <- IOEnv (Env DsGblEnv DsLclEnv) DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  PrintUnqualified
printer <- DsM PrintUnqualified
mkPrintUnqualifiedDs
  IO () -> DsM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> DsM ()) -> IO () -> DsM ()
forall a b. (a -> b) -> a -> b
$ PrintUnqualified -> DynFlags -> DumpFlag -> SDoc -> IO ()
dumpIfSet_dyn_printer PrintUnqualified
printer DynFlags
dflags
            DumpFlag
Opt_D_dump_ec_trace (String -> SDoc
text String
herald SDoc -> SDoc -> SDoc
$$ (Int -> SDoc -> SDoc
nest 2 SDoc
doc))


pprPmPatDebug :: PmPat a -> SDoc
pprPmPatDebug :: PmPat a -> SDoc
pprPmPatDebug (PmCon cc :: ConLike
cc _arg_tys :: [Type]
_arg_tys _con_tvs :: [TyVar]
_con_tvs _con_dicts :: [TyVar]
_con_dicts con_args :: [PmPat a]
con_args)
  = [SDoc] -> SDoc
hsep [String -> SDoc
text "PmCon", ConLike -> SDoc
forall a. Outputable a => a -> SDoc
ppr ConLike
cc, [SDoc] -> SDoc
hsep ((PmPat a -> SDoc) -> [PmPat a] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map PmPat a -> SDoc
forall (a :: PatTy). PmPat a -> SDoc
pprPmPatDebug [PmPat a]
con_args)]
pprPmPatDebug (PmVar vid :: TyVar
vid) = String -> SDoc
text "PmVar" SDoc -> SDoc -> SDoc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
vid
pprPmPatDebug (PmLit li :: PmLit
li)  = String -> SDoc
text "PmLit" SDoc -> SDoc -> SDoc
<+> PmLit -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmLit
li
pprPmPatDebug (PmNLit i :: TyVar
i nl :: [PmLit]
nl) = String -> SDoc
text "PmNLit" SDoc -> SDoc -> SDoc
<+> TyVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyVar
i SDoc -> SDoc -> SDoc
<+> [PmLit] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [PmLit]
nl
pprPmPatDebug (PmGrd pv :: PatVec
pv ge :: PmExpr
ge) = String -> SDoc
text "PmGrd" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
hsep ((PmPat 'PAT -> SDoc) -> PatVec -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map PmPat 'PAT -> SDoc
forall (a :: PatTy). PmPat a -> SDoc
pprPmPatDebug PatVec
pv)
                                           SDoc -> SDoc -> SDoc
<+> PmExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr PmExpr
ge

pprPatVec :: PatVec -> SDoc
pprPatVec :: PatVec -> SDoc
pprPatVec ps :: PatVec
ps = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Pattern:") 2
                (SDoc -> SDoc
brackets (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep
                  ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate (SDoc
comma SDoc -> SDoc -> SDoc
<> Char -> SDoc
char '\n') ((PmPat 'PAT -> SDoc) -> PatVec -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map PmPat 'PAT -> SDoc
forall (a :: PatTy). PmPat a -> SDoc
pprPmPatDebug PatVec
ps))

pprValAbs :: [ValAbs] -> SDoc
pprValAbs :: [PmPat 'VA] -> SDoc
pprValAbs ps :: [PmPat 'VA]
ps = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "ValAbs:") 2
                (SDoc -> SDoc
brackets (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
sep
                  ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ SDoc -> [SDoc] -> [SDoc]
punctuate (SDoc
comma) ((PmPat 'VA -> SDoc) -> [PmPat 'VA] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map PmPat 'VA -> SDoc
forall (a :: PatTy). PmPat a -> SDoc
pprPmPatDebug [PmPat 'VA]
ps))

pprValVecDebug :: ValVec -> SDoc
pprValVecDebug :: ValVec -> SDoc
pprValVecDebug (ValVec vas :: [PmPat 'VA]
vas _d :: Delta
_d) = String -> SDoc
text "ValVec" SDoc -> SDoc -> SDoc
<+>
                                  SDoc -> SDoc
parens ([PmPat 'VA] -> SDoc
pprValAbs [PmPat 'VA]
vas)