Fix and document cloneWC
[ghc.git] / compiler / typecheck / TcHoleErrors.hs
1 {-# OPTIONS_GHC -fno-warn-orphans #-} -- We don't want to spread the HasOccName
2 -- instance for Either
3 module TcHoleErrors ( findValidHoleFits ) where
4
5 import GhcPrelude
6
7 import TcRnTypes
8 import TcRnMonad
9 import TcMType
10 import TcEvidence
11 import TcType
12 import Type
13 import DataCon
14 import Name
15 import RdrName ( pprNameProvenance , GlobalRdrElt (..), globalRdrEnvElts )
16 import PrelNames ( gHC_ERR )
17 import Id
18 import VarSet
19 import VarEnv
20 import Bag
21 import ConLike ( ConLike(..) )
22 import Util
23 import TcEnv (tcLookup)
24 import Outputable
25 import DynFlags
26 import Maybes
27 import FV ( fvVarList, fvVarSet, unionFV, mkFVs, FV )
28
29 import Control.Arrow ( (&&&) )
30
31 import Control.Monad ( filterM, replicateM )
32 import Data.List ( partition, sort, sortOn, nubBy )
33 import Data.Graph ( graphFromEdges, topSort )
34 import Data.Function ( on )
35
36
37 import TcSimplify ( simpl_top, runTcSDeriveds )
38 import TcUnify ( tcSubType_NC )
39
40 import ExtractDocs ( extractDocs )
41 import qualified Data.Map as Map
42 import HsDoc ( HsDocString, unpackHDS, DeclDocMap(..) )
43 import HscTypes ( ModIface(..) )
44 import LoadIface ( loadInterfaceForNameMaybe )
45
46 {-
47 Note [Valid hole fits include ...]
48 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
49 `findValidHoleFits` returns the "Valid hole fits include ..." message.
50 For example, look at the following definitions in a file called test.hs:
51
52 import Data.List (inits)
53
54 f :: [String]
55 f = _ "hello, world"
56
57 The hole in `f` would generate the message:
58
59 • Found hole: _ :: [Char] -> [String]
60 • In the expression: _
61 In the expression: _ "hello, world"
62 In an equation for ‘f’: f = _ "hello, world"
63 • Relevant bindings include f :: [String] (bound at test.hs:6:1)
64 Valid hole fits include
65 lines :: String -> [String]
66 (imported from ‘Prelude’ at mpt.hs:3:8-9
67 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
68 words :: String -> [String]
69 (imported from ‘Prelude’ at mpt.hs:3:8-9
70 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
71 inits :: forall a. [a] -> [[a]]
72 with inits @Char
73 (imported from ‘Data.List’ at mpt.hs:4:19-23
74 (and originally defined in ‘base-4.11.0.0:Data.OldList’))
75 repeat :: forall a. a -> [a]
76 with repeat @String
77 (imported from ‘Prelude’ at mpt.hs:3:8-9
78 (and originally defined in ‘GHC.List’))
79 fail :: forall (m :: * -> *). Monad m => forall a. String -> m a
80 with fail @[] @String
81 (imported from ‘Prelude’ at mpt.hs:3:8-9
82 (and originally defined in ‘GHC.Base’))
83 return :: forall (m :: * -> *). Monad m => forall a. a -> m a
84 with return @[] @String
85 (imported from ‘Prelude’ at mpt.hs:3:8-9
86 (and originally defined in ‘GHC.Base’))
87 pure :: forall (f :: * -> *). Applicative f => forall a. a -> f a
88 with pure @[] @String
89 (imported from ‘Prelude’ at mpt.hs:3:8-9
90 (and originally defined in ‘GHC.Base’))
91 read :: forall a. Read a => String -> a
92 with read @[String]
93 (imported from ‘Prelude’ at mpt.hs:3:8-9
94 (and originally defined in ‘Text.Read’))
95 mempty :: forall a. Monoid a => a
96 with mempty @([Char] -> [String])
97 (imported from ‘Prelude’ at mpt.hs:3:8-9
98 (and originally defined in ‘GHC.Base’))
99
100 Valid hole fits are found by checking top level identifiers and local bindings
101 in scope for whether their type can be instantiated to the the type of the hole.
102 Additionally, we also need to check whether all relevant constraints are solved
103 by choosing an identifier of that type as well, see Note [Relevant Constraints]
104
105 Since checking for subsumption results in the side-effect of type variables
106 being unified by the simplifier, we need to take care to restore them after
107 to being flexible type variables after we've checked for subsumption.
108 This is to avoid affecting the hole and later checks by prematurely having
109 unified one of the free unification variables.
110
111 When outputting, we sort the hole fits by the size of the types we'd need to
112 apply by type application to the type of the fit to to make it fit. This is done
113 in order to display "more relevant" suggestions first. Another option is to
114 sort by building a subsumption graph of fits, i.e. a graph of which fits subsume
115 what other fits, and then outputting those fits which are are subsumed by other
116 fits (i.e. those more specific than other fits) first. This results in the ones
117 "closest" to the type of the hole to be displayed first.
118
119 To help users understand how the suggested fit works, we also display the values
120 that the quantified type variables would take if that fit is used, like
121 `mempty @([Char] -> [String])` and `pure @[] @String` in the example above.
122 If -XTypeApplications is enabled, this can even be copied verbatim as a
123 replacement for the hole.
124
125
126 Note [Nested implications]
127 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
128
129 For the simplifier to be able to use any givens present in the enclosing
130 implications to solve relevant constraints, we nest the wanted subsumption
131 constraints and relevant constraints within the enclosing implications.
132
133 As an example, let's look at the following code:
134
135 f :: Show a => a -> String
136 f x = show _
137
138 The hole will result in the hole constraint:
139
140 [WD] __a1ph {0}:: a0_a1pd[tau:2] (CHoleCan: ExprHole(_))
141
142 Here the nested implications are just one level deep, namely:
143
144 [Implic {
145 TcLevel = 2
146 Skolems = a_a1pa[sk:2]
147 No-eqs = True
148 Status = Unsolved
149 Given = $dShow_a1pc :: Show a_a1pa[sk:2]
150 Wanted =
151 WC {wc_simple =
152 [WD] __a1ph {0}:: a_a1pd[tau:2] (CHoleCan: ExprHole(_))
153 [WD] $dShow_a1pe {0}:: Show a_a1pd[tau:2] (CDictCan(psc))}
154 Binds = EvBindsVar<a1pi>
155 Needed inner = []
156 Needed outer = []
157 the type signature for:
158 f :: forall a. Show a => a -> String }]
159
160 As we can see, the givens say that the information about the skolem
161 `a_a1pa[sk:2]` fulfills the Show constraint.
162
163 The simples are:
164
165 [[WD] __a1ph {0}:: a0_a1pd[tau:2] (CHoleCan: ExprHole(_)),
166 [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)]
167
168 I.e. the hole `a0_a1pd[tau:2]` and the constraint that the type of the hole must
169 fulfill `Show a0_a1pd[tau:2])`.
170
171 So when we run the check, we need to make sure that the
172
173 [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)
174
175 Constraint gets solved. When we now check for whether `x :: a0_a1pd[tau:2]` fits
176 the hole in `tcCheckHoleFit`, the call to `tcSubType` will end up writing the
177 meta type variable `a0_a1pd[tau:2] := a_a1pa[sk:2]`. By wrapping the wanted
178 constraints needed by tcSubType_NC and the relevant constraints (see
179 Note [Relevant Constraints] for more details) in the nested implications, we
180 can pass the information in the givens along to the simplifier. For our example,
181 we end up needing to check whether the following constraints are soluble.
182
183 WC {wc_impl =
184 Implic {
185 TcLevel = 2
186 Skolems = a_a1pa[sk:2]
187 No-eqs = True
188 Status = Unsolved
189 Given = $dShow_a1pc :: Show a_a1pa[sk:2]
190 Wanted =
191 WC {wc_simple =
192 [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical)}
193 Binds = EvBindsVar<a1pl>
194 Needed inner = []
195 Needed outer = []
196 the type signature for:
197 f :: forall a. Show a => a -> String }}
198
199 But since `a0_a1pd[tau:2] := a_a1pa[sk:2]` and we have from the nested
200 implications that Show a_a1pa[sk:2] is a given, this is trivial, and we end up
201 with a final WC of WC {}, confirming x :: a0_a1pd[tau:2] as a match.
202
203 To avoid side-effects on the nested implications, we create a new EvBindsVar so
204 that any changes to the ev binds during a check remains localised to that check.
205
206
207 Note [Valid refinement hole fits include ...]
208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
209 When the `-frefinement-level-hole-fits=N` flag is given, we additionally look
210 for "valid refinement hole fits"", i.e. valid hole fits with up to N
211 additional holes in them.
212
213 With `-frefinement-level-hole-fits=0` (the default), GHC will find all
214 identifiers 'f' (top-level or nested) that will fit in the hole.
215
216 With `-frefinement-level-hole-fits=1`, GHC will additionally find all
217 applications 'f _' that will fit in the hole, where 'f' is an in-scope
218 identifier, applied to single argument. It will also report the type of the
219 needed argument (a new hole).
220
221 And similarly as the number of arguments increases
222
223 As an example, let's look at the following code:
224
225 f :: [Integer] -> Integer
226 f = _
227
228 with `-frefinement-level-hole-fits=1`, we'd get:
229
230 Valid refinement hole fits include
231
232 foldl1 (_ :: Integer -> Integer -> Integer)
233 with foldl1 @[] @Integer
234 where foldl1 :: forall (t :: * -> *).
235 Foldable t =>
236 forall a. (a -> a -> a) -> t a -> a
237 foldr1 (_ :: Integer -> Integer -> Integer)
238 with foldr1 @[] @Integer
239 where foldr1 :: forall (t :: * -> *).
240 Foldable t =>
241 forall a. (a -> a -> a) -> t a -> a
242 const (_ :: Integer)
243 with const @Integer @[Integer]
244 where const :: forall a b. a -> b -> a
245 ($) (_ :: [Integer] -> Integer)
246 with ($) @'GHC.Types.LiftedRep @[Integer] @Integer
247 where ($) :: forall a b. (a -> b) -> a -> b
248 fail (_ :: String)
249 with fail @((->) [Integer]) @Integer
250 where fail :: forall (m :: * -> *).
251 Monad m =>
252 forall a. String -> m a
253 return (_ :: Integer)
254 with return @((->) [Integer]) @Integer
255 where return :: forall (m :: * -> *). Monad m => forall a. a -> m a
256 (Some refinement hole fits suppressed;
257 use -fmax-refinement-hole-fits=N or -fno-max-refinement-hole-fits)
258
259 Which are hole fits with holes in them. This allows e.g. beginners to
260 discover the fold functions and similar, but also allows for advanced users
261 to figure out the valid functions in the Free monad, e.g.
262
263 instance Functor f => Monad (Free f) where
264 Pure a >>= f = f a
265 Free f >>= g = Free (fmap _a f)
266
267 Will output (with -frefinment-level-hole-fits=1):
268 Found hole: _a :: Free f a -> Free f b
269 Where: ‘a’, ‘b’ are rigid type variables bound by
270 the type signature for:
271 (>>=) :: forall a b. Free f a -> (a -> Free f b) -> Free f b
272 at fms.hs:25:12-14
273 ‘f’ is a rigid type variable bound by
274 ...
275 Relevant bindings include
276 g :: a -> Free f b (bound at fms.hs:27:16)
277 f :: f (Free f a) (bound at fms.hs:27:10)
278 (>>=) :: Free f a -> (a -> Free f b) -> Free f b
279 (bound at fms.hs:25:12)
280 ...
281 Valid refinement hole fits include
282 ...
283 (=<<) (_ :: a -> Free f b)
284 with (=<<) @(Free f) @a @b
285 where (=<<) :: forall (m :: * -> *) a b.
286 Monad m =>
287 (a -> m b) -> m a -> m b
288 (imported from ‘Prelude’ at fms.hs:5:18-22
289 (and originally defined in ‘GHC.Base’))
290 ...
291
292 Where `(=<<) _` is precisely the function we want (we ultimately want `>>= g`).
293
294 We find these refinement suggestions by considering hole fits that don't
295 fit the type of the hole, but ones that would fit if given an additional
296 argument. We do this by creating a new type variable with `newOpenFlexiTyVar`
297 (e.g. `t_a1/m[tau:1]`), and then considering hole fits of the type
298 `t_a1/m[tau:1] -> v` where `v` is the type of the hole.
299
300 Since the simplifier is free to unify this new type variable with any type, we
301 can discover any identifiers that would fit if given another identifier of a
302 suitable type. This is then generalized so that we can consider any number of
303 additional arguments by setting the `-frefinement-level-hole-fits` flag to any
304 number, and then considering hole fits like e.g. `foldl _ _` with two additional
305 arguments.
306
307 To make sure that the refinement hole fits are useful, we check that the types
308 of the additional holes have a concrete value and not just an invented type
309 variable. This eliminates suggestions such as `head (_ :: [t0 -> a]) (_ :: t0)`,
310 and limits the number of less than useful refinement hole fits.
311
312 Additionally, to further aid the user in their implementation, we show the
313 types of the holes the binding would have to be applied to in order to work.
314 In the free monad example above, this is demonstrated with
315 `(=<<) (_ :: a -> Free f b)`, which tells the user that the `(=<<)` needs to
316 be applied to an expression of type `a -> Free f b` in order to match.
317 If -XScopedTypeVariables is enabled, this hole fit can even be copied verbatim.
318
319
320 Note [Relevant Constraints]
321 ~~~~~~~~~~~~~~~~~~~
322
323 As highlighted by Trac #14273, we need to check any relevant constraints as well
324 as checking for subsumption. Relevant constraints are the simple constraints
325 whose free unification variables are mentioned in the type of the hole.
326
327 In the simplest case, these are all non-hole constraints in the simples, such
328 as is the case in
329
330 f :: String
331 f = show _
332
333 Where the simples will be :
334
335 [[WD] __a1kz {0}:: a0_a1kv[tau:1] (CHoleCan: ExprHole(_)),
336 [WD] $dShow_a1kw {0}:: Show a0_a1kv[tau:1] (CNonCanonical)]
337
338 However, when there are multiple holes, we need to be more careful. As an
339 example, Let's take a look at the following code:
340
341 f :: Show a => a -> String
342 f x = show (_b (show _a))
343
344 Here there are two holes, `_a` and `_b`, and the simple constraints passed to
345 findValidHoleFits are:
346
347 [[WD] _a_a1pi {0}:: String
348 -> a0_a1pd[tau:2] (CHoleCan: ExprHole(_b)),
349 [WD] _b_a1ps {0}:: a1_a1po[tau:2] (CHoleCan: ExprHole(_a)),
350 [WD] $dShow_a1pe {0}:: Show a0_a1pd[tau:2] (CNonCanonical),
351 [WD] $dShow_a1pp {0}:: Show a1_a1po[tau:2] (CNonCanonical)]
352
353
354 Here we have the two hole constraints for `_a` and `_b`, but also additional
355 constraints that these holes must fulfill. When we are looking for a match for
356 the hole `_a`, we filter the simple constraints to the "Relevant constraints",
357 by throwing out all hole constraints and any constraints which do not mention
358 a variable mentioned in the type of the hole. For hole `_a`, we will then
359 only require that the `$dShow_a1pp` constraint is solved, since that is
360 the only non-hole constraint that mentions any free type variables mentioned in
361 the hole constraint for `_a`, namely `a_a1pd[tau:2]` , and similarly for the
362 hole `_b` we only require that the `$dShow_a1pe` constraint is solved.
363
364 Note [Leaking errors]
365 ~~~~~~~~~~~~~~~~~~~
366
367 When considering candidates, GHC believes that we're checking for validity in
368 actual source. However, As evidenced by #15321, #15007 and #15202, this can
369 cause bewildering error messages. The solution here is simple: if a candidate
370 would cause the type checker to error, it is not a valid hole fit, and thus it
371 is discarded.
372
373 -}
374
375
376
377
378 data HoleFitDispConfig = HFDC { showWrap :: Bool
379 , showWrapVars :: Bool
380 , showType :: Bool
381 , showProv :: Bool
382 , showMatches :: Bool }
383
384 debugHoleFitDispConfig :: HoleFitDispConfig
385 debugHoleFitDispConfig = HFDC True True True False False
386
387
388 -- We read the various -no-show-*-of-hole-fits flags
389 -- and set the display config accordingly.
390 getHoleFitDispConfig :: TcM HoleFitDispConfig
391 getHoleFitDispConfig
392 = do { sWrap <- goptM Opt_ShowTypeAppOfHoleFits
393 ; sWrapVars <- goptM Opt_ShowTypeAppVarsOfHoleFits
394 ; sType <- goptM Opt_ShowTypeOfHoleFits
395 ; sProv <- goptM Opt_ShowProvOfHoleFits
396 ; sMatc <- goptM Opt_ShowMatchesOfHoleFits
397 ; return HFDC{ showWrap = sWrap, showWrapVars = sWrapVars
398 , showProv = sProv, showType = sType
399 , showMatches = sMatc } }
400
401 -- Which sorting algorithm to use
402 data SortingAlg = NoSorting -- Do not sort the fits at all
403 | BySize -- Sort them by the size of the match
404 | BySubsumption -- Sort by full subsumption
405 deriving (Eq, Ord)
406
407 getSortingAlg :: TcM SortingAlg
408 getSortingAlg =
409 do { shouldSort <- goptM Opt_SortValidHoleFits
410 ; subsumSort <- goptM Opt_SortBySubsumHoleFits
411 ; sizeSort <- goptM Opt_SortBySizeHoleFits
412 -- We default to sizeSort unless it has been explicitly turned off
413 -- or subsumption sorting has been turned on.
414 ; return $ if not shouldSort
415 then NoSorting
416 else if subsumSort
417 then BySubsumption
418 else if sizeSort
419 then BySize
420 else NoSorting }
421
422 -- HoleFit is the type we use for valid hole fits. It contains the
423 -- element that was checked, the Id of that element as found by `tcLookup`,
424 -- and the refinement level of the fit, which is the number of extra argument
425 -- holes that this fit uses (e.g. if hfRefLvl is 2, the fit is for `Id _ _`).
426 data HoleFit = HoleFit { hfElem :: Maybe GlobalRdrElt -- The element that was
427 -- if a global, nothing
428 -- if it is a local.
429 , hfId :: Id -- The elements id in the TcM
430 , hfType :: TcType -- The type of the id, possibly zonked
431 , hfRefLvl :: Int -- The number of holes in this fit
432 , hfWrap :: [TcType] -- The wrapper for the match
433 , hfMatches :: [TcType] -- What the refinement
434 -- variables got matched with,
435 -- if anything
436 , hfDoc :: Maybe HsDocString } -- Documentation of this
437 -- HoleFit, if available.
438
439 hfName :: HoleFit -> Name
440 hfName = idName . hfId
441
442 hfIsLcl :: HoleFit -> Bool
443 hfIsLcl hf = case hfElem hf of
444 Just gre -> gre_lcl gre
445 Nothing -> True
446
447 -- We define an Eq and Ord instance to be able to build a graph.
448 instance Eq HoleFit where
449 (==) = (==) `on` hfId
450
451 -- We compare HoleFits by their gre_name instead of their Id, since we don't
452 -- want our tests to be affected by the non-determinism of `nonDetCmpVar`,
453 -- which is used to compare Ids. When comparing, we want HoleFits with a lower
454 -- refinement level to come first.
455 instance Ord HoleFit where
456 compare a b = cmp a b
457 where cmp = if hfRefLvl a == hfRefLvl b
458 then compare `on` hfName
459 else compare `on` hfRefLvl
460
461 instance Outputable HoleFit where
462 ppr = pprHoleFit debugHoleFitDispConfig
463
464 instance (HasOccName a, HasOccName b) => HasOccName (Either a b) where
465 occName = either occName occName
466
467 instance HasOccName GlobalRdrElt where
468 occName = occName . gre_name
469
470 -- If enabled, we go through the fits and add any associated documentation,
471 -- by looking it up in the module or the environment (for local fits)
472 addDocs :: [HoleFit] -> TcM [HoleFit]
473 addDocs fits =
474 do { showDocs <- goptM Opt_ShowDocsOfHoleFits
475 ; if showDocs
476 then do { (_, DeclDocMap lclDocs, _) <- extractDocs <$> getGblEnv
477 ; mapM (upd lclDocs) fits }
478 else return fits }
479 where
480 msg = text "TcHoleErrors addDocs"
481 lookupInIface name (ModIface { mi_decl_docs = DeclDocMap dmap })
482 = Map.lookup name dmap
483 upd lclDocs fit =
484 let name = hfName fit in
485 do { doc <- if hfIsLcl fit
486 then pure (Map.lookup name lclDocs)
487 else do { mbIface <- loadInterfaceForNameMaybe msg name
488 ; return $ mbIface >>= lookupInIface name }
489 ; return $ fit {hfDoc = doc} }
490
491 -- For pretty printing hole fits, we display the name and type of the fit,
492 -- with added '_' to represent any extra arguments in case of a non-zero
493 -- refinement level.
494 pprHoleFit :: HoleFitDispConfig -> HoleFit -> SDoc
495 pprHoleFit (HFDC sWrp sWrpVars sTy sProv sMs) hf = hang display 2 provenance
496 where name = case hfElem hf of
497 Just gre -> gre_name gre
498 Nothing -> hfName hf
499 ty = hfType hf
500 matches = hfMatches hf
501 wrap = hfWrap hf
502 tyApp = sep $ map ((text "@" <>) . pprParendType) wrap
503 tyAppVars = sep $ punctuate comma $
504 map (\(v,t) -> ppr v <+> text "~" <+> pprParendType t) $
505 zip vars wrap
506 where
507 vars = unwrapTypeVars ty
508 -- Attempts to get all the quantified type variables in a type,
509 -- e.g.
510 -- return :: forall (m :: * -> *) Monad m => (forall a . a) -> m a
511 -- into [m, a]
512 unwrapTypeVars :: Type -> [TyVar]
513 unwrapTypeVars t = vars ++ case splitFunTy_maybe unforalled of
514 Just (_, unfunned) -> unwrapTypeVars unfunned
515 _ -> []
516 where (vars, unforalled) = splitForAllTys t
517 holeVs = sep $ map (parens . (text "_" <+> dcolon <+>) . ppr) matches
518 holeDisp = if sMs then holeVs
519 else sep $ replicate (length matches) $ text "_"
520 occDisp = pprPrefixOcc name
521 tyDisp = ppWhen sTy $ dcolon <+> ppr ty
522 has = not . null
523 wrapDisp = ppWhen (has wrap && (sWrp || sWrpVars))
524 $ text "with" <+> if sWrp || not sTy
525 then occDisp <+> tyApp
526 else tyAppVars
527 docs = case hfDoc hf of
528 Just d ->
529 text "{-^" <>
530 (vcat . map text . lines . unpackHDS) d
531 <> text "-}"
532 _ -> empty
533 funcInfo = ppWhen (has matches && sTy) $
534 text "where" <+> occDisp <+> tyDisp
535 subDisp = occDisp <+> if has matches then holeDisp else tyDisp
536 display = subDisp $$ nest 2 (funcInfo $+$ docs $+$ wrapDisp)
537 provenance = ppWhen sProv $ parens $
538 case hfElem hf of
539 Just gre -> pprNameProvenance gre
540 Nothing -> text "bound at" <+> ppr (getSrcLoc name)
541
542 getLocalBindings :: TidyEnv -> Ct -> TcM [Id]
543 getLocalBindings tidy_orig ct
544 = do { (env1, _) <- zonkTidyOrigin tidy_orig (ctLocOrigin loc)
545 ; go env1 [] (removeBindingShadowing $ tcl_bndrs lcl_env) }
546 where
547 loc = ctEvLoc (ctEvidence ct)
548 lcl_env = ctLocEnv loc
549
550 go :: TidyEnv -> [Id] -> [TcBinder] -> TcM [Id]
551 go _ sofar [] = return (reverse sofar)
552 go env sofar (tc_bndr : tc_bndrs) =
553 case tc_bndr of
554 TcIdBndr id _ -> keep_it id
555 _ -> discard_it
556 where
557 discard_it = go env sofar tc_bndrs
558 keep_it id = go env (id:sofar) tc_bndrs
559
560 -- See Note [Valid hole fits include ...]
561 findValidHoleFits :: TidyEnv --The tidy_env for zonking
562 -> [Implication] --Enclosing implications for givens
563 -> [Ct] -- The unsolved simple constraints in the
564 -- implication for the hole.
565 -> Ct -- The hole constraint itself
566 -> TcM (TidyEnv, SDoc)
567 findValidHoleFits tidy_env implics simples ct | isExprHoleCt ct =
568 do { rdr_env <- getGlobalRdrEnv
569 ; lclBinds <- getLocalBindings tidy_env ct
570 ; maxVSubs <- maxValidHoleFits <$> getDynFlags
571 ; hfdc <- getHoleFitDispConfig
572 ; sortingAlg <- getSortingAlg
573 ; refLevel <- refLevelHoleFits <$> getDynFlags
574 ; traceTc "findingValidHoleFitsFor { " $ ppr ct
575 ; traceTc "hole_lvl is:" $ ppr hole_lvl
576 ; traceTc "implics are: " $ ppr implics
577 ; traceTc "simples are: " $ ppr simples
578 ; traceTc "locals are: " $ ppr lclBinds
579 ; let (lcl, gbl) = partition gre_lcl (globalRdrEnvElts rdr_env)
580 -- We remove binding shadowings here, but only for the local level.
581 -- this is so we e.g. suggest the global fmap from the Functor class
582 -- even though there is a local definition as well, such as in the
583 -- Free monad example.
584 locals = removeBindingShadowing $ map Left lclBinds ++ map Right lcl
585 globals = map Right gbl
586 to_check = locals ++ globals
587 ; (searchDiscards, subs) <-
588 findSubs sortingAlg maxVSubs to_check (hole_ty, [])
589 ; (tidy_env, tidy_subs) <- zonkSubs tidy_env subs
590 ; tidy_sorted_subs <- sortFits sortingAlg tidy_subs
591 ; let (pVDisc, limited_subs) = possiblyDiscard maxVSubs tidy_sorted_subs
592 vDiscards = pVDisc || searchDiscards
593 ; subs_with_docs <- addDocs limited_subs
594 ; let vMsg = ppUnless (null subs_with_docs) $
595 hang (text "Valid hole fits include") 2 $
596 vcat (map (pprHoleFit hfdc) subs_with_docs)
597 $$ ppWhen vDiscards subsDiscardMsg
598 -- Refinement hole fits. See Note [Valid refinement hole fits include ...]
599 ; (tidy_env, refMsg) <- if refLevel >= Just 0 then
600 do { maxRSubs <- maxRefHoleFits <$> getDynFlags
601 -- We can use from just, since we know that Nothing >= _ is False.
602 ; let refLvls = [1..(fromJust refLevel)]
603 -- We make a new refinement type for each level of refinement, where
604 -- the level of refinement indicates number of additional arguments
605 -- to allow.
606 ; ref_tys <- mapM mkRefTy refLvls
607 ; traceTc "ref_tys are" $ ppr ref_tys
608 ; refDs <- mapM (findSubs sortingAlg maxRSubs to_check) ref_tys
609 ; (tidy_env, tidy_rsubs) <- zonkSubs tidy_env $ concatMap snd refDs
610 ; tidy_sorted_rsubs <- sortFits sortingAlg tidy_rsubs
611 -- For refinement substitutions we want matches
612 -- like id (_ :: t), head (_ :: [t]), asTypeOf (_ :: t),
613 -- and others in that vein to appear last, since these are
614 -- unlikely to be the most relevant fits.
615 ; (tidy_env, tidy_hole_ty) <- zonkTidyTcType tidy_env hole_ty
616 ; let hasExactApp = any (tcEqType tidy_hole_ty) . hfWrap
617 (exact, not_exact) = partition hasExactApp tidy_sorted_rsubs
618 (pRDisc, exact_last_rfits) =
619 possiblyDiscard maxRSubs $ not_exact ++ exact
620 rDiscards = pRDisc || any fst refDs
621 ; rsubs_with_docs <- addDocs exact_last_rfits
622 ; return (tidy_env,
623 ppUnless (null rsubs_with_docs) $
624 hang (text "Valid refinement hole fits include") 2 $
625 vcat (map (pprHoleFit hfdc) rsubs_with_docs)
626 $$ ppWhen rDiscards refSubsDiscardMsg) }
627 else return (tidy_env, empty)
628 ; traceTc "findingValidHoleFitsFor }" empty
629 ; return (tidy_env, vMsg $$ refMsg) }
630 where
631 -- We extract the type, the tcLevel and the types free variables
632 -- from from the constraint.
633 hole_ty :: TcPredType
634 hole_ty = ctPred ct
635 hole_fvs = tyCoFVsOfType hole_ty
636 hole_lvl = ctLocLevel $ ctEvLoc $ ctEvidence ct
637
638 -- We make a refinement type by adding a new type variable in front
639 -- of the type of t h hole, going from e.g. [Integer] -> Integer
640 -- to t_a1/m[tau:1] -> [Integer] -> Integer. This allows the simplifier
641 -- to unify the new type variable with any type, allowing us
642 -- to suggest a "refinement hole fit", like `(foldl1 _)` instead
643 -- of only concrete hole fits like `sum`.
644 mkRefTy :: Int -> TcM (TcType, [TcTyVar])
645 mkRefTy refLvl = (wrapWithVars &&& id) <$> newTyVars
646 where newTyVars = replicateM refLvl $ setLvl <$>
647 (newOpenTypeKind >>= newFlexiTyVar)
648 setLvl = flip setMetaTyVarTcLevel hole_lvl
649 wrapWithVars vars = mkFunTys (map mkTyVarTy vars) hole_ty
650
651 sortFits :: SortingAlg -- How we should sort the hole fits
652 -> [HoleFit] -- The subs to sort
653 -> TcM [HoleFit]
654 sortFits NoSorting subs = return subs
655 sortFits BySize subs
656 = (++) <$> sortBySize (sort lclFits)
657 <*> sortBySize (sort gblFits)
658 where (lclFits, gblFits) = span hfIsLcl subs
659
660 -- To sort by subsumption, we invoke the sortByGraph function, which
661 -- builds the subsumption graph for the fits and then sorts them using a
662 -- graph sort. Since we want locals to come first anyway, we can sort
663 -- them separately. The substitutions are already checked in local then
664 -- global order, so we can get away with using span here.
665 -- We use (<*>) to expose the parallelism, in case it becomes useful later.
666 sortFits BySubsumption subs
667 = (++) <$> sortByGraph (sort lclFits)
668 <*> sortByGraph (sort gblFits)
669 where (lclFits, gblFits) = span hfIsLcl subs
670
671
672 -- See Note [Relevant Constraints]
673 relevantCts :: [Ct]
674 relevantCts = if isEmptyVarSet (fvVarSet hole_fvs) then []
675 else filter isRelevant simples
676 where ctFreeVarSet :: Ct -> VarSet
677 ctFreeVarSet = fvVarSet . tyCoFVsOfType . ctPred
678 hole_fv_set = fvVarSet hole_fvs
679 anyFVMentioned :: Ct -> Bool
680 anyFVMentioned ct = not $ isEmptyVarSet $
681 ctFreeVarSet ct `intersectVarSet` hole_fv_set
682 -- We filter out those constraints that have no variables (since
683 -- they won't be solved by finding a type for the type variable
684 -- representing the hole) and also other holes, since we're not
685 -- trying to find hole fits for many holes at once.
686 isRelevant ct = not (isEmptyVarSet (ctFreeVarSet ct))
687 && anyFVMentioned ct
688 && not (isHoleCt ct)
689
690 unfoldWrapper :: HsWrapper -> [Type]
691 unfoldWrapper = reverse . unfWrp'
692 where unfWrp' (WpTyApp ty) = [ty]
693 unfWrp' (WpCompose w1 w2) = unfWrp' w1 ++ unfWrp' w2
694 unfWrp' _ = []
695
696
697 -- We only clone flexi type variables, and we need to be able to check
698 -- whether a variable is filled or not.
699 isFlexiTyVar :: TcTyVar -> TcM Bool
700 isFlexiTyVar tv | isMetaTyVar tv = isFlexi <$> readMetaTyVar tv
701 isFlexiTyVar _ = return False
702
703 -- Takes a list of free variables and restores any Flexi type variables
704 -- in free_vars after the action is run.
705 withoutUnification :: FV -> TcM a -> TcM a
706 withoutUnification free_vars action
707 = do { flexis <- filterM isFlexiTyVar fuvs
708 ; result <- action
709 -- Reset any mutated free variables
710 ; mapM_ restore flexis
711 ; return result }
712 where restore = flip writeTcRef Flexi . metaTyVarRef
713 fuvs = fvVarList free_vars
714
715 -- The real work happens here, where we invoke the type checker using
716 -- tcCheckHoleFit to see whether the given type fits the hole.
717 fitsHole :: (TcType, [TcTyVar]) -- The type of the hole wrapped with the
718 -- refinement variables created to simulate
719 -- additional holes (if any), and the list
720 -- of those variables (possibly empty).
721 -- As an example: If the actual type of the
722 -- hole (as specified by the hole
723 -- constraint CHoleExpr passed to
724 -- findValidHoleFits) is t and we want to
725 -- simulate N additional holes, h_ty will
726 -- be r_1 -> ... -> r_N -> t, and
727 -- ref_vars will be [r_1, ... , r_N].
728 -- In the base case with no additional
729 -- holes, h_ty will just be t and ref_vars
730 -- will be [].
731 -> TcType -- The type we're checking to whether it can be
732 -- instantiated to the type h_ty.
733 -> TcM (Maybe ([TcType], [TcType])) -- If it is not a match, we
734 -- return Nothing. Otherwise,
735 -- we Just return the list of
736 -- types that quantified type
737 -- variables in ty would take
738 -- if used in place of h_ty,
739 -- and the list types of any
740 -- additional holes simulated
741 -- with the refinement
742 -- variables in ref_vars.
743 fitsHole (h_ty, ref_vars) ty =
744 -- We wrap this with the withoutUnification to avoid having side-effects
745 -- beyond the check, but we rely on the side-effects when looking for
746 -- refinement hole fits, so we can't wrap the side-effects deeper than this.
747 withoutUnification fvs $
748 do { traceTc "checkingFitOf {" $ ppr ty
749 ; (fits, wrp) <- tcCheckHoleFit (listToBag relevantCts) implics h_ty ty
750 ; traceTc "Did it fit?" $ ppr fits
751 ; traceTc "wrap is: " $ ppr wrp
752 ; traceTc "checkingFitOf }" empty
753 ; z_wrp_tys <- zonkTcTypes (unfoldWrapper wrp)
754 -- We'd like to avoid refinement suggestions like `id _ _` or
755 -- `head _ _`, and only suggest refinements where our all phantom
756 -- variables got unified during the checking. This can be disabled
757 -- with the `-fabstract-refinement-hole-fits` flag.
758 -- Here we do the additional handling when there are refinement
759 -- variables, i.e. zonk them to read their final value to check for
760 -- abstract refinements, and to report what the type of the simulated
761 -- holes must be for this to be a match.
762 ; if fits
763 then if null ref_vars
764 then return (Just (z_wrp_tys, []))
765 else do { let -- To be concrete matches, matches have to
766 -- be more than just an invented type variable.
767 fvSet = fvVarSet fvs
768 notAbstract :: TcType -> Bool
769 notAbstract t = case getTyVar_maybe t of
770 Just tv -> tv `elemVarSet` fvSet
771 _ -> True
772 allConcrete = all notAbstract z_wrp_tys
773 ; z_vars <- zonkTcTyVars ref_vars
774 ; let z_mtvs = mapMaybe tcGetTyVar_maybe z_vars
775 ; allFilled <- not <$> anyM isFlexiTyVar z_mtvs
776 ; allowAbstract <- goptM Opt_AbstractRefHoleFits
777 ; if allowAbstract || (allFilled && allConcrete )
778 then return $ Just (z_wrp_tys, z_vars)
779 else return Nothing }
780 else return Nothing }
781 where fvs = mkFVs ref_vars `unionFV` hole_fvs `unionFV` tyCoFVsOfType ty
782
783 -- We zonk the hole fits so that the output aligns with the rest
784 -- of the typed hole error message output.
785 zonkSubs :: TidyEnv -> [HoleFit] -> TcM (TidyEnv, [HoleFit])
786 zonkSubs = zonkSubs' []
787 where zonkSubs' zs env [] = return (env, reverse zs)
788 zonkSubs' zs env (hf:hfs) = do { (env', z) <- zonkSub env hf
789 ; zonkSubs' (z:zs) env' hfs }
790 zonkSub env hf@HoleFit{hfType = ty, hfMatches = m, hfWrap = wrp}
791 = do { (env, ty') <- zonkTidyTcType env ty
792 ; (env, m') <- zonkTidyTcTypes env m
793 ; (env, wrp') <- zonkTidyTcTypes env wrp
794 ; let zFit = hf {hfType = ty', hfMatches = m', hfWrap = wrp'}
795 ; return (env, zFit ) }
796
797 -- Based on the flags, we might possibly discard some or all the
798 -- fits we've found.
799 possiblyDiscard :: Maybe Int -> [HoleFit] -> (Bool, [HoleFit])
800 possiblyDiscard (Just max) fits = (fits `lengthExceeds` max, take max fits)
801 possiblyDiscard Nothing fits = (False, fits)
802
803
804 -- Sort by size uses as a measure for relevance the sizes of the
805 -- different types needed to instantiate the fit to the type of the hole.
806 -- This is much quicker than sorting by subsumption, and gives reasonable
807 -- results in most cases.
808 sortBySize :: [HoleFit] -> TcM [HoleFit]
809 sortBySize = return . sortOn sizeOfFit
810 where sizeOfFit :: HoleFit -> TypeSize
811 sizeOfFit = sizeTypes . nubBy tcEqType . hfWrap
812
813 -- Based on a suggestion by phadej on #ghc, we can sort the found fits
814 -- by constructing a subsumption graph, and then do a topological sort of
815 -- the graph. This makes the most specific types appear first, which are
816 -- probably those most relevant. This takes a lot of work (but results in
817 -- much more useful output), and can be disabled by
818 -- '-fno-sort-valid-hole-fits'.
819 sortByGraph :: [HoleFit] -> TcM [HoleFit]
820 sortByGraph fits = go [] fits
821 where tcSubsumesWCloning :: TcType -> TcType -> TcM Bool
822 tcSubsumesWCloning ht ty = withoutUnification fvs (tcSubsumes ht ty)
823 where fvs = tyCoFVsOfTypes [ht,ty]
824 go :: [(HoleFit, [HoleFit])] -> [HoleFit] -> TcM [HoleFit]
825 go sofar [] = do { traceTc "subsumptionGraph was" $ ppr sofar
826 ; return $ uncurry (++)
827 $ partition hfIsLcl topSorted }
828 where toV (hf, adjs) = (hf, hfId hf, map hfId adjs)
829 (graph, fromV, _) = graphFromEdges $ map toV sofar
830 topSorted = map ((\(h,_,_) -> h) . fromV) $ topSort graph
831 go sofar (hf:hfs) =
832 do { adjs <-
833 filterM (tcSubsumesWCloning (hfType hf) . hfType) fits
834 ; go ((hf, adjs):sofar) hfs }
835
836 findSubs :: SortingAlg -- Whether we should sort the subs or not
837 -> Maybe Int -- How many we should output, if limited
838 -> [Either Id GlobalRdrElt] -- The elements to check whether fit
839 -> (TcType, [TcTyVar]) -- The type to check for fits and refinement
840 -- variables for emulating additional holes
841 -> TcM (Bool, [HoleFit]) -- We return whether or not we stopped due
842 -- to running out of gas and the fits we
843 -- found.
844 -- We don't check if no output is desired.
845 findSubs _ (Just 0) _ _ = return (False, [])
846 findSubs sortAlg maxSubs to_check ht@(hole_ty, _) =
847 do { traceTc "checkingFitsFor {" $ ppr hole_ty
848 -- If we're not going to sort anyway, we can stop going after
849 -- having found `maxSubs` hole fits.
850 ; let limit = if sortAlg > NoSorting then Nothing else maxSubs
851 ; (discards, subs) <- go [] emptyVarSet limit ht to_check
852 ; traceTc "checkingFitsFor }" empty
853 ; return (discards, subs) }
854 where
855 -- Kickoff the checking of the elements.
856 -- We iterate over the elements, checking each one in turn for whether
857 -- it fits, and adding it to the results if it does.
858 go :: [HoleFit] -- What we've found so far.
859 -> VarSet -- Ids we've already checked
860 -> Maybe Int -- How many we're allowed to find, if limited
861 -> (TcType, [TcTyVar]) -- The type, and its refinement variables.
862 -> [Either Id GlobalRdrElt] -- The elements we've yet to check.
863 -> TcM (Bool, [HoleFit])
864 go subs _ _ _ [] = return (False, reverse subs)
865 go subs _ (Just 0) _ _ = return (True, reverse subs)
866 go subs seen maxleft ty (el:elts) =
867 -- See Note [Leaking errors]
868 tryTcDiscardingErrs discard_it $
869 do { traceTc "lookingUp" $ ppr el
870 ; maybeThing <- lookup el
871 ; case maybeThing of
872 Just id | not_trivial id ->
873 do { fits <- fitsHole ty (idType id)
874 ; case fits of
875 Just (wrp, matches) -> keep_it id wrp matches
876 _ -> discard_it }
877 _ -> discard_it }
878 where discard_it = go subs seen maxleft ty elts
879 keep_it id wrp ms = go (fit:subs) (extendVarSet seen id)
880 ((\n -> n - 1) <$> maxleft) ty elts
881 where fit = HoleFit { hfElem = mbel, hfId = id
882 , hfType = idType id
883 , hfRefLvl = length (snd ty)
884 , hfWrap = wrp, hfMatches = ms
885 , hfDoc = Nothing }
886 mbel = either (const Nothing) Just el
887 -- We want to filter out undefined and the likes from GHC.Err
888 not_trivial id = nameModule_maybe (idName id) /= Just gHC_ERR
889 lookup :: Either Id GlobalRdrElt -> TcM (Maybe Id)
890 lookup (Left id) = return $ Just id
891 lookup (Right el) =
892 do { thing <- tcLookup (gre_name el)
893 ; case thing of
894 ATcId {tct_id = id} -> return $ Just id
895 AGlobal (AnId id) -> return $ Just id
896 AGlobal (AConLike (RealDataCon con)) ->
897 return $ Just (dataConWrapId con)
898 _ -> return Nothing }
899
900
901 -- We don't (as of yet) handle holes in types, only in expressions.
902 findValidHoleFits env _ _ _ = return (env, empty)
903
904 subsDiscardMsg :: SDoc
905 subsDiscardMsg =
906 text "(Some hole fits suppressed;" <+>
907 text "use -fmax-valid-hole-fits=N" <+>
908 text "or -fno-max-valid-hole-fits)"
909
910 refSubsDiscardMsg :: SDoc
911 refSubsDiscardMsg =
912 text "(Some refinement hole fits suppressed;" <+>
913 text "use -fmax-refinement-hole-fits=N" <+>
914 text "or -fno-max-refinement-hole-fits)"
915
916
917 -- | Reports whether first type (ty_a) subsumes the second type (ty_b),
918 -- discarding any errors. Subsumption here means that the ty_b can fit into the
919 -- ty_a, i.e. `tcSubsumes a b == True` if b is a subtype of a.
920 tcSubsumes :: TcSigmaType -> TcSigmaType -> TcM Bool
921 tcSubsumes ty_a ty_b = fst <$> tcCheckHoleFit emptyBag [] ty_a ty_b
922
923
924 -- | A tcSubsumes which takes into account relevant constraints, to fix trac
925 -- #14273. This makes sure that when checking whether a type fits the hole,
926 -- the type has to be subsumed by type of the hole as well as fulfill all
927 -- constraints on the type of the hole.
928 -- Note: The simplifier may perform unification, so make sure to restore any
929 -- free type variables to avoid side-effects.
930 tcCheckHoleFit :: Cts -- Any relevant Cts to the hole.
931 -> [Implication] -- The nested implications of the hole
932 -- with the innermost implication first
933 -> TcSigmaType -- The type of the hole.
934 -> TcSigmaType -- The type to check whether fits.
935 -> TcM (Bool, HsWrapper)
936 tcCheckHoleFit _ _ hole_ty ty | hole_ty `eqType` ty
937 = return (True, idHsWrapper)
938 tcCheckHoleFit relevantCts implics hole_ty ty = discardErrs $
939 do { -- We wrap the subtype constraint in the implications to pass along the
940 -- givens, and so we must ensure that any nested implications and skolems
941 -- end up with the correct level. The implications are ordered so that
942 -- the innermost (the one with the highest level) is first, so it
943 -- suffices to get the level of the first one (or the current level, if
944 -- there are no implications involved).
945 innermost_lvl <- case implics of
946 [] -> getTcLevel
947 -- imp is the innermost implication
948 (imp:_) -> return (ic_tclvl imp)
949 ; (wrp, wanted) <- setTcLevel innermost_lvl $ captureConstraints $
950 tcSubType_NC ExprSigCtxt ty hole_ty
951 ; traceTc "Checking hole fit {" empty
952 ; traceTc "wanteds are: " $ ppr wanted
953 ; if isEmptyWC wanted && isEmptyBag relevantCts
954 then traceTc "}" empty >> return (True, wrp)
955 else do { fresh_binds <- newTcEvBinds
956 -- The relevant constraints may contain HoleDests, so we must
957 -- take care to clone them as well (to avoid #15370).
958 ; cloned_relevants <- mapBagM cloneWanted relevantCts
959 -- We wrap the WC in the nested implications, see
960 -- Note [Nested Implications]
961 ; let outermost_first = reverse implics
962 setWC = setWCAndBinds fresh_binds
963 -- We add the cloned relevants to the wanteds generated by
964 -- the call to tcSubType_NC, see Note [Relevant Constraints]
965 -- There's no need to clone the wanteds, because they are
966 -- freshly generated by `tcSubtype_NC`.
967 w_rel_cts = addSimples wanted cloned_relevants
968 w_givens = foldr setWC w_rel_cts outermost_first
969 ; traceTc "w_givens are: " $ ppr w_givens
970 ; rem <- runTcSDeriveds $ simpl_top w_givens
971 -- We don't want any insoluble or simple constraints left, but
972 -- solved implications are ok (and neccessary for e.g. undefined)
973 ; traceTc "rems was:" $ ppr rem
974 ; traceTc "}" empty
975 ; return (isSolvedWC rem, wrp) } }
976 where
977 setWCAndBinds :: EvBindsVar -- Fresh ev binds var.
978 -> Implication -- The implication to put WC in.
979 -> WantedConstraints -- The WC constraints to put implic.
980 -> WantedConstraints -- The new constraints.
981 setWCAndBinds binds imp wc
982 = WC { wc_simple = emptyBag
983 , wc_impl = unitBag $ imp { ic_wanted = wc , ic_binds = binds } }