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