Check.hs 90 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

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

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

        -- Pattern-match-specific type operations
        pmIsClosedType, pmTopNormaliseType_maybe
19
    ) where
20

Simon Marlow's avatar
Simon Marlow committed
21
#include "HsVersions.h"
sof's avatar
sof committed
22

23 24
import GhcPrelude

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

45 46 47
import DsMonad
import TcSimplify    (tcCheckSatisfiability)
import TcType        (toTcType, isStringTy, isIntTy, isWordTy)
48 49
import Bag
import ErrUtils
50
import Var           (EvVar)
51
import TyCoRep
52 53
import Type
import UniqSupply
54
import DsGRHSs       (isTrueLHsExpr)
55
import Maybes        (expectJust)
56

57
import Data.List     (find)
58 59
import Data.Maybe    (catMaybes, isJust, fromMaybe)
import Control.Monad (forM, when, forM_, zipWithM)
60 61
import Coercion
import TcEvidence
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 161

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

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

165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
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
187 188 189 190 191 192 193 194 195 196

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
197 198 199 200 201
instance Semi.Semigroup Covered where
  Covered <> _ = Covered
  _ <> Covered = Covered
  NotCovered <> NotCovered = NotCovered

202 203
instance Monoid Covered where
  mempty = NotCovered
204
  mappend = (Semi.<>)
205 206 207 208 209 210 211 212

data Diverged = Diverged | NotDiverged
  deriving Show

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

213 214 215 216 217
instance Semi.Semigroup Diverged where
  Diverged <> _ = Diverged
  _ <> Diverged = Diverged
  NotDiverged <> NotDiverged = NotDiverged

218 219
instance Monoid Diverged where
  mempty = NotDiverged
220
  mappend = (Semi.<>)
221

222 223 224 225 226 227 228 229 230 231
-- | 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

232 233 234 235 236
instance Semi.Semigroup Provenance where
  FromComplete <> _ = FromComplete
  _ <> FromComplete = FromComplete
  _ <> _ = FromBuiltin

237 238
instance Monoid Provenance where
  mempty = FromBuiltin
239
  mappend = (Semi.<>)
240

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

instance Outputable PartialResult where
251 252
  ppr (PartialResult prov c vsa d)
           = text "PartialResult" <+> ppr prov <+> ppr c
253 254
                                  <+> ppr d <+> ppr vsa

255 256 257 258 259 260 261 262 263 264

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)


265
instance Monoid PartialResult where
266
  mempty = PartialResult mempty mempty [] mempty
267
  mappend = (Semi.<>)
268 269

-- newtype ChoiceOf a = ChoiceOf [a]
270

Ben Gamari's avatar
Ben Gamari committed
271 272
-- | Pattern check result
--
273
-- * Redundant clauses
274
-- * Not-covered clauses (or their type, if no pattern is available)
275
-- * Clauses with inaccessible RHS
276 277 278 279 280 281
--
-- 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
--
282 283
data PmResult =
  PmResult {
Simon Peyton Jones's avatar
Simon Peyton Jones committed
284 285 286
      pmresultProvenance   :: Provenance
    , pmresultRedundant    :: [Located [LPat GhcTc]]
    , pmresultUncovered    :: UncoveredCandidates
287
    , pmresultInaccessible :: [Located [LPat GhcTc]] }
288

289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310
-- | 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) []

311 312 313 314 315 316 317
{-
%************************************************************************
%*                                                                      *
       Entry points to the checker: checkSingle and checkMatches
%*                                                                      *
%************************************************************************
-}
318

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

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

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

362
-- | Check a matchgroup (case, functions, etc.)
363
checkMatches :: DynFlags -> DsMatchContext
364
             -> [Id] -> [LMatch GhcTc (LHsExpr GhcTc)] -> DsM ()
365
checkMatches dflags ctxt vars matches = do
366
  tracePmD "checkMatches" (hang (vcat [ppr ctxt
367 368 369 370
                               , ppr vars
                               , text "Matches:"])
                               2
                               (vcat (map ppr matches)))
371 372 373 374 375
  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
376 377 378
  case mb_pm_res of
    Left  _   -> warnPmIters dflags ctxt
    Right res -> dsPmWarn dflags ctxt res
379

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

419
    hsLMatchToLPats :: LMatch id body -> Located [LPat id]
420
    hsLMatchToLPats (L l (Match { m_pats = pats })) = L l pats
421
    hsLMatchToLPats (L _ (XMatch _)) = panic "checMatches'"
422

423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454
-- | 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
  tm_css <- map toComplex . bagToList <$> liftD getTmCsDs
  case tmOracle initialTmState tm_css of
    Just tm_state -> do
      ty_css        <- liftD getDictsDs
      fam_insts     <- liftD dsGetFamInstEnvs
      mb_candidates <- inhabitationCandidates fam_insts (idType var)
      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.
        Right candidates -> do
          missing_m <- flip concatMapM candidates $ \(va,tm_ct,ty_cs) -> do
            let all_ty_cs = unionBags ty_cs ty_css
            sat_ty <- tyOracle all_ty_cs
            return $ case (sat_ty, tmOracle tm_state (tm_ct:tm_css)) of
              (True, Just tm_state') -> [(va, all_ty_cs, tm_state')]
              _non_sat               -> []
          let mkValVec (va,all_ty_cs,tm_state')
                = ValVec [va] (MkDelta all_ty_cs tm_state')
              uncovered = UncoveredPatterns (map mkValVec missing_m)
          return $ if null missing_m
            then emptyPmResult
            else PmResult FromBuiltin [] uncovered []
    Nothing -> return emptyPmResult

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 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 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 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595
-- | 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

pmTopNormaliseType_maybe :: FamInstEnvs -> Type -> 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.
pmTopNormaliseType_maybe env typ
  = do ((ty_f,tm_f), ty) <- topNormaliseTypeX stepper comb typ
       return (eq_src_ty ty (typ : ty_f [ty]), tm_f [], 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 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
      = let (_args_co, ntys) = normaliseTcArgs env Representational tc 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 reduceTyFamApp_maybe env Representational tc ntys of
          Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id)
          _               -> NS_Done

{- 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 = 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 it's core representation, we keep track of the source data
      constructor.
  (c) core_ty is the rewritten type. That is,
        pmTopNormaliseType_maybe env 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 (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).
-}

596 597 598
-- | Generate all inhabitation candidates 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
Gabor Greif's avatar
Gabor Greif committed
599
-- can. In this case, the candidates are the signature of the tycon, each one
600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
-- accompanied by the term- and type- constraints it gives rise to.
-- See also Note [Checking EmptyCase Expressions]
inhabitationCandidates :: FamInstEnvs -> Type
                       -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
inhabitationCandidates fam_insts ty
  = case pmTopNormaliseType_maybe fam_insts ty of
      Just (src_ty, dcs, core_ty) -> alts_to_check src_ty core_ty dcs
      Nothing                     -> alts_to_check ty     ty      []
  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]
                  -> PmM (Either Type [(ValAbs, ComplexEq, Bag EvVar)])
    alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of
      Just (tc, _)
        | tc `elem` trivially_inhabited -> case dcs of
            []    -> return (Left src_ty)
            (_:_) -> do var <- liftD $ mkPmId (toTcType core_ty)
                        let va = build_tm (PmVar var) dcs
                        return $ Right [(va, mkIdEq var, emptyBag)]
629

630
        | pmIsClosedType core_ty -> liftD $ do
631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671
            var  <- mkPmId (toTcType core_ty) -- it would be wrong to unify x
            alts <- mapM (mkOneConFull var . RealDataCon) (tyConDataCons tc)
            return $ Right [(build_tm va dcs, eq, cs) | (va, eq, cs) <- alts]
      -- 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.

672 673 674 675 676
%************************************************************************
%*                                                                      *
              Transform source syntax to *our* syntax
%*                                                                      *
%************************************************************************
Austin Seipp's avatar
Austin Seipp committed
677
-}
sof's avatar
sof committed
678

679 680 681
-- -----------------------------------------------------------------------
-- * Utilities

682
nullaryConPattern :: ConLike -> Pattern
683
-- Nullary data constructor and nullary type constructor
684
nullaryConPattern con =
685 686
  PmCon { pm_con_con = con, pm_con_arg_tys = []
        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = [] }
687
{-# INLINE nullaryConPattern #-}
688 689

truePattern :: Pattern
690
truePattern = nullaryConPattern (RealDataCon trueDataCon)
691
{-# INLINE truePattern #-}
692 693 694

-- | A fake guard pattern (True <- _) used to represent cases we cannot handle
fake_pat :: Pattern
695
fake_pat = PmGrd { pm_grd_pv   = [truePattern]
696
                 , pm_grd_expr = PmExprOther (EWildPat noExt) }
697 698 699 700
{-# INLINE fake_pat #-}

-- | Check whether a guard pattern is generated by the checker (unhandled)
isFakeGuard :: [Pattern] -> PmExpr -> Bool
701
isFakeGuard [PmCon { pm_con_con = RealDataCon c }] (PmExprOther (EWildPat _))
702 703 704 705 706
  | c == trueDataCon = True
  | otherwise        = False
isFakeGuard _pats _e = False

-- | Generate a `canFail` pattern vector of a specific type
707
mkCanFailPmPat :: Type -> DsM PatVec
708 709 710
mkCanFailPmPat ty = do
  var <- mkPmVar ty
  return [var, fake_pat]
711

712
vanillaConPattern :: ConLike -> [Type] -> PatVec -> Pattern
713
-- ADT constructor pattern => no existentials, no local constraints
714
vanillaConPattern con arg_tys args =
715 716
  PmCon { pm_con_con = con, pm_con_arg_tys = arg_tys
        , pm_con_tvs = [], pm_con_dicts = [], pm_con_args = args }
717
{-# INLINE vanillaConPattern #-}
718

719
-- | Create an empty list pattern of a given type
720
nilPattern :: Type -> Pattern
721
nilPattern ty =
722
  PmCon { pm_con_con = RealDataCon nilDataCon, pm_con_arg_tys = [ty]
723 724
        , pm_con_tvs = [], pm_con_dicts = []
        , pm_con_args = [] }
725
{-# INLINE nilPattern #-}
726 727

mkListPatVec :: Type -> PatVec -> PatVec -> PatVec
728
mkListPatVec ty xs ys = [PmCon { pm_con_con = RealDataCon consDataCon
729 730 731
                               , pm_con_arg_tys = [ty]
                               , pm_con_tvs = [], pm_con_dicts = []
                               , pm_con_args = xs++ys }]
732
{-# INLINE mkListPatVec #-}
733

734
-- | Create a (non-overloaded) literal pattern
735
mkLitPattern :: HsLit GhcTc -> Pattern
736
mkLitPattern lit = PmLit { pm_lit_lit = PmSLit lit }
737
{-# INLINE mkLitPattern #-}
738 739 740 741

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

742
translatePat :: FamInstEnvs -> Pat GhcTc -> DsM PatVec
743
translatePat fam_insts pat = case pat of
744 745 746 747
  WildPat  ty  -> mkPmVars [ty]
  VarPat _ id  -> return [PmVar (unLoc id)]
  ParPat _ p   -> translatePat fam_insts (unLoc p)
  LazyPat _ _  -> mkPmVars [hsPatType pat] -- like a variable
748 749

  -- ignore strictness annotations for now
750
  BangPat _ p  -> translatePat fam_insts (unLoc p)
751

752
  AsPat _ lid p -> do
753
     -- Note [Translating As Patterns]
754
    ps <- translatePat fam_insts (unLoc p)
755
    let [e] = map vaToPmExpr (coercePatVec ps)
756
        g   = PmGrd [PmVar (unLoc lid)] e
757 758
    return (ps ++ [g])

759
  SigPat _ty p -> translatePat fam_insts (unLoc p)
760

761
  -- See Note [Translate CoPats]
762
  CoPat _ wrapper p ty
763 764
    | isIdHsWrapper wrapper                   -> translatePat fam_insts p
    | WpCast co <-  wrapper, isReflexiveCo co -> translatePat fam_insts p
765
    | otherwise -> do
766
        ps      <- translatePat fam_insts p
767
        (xp,xe) <- mkPmId2Forms ty
768
        let g = mkGuard ps (mkHsWrap wrapper (unLoc xe))
769
        return [xp,g]
770 771

  -- (n + k)  ===>   x (True <- x >= k) (n <- x-k)
772
  NPlusKPat ty (L _ _n) _k1 _k2 _ge _minus -> mkCanFailPmPat ty
773 774

  -- (fun -> pat)   ===>   x (pat <- fun x)
775
  ViewPat arg_ty lexpr lpat -> do
776
    ps <- translatePat fam_insts (unLoc lpat)
777 778 779
    -- See Note [Guards and Approximation]
    case all cantFailPattern ps of
      True  -> do
780
        (xp,xe) <- mkPmId2Forms arg_ty
781
        let g = mkGuard ps (HsApp noExt lexpr xe)
782
        return [xp,g]
783
      False -> mkCanFailPmPat arg_ty
784 785

  -- list
786
  ListPat (ListPatTc ty Nothing) ps -> do
787 788
    foldr (mkListPatVec ty) [nilPattern ty]
      <$> translatePatVec fam_insts (map unLoc ps)
789 790

  -- overloaded list
791
  ListPat (ListPatTc elem_ty (Just (pat_ty, _to_list))) lpats
792
    | Just e_ty <- splitListTyConApp_maybe pat_ty
793 794 795
    , (_, norm_e_ty) <- normaliseType fam_insts Nominal e_ty
         -- e_ty can be a type family instance, like
         -- `It (List a)`, but we prefer `a`, see Trac #14547
796
    , (_, norm_elem_ty) <- normaliseType fam_insts Nominal elem_ty
797 798
         -- elem_ty is frequently something like
         -- `Item [Int]`, but we prefer `Int`
799
    , norm_elem_ty `eqType` norm_e_ty ->
800 801 802
        -- We have to ensure that the element types are exactly the same.
        -- Otherwise, one may give an instance IsList [Int] (more specific than
        -- the default IsList [a]) with a different implementation for `toList'
803
        translatePat fam_insts (ListPat (ListPatTc e_ty Nothing) lpats)
804 805
      -- See Note [Guards and Approximation]
    | otherwise -> mkCanFailPmPat pat_ty
806

807
  ConPatOut { pat_con     = L _ con
808 809 810 811
            , pat_arg_tys = arg_tys
            , pat_tvs     = ex_tvs
            , pat_dicts   = dicts
            , pat_args    = ps } -> do
812 813 814 815 816 817 818 819 820 821
    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 }]
822

823
  NPat ty (L _ ol) mb_neg _eq -> translateNPat fam_insts ol mb_neg ty
824

825
  LitPat _ lit
826 827 828
      -- If it is a string then convert it to a list of characters
    | HsString src s <- lit ->
        foldr (mkListPatVec charTy) [nilPattern charTy] <$>
829 830
          translatePatVec fam_insts
                            (map (LitPat noExt  . HsChar src) (unpackFS s))
831 832
    | otherwise -> return [mkLitPattern lit]

833
  PArrPat ty ps -> do
834
    tidy_ps <- translatePatVec fam_insts (map unLoc ps)
835
    let fake_con = RealDataCon (parrFakeCon (length ps))
836 837
    return [vanillaConPattern fake_con [ty] (concat tidy_ps)]

838
  TuplePat tys ps boxity -> do
839
    tidy_ps <- translatePatVec fam_insts (map unLoc ps)
840
    let tuple_con = RealDataCon (tupleDataCon boxity (length ps))
841 842
    return [vanillaConPattern tuple_con tys (concat tidy_ps)]

843
  SumPat ty p alt arity -> do
844
    tidy_p <- translatePat fam_insts (unLoc p)
845
    let sum_con = RealDataCon (sumDataCon alt arity)
846 847
    return [vanillaConPattern sum_con ty tidy_p]

848 849 850 851
  -- --------------------------------------------------------------------------
  -- Not supposed to happen
  ConPatIn  {} -> panic "Check.translatePat: ConPatIn"
  SplicePat {} -> panic "Check.translatePat: SplicePat"
852
  XPat      {} -> panic "Check.translatePat: XPat"
853 854

-- | Translate an overloaded literal (see `tidyNPat' in deSugar/MatchLit.hs)
855
translateNPat :: FamInstEnvs
856 857
              -> HsOverLit GhcTc -> Maybe (SyntaxExpr GhcTc) -> Type
              -> DsM PatVec
858
translateNPat fam_insts (OverLit (OverLitTc False ty) val _ ) mb_neg outer_ty
859
  | not type_change, isStringTy ty, HsIsString src s <- val, Nothing <- mb_neg
860
  = translatePat fam_insts (LitPat noExt (HsString src s))
861 862
  | not type_change, isIntTy    ty, HsIntegral i <- val
  = translatePat fam_insts
863 864 865
                 (LitPat noExt $ case mb_neg of
                             Nothing -> HsInt noExt i
                             Just _  -> HsInt noExt (negateIntegralLit i))
866 867
  | not type_change, isWordTy   ty, HsIntegral i <- val
  = translatePat fam_insts
868
                 (LitPat noExt $ case mb_neg of
869 870 871
                             Nothing -> HsWordPrim (il_text i) (il_value i)
                             Just _  -> let ni = negateIntegralLit i in
                                        HsWordPrim (il_text ni) (il_value ni))
872
  where
873
    type_change = not (outer_ty `eqType` ty)
874

875
translateNPat _ ol mb_neg _
876
  = return [PmLit { pm_lit_lit = PmOLit (isJust mb_neg) ol }]
877 878 879

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

883
-- | Translate a constructor pattern
884
translateConPatVec :: FamInstEnvs -> [Type] -> [TyVar]
885
                   -> ConLike -> HsConPatDetails GhcTc -> DsM PatVec
886 887 888 889 890
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 _))
891
    -- Nothing matched. Make up some fresh term variables
892
  | null fs        = mkPmVars arg_tys
893 894 895
    -- 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.
896
  | null orig_lbls = ASSERT(null matched_lbls) mkPmVars arg_tys
897 898 899 900
    -- 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
901
  = ASSERT(orig_lbls `equalLength` arg_tys)
902
      let translateOne (lbl, ty) = case lookup lbl matched_pats of
903
            Just p  -> translatePat fam_insts p
904
            Nothing -> mkPmVars [ty]
905 906 907 908 909
      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
910
      arg_var_pats    <- mkPmVars arg_tys
911
      translated_pats <- forM matched_pats $ \(x,pat) -> do
912
        pvec <- translatePat fam_insts pat
913 914
        return (x, pvec)

915
      let zipped = zip orig_lbls [ x | PmVar x <- arg_var_pats ]
916
          guards = map (\(name,pvec) -> case lookup name zipped of
917
                            Just x  -> PmGrd pvec (PmExprVar (idName x))
918 919 920 921 922 923
                            Nothing -> panic "translateConPatVec: lookup")
                       translated_pats

      return (arg_var_pats ++ guards)
  where
    -- The actual argument types (instantiated)
924
    arg_tys = conLikeInstOrigArgTys c (univ_tys ++ mkTyVarTys ex_tvs)
925 926

    -- Some label information
927
    orig_lbls    = map flSelector $ conLikeFieldLabels c
928 929 930 931 932 933 934 935 936 937 938
    matched_pats = [ (getName (unLoc (hsRecFieldId x)), unLoc (hsRecFieldArg x))
                   | L _ x <- fs]
    matched_lbls = [ name | (name, _pat) <- matched_pats ]

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

939
-- Translate a single match
940 941
translateMatch :: FamInstEnvs -> LMatch GhcTc (LHsExpr GhcTc)
               -> DsM (PatVec,[PatVec])
942
translateMatch fam_insts (L _ (Match { m_pats = lpats, m_grhss = grhss })) = do
943 944
  pats'   <- concat <$> translatePatVec fam_insts pats
  guards' <- mapM (translateGuards fam_insts) guards
945 946
  return (pats', guards')
  where
947
    extractGuards :: LGRHS GhcTc (LHsExpr GhcTc) -> [GuardStmt GhcTc]
948 949
    extractGuards (L _ (GRHS _ gs _)) = map unLoc gs
    extractGuards (L _ (XGRHS _)) = panic "translateMatch"
950 951 952

    pats   = map unLoc lpats
    guards = map extractGuards (grhssGRHSs grhss)
953
translateMatch _ (L _ (XMatch _)) = panic "translateMatch"
954 955 956 957 958

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

-- | Translate a list of guard statements to a pattern vector
959
translateGuards :: FamInstEnvs -> [GuardStmt GhcTc] -> DsM PatVec
960 961
translateGuards fam_insts guards = do
  all_guards <- concat <$> mapM (translateGuard fam_insts) guards
962
  return (replace_unhandled all_guards)
963
  -- It should have been (return all_guards) but it is too expressive.
964 965 966 967 968 969 970 971 972 973 974 975 976 977 978
  -- 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 gv
      | any_unhandled gv = fake_pat : [ p | p <- gv, shouldKeep p ]
      | otherwise        = gv

    any_unhandled :: PatVec -> Bool
    any_unhandled gv = any (not . shouldKeep) gv

    shouldKeep :: Pattern -> Bool
979
    shouldKeep p
980
      | PmVar {} <- p      = True
981
      | PmCon {} <- p      = singleConstructor (pm_con_con p)
982
                             && all shouldKeep (pm_con_args p)
983
    shouldKeep (PmGrd pv e)
984 985 986 987 988 989
      | all shouldKeep pv  = True
      | isNotPmExprOther e = True  -- expensive but we want it
    shouldKeep _other_pat  = False -- let the rest..

-- | Check whether a pattern can fail to match
cantFailPattern :: Pattern -> Bool
990
cantFailPattern p
991
  | PmVar {} <- p = True
992
  | PmCon {} <- p = singleConstructor (pm_con_con p)
993
                    && all cantFailPattern (pm_con_args p)
994
cantFailPattern (PmGrd pv _e)