never executed always true always false
1
2 {-# LANGUAGE LambdaCase #-}
3 {-# LANGUAGE ScopedTypeVariables #-}
4 {-# LANGUAGE ViewPatterns #-}
5
6 {-
7 Authors: George Karachalias <george.karachalias@cs.kuleuven.be>
8 Sebastian Graf <sgraf1337@gmail.com>
9 Ryan Scott <ryan.gl.scott@gmail.com>
10 -}
11
12 -- | Model refinements type as per the
13 -- [Lower Your Guards paper](https://dl.acm.org/doi/abs/10.1145/3408989).
14 -- The main export of the module are the functions 'addPhiCtsNablas' for adding
15 -- facts to the oracle, 'isInhabited' to check if a refinement type is inhabited
16 -- and 'generateInhabitingPatterns' to turn a 'Nabla' into a concrete pattern
17 -- for an equation.
18 --
19 -- In terms of the LYG paper, this module is concerned with Sections 3.4, 3.6
20 -- and 3.7. E.g., it represents refinement types directly as a bunch of
21 -- normalised refinement types 'Nabla'.
22
23 module GHC.HsToCore.Pmc.Solver (
24
25 Nabla, Nablas(..), initNablas,
26
27 PhiCt(..), PhiCts,
28 addPhiCtNablas,
29 addPhiCtsNablas,
30
31 isInhabited,
32 generateInhabitingPatterns
33
34 ) where
35
36 import GHC.Prelude
37
38 import GHC.HsToCore.Pmc.Types
39 import GHC.HsToCore.Pmc.Utils (tracePm, traceWhenFailPm, mkPmId)
40
41 import GHC.Driver.Session
42 import GHC.Driver.Config
43 import GHC.Utils.Outputable
44 import GHC.Utils.Misc
45 import GHC.Utils.Monad (allM)
46 import GHC.Utils.Panic
47 import GHC.Utils.Panic.Plain
48 import GHC.Data.Bag
49 import GHC.Types.CompleteMatch
50 import GHC.Types.Unique.Set
51 import GHC.Types.Unique.DSet
52 import GHC.Types.Unique.SDFM
53 import GHC.Types.Id
54 import GHC.Types.Name
55 import GHC.Types.Var (EvVar)
56 import GHC.Types.Var.Env
57 import GHC.Types.Var.Set
58 import GHC.Core
59 import GHC.Core.FVs (exprFreeVars)
60 import GHC.Core.Map.Expr
61 import GHC.Core.SimpleOpt (simpleOptExpr, exprIsConApp_maybe)
62 import GHC.Core.Utils (exprType)
63 import GHC.Core.Make (mkListExpr, mkCharExpr)
64 import GHC.Types.Unique.Supply
65 import GHC.Data.FastString
66 import GHC.Types.SrcLoc
67 import GHC.Data.Maybe
68 import GHC.Core.ConLike
69 import GHC.Core.DataCon
70 import GHC.Core.PatSyn
71 import GHC.Core.TyCon
72 import GHC.Core.TyCon.RecWalk
73 import GHC.Builtin.Names
74 import GHC.Builtin.Types
75 import GHC.Builtin.Types.Prim (tYPETyCon)
76 import GHC.Core.TyCo.Rep
77 import GHC.Core.TyCo.Subst (elemTCvSubst)
78 import GHC.Core.Type
79 import GHC.Tc.Solver (tcNormalise, tcCheckGivens, tcCheckWanteds)
80 import GHC.Core.Unify (tcMatchTy)
81 import GHC.Core.Coercion
82 import GHC.Core.Reduction
83 import GHC.HsToCore.Monad hiding (foldlM)
84 import GHC.Tc.Instance.Family
85 import GHC.Core.FamInstEnv
86
87 import Control.Applicative ((<|>))
88 import Control.Monad (foldM, forM, guard, mzero, when, filterM)
89 import Control.Monad.Trans.Class (lift)
90 import Control.Monad.Trans.State.Strict
91 import Data.Coerce
92 import Data.Either (partitionEithers)
93 import Data.Foldable (foldlM, minimumBy, toList)
94 import Data.Monoid (Any(..))
95 import Data.List (sortBy, find)
96 import qualified Data.List.NonEmpty as NE
97 import Data.Ord (comparing)
98
99 import GHC.Utils.Trace
100 _ = pprTrace -- to silence unused import warnings
101
102 --
103 -- * Main exports
104 --
105
106 -- | Add a bunch of 'PhiCt's to all the 'Nabla's.
107 -- Lifts 'addPhiCts' over many 'Nablas'.
108 addPhiCtsNablas :: Nablas -> PhiCts -> DsM Nablas
109 addPhiCtsNablas nablas cts = liftNablasM (\d -> addPhiCts d cts) nablas
110
111 -- | 'addPmCtsNablas' for a single 'PmCt'.
112 addPhiCtNablas :: Nablas -> PhiCt -> DsM Nablas
113 addPhiCtNablas nablas ct = addPhiCtsNablas nablas (unitBag ct)
114
115 liftNablasM :: Monad m => (Nabla -> m (Maybe Nabla)) -> Nablas -> m Nablas
116 liftNablasM f (MkNablas ds) = MkNablas . catBagMaybes <$> (traverse f ds)
117
118 -- | Test if any of the 'Nabla's is inhabited. Currently this is pure, because
119 -- we preserve the invariant that there are no uninhabited 'Nabla's. But that
120 -- could change in the future, for example by implementing this function in
121 -- terms of @notNull <$> generateInhabitingPatterns 1 ds@.
122 isInhabited :: Nablas -> DsM Bool
123 isInhabited (MkNablas ds) = pure (not (null ds))
124
125 -----------------------------------------------
126 -- * Caching residual COMPLETE sets
127
128 -- See Note [Implementation of COMPLETE pragmas]
129
130 -- | Update the COMPLETE sets of 'ResidualCompleteMatches', or 'Nothing'
131 -- if there was no change as per the update function.
132 updRcm :: (CompleteMatch -> (Bool, CompleteMatch))
133 -> ResidualCompleteMatches -> (Maybe ResidualCompleteMatches)
134 updRcm f (RCM vanilla pragmas)
135 | not any_change = Nothing
136 | otherwise = Just (RCM vanilla' pragmas')
137 where
138 f' :: CompleteMatch -> (Any, CompleteMatch)
139 f' = coerce f
140 (chgd, vanilla') = traverse f' vanilla
141 (chgds, pragmas') = traverse (traverse f') pragmas
142 any_change = getAny $ chgd `mappend` chgds
143
144 -- | A pseudo-'CompleteMatch' for the vanilla complete set of the given data
145 -- 'TyCon'.
146 -- Ex.: @vanillaCompleteMatchTC 'Maybe' ==> Just ("Maybe", {'Just','Nothing'})@
147 vanillaCompleteMatchTC :: TyCon -> Maybe CompleteMatch
148 vanillaCompleteMatchTC tc =
149 let -- | TYPE acts like an empty data type on the term-level (#14086), but
150 -- it is a PrimTyCon, so tyConDataCons_maybe returns Nothing. Hence a
151 -- special case.
152 mb_dcs | tc == tYPETyCon = Just []
153 | otherwise = tyConDataCons_maybe tc
154 in vanillaCompleteMatch . mkUniqDSet . map RealDataCon <$> mb_dcs
155
156 -- | Initialise from 'dsGetCompleteMatches' (containing all COMPLETE pragmas)
157 -- if the given 'ResidualCompleteMatches' were empty.
158 addCompleteMatches :: ResidualCompleteMatches -> DsM ResidualCompleteMatches
159 addCompleteMatches (RCM v Nothing) = RCM v . Just <$> dsGetCompleteMatches
160 addCompleteMatches rcm = pure rcm
161
162 -- | Adds the declared 'CompleteMatches' from COMPLETE pragmas, as well as the
163 -- vanilla data defn if it is a 'DataCon'.
164 addConLikeMatches :: ConLike -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
165 addConLikeMatches (RealDataCon dc) rcm = addTyConMatches (dataConTyCon dc) rcm
166 addConLikeMatches (PatSynCon _) rcm = addCompleteMatches rcm
167
168 -- | Adds
169 -- * the 'CompleteMatches' from COMPLETE pragmas
170 -- * and the /vanilla/ 'CompleteMatch' from the data 'TyCon'
171 -- to the 'ResidualCompleteMatches', if not already present.
172 addTyConMatches :: TyCon -> ResidualCompleteMatches -> DsM ResidualCompleteMatches
173 addTyConMatches tc rcm = add_tc_match <$> addCompleteMatches rcm
174 where
175 -- | Add the vanilla COMPLETE set from the data defn, if any. But only if
176 -- it's not already present.
177 add_tc_match rcm
178 = rcm{rcm_vanilla = rcm_vanilla rcm <|> vanillaCompleteMatchTC tc}
179
180 markMatched :: PmAltCon -> ResidualCompleteMatches -> DsM (Maybe ResidualCompleteMatches)
181 -- Nothing means the PmAltCon didn't occur in any COMPLETE set.
182 -- See Note [Shortcutting the inhabitation test] for how this is useful for
183 -- performance on T17836.
184 markMatched (PmAltLit _) _ = pure Nothing -- lits are never part of a COMPLETE set
185 markMatched (PmAltConLike cl) rcm = do
186 rcm' <- addConLikeMatches cl rcm
187 let go cm = case lookupUniqDSet (cmConLikes cm) cl of
188 Nothing -> (False, cm)
189 Just _ -> (True, cm { cmConLikes = delOneFromUniqDSet (cmConLikes cm) cl })
190 pure $ updRcm go rcm'
191
192 {-
193 Note [Implementation of COMPLETE pragmas]
194 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
195 A COMPLETE set represents a set of conlikes (i.e., constructors or
196 pattern synonyms) such that if they are all pattern-matched against in a
197 function, it gives rise to a total function. An example is:
198
199 newtype Boolean = Boolean Int
200 pattern F, T :: Boolean
201 pattern F = Boolean 0
202 pattern T = Boolean 1
203 {-# COMPLETE F, T #-}
204
205 -- This is a total function
206 booleanToInt :: Boolean -> Int
207 booleanToInt F = 0
208 booleanToInt T = 1
209
210 COMPLETE sets are represented internally in GHC as a set of 'ConLike's. For
211 example, the pragma {-# COMPLETE F, T #-} would be represented as:
212
213 CompleteMatch {F, T} Nothing
214
215 What is the Maybe for? Answer: COMPLETE pragmas may optionally specify a
216 result *type constructor* (cf. T14422):
217
218 class C f where
219 foo :: f a -> ()
220 pattern P :: C f => f a
221 pattern P <- (foo -> ())
222
223 instance C State where
224 foo _ = ()
225 {-# COMPLETE P :: State #-}
226
227 f :: State a -> ()
228 f P = ()
229 g :: C f => f a -> ()
230 g P = ()
231
232 The @:: State@ here means that the types at which the COMPLETE pragma *applies*
233 is restricted to scrutinee types that are applications of the 'State' TyCon. So
234 it applies to the match in @f@ but not in @g@ above, resulting in a warning for
235 the latter but not for the former. The pragma is represented as
236
237 CompleteMatch {P} (Just State)
238
239 GHC collects all COMPLETE pragmas from the current module and from imports
240 into a field in the DsM environment, which can be accessed with
241 dsGetCompleteMatches from "GHC.HsToCore.Monad".
242 Currently, COMPLETE pragmas can't be orphans (e.g. at least one ConLike must
243 also be defined in the module of the pragma) and do not impact recompilation
244 checking (#18675).
245
246 The pattern-match checker will then initialise each variable's 'VarInfo' with
247 *all* imported COMPLETE sets (in 'GHC.HsToCore.Pmc.Solver.addCompleteMatches'),
248 well-typed or not, into a 'ResidualCompleteMatches'. The trick is that a
249 COMPLETE set that is ill-typed for that match variable could never be written by
250 the user! And we make sure not to report any ill-typed COMPLETE sets when
251 formatting 'Nabla's for warnings in 'generateInhabitingPatterns'.
252
253 A 'ResidualCompleteMatches' is a list of all COMPLETE sets, minus the ConLikes
254 we know a particular variable can't be (through negative constructor constraints
255 @x /~ K@ or a failed attempt at instantiating that ConLike during inhabitation
256 testing). If *any* of the COMPLETE sets become empty, we know that the match
257 was exhaustive.
258
259 We assume that a COMPLETE set does not apply if for one of its
260 ConLikes we fail to 'matchConLikeResTy' or the
261 type of the match variable isn't an application of the optional
262 result type constructor from the pragma. Why don't we simply
263 prune inapplicable COMPLETE sets from 'ResidualCompleteMatches'?
264 The answer is that additional type constraints might make more
265 COMPLETE sets applicable! Example:
266
267 h :: a -> a :~: Boolean -> ()
268 h x Refl | T <- x = ()
269 | F <- x = ()
270
271 If we eagerly prune {F,T} from the residual matches of @x@, then we don't see
272 that the match in the guards of @h@ is exhaustive, where the COMPLETE set
273 applies due to refined type information.
274 -}
275
276 -----------------------
277 -- * Type normalisation
278
279 -- | The return value of 'pmTopNormaliseType'
280 data TopNormaliseTypeResult
281 = NormalisedByConstraints Type
282 -- ^ 'tcNormalise' was able to simplify the type with some local constraint
283 -- from the type oracle, but 'topNormaliseTypeX' couldn't identify a type
284 -- redex.
285 | HadRedexes Type [(Type, DataCon, Type)] Type
286 -- ^ 'tcNormalise' may or may not been able to simplify the type, but
287 -- 'topNormaliseTypeX' made progress either way and got rid of at least one
288 -- outermost type or data family redex or newtype.
289 -- The first field is the last type that was reduced solely through type
290 -- family applications (possibly just the 'tcNormalise'd type). This is the
291 -- one that is equal (in source Haskell) to the initial type.
292 -- The third field is the type that we get when also looking through data
293 -- family applications and newtypes. This would be the representation type in
294 -- Core (modulo casts).
295 -- The second field is the list of Newtype 'DataCon's that we looked through
296 -- in the chain of reduction steps between the Source type and the Core type.
297 -- We also keep the type of the DataCon application and its field, so that we
298 -- don't have to reconstruct it in 'inhabitationCandidates' and
299 -- 'generateInhabitingPatterns'.
300 -- For an example, see Note [Type normalisation].
301
302 -- | Return the fields of 'HadRedexes'. Returns appropriate defaults in the
303 -- other cases.
304 tntrGuts :: TopNormaliseTypeResult -> (Type, [(Type, DataCon, Type)], Type)
305 tntrGuts (NormalisedByConstraints ty) = (ty, [], ty)
306 tntrGuts (HadRedexes src_ty ds core_ty) = (src_ty, ds, core_ty)
307
308 instance Outputable TopNormaliseTypeResult where
309 ppr (NormalisedByConstraints ty) = text "NormalisedByConstraints" <+> ppr ty
310 ppr (HadRedexes src_ty ds core_ty) = text "HadRedexes" <+> braces fields
311 where
312 fields = fsep (punctuate comma [ text "src_ty =" <+> ppr src_ty
313 , text "newtype_dcs =" <+> ppr ds
314 , text "core_ty =" <+> ppr core_ty ])
315
316 pmTopNormaliseType :: TyState -> Type -> DsM TopNormaliseTypeResult
317 -- ^ Get rid of *outermost* (or toplevel)
318 -- * type function redex
319 -- * data family redex
320 -- * newtypes
321 --
322 -- Behaves like `topNormaliseType_maybe`, but instead of returning a
323 -- coercion, it returns useful information for issuing pattern matching
324 -- warnings. See Note [Type normalisation] for details.
325 -- It also initially 'tcNormalise's the type with the bag of local constraints.
326 --
327 -- See 'TopNormaliseTypeResult' for the meaning of the return value.
328 --
329 -- NB: Normalisation can potentially change kinds, if the head of the type
330 -- is a type family with a variable result kind. I (Richard E) can't think
331 -- of a way to cause trouble here, though.
332 pmTopNormaliseType (TySt _ inert) typ = {-# SCC "pmTopNormaliseType" #-} do
333 env <- dsGetFamInstEnvs
334 tracePm "normalise" (ppr typ)
335 -- Before proceeding, we chuck typ into the constraint solver, in case
336 -- solving for given equalities may reduce typ some. See
337 -- "Wrinkle: local equalities" in Note [Type normalisation].
338 typ' <- initTcDsForSolver $ tcNormalise inert typ
339 -- Now we look with topNormaliseTypeX through type and data family
340 -- applications and newtypes, which tcNormalise does not do.
341 -- See also 'TopNormaliseTypeResult'.
342 pure $ case topNormaliseTypeX (stepper env) comb typ' of
343 Nothing -> NormalisedByConstraints typ'
344 Just ((ty_f,tm_f), ty) -> HadRedexes src_ty newtype_dcs core_ty
345 where
346 src_ty = eq_src_ty ty (typ' : ty_f [ty])
347 newtype_dcs = tm_f []
348 core_ty = ty
349 where
350 -- Find the first type in the sequence of rewrites that is a data type,
351 -- newtype, or a data family application (not the representation tycon!).
352 -- This is the one that is equal (in source Haskell) to the initial type.
353 -- If none is found in the list, then all of them are type family
354 -- applications, so we simply return the last one, which is the *simplest*.
355 eq_src_ty :: Type -> [Type] -> Type
356 eq_src_ty ty tys = maybe ty id (find is_closed_or_data_family tys)
357
358 is_closed_or_data_family :: Type -> Bool
359 is_closed_or_data_family ty = pmIsClosedType ty || isDataFamilyAppType ty
360
361 -- For efficiency, represent both lists as difference lists.
362 -- comb performs the concatenation, for both lists.
363 comb (tyf1, tmf1) (tyf2, tmf2) = (tyf1 . tyf2, tmf1 . tmf2)
364
365 stepper env = newTypeStepper `composeSteppers` tyFamStepper env
366
367 -- A 'NormaliseStepper' that unwraps newtypes, careful not to fall into
368 -- a loop. If it would fall into a loop, it produces 'NS_Abort'.
369 newTypeStepper :: NormaliseStepper ([Type] -> [Type],[(Type, DataCon, Type)] -> [(Type, DataCon, Type)])
370 newTypeStepper rec_nts tc tys
371 | Just (ty', _co) <- instNewTyCon_maybe tc tys
372 , let orig_ty = TyConApp tc tys
373 = case checkRecTc rec_nts tc of
374 Just rec_nts' -> let tyf = (orig_ty:)
375 tmf = ((orig_ty, tyConSingleDataCon tc, ty'):)
376 in NS_Step rec_nts' ty' (tyf, tmf)
377 Nothing -> NS_Abort
378 | otherwise
379 = NS_Done
380
381 tyFamStepper :: FamInstEnvs -> NormaliseStepper ([Type] -> [Type], a -> a)
382 tyFamStepper env rec_nts tc tys -- Try to step a type/data family
383 = case topReduceTyFamApp_maybe env tc tys of
384 Just (HetReduction (Reduction _ rhs) _)
385 -> NS_Step rec_nts rhs ((rhs:), id)
386 _ -> NS_Done
387
388 -- | Returns 'True' if the argument 'Type' is a fully saturated application of
389 -- a closed type constructor.
390 --
391 -- Closed type constructors are those with a fixed right hand side, as
392 -- opposed to e.g. associated types. These are of particular interest for
393 -- pattern-match coverage checking, because GHC can exhaustively consider all
394 -- possible forms that values of a closed type can take on.
395 --
396 -- Note that this function is intended to be used to check types of value-level
397 -- patterns, so as a consequence, the 'Type' supplied as an argument to this
398 -- function should be of kind @Type@.
399 pmIsClosedType :: Type -> Bool
400 pmIsClosedType ty
401 = case splitTyConApp_maybe ty of
402 Just (tc, ty_args)
403 | is_algebraic_like tc && not (isFamilyTyCon tc)
404 -> assertPpr (ty_args `lengthIs` tyConArity tc) (ppr ty) True
405 _other -> False
406 where
407 -- This returns True for TyCons which /act like/ algebraic types.
408 -- (See "Type#type_classification" for what an algebraic type is.)
409 --
410 -- This is qualified with \"like\" because of a particular special
411 -- case: TYPE (the underlyind kind behind Type, among others). TYPE
412 -- is conceptually a datatype (and thus algebraic), but in practice it is
413 -- a primitive builtin type, so we must check for it specially.
414 --
415 -- NB: it makes sense to think of TYPE as a closed type in a value-level,
416 -- pattern-matching context. However, at the kind level, TYPE is certainly
417 -- not closed! Since this function is specifically tailored towards pattern
418 -- matching, however, it's OK to label TYPE as closed.
419 is_algebraic_like :: TyCon -> Bool
420 is_algebraic_like tc = isAlgTyCon tc || tc == tYPETyCon
421
422 -- | Normalise the given source type to WHNF. If it isn't already in WHNF
423 -- ('isSourceTypeInWHNF') , it will normalise the type and then try to step
424 -- through type family applications, but not data family applications or
425 -- newtypes.
426 --
427 -- This is a pretty common case of calling 'pmTopNormaliseType' and it should be
428 -- efficient.
429 normaliseSourceTypeWHNF :: TyState -> Type -> DsM Type
430 normaliseSourceTypeWHNF _ ty | isSourceTypeInWHNF ty = pure ty
431 normaliseSourceTypeWHNF ty_st ty =
432 pmTopNormaliseType ty_st ty >>= \case
433 NormalisedByConstraints ty -> pure ty
434 HadRedexes ty _ _ -> pure ty
435
436 -- | Is the source type in WHNF wrt. 'pmTopNormaliseType'?
437 --
438 -- Returns False if the given type is not a TyCon application, or if the TyCon
439 -- app head is a type family TyCon. (But not for data family TyCons!)
440 isSourceTypeInWHNF :: Type -> Bool
441 isSourceTypeInWHNF ty
442 | Just (tc, _) <- splitTyConApp_maybe ty = not (isTypeFamilyTyCon tc)
443 | otherwise = False
444
445 {- Note [Type normalisation]
446 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
447 Constructs like -XEmptyCase or a previous unsuccessful pattern match on a data
448 constructor place a non-void constraint on the matched thing. This means that it
449 boils down to checking whether the type of the scrutinee is inhabited. Function
450 pmTopNormaliseType gets rid of the outermost type function/data family redex and
451 newtypes, in search of an algebraic type constructor, which is easier to check
452 for inhabitation.
453
454 It returns 3 results instead of one, because there are 2 subtle points:
455 1. Newtypes are isomorphic to the underlying type in core but not in the source
456 language,
457 2. The representational data family tycon is used internally but should not be
458 shown to the user
459
460 Hence, if pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty),
461 then
462 (a) src_ty is the rewritten type which we can show to the user. That is, the
463 type we get if we rewrite type families but not data families or
464 newtypes.
465 (b) dcs is the list of newtype constructors "skipped", every time we normalise
466 a newtype to its core representation, we keep track of the source data
467 constructor. For convenience, we also track the type we unwrap and the
468 type of its field. Example: @Down 42@ => @[(Down @Int, Down, Int)]
469 (c) core_ty is the rewritten type. That is,
470 pmTopNormaliseType env ty_cs ty = Just (src_ty, dcs, core_ty)
471 implies
472 topNormaliseType_maybe env ty = Just (co, core_ty)
473 for some coercion co.
474
475 To see how all cases come into play, consider the following example:
476
477 data family T a :: *
478 data instance T Int = T1 | T2 Bool
479 -- Which gives rise to FC:
480 -- data T a
481 -- data R:TInt = T1 | T2 Bool
482 -- axiom ax_ti : T Int ~R R:TInt
483
484 newtype G1 = MkG1 (T Int)
485 newtype G2 = MkG2 G1
486
487 type instance F Int = F Char
488 type instance F Char = G2
489
490 In this case pmTopNormaliseType env ty_cs (F Int) results in
491
492 Just (G2, [(G2,MkG2,G1),(G1,MkG1,T Int)], R:TInt)
493
494 Which means that in source Haskell:
495 - G2 is equivalent to F Int (in contrast, G1 isn't).
496 - if (x : R:TInt) then (MkG2 (MkG1 x) : F Int).
497
498 -----
499 -- Wrinkle: Local equalities
500 -----
501
502 Given the following type family:
503
504 type family F a
505 type instance F Int = Void
506
507 Should the following program (from #14813) be considered exhaustive?
508
509 f :: (i ~ Int) => F i -> a
510 f x = case x of {}
511
512 You might think "of course, since `x` is obviously of type Void". But the
513 idType of `x` is technically F i, not Void, so if we pass F i to
514 inhabitationCandidates, we'll mistakenly conclude that `f` is non-exhaustive.
515 In order to avoid this pitfall, we need to normalise the type passed to
516 pmTopNormaliseType, using the constraint solver to solve for any local
517 equalities (such as i ~ Int) that may be in scope.
518
519 Note [Coverage checking Newtype matches]
520 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
521 Newtypes have quite peculiar match semantics compared to ordinary DataCons. In a
522 pattern-match, they behave like a irrefutable (lazy) match, but for inhabitation
523 testing purposes (e.g. at construction sites), they behave rather like a DataCon
524 with a *strict* field, because they don't contribute their own bottom and are
525 inhabited iff the wrapped type is inhabited.
526
527 This distinction becomes apparent in #17248:
528
529 newtype T2 a = T2 a
530 g _ True = ()
531 g (T2 _) True = ()
532 g !_ True = ()
533
534 If we treat Newtypes like we treat regular DataCons, we would mark the third
535 clause as redundant, which clearly is unsound. The solution:
536 1. 'isPmAltConMatchStrict' returns False for newtypes, indicating that a
537 newtype match is lazy.
538 2. When we find @x ~ T2 y@, transfer all constraints on @x@ (which involve @⊥@)
539 to @y@, similar to what 'equate' does, and don't add a @x ≁ ⊥@ constraint.
540 This way, the third clause will still be marked as inaccessible RHS instead
541 of redundant. This is ensured by calling 'lookupVarInfoNT'.
542 3. Immediately reject when we find @x ≁ T2@.
543 Handling of Newtypes is also described in the Appendix of the Lower Your Guards paper,
544 where you can find the solution in a perhaps more digestible format.
545 -}
546
547 -------------------------
548 -- * Adding φ constraints
549 --
550 -- Figure 7 in the LYG paper.
551
552 -- | A high-level pattern-match constraint. Corresponds to φ from Figure 3 of
553 -- the LYG paper.
554 data PhiCt
555 = PhiTyCt !PredType
556 -- ^ A type constraint "T ~ U".
557 | PhiCoreCt !Id !CoreExpr
558 -- ^ @PhiCoreCt x e@ encodes "x ~ e", equating @x@ with the 'CoreExpr' @e@.
559 | PhiConCt !Id !PmAltCon ![TyVar] ![PredType] ![Id]
560 -- ^ @PhiConCt x K tvs dicts ys@ encodes @K \@tvs dicts ys <- x@, matching @x@
561 -- against the 'PmAltCon' application @K \@tvs dicts ys@, binding @tvs@,
562 -- @dicts@ and possibly unlifted fields @ys@ in the process.
563 -- See Note [Strict fields and fields of unlifted type].
564 | PhiNotConCt !Id !PmAltCon
565 -- ^ @PhiNotConCt x K@ encodes "x ≁ K", asserting that @x@ can't be headed
566 -- by @K@.
567 | PhiBotCt !Id
568 -- ^ @PhiBotCt x@ encodes "x ~ ⊥", equating @x@ to ⊥.
569 -- by @K@.
570 | PhiNotBotCt !Id
571 -- ^ @PhiNotBotCt x y@ encodes "x ≁ ⊥", asserting that @x@ can't be ⊥.
572
573 instance Outputable PhiCt where
574 ppr (PhiTyCt ty_ct) = ppr ty_ct
575 ppr (PhiCoreCt x e) = ppr x <+> char '~' <+> ppr e
576 ppr (PhiConCt x con tvs dicts args) =
577 hsep (ppr con : pp_tvs ++ pp_dicts ++ pp_args) <+> text "<-" <+> ppr x
578 where
579 pp_tvs = map ((<> char '@') . ppr) tvs
580 pp_dicts = map ppr dicts
581 pp_args = map ppr args
582 ppr (PhiNotConCt x con) = ppr x <+> text "≁" <+> ppr con
583 ppr (PhiBotCt x) = ppr x <+> text "~ ⊥"
584 ppr (PhiNotBotCt x) = ppr x <+> text "≁ ⊥"
585
586 type PhiCts = Bag PhiCt
587
588 -- | The fuel for the inhabitation test.
589 -- See Note [Fuel for the inhabitation test].
590 initFuel :: Int
591 initFuel = 4 -- 4 because it's the smallest number that passes f' in T17977b
592
593 -- | Adds new constraints to 'Nabla' and returns 'Nothing' if that leads to a
594 -- contradiction.
595 --
596 -- In terms of the paper, this function models the \(⊕_φ\) function in
597 -- Figure 7 on batches of φ constraints.
598 addPhiCts :: Nabla -> PhiCts -> DsM (Maybe Nabla)
599 -- See Note [TmState invariants].
600 addPhiCts nabla cts = runMaybeT $ do
601 let (ty_cts, tm_cts) = partitionPhiCts cts
602 nabla' <- addTyCts nabla (listToBag ty_cts)
603 nabla'' <- foldlM addPhiTmCt nabla' (listToBag tm_cts)
604 inhabitationTest initFuel (nabla_ty_st nabla) nabla''
605
606 partitionPhiCts :: PhiCts -> ([PredType], [PhiCt])
607 partitionPhiCts = partitionEithers . map to_either . toList
608 where
609 to_either (PhiTyCt pred_ty) = Left pred_ty
610 to_either ct = Right ct
611
612 -----------------------------
613 -- ** Adding type constraints
614
615 -- | Adds new type-level constraints by calling out to the type-checker via
616 -- 'tyOracle'.
617 addTyCts :: Nabla -> Bag PredType -> MaybeT DsM Nabla
618 addTyCts nabla@MkNabla{ nabla_ty_st = ty_st } new_ty_cs = do
619 ty_st' <- MaybeT (tyOracle ty_st new_ty_cs)
620 pure nabla{ nabla_ty_st = ty_st' }
621
622 -- | Add some extra type constraints to the 'TyState'; return 'Nothing' if we
623 -- find a contradiction (e.g. @Int ~ Bool@).
624 --
625 -- See Note [Pattern match warnings with insoluble Givens] in GHC.Tc.Solver.
626 tyOracle :: TyState -> Bag PredType -> DsM (Maybe TyState)
627 tyOracle ty_st@(TySt n inert) cts
628 | isEmptyBag cts
629 = pure (Just ty_st)
630 | otherwise
631 = {-# SCC "tyOracle" #-}
632 do { evs <- traverse nameTyCt cts
633 ; tracePm "tyOracle" (ppr n $$ ppr cts $$ ppr inert)
634 ; mb_new_inert <- initTcDsForSolver $ tcCheckGivens inert evs
635 -- return the new inert set and increment the sequence number n
636 ; return (TySt (n+1) <$> mb_new_inert) }
637
638 -- | Allocates a fresh 'EvVar' name for 'PredTy's.
639 nameTyCt :: PredType -> DsM EvVar
640 nameTyCt pred_ty = do
641 unique <- getUniqueM
642 let occname = mkVarOccFS (fsLit ("pm_"++show unique))
643 idname = mkInternalName unique occname noSrcSpan
644 return (mkLocalIdOrCoVar idname Many pred_ty)
645
646 -----------------------------
647 -- ** Adding term constraints
648
649 -- | Adds a single higher-level φ constraint by dispatching to the various
650 -- oracle functions.
651 --
652 -- In terms of the paper, this function amounts to the constructor constraint
653 -- case of \(⊕_φ\) in Figure 7, which "desugars" higher-level φ constraints
654 -- into lower-level δ constraints. We don't have a data type for δ constraints
655 -- and call the corresponding oracle function directly instead.
656 --
657 -- Precondition: The φ is /not/ a type constraint! These should be handled by
658 -- 'addTyCts' before, through 'addPhiCts'.
659 addPhiTmCt :: Nabla -> PhiCt -> MaybeT DsM Nabla
660 addPhiTmCt _ (PhiTyCt ct) = pprPanic "addPhiCt:TyCt" (ppr ct) -- See the precondition
661 addPhiTmCt nabla (PhiCoreCt x e) = addCoreCt nabla x e
662 addPhiTmCt nabla (PhiConCt x con tvs dicts args) = do
663 -- Case (1) of Note [Strict fields and variables of unlifted type]
664 -- PhiConCt correspond to the higher-level φ constraints from the paper with
665 -- bindings semantics. It disperses into lower-level δ constraints that the
666 -- 'add*Ct' functions correspond to.
667 nabla' <- addTyCts nabla (listToBag dicts)
668 nabla'' <- addConCt nabla' x con tvs args
669 foldlM addNotBotCt nabla'' (filterUnliftedFields con args)
670 addPhiTmCt nabla (PhiNotConCt x con) = addNotConCt nabla x con
671 addPhiTmCt nabla (PhiBotCt x) = addBotCt nabla x
672 addPhiTmCt nabla (PhiNotBotCt x) = addNotBotCt nabla x
673
674 filterUnliftedFields :: PmAltCon -> [Id] -> [Id]
675 filterUnliftedFields con args =
676 [ arg | (arg, bang) <- zipEqual "addPhiCt" args (pmAltConImplBangs con)
677 , isBanged bang || isUnliftedType (idType arg) ]
678
679 -- | Adds the constraint @x ~ ⊥@, e.g. that evaluation of a particular 'Id' @x@
680 -- surely diverges. Quite similar to 'addConCt', only that it only cares about
681 -- ⊥.
682 addBotCt :: Nabla -> Id -> MaybeT DsM Nabla
683 addBotCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x = do
684 let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x
685 case bot of
686 IsNotBot -> mzero -- There was x ≁ ⊥. Contradiction!
687 IsBot -> pure nabla -- There already is x ~ ⊥. Nothing left to do
688 MaybeBot -> do -- We add x ~ ⊥
689 let vi' = vi{ vi_bot = IsBot }
690 pure nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env y vi' } }
691
692 -- | Adds the constraint @x ~/ ⊥@ to 'Nabla'. Quite similar to 'addNotConCt',
693 -- but only cares for the ⊥ "constructor".
694 addNotBotCt :: Nabla -> Id -> MaybeT DsM Nabla
695 addNotBotCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ts_facts=env} } x = do
696 let (y, vi@VI { vi_bot = bot }) = lookupVarInfoNT (nabla_tm_st nabla) x
697 case bot of
698 IsBot -> mzero -- There was x ~ ⊥. Contradiction!
699 IsNotBot -> pure nabla -- There already is x ≁ ⊥. Nothing left to do
700 MaybeBot -> do -- We add x ≁ ⊥ and test if x is still inhabited
701 -- Mark dirty for a delayed inhabitation test
702 let vi' = vi{ vi_bot = IsNotBot}
703 pure $ markDirty y
704 $ nabla{ nabla_tm_st = ts{ ts_facts = addToUSDFM env y vi' } }
705
706 -- | Record a @x ~/ K@ constraint, e.g. that a particular 'Id' @x@ can't
707 -- take the shape of a 'PmAltCon' @K@ in the 'Nabla' and return @Nothing@ if
708 -- that leads to a contradiction.
709 -- See Note [TmState invariants].
710 addNotConCt :: Nabla -> Id -> PmAltCon -> MaybeT DsM Nabla
711 addNotConCt _ _ (PmAltConLike (RealDataCon dc))
712 | isNewDataCon dc = mzero -- (3) in Note [Coverage checking Newtype matches]
713 addNotConCt nabla x nalt = do
714 (mb_mark_dirty, nabla') <- trvVarInfo go nabla x
715 pure $ case mb_mark_dirty of
716 Just x -> markDirty x nabla'
717 Nothing -> nabla'
718 where
719 -- | Update `x`'s 'VarInfo' entry. Fail ('MaybeT') if contradiction,
720 -- otherwise return updated entry and `Just x'` if `x` should be marked dirty,
721 -- where `x'` is the representative of `x`.
722 go :: VarInfo -> MaybeT DsM (Maybe Id, VarInfo)
723 go vi@(VI x' pos neg _ rcm) = do
724 -- 1. Bail out quickly when nalt contradicts a solution
725 let contradicts nalt sol = eqPmAltCon (paca_con sol) nalt == Equal
726 guard (not (any (contradicts nalt) pos))
727 -- 2. Only record the new fact when it's not already implied by one of the
728 -- solutions
729 let implies nalt sol = eqPmAltCon (paca_con sol) nalt == Disjoint
730 let neg'
731 | any (implies nalt) pos = neg
732 -- See Note [Completeness checking with required Thetas]
733 | hasRequiredTheta nalt = neg
734 | otherwise = extendPmAltConSet neg nalt
735 massert (isPmAltConMatchStrict nalt)
736 let vi' = vi{ vi_neg = neg', vi_bot = IsNotBot }
737 -- 3. Make sure there's at least one other possible constructor
738 mb_rcm' <- lift (markMatched nalt rcm)
739 pure $ case mb_rcm' of
740 -- If nalt could be removed from a COMPLETE set, we'll get back Just and
741 -- have to mark x dirty, by returning Just x'.
742 Just rcm' -> (Just x', vi'{ vi_rcm = rcm' })
743 -- Otherwise, nalt didn't occur in any residual COMPLETE set and we
744 -- don't have to mark it dirty. So we return Nothing, which in the case
745 -- above would have compromised precision.
746 -- See Note [Shortcutting the inhabitation test], grep for T17836.
747 Nothing -> (Nothing, vi')
748
749 hasRequiredTheta :: PmAltCon -> Bool
750 hasRequiredTheta (PmAltConLike cl) = notNull req_theta
751 where
752 (_,_,_,_,req_theta,_,_) = conLikeFullSig cl
753 hasRequiredTheta _ = False
754
755 -- | Add a @x ~ K tvs args ts@ constraint.
756 -- @addConCt x K tvs args ts@ extends the substitution with a solution
757 -- @x :-> (K, tvs, args)@ if compatible with the negative and positive info we
758 -- have on @x@, reject (@Nothing@) otherwise.
759 --
760 -- See Note [TmState invariants].
761 addConCt :: Nabla -> Id -> PmAltCon -> [TyVar] -> [Id] -> MaybeT DsM Nabla
762 addConCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts=env } } x alt tvs args = do
763 let vi@(VI _ pos neg bot _) = lookupVarInfo ts x
764 -- First try to refute with a negative fact
765 guard (not (elemPmAltConSet alt neg))
766 -- Then see if any of the other solutions (remember: each of them is an
767 -- additional refinement of the possible values x could take) indicate a
768 -- contradiction
769 guard (all ((/= Disjoint) . eqPmAltCon alt . paca_con) pos)
770 -- Now we should be good! Add (alt, tvs, args) as a possible solution, or
771 -- refine an existing one
772 case find ((== Equal) . eqPmAltCon alt . paca_con) pos of
773 Just (PACA _con other_tvs other_args) -> do
774 -- We must unify existentially bound ty vars and arguments!
775 let ty_cts = equateTys (map mkTyVarTy tvs) (map mkTyVarTy other_tvs)
776 nabla' <- MaybeT $ addPhiCts nabla (listToBag ty_cts)
777 let add_var_ct nabla (a, b) = addVarCt nabla a b
778 foldlM add_var_ct nabla' $ zipEqual "addConCt" args other_args
779 Nothing -> do
780 let pos' = PACA alt tvs args : pos
781 let nabla_with bot' =
782 nabla{ nabla_tm_st = ts{ts_facts = addToUSDFM env x (vi{vi_pos = pos', vi_bot = bot'})} }
783 -- Do (2) in Note [Coverage checking Newtype matches]
784 case (alt, args) of
785 (PmAltConLike (RealDataCon dc), [y]) | isNewDataCon dc ->
786 case bot of
787 MaybeBot -> pure (nabla_with MaybeBot)
788 IsBot -> addBotCt (nabla_with MaybeBot) y
789 IsNotBot -> addNotBotCt (nabla_with MaybeBot) y
790 _ -> assert (isPmAltConMatchStrict alt )
791 pure (nabla_with IsNotBot) -- strict match ==> not ⊥
792
793 equateTys :: [Type] -> [Type] -> [PhiCt]
794 equateTys ts us =
795 [ PhiTyCt (mkPrimEqPred t u)
796 | (t, u) <- zipEqual "equateTys" ts us
797 -- The following line filters out trivial Refl constraints, so that we don't
798 -- need to initialise the type oracle that often
799 , not (eqType t u)
800 ]
801
802 -- | Adds a @x ~ y@ constraint by merging the two 'VarInfo's and record the
803 -- gained knowledge in 'Nabla'.
804 --
805 -- Returns @Nothing@ when there's a contradiction while merging. Returns @Just
806 -- nabla@ when the constraint was compatible with prior facts, in which case
807 -- @nabla@ has integrated the knowledge from the equality constraint.
808 --
809 -- See Note [TmState invariants].
810 addVarCt :: Nabla -> Id -> Id -> MaybeT DsM Nabla
811 addVarCt nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_facts = env } } x y =
812 case equateUSDFM env x y of
813 (Nothing, env') -> pure (nabla{ nabla_tm_st = ts{ ts_facts = env' } })
814 -- Add the constraints we had for x to y
815 (Just vi_x, env') -> do
816 let nabla_equated = nabla{ nabla_tm_st = ts{ts_facts = env'} }
817 -- and then gradually merge every positive fact we have on x into y
818 let add_pos nabla (PACA cl tvs args) = addConCt nabla y cl tvs args
819 nabla_pos <- foldlM add_pos nabla_equated (vi_pos vi_x)
820 -- Do the same for negative info
821 let add_neg nabla nalt = addNotConCt nabla y nalt
822 foldlM add_neg nabla_pos (pmAltConSetElems (vi_neg vi_x))
823
824 -- | Inspects a 'PmCoreCt' @let x = e@ by recording constraints for @x@ based
825 -- on the shape of the 'CoreExpr' @e@. Examples:
826 --
827 -- * For @let x = Just (42, 'z')@ we want to record the
828 -- constraints @x ~ Just a, a ~ (b, c), b ~ 42, c ~ 'z'@.
829 -- See 'data_con_app'.
830 -- * For @let x = unpackCString# "tmp"@ we want to record the literal
831 -- constraint @x ~ "tmp"@.
832 -- * For @let x = I# 42@ we want the literal constraint @x ~ 42@. Similar
833 -- for other literals. See 'coreExprAsPmLit'.
834 -- * Finally, if we have @let x = e@ and we already have seen @let y = e@, we
835 -- want to record @x ~ y@.
836 addCoreCt :: Nabla -> Id -> CoreExpr -> MaybeT DsM Nabla
837 addCoreCt nabla x e = do
838 simpl_opts <- initSimpleOpts <$> getDynFlags
839 let e' = simpleOptExpr simpl_opts e
840 -- lift $ tracePm "addCoreCt" (ppr x <+> dcolon <+> ppr (idType x) $$ ppr e $$ ppr e')
841 execStateT (core_expr x e') nabla
842 where
843 -- | Takes apart a 'CoreExpr' and tries to extract as much information about
844 -- literals and constructor applications as possible.
845 core_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
846 -- TODO: Handle newtypes properly, by wrapping the expression in a DataCon
847 -- This is the right thing for casts involving data family instances and
848 -- their representation TyCon, though (which are not visible in source
849 -- syntax). See Note [COMPLETE sets on data families]
850 -- core_expr x e | pprTrace "core_expr" (ppr x $$ ppr e) False = undefined
851 core_expr x (Cast e _co) = core_expr x e
852 core_expr x (Tick _t e) = core_expr x e
853 core_expr x e
854 | Just (pmLitAsStringLit -> Just s) <- coreExprAsPmLit e
855 , expr_ty `eqType` stringTy
856 -- See Note [Representation of Strings in TmState]
857 = case unpackFS s of
858 -- We need this special case to break a loop with coreExprAsPmLit
859 -- Otherwise we alternate endlessly between [] and ""
860 [] -> data_con_app x emptyInScopeSet nilDataCon []
861 s' -> core_expr x (mkListExpr charTy (map mkCharExpr s'))
862 | Just lit <- coreExprAsPmLit e
863 = pm_lit x lit
864 | Just (in_scope, _empty_floats@[], dc, _arg_tys, args)
865 <- exprIsConApp_maybe in_scope_env e
866 = data_con_app x in_scope dc args
867 -- See Note [Detecting pattern synonym applications in expressions]
868 | Var y <- e, Nothing <- isDataConId_maybe x
869 -- We don't consider DataCons flexible variables
870 = modifyT (\nabla -> addVarCt nabla x y)
871 | otherwise
872 -- Any other expression. Try to find other uses of a semantically
873 -- equivalent expression and represent them by the same variable!
874 = equate_with_similar_expr x e
875 where
876 expr_ty = exprType e
877 expr_in_scope = mkInScopeSet (exprFreeVars e)
878 in_scope_env = (expr_in_scope, const NoUnfolding)
879 -- It's inconvenient to get hold of a global in-scope set
880 -- here, but it'll only be needed if exprIsConApp_maybe ends
881 -- up substituting inside a forall or lambda (i.e. seldom)
882 -- so using exprFreeVars seems fine. See MR !1647.
883
884 -- | The @e@ in @let x = e@ had no familiar form. But we can still see if
885 -- see if we already encountered a constraint @let y = e'@ with @e'@
886 -- semantically equivalent to @e@, in which case we may add the constraint
887 -- @x ~ y@.
888 equate_with_similar_expr :: Id -> CoreExpr -> StateT Nabla (MaybeT DsM) ()
889 equate_with_similar_expr x e = do
890 rep <- StateT $ \nabla -> lift (representCoreExpr nabla e)
891 -- Note that @rep == x@ if we encountered @e@ for the first time.
892 modifyT (\nabla -> addVarCt nabla x rep)
893
894 bind_expr :: CoreExpr -> StateT Nabla (MaybeT DsM) Id
895 bind_expr e = do
896 x <- lift (lift (mkPmId (exprType e)))
897 core_expr x e
898 pure x
899
900 -- | Look at @let x = K taus theta es@ and generate the following
901 -- constraints (assuming universals were dropped from @taus@ before):
902 -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor.
903 -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@
904 -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
905 -- 4. @x ~ K as ys@
906 -- This is quite similar to PmCheck.pmConCts.
907 data_con_app :: Id -> InScopeSet -> DataCon -> [CoreExpr] -> StateT Nabla (MaybeT DsM) ()
908 data_con_app x in_scope dc args = do
909 let dc_ex_tvs = dataConExTyCoVars dc
910 arty = dataConSourceArity dc
911 (ex_ty_args, val_args) = splitAtList dc_ex_tvs args
912 ex_tys = map exprToType ex_ty_args
913 vis_args = reverse $ take arty $ reverse val_args
914 uniq_supply <- lift $ lift $ getUniqueSupplyM
915 let (_, ex_tvs) = cloneTyVarBndrs (mkEmptyTCvSubst in_scope) dc_ex_tvs uniq_supply
916 ty_cts = equateTys (map mkTyVarTy ex_tvs) ex_tys
917 -- 1. @x ≁ ⊥@ if 'K' is not a Newtype constructor (#18341)
918 when (not (isNewDataCon dc)) $
919 modifyT $ \nabla -> addNotBotCt nabla x
920 -- 2. @a_1 ~ tau_1, ..., a_n ~ tau_n@ for fresh @a_i@. See also #17703
921 modifyT $ \nabla -> MaybeT $ addPhiCts nabla (listToBag ty_cts)
922 -- 3. @y_1 ~ e_1, ..., y_m ~ e_m@ for fresh @y_i@
923 arg_ids <- traverse bind_expr vis_args
924 -- 4. @x ~ K as ys@
925 pm_alt_con_app x (PmAltConLike (RealDataCon dc)) ex_tvs arg_ids
926
927 -- | Adds a literal constraint, i.e. @x ~ 42@.
928 -- Also we assume that literal expressions won't diverge, so this
929 -- will add a @x ~/ ⊥@ constraint.
930 pm_lit :: Id -> PmLit -> StateT Nabla (MaybeT DsM) ()
931 pm_lit x lit = do
932 modifyT $ \nabla -> addNotBotCt nabla x
933 pm_alt_con_app x (PmAltLit lit) [] []
934
935 -- | Adds the given constructor application as a solution for @x@.
936 pm_alt_con_app :: Id -> PmAltCon -> [TyVar] -> [Id] -> StateT Nabla (MaybeT DsM) ()
937 pm_alt_con_app x con tvs args = modifyT $ \nabla -> addConCt nabla x con tvs args
938
939 -- | Finds a representant of the semantic equality class of the given @e@.
940 -- Which is the @x@ of a @let x = e'@ constraint (with @e@ semantically
941 -- equivalent to @e'@) we encountered earlier, or a fresh identifier if
942 -- there weren't any such constraints.
943 representCoreExpr :: Nabla -> CoreExpr -> DsM (Id, Nabla)
944 representCoreExpr nabla@MkNabla{ nabla_tm_st = ts@TmSt{ ts_reps = reps } } e
945 | Just rep <- lookupCoreMap reps e = pure (rep, nabla)
946 | otherwise = do
947 rep <- mkPmId (exprType e)
948 let reps' = extendCoreMap reps e rep
949 let nabla' = nabla{ nabla_tm_st = ts{ ts_reps = reps' } }
950 pure (rep, nabla')
951
952 -- | Like 'modify', but with an effectful modifier action
953 modifyT :: Monad m => (s -> m s) -> StateT s m ()
954 modifyT f = StateT $ fmap ((,) ()) . f
955
956 {- Note [The Pos/Neg invariant]
957 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
958 Invariant applying to each VarInfo: Whenever we have @C @tvs args@ in 'vi_pos',
959 any entry in 'vi_neg' must be incomparable to C (return Nothing) according to
960 'eqPmAltCons'. Those entries that are comparable either lead to a refutation
961 or are redundant. Examples:
962 * @x ~ Just y@, @x ≁ [Just]@. 'eqPmAltCon' returns @Equal@, so refute.
963 * @x ~ Nothing@, @x ≁ [Just]@. 'eqPmAltCon' returns @Disjoint@, so negative
964 info is redundant and should be discarded.
965 * @x ~ I# y@, @x ≁ [4,2]@. 'eqPmAltCon' returns @PossiblyOverlap@, so orthogal.
966 We keep this info in order to be able to refute a redundant match on i.e. 4
967 later on.
968
969 This carries over to pattern synonyms and overloaded literals. Say, we have
970 pattern Just42 = Just 42
971 case Just42 of x
972 Nothing -> ()
973 Just _ -> ()
974 Even though we had a solution for the value abstraction called x here in form
975 of a PatSynCon Just42, this solution is incomparable to both Nothing and
976 Just. Hence we retain the info in vi_neg, which eventually allows us to detect
977 the complete pattern match.
978
979 The Pos/Neg invariant extends to vi_rcm, which essentially stores positive
980 information. We make sure that vi_neg and vi_rcm never overlap. This isn't
981 strictly necessary since vi_rcm is just a cache, so doesn't need to be
982 accurate: Every suggestion of a possible ConLike from vi_rcm might be
983 refutable by the type oracle anyway. But it helps to maintain sanity while
984 debugging traces.
985
986 Note [Why record both positive and negative info?]
987 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
988 You might think that knowing positive info (like x ~ Just y) would render
989 negative info irrelevant, but not so because of pattern synonyms. E.g we might
990 know that x cannot match (Foo 4), where pattern Foo p = Just p
991
992 Also overloaded literals themselves behave like pattern synonyms. E.g if
993 postively we know that (x ~ I# y), we might also negatively want to record that
994 x does not match 45 f 45 = e2 f (I# 22#) = e3 f 45 = e4 --
995 Overlapped
996
997 Note [TmState invariants]
998 ~~~~~~~~~~~~~~~~~~~~~~~~~
999 The term oracle state is never obviously (i.e., without consulting the type
1000 oracle or doing inhabitation testing) contradictory. This implies a few
1001 invariants:
1002 * Whenever vi_pos overlaps with vi_neg according to 'eqPmAltCon', we refute.
1003 This is implied by the Note [Pos/Neg invariant].
1004 * Whenever vi_neg subsumes a COMPLETE set, we refute. We consult vi_rcm to
1005 detect this, but we could just compare whole COMPLETE sets to vi_neg every
1006 time, if it weren't for performance.
1007
1008 Maintaining these invariants in 'addVarCt' (the core of the term oracle) and
1009 'addNotConCt' is subtle.
1010 * Merging VarInfos. Example: Add the fact @x ~ y@ (see 'equate').
1011 - (COMPLETE) If we had @x ≁ True@ and @y ≁ False@, then we get
1012 @x ≁ [True,False]@. This is vacuous by matter of comparing to the built-in
1013 COMPLETE set, so should refute.
1014 - (Pos/Neg) If we had @x ≁ True@ and @y ~ True@, we have to refute.
1015 * Adding positive information. Example: Add the fact @x ~ K ys@ (see 'addConCt')
1016 - (Neg) If we had @x ≁ K@, refute.
1017 - (Pos) If we had @x ~ K2@, and that contradicts the new solution according to
1018 'eqPmAltCon' (ex. K2 is [] and K is (:)), then refute.
1019 - (Refine) If we had @x ≁ K zs@, unify each y with each z in turn.
1020 * Adding negative information. Example: Add the fact @x ≁ Nothing@ (see 'addNotConCt')
1021 - (Refut) If we have @x ~ K ys@, refute.
1022 - (COMPLETE) If K=Nothing and we had @x ≁ Just@, then we get
1023 @x ≁ [Just,Nothing]@. This is vacuous by matter of comparing to the built-in
1024 COMPLETE set, so should refute.
1025
1026 Note that merging VarInfo in equate can be done by calling out to 'addConCt' and
1027 'addNotConCt' for each of the facts individually.
1028
1029 Note [Representation of Strings in TmState]
1030 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1031 Instead of treating regular String literals as a PmLits, we treat it as a list
1032 of characters in the oracle for better overlap reasoning. The following example
1033 shows why:
1034
1035 f :: String -> ()
1036 f ('f':_) = ()
1037 f "foo" = ()
1038 f _ = ()
1039
1040 The second case is redundant, and we like to warn about it. Therefore either
1041 the oracle will have to do some smart conversion between the list and literal
1042 representation or treat is as the list it really is at runtime.
1043
1044 The "smart conversion" has the advantage of leveraging the more compact literal
1045 representation wherever possible, but is really nasty to get right with negative
1046 equalities: Just think of how to encode @x /= "foo"@.
1047 The "list" option is far simpler, but incurs some overhead in representation and
1048 warning messages (which can be alleviated by someone with enough dedication).
1049
1050 Note [Detecting pattern synonym applications in expressions]
1051 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1052 At the moment we fail to detect pattern synonyms in scrutinees and RHS of
1053 guards. This could be alleviated with considerable effort and complexity, but
1054 the returns are meager. Consider:
1055
1056 pattern P
1057 pattern Q
1058 case P 15 of
1059 Q _ -> ...
1060 P 15 ->
1061
1062 Compared to the situation where P and Q are DataCons, the lack of generativity
1063 means we could never flag Q as redundant. (also see Note [Undecidable Equality
1064 for PmAltCons] in PmTypes.) On the other hand, if we fail to recognise the
1065 pattern synonym, we flag the pattern match as inexhaustive. That wouldn't happen
1066 if we had knowledge about the scrutinee, in which case the oracle basically
1067 knows "If it's a P, then its field is 15".
1068
1069 This is a pretty narrow use case and I don't think we should to try to fix it
1070 until a user complains energetically.
1071
1072 Note [Completeness checking with required Thetas]
1073 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1074 Consider the situation in #11224
1075
1076 import Text.Read (readMaybe)
1077 pattern PRead :: Read a => () => a -> String
1078 pattern PRead x <- (readMaybe -> Just x)
1079 f :: String -> Int
1080 f (PRead x) = x
1081 f (PRead xs) = length xs
1082 f _ = 0
1083
1084 Is the first match exhaustive on the PRead synonym? Should the second line thus
1085 deemed redundant? The answer is, of course, No! The required theta is like a
1086 hidden parameter which must be supplied at the pattern match site, so PRead
1087 is much more like a view pattern (where behavior depends on the particular value
1088 passed in).
1089 The simple solution here is to forget in 'addNotConCt' that we matched
1090 on synonyms with a required Theta like @PRead@, so that subsequent matches on
1091 the same constructor are never flagged as redundant. The consequence is that
1092 we no longer detect the actually redundant match in
1093
1094 g :: String -> Int
1095 g (PRead x) = x
1096 g (PRead y) = y -- redundant!
1097 g _ = 0
1098
1099 But that's a small price to pay, compared to the proper solution here involving
1100 storing required arguments along with the PmAltConLike in 'vi_neg'.
1101
1102 Note [Strict fields and variables of unlifted type]
1103 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1104 Binders of unlifted type (and strict fields) are unlifted by construction;
1105 they are conceived with an implicit @≁⊥@ constraint to begin with. Hence,
1106 desugaring in "GHC.HsToCore.Pmc" is entirely unconcerned by strict fields,
1107 since the forcing happens *before* pattern matching.
1108 And the φ constructor constraints emitted by 'GHC.HsToCore.Pmc.checkGrd'
1109 have complex binding semantics (binding type constraints and unlifted fields),
1110 so unliftedness semantics are entirely confined to the oracle.
1111
1112 These are the moving parts:
1113
1114 1. For each strict (or more generally, unlifted) field @s@ of a 'PhiConCt'
1115 we have to add a @s ≁ ⊥@ constraint in the corresponding case of
1116 'addPhiTmCt'. Strict fields are devoid of ⊥ by construction, there's
1117 nothing that a bang pattern would act on. Example from #18341:
1118
1119 data T = MkT !Int
1120 f :: T -> ()
1121 f (MkT _) | False = () -- inaccessible
1122 f (MkT !_) | False = () -- redundant, not only inaccessible!
1123 f _ = ()
1124
1125 The second clause desugars to @MkT n <- x, !n@. When coverage checked,
1126 the 'PmCon' @MkT n <- x@ refines the set of values that reach the bang
1127 pattern with the φ constraints @MkT n <- x@ (Nothing surprising so far).
1128 Upon that constraint, it disperses into two lower-level δ constraints
1129 @x ~ MkT n, n ≁ ⊥@ per Equation (3) in Figure 7 of the paper.
1130
1131 Checking the 'PmBang' @!n@ will then try to add the
1132 constraint @n ~ ⊥@ to this set to get the diverging set, which is found
1133 to be empty. Hence the whole clause is detected as redundant, as
1134 expected.
1135
1136 2. Similarly, when performing the 'inhabitationTest', when instantiating a
1137 constructor we call 'instCon', which generates a higher-level φ
1138 constructor constraint.
1139
1140 3. The preceding points handle unlifted constructor fields, but there also
1141 are regular binders of unlifted type.
1142 Since the oracle as implemented has no notion of scoping and bindings,
1143 we can't know *when* an unlifted variable comes into scope. But that's
1144 not actually a problem, because we can just add the @x ≁ ⊥@ to the
1145 'emptyVarInfo' when we first encounter it.
1146 -}
1147
1148 -------------------------
1149 -- * Inhabitation testing
1150 --
1151 -- Figure 8 in the LYG paper.
1152
1153 tyStateRefined :: TyState -> TyState -> Bool
1154 -- Makes use of the fact that the two TyStates we compare will never have the
1155 -- same sequence number. It is invalid to call this function when a is not a
1156 -- refinement of b or vice versa!
1157 tyStateRefined a b = ty_st_n a /= ty_st_n b
1158
1159 markDirty :: Id -> Nabla -> Nabla
1160 markDirty x nabla@MkNabla{nabla_tm_st = ts@TmSt{ts_dirty = dirty} } =
1161 nabla{ nabla_tm_st = ts{ ts_dirty = extendDVarSet dirty x } }
1162
1163 traverseDirty :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
1164 traverseDirty f ts@TmSt{ts_facts = env, ts_dirty = dirty} =
1165 go (uniqDSetToList dirty) env
1166 where
1167 go [] env = pure ts{ts_facts=env}
1168 go (x:xs) !env = do
1169 vi' <- f (lookupVarInfo ts x)
1170 go xs (addToUSDFM env x vi')
1171
1172 traverseAll :: Monad m => (VarInfo -> m VarInfo) -> TmState -> m TmState
1173 traverseAll f ts@TmSt{ts_facts = env} = do
1174 env' <- traverseUSDFM f env
1175 pure ts{ts_facts = env'}
1176
1177 -- | Makes sure the given 'Nabla' is still inhabited, by trying to instantiate
1178 -- all dirty variables (or all variables when the 'TyState' changed) to concrete
1179 -- inhabitants. It returns a 'Nabla' with the *same* inhabitants, but with some
1180 -- amount of work cached (like failed instantiation attempts) from the test.
1181 --
1182 -- The \(∇ ⊢ x inh\) judgment form in Figure 8 of the LYG paper.
1183 inhabitationTest :: Int -> TyState -> Nabla -> MaybeT DsM Nabla
1184 inhabitationTest 0 _ nabla = pure nabla
1185 inhabitationTest fuel old_ty_st nabla@MkNabla{ nabla_tm_st = ts } = {-# SCC "inhabitationTest" #-} do
1186 -- lift $ tracePm "inhabitation test" $ vcat
1187 -- [ ppr fuel
1188 -- , ppr old_ty_st
1189 -- , ppr nabla
1190 -- , text "tyStateRefined:" <+> ppr (tyStateRefined old_ty_st (nabla_ty_st nabla))
1191 -- ]
1192 -- When type state didn't change, we only need to traverse dirty VarInfos
1193 ts' <- if tyStateRefined old_ty_st (nabla_ty_st nabla)
1194 then traverseAll test_one ts
1195 else traverseDirty test_one ts
1196 pure nabla{ nabla_tm_st = ts'{ts_dirty=emptyDVarSet}}
1197 where
1198 nabla_not_dirty = nabla{ nabla_tm_st = ts{ts_dirty=emptyDVarSet} }
1199 test_one :: VarInfo -> MaybeT DsM VarInfo
1200 test_one vi =
1201 lift (varNeedsTesting old_ty_st nabla vi) >>= \case
1202 True -> do
1203 -- lift $ tracePm "test_one" (ppr vi)
1204 -- No solution yet and needs testing
1205 -- We have to test with a Nabla where all dirty bits are cleared
1206 instantiate (fuel-1) nabla_not_dirty vi
1207 _ -> pure vi
1208
1209 -- | Checks whether the given 'VarInfo' needs to be tested for inhabitants.
1210 -- Returns `False` when we can skip the inhabitation test, presuming it would
1211 -- say "yes" anyway. See Note [Shortcutting the inhabitation test].
1212 varNeedsTesting :: TyState -> Nabla -> VarInfo -> DsM Bool
1213 varNeedsTesting _ MkNabla{nabla_tm_st=tm_st} vi
1214 | elemDVarSet (vi_id vi) (ts_dirty tm_st) = pure True
1215 varNeedsTesting _ _ vi
1216 | notNull (vi_pos vi) = pure False
1217 varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} _
1218 -- Same type state => still inhabited
1219 | not (tyStateRefined old_ty_st new_ty_st) = pure False
1220 varNeedsTesting old_ty_st MkNabla{nabla_ty_st=new_ty_st} vi = do
1221 -- These normalisations are relatively expensive, but still better than having
1222 -- to perform a full inhabitation test
1223 (_, _, old_norm_ty) <- tntrGuts <$> pmTopNormaliseType old_ty_st (idType $ vi_id vi)
1224 (_, _, new_norm_ty) <- tntrGuts <$> pmTopNormaliseType new_ty_st (idType $ vi_id vi)
1225 if old_norm_ty `eqType` new_norm_ty
1226 then pure False
1227 else pure True
1228
1229 -- | Returns (Just vi) if at least one member of each ConLike in the COMPLETE
1230 -- set satisfies the oracle
1231 --
1232 -- Internally uses and updates the CompleteMatchs in vi_rcm.
1233 --
1234 -- NB: Does /not/ filter each CompleteMatch with the oracle; members may
1235 -- remain that do not statisfy it. This lazy approach just
1236 -- avoids doing unnecessary work.
1237 instantiate :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
1238 instantiate fuel nabla vi = {-# SCC "instantiate" #-}
1239 (instBot fuel nabla vi <|> instCompleteSets fuel nabla vi)
1240
1241 -- | The \(⊢_{Bot}\) rule from the paper
1242 instBot :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
1243 instBot _fuel nabla vi = {-# SCC "instBot" #-} do
1244 _nabla' <- addBotCt nabla (vi_id vi)
1245 pure vi
1246
1247 addNormalisedTypeMatches :: Nabla -> Id -> DsM (ResidualCompleteMatches, Nabla)
1248 addNormalisedTypeMatches nabla@MkNabla{ nabla_ty_st = ty_st } x
1249 = trvVarInfo add_matches nabla x
1250 where
1251 add_matches vi@VI{ vi_rcm = rcm }
1252 -- important common case, shaving down allocations of PmSeriesG by -5%
1253 | isRcmInitialised rcm = pure (rcm, vi)
1254 add_matches vi@VI{ vi_rcm = rcm } = do
1255 norm_res_ty <- normaliseSourceTypeWHNF ty_st (idType x)
1256 env <- dsGetFamInstEnvs
1257 rcm' <- case splitReprTyConApp_maybe env norm_res_ty of
1258 Just (rep_tc, _args, _co) -> addTyConMatches rep_tc rcm
1259 Nothing -> addCompleteMatches rcm
1260 pure (rcm', vi{ vi_rcm = rcm' })
1261
1262 -- | Does a 'splitTyConApp_maybe' and then tries to look through a data family
1263 -- application to find the representation TyCon, to which the data constructors
1264 -- are attached. Returns the representation TyCon, the TyCon application args
1265 -- and a representational coercion that will be Refl for non-data family apps.
1266 splitReprTyConApp_maybe :: FamInstEnvs -> Type -> Maybe (TyCon, [Type], Coercion)
1267 splitReprTyConApp_maybe env ty =
1268 uncurry (tcLookupDataFamInst env) <$> splitTyConApp_maybe ty
1269
1270 -- | This is the |-Inst rule from the paper (section 4.5). Tries to
1271 -- find an inhabitant in every complete set by instantiating with one their
1272 -- constructors. If there is any complete set where we can't find an
1273 -- inhabitant, the whole thing is uninhabited. It returns the updated 'VarInfo'
1274 -- where all the attempted ConLike instantiations have been purged from the
1275 -- 'ResidualCompleteMatches', which functions as a cache.
1276 instCompleteSets :: Int -> Nabla -> VarInfo -> MaybeT DsM VarInfo
1277 instCompleteSets fuel nabla vi = {-# SCC "instCompleteSets" #-} do
1278 let x = vi_id vi
1279 (rcm, nabla) <- lift (addNormalisedTypeMatches nabla x)
1280 nabla <- foldM (\nabla cls -> instCompleteSet fuel nabla x cls) nabla (getRcm rcm)
1281 pure (lookupVarInfo (nabla_tm_st nabla) x)
1282
1283 anyConLikeSolution :: (ConLike -> Bool) -> [PmAltConApp] -> Bool
1284 anyConLikeSolution p = any (go . paca_con)
1285 where
1286 go (PmAltConLike cl) = p cl
1287 go _ = False
1288
1289 -- | @instCompleteSet fuel nabla x cls@ iterates over @cls@ until it finds
1290 -- the first inhabited ConLike (as per 'instCon'). Any failed instantiation
1291 -- attempts of a ConLike are recorded as negative information in the returned
1292 -- 'Nabla', so that later calls to this function can skip repeatedly fruitless
1293 -- instantiation of that same constructor.
1294 --
1295 -- Note that the returned Nabla is just a different representation of the
1296 -- original Nabla, not a proper refinement! No positive information will be
1297 -- added, only negative information from failed instantiation attempts,
1298 -- entirely as an optimisation.
1299 instCompleteSet :: Int -> Nabla -> Id -> CompleteMatch -> MaybeT DsM Nabla
1300 instCompleteSet fuel nabla x cs
1301 | anyConLikeSolution (`elementOfUniqDSet` (cmConLikes cs)) (vi_pos vi)
1302 -- No need to instantiate a constructor of this COMPLETE set if we already
1303 -- have a solution!
1304 = pure nabla
1305 | not (completeMatchAppliesAtType (varType x) cs)
1306 = pure nabla
1307 | otherwise
1308 = {-# SCC "instCompleteSet" #-} go nabla (sorted_candidates cs)
1309 where
1310 vi = lookupVarInfo (nabla_tm_st nabla) x
1311
1312 sorted_candidates :: CompleteMatch -> [ConLike]
1313 sorted_candidates cm
1314 -- If there aren't many candidates, we can try to sort them by number of
1315 -- strict fields, type constraints, etc., so that we are fast in the
1316 -- common case
1317 -- (either many simple constructors *or* few "complicated" ones).
1318 | sizeUniqDSet cs <= 5 = sortBy compareConLikeTestability (uniqDSetToList cs)
1319 | otherwise = uniqDSetToList cs
1320 where cs = cmConLikes cm
1321
1322 go :: Nabla -> [ConLike] -> MaybeT DsM Nabla
1323 go _ [] = mzero
1324 go nabla (RealDataCon dc:_)
1325 -- See Note [DataCons that are definitely inhabitable]
1326 -- Recall that dc can't be in vi_neg, because then it would be
1327 -- deleted from the residual COMPLETE set.
1328 | isDataConTriviallyInhabited dc
1329 = pure nabla
1330 go nabla (con:cons) = do
1331 let x = vi_id vi
1332 let recur_not_con = do
1333 nabla' <- addNotConCt nabla x (PmAltConLike con)
1334 go nabla' cons
1335 (nabla <$ instCon fuel nabla x con) -- return the original nabla, not the
1336 -- refined one!
1337 <|> recur_not_con -- Assume that x can't be con. Encode that fact
1338 -- with addNotConCt and recur.
1339
1340 -- | Is this 'DataCon' trivially inhabited, that is, without needing to perform
1341 -- any inhabitation testing because of strict/unlifted fields or type
1342 -- equalities? See Note [DataCons that are definitely inhabitable]
1343 isDataConTriviallyInhabited :: DataCon -> Bool
1344 isDataConTriviallyInhabited dc
1345 | isTyConTriviallyInhabited (dataConTyCon dc) = True
1346 isDataConTriviallyInhabited dc =
1347 null (dataConTheta dc) && -- (1)
1348 null (dataConImplBangs dc) && -- (2)
1349 null (dataConUnliftedFieldTys dc) -- (3)
1350
1351 dataConUnliftedFieldTys :: DataCon -> [Type]
1352 dataConUnliftedFieldTys =
1353 -- A representation-polymorphic field requires an inhabitation test, hence compare to
1354 -- @Just True@
1355 filter ((== Just True) . isLiftedType_maybe) . map scaledThing . dataConOrigArgTys
1356
1357 isTyConTriviallyInhabited :: TyCon -> Bool
1358 isTyConTriviallyInhabited tc = elementOfUniqSet (getUnique tc) triviallyInhabitedTyConKeys
1359
1360 -- | All these types are trivially inhabited
1361 triviallyInhabitedTyConKeys :: UniqSet Unique
1362 triviallyInhabitedTyConKeys = mkUniqSet [
1363 charTyConKey, doubleTyConKey, floatTyConKey,
1364 intTyConKey, int8TyConKey, int16TyConKey, int32TyConKey, int64TyConKey,
1365 intPrimTyConKey, int8PrimTyConKey, int16PrimTyConKey, int32PrimTyConKey, int64PrimTyConKey,
1366 wordTyConKey, word8TyConKey, word16TyConKey, word32TyConKey, word64TyConKey,
1367 wordPrimTyConKey, word8PrimTyConKey, word16PrimTyConKey, word32PrimTyConKey, word64PrimTyConKey,
1368 trTyConTyConKey
1369 ]
1370
1371 compareConLikeTestability :: ConLike -> ConLike -> Ordering
1372 -- We should instantiate DataCons first, because they are likely to occur in
1373 -- multiple COMPLETE sets at once and we might find that multiple COMPLETE sets
1374 -- are inhabitated by instantiating only a single DataCon.
1375 compareConLikeTestability PatSynCon{} _ = GT
1376 compareConLikeTestability _ PatSynCon{} = GT
1377 compareConLikeTestability (RealDataCon a) (RealDataCon b) = mconcat
1378 -- Thetas are most expensive to check, as they might incur a whole new round
1379 -- of inhabitation testing
1380 [ comparing (fast_length . dataConTheta)
1381 -- Unlifted or strict fields only incur an inhabitation test for that
1382 -- particular field. Still something to avoid.
1383 , comparing unlifted_or_strict_fields
1384 ] a b
1385 where
1386 fast_length :: [a] -> Int
1387 fast_length xs = atLength length 6 xs 5 -- @min 6 (length xs)@, but O(1)
1388
1389 -- An upper bound on the number of strict or unlifted fields. Approximate in
1390 -- the unlikely bogus case of an unlifted field that has a bang.
1391 unlifted_or_strict_fields :: DataCon -> Int
1392 unlifted_or_strict_fields dc = fast_length (dataConImplBangs dc)
1393 + fast_length (dataConUnliftedFieldTys dc)
1394
1395 -- | @instCon fuel nabla (x::match_ty) K@ tries to instantiate @x@ to @K@ by
1396 -- adding the proper constructor constraint.
1397 --
1398 -- See Note [Instantiating a ConLike].
1399 instCon :: Int -> Nabla -> Id -> ConLike -> MaybeT DsM Nabla
1400 instCon fuel nabla@MkNabla{nabla_ty_st = ty_st} x con = {-# SCC "instCon" #-} MaybeT $ do
1401 let hdr what = "instCon " ++ show fuel ++ " " ++ what
1402 env <- dsGetFamInstEnvs
1403 let match_ty = idType x
1404 tracePm (hdr "{") $
1405 ppr con <+> text "... <-" <+> ppr x <+> dcolon <+> ppr match_ty
1406 norm_match_ty <- normaliseSourceTypeWHNF ty_st match_ty
1407 mb_sigma_univ <- matchConLikeResTy env ty_st norm_match_ty con
1408 case mb_sigma_univ of
1409 Just sigma_univ -> do
1410 let (_univ_tvs, ex_tvs, eq_spec, thetas, _req_theta, field_tys, _con_res_ty)
1411 = conLikeFullSig con
1412 -- Following Note [Instantiating a ConLike]:
1413 -- (1) _req_theta has been tested in 'matchConLikeResTy'
1414 -- (2) Instantiate fresh existentials
1415 (sigma_ex, _) <- cloneTyVarBndrs sigma_univ ex_tvs <$> getUniqueSupplyM
1416 -- (3) Substitute provided constraints bound by the constructor.
1417 -- These are added to the type oracle as new facts (in a moment)
1418 let gammas = substTheta sigma_ex (eqSpecPreds eq_spec ++ thetas)
1419 -- (4) Instantiate fresh term variables as arguments to the constructor
1420 let field_tys' = substTys sigma_ex $ map scaledThing field_tys
1421 arg_ids <- mapM mkPmId field_tys'
1422 tracePm (hdr "(cts)") $ vcat
1423 [ ppr x <+> dcolon <+> ppr match_ty
1424 , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
1425 , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
1426 , ppr (map (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs)
1427 , ppr gammas
1428 , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids)
1429 ]
1430 -- (5) Finally add the new constructor constraint
1431 runMaybeT $ do
1432 -- Case (2) of Note [Strict fields and variables of unlifted type]
1433 let alt = PmAltConLike con
1434 let branching_factor = length $ filterUnliftedFields alt arg_ids
1435 let ct = PhiConCt x alt ex_tvs gammas arg_ids
1436 nabla1 <- traceWhenFailPm (hdr "(ct unsatisfiable) }") (ppr ct) $
1437 addPhiTmCt nabla ct
1438 -- See Note [Fuel for the inhabitation test]
1439 let new_fuel
1440 | branching_factor <= 1 = fuel
1441 | otherwise = min fuel 2
1442 lift $ tracePm (hdr "(ct satisfiable)") $ vcat
1443 [ ppr ct
1444 , ppr x <+> dcolon <+> ppr match_ty
1445 , text "In WHNF:" <+> ppr (isSourceTypeInWHNF match_ty) <+> ppr norm_match_ty
1446 , ppr con <+> dcolon <+> text "... ->" <+> ppr _con_res_ty
1447 , ppr (map (\tv -> ppr tv <+> char '↦' <+> ppr (substTyVar sigma_univ tv)) _univ_tvs)
1448 , ppr gammas
1449 , ppr (map (\x -> ppr x <+> dcolon <+> ppr (idType x)) arg_ids)
1450 , ppr branching_factor
1451 , ppr new_fuel
1452 ]
1453 nabla2 <- traceWhenFailPm (hdr "(inh test failed) }") (ppr nabla1) $
1454 inhabitationTest new_fuel (nabla_ty_st nabla) nabla1
1455 lift $ tracePm (hdr "(inh test succeeded) }") (ppr nabla2)
1456 pure nabla2
1457 Nothing -> do
1458 tracePm (hdr "(match_ty not instance of res_ty) }") empty
1459 pure (Just nabla) -- Matching against match_ty failed. Inhabited!
1460 -- See Note [Instantiating a ConLike].
1461
1462 -- | @matchConLikeResTy _ _ ty K@ tries to match @ty@ against the result
1463 -- type of @K@, @res_ty@. It returns a substitution @s@ for @K@'s universal
1464 -- tyvars such that @s(res_ty)@ equals @ty@ if successful.
1465 --
1466 -- Make sure that @ty@ is normalised before.
1467 --
1468 -- See Note [Matching against a ConLike result type].
1469 matchConLikeResTy :: FamInstEnvs -> TyState -> Type -> ConLike -> DsM (Maybe TCvSubst)
1470 matchConLikeResTy env _ ty (RealDataCon dc) = pure $ do
1471 (rep_tc, tc_args, _co) <- splitReprTyConApp_maybe env ty
1472 if rep_tc == dataConTyCon dc
1473 then Just (zipTCvSubst (dataConUnivTyVars dc) tc_args)
1474 else Nothing
1475 matchConLikeResTy _ (TySt _ inert) ty (PatSynCon ps) = {-# SCC "matchConLikeResTy" #-} runMaybeT $ do
1476 let (univ_tvs,req_theta,_,_,_,con_res_ty) = patSynSig ps
1477 subst <- MaybeT $ pure $ tcMatchTy con_res_ty ty
1478 guard $ all (`elemTCvSubst` subst) univ_tvs -- See the Note about T11336b
1479 if null req_theta
1480 then pure subst
1481 else do
1482 let req_theta' = substTys subst req_theta
1483 satisfiable <- lift $ initTcDsForSolver $ tcCheckWanteds inert req_theta'
1484 if satisfiable
1485 then pure subst
1486 else mzero
1487
1488 {- Note [Soundness and completeness]
1489 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1490 Soundness and completeness of the pattern-match checker depend entirely on the
1491 soundness and completeness of the inhabitation test.
1492
1493 Achieving both soundness and completeness at the same time is undecidable.
1494 See also T17977 and Note [Fuel for the inhabitation test].
1495 Losing soundness would make the algorithm pointless; hence we give up on
1496 completeness, but try to get as close as possible (how close is called
1497 the 'precision' of the algorithm).
1498
1499 Soundness means that you
1500 1. Can remove clauses flagged as redundant without changing program semantics
1501 (no false positives).
1502 2. Can be sure that your program is free of incomplete pattern matches
1503 when the checker doesn't flag any inexhaustive definitions
1504 (no false negatives).
1505
1506 A complete algorithm would mean that
1507 1. When a clause can be deleted without changing program semantics, it will
1508 be flagged as redundant (no false negatives).
1509 2. A program that is free of incomplete pattern matches will never have a
1510 definition be flagged as inexhaustive (no false positives).
1511
1512 Via the LYG algorithm, we reduce both these properties to a property on
1513 the inhabitation test of refinementment types:
1514 *Soundness*: If the inhabitation test says "no" for a given refinement type
1515 Nabla, then it provably has no inhabitant.
1516 *Completeness*: If the inhabitation test says "yes" for a given refinement type
1517 Nabla, then it provably has an inhabitant.
1518 Our test is sound, but incomplete, so there are instances where we say
1519 "yes" but in fact the Nabla is empty. Which entails false positive exhaustivity
1520 and false negative redundancy warnings, as above.
1521
1522 In summary, we have the following correspondence:
1523
1524 Property | Exhaustiveness warnings | Redundancy warnings | Inhabitation test |
1525 -------------|-------------------------|---------------------|-------------------|
1526 Soundness | No false negatives | No false positives | Only says "no" |
1527 | | | if there is no |
1528 | | | inhabitant |
1529 Completeness | No false positives | No false negatives | Only says "yes" |
1530 | | | if there is an |
1531 | | | inhabitant |
1532
1533 Note [Shortcutting the inhabitation test]
1534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1535 Generally, we have to re-test a refinement type for inhabitants whenever we
1536 add a new constraint. Often, we can say "no" early, upon trying to add a
1537 contradicting constraint, see Note [The Pos/Neg invariant]. Still, COMPLETE
1538 sets and type evidence are best handled in a delayed fashion, because of
1539 the recursive nature of the test and our fuel-based approach.
1540 But even then there are some cases in which we can skip the full test,
1541 because we are sure that the refinement type is still inhabited. These
1542 conditions are monitored by 'varNeedsTesting'. It returns
1543
1544 - `True` whenever a full inhabitation test is needed
1545 - `False` whenever the test can be skipped, amounting to an inhabitation test
1546 that says "yes".
1547
1548 According to Note [Soundness and Completeness], this test will never compromise
1549 soundness: The `True` case just forwards to the actual inhabitation test and the
1550 `False` case amounts to an inhabitation test that is trivially sound, because it
1551 never says "no".
1552
1553 Of course, if the returns says `False`, Completeness (and thus Precision) of the
1554 algorithm is affected, but we get to skip costly inhabitation tests. We try to
1555 trade as little Precision as possible against as much Performance as possible.
1556 Here are the tests, in order:
1557
1558 1. If a variable is dirty (because of a newly added negative term constraint),
1559 we have to test.
1560 2. If a variable has positive information, we don't have to test: The
1561 positive information acts as constructive proof for inhabitation.
1562 3. If the type state didn't change, there is no need to test.
1563 4. If the variable's normalised type didn't change, there is no need to test.
1564 5. Otherwise, we have to test.
1565
1566 Why (1) before (2)?
1567 -------------------
1568 Consider the reverse for (T18960):
1569 pattern P x = x
1570 {-# COMPLETE P :: () #-}
1571 foo = case () of x@(P _) -> ()
1572 This should be exhaustive. But if we say "We know `x` has solution `()`, so it's
1573 inhabited", then we'll get a warning saying that `()` wasn't matched.
1574 But the match on `P` added the new negative information to the uncovered set,
1575 in the process of which we marked `x` as dirty. By giving the dirty flag a
1576 higher priority than positive info, we get to test again and see that `x` is
1577 uninhabited and the match is exhaustive.
1578
1579 But suppose that `P` wasn't mentioned in any COMPLETE set. Then we simply
1580 don't mark `x` as dirty and will emit a warning again (which we would anyway),
1581 without running a superfluous inhabitation test. That speeds up T17836
1582 considerably.
1583
1584 Why (2) before (3) and (4)?
1585 ---------------------------
1586 Simply because (2) is more efficient to test than (3) (not by a lot), which
1587 is more efficient to test than (4), which is still more efficient than running
1588 the full inhabitation test (5).
1589
1590 Note [Fuel for the inhabitation test]
1591 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1592 Whether or not a type is inhabited is undecidable in general, see also
1593 Note [Soundness and Completeness]. As a result, we can run into infinite
1594 loops in `inhabitationTest`. Therefore, we adopt a fuel-based approach to
1595 prevent that.
1596
1597 Consider the following example:
1598
1599 data Abyss = MkAbyss !Abyss
1600 stareIntoTheAbyss :: Abyss -> a
1601 stareIntoTheAbyss x = case x of {}
1602
1603 In principle, stareIntoTheAbyss is exhaustive, since there is no way to
1604 construct a terminating value using MkAbyss. But this can't be proven by mere
1605 instantiation and requires an inductive argument, which `inhabitationTest`
1606 currently isn't equipped to do.
1607
1608 In order to prevent endless instantiation attempts in @inhabitationTest@, we
1609 use the fuel as an upper bound on such attempts.
1610
1611 The same problem occurs with recursive newtypes, like in the following code:
1612
1613 newtype Chasm = MkChasm Chasm
1614 gazeIntoTheChasm :: Chasm -> a
1615 gazeIntoTheChasm x = case x of {} -- Erroneously warned as non-exhaustive
1616
1617 So this limitation is somewhat understandable.
1618
1619 Note that even with this recursion detection, there is still a possibility that
1620 `inhabitationTest` can run in exponential time in the amount of fuel. Consider
1621 the following data type:
1622
1623 data T = MkT !T !T !T
1624
1625 If we try to instantiate each of its fields, that will require us to once again
1626 check if `MkT` is inhabitable in each of those three fields, which in turn will
1627 require us to check if `MkT` is inhabitable again... As you can see, the
1628 branching factor adds up quickly, and if the initial fuel is, say,
1629 100, then the inhabiation test will effectively take forever.
1630
1631 To mitigate this, we check the branching factor every time we are about to do
1632 inhabitation testing in 'instCon'. If the branching factor exceeds 1
1633 (i.e., if there is potential for exponential runtime), then we limit the
1634 maximum recursion depth to 1 to mitigate the problem. If the branching factor
1635 is exactly 1 (i.e., we have a linear chain instead of a tree), then it's okay
1636 to stick with a larger maximum recursion depth.
1637
1638 In #17977 we saw that the defaultRecTcMaxBound (100 at the time of writing) was
1639 too large and had detrimental effect on performance of the coverage checker.
1640 Given that we only commit to a best effort anyway, we decided to substantially
1641 decrement the fuel to 4, at the cost of precision in some edge cases
1642 like
1643
1644 data Nat = Z | S Nat
1645 data Down :: Nat -> Type where
1646 Down :: !(Down n) -> Down (S n)
1647 f :: Down (S (S (S (S (S Z))))) -> ()
1648 f x = case x of {}
1649
1650 Since the coverage won't bother to instantiate Down 4 levels deep to see that it
1651 is in fact uninhabited, it will emit a inexhaustivity warning for the case.
1652
1653 Note [DataCons that are definitely inhabitable]
1654 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1655 Another microoptimization applies to data types like this one:
1656
1657 data S a = S ![a] !T
1658
1659 Even though there is a strict field of type [a], it's quite silly to call
1660 'instCon' on it, since it's "obvious" that it is inhabitable. To make this
1661 intuition formal, we say that a DataCon C is definitely inhabitable (DI) if:
1662
1663 1. C has no equality constraints (since they might be unsatisfiable)
1664 2. C has no strict arguments (since they might be uninhabitable)
1665 3. C has no unlifted argument types (since they might be uninhabitable)
1666
1667 It's relatively cheap to check if a DataCon is DI, so before we call 'instCon'
1668 on a constructor of a COMPLETE set, we filter out all of the DI ones.
1669
1670 This fast path shaves down -7% allocations for PmSeriesG, for example.
1671
1672 Note [Matching against a ConLike result type]
1673 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1674 Given a ConLike
1675
1676 > C :: forall us. R => ... -> res_ty
1677
1678 is a pattern `C ...` compatible with the type `ty`? Clearly that is the case if
1679 `res_ty` /subsumes/ `ty` and the required constraints `R` (strictly a feature of
1680 pattern synonyms) are satisfiable. In that case, 'matchConLikeResTy' returns a
1681 substitution σ over `us` such that `σ(res_ty) == ty`.
1682
1683 It's surprisingly tricky to implement correctly, and works quite different for
1684 DataCons and PatSynCons:
1685
1686 * For data cons, we look at `ty` and see if it's a TyCon app `T t1 ... tn`.
1687 If that is the case, we make sure that `C` is a DataCon of `T` and return
1688 a substitution mapping `C`'s universal tyvars `us` to `t1`...`tn`.
1689
1690 Wrinkle: Since `T` might be a data family TyCon, we have to look up its
1691 representation TyCon before we compare to `C`'s TyCon.
1692 So we use 'splitReprTyConApp_maybe' instead of 'splitTyConApp_maybe'.
1693
1694 * For pattern synonyms, we directly match `ty` against `res_ty` to get the
1695 substitution σ. See Note [Pattern synonym result type] in "GHC.Core.PatSyn".
1696
1697 Fortunately, we don't have to treat data family TyCons specially:
1698 Pattern synonyms /never/ apply to a data family representation TyCon.
1699 We do have to consider the required constraints `σ(R)`, though, as we have
1700 seen in #19475. That is done by solving them as Wanted constraints given the
1701 inert set of the current type state (which is part of a Nabla's TySt). Since
1702 spinning up a constraint solver session is costly, we only do so in the rare
1703 cases that a pattern synonym actually carries any required constraints.
1704
1705 We can get into the strange situation that not all universal type variables
1706 `us` occur in `res_ty`. Example from T11336b:
1707
1708 instance C Proxy where ... -- impl uninteresting
1709 pattern P :: forall f a. C f => f a -> Proxy a -- impl uninteresting
1710
1711 fun :: Proxy a -> ()
1712 fun (P Proxy) = ()
1713 fun (P Proxy) = () -- ideally detected as redundant
1714
1715 `f` is a universal type variable and `C f` the required constraint of
1716 pattern synonym `P`. But `f` doesn't occur in the result type `Proxy a` of
1717 `P`, so σ will not even have `f` in its in-scope set. It's a bit unclear
1718 what to do here; we might want to freshen `f` to `f'` and see if we can
1719 solve `C f'` as a Wanted constraint, which we most likely can't.
1720 Hence, we simply skip the freshening and declare the match as failed when
1721 there is a variable like `f`. For the definition of `fun`, that
1722 means we will not remember that we matched on `P` and thus will
1723 not detect its second clause as redundant.
1724
1725 See Note [Pattern synonym result type] in "GHC.Core.PatSyn" for similar
1726 oddities.
1727
1728 Note [Instantiating a ConLike]
1729 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1730 `instCon` implements the the \(Inst\) function from Figure 8 of the LYG paper.
1731
1732 Given the following type of ConLike `K`
1733
1734 > K :: forall us. R => forall es. P => t1 -> ... -> tn -> res_ty
1735
1736 and a variable `x::match_ty`, it tries to find an instantiation
1737 `K ex_tvs gammas arg_ids :: match_ty` (for fresh `arg_ids`) and ultimately adds
1738 a constructor constraint `K ex_tvs gammas arg_ids <- x` to the given Nabla.
1739
1740 As a first step, it tries (via 'matchConLikeResTy') to match `match_ty` against
1741 `res_ty` and checks that that the required constraints @R@ are satisfiable.
1742 See Note [Matching against a ConLike result type].
1743
1744 If matching /fails/, it trivially (and conservatively) reports "inhabited" by
1745 returning the unrefined input Nabla. After all, the match might have failed due
1746 to incomplete type information in Nabla.
1747 (Later type refinement from unpacking GADT constructors might monomorphise
1748 `match_ty` so much that `res_ty` ultimately subsumes it.)
1749
1750 If matching /succeeds/, we get a substitution σ for the (universal)
1751 tyvars `us`. After applying σ, we get
1752
1753 > K @σ(us) :: σ(R) => forall σ(es). σ(P) => σ(t1) -> ... -> σ(tn) -> match_ty
1754
1755 The existentials `es` might still occur in argument types `σ(tn)`, though.
1756 Now 'instCon' performs the following steps:
1757
1758 1. It drops the required constraints `σ(R)`, as they have already been
1759 discharged by 'matchConLikeResTy'.
1760 2. It instantiates fresh binders `es'` for the other type variables `es`
1761 bound by `K` and adds the mapping to σ to get σ', so that we have
1762
1763 > K @σ(us) @es' :: σ'(P) => σ'(t1) -> ... -> σ'(tn) -> match_ty
1764
1765 3. It adds new type constraints from the substituted
1766 provided constraints @σ'(P)@.
1767 4. It substitutes and conjures new binders @arg_ids@ for the argument types
1768 @σ'(t1) ... σ'(tn)@.
1769 5. It adds a term constraint @K es' σ'(P) arg_ids <- x@, which handles
1770 the details regarding type constraints and unlifted fields.
1771
1772 And finally the extended 'Nabla' is returned if all the constraints were
1773 compatible.
1774 -}
1775
1776 --------------------------------------
1777 -- * Generating inhabitants of a Nabla
1778 --
1779 -- This is important for warnings. Roughly corresponds to G in Figure 6 of the
1780 -- LYG paper, with a few tweaks for better warning messages.
1781
1782 -- | @generateInhabitingPatterns vs n nabla@ returns a list of at most @n@ (but
1783 -- perhaps empty) refinements of @nabla@ that represent inhabited patterns.
1784 -- Negative information is only retained if literals are involved or for
1785 -- recursive GADTs.
1786 generateInhabitingPatterns :: [Id] -> Int -> Nabla -> DsM [Nabla]
1787 -- See Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
1788 generateInhabitingPatterns _ 0 _ = pure []
1789 generateInhabitingPatterns [] _ nabla = pure [nabla]
1790 generateInhabitingPatterns (x:xs) n nabla = do
1791 tracePm "generateInhabitingPatterns" (ppr n <+> ppr (x:xs) $$ ppr nabla)
1792 let VI _ pos neg _ _ = lookupVarInfo (nabla_tm_st nabla) x
1793 case pos of
1794 _:_ -> do
1795 -- All solutions must be valid at once. Try to find candidates for their
1796 -- fields. Example:
1797 -- f x@(Just _) True = case x of SomePatSyn _ -> ()
1798 -- after this clause, we want to report that
1799 -- * @f Nothing _@ is uncovered
1800 -- * @f x False@ is uncovered
1801 -- where @x@ will have two possibly compatible solutions, @Just y@ for
1802 -- some @y@ and @SomePatSyn z@ for some @z@. We must find evidence for @y@
1803 -- and @z@ that is valid at the same time. These constitute arg_vas below.
1804 let arg_vas = concatMap paca_ids pos
1805 generateInhabitingPatterns (arg_vas ++ xs) n nabla
1806 []
1807 -- When there are literals involved, just print negative info
1808 -- instead of listing missed constructors
1809 | notNull [ l | PmAltLit l <- pmAltConSetElems neg ]
1810 -> generateInhabitingPatterns xs n nabla
1811 [] -> try_instantiate x xs n nabla
1812 where
1813 -- | Tries to instantiate a variable by possibly following the chain of
1814 -- newtypes and then instantiating to all ConLikes of the wrapped type's
1815 -- minimal residual COMPLETE set.
1816 try_instantiate :: Id -> [Id] -> Int -> Nabla -> DsM [Nabla]
1817 -- Convention: x binds the outer constructor in the chain, y the inner one.
1818 try_instantiate x xs n nabla = do
1819 (_src_ty, dcs, rep_ty) <- tntrGuts <$> pmTopNormaliseType (nabla_ty_st nabla) (idType x)
1820 mb_stuff <- runMaybeT $ instantiate_newtype_chain x nabla dcs
1821 case mb_stuff of
1822 Nothing -> pure []
1823 Just (y, newty_nabla) -> do
1824 let vi = lookupVarInfo (nabla_tm_st newty_nabla) y
1825 env <- dsGetFamInstEnvs
1826 rcm <- case splitReprTyConApp_maybe env rep_ty of
1827 Just (tc, _, _) -> addTyConMatches tc (vi_rcm vi)
1828 Nothing -> addCompleteMatches (vi_rcm vi)
1829
1830 -- Test all COMPLETE sets for inhabitants (n inhs at max). Take care of ⊥.
1831 clss <- pickApplicableCompleteSets (nabla_ty_st nabla) rep_ty rcm
1832 case NE.nonEmpty (uniqDSetToList . cmConLikes <$> clss) of
1833 Nothing ->
1834 -- No COMPLETE sets ==> inhabited
1835 generateInhabitingPatterns xs n newty_nabla
1836 Just clss -> do
1837 -- Try each COMPLETE set, pick the one with the smallest number of
1838 -- inhabitants
1839 nablass' <- forM clss (instantiate_cons y rep_ty xs n newty_nabla)
1840 let nablas' = minimumBy (comparing length) nablass'
1841 if null nablas' && vi_bot vi /= IsNotBot
1842 then generateInhabitingPatterns xs n newty_nabla -- bot is still possible. Display a wildcard!
1843 else pure nablas'
1844
1845 -- | Instantiates a chain of newtypes, beginning at @x@.
1846 -- Turns @x nabla [T,U,V]@ to @(y, nabla')@, where @nabla'@ we has the fact
1847 -- @x ~ T (U (V y))@.
1848 instantiate_newtype_chain :: Id -> Nabla -> [(Type, DataCon, Type)] -> MaybeT DsM (Id, Nabla)
1849 instantiate_newtype_chain x nabla [] = pure (x, nabla)
1850 instantiate_newtype_chain x nabla ((_ty, dc, arg_ty):dcs) = do
1851 y <- lift $ mkPmId arg_ty
1852 -- Newtypes don't have existentials (yet?!), so passing an empty
1853 -- list as ex_tvs.
1854 nabla' <- addConCt nabla x (PmAltConLike (RealDataCon dc)) [] [y]
1855 instantiate_newtype_chain y nabla' dcs
1856
1857 instantiate_cons :: Id -> Type -> [Id] -> Int -> Nabla -> [ConLike] -> DsM [Nabla]
1858 instantiate_cons _ _ _ _ _ [] = pure []
1859 instantiate_cons _ _ _ 0 _ _ = pure []
1860 instantiate_cons _ ty xs n nabla _
1861 -- We don't want to expose users to GHC-specific constructors for Int etc.
1862 | fmap (isTyConTriviallyInhabited . fst) (splitTyConApp_maybe ty) == Just True
1863 = generateInhabitingPatterns xs n nabla
1864 instantiate_cons x ty xs n nabla (cl:cls) = do
1865 -- The following line is where we call out to the inhabitationTest!
1866 mb_nabla <- runMaybeT $ instCon 4 nabla x cl
1867 tracePm "instantiate_cons" (vcat [ ppr x <+> dcolon <+> ppr (idType x)
1868 , ppr ty
1869 , ppr cl
1870 , ppr nabla
1871 , ppr mb_nabla
1872 , ppr n ])
1873 con_nablas <- case mb_nabla of
1874 Nothing -> pure []
1875 -- NB: We don't prepend arg_vars as we don't have any evidence on
1876 -- them and we only want to split once on a data type. They are
1877 -- inhabited, otherwise the inhabitation test would have refuted.
1878 Just nabla' -> generateInhabitingPatterns xs n nabla'
1879 other_cons_nablas <- instantiate_cons x ty xs (n - length con_nablas) nabla cls
1880 pure (con_nablas ++ other_cons_nablas)
1881
1882 pickApplicableCompleteSets :: TyState -> Type -> ResidualCompleteMatches -> DsM [CompleteMatch]
1883 -- See Note [Implementation of COMPLETE pragmas] on what "applicable" means
1884 pickApplicableCompleteSets ty_st ty rcm = do
1885 let cl_res_ty_ok :: ConLike -> DsM Bool
1886 cl_res_ty_ok cl = do
1887 env <- dsGetFamInstEnvs
1888 isJust <$> matchConLikeResTy env ty_st ty cl
1889 let cm_applicable :: CompleteMatch -> DsM Bool
1890 cm_applicable cm = do
1891 cls_ok <- allM cl_res_ty_ok (uniqDSetToList (cmConLikes cm))
1892 let match_ty_ok = completeMatchAppliesAtType ty cm
1893 pure (cls_ok && match_ty_ok)
1894 applicable_cms <- filterM cm_applicable (getRcm rcm)
1895 tracePm "pickApplicableCompleteSets:" $
1896 vcat
1897 [ ppr ty
1898 , ppr rcm
1899 , ppr applicable_cms
1900 ]
1901 return applicable_cms
1902
1903 {- Note [Why inhabitationTest doesn't call generateInhabitingPatterns]
1904 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1905 Why can't we define `inhabitationTest` (IT) in terms of
1906 `generateInhabitingPatterns` (GIP) as
1907
1908 inhabitationTest nabla = do
1909 nablas <- lift $ generateInhabitingPatterns all_variables 1 nabla
1910 guard (notNull nablas)
1911
1912 There are a few technical reasons, like the lack of a fuel-tracking approach
1913 to stay decidable, that could be overcome. But the nail in the coffin is
1914 performance: In order to provide good warning messages, GIP commits to *one*
1915 COMPLETE set, and goes through some hoops to find the minimal one. This implies
1916 it has to look at *all* constructors in the residual COMPLETE matches and see if
1917 they match, if only to filter out ill-typed COMPLETE sets
1918 (see Note [Implementation of COMPLETE pragmas]). That is untractable for an
1919 efficient IT on huge enumerations.
1920
1921 But we still need GIP to produce the Nablas as proxies for
1922 uncovered patterns that we display warnings for. It's fine to pay this price
1923 once at the end, but IT is called far more often than that.
1924 -}