1{- 2Authors: George Karachalias <george.karachalias@cs.kuleuven.be> 3 Sebastian Graf <sgraf1337@gmail.com> 4 Ryan Scott <ryan.gl.scott@gmail.com> 5-} 6 7{-# LANGUAGE CPP, LambdaCase, TupleSections, PatternSynonyms, ViewPatterns, MultiWayIf #-} 8 9-- | The pattern match oracle. The main export of the module are the functions 10-- 'addTmCt', 'addVarCoreCt', 'addRefutableAltCon' and 'addTypeEvidence' for 11-- adding facts to the oracle, and 'provideEvidence' to turn a 12-- 'Delta' into a concrete evidence for an equation. 13module GHC.HsToCore.PmCheck.Oracle ( 14 15 DsM, tracePm, mkPmId, 16 Delta, initDelta, lookupRefuts, lookupSolution, 17 18 TmCt(..), 19 addTypeEvidence, -- Add type equalities 20 addRefutableAltCon, -- Add a negative term equality 21 addTmCt, -- Add a positive term equality x ~ e 22 addVarCoreCt, -- Add a positive term equality x ~ core_expr 23 canDiverge, -- Try to add the term equality x ~ ⊥ 24 provideEvidence, 25 ) where 26 27#include "HsVersions.h" 28 29import GhcPrelude 30 31import GHC.HsToCore.PmCheck.Types 32 33import DynFlags 34import Outputable 35import ErrUtils 36import Util 37import Bag 38import UniqSet 39import UniqDSet 40import Unique 41import Id 42import VarEnv 43import UniqDFM 44import Var (EvVar) 45import Name 46import CoreSyn 47import CoreFVs ( exprFreeVars ) 48import CoreMap 49import CoreOpt (simpleOptExpr, exprIsConApp_maybe) 50import CoreUtils (exprType) 51import MkCore (mkListExpr, mkCharExpr) 52import UniqSupply 53import FastString 54import SrcLoc 55import ListSetOps (unionLists) 56import Maybes 57import ConLike 58import DataCon 59import PatSyn 60import TyCon 61import TysWiredIn 62import TysPrim (tYPETyCon) 63import TyCoRep 64import Type 65import TcSimplify (tcNormalise, tcCheckSatisfiability) 66import TcType (evVarPred) 67import Unify (tcMatchTy) 68import TcRnTypes (completeMatchConLikes) 69import Coercion 70import MonadUtils hiding (foldlM) 71import DsMonad hiding (foldlM) 72import FamInst 73import FamInstEnv 74 75import Control.Monad (guard, mzero) 76import Control.Monad.Trans.Class (lift) 77import Control.Monad.Trans.State.Strict 78import Data.Bifunctor (second) 79import Data.Foldable (foldlM, minimumBy) 80import Data.List (find) 81import qualified Data.List.NonEmpty as NonEmpty 82import Data.Ord (comparing) 83import qualified Data.Semigroup as Semigroup 84import Data.Tuple (swap) 85 86-- Debugging Infrastructre 87 88tracePm :: String -> SDoc -> DsM () 89tracePm herald doc = do 90 dflags <- getDynFlags 91 printer <- mkPrintUnqualifiedDs 92 liftIO $ dumpIfSet_dyn_printer printer dflags 93 Opt_D_dump_ec_trace (text herald $$ (nest 2 doc)) 94 95-- | Generate a fresh `Id` of a given type 96mkPmId :: Type -> DsM Id 97mkPmId ty = getUniqueM >>= \unique -> 98 let occname = mkVarOccFS $ fsLit "pm" 99 name = mkInternalName unique occname noSrcSpan 100 in return (mkLocalId name ty) 101 102----------------------------------------------- 103-- * Caching possible matches of a COMPLETE set 104 105markMatched :: ConLike -> PossibleMatches -> PossibleMatches 106markMatched _ NoPM = NoPM 107markMatched con (PM ms) = PM (del_one_con con <$> ms) 108 where 109 del_one_con = flip delOneFromUniqDSet 110 111--------------------------------------------------- 112-- * Instantiating constructors, types and evidence 113 114-- | Instantiate a 'ConLike' given its universal type arguments. Instantiates 115-- existential and term binders with fresh variables of appropriate type. 116-- Returns instantiated term variables from the match, type evidence and the 117-- types of strict constructor fields. 118mkOneConFull :: [Type] -> ConLike -> DsM ([Id], Bag TyCt, [Type]) 119-- * 'con' K is a ConLike 120-- - In the case of DataCons and most PatSynCons, these 121-- are associated with a particular TyCon T 122-- - But there are PatSynCons for this is not the case! See #11336, #17112 123-- 124-- * 'arg_tys' tys are the types K's universally quantified type 125-- variables should be instantiated to. 126-- - For DataCons and most PatSyns these are the arguments of their TyCon 127-- - For cases like the PatSyns in #11336, #17112, we can't easily guess 128-- these, so don't call this function. 129-- 130-- After instantiating the universal tyvars of K to tys we get 131-- K @tys :: forall bs. Q => s1 .. sn -> T tys 132-- Note that if K is a PatSynCon, depending on arg_tys, T might not necessarily 133-- be a concrete TyCon. 134-- 135-- Suppose y1 is a strict field. Then we get 136-- Results: [y1,..,yn] 137-- Q 138-- [s1] 139mkOneConFull arg_tys con = do 140 let (univ_tvs, ex_tvs, eq_spec, thetas, _req_theta , field_tys, _con_res_ty) 141 = conLikeFullSig con 142 -- pprTrace "mkOneConFull" (ppr con $$ ppr arg_tys $$ ppr univ_tvs $$ ppr _con_res_ty) (return ()) 143 -- Substitute universals for type arguments 144 let subst_univ = zipTvSubst univ_tvs arg_tys 145 -- Instantiate fresh existentials as arguments to the contructor. This is 146 -- important for instantiating the Thetas and field types. 147 (subst, _) <- cloneTyVarBndrs subst_univ ex_tvs <$> getUniqueSupplyM 148 let field_tys' = substTys subst field_tys 149 -- Instantiate fresh term variables (VAs) as arguments to the constructor 150 vars <- mapM mkPmId field_tys' 151 -- All constraints bound by the constructor (alpha-renamed), these are added 152 -- to the type oracle 153 let ty_cs = map TyCt (substTheta subst (eqSpecPreds eq_spec ++ thetas)) 154 -- Figure out the types of strict constructor fields 155 let arg_is_strict 156 | RealDataCon dc <- con 157 , isNewTyCon (dataConTyCon dc) 158 = [True] -- See Note [Divergence of Newtype matches] 159 | otherwise 160 = map isBanged $ conLikeImplBangs con 161 strict_arg_tys = filterByList arg_is_strict field_tys' 162 return (vars, listToBag ty_cs, strict_arg_tys) 163 164------------------------- 165-- * Pattern match oracle 166 167 168{- Note [Recovering from unsatisfiable pattern-matching constraints] 169~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 170Consider the following code (see #12957 and #15450): 171 172 f :: Int ~ Bool => () 173 f = case True of { False -> () } 174 175We want to warn that the pattern-matching in `f` is non-exhaustive. But GHC 176used not to do this; in fact, it would warn that the match was /redundant/! 177This is because the constraint (Int ~ Bool) in `f` is unsatisfiable, and the 178coverage checker deems any matches with unsatifiable constraint sets to be 179unreachable. 180 181We decide to better than this. When beginning coverage checking, we first 182check if the constraints in scope are unsatisfiable, and if so, we start 183afresh with an empty set of constraints. This way, we'll get the warnings 184that we expect. 185-} 186 187------------------------------------- 188-- * Composable satisfiability checks 189 190-- | Given a 'Delta', check if it is compatible with new facts encoded in this 191-- this check. If so, return 'Just' a potentially extended 'Delta'. Return 192-- 'Nothing' if unsatisfiable. 193-- 194-- There are three essential SatisfiabilityChecks: 195-- 1. 'tmIsSatisfiable', adding term oracle facts 196-- 2. 'tyIsSatisfiable', adding type oracle facts 197-- 3. 'tysAreNonVoid', checks if the given types have an inhabitant 198-- Functions like 'pmIsSatisfiable', 'nonVoid' and 'testInhabited' plug these 199-- together as they see fit. 200newtype SatisfiabilityCheck = SC (Delta -> DsM (Maybe Delta)) 201 202-- | Check the given 'Delta' for satisfiability by the the given 203-- 'SatisfiabilityCheck'. Return 'Just' a new, potentially extended, 'Delta' if 204-- successful, and 'Nothing' otherwise. 205runSatisfiabilityCheck :: Delta -> SatisfiabilityCheck -> DsM (Maybe Delta) 206runSatisfiabilityCheck delta (SC chk) = chk delta 207 208-- | Allowing easy composition of 'SatisfiabilityCheck's. 209instance Semigroup SatisfiabilityCheck where 210 -- This is @a >=> b@ from MaybeT DsM 211 SC a <> SC b = SC c 212 where 213 c delta = a delta >>= \case 214 Nothing -> pure Nothing 215 Just delta' -> b delta' 216 217instance Monoid SatisfiabilityCheck where 218 -- We only need this because of mconcat (which we use in place of sconcat, 219 -- which requires NonEmpty lists as argument, making all call sites ugly) 220 mempty = SC (pure . Just) 221 222------------------------------- 223-- * Oracle transition function 224 225-- | Given a conlike's term constraints, type constraints, and strict argument 226-- types, check if they are satisfiable. 227-- (In other words, this is the ⊢_Sat oracle judgment from the GADTs Meet 228-- Their Match paper.) 229-- 230-- Taking strict argument types into account is something which was not 231-- discussed in GADTs Meet Their Match. For an explanation of what role they 232-- serve, see @Note [Strict argument type constraints]@. 233pmIsSatisfiable 234 :: Delta -- ^ The ambient term and type constraints 235 -- (known to be satisfiable). 236 -> Bag TmCt -- ^ The new term constraints. 237 -> Bag TyCt -- ^ The new type constraints. 238 -> [Type] -- ^ The strict argument types. 239 -> DsM (Maybe Delta) 240 -- ^ @'Just' delta@ if the constraints (@delta@) are 241 -- satisfiable, and each strict argument type is inhabitable. 242 -- 'Nothing' otherwise. 243pmIsSatisfiable amb_cs new_tm_cs new_ty_cs strict_arg_tys = 244 -- The order is important here! Check the new type constraints before we check 245 -- whether strict argument types are inhabited given those constraints. 246 runSatisfiabilityCheck amb_cs $ mconcat 247 [ tyIsSatisfiable True new_ty_cs 248 , tmIsSatisfiable new_tm_cs 249 , tysAreNonVoid initRecTc strict_arg_tys 250 ] 251 252----------------------- 253-- * Type normalisation 254 255-- | The return value of 'pmTopNormaliseType' 256data TopNormaliseTypeResult 257 = NoChange Type 258 -- ^ 'tcNormalise' failed to simplify the type and 'topNormaliseTypeX' was 259 -- unable to reduce the outermost type application, so the type came out 260 -- unchanged. 261 | NormalisedByConstraints Type 262 -- ^ 'tcNormalise' was able to simplify the type with some local constraint 263 -- from the type oracle, but 'topNormaliseTypeX' couldn't identify a type 264 -- redex. 265 | HadRedexes Type [(Type, DataCon, Type)] Type 266 -- ^ 'tcNormalise' may or may not been able to simplify the type, but 267 -- 'topNormaliseTypeX' made progress either way and got rid of at least one 268 -- outermost type or data family redex or newtype. 269 -- The first field is the last type that was reduced solely through type 270 -- family applications (possibly just the 'tcNormalise'd type). This is the 271 -- one that is equal (in source Haskell) to the initial type. 272 -- The third field is the type that we get when also looking through data 273 -- family applications and newtypes. This would be the representation type in 274 -- Core (modulo casts). 275 -- The second field is the list of Newtype 'DataCon's that we looked through 276 -- in the chain of reduction steps between the Source type and the Core type. 277 -- We also keep the type of the DataCon application and its field, so that we 278 -- don't have to reconstruct it in 'inhabitationCandidates' and 279 -- 'provideEvidence'. 280 -- For an example, see Note [Type normalisation]. 281 282-- | Just give me the potentially normalised source type, unchanged or not! 283normalisedSourceType :: TopNormaliseTypeResult -> Type 284normalisedSourceType (NoChange ty) = ty 285normalisedSourceType (NormalisedByConstraints ty) = ty 286normalisedSourceType (HadRedexes ty _ _) = ty 287 288-- | Return the fields of 'HadRedexes'. Returns appropriate defaults in the 289-- other cases. 290tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type) 291tntrGuts (NoChange ty) = (ty, [], ty) 292tntrGuts (NormalisedByConstraints ty) = (ty, [], ty) 293tntrGuts (HadRedexes src_ty ds core_ty) = (src_ty, ds, core_ty) 294 295instance Outputable TopNormaliseTypeResult where 296 ppr (NoChange ty) = text "NoChange" <+> ppr ty 297 ppr (NormalisedByConstraints ty) = text "NormalisedByConstraints" <+> ppr ty 298 ppr (HadRedexes src_ty ds core_ty) = text "HadRedexes" <+> braces fields 299 where 300 fields = fsep (punctuate comma [ text "src_ty =" <+> ppr src_ty 301 , text "newtype_dcs =" <+> ppr ds 302 , text "core_ty =" <+> ppr core_ty ]) 303 304pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult 305-- ^ Get rid of *outermost* (or toplevel) 306-- * type function redex 307-- * data family redex 308-- * newtypes 309-- 310-- Behaves like `topNormaliseType_maybe`, but instead of returning a 311-- coercion, it returns useful information for issuing pattern matching 312-- warnings. See Note [Type normalisation] for details. 313-- It also initially 'tcNormalise's the type with the bag of local constraints. 314-- 315-- See 'TopNormaliseTypeResult' for the meaning of the return value. 316-- 317-- NB: Normalisation can potentially change kinds, if the head of the type 318-- is a type family with a variable result kind. I (Richard E) can't think 319-- of a way to cause trouble here, though. 320pmTopNormaliseType (TySt inert) typ 321 = do env <- dsGetFamInstEnvs 322 -- Before proceeding, we chuck typ into the constraint solver, in case 323 -- solving for given equalities may reduce typ some. See 324 -- "Wrinkle: local equalities" in Note [Type normalisation]. 325 (_, mb_typ') <- initTcDsForSolver $ tcNormalise inert typ 326 -- If tcNormalise didn't manage to simplify the type, continue anyway. 327 -- We might be able to reduce type applications nonetheless! 328 let typ' = fromMaybe typ mb_typ' 329 -- Now we look with topNormaliseTypeX through type and data family 330 -- applications and newtypes, which tcNormalise does not do. 331 -- See also 'TopNormaliseTypeResult'. 332 pure $ case topNormaliseTypeX (stepper env) comb typ' of 333 Nothing 334 | Nothing <- mb_typ' -> NoChange typ 335 | otherwise -> NormalisedByConstraints typ' 336 Just ((ty_f,tm_f), ty) -> HadRedexes src_ty newtype_dcs core_ty 337 where 338 src_ty = eq_src_ty ty (typ' : ty_f [ty]) 339 newtype_dcs = tm_f [] 340 core_ty = ty 341 where 342 -- Find the first type in the sequence of rewrites that is a data type, 343 -- newtype, or a data family application (not the representation tycon!). 344 -- This is the one that is equal (in source Haskell) to the initial type. 345 -- If none is found in the list, then all of them are type family 346 -- applications, so we simply return the last one, which is the *simplest*. 347 eq_src_ty :: Type -> [Type] -> Type 348 eq_src_ty ty tys = maybe ty id (find is_closed_or_data_family tys) 349 350 is_closed_or_data_family :: Type -> Bool 351 is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyAppType ty 352 353 -- For efficiency, represent both lists as difference lists. 354 -- comb performs the concatenation, for both lists. 355 comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2) 356 357 stepper env = newTypeStepper `composeSteppers` tyFamStepper env 358 359 -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into 360 -- a loop. If it would fall into a loop, it produces 'NS_Abort'. 361 newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)]) 362 newTypeStepper rec_nts tc tys 363 | Just (ty', _co) <- instNewTyCon_maybe tc tys 364 , let orig_ty = TyConApp tc tys 365 = case checkRecTc rec_nts tc of 366 Just rec_nts' -> let tyf = (orig_ty:) 367 tmf = ((orig_ty, tyConSingleDataCon tc, ty'):) 368 in NS_Step rec_nts' ty' (tyf, tmf) 369 Nothing -> NS_Abort 370 | otherwise 371 = NS_Done 372 373 tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a) 374 tyFamStepper env rec_nts tc tys -- Try to step a type/data family 375 = let (_args_co, ntys, _res_co) = normaliseTcArgs env Representational tc tys in 376 -- NB: It's OK to use normaliseTcArgs here instead of 377 -- normalise_tc_args (which takes the LiftingContext described 378 -- in Note [Normalising types]) because the reduceTyFamApp below 379 -- works only at top level. We'll never recur in this function 380 -- after reducing the kind of a bound tyvar. 381 382 case reduceTyFamApp_maybe env Representational tc ntys of 383 Just (_co, rhs) -> NS_Step rec_nts rhs ((rhs:), id) 384 _ -> NS_Done 385 386-- | Returns 'True' if the argument 'Type' is a fully saturated application of 387-- a closed type constructor. 388-- 389-- Closed type constructors are those with a fixed right hand side, as 390-- opposed to e.g. associated types. These are of particular interest for 391-- pattern-match coverage checking, because GHC can exhaustively consider all 392-- possible forms that values of a closed type can take on. 393-- 394-- Note that this function is intended to be used to check types of value-level 395-- patterns, so as a consequence, the 'Type' supplied as an argument to this 396-- function should be of kind @Type@. 397pmIsClosedType :: Type -> Bool 398pmIsClosedType ty 399 = case splitTyConApp_maybe ty of 400 Just (tc, ty_args) 401 | is_algebraic_like tc && not (isFamilyTyCon tc) 402 -> ASSERT2( ty_args `lengthIs` tyConArity tc, ppr ty ) True 403 _other -> False 404 where 405 -- This returns True for TyCons which /act like/ algebraic types. 406 -- (See "Type#type_classification" for what an algebraic type is.) 407 -- 408 -- This is qualified with \"like\" because of a particular special 409 -- case: TYPE (the underlyind kind behind Type, among others). TYPE 410 -- is conceptually a datatype (and thus algebraic), but in practice it is 411 -- a primitive builtin type, so we must check for it specially. 412 -- 413 -- NB: it makes sense to think of TYPE as a closed type in a value-level, 414 -- pattern-matching context. However, at the kind level, TYPE is certainly 415 -- not closed! Since this function is specifically tailored towards pattern 416 -- matching, however, it's OK to label TYPE as closed. 417 is_algebraic_like :: TyCon -> Bool 418 is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon 419 420{- Note [Type normalisation] 421~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 422Constructs like -XEmptyCase or a previous unsuccessful pattern match on a data 423constructor place a non-void constraint on the matched thing. This means that it 424boils down to checking whether the type of the scrutinee is inhabited. Function 425pmTopNormaliseType gets rid of the outermost type function/data family redex and 426newtypes, in search of an algebraic type constructor, which is easier to check 427for inhabitation. 428 429It returns 3 results instead of one, because there are 2 subtle points: 4301. Newtypes are isomorphic to the underlying type in core but not in the source 431 language, 4322. The representational data family tycon is used internally but should not be 433 shown to the user 434 435Hence, if pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty), 436then 437 (a) src_ty is the rewritten type which we can show to the user. That is, the 438 type we get if we rewrite type families but not data families or 439 newtypes. 440 (b) dcs is the list of newtype constructors "skipped", every time we normalise 441 a newtype to its core representation, we keep track of the source data 442 constructor. For convenienve, we also track the type we unwrap and the 443 type of its field. Example: @Down 42@ => @[(Down @Int, Down, Int)] 444 (c) core_ty is the rewritten type. That is, 445 pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty) 446 implies 447 topNormaliseType_maybe env ty = Just (co, core_ty) 448 for some coercion co. 449 450To see how all cases come into play, consider the following example: 451 452 data family T a :: * 453 data instance T Int = T1 | T2 Bool 454 -- Which gives rise to FC: 455 -- data T a 456 -- data R:TInt = T1 | T2 Bool 457 -- axiom ax_ti : T Int ~R R:TInt 458 459 newtype G1 = MkG1 (T Int) 460 newtype G2 = MkG2 G1 461 462 type instance F Int = F Char 463 type instance F Char = G2 464 465In this case pmTopNormaliseType env ty_cs (F Int) results in 466 467 Just (G2, [(G2,MkG2,G1),(G1,MkG1,T Int)], R:TInt) 468 469Which means that in source Haskell: 470 - G2 is equivalent to F Int (in contrast, G1 isn't). 471 - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int). 472 473----- 474-- Wrinkle: Local equalities 475----- 476 477Given the following type family: 478 479 type family F a 480 type instance F Int = Void 481 482Should the following program (from #14813) be considered exhaustive? 483 484 f :: (i ~ Int) => F i -> a 485 f x = case x of {} 486 487You might think "of course, since `x` is obviously of type Void". But the 488idType of `x` is technically F i, not Void, so if we pass F i to 489inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive. 490In order to avoid this pitfall, we need to normalise the type passed to 491pmTopNormaliseType, using the constraint solver to solve for any local 492equalities (such as i ~ Int) that may be in scope. 493-} 494 495---------------- 496-- * Type oracle 497 498-- | Wraps a 'PredType', which is a constraint type. 499newtype TyCt = TyCt PredType 500 501instance Outputable TyCt where 502 ppr (TyCt pred_ty) = ppr pred_ty 503 504-- | Allocates a fresh 'EvVar' name for 'PredTyCt's, or simply returns the 505-- wrapped 'EvVar' for 'EvVarTyCt's. 506nameTyCt :: TyCt -> DsM EvVar 507nameTyCt (TyCt pred_ty) = do 508 unique <- getUniqueM 509 let occname = mkVarOccFS (fsLit ("pm_"++show unique)) 510 idname = mkInternalName unique occname noSrcSpan 511 return (mkLocalId idname pred_ty) 512 513-- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we 514-- find a contradiction (e.g. @Int ~ Bool@). 515tyOracle :: TyState -> Bag TyCt -> DsM (Maybe TyState) 516tyOracle (TySt inert) cts 517 = do { evs <- traverse nameTyCt cts 518 ; let new_inert = inert `unionBags` evs 519 ; tracePm "tyOracle" (ppr cts) 520 ; ((_warns, errs), res) <- initTcDsForSolver $ tcCheckSatisfiability new_inert 521 ; case res of 522 -- Note how this implicitly gives all former PredTyCts a name, so 523 -- that we don't needlessly re-allocate them every time! 524 Just True -> return (Just (TySt new_inert)) 525 Just False -> return Nothing 526 Nothing -> pprPanic "tyOracle" (vcat $ pprErrMsgBagWithLoc errs) } 527 528-- | A 'SatisfiabilityCheck' based on new type-level constraints. 529-- Returns a new 'Delta' if the new constraints are compatible with existing 530-- ones. Doesn't bother calling out to the type oracle if the bag of new type 531-- constraints was empty. Will only recheck 'PossibleMatches' in the term oracle 532-- for emptiness if the first argument is 'True'. 533tyIsSatisfiable :: Bool -> Bag TyCt -> SatisfiabilityCheck 534tyIsSatisfiable recheck_complete_sets new_ty_cs = SC $ \delta -> 535 if isEmptyBag new_ty_cs 536 then pure (Just delta) 537 else tyOracle (delta_ty_st delta) new_ty_cs >>= \case 538 Nothing -> pure Nothing 539 Just ty_st' -> do 540 let delta' = delta{ delta_ty_st = ty_st' } 541 if recheck_complete_sets 542 then ensureAllPossibleMatchesInhabited delta' 543 else pure (Just delta') 544 545 546{- ********************************************************************* 547* * 548 DIdEnv with sharing 549* * 550********************************************************************* -} 551 552 553{- ********************************************************************* 554* * 555 TmState 556 What we know about terms 557* * 558********************************************************************* -} 559 560{- Note [The Pos/Neg invariant] 561~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 562Invariant applying to each VarInfo: Whenever we have @(C, [y,z])@ in 'vi_pos', 563any entry in 'vi_neg' must be incomparable to C (return Nothing) according to 564'eqPmAltCons'. Those entries that are comparable either lead to a refutation 565or are redudant. Examples: 566* @x ~ Just y@, @x /~ [Just]@. 'eqPmAltCon' returns @Equal@, so refute. 567* @x ~ Nothing@, @x /~ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative 568 info is redundant and should be discarded. 569* @x ~ I# y@, @x /~ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal. 570 We keep this info in order to be able to refute a redundant match on i.e. 4 571 later on. 572 573This carries over to pattern synonyms and overloaded literals. Say, we have 574 pattern Just42 = Just 42 575 case Just42 of x 576 Nothing -> () 577 Just _ -> () 578Even though we had a solution for the value abstraction called x here in form 579of a PatSynCon (Just42,[]), this solution is incomparable to both Nothing and 580Just. Hence we retain the info in vi_neg, which eventually allows us to detect 581the complete pattern match. 582 583The Pos/Neg invariant extends to vi_cache, which stores essentially positive 584information. We make sure that vi_neg and vi_cache never overlap. This isn't 585strictly necessary since vi_cache is just a cache, so doesn't need to be 586accurate: Every suggestion of a possible ConLike from vi_cache might be 587refutable by the type oracle anyway. But it helps to maintain sanity while 588debugging traces. 589 590Note [Why record both positive and negative info?] 591~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 592You might think that knowing positive info (like x ~ Just y) would render 593negative info irrelevant, but not so because of pattern synonyms. E.g we might 594know that x cannot match (Foo 4), where pattern Foo p = Just p 595 596Also overloaded literals themselves behave like pattern synonyms. E.g if 597postively we know that (x ~ I# y), we might also negatively want to record that 598x does not match 45 f 45 = e2 f (I# 22#) = e3 f 45 = e4 -- 599Overlapped 600 601Note [TmState invariants] 602~~~~~~~~~~~~~~~~~~~~~~~~~ 603The term oracle state is never obviously (i.e., without consulting the type 604oracle) contradictory. This implies a few invariants: 605* Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute. 606 This is implied by the Note [Pos/Neg invariant]. 607* Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_cache to 608 detect this, but we could just compare whole COMPLETE sets to vi_neg every 609 time, if it weren't for performance. 610 611Maintaining these invariants in 'addVarVarCt' (the core of the term oracle) and 612'addRefutableAltCon' is subtle. 613* Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate'). 614 - (COMPLETE) If we had @x /~ True@ and @y /~ False@, then we get 615 @x /~ [True,False]@. This is vacuous by matter of comparing to the built-in 616 COMPLETE set, so should refute. 617 - (Pos/Neg) If we had @x /~ True@ and @y ~ True@, we have to refute. 618* Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addVarConCt') 619 - (Neg) If we had @x /~ K@, refute. 620 - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to 621 'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute. 622 - (Refine) If we had @x /~ K zs@, unify each y with each z in turn. 623* Adding negative information. Example: Add the fact @x /~ Nothing@ (see 'addRefutableAltCon') 624 - (Refut) If we have @x ~ K ys@, refute. 625 - (Redundant) If we have @x ~ K2@ and @eqPmAltCon K K2 == Disjoint@ 626 (ex. Just and Nothing), the info is redundant and can be 627 discarded. 628 - (COMPLETE) If K=Nothing and we had @x /~ Just@, then we get 629 @x /~ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in 630 COMPLETE set, so should refute. 631 632Note that merging VarInfo in equate can be done by calling out to 'addVarConCt' and 633'addRefutableAltCon' for each of the facts individually. 634 635Note [Representation of Strings in TmState] 636~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 637Instead of treating regular String literals as a PmLits, we treat it as a list 638of characters in the oracle for better overlap reasoning. The following example 639shows why: 640 641 f :: String -> () 642 f ('f':_) = () 643 f "foo" = () 644 f _ = () 645 646The second case is redundant, and we like to warn about it. Therefore either 647the oracle will have to do some smart conversion between the list and literal 648representation or treat is as the list it really is at runtime. 649 650The "smart conversion" has the advantage of leveraging the more compact literal 651representation wherever possible, but is really nasty to get right with negative 652equalities: Just think of how to encode @x /= "foo"@. 653The "list" option is far simpler, but incurs some overhead in representation and 654warning messages (which can be alleviated by someone with enough dedication). 655-} 656 657-- | A 'SatisfiabilityCheck' based on new term-level constraints. 658-- Returns a new 'Delta' if the new constraints are compatible with existing 659-- ones. 660tmIsSatisfiable :: Bag TmCt -> SatisfiabilityCheck 661tmIsSatisfiable new_tm_cs = SC $ \delta -> runMaybeT $ foldlM go delta new_tm_cs 662 where 663 go delta ct = MaybeT (addTmCt delta ct) 664 665----------------------- 666-- * Looking up VarInfo 667 668emptyVarInfo :: Id -> VarInfo 669emptyVarInfo x = VI (idType x) [] [] NoPM 670 671lookupVarInfo :: TmState -> Id -> VarInfo 672-- (lookupVarInfo tms x) tells what we know about 'x' 673lookupVarInfo (TmSt env _) x = fromMaybe (emptyVarInfo x) (lookupSDIE env x) 674 675initPossibleMatches :: TyState -> VarInfo -> DsM VarInfo 676initPossibleMatches ty_st vi@VI{ vi_ty = ty, vi_cache = NoPM } = do 677 -- New evidence might lead to refined info on ty, in turn leading to discovery 678 -- of a COMPLETE set. 679 res <- pmTopNormaliseType ty_st ty 680 let ty' = normalisedSourceType res 681 case splitTyConApp_maybe ty' of 682 Nothing -> pure vi{ vi_ty = ty' } 683 Just (tc, [_]) 684 | tc == tYPETyCon 685 -- TYPE acts like an empty data type on the term-level (#14086), but 686 -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a 687 -- special case. 688 -> pure vi{ vi_ty = ty', vi_cache = PM (pure emptyUniqDSet) } 689 Just (tc, tc_args) -> do 690 -- See Note [COMPLETE sets on data families] 691 (tc_rep, tc_fam) <- case tyConFamInst_maybe tc of 692 Just (tc_fam, _) -> pure (tc, tc_fam) 693 Nothing -> do 694 env <- dsGetFamInstEnvs 695 let (tc_rep, _tc_rep_args, _co) = tcLookupDataFamInst env tc tc_args 696 pure (tc_rep, tc) 697 -- Note that the common case here is tc_rep == tc_fam 698 let mb_rdcs = map RealDataCon <$> tyConDataCons_maybe tc_rep 699 let rdcs = maybeToList mb_rdcs 700 -- NB: tc_fam, because COMPLETE sets are associated with the parent data 701 -- family TyCon 702 pragmas <- dsGetCompleteMatches tc_fam 703 let fams = mapM dsLookupConLike . completeMatchConLikes 704 pscs <- mapM fams pragmas 705 -- pprTrace "initPossibleMatches" (ppr ty $$ ppr ty' $$ ppr tc_rep <+> ppr tc_fam <+> ppr tc_args $$ ppr (rdcs ++ pscs)) (return ()) 706 case NonEmpty.nonEmpty (rdcs ++ pscs) of 707 Nothing -> pure vi{ vi_ty = ty' } -- Didn't find any COMPLETE sets 708 Just cs -> pure vi{ vi_ty = ty', vi_cache = PM (mkUniqDSet <$> cs) } 709initPossibleMatches _ vi = pure vi 710 711-- | @initLookupVarInfo ts x@ looks up the 'VarInfo' for @x@ in @ts@ and tries 712-- to initialise the 'vi_cache' component if it was 'NoPM' through 713-- 'initPossibleMatches'. 714initLookupVarInfo :: Delta -> Id -> DsM VarInfo 715initLookupVarInfo MkDelta{ delta_tm_st = ts, delta_ty_st = ty_st } x 716 = initPossibleMatches ty_st (lookupVarInfo ts x) 717 718{- Note [COMPLETE sets on data families] 719~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 720User-defined COMPLETE sets involving data families are attached to the family 721TyCon, whereas the built-in COMPLETE set is attached to a data family instance's 722representation TyCon. This matters for COMPLETE sets involving both DataCons 723and PatSyns (from #17207): 724 725 data family T a 726 data family instance T () = A | B 727 pattern C = B 728 {-# COMPLETE A, C #-} 729 f :: T () -> () 730 f A = () 731 f C = () 732 733The match on A is actually wrapped in a CoPat, matching impedance between T () 734and its representation TyCon, which we translate as 735@x | let y = x |> co, A <- y@ in PmCheck. 736 737Which TyCon should we use for looking up the COMPLETE set? The representation 738TyCon from the match on A would only reveal the built-in COMPLETE set, while the 739data family TyCon would only give the user-defined one. But when initialising 740the PossibleMatches for a given Type, we want to do so only once, because 741merging different COMPLETE sets after the fact is very complicated and possibly 742inefficient. 743 744So in fact, we just *drop* the coercion arising from the CoPat when handling 745handling the constraint @y ~ x |> co@ in addVarCoreCt, just equating @y ~ x@. 746We then handle the fallout in initPossibleMatches, which has to get a hand at 747both the representation TyCon tc_rep and the parent data family TyCon tc_fam. 748It considers three cases after having established that the Type is a TyConApp: 749 7501. The TyCon is a vanilla data type constructor 7512. The TyCon is tc_rep 7523. The TyCon is tc_fam 753 7541. is simple and subsumed by the handling of the other two. 755We check for case 2. by 'tyConFamInst_maybe' and get the tc_fam out. 756Otherwise (3.), we try to lookup the data family instance at that particular 757type to get out the tc_rep. In case 1., this will just return the original 758TyCon, so tc_rep = tc_fam afterwards. 759-} 760 761------------------------------------------------ 762-- * Exported utility functions querying 'Delta' 763 764-- | Check whether adding a constraint @x ~ BOT@ to 'Delta' succeeds. 765canDiverge :: Delta -> Id -> Bool 766canDiverge delta@MkDelta{ delta_tm_st = ts } x 767 | VI _ pos neg _ <- lookupVarInfo ts x 768 = null neg && all pos_can_diverge pos 769 where 770 pos_can_diverge (PmAltConLike (RealDataCon dc), [y]) 771 -- See Note [Divergence of Newtype matches] 772 | isNewTyCon (dataConTyCon dc) = canDiverge delta y 773 pos_can_diverge _ = False 774 775{- Note [Divergence of Newtype matches] 776~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 777Newtypes behave rather strangely when compared to ordinary DataCons. In a 778pattern-match, they behave like a irrefutable (lazy) match, but for inhabitation 779testing purposes (e.g. at construction sites), they behave rather like a DataCon 780with a *strict* field, because they don't contribute their own bottom and are 781inhabited iff the wrapped type is inhabited. 782 783This distinction becomes apparent in #17248: 784 785 newtype T2 a = T2 a 786 g _ True = () 787 g (T2 _) True = () 788 g !_ True = () 789 790If we treat Newtypes like we treat regular DataCons, we would mark the third 791clause as redundant, which clearly is unsound. The solution: 7921. When checking the PmCon in 'pmCheck', never mark the result as Divergent if 793 it's a Newtype match. 7942. Regard @T2 x@ as 'canDiverge' iff @x@ 'canDiverge'. E.g. @T2 x ~ _|_@ <=> 795 @x ~ _|_@. This way, the third clause will still be marked as inaccessible 796 RHS instead of redundant. 7973. When testing for inhabitants ('mkOneConFull'), we regard the newtype field as 798 strict, so that the newtype is inhabited iff its field is inhabited. 799-} 800 801lookupRefuts :: Uniquable k => Delta -> k -> [PmAltCon] 802-- Unfortunately we need the extra bit of polymorphism and the unfortunate 803-- duplication of lookupVarInfo here. 804lookupRefuts MkDelta{ delta_tm_st = ts@(TmSt (SDIE env) _) } k = 805 case lookupUDFM env k of 806 Nothing -> [] 807 Just (Indirect y) -> vi_neg (lookupVarInfo ts y) 808 Just (Entry vi) -> vi_neg vi 809 810isDataConSolution :: (PmAltCon, [Id]) -> Bool 811isDataConSolution (PmAltConLike (RealDataCon _), _) = True 812isDataConSolution _ = False 813 814-- @lookupSolution delta x@ picks a single solution ('vi_pos') of @x@ from 815-- possibly many, preferring 'RealDataCon' solutions whenever possible. 816lookupSolution :: Delta -> Id -> Maybe (PmAltCon, [Id]) 817lookupSolution delta x = case vi_pos (lookupVarInfo (delta_tm_st delta) x) of 818 [] -> Nothing 819 pos 820 | Just sol <- find isDataConSolution pos -> Just sol 821 | otherwise -> Just (head pos) 822 823------------------------------- 824-- * Adding facts to the oracle 825 826-- | A term constraint. Either equates two variables or a variable with a 827-- 'PmAltCon' application. 828data TmCt 829 = TmVarVar !Id !Id 830 | TmVarCon !Id !PmAltCon ![Id] 831 | TmVarNonVoid !Id 832 833instance Outputable TmCt where 834 ppr (TmVarVar x y) = ppr x <+> char '~' <+> ppr y 835 ppr (TmVarCon x con args) = ppr x <+> char '~' <+> hsep (ppr con : map ppr args) 836 ppr (TmVarNonVoid x) = ppr x <+> text "/~ ⊥" 837 838-- | Add type equalities to 'Delta'. 839addTypeEvidence :: Delta -> Bag EvVar -> DsM (Maybe Delta) 840addTypeEvidence delta dicts 841 = runSatisfiabilityCheck delta (tyIsSatisfiable True (TyCt . evVarPred <$> dicts)) 842 843-- | Tries to equate two representatives in 'Delta'. 844-- See Note [TmState invariants]. 845addTmCt :: Delta -> TmCt -> DsM (Maybe Delta) 846addTmCt delta ct = runMaybeT $ case ct of 847 TmVarVar x y -> addVarVarCt delta (x, y) 848 TmVarCon x con args -> addVarConCt delta x con args 849 TmVarNonVoid x -> addVarNonVoidCt delta x 850 851-- | Record that a particular 'Id' can't take the shape of a 'PmAltCon' in the 852-- 'Delta' and return @Nothing@ if that leads to a contradiction. 853-- See Note [TmState invariants]. 854addRefutableAltCon :: Delta -> Id -> PmAltCon -> DsM (Maybe Delta) 855addRefutableAltCon delta@MkDelta{ delta_tm_st = TmSt env reps } x nalt = runMaybeT $ do 856 vi@(VI _ pos neg pm) <- lift (initLookupVarInfo delta x) 857 -- 1. Bail out quickly when nalt contradicts a solution 858 let contradicts nalt (cl, _args) = eqPmAltCon cl nalt == Equal 859 guard (not (any (contradicts nalt) pos)) 860 -- 2. Only record the new fact when it's not already implied by one of the 861 -- solutions 862 let implies nalt (cl, _args) = eqPmAltCon cl nalt == Disjoint 863 let neg' 864 | any (implies nalt) pos = neg 865 -- See Note [Completeness checking with required Thetas] 866 | hasRequiredTheta nalt = neg 867 | otherwise = unionLists neg [nalt] 868 let vi_ext = vi{ vi_neg = neg' } 869 -- 3. Make sure there's at least one other possible constructor 870 vi' <- case nalt of 871 PmAltConLike cl 872 -> MaybeT (ensureInhabited delta vi_ext{ vi_cache = markMatched cl pm }) 873 _ -> pure vi_ext 874 pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') reps } 875 876hasRequiredTheta :: PmAltCon -> Bool 877hasRequiredTheta (PmAltConLike cl) = notNull req_theta 878 where 879 (_,_,_,_,req_theta,_,_) = conLikeFullSig cl 880hasRequiredTheta _ = False 881 882{- Note [Completeness checking with required Thetas] 883~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 884Consider the situation in #11224 885 886 import Text.Read (readMaybe) 887 pattern PRead :: Read a => () => a -> String 888 pattern PRead x <- (readMaybe -> Just x) 889 f :: String -> Int 890 f (PRead x) = x 891 f (PRead xs) = length xs 892 f _ = 0 893 894Is the first match exhaustive on the PRead synonym? Should the second line thus 895deemed redundant? The answer is, of course, No! The required theta is like a 896hidden parameter which must be supplied at the pattern match site, so PRead 897is much more like a view pattern (where behavior depends on the particular value 898passed in). 899The simple solution here is to forget in 'addRefutableAltCon' that we matched 900on synonyms with a required Theta like @PRead@, so that subsequent matches on 901the same constructor are never flagged as redundant. The consequence is that 902we no longer detect the actually redundant match in 903 904 g :: String -> Int 905 g (PRead x) = x 906 g (PRead y) = y -- redundant! 907 g _ = 0 908 909But that's a small price to pay, compared to the proper solution here involving 910storing required arguments along with the PmAltConLike in 'vi_neg'. 911-} 912 913-- | Guess the universal argument types of a ConLike from an instantiation of 914-- its result type. Rather easy for DataCons, but not so much for PatSynCons. 915-- See Note [Pattern synonym result type] in PatSyn.hs. 916guessConLikeUnivTyArgsFromResTy :: FamInstEnvs -> Type -> ConLike -> Maybe [Type] 917guessConLikeUnivTyArgsFromResTy env res_ty (RealDataCon _) = do 918 (tc, tc_args) <- splitTyConApp_maybe res_ty 919 -- Consider data families: In case of a DataCon, we need to translate to 920 -- the representation TyCon. For PatSyns, they are relative to the data 921 -- family TyCon, so we don't need to translate them. 922 let (_, tc_args', _) = tcLookupDataFamInst env tc tc_args 923 Just tc_args' 924guessConLikeUnivTyArgsFromResTy _ res_ty (PatSynCon ps) = do 925 -- We are successful if we managed to instantiate *every* univ_tv of con. 926 -- This is difficult and bound to fail in some cases, see 927 -- Note [Pattern synonym result type] in PatSyn.hs. So we just try our best 928 -- here and be sure to return an instantiation when we can substitute every 929 -- universally quantified type variable. 930 -- We *could* instantiate all the other univ_tvs just to fresh variables, I 931 -- suppose, but that means we get weird field types for which we don't know 932 -- anything. So we prefer to keep it simple here. 933 let (univ_tvs,_,_,_,_,con_res_ty) = patSynSig ps 934 subst <- tcMatchTy con_res_ty res_ty 935 traverse (lookupTyVar subst) univ_tvs 936 937-- | Kind of tries to add a non-void contraint to 'Delta', but doesn't really 938-- commit to upholding that constraint in the future. This will be rectified 939-- in a follow-up patch. The status quo should work good enough for now. 940addVarNonVoidCt :: Delta -> Id -> MaybeT DsM Delta 941addVarNonVoidCt delta@MkDelta{ delta_tm_st = TmSt env reps } x = do 942 vi <- lift $ initLookupVarInfo delta x 943 vi' <- MaybeT $ ensureInhabited delta vi 944 -- vi' has probably constructed and then thinned out some PossibleMatches. 945 -- We want to cache that work 946 pure delta{ delta_tm_st = TmSt (setEntrySDIE env x vi') reps} 947 948ensureInhabited :: Delta -> VarInfo -> DsM (Maybe VarInfo) 949 -- Returns (Just vi) if at least one member of each ConLike in the COMPLETE 950 -- set satisfies the oracle 951 -- 952 -- Internally uses and updates the ConLikeSets in vi_cache. 953 -- 954 -- NB: Does /not/ filter each ConLikeSet with the oracle; members may 955 -- remain that do not statisfy it. This lazy approach just 956 -- avoids doing unnecessary work. 957ensureInhabited delta vi = fmap (set_cache vi) <$> test (vi_cache vi) -- This would be much less tedious with lenses 958 where 959 set_cache vi cache = vi { vi_cache = cache } 960 961 test NoPM = pure (Just NoPM) 962 test (PM ms) = runMaybeT (PM <$> traverse one_set ms) 963 964 one_set cs = find_one_inh cs (uniqDSetToList cs) 965 966 find_one_inh :: ConLikeSet -> [ConLike] -> MaybeT DsM ConLikeSet 967 -- (find_one_inh cs cls) iterates over cls, deleting from cs 968 -- any uninhabited elements of cls. Stop (returning Just cs) 969 -- when you see an inhabited element; return Nothing if all 970 -- are uninhabited 971 find_one_inh _ [] = mzero 972 find_one_inh cs (con:cons) = lift (inh_test con) >>= \case 973 True -> pure cs 974 False -> find_one_inh (delOneFromUniqDSet cs con) cons 975 976 inh_test :: ConLike -> DsM Bool 977 -- @inh_test K@ Returns False if a non-bottom value @v::ty@ cannot possibly 978 -- be of form @K _ _ _@. Returning True is always sound. 979 -- 980 -- It's like 'DataCon.dataConCannotMatch', but more clever because it takes 981 -- the facts in Delta into account. 982 inh_test con = do 983 env <- dsGetFamInstEnvs 984 case guessConLikeUnivTyArgsFromResTy env (vi_ty vi) con of 985 Nothing -> pure True -- be conservative about this 986 Just arg_tys -> do 987 (_vars, ty_cs, strict_arg_tys) <- mkOneConFull arg_tys con 988 tracePm "inh_test" (ppr con $$ ppr ty_cs) 989 -- No need to run the term oracle compared to pmIsSatisfiable 990 fmap isJust <$> runSatisfiabilityCheck delta $ mconcat 991 -- Important to pass False to tyIsSatisfiable here, so that we won't 992 -- recursively call ensureAllPossibleMatchesInhabited, leading to an 993 -- endless recursion. 994 [ tyIsSatisfiable False ty_cs 995 , tysAreNonVoid initRecTc strict_arg_tys 996 ] 997 998-- | Checks if every 'VarInfo' in the term oracle has still an inhabited 999-- 'vi_cache', considering the current type information in 'Delta'. 1000-- This check is necessary after having matched on a GADT con to weed out 1001-- impossible matches. 1002ensureAllPossibleMatchesInhabited :: Delta -> DsM (Maybe Delta) 1003ensureAllPossibleMatchesInhabited delta@MkDelta{ delta_tm_st = TmSt env reps } 1004 = runMaybeT (set_tm_cs_env delta <$> traverseSDIE go env) 1005 where 1006 set_tm_cs_env delta env = delta{ delta_tm_st = TmSt env reps } 1007 go vi = MaybeT (ensureInhabited delta vi) 1008 1009-------------------------------------- 1010-- * Term oracle unification procedure 1011 1012-- | Try to unify two 'Id's and record the gained knowledge in 'Delta'. 1013-- 1014-- Returns @Nothing@ when there's a contradiction. Returns @Just delta@ 1015-- when the constraint was compatible with prior facts, in which case @delta@ 1016-- has integrated the knowledge from the equality constraint. 1017-- 1018-- See Note [TmState invariants]. 1019addVarVarCt :: Delta -> (Id, Id) -> MaybeT DsM Delta 1020addVarVarCt delta@MkDelta{ delta_tm_st = TmSt env _ } (x, y) 1021 -- It's important that we never @equate@ two variables of the same equivalence 1022 -- class, otherwise we might get cyclic substitutions. 1023 -- Cf. 'extendSubstAndSolve' and 1024 -- @testsuite/tests/pmcheck/should_compile/CyclicSubst.hs@. 1025 | sameRepresentativeSDIE env x y = pure delta 1026 | otherwise = equate delta x y 1027 1028-- | @equate ts@(TmSt env) x y@ merges the equivalence classes of @x@ and @y@ by 1029-- adding an indirection to the environment. 1030-- Makes sure that the positive and negative facts of @x@ and @y@ are 1031-- compatible. 1032-- Preconditions: @not (sameRepresentativeSDIE env x y)@ 1033-- 1034-- See Note [TmState invariants]. 1035equate :: Delta -> Id -> Id -> MaybeT DsM Delta 1036equate delta@MkDelta{ delta_tm_st = TmSt env reps } x y 1037 = ASSERT( not (sameRepresentativeSDIE env x y) ) 1038 case (lookupSDIE env x, lookupSDIE env y) of 1039 (Nothing, _) -> pure (delta{ delta_tm_st = TmSt (setIndirectSDIE env x y) reps }) 1040 (_, Nothing) -> pure (delta{ delta_tm_st = TmSt (setIndirectSDIE env y x) reps }) 1041 -- Merge the info we have for x into the info for y 1042 (Just vi_x, Just vi_y) -> do 1043 -- This assert will probably trigger at some point... 1044 -- We should decide how to break the tie 1045 MASSERT2( vi_ty vi_x `eqType` vi_ty vi_y, text "Not same type" ) 1046 -- First assume that x and y are in the same equivalence class 1047 let env_ind = setIndirectSDIE env x y 1048 -- Then sum up the refinement counters 1049 let env_refs = setEntrySDIE env_ind y vi_y 1050 let delta_refs = delta{ delta_tm_st = TmSt env_refs reps } 1051 -- and then gradually merge every positive fact we have on x into y 1052 let add_fact delta (cl, args) = addVarConCt delta y cl args 1053 delta_pos <- foldlM add_fact delta_refs (vi_pos vi_x) 1054 -- Do the same for negative info 1055 let add_refut delta nalt = MaybeT (addRefutableAltCon delta y nalt) 1056 delta_neg <- foldlM add_refut delta_pos (vi_neg vi_x) 1057 -- vi_cache will be updated in addRefutableAltCon, so we are good to 1058 -- go! 1059 pure delta_neg 1060 1061-- | @addVarConCt x alt args ts@ extends the substitution with a solution 1062-- @x :-> (alt, args)@ if compatible with refutable shapes of @x@ and its 1063-- other solutions, reject (@Nothing@) otherwise. 1064-- 1065-- See Note [TmState invariants]. 1066addVarConCt :: Delta -> Id -> PmAltCon -> [Id] -> MaybeT DsM Delta 1067addVarConCt delta@MkDelta{ delta_tm_st = TmSt env reps } x alt args = do 1068 VI ty pos neg cache <- lift (initLookupVarInfo delta x) 1069 -- First try to refute with a negative fact 1070 guard (all ((/= Equal) . eqPmAltCon alt) neg) 1071 -- Then see if any of the other solutions (remember: each of them is an 1072 -- additional refinement of the possible values x could take) indicate a 1073 -- contradiction 1074 guard (all ((/= Disjoint) . eqPmAltCon alt . fst) pos) 1075 -- Now we should be good! Add (alt, args) as a possible solution, or refine an 1076 -- existing one 1077 case find ((== Equal) . eqPmAltCon alt . fst) pos of 1078 Just (_, other_args) -> do 1079 foldlM addVarVarCt delta (zip args other_args) 1080 Nothing -> do 1081 -- Filter out redundant negative facts (those that compare Just False to 1082 -- the new solution) 1083 let neg' = filter ((== PossiblyOverlap) . eqPmAltCon alt) neg 1084 let pos' = (alt,args):pos 1085 pure delta{ delta_tm_st = TmSt (setEntrySDIE env x (VI ty pos' neg' cache)) reps} 1086 1087---------------------------------------- 1088-- * Enumerating inhabitation candidates 1089 1090-- | Information about a conlike that is relevant to coverage checking. 1091-- It is called an \"inhabitation candidate\" since it is a value which may 1092-- possibly inhabit some type, but only if its term constraints ('ic_tm_cs') 1093-- and type constraints ('ic_ty_cs') are permitting, and if all of its strict 1094-- argument types ('ic_strict_arg_tys') are inhabitable. 1095-- See @Note [Strict argument type constraints]@. 1096data InhabitationCandidate = 1097 InhabitationCandidate 1098 { ic_tm_cs :: Bag TmCt 1099 , ic_ty_cs :: Bag TyCt 1100 , ic_strict_arg_tys :: [Type] 1101 } 1102 1103instance Outputable InhabitationCandidate where 1104 ppr (InhabitationCandidate tm_cs ty_cs strict_arg_tys) = 1105 text "InhabitationCandidate" <+> 1106 vcat [ text "ic_tm_cs =" <+> ppr tm_cs 1107 , text "ic_ty_cs =" <+> ppr ty_cs 1108 , text "ic_strict_arg_tys =" <+> ppr strict_arg_tys ] 1109 1110mkInhabitationCandidate :: Id -> DataCon -> DsM InhabitationCandidate 1111-- Precondition: idType x is a TyConApp, so that tyConAppArgs in here is safe. 1112mkInhabitationCandidate x dc = do 1113 let cl = RealDataCon dc 1114 let tc_args = tyConAppArgs (idType x) 1115 (arg_vars, ty_cs, strict_arg_tys) <- mkOneConFull tc_args cl 1116 pure InhabitationCandidate 1117 { ic_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars) 1118 , ic_ty_cs = ty_cs 1119 , ic_strict_arg_tys = strict_arg_tys 1120 } 1121 1122-- | Generate all 'InhabitationCandidate's for a given type. The result is 1123-- either @'Left' ty@, if the type cannot be reduced to a closed algebraic type 1124-- (or if it's one trivially inhabited, like 'Int'), or @'Right' candidates@, 1125-- if it can. In this case, the candidates are the signature of the tycon, each 1126-- one accompanied by the term- and type- constraints it gives rise to. 1127-- See also Note [Checking EmptyCase Expressions] 1128inhabitationCandidates :: Delta -> Type 1129 -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])) 1130inhabitationCandidates MkDelta{ delta_ty_st = ty_st } ty = do 1131 pmTopNormaliseType ty_st ty >>= \case 1132 NoChange _ -> alts_to_check ty ty [] 1133 NormalisedByConstraints ty' -> alts_to_check ty' ty' [] 1134 HadRedexes src_ty dcs core_ty -> alts_to_check src_ty core_ty dcs 1135 where 1136 build_newtype :: (Type, DataCon, Type) -> Id -> DsM (Id, TmCt) 1137 build_newtype (ty, dc, _arg_ty) x = do 1138 -- ty is the type of @dc x@. It's a @dataConTyCon dc@ application. 1139 y <- mkPmId ty 1140 pure (y, TmVarCon y (PmAltConLike (RealDataCon dc)) [x]) 1141 1142 build_newtypes :: Id -> [(Type, DataCon, Type)] -> DsM (Id, [TmCt]) 1143 build_newtypes x = foldrM (\dc (x, cts) -> go dc x cts) (x, []) 1144 where 1145 go dc x cts = second (:cts) <$> build_newtype dc x 1146 1147 -- Inhabitation candidates, using the result of pmTopNormaliseType 1148 alts_to_check :: Type -> Type -> [(Type, DataCon, Type)] 1149 -> DsM (Either Type (TyCon, Id, [InhabitationCandidate])) 1150 alts_to_check src_ty core_ty dcs = case splitTyConApp_maybe core_ty of 1151 Just (tc, _) 1152 | isTyConTriviallyInhabited tc 1153 -> case dcs of 1154 [] -> return (Left src_ty) 1155 (_:_) -> do inner <- mkPmId core_ty 1156 (outer, new_tm_cts) <- build_newtypes inner dcs 1157 return $ Right (tc, outer, [InhabitationCandidate 1158 { ic_tm_cs = listToBag new_tm_cts 1159 , ic_ty_cs = emptyBag, ic_strict_arg_tys = [] }]) 1160 1161 | pmIsClosedType core_ty && not (isAbstractTyCon tc) 1162 -- Don't consider abstract tycons since we don't know what their 1163 -- constructors are, which makes the results of coverage checking 1164 -- them extremely misleading. 1165 -> do 1166 inner <- mkPmId core_ty -- it would be wrong to unify inner 1167 alts <- mapM (mkInhabitationCandidate inner) (tyConDataCons tc) 1168 (outer, new_tm_cts) <- build_newtypes inner dcs 1169 let wrap_dcs alt = alt{ ic_tm_cs = listToBag new_tm_cts `unionBags` ic_tm_cs alt} 1170 return $ Right (tc, outer, map wrap_dcs alts) 1171 -- For other types conservatively assume that they are inhabited. 1172 _other -> return (Left src_ty) 1173 1174-- | All these types are trivially inhabited 1175triviallyInhabitedTyCons :: UniqSet TyCon 1176triviallyInhabitedTyCons = mkUniqSet [ 1177 charTyCon, doubleTyCon, floatTyCon, intTyCon, wordTyCon, word8TyCon 1178 ] 1179 1180isTyConTriviallyInhabited :: TyCon -> Bool 1181isTyConTriviallyInhabited tc = elementOfUniqSet tc triviallyInhabitedTyCons 1182 1183---------------------------- 1184-- * Detecting vacuous types 1185 1186{- Note [Checking EmptyCase Expressions] 1187~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1188Empty case expressions are strict on the scrutinee. That is, `case x of {}` 1189will force argument `x`. Hence, `checkMatches` is not sufficient for checking 1190empty cases, because it assumes that the match is not strict (which is true 1191for all other cases, apart from EmptyCase). This gave rise to #10746. Instead, 1192we do the following: 1193 11941. We normalise the outermost type family redex, data family redex or newtype, 1195 using pmTopNormaliseType (in types/FamInstEnv.hs). This computes 3 1196 things: 1197 (a) A normalised type src_ty, which is equal to the type of the scrutinee in 1198 source Haskell (does not normalise newtypes or data families) 1199 (b) The actual normalised type core_ty, which coincides with the result 1200 topNormaliseType_maybe. This type is not necessarily equal to the input 1201 type in source Haskell. And this is precicely the reason we compute (a) 1202 and (c): the reasoning happens with the underlying types, but both the 1203 patterns and types we print should respect newtypes and also show the 1204 family type constructors and not the representation constructors. 1205 1206 (c) A list of all newtype data constructors dcs, each one corresponding to a 1207 newtype rewrite performed in (b). 1208 1209 For an example see also Note [Type normalisation] 1210 in types/FamInstEnv.hs. 1211 12122. Function Check.checkEmptyCase' performs the check: 1213 - If core_ty is not an algebraic type, then we cannot check for 1214 inhabitation, so we emit (_ :: src_ty) as missing, conservatively assuming 1215 that the type is inhabited. 1216 - If core_ty is an algebraic type, then we unfold the scrutinee to all 1217 possible constructor patterns, using inhabitationCandidates, and then 1218 check each one for constraint satisfiability, same as we do for normal 1219 pattern match checking. 1220-} 1221 1222-- | A 'SatisfiabilityCheck' based on "NonVoid ty" constraints, e.g. Will 1223-- check if the @strict_arg_tys@ are actually all inhabited. 1224-- Returns the old 'Delta' if all the types are non-void according to 'Delta'. 1225tysAreNonVoid :: RecTcChecker -> [Type] -> SatisfiabilityCheck 1226tysAreNonVoid rec_env strict_arg_tys = SC $ \delta -> do 1227 all_non_void <- checkAllNonVoid rec_env delta strict_arg_tys 1228 -- Check if each strict argument type is inhabitable 1229 pure $ if all_non_void 1230 then Just delta 1231 else Nothing 1232 1233-- | Implements two performance optimizations, as described in 1234-- @Note [Strict argument type constraints]@. 1235checkAllNonVoid :: RecTcChecker -> Delta -> [Type] -> DsM Bool 1236checkAllNonVoid rec_ts amb_cs strict_arg_tys = do 1237 let definitely_inhabited = definitelyInhabitedType (delta_ty_st amb_cs) 1238 tys_to_check <- filterOutM definitely_inhabited strict_arg_tys 1239 -- See Note [Fuel for the inhabitation test] 1240 let rec_max_bound | tys_to_check `lengthExceeds` 1 1241 = 1 1242 | otherwise 1243 = 3 1244 rec_ts' = setRecTcMaxBound rec_max_bound rec_ts 1245 allM (nonVoid rec_ts' amb_cs) tys_to_check 1246 1247-- | Checks if a strict argument type of a conlike is inhabitable by a 1248-- terminating value (i.e, an 'InhabitationCandidate'). 1249-- See @Note [Strict argument type constraints]@. 1250nonVoid 1251 :: RecTcChecker -- ^ The per-'TyCon' recursion depth limit. 1252 -> Delta -- ^ The ambient term/type constraints (known to be 1253 -- satisfiable). 1254 -> Type -- ^ The strict argument type. 1255 -> DsM Bool -- ^ 'True' if the strict argument type might be inhabited by 1256 -- a terminating value (i.e., an 'InhabitationCandidate'). 1257 -- 'False' if it is definitely uninhabitable by anything 1258 -- (except bottom). 1259nonVoid rec_ts amb_cs strict_arg_ty = do 1260 mb_cands <- inhabitationCandidates amb_cs strict_arg_ty 1261 case mb_cands of 1262 Right (tc, _, cands) 1263 -- See Note [Fuel for the inhabitation test] 1264 | Just rec_ts' <- checkRecTc rec_ts tc 1265 -> anyM (cand_is_inhabitable rec_ts' amb_cs) cands 1266 -- A strict argument type is inhabitable by a terminating value if 1267 -- at least one InhabitationCandidate is inhabitable. 1268 _ -> pure True 1269 -- Either the type is trivially inhabited or we have exceeded the 1270 -- recursion depth for some TyCon (so bail out and conservatively 1271 -- claim the type is inhabited). 1272 where 1273 -- Checks if an InhabitationCandidate for a strict argument type: 1274 -- 1275 -- (1) Has satisfiable term and type constraints. 1276 -- (2) Has 'nonVoid' strict argument types (we bail out of this 1277 -- check if recursion is detected). 1278 -- 1279 -- See Note [Strict argument type constraints] 1280 cand_is_inhabitable :: RecTcChecker -> Delta 1281 -> InhabitationCandidate -> DsM Bool 1282 cand_is_inhabitable rec_ts amb_cs 1283 (InhabitationCandidate{ ic_tm_cs = new_tm_cs 1284 , ic_ty_cs = new_ty_cs 1285 , ic_strict_arg_tys = new_strict_arg_tys }) = 1286 fmap isJust $ runSatisfiabilityCheck amb_cs $ mconcat 1287 [ tyIsSatisfiable False new_ty_cs 1288 , tmIsSatisfiable new_tm_cs 1289 , tysAreNonVoid rec_ts new_strict_arg_tys 1290 ] 1291 1292-- | @'definitelyInhabitedType' ty@ returns 'True' if @ty@ has at least one 1293-- constructor @C@ such that: 1294-- 1295-- 1. @C@ has no equality constraints. 1296-- 2. @C@ has no strict argument types. 1297-- 1298-- See the @Note [Strict argument type constraints]@. 1299definitelyInhabitedType :: TyState -> Type -> DsM Bool 1300definitelyInhabitedType ty_st ty = do 1301 res <- pmTopNormaliseType ty_st ty 1302 pure $ case res of 1303 HadRedexes _ cons _ -> any meets_criteria cons 1304 _ -> False 1305 where 1306 meets_criteria :: (Type, DataCon, Type) -> Bool 1307 meets_criteria (_, con, _) = 1308 null (dataConEqSpec con) && -- (1) 1309 null (dataConImplBangs con) -- (2) 1310 1311{- Note [Strict argument type constraints] 1312~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1313In the ConVar case of clause processing, each conlike K traditionally 1314generates two different forms of constraints: 1315 1316* A term constraint (e.g., x ~ K y1 ... yn) 1317* Type constraints from the conlike's context (e.g., if K has type 1318 forall bs. Q => s1 .. sn -> T tys, then Q would be its type constraints) 1319 1320As it turns out, these alone are not enough to detect a certain class of 1321unreachable code. Consider the following example (adapted from #15305): 1322 1323 data K = K1 | K2 !Void 1324 1325 f :: K -> () 1326 f K1 = () 1327 1328Even though `f` doesn't match on `K2`, `f` is exhaustive in its patterns. Why? 1329Because it's impossible to construct a terminating value of type `K` using the 1330`K2` constructor, and thus it's impossible for `f` to ever successfully match 1331on `K2`. 1332 1333The reason is because `K2`'s field of type `Void` is //strict//. Because there 1334are no terminating values of type `Void`, any attempt to construct something 1335using `K2` will immediately loop infinitely or throw an exception due to the 1336strictness annotation. (If the field were not strict, then `f` could match on, 1337say, `K2 undefined` or `K2 (let x = x in x)`.) 1338 1339Since neither the term nor type constraints mentioned above take strict 1340argument types into account, we make use of the `nonVoid` function to 1341determine whether a strict type is inhabitable by a terminating value or not. 1342We call this the "inhabitation test". 1343 1344`nonVoid ty` returns True when either: 13451. `ty` has at least one InhabitationCandidate for which both its term and type 1346 constraints are satifiable, and `nonVoid` returns `True` for all of the 1347 strict argument types in that InhabitationCandidate. 13482. We're unsure if it's inhabited by a terminating value. 1349 1350`nonVoid ty` returns False when `ty` is definitely uninhabited by anything 1351(except bottom). Some examples: 1352 1353* `nonVoid Void` returns False, since Void has no InhabitationCandidates. 1354 (This is what lets us discard the `K2` constructor in the earlier example.) 1355* `nonVoid (Int :~: Int)` returns True, since it has an InhabitationCandidate 1356 (through the Refl constructor), and its term constraint (x ~ Refl) and 1357 type constraint (Int ~ Int) are satisfiable. 1358* `nonVoid (Int :~: Bool)` returns False. Although it has an 1359 InhabitationCandidate (by way of Refl), its type constraint (Int ~ Bool) is 1360 not satisfiable. 1361* Given the following definition of `MyVoid`: 1362 1363 data MyVoid = MkMyVoid !Void 1364 1365 `nonVoid MyVoid` returns False. The InhabitationCandidate for the MkMyVoid 1366 constructor contains Void as a strict argument type, and since `nonVoid Void` 1367 returns False, that InhabitationCandidate is discarded, leaving no others. 1368* Whether or not a type is inhabited is undecidable in general. 1369 See Note [Fuel for the inhabitation test]. 1370* For some types, inhabitation is evident immediately and we don't need to 1371 perform expensive tests. See Note [Types that are definitely inhabitable]. 1372 1373Note [Fuel for the inhabitation test] 1374~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1375Whether or not a type is inhabited is undecidable in general. As a result, we 1376can run into infinite loops in `nonVoid`. Therefore, we adopt a fuel-based 1377approach to prevent that. 1378 1379Consider the following example: 1380 1381 data Abyss = MkAbyss !Abyss 1382 stareIntoTheAbyss :: Abyss -> a 1383 stareIntoTheAbyss x = case x of {} 1384 1385In principle, stareIntoTheAbyss is exhaustive, since there is no way to 1386construct a terminating value using MkAbyss. However, both the term and type 1387constraints for MkAbyss are satisfiable, so the only way one could determine 1388that MkAbyss is unreachable is to check if `nonVoid Abyss` returns False. 1389There is only one InhabitationCandidate for Abyss—MkAbyss—and both its term 1390and type constraints are satisfiable, so we'd need to check if `nonVoid Abyss` 1391returns False... and now we've entered an infinite loop! 1392 1393To avoid this sort of conundrum, `nonVoid` uses a simple test to detect the 1394presence of recursive types (through `checkRecTc`), and if recursion is 1395detected, we bail out and conservatively assume that the type is inhabited by 1396some terminating value. This avoids infinite loops at the expense of making 1397the coverage checker incomplete with respect to functions like 1398stareIntoTheAbyss above. Then again, the same problem occurs with recursive 1399newtypes, like in the following code: 1400 1401 newtype Chasm = MkChasm Chasm 1402 gazeIntoTheChasm :: Chasm -> a 1403 gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive 1404 1405So this limitation is somewhat understandable. 1406 1407Note that even with this recursion detection, there is still a possibility that 1408`nonVoid` can run in exponential time. Consider the following data type: 1409 1410 data T = MkT !T !T !T 1411 1412If we call `nonVoid` on each of its fields, that will require us to once again 1413check if `MkT` is inhabitable in each of those three fields, which in turn will 1414require us to check if `MkT` is inhabitable again... As you can see, the 1415branching factor adds up quickly, and if the recursion depth limit is, say, 1416100, then `nonVoid T` will effectively take forever. 1417 1418To mitigate this, we check the branching factor every time we are about to call 1419`nonVoid` on a list of strict argument types. If the branching factor exceeds 1 1420(i.e., if there is potential for exponential runtime), then we limit the 1421maximum recursion depth to 1 to mitigate the problem. If the branching factor 1422is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay 1423to stick with a larger maximum recursion depth. 1424 1425In #17977 we saw that the defaultRecTcMaxBound (100 at the time of writing) was 1426too large and had detrimental effect on performance of the coverage checker. 1427Given that we only commit to a best effort anyway, we decided to substantially 1428decrement the recursion depth to 3, at the cost of precision in some edge cases 1429like 1430 1431 data Nat = Z | S Nat 1432 data Down :: Nat -> Type where 1433 Down :: !(Down n) -> Down (S n) 1434 f :: Down (S (S (S (S (S Z))))) -> () 1435 f x = case x of {} 1436 1437Since the coverage won't bother to instantiate Down 4 levels deep to see that it 1438is in fact uninhabited, it will emit a inexhaustivity warning for the case. 1439 1440Note [Types that are definitely inhabitable] 1441~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1442Another microoptimization applies to data types like this one: 1443 1444 data S a = S ![a] !T 1445 1446Even though there is a strict field of type [a], it's quite silly to call 1447nonVoid on it, since it's "obvious" that it is inhabitable. To make this 1448intuition formal, we say that a type is definitely inhabitable (DI) if: 1449 1450 * It has at least one constructor C such that: 1451 1. C has no equality constraints (since they might be unsatisfiable) 1452 2. C has no strict argument types (since they might be uninhabitable) 1453 1454It's relatively cheap to check if a type is DI, so before we call `nonVoid` 1455on a list of strict argument types, we filter out all of the DI ones. 1456-} 1457 1458-------------------------------------------- 1459-- * Providing positive evidence for a Delta 1460 1461-- | @provideEvidence vs n delta@ returns a list of 1462-- at most @n@ (but perhaps empty) refinements of @delta@ that instantiate 1463-- @vs@ to compatible constructor applications or wildcards. 1464-- Negative information is only retained if literals are involved or when 1465-- for recursive GADTs. 1466provideEvidence :: [Id] -> Int -> Delta -> DsM [Delta] 1467provideEvidence = go 1468 where 1469 go _ 0 _ = pure [] 1470 go [] _ delta = pure [delta] 1471 go (x:xs) n delta = do 1472 tracePm "provideEvidence" (ppr x $$ ppr xs $$ ppr delta $$ ppr n) 1473 VI _ pos neg _ <- initLookupVarInfo delta x 1474 case pos of 1475 _:_ -> do 1476 -- All solutions must be valid at once. Try to find candidates for their 1477 -- fields. Example: 1478 -- f x@(Just _) True = case x of SomePatSyn _ -> () 1479 -- after this clause, we want to report that 1480 -- * @f Nothing _@ is uncovered 1481 -- * @f x False@ is uncovered 1482 -- where @x@ will have two possibly compatible solutions, @Just y@ for 1483 -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@ 1484 -- and @z@ that is valid at the same time. These constitute arg_vas below. 1485 let arg_vas = concatMap (\(_cl, args) -> args) pos 1486 go (arg_vas ++ xs) n delta 1487 [] 1488 -- When there are literals involved, just print negative info 1489 -- instead of listing missed constructors 1490 | notNull [ l | PmAltLit l <- neg ] 1491 -> go xs n delta 1492 [] -> try_instantiate x xs n delta 1493 1494 -- | Tries to instantiate a variable by possibly following the chain of 1495 -- newtypes and then instantiating to all ConLikes of the wrapped type's 1496 -- minimal residual COMPLETE set. 1497 try_instantiate :: Id -> [Id] -> Int -> Delta -> DsM [Delta] 1498 -- Convention: x binds the outer constructor in the chain, y the inner one. 1499 try_instantiate x xs n delta = do 1500 (_src_ty, dcs, core_ty) <- tntrGuts <$> pmTopNormaliseType (delta_ty_st delta) (idType x) 1501 let build_newtype (x, delta) (_ty, dc, arg_ty) = do 1502 y <- lift $ mkPmId arg_ty 1503 delta' <- addVarConCt delta x (PmAltConLike (RealDataCon dc)) [y] 1504 pure (y, delta') 1505 runMaybeT (foldlM build_newtype (x, delta) dcs) >>= \case 1506 Nothing -> pure [] 1507 Just (y, newty_delta) -> do 1508 -- Pick a COMPLETE set and instantiate it (n at max). Take care of ⊥. 1509 pm <- vi_cache <$> initLookupVarInfo newty_delta y 1510 mb_cls <- pickMinimalCompleteSet newty_delta pm 1511 case uniqDSetToList <$> mb_cls of 1512 Just cls@(_:_) -> instantiate_cons y core_ty xs n newty_delta cls 1513 Just [] | not (canDiverge newty_delta y) -> pure [] 1514 -- Either ⊥ is still possible (think Void) or there are no COMPLETE 1515 -- sets available, so we can assume it's inhabited 1516 _ -> go xs n newty_delta 1517 1518 instantiate_cons :: Id -> Type -> [Id] -> Int -> Delta -> [ConLike] -> DsM [Delta] 1519 instantiate_cons _ _ _ _ _ [] = pure [] 1520 instantiate_cons _ _ _ 0 _ _ = pure [] 1521 instantiate_cons _ ty xs n delta _ 1522 -- We don't want to expose users to GHC-specific constructors for Int etc. 1523 | fmap (isTyConTriviallyInhabited . fst) (splitTyConApp_maybe ty) == Just True 1524 = go xs n delta 1525 instantiate_cons x ty xs n delta (cl:cls) = do 1526 env <- dsGetFamInstEnvs 1527 case guessConLikeUnivTyArgsFromResTy env ty cl of 1528 Nothing -> pure [delta] -- No idea idea how to refine this one, so just finish off with a wildcard 1529 Just arg_tys -> do 1530 (arg_vars, new_ty_cs, strict_arg_tys) <- mkOneConFull arg_tys cl 1531 let new_tm_cs = unitBag (TmVarCon x (PmAltConLike cl) arg_vars) 1532 -- Now check satifiability 1533 mb_delta <- pmIsSatisfiable delta new_tm_cs new_ty_cs strict_arg_tys 1534 tracePm "instantiate_cons" (vcat [ ppr x 1535 , ppr (idType x) 1536 , ppr ty 1537 , ppr cl 1538 , ppr arg_tys 1539 , ppr new_tm_cs 1540 , ppr new_ty_cs 1541 , ppr strict_arg_tys 1542 , ppr delta 1543 , ppr mb_delta 1544 , ppr n ]) 1545 con_deltas <- case mb_delta of 1546 Nothing -> pure [] 1547 -- NB: We don't prepend arg_vars as we don't have any evidence on 1548 -- them and we only want to split once on a data type. They are 1549 -- inhabited, otherwise pmIsSatisfiable would have refuted. 1550 Just delta' -> go xs n delta' 1551 other_cons_deltas <- instantiate_cons x ty xs (n - length con_deltas) delta cls 1552 pure (con_deltas ++ other_cons_deltas) 1553 1554pickMinimalCompleteSet :: Delta -> PossibleMatches -> DsM (Maybe ConLikeSet) 1555pickMinimalCompleteSet _ NoPM = pure Nothing 1556-- TODO: First prune sets with type info in delta. But this is good enough for 1557-- now and less costly. See #17386. 1558pickMinimalCompleteSet _ (PM clss) = do 1559 tracePm "pickMinimalCompleteSet" (ppr $ NonEmpty.toList clss) 1560 pure (Just (minimumBy (comparing sizeUniqDSet) clss)) 1561 1562-- | See if we already encountered a semantically equivalent expression and 1563-- return its representative. 1564representCoreExpr :: Delta -> CoreExpr -> DsM (Delta, Id) 1565representCoreExpr delta@MkDelta{ delta_tm_st = ts@TmSt{ ts_reps = reps } } e = do 1566 dflags <- getDynFlags 1567 let e' = simpleOptExpr dflags e 1568 case lookupCoreMap reps e' of 1569 Just rep -> pure (delta, rep) 1570 Nothing -> do 1571 rep <- mkPmId (exprType e') 1572 let reps' = extendCoreMap reps e' rep 1573 let delta' = delta{ delta_tm_st = ts{ ts_reps = reps' } } 1574 pure (delta', rep) 1575 1576-- Most of our actions thread around a delta from one computation to the next, 1577-- thereby potentially failing. This is expressed in the following Monad: 1578-- type PmM a = StateT Delta (MaybeT DsM) a 1579 1580-- | Records that a variable @x@ is equal to a 'CoreExpr' @e@. 1581addVarCoreCt :: Delta -> Id -> CoreExpr -> DsM (Maybe Delta) 1582addVarCoreCt delta x e = runMaybeT (execStateT (core_expr x e) delta) 1583 where 1584 -- | Takes apart a 'CoreExpr' and tries to extract as much information about 1585 -- literals and constructor applications as possible. 1586 core_expr :: Id -> CoreExpr -> StateT Delta (MaybeT DsM) () 1587 -- TODO: Handle newtypes properly, by wrapping the expression in a DataCon 1588 -- This is the right thing for casts involving data family instances and 1589 -- their representation TyCon, though (which are not visible in source 1590 -- syntax). See Note [COMPLETE sets on data families] 1591 -- core_expr x e | pprTrace "core_expr" (ppr x $$ ppr e) False = undefined 1592 core_expr x (Cast e _co) = core_expr x e 1593 core_expr x (Tick _t e) = core_expr x e 1594 core_expr x e 1595 | Just (pmLitAsStringLit -> Just s) <- coreExprAsPmLit e 1596 , expr_ty `eqType` stringTy 1597 -- See Note [Representation of Strings in TmState] 1598 = case unpackFS s of 1599 -- We need this special case to break a loop with coreExprAsPmLit 1600 -- Otherwise we alternate endlessly between [] and "" 1601 [] -> data_con_app x nilDataCon [] 1602 s' -> core_expr x (mkListExpr charTy (map mkCharExpr s')) 1603 | Just lit <- coreExprAsPmLit e 1604 = pm_lit x lit 1605 | Just (_in_scope, _empty_floats@[], dc, _arg_tys, args) 1606 <- exprIsConApp_maybe in_scope_env e 1607 = do { arg_ids <- traverse bind_expr args 1608 ; data_con_app x dc arg_ids } 1609 -- See Note [Detecting pattern synonym applications in expressions] 1610 | Var y <- e, Nothing <- isDataConId_maybe x 1611 -- We don't consider DataCons flexible variables 1612 = modifyT (\delta -> addVarVarCt delta (x, y)) 1613 | otherwise 1614 -- Any other expression. Try to find other uses of a semantically 1615 -- equivalent expression and represent them by the same variable! 1616 = do { rep <- represent_expr e 1617 ; modifyT (\delta -> addVarVarCt delta (x, rep)) } 1618 where 1619 expr_ty = exprType e 1620 expr_in_scope = mkInScopeSet (exprFreeVars e) 1621 in_scope_env = (expr_in_scope, const NoUnfolding) 1622 -- It's inconvenient to get hold of a global in-scope set 1623 -- here, but it'll only be needed if exprIsConApp_maybe ends 1624 -- up substituting inside a forall or lambda (i.e. seldom) 1625 -- so using exprFreeVars seems fine. See MR !1647. 1626 1627 bind_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id 1628 bind_expr e = do 1629 x <- lift (lift (mkPmId (exprType e))) 1630 core_expr x e 1631 pure x 1632 1633 -- See if we already encountered a semantically equivalent expression 1634 -- and return its representative 1635 represent_expr :: CoreExpr -> StateT Delta (MaybeT DsM) Id 1636 represent_expr e = StateT $ \delta -> 1637 swap <$> lift (representCoreExpr delta e) 1638 1639 data_con_app :: Id -> DataCon -> [Id] -> StateT Delta (MaybeT DsM) () 1640 data_con_app x dc args = pm_alt_con_app x (PmAltConLike (RealDataCon dc)) args 1641 1642 pm_lit :: Id -> PmLit -> StateT Delta (MaybeT DsM) () 1643 pm_lit x lit = pm_alt_con_app x (PmAltLit lit) [] 1644 1645 -- | Adds the given constructor application as a solution for @x@. 1646 pm_alt_con_app :: Id -> PmAltCon -> [Id] -> StateT Delta (MaybeT DsM) () 1647 pm_alt_con_app x con args = modifyT $ \delta -> addVarConCt delta x con args 1648 1649-- | Like 'modify', but with an effectful modifier action 1650modifyT :: Monad m => (s -> m s) -> StateT s m () 1651modifyT f = StateT $ fmap ((,) ()) . f 1652 1653{- Note [Detecting pattern synonym applications in expressions] 1654~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1655At the moment we fail to detect pattern synonyms in scrutinees and RHS of 1656guards. This could be alleviated with considerable effort and complexity, but 1657the returns are meager. Consider: 1658 1659 pattern P 1660 pattern Q 1661 case P 15 of 1662 Q _ -> ... 1663 P 15 -> 1664 1665Compared to the situation where P and Q are DataCons, the lack of generativity 1666means we could never flag Q as redundant. 1667(also see Note [Undecidable Equality for PmAltCons] in PmTypes.) 1668On the other hand, if we fail to recognise the pattern synonym, we flag the 1669pattern match as inexhaustive. That wouldn't happen if we had knowledge about 1670the scrutinee, in which case the oracle basically knows "If it's a P, then its 1671field is 15". 1672 1673This is a pretty narrow use case and I don't think we should to try to fix it 1674until a user complains energetically. 1675-} 1676