Check.hs 112 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1
{-
2
Author: George Karachalias <george.karachalias@cs.kuleuven.be>
Austin Seipp's avatar
Austin Seipp committed
3

4
Pattern Matching Coverage Checking.
Austin Seipp's avatar
Austin Seipp committed
5
-}
sof's avatar
sof committed
6

7
{-# LANGUAGE CPP, GADTs, DataKinds, KindSignatures #-}
8
{-# LANGUAGE TupleSections #-}
9
{-# LANGUAGE ViewPatterns  #-}
10

11
module Check (
12
        -- Checking and printing
13
        checkSingle, checkMatches, checkGuardMatches, isAnyPmCheckEnabled,
14

15
        -- See Note [Type and Term Equality Propagation]
16
        genCaseTmCs1, genCaseTmCs2
17
    ) where
18

Simon Marlow's avatar
Simon Marlow committed
19
#include "HsVersions.h"
sof's avatar
sof committed
20

21 22
import GhcPrelude

23
import TmOracle
24
import Unify( tcMatchTy )
25
import DynFlags
Ian Lynagh's avatar
Ian Lynagh committed
26
import HsSyn
Simon Marlow's avatar
Simon Marlow committed
27 28
import TcHsSyn
import Id
cactus's avatar
cactus committed
29
import ConLike
Simon Marlow's avatar
Simon Marlow committed
30
import Name
31
import FamInstEnv
32
import TysPrim (tYPETyCon)
33
import TysWiredIn
Simon Marlow's avatar
Simon Marlow committed
34 35 36
import TyCon
import SrcLoc
import Util
37
import Outputable
38
import FastString
39
import DataCon
40
import PatSyn
41
import HscTypes (CompleteMatch(..))
sof's avatar
sof committed
42

43 44
import DsMonad
import TcSimplify    (tcCheckSatisfiability)
45
import TcType        (isStringTy)
46 47
import Bag
import ErrUtils
48
import Var           (EvVar)
49
import TyCoRep
50 51
import Type
import UniqSupply
52
import DsUtils       (isTrueLHsExpr)
53
import Maybes        (expectJust)
Tao He's avatar
Tao He committed
54
import qualified GHC.LanguageExtensions as LangExt
55

56
import Data.List     (find)
57 58
import Data.Maybe    (catMaybes, isJust, fromMaybe)
import Control.Monad (forM, when, forM_, zipWithM)
59 60
import Coercion
import TcEvidence
61
import TcSimplify    (tcNormalise)
62
import IOEnv
63
import qualified Data.Semigroup as Semi
sof's avatar
sof committed
64

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

67 68 69 70 71 72 73
{-
This module checks pattern matches for:
\begin{enumerate}
  \item Equations that are redundant
  \item Equations with inaccessible right-hand-side
  \item Exhaustiveness
\end{enumerate}
sof's avatar
sof committed
74

75
The algorithm is based on the paper:
76

77 78
  "GADTs Meet Their Match:
     Pattern-matching Warnings That Account for GADTs, Guards, and Laziness"
sof's avatar
sof committed
79

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

82 83 84 85 86 87
%************************************************************************
%*                                                                      *
                     Pattern Match Check Types
%*                                                                      *
%************************************************************************
-}
88

89 90 91 92 93 94 95 96 97 98 99 100 101
-- 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 m = ListT $ \sk fk -> m >>= \a -> sk a fk

102 103
-- 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
Gabor Greif's avatar
Gabor Greif committed
104
-- by the number of inaccessible clauses followed by number of redundant
105 106 107 108 109 110
-- 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.
111
getResult :: PmM PmResult -> DsM PmResult
Simon Peyton Jones's avatar
Simon Peyton Jones committed
112 113 114 115 116
getResult ls
  = do { res <- fold ls goM (pure Nothing)
       ; case res of
            Nothing -> panic "getResult is empty"
            Just a  -> return a }
117
  where
118
    goM :: PmResult -> DsM (Maybe PmResult) -> DsM (Maybe PmResult)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
119 120 121
    goM mpm dpm = do { pmr <- dpm
                     ; return $ Just $ go pmr mpm }

122
    -- Careful not to force unecessary results
Simon Peyton Jones's avatar
Simon Peyton Jones committed
123 124 125
    go :: Maybe PmResult -> PmResult -> PmResult
    go Nothing rs = rs
    go (Just old@(PmResult prov rs (UncoveredPatterns us) is)) new
126 127
      | null us && null rs && null is = old
      | otherwise =
128
        let PmResult prov' rs' (UncoveredPatterns us') is' = new
129 130 131
        in case compareLength us us'
                `mappend` (compareLength is is')
                `mappend` (compareLength rs rs')
132
                `mappend` (compare prov prov') of
Simon Peyton Jones's avatar
Simon Peyton Jones committed
133 134
              GT  -> new
              EQ  -> new
135
              LT  -> old
136 137
    go (Just (PmResult _ _ (TypeOfUncovered _) _)) _new
      = panic "getResult: No inhabitation candidates"
138

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

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

144
data PmPat :: PatTy -> * where
145
  PmCon  :: { pm_con_con     :: ConLike
146 147 148 149 150
            , pm_con_arg_tys :: [Type]
            , pm_con_tvs     :: [TyVar]
            , pm_con_dicts   :: [EvVar]
            , pm_con_args    :: [PmPat t] } -> PmPat t
            -- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hs
151
  PmVar  :: { pm_var_id   :: Id } -> PmPat t
152
  PmLit  :: { pm_lit_lit  :: PmLit } -> PmPat t -- See Note [Literals in PmPat]
153 154
  PmNLit :: { pm_lit_id   :: Id
            , pm_lit_not  :: [PmLit] } -> PmPat 'VA
155
  PmGrd  :: { pm_grd_pv   :: PatVec
156
            , pm_grd_expr :: PmExpr  } -> PmPat 'PAT
157

158 159 160
instance Outputable (PmPat a) where
  ppr = pprPmPatDebug

161 162 163 164
-- 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

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

168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189
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_ty_cs :: Bag EvVar
                     , 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
190 191 192 193 194 195 196 197 198 199

data Covered = Covered | NotCovered
  deriving Show

instance Outputable Covered where
  ppr (Covered) = text "Covered"
  ppr (NotCovered) = text "NotCovered"

-- Like the or monoid for booleans
-- Covered = True, Uncovered = False
200 201 202 203 204
instance Semi.Semigroup Covered where
  Covered <> _ = Covered
  _ <> Covered = Covered
  NotCovered <> NotCovered = NotCovered

205 206
instance Monoid Covered where
  mempty = NotCovered
207
  mappend = (Semi.<>)
208 209 210 211 212 213 214 215

data Diverged = Diverged | NotDiverged
  deriving Show

instance Outputable Diverged where
  ppr Diverged = text "Diverged"
  ppr NotDiverged = text "NotDiverged"

216 217 218 219 220
instance Semi.Semigroup Diverged where
  Diverged <> _ = Diverged
  _ <> Diverged = Diverged
  NotDiverged <> NotDiverged = NotDiverged

221 222
instance Monoid Diverged where
  mempty = NotDiverged
223
  mappend = (Semi.<>)
224

225 226 227 228 229 230 231 232 233 234
-- | 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 (Show, Eq, Ord)

instance Outputable Provenance where
  ppr  = text . show

235 236 237 238 239
instance Semi.Semigroup Provenance where
  FromComplete <> _ = FromComplete
  _ <> FromComplete = FromComplete
  _ <> _ = FromBuiltin

240 241
instance Monoid Provenance where
  mempty = FromBuiltin
242
  mappend = (Semi.<>)
243

244
data PartialResult = PartialResult {
Gabor Greif's avatar
Gabor Greif committed
245
                        presultProvenance :: Provenance
246 247
                         -- keep track of provenance because we don't want
                         -- to warn about redundant matches if the result
Gabor Greif's avatar
Gabor Greif committed
248
                         -- is contaminated with a COMPLETE pragma
249
                      , presultCovered :: Covered
250 251 252 253
                      , presultUncovered :: Uncovered
                      , presultDivergent :: Diverged }

instance Outputable PartialResult where
254 255
  ppr (PartialResult prov c vsa d)
           = text "PartialResult" <+> ppr prov <+> ppr c
256 257
                                  <+> ppr d <+> ppr vsa

258 259 260 261 262 263 264 265 266 267

instance Semi.Semigroup PartialResult where
  (PartialResult prov1 cs1 vsa1 ds1)
    <> (PartialResult prov2 cs2 vsa2 ds2)
      = PartialResult (prov1 Semi.<> prov2)
                      (cs1 Semi.<> cs2)
                      (vsa1 Semi.<> vsa2)
                      (ds1 Semi.<> ds2)


268
instance Monoid PartialResult where
269
  mempty = PartialResult mempty mempty [] mempty
270
  mappend = (Semi.<>)
271 272

-- newtype ChoiceOf a = ChoiceOf [a]
273

Ben Gamari's avatar
Ben Gamari committed
274 275
-- | Pattern check result
--
276
-- * Redundant clauses
277
-- * Not-covered clauses (or their type, if no pattern is available)
278
-- * Clauses with inaccessible RHS
279 280 281 282
--
-- More details about the classification of clauses into useful, redundant
-- and with inaccessible right hand side can be found here:
--
283
--     https://gitlab.haskell.org/ghc/ghc/wikis/pattern-match-check
284
--
285 286
data PmResult =
  PmResult {
Simon Peyton Jones's avatar
Simon Peyton Jones committed
287 288 289
      pmresultProvenance   :: Provenance
    , pmresultRedundant    :: [Located [LPat GhcTc]]
    , pmresultUncovered    :: UncoveredCandidates
290
    , pmresultInaccessible :: [Located [LPat GhcTc]] }
291

292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313
-- | 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 FromBuiltin [] (UncoveredPatterns []) []

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

314 315 316 317 318 319 320
{-
%************************************************************************
%*                                                                      *
       Entry points to the checker: checkSingle and checkMatches
%*                                                                      *
%************************************************************************
-}
321

322
-- | Check a single pattern binding (let)
323
checkSingle :: DynFlags -> DsMatchContext -> Id -> Pat GhcTc -> DsM ()
324
checkSingle dflags ctxt@(DsMatchContext _ locn) var p = do
325
  tracePmD "checkSingle" (vcat [ppr ctxt, ppr var, ppr p])
326
  mb_pm_res <- tryM (getResult (checkSingle' locn var p))
327 328 329 330 331
  case mb_pm_res of
    Left  _   -> warnPmIters dflags ctxt
    Right res -> dsPmWarn dflags ctxt res

-- | Check a single pattern binding (let)
332
checkSingle' :: SrcSpan -> Id -> Pat GhcTc -> PmM PmResult
333
checkSingle' locn var p = do
334 335 336
  liftD resetPmIterDs -- set the iter-no to zero
  fam_insts <- liftD dsGetFamInstEnvs
  clause    <- liftD $ translatePat fam_insts p
337
  missing   <- mkInitialUncovered [var]
Simon Jakobi's avatar
Simon Jakobi committed
338 339
  tracePm "checkSingle': missing" (vcat (map pprValVecDebug missing))
                                  -- no guards
340
  PartialResult prov cs us ds <- runMany (pmcheckI clause []) missing
341
  let us' = UncoveredPatterns us
342
  return $ case (cs,ds) of
343 344 345
    (Covered,  _    )         -> PmResult prov [] us' [] -- useful
    (NotCovered, NotDiverged) -> PmResult prov m  us' [] -- redundant
    (NotCovered, Diverged )   -> PmResult prov [] us' m  -- inaccessible rhs
346
  where m = [cL locn [cL locn p]]
347

348 349 350 351 352
-- | 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 ()
353
checkGuardMatches hs_ctx guards@(GRHSs _ grhss _) = do
354 355 356
    dflags <- getDynFlags
    let combinedLoc = foldl1 combineSrcSpans (map getLoc grhss)
        dsMatchContext = DsMatchContext hs_ctx combinedLoc
357
        match = cL combinedLoc $
358 359
                  Match { m_ext = noExt
                        , m_ctxt = hs_ctx
360 361 362
                        , m_pats = []
                        , m_grhss = guards }
    checkMatches dflags dsMatchContext [] [match]
363
checkGuardMatches _ (XGRHSs _) = panic "checkGuardMatches"
364

365
-- | Check a matchgroup (case, functions, etc.)
366
checkMatches :: DynFlags -> DsMatchContext
367
             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
368
checkMatches dflags ctxt vars matches = do
369
  tracePmD "checkMatches" (hang (vcat [ppr ctxt
370 371 372 373
                               , ppr vars
                               , text "Matches:"])
                               2
                               (vcat (map ppr matches)))
374 375 376 377 378
  mb_pm_res <- tryM $ getResult $ case matches of
    -- Check EmptyCase separately
    -- See Note [Checking EmptyCase Expressions]
    [] | [var] <- vars -> checkEmptyCase' var
    _normal_match      -> checkMatches' vars matches
379 380 381
  case mb_pm_res of
    Left  _   -> warnPmIters dflags ctxt
    Right res -> dsPmWarn dflags ctxt res
382

383 384
-- | Check a matchgroup (case, functions, etc.). To be called on a non-empty
-- list of matches. For empty case expressions, use checkEmptyCase' instead.
385
checkMatches' :: [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> PmM PmResult
386
checkMatches' vars matches
387
  | null matches = panic "checkMatches': EmptyCase"
388
  | otherwise = do
389
      liftD resetPmIterDs -- set the iter-no to zero
390
      missing    <- mkInitialUncovered vars
391
      tracePm "checkMatches': missing" (vcat (map pprValVecDebug missing))
392
      (prov, rs,us,ds) <- go matches missing
393 394 395 396 397
      return $ PmResult {
                   pmresultProvenance   = prov
                 , pmresultRedundant    = map hsLMatchToLPats rs
                 , pmresultUncovered    = UncoveredPatterns us
                 , pmresultInaccessible = map hsLMatchToLPats ds }
398
  where
399
    go :: [LMatch GhcTc (LHsExpr GhcTc)] -> Uncovered
400
       -> PmM (Provenance
401
              , [LMatch GhcTc (LHsExpr GhcTc)]
402
              , Uncovered
403
              , [LMatch GhcTc (LHsExpr GhcTc)])
404
    go []     missing = return (mempty, [], missing, [])
405
    go (m:ms) missing = do
Simon Jakobi's avatar
Simon Jakobi committed
406
      tracePm "checkMatches': go" (ppr m $$ ppr missing)
407 408
      fam_insts          <- liftD dsGetFamInstEnvs
      (clause, guards)   <- liftD $ translateMatch fam_insts m
409
      r@(PartialResult prov cs missing' ds)
410
        <- runMany (pmcheckI clause guards) missing
Simon Jakobi's avatar
Simon Jakobi committed
411
      tracePm "checkMatches': go: res" (ppr r)
412 413
      (ms_prov, rs, final_u, is)  <- go ms missing'
      let final_prov = prov `mappend` ms_prov
414
      return $ case (cs, ds) of
415 416 417 418 419 420
        -- useful
        (Covered,  _    )        -> (final_prov,  rs, final_u,   is)
        -- redundant
        (NotCovered, NotDiverged) -> (final_prov, m:rs, final_u,is)
        -- inaccessible
        (NotCovered, Diverged )   -> (final_prov,  rs, final_u, m:is)
421

422
    hsLMatchToLPats :: LMatch id body -> Located [LPat id]
423
    hsLMatchToLPats (dL->L l (Match { m_pats = pats })) = cL l pats
Simon Jakobi's avatar
Simon Jakobi committed
424
    hsLMatchToLPats _                                   = panic "checkMatches'"
425

426 427 428 429 430
-- | 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' var = do
431
  tm_ty_css     <- pmInitialTmTyCs
432
  mb_candidates <- inhabitationCandidates (delta_ty_cs tm_ty_css) (idType var)
433 434 435 436 437 438
  case mb_candidates of
    -- Inhabitation checking failed / the type is trivially inhabited
    Left ty -> return (uncoveredWithTy ty)

    -- A list of inhabitant candidates is available: Check for each
    -- one for the satisfiability of the constraints it gives rise to.
439
    Right (_, candidates) -> do
440 441 442 443 444 445
      missing_m <- flip mapMaybeM candidates $
          \InhabitationCandidate{ ic_val_abs = va, ic_tm_ct = tm_ct
                                , ic_ty_cs = ty_cs
                                , ic_strict_arg_tys = strict_arg_tys } -> do
        mb_sat <- pmIsSatisfiable tm_ty_css tm_ct ty_cs strict_arg_tys
        pure $ fmap (ValVec [va]) mb_sat
446 447
      return $ if null missing_m
        then emptyPmResult
448
        else PmResult FromBuiltin [] (UncoveredPatterns missing_m) []
449

450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483
-- | 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 ty
  = case splitTyConApp_maybe ty of
      Just (tc, ty_args)
             | is_algebraic_like tc && not (isFamilyTyCon tc)
             -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True
      _other -> 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 tc = isAlgTyCon tc || tc == tYPETyCon

484 485
pmTopNormaliseType_maybe :: FamInstEnvs -> Bag EvVar -> Type
                         -> PmM (Maybe (Type, [DataCon], Type))
486 487 488 489 490 491 492 493
-- ^ 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.
494 495 496 497
--
-- 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.
498 499 500 501 502 503 504 505 506 507 508 509
pmTopNormaliseType_maybe env ty_cs typ
  = do (_, mb_typ') <- liftD $ initTcDsForSolver $ tcNormalise ty_cs 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].
       pure $ do typ' <- mb_typ'
                 ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ'
                 -- We need to do topNormaliseTypeX in addition to tcNormalise,
                 -- since topNormaliseX looks through newtypes, which
                 -- tcNormalise does not do.
                 Just (eq_src_ty ty (typ' : ty_f [ty]), tm_f [], ty)
510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542
  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 ty tys = maybe ty id (find is_closed_or_data_family tys)

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

    -- For efficiency, represent both lists as difference lists.
    -- comb performs the concatenation, for both lists.
    comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2)

    stepper = newTypeStepper `composeSteppers` 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 rec_nts tc tys
      | Just (ty', _co) <- instNewTyCon_maybe tc tys
      = case checkRecTc rec_nts tc of
          Just rec_nts' -> let tyf = ((TyConApp tc tys):)
                               tmf = ((tyConSingleDataCon tc):)
                           in  NS_Step rec_nts' ty' (tyf, tmf)
          Nothing       -> NS_Abort
      | otherwise
      = NS_Done

    tyFamStepper :: NormaliseStepper ([Type] -> [Type], [DataCon] -> [DataCon])
    tyFamStepper rec_nts tc tys  -- Try to step a type/data family
543
      = let (_args_co, ntys, _res_co) = normaliseTcArgs env Representational tc tys in
544 545 546 547 548 549 550 551 552 553
          -- 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 reduceTyFamApp_maybe env Representational tc ntys of
          Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id)
          _               -> NS_Done

554 555 556 557 558 559
-- | 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.)
560
pmInitialTmTyCs :: PmM Delta
561 562 563 564 565 566
pmInitialTmTyCs = do
  ty_cs  <- liftD getDictsDs
  tm_cs  <- map toComplex . bagToList <$> liftD getTmCsDs
  sat_ty <- tyOracle ty_cs
  let initTyCs = if sat_ty then ty_cs else emptyBag
      initTmState = fromMaybe initialTmState (tmOracle initialTmState tm_cs)
567
  pure $ MkDelta{ delta_tm_cs = initTmState, delta_ty_cs = initTyCs }
568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588

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

589 590
-- | Given a conlike's term constraints, type constraints, and strict argument
-- types, check if they are satisfiable.
591 592 593 594 595 596 597 598 599 600 601 602 603
-- (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).
604 605 606 607
--
-- 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]@.
608
pmIsSatisfiable
609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624
  :: 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 amb_cs new_tm_c new_ty_cs strict_arg_tys = do
  mb_sat <- tmTyCsAreSatisfiable amb_cs new_tm_c new_ty_cs
  case mb_sat of
    Nothing -> pure Nothing
    Just delta -> do
      -- We know that the term and type constraints are inhabitable, so now
      -- check if each strict argument type is inhabitable.
625 626 627
      all_non_void <- checkAllNonVoid initRecTc delta strict_arg_tys
      pure $ if all_non_void -- Check if each strict argument type
                             -- is inhabitable
628 629 630 631 632
                then Just delta
                else Nothing

-- | Like 'pmIsSatisfiable', but only checks if term and type constraints are
-- satisfiable, and doesn't bother checking anything related to strict argument
633
-- types.
634 635 636 637
tmTyCsAreSatisfiable
  :: Delta     -- ^ The ambient term and type constraints
               --   (known to be satisfiable).
  -> ComplexEq -- ^ The new term constraint.
638
  -> Bag EvVar -- ^ The new type constraints.
639 640 641 642 643 644
  -> PmM (Maybe Delta)
       -- ^ @'Just' delta@ if the constraints (@delta@) are
       -- satisfiable. 'Nothing' otherwise.
tmTyCsAreSatisfiable
    (MkDelta{ delta_tm_cs = amb_tm_cs, delta_ty_cs = amb_ty_cs })
    new_tm_c new_ty_cs = do
645 646 647 648
  let ty_cs = new_ty_cs `unionBags` amb_ty_cs
  sat_ty <- if isEmptyBag new_ty_cs
               then pure True
               else tyOracle ty_cs
649 650 651
  pure $ case (sat_ty, solveOneEq amb_tm_cs new_tm_c) of
           (True, Just term_cs) -> Just $ MkDelta{ delta_ty_cs = ty_cs
                                                 , delta_tm_cs = term_cs }
652 653
           _unsat               -> Nothing

654 655 656 657 658 659
-- | 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 rec_ts amb_cs strict_arg_tys = do
  fam_insts <- liftD dsGetFamInstEnvs
660 661 662 663
  let definitely_inhabited =
        definitelyInhabitedType fam_insts (delta_ty_cs amb_cs)
  tys_to_check <- filterOutM definitely_inhabited strict_arg_tys
  let rec_max_bound | tys_to_check `lengthExceeds` 1
664 665 666 667 668 669
                    = 1
                    | otherwise
                    = defaultRecTcMaxBound
      rec_ts' = setRecTcMaxBound rec_max_bound rec_ts
  allM (nonVoid rec_ts' amb_cs) tys_to_check

670 671 672 673
-- | 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
674 675 676 677 678 679 680 681 682
  :: 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 rec_ts amb_cs strict_arg_ty = do
683
  mb_cands <- inhabitationCandidates (delta_ty_cs amb_cs) strict_arg_ty
684
  case mb_cands of
685 686 687 688 689 690 691 692 693
    Right (tc, cands)
      |  Just rec_ts' <- checkRecTc rec_ts tc
      -> anyM (cand_is_inhabitable rec_ts' amb_cs) cands
           -- A strict argument type is inhabitable by a terminating value if
           -- at least one InhabitationCandidate is inhabitable.
    _ -> pure 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).
694
  where
695 696 697 698 699 700
    -- 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).
    --
701
    -- See Note [Extensions to GADTs Meet Their Match]
702 703 704 705 706 707
    cand_is_inhabitable :: RecTcChecker -> Delta
                        -> InhabitationCandidate -> PmM Bool
    cand_is_inhabitable rec_ts amb_cs
      (InhabitationCandidate{ ic_tm_ct          = new_term_c
                            , ic_ty_cs          = new_ty_cs
                            , ic_strict_arg_tys = new_strict_arg_tys }) = do
708
        mb_sat <- tmTyCsAreSatisfiable amb_cs new_term_c new_ty_cs
709 710 711 712 713 714 715 716 717 718 719 720 721
        case mb_sat of
          Nothing -> pure False
          Just new_delta -> do
            checkAllNonVoid rec_ts new_delta 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]@.
722 723 724 725 726 727
definitelyInhabitedType :: FamInstEnvs -> Bag EvVar -> Type -> PmM Bool
definitelyInhabitedType env ty_cs ty = do
  mb_res <- pmTopNormaliseType_maybe env ty_cs ty
  pure $ case mb_res of
           Just (_, cons, _) -> any meets_criteria cons
           Nothing           -> False
728 729 730 731 732
  where
    meets_criteria :: DataCon -> Bool
    meets_criteria con =
      null (dataConEqSpec con) && -- (1)
      null (dataConImplBangs con) -- (2)
733

734 735 736 737 738 739 740 741 742 743 744 745 746 747
{- 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

748 749
Hence, if pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty),
then
750 751 752 753
  (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
754
      newtype to its core representation, we keep track of the source data
755 756
      constructor.
  (c) core_ty is the rewritten type. That is,
757
        pmTopNormaliseType_maybe env ty_cs ty = Just (src_ty, dcs, core_ty)
758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776
      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

777
In this case pmTopNormaliseType_maybe env ty_cs (F Int) results in
778 779 780 781 782 783

  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).
784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804

-----
-- 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.
805 806
-}

807 808 809 810 811
-- | 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.
812
-- See also Note [Checking EmptyCase Expressions]
813
inhabitationCandidates :: Bag EvVar -> Type
814
                       -> PmM (Either Type (TyCon, [InhabitationCandidate]))
815 816 817 818 819 820
inhabitationCandidates ty_cs ty = do
  fam_insts   <- liftD dsGetFamInstEnvs
  mb_norm_res <- pmTopNormaliseType_maybe fam_insts ty_cs ty
  case mb_norm_res of
    Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
    Nothing                     -> alts_to_check ty     ty      []
821 822 823 824 825 826 827 828 829 830 831 832 833
  where
    -- All these types are trivially inhabited
    trivially_inhabited = [ charTyCon, doubleTyCon, floatTyCon
                          , intTyCon, wordTyCon, 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 = foldr (\dc e -> PmCon (RealDataCon dc) [] [] [] [e])

    -- Inhabitation candidates, using the result of pmTopNormaliseType_maybe
    alts_to_check :: Type -> Type -> [DataCon]
834
                  -> PmM (Either Type (TyCon, [InhabitationCandidate]))
835 836
    alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
      Just (tc, _)
837 838 839 840 841
        |  tc `elem` trivially_inhabited
        -> case dcs of
             []    -> return (Left src_ty)
             (_:_) -> do var <- liftD $ mkPmId core_ty
                         let va = build_tm (PmVar var) dcs
842
                         return $ Right (tc, [InhabitationCandidate
843
                           { ic_val_abs = va, ic_tm_ct = mkIdEq var
844
                           , ic_ty_cs = emptyBag, ic_strict_arg_tys = [] }])
845 846 847 848 849 850 851 852

        |  pmIsClosedType core_ty && not (isAbstractTyCon 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.
        -> liftD $ do
             var  <- mkPmId core_ty -- it would be wrong to unify x
             alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
853 854 855
             return $ Right
               (tc, [ alt{ic_val_abs = build_tm (ic_val_abs alt) dcs}
                    | alt <- alts ])
856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893
      -- For other types conservatively assume that they are inhabited.
      _other -> return (Left 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.

894 895 896 897 898
%************************************************************************
%*                                                                      *
              Transform source syntax to *our* syntax
%*                                                                      *
%************************************************************************
Austin Seipp's avatar
Austin Seipp committed
899
-}
sof's avatar
sof committed
900

901 902 903
-- -----------------------------------------------------------------------
-- * Utilities

904
nullaryConPattern :: ConLike -> Pattern
905
-- Nullary data constructor and nullary type constructor
906
nullaryConPattern con =
907 908
  PmCon { pm_con_con = con, pm_con_arg_tys = []
        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
909
{-# INLINE nullaryConPattern #-}
910 911

truePattern :: Pattern
912
truePattern = nullaryConPattern (RealDataCon trueDataCon)
913
{-# INLINE truePattern #-}
914 915 916

-- | A fake guard pattern (True <- _) used to represent cases we cannot handle
fake_pat :: Pattern
917
fake_pat = PmGrd { pm_grd_pv   = [truePattern]
918
                 , pm_grd_expr = PmExprOther (EWildPat noExt) }
919 920 921 922
{-# INLINE fake_pat #-}

-- | Check whether a guard pattern is generated by the checker (unhandled)
isFakeGuard :: [Pattern] -> PmExpr -> Bool
923
isFakeGuard [PmCon { pm_con_con = RealDataCon c }] (PmExprOther (EWildPat _))
924 925 926 927 928
  | c == trueDataCon = True
  | otherwise        = False
isFakeGuard _pats _e = False

-- | Generate a `canFail` pattern vector of a specific type
929
mkCanFailPmPat :: Type -> DsM PatVec
930 931 932
mkCanFailPmPat ty = do
  var <- mkPmVar ty
  return [var, fake_pat]
933

934
vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
935
-- ADT constructor pattern => no existentials, no local constraints
936
vanillaConPattern con arg_tys args =
937 938
  PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
939
{-# INLINE vanillaConPattern #-}
940

941
-- | Create an empty list pattern of a given type
942
nilPattern :: Type -> Pattern
943
nilPattern ty =
944
  PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty]
945 946
        , pm_con_tvs = [], pm_con_dicts = []
        , pm_con_args = [] }
947
{-# INLINE nilPattern #-}
948 949

mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
950
mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon
951 952 953
                               , pm_con_arg_tys = [ty]
                               , pm_con_tvs = [], pm_con_dicts = []
                               , pm_con_args = xs++ys }]
954
{-# INLINE mkListPatVec #-}
955

956
-- | Create a (non-overloaded) literal pattern
957
mkLitPattern :: HsLit GhcTc -> Pattern
958
mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
959
{-# INLINE mkLitPattern #-}
960 961 962 963

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

964
translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
965
translatePat fam_insts pat = case pat of
966 967 968 969
  WildPat  ty  -> mkPmVars [ty]
  VarPat _ id  -> return [PmVar (unLoc id)]
  ParPat _ p   -> translatePat fam_insts (unLoc p)
  LazyPat _ _  -> mkPmVars [hsPatType pat] -- like a variable
970 971

  -- ignore strictness annotations for now
972
  BangPat _ p  -> translatePat fam_insts (unLoc p)
973

974
  AsPat _ lid p -> do
975
     -- Note [Translating As Patterns]
976
    ps <- translatePat fam_insts (unLoc p)
977
    let [e] = map vaToPmExpr (coercePatVec ps)
978
        g   = PmGrd [PmVar (unLoc lid)] e
979 980
    return (ps ++ [g])

981
  SigPat _ p _ty -> translatePat fam_insts (unLoc p)
982

983
  -- See Note [Translate CoPats]
984
  CoPat _ wrapper p ty
985 986
    | isIdHsWrapper wrapper                   -> translatePat fam_insts p
    | WpCast co <-  wrapper, isReflexiveCo co -> translatePat fam_insts p
987
    | otherwise -> do
988
        ps      <- translatePat fam_insts p
989
        (xp,xe) <- mkPmId2Forms ty
990
        let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
991
        return [xp,g]
992 993

  -- (n + k)  ===>   x (True <- x >= k) (n <- x-k)
994
  NPlusKPat ty (dL->L _ _n) _k1 _k2 _ge _minus -> mkCanFailPmPat ty
995 996

  -- (fun -> pat)   ===>   x (pat <- fun x)
997
  ViewPat arg_ty lexpr lpat -> do
998
    ps <- translatePat fam_insts (unLoc lpat)
999 1000 1001
    -- See Note [Guards and Approximation]
    case all cantFailPattern ps of
      True  -> do
1002
        (xp,xe) <- mkPmId2Forms arg_ty
1003
        let g = mkGuard ps (HsApp noExt lexpr xe)
1004
        return [xp,g]
1005
      False -> mkCanFailPmPat arg_ty
1006 1007

  -- list
1008
  ListPat (ListPatTc ty Nothing) ps -> do
1009 1010
    foldr (mkListPatVec ty) [nilPattern ty]
      <$> translatePatVec fam_insts (map unLoc ps)
1011 1012

  -- overloaded list
Tao He's avatar
Tao He committed
1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032
  ListPat (ListPatTc _elem_ty (Just (pat_ty, _to_list))) lpats -> do
    dflags <- getDynFlags
    if xopt LangExt.RebindableSyntax dflags
       then mkCanFailPmPat pat_ty
       else case splitListTyConApp_maybe pat_ty of
              Just e_ty -> translatePat fam_insts
                                        (ListPat (ListPatTc e_ty Nothing) lpats)
              Nothing   -> mkCanFailPmPat 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.
    --
1033
    -- See #14547, especially comment#9 and comment#10.
Tao He's avatar
Tao He committed
1034 1035 1036 1037
    --
    -- 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].
1038

1039
  ConPatOut { pat_con     = (dL->L _ con)
1040 1041 1042 1043
            , pat_arg_tys = arg_tys
            , pat_tvs     = ex_tvs
            , pat_dicts   = dicts
            , pat_args    = ps } -> do
1044 1045 1046 1047 1048 1049 1050 1051 1052 1053
    groups <- allCompleteMatches con arg_tys
    case groups of
      [] -> mkCanFailPmPat (conLikeResTy con arg_tys)
      _  -> do
        args <- translateConPatVec fam_insts arg_tys ex_tvs con ps
        return [PmCon { pm_con_con     = con
                      , pm_con_arg_tys = arg_tys
                      , pm_con_tvs     = ex_tvs
                      , pm_con_dicts   = dicts
                      , pm_con_args    = args }]
1054

1055
  -- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
1056
  NPat _ (dL->L _ olit) mb_neg _
1057 1058 1059 1060 1061 1062
    | OverLit (OverLitTc False ty) (HsIsString src s) _ <- olit
    , isStringTy ty ->
        foldr (mkListPatVec charTy) [nilPattern charTy] <$>
          translatePatVec fam_insts
            (map (LitPat noExt . HsChar src) (unpackFS s))
    | otherwise -> return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) olit }]
1063

1064
  -- See Note [Translate Overloaded Literal for Exhaustiveness Checking]
1065
  LitPat _ lit
1066 1067
    | HsString src s <- lit ->
        foldr (mkListPatVec charTy) [nilPattern charTy] <$>
1068
          translatePatVec fam_insts
1069
            (map (LitPat noExt . HsChar src) (unpackFS s))
1070 1071
    | otherwise -> return [mkLitPattern lit]

1072
  TuplePat tys ps boxity -> do
1073
    tidy_ps <- translatePatVec fam_insts (map unLoc ps)
1074
    let tuple_con = RealDataCon (tupleDataCon boxity (length ps))
1075 1076
    return [vanillaConPattern tuple_con tys (concat tidy_ps)]

1077
  SumPat ty p alt arity -> do
1078
    tidy_p <- translatePat fam_insts (unLoc p)
1079
    let sum_con = RealDataCon (sumDataCon alt arity)
1080 1081
    return [vanillaConPattern sum_con ty tidy_p]

1082 1083 1084 1085
  -- --------------------------------------------------------------------------
  -- Not supposed to happen
  ConPatIn  {} -> panic "Check.translatePat: ConPatIn"
  SplicePat {} -> panic "Check.translatePat: SplicePat"
1086
  XPat      {} -> panic "Check.translatePat: XPat"
1087

1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102
{- 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
1103
    #14546.
1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123

  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,
1124
    as reported in #14546. In this patch we remove the specialization of
1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143
    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
1144
    non-exhaustive pattern matching warnings, as reported in #14546.
1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169

    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
1170
  #14546.
1171
-}
1172 1173 1174

-- | Translate a list of patterns (Note: each pattern is translated
-- to a pattern vector but we do not concatenate the results).
1175
translatePatVec :: FamInstEnvs -> [Pat GhcTc] -> DsM [PatVec]
1176
translatePatVec fam_insts pats = mapM (translatePat fam_insts) pats
1177

1178
-- | Translate a constructor pattern
1179
translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
1180
                   -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
1181 1182 1183 1184 1185
translateConPatVec fam_insts _univ_tys _ex_tvs _ (PrefixCon ps)
  = concat <$> translatePatVec fam_insts (map unLoc ps)
translateConPatVec fam_insts _univ_tys _ex_tvs _ (InfixCon p1 p2)
  = concat <$> translatePatVec fam_insts (map unLoc [p1,p2])
translateConPatVec fam_insts  univ_tys  ex_tvs c (RecCon (HsRecFields fs _))
1186
    -- Nothing matched. Make up some fresh term variables
1187
  | null fs        = mkPmVars arg_tys
1188 1189 1190
    -- 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.
1191
  | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
1192 1193 1194 1195
    -- 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
  | matched_lbls `subsetOf` orig_lbls
1196
  = ASSERT(orig_lbls `equalLength` arg_tys)
1197
      let translateOne (lbl, ty) = case lookup lbl matched_pats of
1198
            Just p  -> translatePat fam_insts p
1199
            Nothing -> mkPmVars [ty]
1200 1201 1202 1203 1204
      in  concatMapM translateOne (zip orig_lbls 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.
  | otherwise = do
1205
      arg_var_pats    <- mkPmVars arg_tys
1206
      translated_pats <- forM matched_pats $ \(x,pat) -> do
1207
        pvec <- translatePat fam_insts pat
1208 1209
        return (x, pvec)

1210
      let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
1211
          guards = map (\(name,pvec) -> case lookup name zipped of
1212
                            Just x  -> PmGrd pvec (PmExprVar (idName x))