never executed always true always false
1
2
3 module GHC.Tc.Solver(
4 InferMode(..), simplifyInfer, findInferredDiff,
5 growThetaTyVars,
6 simplifyAmbiguityCheck,
7 simplifyDefault,
8 simplifyTop, simplifyTopImplic,
9 simplifyInteractive,
10 solveEqualities,
11 pushLevelAndSolveEqualities, pushLevelAndSolveEqualitiesX,
12 reportUnsolvedEqualities,
13 simplifyWantedsTcM,
14 tcCheckGivens,
15 tcCheckWanteds,
16 tcNormalise,
17
18 captureTopConstraints,
19
20 simplifyTopWanteds,
21
22 promoteTyVarSet, simplifyAndEmitFlatConstraints,
23
24 -- For Rules we need these
25 solveWanteds, solveWantedsAndDrop,
26 approximateWC, runTcSDeriveds,
27
28 -- We need this for valid hole-fits
29 runTcSDerivedsEarlyAbort
30
31 ) where
32
33 import GHC.Prelude
34
35 import GHC.Data.Bag
36 import GHC.Core.Class ( Class, classKey, classTyCon )
37 import GHC.Driver.Session
38 import GHC.Tc.Utils.Instantiate
39 import GHC.Data.List.SetOps
40 import GHC.Types.Name
41 import GHC.Types.Id( idType )
42 import GHC.Utils.Outputable
43 import GHC.Builtin.Utils
44 import GHC.Builtin.Names
45 import GHC.Tc.Errors
46 import GHC.Tc.Errors.Types
47 import GHC.Tc.Types.Evidence
48 import GHC.Tc.Solver.Interact
49 import GHC.Tc.Solver.Canonical ( makeSuperClasses, solveCallStack )
50 import GHC.Tc.Solver.Rewrite ( rewriteType )
51 import GHC.Tc.Utils.Unify ( buildTvImplication )
52 import GHC.Tc.Utils.TcMType as TcM
53 import GHC.Tc.Utils.Monad as TcM
54 import GHC.Tc.Solver.InertSet
55 import GHC.Tc.Solver.Monad as TcS
56 import GHC.Tc.Types.Constraint
57 import GHC.Core.Predicate
58 import GHC.Tc.Types.Origin
59 import GHC.Tc.Utils.TcType
60 import GHC.Core.Type
61 import GHC.Builtin.Types ( liftedRepTy, manyDataConTy, liftedDataConTy )
62 import GHC.Core.Unify ( tcMatchTyKi )
63 import GHC.Utils.Misc
64 import GHC.Utils.Panic
65 import GHC.Types.Var
66 import GHC.Types.Var.Set
67 import GHC.Types.Basic ( IntWithInf, intGtLimit
68 , DefaultKindVars(..), allVarsOfKindDefault )
69 import GHC.Types.Error
70 import qualified GHC.LanguageExtensions as LangExt
71
72 import Control.Monad
73 import Data.Foldable ( toList )
74 import Data.List ( partition )
75 import Data.List.NonEmpty ( NonEmpty(..) )
76
77 {-
78 *********************************************************************************
79 * *
80 * External interface *
81 * *
82 *********************************************************************************
83 -}
84
85 captureTopConstraints :: TcM a -> TcM (a, WantedConstraints)
86 -- (captureTopConstraints m) runs m, and returns the type constraints it
87 -- generates plus the constraints produced by static forms inside.
88 -- If it fails with an exception, it reports any insolubles
89 -- (out of scope variables) before doing so
90 --
91 -- captureTopConstraints is used exclusively by GHC.Tc.Module at the top
92 -- level of a module.
93 --
94 -- Importantly, if captureTopConstraints propagates an exception, it
95 -- reports any insoluble constraints first, lest they be lost
96 -- altogether. This is important, because solveEqualities (maybe
97 -- other things too) throws an exception without adding any error
98 -- messages; it just puts the unsolved constraints back into the
99 -- monad. See GHC.Tc.Utils.Monad Note [Constraints and errors]
100 -- #16376 is an example of what goes wrong if you don't do this.
101 --
102 -- NB: the caller should bring any environments into scope before
103 -- calling this, so that the reportUnsolved has access to the most
104 -- complete GlobalRdrEnv
105 captureTopConstraints thing_inside
106 = do { static_wc_var <- TcM.newTcRef emptyWC ;
107 ; (mb_res, lie) <- TcM.updGblEnv (\env -> env { tcg_static_wc = static_wc_var } ) $
108 TcM.tryCaptureConstraints thing_inside
109 ; stWC <- TcM.readTcRef static_wc_var
110
111 -- See GHC.Tc.Utils.Monad Note [Constraints and errors]
112 -- If the thing_inside threw an exception, but generated some insoluble
113 -- constraints, report the latter before propagating the exception
114 -- Otherwise they will be lost altogether
115 ; case mb_res of
116 Just res -> return (res, lie `andWC` stWC)
117 Nothing -> do { _ <- simplifyTop lie; failM } }
118 -- This call to simplifyTop is the reason
119 -- this function is here instead of GHC.Tc.Utils.Monad
120 -- We call simplifyTop so that it does defaulting
121 -- (esp of runtime-reps) before reporting errors
122
123 simplifyTopImplic :: Bag Implication -> TcM ()
124 simplifyTopImplic implics
125 = do { empty_binds <- simplifyTop (mkImplicWC implics)
126
127 -- Since all the inputs are implications the returned bindings will be empty
128 ; massertPpr (isEmptyBag empty_binds) (ppr empty_binds)
129
130 ; return () }
131
132 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
133 -- Simplify top-level constraints
134 -- Usually these will be implications,
135 -- but when there is nothing to quantify we don't wrap
136 -- in a degenerate implication, so we do that here instead
137 simplifyTop wanteds
138 = do { traceTc "simplifyTop {" $ text "wanted = " <+> ppr wanteds
139 ; ((final_wc, unsafe_ol), binds1) <- runTcS $
140 do { final_wc <- simplifyTopWanteds wanteds
141 ; unsafe_ol <- getSafeOverlapFailures
142 ; return (final_wc, unsafe_ol) }
143 ; traceTc "End simplifyTop }" empty
144
145 ; binds2 <- reportUnsolved final_wc
146
147 ; traceTc "reportUnsolved (unsafe overlapping) {" empty
148 ; unless (isEmptyCts unsafe_ol) $ do {
149 -- grab current error messages and clear, warnAllUnsolved will
150 -- update error messages which we'll grab and then restore saved
151 -- messages.
152 ; errs_var <- getErrsVar
153 ; saved_msg <- TcM.readTcRef errs_var
154 ; TcM.writeTcRef errs_var emptyMessages
155
156 ; warnAllUnsolved $ emptyWC { wc_simple = unsafe_ol }
157
158 ; whyUnsafe <- getWarningMessages <$> TcM.readTcRef errs_var
159 ; TcM.writeTcRef errs_var saved_msg
160 ; recordUnsafeInfer (mkMessages whyUnsafe)
161 }
162 ; traceTc "reportUnsolved (unsafe overlapping) }" empty
163
164 ; return (evBindMapBinds binds1 `unionBags` binds2) }
165
166 pushLevelAndSolveEqualities :: SkolemInfo -> [TcTyVar] -> TcM a -> TcM a
167 -- Push level, and solve all resulting equalities
168 -- If there are any unsolved equalities, report them
169 -- and fail (in the monad)
170 --
171 -- Panics if we solve any non-equality constraints. (In runTCSEqualities
172 -- we use an error thunk for the evidence bindings.)
173 pushLevelAndSolveEqualities skol_info skol_tvs thing_inside
174 = do { (tclvl, wanted, res) <- pushLevelAndSolveEqualitiesX
175 "pushLevelAndSolveEqualities" thing_inside
176 ; reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
177 ; return res }
178
179 pushLevelAndSolveEqualitiesX :: String -> TcM a
180 -> TcM (TcLevel, WantedConstraints, a)
181 -- Push the level, gather equality constraints, and then solve them.
182 -- Returns any remaining unsolved equalities.
183 -- Does not report errors.
184 --
185 -- Panics if we solve any non-equality constraints. (In runTCSEqualities
186 -- we use an error thunk for the evidence bindings.)
187 pushLevelAndSolveEqualitiesX callsite thing_inside
188 = do { traceTc "pushLevelAndSolveEqualitiesX {" (text "Called from" <+> text callsite)
189 ; (tclvl, (wanted, res))
190 <- pushTcLevelM $
191 do { (res, wanted) <- captureConstraints thing_inside
192 ; wanted <- runTcSEqualities (simplifyTopWanteds wanted)
193 ; return (wanted,res) }
194 ; traceTc "pushLevelAndSolveEqualities }" (vcat [ text "Residual:" <+> ppr wanted
195 , text "Level:" <+> ppr tclvl ])
196 ; return (tclvl, wanted, res) }
197
198 -- | Type-check a thing that emits only equality constraints, solving any
199 -- constraints we can and re-emitting constraints that we can't.
200 -- Use this variant only when we'll get another crack at it later
201 -- See Note [Failure in local type signatures]
202 --
203 -- Panics if we solve any non-equality constraints. (In runTCSEqualities
204 -- we use an error thunk for the evidence bindings.)
205 solveEqualities :: String -> TcM a -> TcM a
206 solveEqualities callsite thing_inside
207 = do { traceTc "solveEqualities {" (text "Called from" <+> text callsite)
208 ; (res, wanted) <- captureConstraints thing_inside
209 ; simplifyAndEmitFlatConstraints wanted
210 -- simplifyAndEmitFlatConstraints fails outright unless
211 -- the only unsolved constraints are soluble-looking
212 -- equalities that can float out
213 ; traceTc "solveEqualities }" empty
214 ; return res }
215
216 simplifyAndEmitFlatConstraints :: WantedConstraints -> TcM ()
217 -- See Note [Failure in local type signatures]
218 simplifyAndEmitFlatConstraints wanted
219 = do { -- Solve and zonk to esablish the
220 -- preconditions for floatKindEqualities
221 wanted <- runTcSEqualities (solveWanteds wanted)
222 ; wanted <- TcM.zonkWC wanted
223
224 ; traceTc "emitFlatConstraints {" (ppr wanted)
225 ; case floatKindEqualities wanted of
226 Nothing -> do { traceTc "emitFlatConstraints } failing" (ppr wanted)
227 -- Emit the bad constraints, wrapped in an implication
228 -- See Note [Wrapping failing kind equalities]
229 ; tclvl <- TcM.getTcLevel
230 ; implic <- buildTvImplication UnkSkol [] (pushTcLevel tclvl) wanted
231 -- ^^^^^^ | ^^^^^^^^^^^^^^^^^
232 -- it's OK to use UnkSkol | we must increase the TcLevel,
233 -- because we don't bind | as explained in
234 -- any skolem variables here | Note [Wrapping failing kind equalities]
235 ; emitImplication implic
236 ; failM }
237 Just (simples, holes)
238 -> do { _ <- promoteTyVarSet (tyCoVarsOfCts simples)
239 ; traceTc "emitFlatConstraints }" $
240 vcat [ text "simples:" <+> ppr simples
241 , text "holes: " <+> ppr holes ]
242 ; emitHoles holes -- Holes don't need promotion
243 ; emitSimples simples } }
244
245 floatKindEqualities :: WantedConstraints -> Maybe (Bag Ct, Bag Hole)
246 -- Float out all the constraints from the WantedConstraints,
247 -- Return Nothing if any constraints can't be floated (captured
248 -- by skolems), or if there is an insoluble constraint, or
249 -- IC_Telescope telescope error
250 -- Precondition 1: we have tried to solve the 'wanteds', both so that
251 -- the ic_status field is set, and because solving can make constraints
252 -- more floatable.
253 -- Precondition 2: the 'wanteds' are zonked, since floatKindEqualities
254 -- is not monadic
255 -- See Note [floatKindEqualities vs approximateWC]
256 floatKindEqualities wc = float_wc emptyVarSet wc
257 where
258 float_wc :: TcTyCoVarSet -> WantedConstraints -> Maybe (Bag Ct, Bag Hole)
259 float_wc trapping_tvs (WC { wc_simple = simples
260 , wc_impl = implics
261 , wc_holes = holes })
262 | all is_floatable simples
263 = do { (inner_simples, inner_holes)
264 <- flatMapBagPairM (float_implic trapping_tvs) implics
265 ; return ( simples `unionBags` inner_simples
266 , holes `unionBags` inner_holes) }
267 | otherwise
268 = Nothing
269 where
270 is_floatable ct
271 | insolubleEqCt ct = False
272 | otherwise = tyCoVarsOfCt ct `disjointVarSet` trapping_tvs
273
274 float_implic :: TcTyCoVarSet -> Implication -> Maybe (Bag Ct, Bag Hole)
275 float_implic trapping_tvs (Implic { ic_wanted = wanted, ic_given_eqs = given_eqs
276 , ic_skols = skols, ic_status = status })
277 | isInsolubleStatus status
278 = Nothing -- A short cut /plus/ we must keep track of IC_BadTelescope
279 | otherwise
280 = do { (simples, holes) <- float_wc new_trapping_tvs wanted
281 ; when (not (isEmptyBag simples) && given_eqs == MaybeGivenEqs) $
282 Nothing
283 -- If there are some constraints to float out, but we can't
284 -- because we don't float out past local equalities
285 -- (c.f GHC.Tc.Solver.approximateWC), then fail
286 ; return (simples, holes) }
287 where
288 new_trapping_tvs = trapping_tvs `extendVarSetList` skols
289
290
291 {- Note [Failure in local type signatures]
292 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
293 When kind checking a type signature, we like to fail fast if we can't
294 solve all the kind equality constraints, for two reasons:
295
296 * A kind-bogus type signature may cause a cascade of knock-on
297 errors if we let it pass
298
299 * More seriously, we don't have a convenient term-level place to add
300 deferred bindings for unsolved kind-equality constraints. In
301 earlier GHCs this led to un-filled-in coercion holes, which caused
302 GHC to crash with "fvProv falls into a hole" See #11563, #11520,
303 #11516, #11399
304
305 But what about /local/ type signatures, mentioning in-scope type
306 variables for which there might be 'given' equalities? For these we
307 might not be able to solve all the equalities locally. Here's an
308 example (T15076b):
309
310 class (a ~ b) => C a b
311 data SameKind :: k -> k -> Type where { SK :: SameKind a b }
312
313 bar :: forall (a :: Type) (b :: Type).
314 C a b => Proxy a -> Proxy b -> ()
315 bar _ _ = const () (undefined :: forall (x :: a) (y :: b). SameKind x y)
316
317 Consider the type signature on 'undefined'. It's ill-kinded unless
318 a~b. But the superclass of (C a b) means that indeed (a~b). So all
319 should be well. BUT it's hard to see that when kind-checking the signature
320 for undefined. We want to emit a residual (a~b) constraint, to solve
321 later.
322
323 Another possibility is that we might have something like
324 F alpha ~ [Int]
325 where alpha is bound further out, which might become soluble
326 "later" when we learn more about alpha. So we want to emit
327 those residual constraints.
328
329 BUT it's no good simply wrapping all unsolved constraints from
330 a type signature in an implication constraint to solve later. The
331 problem is that we are going to /use/ that signature, including
332 instantiate it. Say we have
333 f :: forall a. (forall b. blah) -> blah2
334 f x = <body>
335 To typecheck the definition of f, we have to instantiate those
336 foralls. Moreover, any unsolved kind equalities will be coercion
337 holes in the type. If we naively wrap them in an implication like
338 forall a. (co1:k1~k2, forall b. co2:k3~k4)
339 hoping to solve it later, we might end up filling in the holes
340 co1 and co2 with coercions involving 'a' and 'b' -- but by now
341 we've instantiated the type. Chaos!
342
343 Moreover, the unsolved constraints might be skolem-escape things, and
344 if we proceed with f bound to a nonsensical type, we get a cascade of
345 follow-up errors. For example polykinds/T12593, T15577, and many others.
346
347 So here's the plan (see tcHsSigType):
348
349 * pushLevelAndSolveEqualitiesX: try to solve the constraints
350
351 * kindGeneraliseSome: do kind generalisation
352
353 * buildTvImplication: build an implication for the residual, unsolved
354 constraint
355
356 * simplifyAndEmitFlatConstraints: try to float out every unsolved equality
357 inside that implication, in the hope that it constrains only global
358 type variables, not the locally-quantified ones.
359
360 * If we fail, or find an insoluble constraint, emit the implication,
361 so that the errors will be reported, and fail.
362
363 * If we succeed in floating all the equalities, promote them and
364 re-emit them as flat constraint, not wrapped at all (since they
365 don't mention any of the quantified variables.
366
367 * Note that this float-and-promote step means that anonymous
368 wildcards get floated to top level, as we want; see
369 Note [Checking partial type signatures] in GHC.Tc.Gen.HsType.
370
371 All this is done:
372
373 * In GHC.Tc.Gen.HsType.tcHsSigType, as above
374
375 * solveEqualities. Use this when there no kind-generalisation
376 step to complicate matters; then we don't need to push levels,
377 and can solve the equalities immediately without needing to
378 wrap it in an implication constraint. (You'll generally see
379 a kindGeneraliseNone nearby.)
380
381 * In GHC.Tc.TyCl and GHC.Tc.TyCl.Instance; see calls to
382 pushLevelAndSolveEqualitiesX, followed by quantification, and
383 then reportUnsolvedEqualities.
384
385 NB: we call reportUnsolvedEqualities before zonkTcTypeToType
386 because the latter does not expect to see any un-filled-in
387 coercions, which will happen if we have unsolved equalities.
388 By calling reportUnsolvedEqualities first, which fails after
389 reporting errors, we avoid that happening.
390
391 See also #18062, #11506
392
393 Note [Wrapping failing kind equalities]
394 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
395 In simplifyAndEmitFlatConstraints, if we fail to get down to simple
396 flat constraints we will
397 * re-emit the constraints so that they are reported
398 * fail in the monad
399 But there is a Terrible Danger that, if -fdefer-type-errors is on, and
400 we just re-emit an insoluble constraint like (* ~ (*->*)), that we'll
401 report only a warning and proceed with compilation. But if we ever fail
402 in the monad it should be fatal; we should report an error and stop after
403 the type checker. If not, chaos results: #19142.
404
405 Our solution is this:
406 * Even with -fdefer-type-errors, inside an implication with no place for
407 value bindings (ic_binds = CoEvBindsVar), report failing equalities as
408 errors. We have to do this anyway; see GHC.Tc.Errors
409 Note [Failing equalities with no evidence bindings].
410
411 * Right here in simplifyAndEmitFlatConstraints, use buildTvImplication
412 to wrap the failing constraint in a degenerate implication (no
413 skolems, no theta), with ic_binds = CoEvBindsVar. This setting of
414 `ic_binds` means that any failing equalities will lead to an
415 error not a warning, irrespective of -fdefer-type-errors: see
416 Note [Failing equalities with no evidence bindings] in GHC.Tc.Errors,
417 and `maybeSwitchOffDefer` in that module.
418
419 We still take care to bump the TcLevel of the implication. Partly,
420 that ensures that nested implications have increasing level numbers
421 which seems nice. But more specifically, suppose the outer level
422 has a Given `(C ty)`, which has pending (not-yet-expanded)
423 superclasses. Consider what happens when we process this implication
424 constraint (which we have re-emitted) in that context:
425 - in the inner implication we'll call `getPendingGivenScs`,
426 - we /do not/ want to get the `(C ty)` from the outer level,
427 lest we try to add an evidence term for the superclass,
428 which we can't do because we have specifically set
429 `ic_binds` = `CoEvBindsVar`.
430 - as `getPendingGivenSCcs is careful to only get Givens from
431 the /current/ level, and we bumped the `TcLevel` of the implication,
432 we're OK.
433
434 TL;DR: bump the `TcLevel` when creating the nested implication.
435 If we don't we get a panic in `GHC.Tc.Utils.Monad.addTcEvBind` (#20043).
436
437
438 We re-emit the implication rather than reporting the errors right now,
439 so that the error mesages are improved by other solving and defaulting.
440 e.g. we prefer
441 Cannot match 'Type->Type' with 'Type'
442 to Cannot match 'Type->Type' with 'TYPE r0'
443
444
445 Note [floatKindEqualities vs approximateWC]
446 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
447 floatKindEqualities and approximateWC are strikingly similar to each
448 other, but
449
450 * floatKindEqualites tries to float /all/ equalities, and fails if
451 it can't, or if any implication is insoluble.
452 * approximateWC just floats out any constraints
453 (not just equalities) that can float; it never fails.
454 -}
455
456
457 reportUnsolvedEqualities :: SkolemInfo -> [TcTyVar] -> TcLevel
458 -> WantedConstraints -> TcM ()
459 -- Reports all unsolved wanteds provided; fails in the monad if there are any.
460 --
461 -- The provided SkolemInfo and [TcTyVar] arguments are used in an implication to
462 -- provide skolem info for any errors.
463 --
464 reportUnsolvedEqualities skol_info skol_tvs tclvl wanted
465 | isEmptyWC wanted
466 = return ()
467 | otherwise
468 = checkNoErrs $ -- Fail
469 do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted
470 ; reportAllUnsolved (mkImplicWC (unitBag implic)) }
471
472
473 -- | Simplify top-level constraints, but without reporting any unsolved
474 -- constraints nor unsafe overlapping.
475 simplifyTopWanteds :: WantedConstraints -> TcS WantedConstraints
476 -- See Note [Top-level Defaulting Plan]
477 simplifyTopWanteds wanteds
478 = do { wc_first_go <- nestTcS (solveWantedsAndDrop wanteds)
479 -- This is where the main work happens
480 ; dflags <- getDynFlags
481 ; try_tyvar_defaulting dflags wc_first_go }
482 where
483 try_tyvar_defaulting :: DynFlags -> WantedConstraints -> TcS WantedConstraints
484 try_tyvar_defaulting dflags wc
485 | isEmptyWC wc
486 = return wc
487 | insolubleWC wc
488 , gopt Opt_PrintExplicitRuntimeReps dflags -- See Note [Defaulting insolubles]
489 = try_class_defaulting wc
490 | otherwise
491 = do { free_tvs <- TcS.zonkTyCoVarsAndFVList (tyCoVarsOfWCList wc)
492 ; let meta_tvs = filter (isTyVar <&&> isMetaTyVar) free_tvs
493 -- zonkTyCoVarsAndFV: the wc_first_go is not yet zonked
494 -- filter isMetaTyVar: we might have runtime-skolems in GHCi,
495 -- and we definitely don't want to try to assign to those!
496 -- The isTyVar is needed to weed out coercion variables
497
498 ; defaulted <- mapM defaultTyVarTcS meta_tvs -- Has unification side effects
499 ; if or defaulted
500 then do { wc_residual <- nestTcS (solveWanteds wc)
501 -- See Note [Must simplify after defaulting]
502 ; try_class_defaulting wc_residual }
503 else try_class_defaulting wc } -- No defaulting took place
504
505 try_class_defaulting :: WantedConstraints -> TcS WantedConstraints
506 try_class_defaulting wc
507 | isEmptyWC wc || insolubleWC wc -- See Note [Defaulting insolubles]
508 = return wc
509 | otherwise -- See Note [When to do type-class defaulting]
510 = do { something_happened <- applyDefaultingRules wc
511 -- See Note [Top-level Defaulting Plan]
512 ; if something_happened
513 then do { wc_residual <- nestTcS (solveWantedsAndDrop wc)
514 ; try_class_defaulting wc_residual }
515 -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
516 else try_callstack_defaulting wc }
517
518 try_callstack_defaulting :: WantedConstraints -> TcS WantedConstraints
519 try_callstack_defaulting wc
520 | isEmptyWC wc
521 = return wc
522 | otherwise
523 = defaultCallStacks wc
524
525 -- | Default any remaining @CallStack@ constraints to empty @CallStack@s.
526 defaultCallStacks :: WantedConstraints -> TcS WantedConstraints
527 -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
528 defaultCallStacks wanteds
529 = do simples <- handle_simples (wc_simple wanteds)
530 mb_implics <- mapBagM handle_implic (wc_impl wanteds)
531 return (wanteds { wc_simple = simples
532 , wc_impl = catBagMaybes mb_implics })
533
534 where
535
536 handle_simples simples
537 = catBagMaybes <$> mapBagM defaultCallStack simples
538
539 handle_implic :: Implication -> TcS (Maybe Implication)
540 -- The Maybe is because solving the CallStack constraint
541 -- may well allow us to discard the implication entirely
542 handle_implic implic
543 | isSolvedStatus (ic_status implic)
544 = return (Just implic)
545 | otherwise
546 = do { wanteds <- setEvBindsTcS (ic_binds implic) $
547 -- defaultCallStack sets a binding, so
548 -- we must set the correct binding group
549 defaultCallStacks (ic_wanted implic)
550 ; setImplicationStatus (implic { ic_wanted = wanteds }) }
551
552 defaultCallStack ct
553 | ClassPred cls tys <- classifyPredType (ctPred ct)
554 , Just {} <- isCallStackPred cls tys
555 = do { solveCallStack (ctEvidence ct) EvCsEmpty
556 ; return Nothing }
557
558 defaultCallStack ct
559 = return (Just ct)
560
561
562 {- Note [When to do type-class defaulting]
563 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
564 In GHC 7.6 and 7.8.2, we did type-class defaulting only if insolubleWC
565 was false, on the grounds that defaulting can't help solve insoluble
566 constraints. But if we *don't* do defaulting we may report a whole
567 lot of errors that would be solved by defaulting; these errors are
568 quite spurious because fixing the single insoluble error means that
569 defaulting happens again, which makes all the other errors go away.
570 This is jolly confusing: #9033.
571
572 So it seems better to always do type-class defaulting.
573
574 However, always doing defaulting does mean that we'll do it in
575 situations like this (#5934):
576 run :: (forall s. GenST s) -> Int
577 run = fromInteger 0
578 We don't unify the return type of fromInteger with the given function
579 type, because the latter involves foralls. So we're left with
580 (Num alpha, alpha ~ (forall s. GenST s) -> Int)
581 Now we do defaulting, get alpha := Integer, and report that we can't
582 match Integer with (forall s. GenST s) -> Int. That's not totally
583 stupid, but perhaps a little strange.
584
585 Another potential alternative would be to suppress *all* non-insoluble
586 errors if there are *any* insoluble errors, anywhere, but that seems
587 too drastic.
588
589 Note [Must simplify after defaulting]
590 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
591 We may have a deeply buried constraint
592 (t:*) ~ (a:Open)
593 which we couldn't solve because of the kind incompatibility, and 'a' is free.
594 Then when we default 'a' we can solve the constraint. And we want to do
595 that before starting in on type classes. We MUST do it before reporting
596 errors, because it isn't an error! #7967 was due to this.
597
598 Note [Top-level Defaulting Plan]
599 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
600 We have considered two design choices for where/when to apply defaulting.
601 (i) Do it in SimplCheck mode only /whenever/ you try to solve some
602 simple constraints, maybe deep inside the context of implications.
603 This used to be the case in GHC 7.4.1.
604 (ii) Do it in a tight loop at simplifyTop, once all other constraints have
605 finished. This is the current story.
606
607 Option (i) had many disadvantages:
608 a) Firstly, it was deep inside the actual solver.
609 b) Secondly, it was dependent on the context (Infer a type signature,
610 or Check a type signature, or Interactive) since we did not want
611 to always start defaulting when inferring (though there is an exception to
612 this, see Note [Default while Inferring]).
613 c) It plainly did not work. Consider typecheck/should_compile/DfltProb2.hs:
614 f :: Int -> Bool
615 f x = const True (\y -> let w :: a -> a
616 w a = const a (y+1)
617 in w y)
618 We will get an implication constraint (for beta the type of y):
619 [untch=beta] forall a. 0 => Num beta
620 which we really cannot default /while solving/ the implication, since beta is
621 untouchable.
622
623 Instead our new defaulting story is to pull defaulting out of the solver loop and
624 go with option (ii), implemented at SimplifyTop. Namely:
625 - First, have a go at solving the residual constraint of the whole
626 program
627 - Try to approximate it with a simple constraint
628 - Figure out derived defaulting equations for that simple constraint
629 - Go round the loop again if you did manage to get some equations
630
631 Now, that has to do with class defaulting. However there exists type variable /kind/
632 defaulting. Again this is done at the top-level and the plan is:
633 - At the top-level, once you had a go at solving the constraint, do
634 figure out /all/ the touchable unification variables of the wanted constraints.
635 - Apply defaulting to their kinds
636
637 More details in Note [DefaultTyVar].
638
639 Note [Safe Haskell Overlapping Instances]
640 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
641 In Safe Haskell, we apply an extra restriction to overlapping instances. The
642 motive is to prevent untrusted code provided by a third-party, changing the
643 behavior of trusted code through type-classes. This is due to the global and
644 implicit nature of type-classes that can hide the source of the dictionary.
645
646 Another way to state this is: if a module M compiles without importing another
647 module N, changing M to import N shouldn't change the behavior of M.
648
649 Overlapping instances with type-classes can violate this principle. However,
650 overlapping instances aren't always unsafe. They are just unsafe when the most
651 selected dictionary comes from untrusted code (code compiled with -XSafe) and
652 overlaps instances provided by other modules.
653
654 In particular, in Safe Haskell at a call site with overlapping instances, we
655 apply the following rule to determine if it is a 'unsafe' overlap:
656
657 1) Most specific instance, I1, defined in an `-XSafe` compiled module.
658 2) I1 is an orphan instance or a MPTC.
659 3) At least one overlapped instance, Ix, is both:
660 A) from a different module than I1
661 B) Ix is not marked `OVERLAPPABLE`
662
663 This is a slightly involved heuristic, but captures the situation of an
664 imported module N changing the behavior of existing code. For example, if
665 condition (2) isn't violated, then the module author M must depend either on a
666 type-class or type defined in N.
667
668 Secondly, when should these heuristics be enforced? We enforced them when the
669 type-class method call site is in a module marked `-XSafe` or `-XTrustworthy`.
670 This allows `-XUnsafe` modules to operate without restriction, and for Safe
671 Haskell inferrence to infer modules with unsafe overlaps as unsafe.
672
673 One alternative design would be to also consider if an instance was imported as
674 a `safe` import or not and only apply the restriction to instances imported
675 safely. However, since instances are global and can be imported through more
676 than one path, this alternative doesn't work.
677
678 Note [Safe Haskell Overlapping Instances Implementation]
679 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
680
681 How is this implemented? It's complicated! So we'll step through it all:
682
683 1) `InstEnv.lookupInstEnv` -- Performs instance resolution, so this is where
684 we check if a particular type-class method call is safe or unsafe. We do this
685 through the return type, `ClsInstLookupResult`, where the last parameter is a
686 list of instances that are unsafe to overlap. When the method call is safe,
687 the list is null.
688
689 2) `GHC.Tc.Solver.Interact.matchClassInst` -- This module drives the instance resolution
690 / dictionary generation. The return type is `ClsInstResult`, which either
691 says no instance matched, or one found, and if it was a safe or unsafe
692 overlap.
693
694 3) `GHC.Tc.Solver.Interact.doTopReactDict` -- Takes a dictionary / class constraint and
695 tries to resolve it by calling (in part) `matchClassInst`. The resolving
696 mechanism has a work list (of constraints) that it process one at a time. If
697 the constraint can't be resolved, it's added to an inert set. When compiling
698 an `-XSafe` or `-XTrustworthy` module, we follow this approach as we know
699 compilation should fail. These are handled as normal constraint resolution
700 failures from here-on (see step 6).
701
702 Otherwise, we may be inferring safety (or using `-Wunsafe`), and
703 compilation should succeed, but print warnings and/or mark the compiled module
704 as `-XUnsafe`. In this case, we call `insertSafeOverlapFailureTcS` which adds
705 the unsafe (but resolved!) constraint to the `inert_safehask` field of
706 `InertCans`.
707
708 4) `GHC.Tc.Solver.simplifyTop`:
709 * Call simplifyTopWanteds, the top-level function for driving the simplifier for
710 constraint resolution.
711
712 * Once finished, call `getSafeOverlapFailures` to retrieve the
713 list of overlapping instances that were successfully resolved,
714 but unsafe. Remember, this is only applicable for generating warnings
715 (`-Wunsafe`) or inferring a module unsafe. `-XSafe` and `-XTrustworthy`
716 cause compilation failure by not resolving the unsafe constraint at all.
717
718 * For unresolved constraints (all types), call `GHC.Tc.Errors.reportUnsolved`,
719 while for resolved but unsafe overlapping dictionary constraints, call
720 `GHC.Tc.Errors.warnAllUnsolved`. Both functions convert constraints into a
721 warning message for the user.
722
723 * In the case of `warnAllUnsolved` for resolved, but unsafe
724 dictionary constraints, we collect the generated warning
725 message (pop it) and call `GHC.Tc.Utils.Monad.recordUnsafeInfer` to
726 mark the module we are compiling as unsafe, passing the
727 warning message along as the reason.
728
729 5) `GHC.Tc.Errors.*Unsolved` -- Generates error messages for constraints by
730 actually calling `InstEnv.lookupInstEnv` again! Yes, confusing, but all we
731 know is the constraint that is unresolved or unsafe. For dictionary, all we
732 know is that we need a dictionary of type C, but not what instances are
733 available and how they overlap. So we once again call `lookupInstEnv` to
734 figure that out so we can generate a helpful error message.
735
736 6) `GHC.Tc.Utils.Monad.recordUnsafeInfer` -- Save the unsafe result and reason in
737 IORefs called `tcg_safe_infer` and `tcg_safe_infer_reason`.
738
739 7) `GHC.Driver.Main.tcRnModule'` -- Reads `tcg_safe_infer` after type-checking, calling
740 `GHC.Driver.Main.markUnsafeInfer` (passing the reason along) when safe-inferrence
741 failed.
742
743 Note [No defaulting in the ambiguity check]
744 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
745 When simplifying constraints for the ambiguity check, we use
746 solveWantedsAndDrop, not simplifyTopWanteds, so that we do no defaulting.
747 #11947 was an example:
748 f :: Num a => Int -> Int
749 This is ambiguous of course, but we don't want to default the
750 (Num alpha) constraint to (Num Int)! Doing so gives a defaulting
751 warning, but no error.
752
753 Note [Defaulting insolubles]
754 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
755 If a set of wanteds is insoluble, we have no hope of accepting the
756 program. Yet we do not stop constraint solving, etc., because we may
757 simplify the wanteds to produce better error messages. So, once
758 we have an insoluble constraint, everything we do is just about producing
759 helpful error messages.
760
761 Should we default in this case or not? Let's look at an example (tcfail004):
762
763 (f,g) = (1,2,3)
764
765 With defaulting, we get a conflict between (a0,b0) and (Integer,Integer,Integer).
766 Without defaulting, we get a conflict between (a0,b0) and (a1,b1,c1). I (Richard)
767 find the latter more helpful. Several other test cases (e.g. tcfail005) suggest
768 similarly. So: we should not do class defaulting with insolubles.
769
770 On the other hand, RuntimeRep-defaulting is different. Witness tcfail078:
771
772 f :: Integer i => i
773 f = 0
774
775 Without RuntimeRep-defaulting, we GHC suggests that Integer should have kind
776 TYPE r0 -> Constraint and then complains that r0 is actually untouchable
777 (presumably, because it can't be sure if `Integer i` entails an equality).
778 If we default, we are told of a clash between (* -> Constraint) and Constraint.
779 The latter seems far better, suggesting we *should* do RuntimeRep-defaulting
780 even on insolubles.
781
782 But, evidently, not always. Witness UnliftedNewtypesInfinite:
783
784 newtype Foo = FooC (# Int#, Foo #)
785
786 This should fail with an occurs-check error on the kind of Foo (with -XUnliftedNewtypes).
787 If we default RuntimeRep-vars, we get
788
789 Expecting a lifted type, but ‘(# Int#, Foo #)’ is unlifted
790
791 which is just plain wrong.
792
793 Conclusion: we should do RuntimeRep-defaulting on insolubles only when the user does not
794 want to hear about RuntimeRep stuff -- that is, when -fprint-explicit-runtime-reps
795 is not set.
796 -}
797
798 ------------------
799 simplifyAmbiguityCheck :: Type -> WantedConstraints -> TcM ()
800 simplifyAmbiguityCheck ty wanteds
801 = do { traceTc "simplifyAmbiguityCheck {" (text "type = " <+> ppr ty $$ text "wanted = " <+> ppr wanteds)
802 ; (final_wc, _) <- runTcS $ solveWantedsAndDrop wanteds
803 -- NB: no defaulting! See Note [No defaulting in the ambiguity check]
804
805 ; traceTc "End simplifyAmbiguityCheck }" empty
806
807 -- Normally report all errors; but with -XAllowAmbiguousTypes
808 -- report only insoluble ones, since they represent genuinely
809 -- inaccessible code
810 ; allow_ambiguous <- xoptM LangExt.AllowAmbiguousTypes
811 ; traceTc "reportUnsolved(ambig) {" empty
812 ; unless (allow_ambiguous && not (insolubleWC final_wc))
813 (discardResult (reportUnsolved final_wc))
814 ; traceTc "reportUnsolved(ambig) }" empty
815
816 ; return () }
817
818 ------------------
819 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
820 simplifyInteractive wanteds
821 = traceTc "simplifyInteractive" empty >>
822 simplifyTop wanteds
823
824 ------------------
825 simplifyDefault :: ThetaType -- Wanted; has no type variables in it
826 -> TcM Bool -- Return if the constraint is soluble
827 simplifyDefault theta
828 = do { traceTc "simplifyDefault" empty
829 ; wanteds <- newWanteds DefaultOrigin theta
830 ; unsolved <- runTcSDeriveds (solveWantedsAndDrop (mkSimpleWC wanteds))
831 ; return (isEmptyWC unsolved) }
832
833 ------------------
834 {- Note [Pattern match warnings with insoluble Givens]
835 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
836 A pattern match on a GADT can introduce new type-level information, which needs
837 to be analysed in order to get the expected pattern match warnings.
838
839 For example:
840
841 > type IsBool :: Type -> Constraint
842 > type family IsBool a where
843 > IsBool Bool = ()
844 > IsBool b = b ~ Bool
845 >
846 > data T a where
847 > MkTInt :: Int -> T Int
848 > MkTBool :: IsBool b => b -> T b
849 >
850 > f :: T Int -> Int
851 > f (MkTInt i) = i
852
853 The pattern matching performed by `f` is complete: we can't ever call
854 `f (MkTBool b)`, as type-checking that application would require producing
855 evidence for `Int ~ Bool`, which can't be done.
856
857 The pattern match checker uses `tcCheckGivens` to accumulate all the Given
858 constraints, and relies on `tcCheckGivens` to return Nothing if the
859 Givens become insoluble. `tcCheckGivens` in turn relies on `insolubleCt`
860 to identify these insoluble constraints. So the precise definition of
861 `insolubleCt` has a big effect on pattern match overlap warnings.
862
863 To detect this situation, we check whether there are any insoluble Given
864 constraints. In the example above, the insoluble constraint was an
865 equality constraint, but it is also important to detect custom type errors:
866
867 > type NotInt :: Type -> Constraint
868 > type family NotInt a where
869 > NotInt Int = TypeError (Text "That's Int, silly.")
870 > NotInt _ = ()
871 >
872 > data R a where
873 > MkT1 :: a -> R a
874 > MkT2 :: NotInt a => R a
875 >
876 > foo :: R Int -> Int
877 > foo (MkT1 x) = x
878
879 To see that we can't call `foo (MkT2)`, we must detect that `NotInt Int` is insoluble
880 because it is a custom type error.
881 Failing to do so proved quite inconvenient for users, as evidence by the
882 tickets #11503 #14141 #16377 #20180.
883 Test cases: T11503, T14141.
884
885 Examples of constraints that tcCheckGivens considers insoluble:
886 - Int ~ Bool,
887 - Coercible Float Word,
888 - TypeError msg.
889
890 Non-examples:
891 - constraints which we know aren't satisfied,
892 e.g. Show (Int -> Int) when no such instance is in scope,
893 - Eq (TypeError msg),
894 - C (Int ~ Bool), with @class C (c :: Constraint)@.
895 -}
896
897 tcCheckGivens :: InertSet -> Bag EvVar -> TcM (Maybe InertSet)
898 -- ^ Return (Just new_inerts) if the Givens are satisfiable, Nothing if definitely
899 -- contradictory.
900 --
901 -- See Note [Pattern match warnings with insoluble Givens] above.
902 tcCheckGivens inerts given_ids = do
903 (sat, new_inerts) <- runTcSInerts inerts $ do
904 traceTcS "checkGivens {" (ppr inerts <+> ppr given_ids)
905 lcl_env <- TcS.getLclEnv
906 let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
907 let given_cts = mkGivens given_loc (bagToList given_ids)
908 -- See Note [Superclasses and satisfiability]
909 solveSimpleGivens given_cts
910 insols <- getInertInsols
911 insols <- try_harder insols
912 traceTcS "checkGivens }" (ppr insols)
913 return (isEmptyBag insols)
914 return $ if sat then Just new_inerts else Nothing
915 where
916 try_harder :: Cts -> TcS Cts
917 -- Maybe we have to search up the superclass chain to find
918 -- an unsatisfiable constraint. Example: pmcheck/T3927b.
919 -- At the moment we try just once
920 try_harder insols
921 | not (isEmptyBag insols) -- We've found that it's definitely unsatisfiable
922 = return insols -- Hurrah -- stop now.
923 | otherwise
924 = do { pending_given <- getPendingGivenScs
925 ; new_given <- makeSuperClasses pending_given
926 ; solveSimpleGivens new_given
927 ; getInertInsols }
928
929 tcCheckWanteds :: InertSet -> ThetaType -> TcM Bool
930 -- ^ Return True if the Wanteds are soluble, False if not
931 tcCheckWanteds inerts wanteds = do
932 cts <- newWanteds PatCheckOrigin wanteds
933 (sat, _new_inerts) <- runTcSInerts inerts $ do
934 traceTcS "checkWanteds {" (ppr inerts <+> ppr wanteds)
935 -- See Note [Superclasses and satisfiability]
936 wcs <- solveWantedsAndDrop (mkSimpleWC cts)
937 traceTcS "checkWanteds }" (ppr wcs)
938 return (isSolvedWC wcs)
939 return sat
940
941 -- | Normalise a type as much as possible using the given constraints.
942 -- See @Note [tcNormalise]@.
943 tcNormalise :: InertSet -> Type -> TcM Type
944 tcNormalise inerts ty
945 = do { norm_loc <- getCtLocM PatCheckOrigin Nothing
946 ; (res, _new_inerts) <- runTcSInerts inerts $
947 do { traceTcS "tcNormalise {" (ppr inerts)
948 ; ty' <- rewriteType norm_loc ty
949 ; traceTcS "tcNormalise }" (ppr ty')
950 ; pure ty' }
951 ; return res }
952
953 {- Note [Superclasses and satisfiability]
954 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
955 Expand superclasses before starting, because (Int ~ Bool), has
956 (Int ~~ Bool) as a superclass, which in turn has (Int ~N# Bool)
957 as a superclass, and it's the latter that is insoluble. See
958 Note [The equality types story] in GHC.Builtin.Types.Prim.
959
960 If we fail to prove unsatisfiability we (arbitrarily) try just once to
961 find superclasses, using try_harder. Reason: we might have a type
962 signature
963 f :: F op (Implements push) => ..
964 where F is a type function. This happened in #3972.
965
966 We could do more than once but we'd have to have /some/ limit: in the
967 the recursive case, we would go on forever in the common case where
968 the constraints /are/ satisfiable (#10592 comment:12!).
969
970 For stratightforard situations without type functions the try_harder
971 step does nothing.
972
973 Note [tcNormalise]
974 ~~~~~~~~~~~~~~~~~~
975 tcNormalise is a rather atypical entrypoint to the constraint solver. Whereas
976 most invocations of the constraint solver are intended to simplify a set of
977 constraints or to decide if a particular set of constraints is satisfiable,
978 the purpose of tcNormalise is to take a type, plus some locally solved
979 constraints in the form of an InertSet, and normalise the type as much as
980 possible with respect to those constraints.
981
982 It does *not* reduce type or data family applications or look through newtypes.
983
984 Why is this useful? As one example, when coverage-checking an EmptyCase
985 expression, it's possible that the type of the scrutinee will only reduce
986 if some local equalities are solved for. See "Wrinkle: Local equalities"
987 in Note [Type normalisation] in "GHC.HsToCore.Pmc".
988
989 To accomplish its stated goal, tcNormalise first initialises the solver monad
990 with the given InertCans, then uses rewriteType to simplify the desired type
991 with respect to the Givens in the InertCans.
992
993 ***********************************************************************************
994 * *
995 * Inference
996 * *
997 ***********************************************************************************
998
999 Note [Inferring the type of a let-bound variable]
1000 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1001 Consider
1002 f x = rhs
1003
1004 To infer f's type we do the following:
1005 * Gather the constraints for the RHS with ambient level *one more than*
1006 the current one. This is done by the call
1007 pushLevelAndCaptureConstraints (tcMonoBinds...)
1008 in GHC.Tc.Gen.Bind.tcPolyInfer
1009
1010 * Call simplifyInfer to simplify the constraints and decide what to
1011 quantify over. We pass in the level used for the RHS constraints,
1012 here called rhs_tclvl.
1013
1014 This ensures that the implication constraint we generate, if any,
1015 has a strictly-increased level compared to the ambient level outside
1016 the let binding.
1017
1018 -}
1019
1020 -- | How should we choose which constraints to quantify over?
1021 data InferMode = ApplyMR -- ^ Apply the monomorphism restriction,
1022 -- never quantifying over any constraints
1023 | EagerDefaulting -- ^ See Note [TcRnExprMode] in "GHC.Tc.Module",
1024 -- the :type +d case; this mode refuses
1025 -- to quantify over any defaultable constraint
1026 | NoRestrictions -- ^ Quantify over any constraint that
1027 -- satisfies 'GHC.Tc.Utils.TcType.pickQuantifiablePreds'
1028
1029 instance Outputable InferMode where
1030 ppr ApplyMR = text "ApplyMR"
1031 ppr EagerDefaulting = text "EagerDefaulting"
1032 ppr NoRestrictions = text "NoRestrictions"
1033
1034 simplifyInfer :: TcLevel -- Used when generating the constraints
1035 -> InferMode
1036 -> [TcIdSigInst] -- Any signatures (possibly partial)
1037 -> [(Name, TcTauType)] -- Variables to be generalised,
1038 -- and their tau-types
1039 -> WantedConstraints
1040 -> TcM ([TcTyVar], -- Quantify over these type variables
1041 [EvVar], -- ... and these constraints (fully zonked)
1042 TcEvBinds, -- ... binding these evidence variables
1043 Bool) -- True <=> the residual constraints are insoluble
1044
1045 simplifyInfer rhs_tclvl infer_mode sigs name_taus wanteds
1046 | isEmptyWC wanteds
1047 = do { -- When quantifying, we want to preserve any order of variables as they
1048 -- appear in partial signatures. cf. decideQuantifiedTyVars
1049 let psig_tv_tys = [ mkTyVarTy tv | sig <- partial_sigs
1050 , (_,Bndr tv _) <- sig_inst_skols sig ]
1051 psig_theta = [ pred | sig <- partial_sigs
1052 , pred <- sig_inst_theta sig ]
1053
1054 ; dep_vars <- candidateQTyVarsOfTypes (psig_tv_tys ++ psig_theta ++ map snd name_taus)
1055 ; qtkvs <- quantifyTyVars allVarsOfKindDefault dep_vars
1056 ; traceTc "simplifyInfer: empty WC" (ppr name_taus $$ ppr qtkvs)
1057 ; return (qtkvs, [], emptyTcEvBinds, False) }
1058
1059 | otherwise
1060 = do { traceTc "simplifyInfer {" $ vcat
1061 [ text "sigs =" <+> ppr sigs
1062 , text "binds =" <+> ppr name_taus
1063 , text "rhs_tclvl =" <+> ppr rhs_tclvl
1064 , text "infer_mode =" <+> ppr infer_mode
1065 , text "(unzonked) wanted =" <+> ppr wanteds
1066 ]
1067
1068 ; let psig_theta = concatMap sig_inst_theta partial_sigs
1069
1070 -- First do full-blown solving
1071 -- NB: we must gather up all the bindings from doing
1072 -- this solving; hence (runTcSWithEvBinds ev_binds_var).
1073 -- And note that since there are nested implications,
1074 -- calling solveWanteds will side-effect their evidence
1075 -- bindings, so we can't just revert to the input
1076 -- constraint.
1077
1078 ; ev_binds_var <- TcM.newTcEvBinds
1079 ; psig_evs <- newWanteds AnnOrigin psig_theta
1080 ; wanted_transformed_incl_derivs
1081 <- setTcLevel rhs_tclvl $
1082 runTcSWithEvBinds ev_binds_var $
1083 solveWanteds (mkSimpleWC psig_evs `andWC` wanteds)
1084 -- psig_evs : see Note [Add signature contexts as givens]
1085
1086 -- Find quant_pred_candidates, the predicates that
1087 -- we'll consider quantifying over
1088 -- NB1: wanted_transformed does not include anything provable from
1089 -- the psig_theta; it's just the extra bit
1090 -- NB2: We do not do any defaulting when inferring a type, this can lead
1091 -- to less polymorphic types, see Note [Default while Inferring]
1092 ; wanted_transformed_incl_derivs <- TcM.zonkWC wanted_transformed_incl_derivs
1093 ; let definite_error = insolubleWC wanted_transformed_incl_derivs
1094 -- See Note [Quantification with errors]
1095 -- NB: must include derived errors in this test,
1096 -- hence "incl_derivs"
1097 wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
1098 quant_pred_candidates
1099 | definite_error = []
1100 | otherwise = ctsPreds (approximateWC False wanted_transformed)
1101
1102 -- Decide what type variables and constraints to quantify
1103 -- NB: quant_pred_candidates is already fully zonked
1104 -- NB: bound_theta are constraints we want to quantify over,
1105 -- including the psig_theta, which we always quantify over
1106 -- NB: bound_theta are fully zonked
1107 ; (qtvs, bound_theta, co_vars) <- decideQuantification infer_mode rhs_tclvl
1108 name_taus partial_sigs
1109 quant_pred_candidates
1110 ; bound_theta_vars <- mapM TcM.newEvVar bound_theta
1111
1112 -- Now emit the residual constraint
1113 ; emitResidualConstraints rhs_tclvl ev_binds_var
1114 name_taus co_vars qtvs bound_theta_vars
1115 wanted_transformed
1116
1117 -- All done!
1118 ; traceTc "} simplifyInfer/produced residual implication for quantification" $
1119 vcat [ text "quant_pred_candidates =" <+> ppr quant_pred_candidates
1120 , text "psig_theta =" <+> ppr psig_theta
1121 , text "bound_theta =" <+> ppr bound_theta
1122 , text "qtvs =" <+> ppr qtvs
1123 , text "definite_error =" <+> ppr definite_error ]
1124
1125 ; return ( qtvs, bound_theta_vars, TcEvBinds ev_binds_var, definite_error ) }
1126 -- NB: bound_theta_vars must be fully zonked
1127 where
1128 partial_sigs = filter isPartialSig sigs
1129
1130 --------------------
1131 emitResidualConstraints :: TcLevel -> EvBindsVar
1132 -> [(Name, TcTauType)]
1133 -> VarSet -> [TcTyVar] -> [EvVar]
1134 -> WantedConstraints -> TcM ()
1135 -- Emit the remaining constraints from the RHS.
1136 emitResidualConstraints rhs_tclvl ev_binds_var
1137 name_taus co_vars qtvs full_theta_vars wanteds
1138 | isEmptyWC wanteds
1139 = return ()
1140
1141 | otherwise
1142 = do { wanted_simple <- TcM.zonkSimples (wc_simple wanteds)
1143 ; let (outer_simple, inner_simple) = partitionBag is_mono wanted_simple
1144 is_mono ct = isWantedCt ct && ctEvId ct `elemVarSet` co_vars
1145 -- Reason for the partition:
1146 -- see Note [Emitting the residual implication in simplifyInfer]
1147
1148 -- Already done by defaultTyVarsAndSimplify
1149 -- ; _ <- TcM.promoteTyVarSet (tyCoVarsOfCts outer_simple)
1150
1151 ; let inner_wanted = wanteds { wc_simple = inner_simple }
1152 ; implics <- if isEmptyWC inner_wanted
1153 then return emptyBag
1154 else do implic1 <- newImplication
1155 return $ unitBag $
1156 implic1 { ic_tclvl = rhs_tclvl
1157 , ic_skols = qtvs
1158 , ic_given = full_theta_vars
1159 , ic_wanted = inner_wanted
1160 , ic_binds = ev_binds_var
1161 , ic_given_eqs = MaybeGivenEqs
1162 , ic_info = skol_info }
1163
1164 ; emitConstraints (emptyWC { wc_simple = outer_simple
1165 , wc_impl = implics }) }
1166 where
1167 full_theta = map idType full_theta_vars
1168 skol_info = InferSkol [ (name, mkSigmaTy [] full_theta ty)
1169 | (name, ty) <- name_taus ]
1170 -- We don't add the quantified variables here, because they are
1171 -- also bound in ic_skols and we want them to be tidied
1172 -- uniformly.
1173
1174 --------------------
1175 ctsPreds :: Cts -> [PredType]
1176 ctsPreds cts = [ ctEvPred ev | ct <- bagToList cts
1177 , let ev = ctEvidence ct ]
1178
1179 findInferredDiff :: TcThetaType -> TcThetaType -> TcM TcThetaType
1180 findInferredDiff annotated_theta inferred_theta
1181 = pushTcLevelM_ $
1182 do { lcl_env <- TcM.getLclEnv
1183 ; given_ids <- mapM TcM.newEvVar annotated_theta
1184 ; wanteds <- newWanteds AnnOrigin inferred_theta
1185 ; let given_loc = mkGivenLoc topTcLevel UnkSkol lcl_env
1186 given_cts = mkGivens given_loc given_ids
1187
1188 ; residual <- runTcSDeriveds $
1189 do { _ <- solveSimpleGivens given_cts
1190 ; solveSimpleWanteds (listToBag (map mkNonCanonical wanteds)) }
1191 -- NB: There are no meta tyvars fromn this level annotated_theta
1192 -- because we have either promoted them or unified them
1193 -- See `Note [Quantification and partial signatures]` Wrinkle 2
1194
1195 ; return (map (box_pred . ctPred) $
1196 bagToList $
1197 wc_simple residual) }
1198 where
1199 box_pred :: PredType -> PredType
1200 box_pred pred = case classifyPredType pred of
1201 EqPred rel ty1 ty2
1202 | Just (cls,tys) <- boxEqPred rel ty1 ty2
1203 -> mkClassPred cls tys
1204 | otherwise
1205 -> pprPanic "findInferredDiff" (ppr pred)
1206 _other -> pred
1207
1208 {- Note [Emitting the residual implication in simplifyInfer]
1209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1210 Consider
1211 f = e
1212 where f's type is inferred to be something like (a, Proxy k (Int |> co))
1213 and we have an as-yet-unsolved, or perhaps insoluble, constraint
1214 [W] co :: Type ~ k
1215 We can't form types like (forall co. blah), so we can't generalise over
1216 the coercion variable, and hence we can't generalise over things free in
1217 its kind, in the case 'k'. But we can still generalise over 'a'. So
1218 we'll generalise to
1219 f :: forall a. (a, Proxy k (Int |> co))
1220 Now we do NOT want to form the residual implication constraint
1221 forall a. [W] co :: Type ~ k
1222 because then co's eventual binding (which will be a value binding if we
1223 use -fdefer-type-errors) won't scope over the entire binding for 'f' (whose
1224 type mentions 'co'). Instead, just as we don't generalise over 'co', we
1225 should not bury its constraint inside the implication. Instead, we must
1226 put it outside.
1227
1228 That is the reason for the partitionBag in emitResidualConstraints,
1229 which takes the CoVars free in the inferred type, and pulls their
1230 constraints out. (NB: this set of CoVars should be closed-over-kinds.)
1231
1232 All rather subtle; see #14584.
1233
1234 Note [Add signature contexts as wanteds]
1235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1236 Consider this (#11016):
1237 f2 :: (?x :: Int) => _
1238 f2 = ?x
1239
1240 or this
1241 class C a b | a -> b
1242 g :: C p q => p -> q
1243 f3 :: C Int b => _
1244 f3 = g (3::Int)
1245
1246 We'll use plan InferGen because there are holes in the type. But:
1247 * For f2 we want to have the (?x :: Int) constraint floating around
1248 so that the functional dependencies kick in. Otherwise the
1249 occurrence of ?x on the RHS produces constraint (?x :: alpha), and
1250 we won't unify alpha:=Int.
1251
1252 * For f3 want the (C Int b) constraint from the partial signature
1253 to meet the (C Int beta) constraint we get from the call to g; again,
1254 fundeps
1255
1256 Solution: in simplifyInfer, we add the constraints from the signature
1257 as extra Wanteds
1258
1259 ************************************************************************
1260 * *
1261 Quantification
1262 * *
1263 ************************************************************************
1264
1265 Note [Deciding quantification]
1266 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1267 If the monomorphism restriction does not apply, then we quantify as follows:
1268
1269 * Step 1. Take the global tyvars, and "grow" them using the equality
1270 constraints
1271 E.g. if x:alpha is in the environment, and alpha ~ [beta] (which can
1272 happen because alpha is untouchable here) then do not quantify over
1273 beta, because alpha fixes beta, and beta is effectively free in
1274 the environment too
1275
1276 We also account for the monomorphism restriction; if it applies,
1277 add the free vars of all the constraints.
1278
1279 Result is mono_tvs; we will not quantify over these.
1280
1281 * Step 2. Default any non-mono tyvars (i.e ones that are definitely
1282 not going to become further constrained), and re-simplify the
1283 candidate constraints.
1284
1285 Motivation for re-simplification (#7857): imagine we have a
1286 constraint (C (a->b)), where 'a :: TYPE l1' and 'b :: TYPE l2' are
1287 not free in the envt, and instance forall (a::*) (b::*). (C a) => C
1288 (a -> b) The instance doesn't match while l1,l2 are polymorphic, but
1289 it will match when we default them to LiftedRep.
1290
1291 This is all very tiresome.
1292
1293 * Step 3: decide which variables to quantify over, as follows:
1294
1295 - Take the free vars of the tau-type (zonked_tau_tvs) and "grow"
1296 them using all the constraints. These are tau_tvs_plus
1297
1298 - Use quantifyTyVars to quantify over (tau_tvs_plus - mono_tvs), being
1299 careful to close over kinds, and to skolemise the quantified tyvars.
1300 (This actually unifies each quantifies meta-tyvar with a fresh skolem.)
1301
1302 Result is qtvs.
1303
1304 * Step 4: Filter the constraints using pickQuantifiablePreds and the
1305 qtvs. We have to zonk the constraints first, so they "see" the
1306 freshly created skolems.
1307
1308 -}
1309
1310 decideQuantification
1311 :: InferMode
1312 -> TcLevel
1313 -> [(Name, TcTauType)] -- Variables to be generalised
1314 -> [TcIdSigInst] -- Partial type signatures (if any)
1315 -> [PredType] -- Candidate theta; already zonked
1316 -> TcM ( [TcTyVar] -- Quantify over these (skolems)
1317 , [PredType] -- and this context (fully zonked)
1318 , VarSet)
1319 -- See Note [Deciding quantification]
1320 decideQuantification infer_mode rhs_tclvl name_taus psigs candidates
1321 = do { -- Step 1: find the mono_tvs
1322 ; (mono_tvs, candidates, co_vars) <- decideMonoTyVars infer_mode
1323 name_taus psigs candidates
1324
1325 -- Step 2: default any non-mono tyvars, and re-simplify
1326 -- This step may do some unification, but result candidates is zonked
1327 ; candidates <- defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
1328
1329 -- Step 3: decide which kind/type variables to quantify over
1330 ; qtvs <- decideQuantifiedTyVars name_taus psigs candidates
1331
1332 -- Step 4: choose which of the remaining candidate
1333 -- predicates to actually quantify over
1334 -- NB: decideQuantifiedTyVars turned some meta tyvars
1335 -- into quantified skolems, so we have to zonk again
1336 ; candidates <- TcM.zonkTcTypes candidates
1337 ; psig_theta <- TcM.zonkTcTypes (concatMap sig_inst_theta psigs)
1338 ; let quantifiable_candidates
1339 = pickQuantifiablePreds (mkVarSet qtvs) candidates
1340
1341 theta = mkMinimalBySCs id $ -- See Note [Minimize by Superclasses]
1342 psig_theta ++ quantifiable_candidates
1343 -- NB: add psig_theta back in here, even though it's already
1344 -- part of candidates, because we always want to quantify over
1345 -- psig_theta, and pickQuantifiableCandidates might have
1346 -- dropped some e.g. CallStack constraints. c.f #14658
1347 -- equalities (a ~ Bool)
1348 -- Remember, this is the theta for the residual constraint
1349
1350 ; traceTc "decideQuantification"
1351 (vcat [ text "infer_mode:" <+> ppr infer_mode
1352 , text "candidates:" <+> ppr candidates
1353 , text "psig_theta:" <+> ppr psig_theta
1354 , text "mono_tvs:" <+> ppr mono_tvs
1355 , text "co_vars:" <+> ppr co_vars
1356 , text "qtvs:" <+> ppr qtvs
1357 , text "theta:" <+> ppr theta ])
1358 ; return (qtvs, theta, co_vars) }
1359
1360 ------------------
1361 decideMonoTyVars :: InferMode
1362 -> [(Name,TcType)]
1363 -> [TcIdSigInst]
1364 -> [PredType]
1365 -> TcM (TcTyCoVarSet, [PredType], CoVarSet)
1366 -- Decide which tyvars and covars cannot be generalised:
1367 -- (a) Free in the environment
1368 -- (b) Mentioned in a constraint we can't generalise
1369 -- (c) Connected by an equality to (a) or (b)
1370 -- Also return CoVars that appear free in the final quantified types
1371 -- we can't quantify over these, and we must make sure they are in scope
1372 decideMonoTyVars infer_mode name_taus psigs candidates
1373 = do { (no_quant, maybe_quant) <- pick infer_mode candidates
1374
1375 -- If possible, we quantify over partial-sig qtvs, so they are
1376 -- not mono. Need to zonk them because they are meta-tyvar TyVarTvs
1377 ; psig_qtvs <- mapM zonkTcTyVarToTyVar $ binderVars $
1378 concatMap (map snd . sig_inst_skols) psigs
1379
1380 ; psig_theta <- mapM TcM.zonkTcType $
1381 concatMap sig_inst_theta psigs
1382
1383 ; taus <- mapM (TcM.zonkTcType . snd) name_taus
1384
1385 ; tc_lvl <- TcM.getTcLevel
1386 ; let psig_tys = mkTyVarTys psig_qtvs ++ psig_theta
1387
1388 co_vars = coVarsOfTypes (psig_tys ++ taus)
1389 co_var_tvs = closeOverKinds co_vars
1390 -- The co_var_tvs are tvs mentioned in the types of covars or
1391 -- coercion holes. We can't quantify over these covars, so we
1392 -- must include the variable in their types in the mono_tvs.
1393 -- E.g. If we can't quantify over co :: k~Type, then we can't
1394 -- quantify over k either! Hence closeOverKinds
1395
1396 mono_tvs0 = filterVarSet (not . isQuantifiableTv tc_lvl) $
1397 tyCoVarsOfTypes candidates
1398 -- We need to grab all the non-quantifiable tyvars in the
1399 -- candidates so that we can grow this set to find other
1400 -- non-quantifiable tyvars. This can happen with something
1401 -- like
1402 -- f x y = ...
1403 -- where z = x 3
1404 -- The body of z tries to unify the type of x (call it alpha[1])
1405 -- with (beta[2] -> gamma[2]). This unification fails because
1406 -- alpha is untouchable. But we need to know not to quantify over
1407 -- beta or gamma, because they are in the equality constraint with
1408 -- alpha. Actual test case: typecheck/should_compile/tc213
1409
1410 mono_tvs1 = mono_tvs0 `unionVarSet` co_var_tvs
1411
1412 eq_constraints = filter isEqPrimPred candidates
1413 mono_tvs2 = growThetaTyVars eq_constraints mono_tvs1
1414
1415 constrained_tvs = filterVarSet (isQuantifiableTv tc_lvl) $
1416 (growThetaTyVars eq_constraints
1417 (tyCoVarsOfTypes no_quant)
1418 `minusVarSet` mono_tvs2)
1419 `delVarSetList` psig_qtvs
1420 -- constrained_tvs: the tyvars that we are not going to
1421 -- quantify solely because of the monomorphism restriction
1422 --
1423 -- (`minusVarSet` mono_tvs2`): a type variable is only
1424 -- "constrained" (so that the MR bites) if it is not
1425 -- free in the environment (#13785)
1426 --
1427 -- (`delVarSetList` psig_qtvs): if the user has explicitly
1428 -- asked for quantification, then that request "wins"
1429 -- over the MR. Note: do /not/ delete psig_qtvs from
1430 -- mono_tvs1, because mono_tvs1 cannot under any circumstances
1431 -- be quantified (#14479); see
1432 -- Note [Quantification and partial signatures], Wrinkle 3, 4
1433
1434 mono_tvs = mono_tvs2 `unionVarSet` constrained_tvs
1435
1436 -- Warn about the monomorphism restriction
1437 ; when (case infer_mode of { ApplyMR -> True; _ -> False}) $ do
1438 let dia = TcRnMonomorphicBindings (map fst name_taus)
1439 diagnosticTc (constrained_tvs `intersectsVarSet` tyCoVarsOfTypes taus) dia
1440
1441 ; traceTc "decideMonoTyVars" $ vcat
1442 [ text "infer_mode =" <+> ppr infer_mode
1443 , text "mono_tvs0 =" <+> ppr mono_tvs0
1444 , text "no_quant =" <+> ppr no_quant
1445 , text "maybe_quant =" <+> ppr maybe_quant
1446 , text "eq_constraints =" <+> ppr eq_constraints
1447 , text "mono_tvs =" <+> ppr mono_tvs
1448 , text "co_vars =" <+> ppr co_vars ]
1449
1450 ; return (mono_tvs, maybe_quant, co_vars) }
1451 where
1452 pick :: InferMode -> [PredType] -> TcM ([PredType], [PredType])
1453 -- Split the candidates into ones we definitely
1454 -- won't quantify, and ones that we might
1455 pick NoRestrictions cand = return ([], cand)
1456 pick ApplyMR cand = return (cand, [])
1457 pick EagerDefaulting cand = do { os <- xoptM LangExt.OverloadedStrings
1458 ; return (partition (is_int_ct os) cand) }
1459
1460 -- For EagerDefaulting, do not quantify over
1461 -- over any interactive class constraint
1462 is_int_ct ovl_strings pred
1463 | Just (cls, _) <- getClassPredTys_maybe pred
1464 = isInteractiveClass ovl_strings cls
1465 | otherwise
1466 = False
1467
1468 -------------------
1469 defaultTyVarsAndSimplify :: TcLevel
1470 -> TyCoVarSet
1471 -> [PredType] -- Assumed zonked
1472 -> TcM [PredType] -- Guaranteed zonked
1473 -- Default any tyvar free in the constraints,
1474 -- and re-simplify in case the defaulting allows further simplification
1475 defaultTyVarsAndSimplify rhs_tclvl mono_tvs candidates
1476 = do { -- Promote any tyvars that we cannot generalise
1477 -- See Note [Promote monomorphic tyvars]
1478 ; traceTc "decideMonoTyVars: promotion:" (ppr mono_tvs)
1479 ; any_promoted <- promoteTyVarSet mono_tvs
1480
1481 -- Default any kind/levity vars
1482 ; DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs}
1483 <- candidateQTyVarsOfTypes candidates
1484 -- any covars should already be handled by
1485 -- the logic in decideMonoTyVars, which looks at
1486 -- the constraints generated
1487
1488 ; poly_kinds <- xoptM LangExt.PolyKinds
1489 ; default_kvs <- mapM (default_one poly_kinds True)
1490 (dVarSetElems cand_kvs)
1491 ; default_tvs <- mapM (default_one poly_kinds False)
1492 (dVarSetElems (cand_tvs `minusDVarSet` cand_kvs))
1493 ; let some_default = or default_kvs || or default_tvs
1494
1495 ; case () of
1496 _ | some_default -> simplify_cand candidates
1497 | any_promoted -> mapM TcM.zonkTcType candidates
1498 | otherwise -> return candidates
1499 }
1500 where
1501 default_one poly_kinds is_kind_var tv
1502 | not (isMetaTyVar tv)
1503 = return False
1504 | tv `elemVarSet` mono_tvs
1505 = return False
1506 | otherwise
1507 = defaultTyVar
1508 (if not poly_kinds && is_kind_var then DefaultKinds else Don'tDefaultKinds)
1509 allVarsOfKindDefault
1510 tv
1511
1512 simplify_cand candidates
1513 = do { clone_wanteds <- newWanteds DefaultOrigin candidates
1514 ; WC { wc_simple = simples } <- setTcLevel rhs_tclvl $
1515 simplifyWantedsTcM clone_wanteds
1516 -- Discard evidence; simples is fully zonked
1517
1518 ; let new_candidates = ctsPreds simples
1519 ; traceTc "Simplified after defaulting" $
1520 vcat [ text "Before:" <+> ppr candidates
1521 , text "After:" <+> ppr new_candidates ]
1522 ; return new_candidates }
1523
1524 ------------------
1525 decideQuantifiedTyVars
1526 :: [(Name,TcType)] -- Annotated theta and (name,tau) pairs
1527 -> [TcIdSigInst] -- Partial signatures
1528 -> [PredType] -- Candidates, zonked
1529 -> TcM [TyVar]
1530 -- Fix what tyvars we are going to quantify over, and quantify them
1531 decideQuantifiedTyVars name_taus psigs candidates
1532 = do { -- Why psig_tys? We try to quantify over everything free in here
1533 -- See Note [Quantification and partial signatures]
1534 -- Wrinkles 2 and 3
1535 ; psig_tv_tys <- mapM TcM.zonkTcTyVar [ tv | sig <- psigs
1536 , (_,Bndr tv _) <- sig_inst_skols sig ]
1537 ; psig_theta <- mapM TcM.zonkTcType [ pred | sig <- psigs
1538 , pred <- sig_inst_theta sig ]
1539 ; tau_tys <- mapM (TcM.zonkTcType . snd) name_taus
1540
1541 ; let -- Try to quantify over variables free in these types
1542 psig_tys = psig_tv_tys ++ psig_theta
1543 seed_tys = psig_tys ++ tau_tys
1544
1545 -- Now "grow" those seeds to find ones reachable via 'candidates'
1546 grown_tcvs = growThetaTyVars candidates (tyCoVarsOfTypes seed_tys)
1547
1548 -- Now we have to classify them into kind variables and type variables
1549 -- (sigh) just for the benefit of -XNoPolyKinds; see quantifyTyVars
1550 --
1551 -- Keep the psig_tys first, so that candidateQTyVarsOfTypes produces
1552 -- them in that order, so that the final qtvs quantifies in the same
1553 -- order as the partial signatures do (#13524)
1554 ; dv@DV {dv_kvs = cand_kvs, dv_tvs = cand_tvs} <- candidateQTyVarsOfTypes $
1555 psig_tys ++ candidates ++ tau_tys
1556 ; let pick = (`dVarSetIntersectVarSet` grown_tcvs)
1557 dvs_plus = dv { dv_kvs = pick cand_kvs, dv_tvs = pick cand_tvs }
1558
1559 ; traceTc "decideQuantifiedTyVars" (vcat
1560 [ text "tau_tys =" <+> ppr tau_tys
1561 , text "candidates =" <+> ppr candidates
1562 , text "cand_kvs =" <+> ppr cand_kvs
1563 , text "cand_tvs =" <+> ppr cand_tvs
1564 , text "tau_tys =" <+> ppr tau_tys
1565 , text "seed_tys =" <+> ppr seed_tys
1566 , text "seed_tcvs =" <+> ppr (tyCoVarsOfTypes seed_tys)
1567 , text "grown_tcvs =" <+> ppr grown_tcvs
1568 , text "dvs =" <+> ppr dvs_plus])
1569
1570 ; quantifyTyVars allVarsOfKindDefault dvs_plus }
1571
1572 ------------------
1573 growThetaTyVars :: ThetaType -> TyCoVarSet -> TyCoVarSet
1574 -- See Note [Growing the tau-tvs using constraints]
1575 growThetaTyVars theta tcvs
1576 | null theta = tcvs
1577 | otherwise = transCloVarSet mk_next seed_tcvs
1578 where
1579 seed_tcvs = tcvs `unionVarSet` tyCoVarsOfTypes ips
1580 (ips, non_ips) = partition isIPLikePred theta
1581 -- See Note [Inheriting implicit parameters] in GHC.Tc.Utils.TcType
1582
1583 mk_next :: VarSet -> VarSet -- Maps current set to newly-grown ones
1584 mk_next so_far = foldr (grow_one so_far) emptyVarSet non_ips
1585 grow_one so_far pred tcvs
1586 | pred_tcvs `intersectsVarSet` so_far = tcvs `unionVarSet` pred_tcvs
1587 | otherwise = tcvs
1588 where
1589 pred_tcvs = tyCoVarsOfType pred
1590
1591
1592 {- Note [Promote monomorphic tyvars]
1593 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1594 Promote any type variables that are free in the environment. Eg
1595 f :: forall qtvs. bound_theta => zonked_tau
1596 The free vars of f's type become free in the envt, and hence will show
1597 up whenever 'f' is called. They may currently at rhs_tclvl, but they
1598 had better be unifiable at the outer_tclvl! Example: envt mentions
1599 alpha[1]
1600 tau_ty = beta[2] -> beta[2]
1601 constraints = alpha ~ [beta]
1602 we don't quantify over beta (since it is fixed by envt)
1603 so we must promote it! The inferred type is just
1604 f :: beta -> beta
1605
1606 NB: promoteTyVarSet ignores coercion variables
1607
1608 Note [Quantification and partial signatures]
1609 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1610 When choosing type variables to quantify, the basic plan is to
1611 quantify over all type variables that are
1612 * free in the tau_tvs, and
1613 * not forced to be monomorphic (mono_tvs),
1614 for example by being free in the environment.
1615
1616 However, in the case of a partial type signature, be doing inference
1617 *in the presence of a type signature*. For example:
1618 f :: _ -> a
1619 f x = ...
1620 or
1621 g :: (Eq _a) => _b -> _b
1622 In both cases we use plan InferGen, and hence call simplifyInfer. But
1623 those 'a' variables are skolems (actually TyVarTvs), and we should be
1624 sure to quantify over them. This leads to several wrinkles:
1625
1626 * Wrinkle 1. In the case of a type error
1627 f :: _ -> Maybe a
1628 f x = True && x
1629 The inferred type of 'f' is f :: Bool -> Bool, but there's a
1630 left-over error of form (HoleCan (Maybe a ~ Bool)). The error-reporting
1631 machine expects to find a binding site for the skolem 'a', so we
1632 add it to the quantified tyvars.
1633
1634 * Wrinkle 2. Consider the partial type signature
1635 f :: (Eq _) => Int -> Int
1636 f x = x
1637 In normal cases that makes sense; e.g.
1638 g :: Eq _a => _a -> _a
1639 g x = x
1640 where the signature makes the type less general than it could
1641 be. But for 'f' we must therefore quantify over the user-annotated
1642 constraints, to get
1643 f :: forall a. Eq a => Int -> Int
1644 (thereby correctly triggering an ambiguity error later). If we don't
1645 we'll end up with a strange open type
1646 f :: Eq alpha => Int -> Int
1647 which isn't ambiguous but is still very wrong.
1648
1649 Bottom line: Try to quantify over any variable free in psig_theta,
1650 just like the tau-part of the type.
1651
1652 * Wrinkle 3 (#13482). Also consider
1653 f :: forall a. _ => Int -> Int
1654 f x = if (undefined :: a) == undefined then x else 0
1655 Here we get an (Eq a) constraint, but it's not mentioned in the
1656 psig_theta nor the type of 'f'. But we still want to quantify
1657 over 'a' even if the monomorphism restriction is on.
1658
1659 * Wrinkle 4 (#14479)
1660 foo :: Num a => a -> a
1661 foo xxx = g xxx
1662 where
1663 g :: forall b. Num b => _ -> b
1664 g y = xxx + y
1665
1666 In the signature for 'g', we cannot quantify over 'b' because it turns out to
1667 get unified with 'a', which is free in g's environment. So we carefully
1668 refrain from bogusly quantifying, in GHC.Tc.Solver.decideMonoTyVars. We
1669 report the error later, in GHC.Tc.Gen.Bind.chooseInferredQuantifiers.
1670
1671 Note [Growing the tau-tvs using constraints]
1672 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1673 (growThetaTyVars insts tvs) is the result of extending the set
1674 of tyvars, tvs, using all conceivable links from pred
1675
1676 E.g. tvs = {a}, preds = {H [a] b, K (b,Int) c, Eq e}
1677 Then growThetaTyVars preds tvs = {a,b,c}
1678
1679 Notice that
1680 growThetaTyVars is conservative if v might be fixed by vs
1681 => v `elem` grow(vs,C)
1682
1683 Note [Quantification with errors]
1684 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1685 If we find that the RHS of the definition has some absolutely-insoluble
1686 constraints (including especially "variable not in scope"), we
1687
1688 * Abandon all attempts to find a context to quantify over,
1689 and instead make the function fully-polymorphic in whatever
1690 type we have found
1691
1692 * Return a flag from simplifyInfer, indicating that we found an
1693 insoluble constraint. This flag is used to suppress the ambiguity
1694 check for the inferred type, which may well be bogus, and which
1695 tends to obscure the real error. This fix feels a bit clunky,
1696 but I failed to come up with anything better.
1697
1698 Reasons:
1699 - Avoid downstream errors
1700 - Do not perform an ambiguity test on a bogus type, which might well
1701 fail spuriously, thereby obfuscating the original insoluble error.
1702 #14000 is an example
1703
1704 I tried an alternative approach: simply failM, after emitting the
1705 residual implication constraint; the exception will be caught in
1706 GHC.Tc.Gen.Bind.tcPolyBinds, which gives all the binders in the group the type
1707 (forall a. a). But that didn't work with -fdefer-type-errors, because
1708 the recovery from failM emits no code at all, so there is no function
1709 to run! But -fdefer-type-errors aspires to produce a runnable program.
1710
1711 NB that we must include *derived* errors in the check for insolubles.
1712 Example:
1713 (a::*) ~ Int#
1714 We get an insoluble derived error *~#, and we don't want to discard
1715 it before doing the isInsolubleWC test! (#8262)
1716
1717 Note [Default while Inferring]
1718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1719 Our current plan is that defaulting only happens at simplifyTop and
1720 not simplifyInfer. This may lead to some insoluble deferred constraints.
1721 Example:
1722
1723 instance D g => C g Int b
1724
1725 constraint inferred = (forall b. 0 => C gamma alpha b) /\ Num alpha
1726 type inferred = gamma -> gamma
1727
1728 Now, if we try to default (alpha := Int) we will be able to refine the implication to
1729 (forall b. 0 => C gamma Int b)
1730 which can then be simplified further to
1731 (forall b. 0 => D gamma)
1732 Finally, we /can/ approximate this implication with (D gamma) and infer the quantified
1733 type: forall g. D g => g -> g
1734
1735 Instead what will currently happen is that we will get a quantified type
1736 (forall g. g -> g) and an implication:
1737 forall g. 0 => (forall b. 0 => C g alpha b) /\ Num alpha
1738
1739 Which, even if the simplifyTop defaults (alpha := Int) we will still be left with an
1740 unsolvable implication:
1741 forall g. 0 => (forall b. 0 => D g)
1742
1743 The concrete example would be:
1744 h :: C g a s => g -> a -> ST s a
1745 f (x::gamma) = (\_ -> x) (runST (h x (undefined::alpha)) + 1)
1746
1747 But it is quite tedious to do defaulting and resolve the implication constraints, and
1748 we have not observed code breaking because of the lack of defaulting in inference, so
1749 we don't do it for now.
1750
1751
1752
1753 Note [Minimize by Superclasses]
1754 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1755 When we quantify over a constraint, in simplifyInfer we need to
1756 quantify over a constraint that is minimal in some sense: For
1757 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
1758 we'd like to quantify over Ord alpha, because we can just get Eq alpha
1759 from superclass selection from Ord alpha. This minimization is what
1760 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
1761 to check the original wanted.
1762
1763
1764 Note [Avoid unnecessary constraint simplification]
1765 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1766 -------- NB NB NB (Jun 12) -------------
1767 This note not longer applies; see the notes with #4361.
1768 But I'm leaving it in here so we remember the issue.)
1769 ----------------------------------------
1770 When inferring the type of a let-binding, with simplifyInfer,
1771 try to avoid unnecessarily simplifying class constraints.
1772 Doing so aids sharing, but it also helps with delicate
1773 situations like
1774
1775 instance C t => C [t] where ..
1776
1777 f :: C [t] => ....
1778 f x = let g y = ...(constraint C [t])...
1779 in ...
1780 When inferring a type for 'g', we don't want to apply the
1781 instance decl, because then we can't satisfy (C t). So we
1782 just notice that g isn't quantified over 't' and partition
1783 the constraints before simplifying.
1784
1785 This only half-works, but then let-generalisation only half-works.
1786
1787 *********************************************************************************
1788 * *
1789 * Main Simplifier *
1790 * *
1791 ***********************************************************************************
1792
1793 -}
1794
1795 simplifyWantedsTcM :: [CtEvidence] -> TcM WantedConstraints
1796 -- Solve the specified Wanted constraints
1797 -- Discard the evidence binds
1798 -- Discards all Derived stuff in result
1799 -- Postcondition: fully zonked
1800 simplifyWantedsTcM wanted
1801 = do { traceTc "simplifyWantedsTcM {" (ppr wanted)
1802 ; (result, _) <- runTcS (solveWantedsAndDrop (mkSimpleWC wanted))
1803 ; result <- TcM.zonkWC result
1804 ; traceTc "simplifyWantedsTcM }" (ppr result)
1805 ; return result }
1806
1807 solveWantedsAndDrop :: WantedConstraints -> TcS WantedConstraints
1808 -- Since solveWanteds returns the residual WantedConstraints,
1809 -- it should always be called within a runTcS or something similar,
1810 -- Result is not zonked
1811 solveWantedsAndDrop wanted
1812 = do { wc <- solveWanteds wanted
1813 ; return (dropDerivedWC wc) }
1814
1815 solveWanteds :: WantedConstraints -> TcS WantedConstraints
1816 -- so that the inert set doesn't mindlessly propagate.
1817 -- NB: wc_simples may be wanted /or/ derived now
1818 solveWanteds wc@(WC { wc_holes = holes })
1819 = do { cur_lvl <- TcS.getTcLevel
1820 ; traceTcS "solveWanteds {" $
1821 vcat [ text "Level =" <+> ppr cur_lvl
1822 , ppr wc ]
1823
1824 ; dflags <- getDynFlags
1825 ; solved_wc <- simplify_loop 0 (solverIterations dflags) True wc
1826
1827 ; holes' <- simplifyHoles holes
1828 ; let final_wc = solved_wc { wc_holes = holes' }
1829
1830 ; ev_binds_var <- getTcEvBindsVar
1831 ; bb <- TcS.getTcEvBindsMap ev_binds_var
1832 ; traceTcS "solveWanteds }" $
1833 vcat [ text "final wc =" <+> ppr final_wc
1834 , text "current evbinds =" <+> ppr (evBindMapBinds bb) ]
1835
1836 ; return final_wc }
1837
1838 simplify_loop :: Int -> IntWithInf -> Bool
1839 -> WantedConstraints -> TcS WantedConstraints
1840 -- Do a round of solving, and call maybe_simplify_again to iterate
1841 -- The 'definitely_redo_implications' flags is False if the only reason we
1842 -- are iterating is that we have added some new Derived superclasses (from Wanteds)
1843 -- hoping for fundeps to help us; see Note [Superclass iteration]
1844 --
1845 -- Does not affect wc_holes at all; reason: wc_holes never affects anything
1846 -- else, so we do them once, at the end in solveWanteds
1847 simplify_loop n limit definitely_redo_implications
1848 wc@(WC { wc_simple = simples, wc_impl = implics })
1849 = do { csTraceTcS $
1850 text "simplify_loop iteration=" <> int n
1851 <+> (parens $ hsep [ text "definitely_redo =" <+> ppr definitely_redo_implications <> comma
1852 , int (lengthBag simples) <+> text "simples to solve" ])
1853 ; traceTcS "simplify_loop: wc =" (ppr wc)
1854
1855 ; (unifs1, wc1) <- reportUnifications $ -- See Note [Superclass iteration]
1856 solveSimpleWanteds simples
1857 -- Any insoluble constraints are in 'simples' and so get rewritten
1858 -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet
1859
1860 ; wc2 <- if not definitely_redo_implications -- See Note [Superclass iteration]
1861 && unifs1 == 0 -- for this conditional
1862 && isEmptyBag (wc_impl wc1)
1863 then return (wc { wc_simple = wc_simple wc1 }) -- Short cut
1864 else do { implics2 <- solveNestedImplications $
1865 implics `unionBags` (wc_impl wc1)
1866 ; return (wc { wc_simple = wc_simple wc1
1867 , wc_impl = implics2 }) }
1868
1869 ; unif_happened <- resetUnificationFlag
1870 -- Note [The Unification Level Flag] in GHC.Tc.Solver.Monad
1871 ; maybe_simplify_again (n+1) limit unif_happened wc2 }
1872
1873 maybe_simplify_again :: Int -> IntWithInf -> Bool
1874 -> WantedConstraints -> TcS WantedConstraints
1875 maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples })
1876 | n `intGtLimit` limit
1877 = do { -- Add an error (not a warning) if we blow the limit,
1878 -- Typically if we blow the limit we are going to report some other error
1879 -- (an unsolved constraint), and we don't want that error to suppress
1880 -- the iteration limit warning!
1881 addErrTcS $ TcRnSimplifierTooManyIterations simples limit wc
1882 ; return wc }
1883
1884 | unif_happened
1885 = simplify_loop n limit True wc
1886
1887 | superClassesMightHelp wc
1888 = -- We still have unsolved goals, and apparently no way to solve them,
1889 -- so try expanding superclasses at this level, both Given and Wanted
1890 do { pending_given <- getPendingGivenScs
1891 ; let (pending_wanted, simples1) = getPendingWantedScs simples
1892 ; if null pending_given && null pending_wanted
1893 then return wc -- After all, superclasses did not help
1894 else
1895 do { new_given <- makeSuperClasses pending_given
1896 ; new_wanted <- makeSuperClasses pending_wanted
1897 ; solveSimpleGivens new_given -- Add the new Givens to the inert set
1898 ; simplify_loop n limit (not (null pending_given)) $
1899 wc { wc_simple = simples1 `unionBags` listToBag new_wanted } } }
1900 -- (not (null pending_given)): see Note [Superclass iteration]
1901
1902 | otherwise
1903 = return wc
1904
1905 {- Note [Superclass iteration]
1906 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1907 Consider this implication constraint
1908 forall a.
1909 [W] d: C Int beta
1910 forall b. blah
1911 where
1912 class D a b | a -> b
1913 class D a b => C a b
1914 We will expand d's superclasses, giving [D] D Int beta, in the hope of geting
1915 fundeps to unify beta. Doing so is usually fruitless (no useful fundeps),
1916 and if so it seems a pity to waste time iterating the implications (forall b. blah)
1917 (If we add new Given superclasses it's a different matter: it's really worth looking
1918 at the implications.)
1919
1920 Hence the definitely_redo_implications flag to simplify_loop. It's usually
1921 True, but False in the case where the only reason to iterate is new Derived
1922 superclasses. In that case we check whether the new Deriveds actually led to
1923 any new unifications, and iterate the implications only if so.
1924 -}
1925
1926 solveNestedImplications :: Bag Implication
1927 -> TcS (Bag Implication)
1928 -- Precondition: the TcS inerts may contain unsolved simples which have
1929 -- to be converted to givens before we go inside a nested implication.
1930 solveNestedImplications implics
1931 | isEmptyBag implics
1932 = return (emptyBag)
1933 | otherwise
1934 = do { traceTcS "solveNestedImplications starting {" empty
1935 ; unsolved_implics <- mapBagM solveImplication implics
1936
1937 -- ... and we are back in the original TcS inerts
1938 -- Notice that the original includes the _insoluble_simples so it was safe to ignore
1939 -- them in the beginning of this function.
1940 ; traceTcS "solveNestedImplications end }" $
1941 vcat [ text "unsolved_implics =" <+> ppr unsolved_implics ]
1942
1943 ; return (catBagMaybes unsolved_implics) }
1944
1945 solveImplication :: Implication -- Wanted
1946 -> TcS (Maybe Implication) -- Simplified implication (empty or singleton)
1947 -- Precondition: The TcS monad contains an empty worklist and given-only inerts
1948 -- which after trying to solve this implication we must restore to their original value
1949 solveImplication imp@(Implic { ic_tclvl = tclvl
1950 , ic_binds = ev_binds_var
1951 , ic_given = given_ids
1952 , ic_wanted = wanteds
1953 , ic_info = info
1954 , ic_status = status })
1955 | isSolvedStatus status
1956 = return (Just imp) -- Do nothing
1957
1958 | otherwise -- Even for IC_Insoluble it is worth doing more work
1959 -- The insoluble stuff might be in one sub-implication
1960 -- and other unsolved goals in another; and we want to
1961 -- solve the latter as much as possible
1962 = do { inerts <- getTcSInerts
1963 ; traceTcS "solveImplication {" (ppr imp $$ text "Inerts" <+> ppr inerts)
1964
1965 -- commented out; see `where` clause below
1966 -- ; when debugIsOn check_tc_level
1967
1968 -- Solve the nested constraints
1969 ; (has_given_eqs, given_insols, residual_wanted)
1970 <- nestImplicTcS ev_binds_var tclvl $
1971 do { let loc = mkGivenLoc tclvl info (ic_env imp)
1972 givens = mkGivens loc given_ids
1973 ; solveSimpleGivens givens
1974
1975 ; residual_wanted <- solveWanteds wanteds
1976 -- solveWanteds, *not* solveWantedsAndDrop, because
1977 -- we want to retain derived equalities so we can float
1978 -- them out in floatEqualities.
1979
1980 ; (has_eqs, given_insols) <- getHasGivenEqs tclvl
1981 -- Call getHasGivenEqs /after/ solveWanteds, because
1982 -- solveWanteds can augment the givens, via expandSuperClasses,
1983 -- to reveal given superclass equalities
1984
1985 ; return (has_eqs, given_insols, residual_wanted) }
1986
1987 ; traceTcS "solveImplication 2"
1988 (ppr given_insols $$ ppr residual_wanted)
1989 ; let final_wanted = residual_wanted `addInsols` given_insols
1990 -- Don't lose track of the insoluble givens,
1991 -- which signal unreachable code; put them in ic_wanted
1992
1993 ; res_implic <- setImplicationStatus (imp { ic_given_eqs = has_given_eqs
1994 , ic_wanted = final_wanted })
1995
1996 ; evbinds <- TcS.getTcEvBindsMap ev_binds_var
1997 ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
1998 ; traceTcS "solveImplication end }" $ vcat
1999 [ text "has_given_eqs =" <+> ppr has_given_eqs
2000 , text "res_implic =" <+> ppr res_implic
2001 , text "implication evbinds =" <+> ppr (evBindMapBinds evbinds)
2002 , text "implication tvcs =" <+> ppr tcvs ]
2003
2004 ; return res_implic }
2005
2006 -- TcLevels must be strictly increasing (see (ImplicInv) in
2007 -- Note [TcLevel invariants] in GHC.Tc.Utils.TcType),
2008 -- and in fact I think they should always increase one level at a time.
2009
2010 -- Though sensible, this check causes lots of testsuite failures. It is
2011 -- remaining commented out for now.
2012 {-
2013 check_tc_level = do { cur_lvl <- TcS.getTcLevel
2014 ; massertPpr (tclvl == pushTcLevel cur_lvl)
2015 (text "Cur lvl =" <+> ppr cur_lvl $$ text "Imp lvl =" <+> ppr tclvl) }
2016 -}
2017
2018 ----------------------
2019 setImplicationStatus :: Implication -> TcS (Maybe Implication)
2020 -- Finalise the implication returned from solveImplication:
2021 -- * Set the ic_status field
2022 -- * Trim the ic_wanted field to remove Derived constraints
2023 -- Precondition: the ic_status field is not already IC_Solved
2024 -- Return Nothing if we can discard the implication altogether
2025 setImplicationStatus implic@(Implic { ic_status = status
2026 , ic_info = info
2027 , ic_wanted = wc
2028 , ic_given = givens })
2029 | assertPpr (not (isSolvedStatus status)) (ppr info) $
2030 -- Precondition: we only set the status if it is not already solved
2031 not (isSolvedWC pruned_wc)
2032 = do { traceTcS "setImplicationStatus(not-all-solved) {" (ppr implic)
2033
2034 ; implic <- neededEvVars implic
2035
2036 ; let new_status | insolubleWC pruned_wc = IC_Insoluble
2037 | otherwise = IC_Unsolved
2038 new_implic = implic { ic_status = new_status
2039 , ic_wanted = pruned_wc }
2040
2041 ; traceTcS "setImplicationStatus(not-all-solved) }" (ppr new_implic)
2042
2043 ; return $ Just new_implic }
2044
2045 | otherwise -- Everything is solved
2046 -- Set status to IC_Solved,
2047 -- and compute the dead givens and outer needs
2048 -- See Note [Tracking redundant constraints]
2049 = do { traceTcS "setImplicationStatus(all-solved) {" (ppr implic)
2050
2051 ; implic@(Implic { ic_need_inner = need_inner
2052 , ic_need_outer = need_outer }) <- neededEvVars implic
2053
2054 ; bad_telescope <- checkBadTelescope implic
2055
2056 ; let dead_givens | warnRedundantGivens info
2057 = filterOut (`elemVarSet` need_inner) givens
2058 | otherwise = [] -- None to report
2059
2060 discard_entire_implication -- Can we discard the entire implication?
2061 = null dead_givens -- No warning from this implication
2062 && not bad_telescope
2063 && isEmptyWC pruned_wc -- No live children
2064 && isEmptyVarSet need_outer -- No needed vars to pass up to parent
2065
2066 final_status
2067 | bad_telescope = IC_BadTelescope
2068 | otherwise = IC_Solved { ics_dead = dead_givens }
2069 final_implic = implic { ic_status = final_status
2070 , ic_wanted = pruned_wc }
2071
2072 ; traceTcS "setImplicationStatus(all-solved) }" $
2073 vcat [ text "discard:" <+> ppr discard_entire_implication
2074 , text "new_implic:" <+> ppr final_implic ]
2075
2076 ; return $ if discard_entire_implication
2077 then Nothing
2078 else Just final_implic }
2079 where
2080 WC { wc_simple = simples, wc_impl = implics, wc_holes = holes } = wc
2081
2082 pruned_simples = dropDerivedSimples simples
2083 pruned_implics = filterBag keep_me implics
2084 pruned_wc = WC { wc_simple = pruned_simples
2085 , wc_impl = pruned_implics
2086 , wc_holes = holes } -- do not prune holes; these should be reported
2087
2088 keep_me :: Implication -> Bool
2089 keep_me ic
2090 | IC_Solved { ics_dead = dead_givens } <- ic_status ic
2091 -- Fully solved
2092 , null dead_givens -- No redundant givens to report
2093 , isEmptyBag (wc_impl (ic_wanted ic))
2094 -- And no children that might have things to report
2095 = False -- Tnen we don't need to keep it
2096 | otherwise
2097 = True -- Otherwise, keep it
2098
2099 checkBadTelescope :: Implication -> TcS Bool
2100 -- True <=> the skolems form a bad telescope
2101 -- See Note [Checking telescopes] in GHC.Tc.Types.Constraint
2102 checkBadTelescope (Implic { ic_info = info
2103 , ic_skols = skols })
2104 | checkTelescopeSkol info
2105 = do{ skols <- mapM TcS.zonkTyCoVarKind skols
2106 ; return (go emptyVarSet (reverse skols))}
2107
2108 | otherwise
2109 = return False
2110
2111 where
2112 go :: TyVarSet -- skolems that appear *later* than the current ones
2113 -> [TcTyVar] -- ordered skolems, in reverse order
2114 -> Bool -- True <=> there is an out-of-order skolem
2115 go _ [] = False
2116 go later_skols (one_skol : earlier_skols)
2117 | tyCoVarsOfType (tyVarKind one_skol) `intersectsVarSet` later_skols
2118 = True
2119 | otherwise
2120 = go (later_skols `extendVarSet` one_skol) earlier_skols
2121
2122 warnRedundantGivens :: SkolemInfo -> Bool
2123 warnRedundantGivens (SigSkol ctxt _ _)
2124 = case ctxt of
2125 FunSigCtxt _ rrc -> reportRedundantConstraints rrc
2126 ExprSigCtxt rrc -> reportRedundantConstraints rrc
2127 _ -> False
2128
2129 -- To think about: do we want to report redundant givens for
2130 -- pattern synonyms, PatSynSigSkol? c.f #9953, comment:21.
2131 warnRedundantGivens (InstSkol {}) = True
2132 warnRedundantGivens _ = False
2133
2134 neededEvVars :: Implication -> TcS Implication
2135 -- Find all the evidence variables that are "needed",
2136 -- and delete dead evidence bindings
2137 -- See Note [Tracking redundant constraints]
2138 -- See Note [Delete dead Given evidence bindings]
2139 --
2140 -- - Start from initial_seeds (from nested implications)
2141 --
2142 -- - Add free vars of RHS of all Wanted evidence bindings
2143 -- and coercion variables accumulated in tcvs (all Wanted)
2144 --
2145 -- - Generate 'needed', the needed set of EvVars, by doing transitive
2146 -- closure through Given bindings
2147 -- e.g. Needed {a,b}
2148 -- Given a = sc_sel a2
2149 -- Then a2 is needed too
2150 --
2151 -- - Prune out all Given bindings that are not needed
2152 --
2153 -- - From the 'needed' set, delete ev_bndrs, the binders of the
2154 -- evidence bindings, to give the final needed variables
2155 --
2156 neededEvVars implic@(Implic { ic_given = givens
2157 , ic_binds = ev_binds_var
2158 , ic_wanted = WC { wc_impl = implics }
2159 , ic_need_inner = old_needs })
2160 = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var
2161 ; tcvs <- TcS.getTcEvTyCoVars ev_binds_var
2162
2163 ; let seeds1 = foldr add_implic_seeds old_needs implics
2164 seeds2 = nonDetStrictFoldEvBindMap add_wanted seeds1 ev_binds
2165 -- It's OK to use a non-deterministic fold here
2166 -- because add_wanted is commutative
2167 seeds3 = seeds2 `unionVarSet` tcvs
2168 need_inner = findNeededEvVars ev_binds seeds3
2169 live_ev_binds = filterEvBindMap (needed_ev_bind need_inner) ev_binds
2170 need_outer = varSetMinusEvBindMap need_inner live_ev_binds
2171 `delVarSetList` givens
2172
2173 ; TcS.setTcEvBindsMap ev_binds_var live_ev_binds
2174 -- See Note [Delete dead Given evidence bindings]
2175
2176 ; traceTcS "neededEvVars" $
2177 vcat [ text "old_needs:" <+> ppr old_needs
2178 , text "seeds3:" <+> ppr seeds3
2179 , text "tcvs:" <+> ppr tcvs
2180 , text "ev_binds:" <+> ppr ev_binds
2181 , text "live_ev_binds:" <+> ppr live_ev_binds ]
2182
2183 ; return (implic { ic_need_inner = need_inner
2184 , ic_need_outer = need_outer }) }
2185 where
2186 add_implic_seeds (Implic { ic_need_outer = needs }) acc
2187 = needs `unionVarSet` acc
2188
2189 needed_ev_bind needed (EvBind { eb_lhs = ev_var
2190 , eb_is_given = is_given })
2191 | is_given = ev_var `elemVarSet` needed
2192 | otherwise = True -- Keep all wanted bindings
2193
2194 add_wanted :: EvBind -> VarSet -> VarSet
2195 add_wanted (EvBind { eb_is_given = is_given, eb_rhs = rhs }) needs
2196 | is_given = needs -- Add the rhs vars of the Wanted bindings only
2197 | otherwise = evVarsOfTerm rhs `unionVarSet` needs
2198
2199 -------------------------------------------------
2200 simplifyHoles :: Bag Hole -> TcS (Bag Hole)
2201 simplifyHoles = mapBagM simpl_hole
2202 where
2203 simpl_hole :: Hole -> TcS Hole
2204
2205 -- See Note [Do not simplify ConstraintHoles]
2206 simpl_hole h@(Hole { hole_sort = ConstraintHole }) = return h
2207
2208 -- other wildcards should be simplified for printing
2209 -- we must do so here, and not in the error-message generation
2210 -- code, because we have all the givens already set up
2211 simpl_hole h@(Hole { hole_ty = ty, hole_loc = loc })
2212 = do { ty' <- rewriteType loc ty
2213 ; return (h { hole_ty = ty' }) }
2214
2215 {- Note [Delete dead Given evidence bindings]
2216 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2217 As a result of superclass expansion, we speculatively
2218 generate evidence bindings for Givens. E.g.
2219 f :: (a ~ b) => a -> b -> Bool
2220 f x y = ...
2221 We'll have
2222 [G] d1 :: (a~b)
2223 and we'll speculatively generate the evidence binding
2224 [G] d2 :: (a ~# b) = sc_sel d
2225
2226 Now d2 is available for solving. But it may not be needed! Usually
2227 such dead superclass selections will eventually be dropped as dead
2228 code, but:
2229
2230 * It won't always be dropped (#13032). In the case of an
2231 unlifted-equality superclass like d2 above, we generate
2232 case heq_sc d1 of d2 -> ...
2233 and we can't (in general) drop that case expression in case
2234 d1 is bottom. So it's technically unsound to have added it
2235 in the first place.
2236
2237 * Simply generating all those extra superclasses can generate lots of
2238 code that has to be zonked, only to be discarded later. Better not
2239 to generate it in the first place.
2240
2241 Moreover, if we simplify this implication more than once
2242 (e.g. because we can't solve it completely on the first iteration
2243 of simpl_looop), we'll generate all the same bindings AGAIN!
2244
2245 Easy solution: take advantage of the work we are doing to track dead
2246 (unused) Givens, and use it to prune the Given bindings too. This is
2247 all done by neededEvVars.
2248
2249 This led to a remarkable 25% overall compiler allocation decrease in
2250 test T12227.
2251
2252 But we don't get to discard all redundant equality superclasses, alas;
2253 see #15205.
2254
2255 Note [Do not simplify ConstraintHoles]
2256 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2257 Before printing the inferred value for a type hole (a _ wildcard in
2258 a partial type signature), we simplify it w.r.t. any Givens. This
2259 makes for an easier-to-understand diagnostic for the user.
2260
2261 However, we do not wish to do this for extra-constraint holes. Here is
2262 the example for why (partial-sigs/should_compile/T12844):
2263
2264 bar :: _ => FooData rngs
2265 bar = foo
2266
2267 data FooData rngs
2268
2269 class Foo xs where foo :: (Head xs ~ '(r,r')) => FooData xs
2270
2271 type family Head (xs :: [k]) where Head (x ': xs) = x
2272
2273 GHC correctly infers that the extra-constraints wildcard on `bar`
2274 should be (Head rngs ~ '(r, r'), Foo rngs). It then adds this
2275 constraint as a Given on the implication constraint for `bar`. (This
2276 implication is emitted by emitResidualConstraints.) The Hole for the _
2277 is stored within the implication's WantedConstraints. When
2278 simplifyHoles is called, that constraint is already assumed as a
2279 Given. Simplifying with respect to it turns it into ('(r, r') ~ '(r,
2280 r'), Foo rngs), which is disastrous.
2281
2282 Furthermore, there is no need to simplify here: extra-constraints wildcards
2283 are filled in with the output of the solver, in chooseInferredQuantifiers
2284 (choose_psig_context), so they are already simplified. (Contrast to normal
2285 type holes, which are just bound to a meta-variable.) Avoiding the poor output
2286 is simple: just don't simplify extra-constraints wildcards.
2287
2288 This is the only reason we need to track ConstraintHole separately
2289 from TypeHole in HoleSort.
2290
2291 See also Note [Extra-constraint holes in partial type signatures]
2292 in GHC.Tc.Gen.HsType.
2293
2294 Note [Tracking redundant constraints]
2295 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2296 With Opt_WarnRedundantConstraints, GHC can report which
2297 constraints of a type signature (or instance declaration) are
2298 redundant, and can be omitted. Here is an overview of how it
2299 works:
2300
2301 ----- What is a redundant constraint?
2302
2303 * The things that can be redundant are precisely the Given
2304 constraints of an implication.
2305
2306 * A constraint can be redundant in two different ways:
2307 a) It is implied by other givens. E.g.
2308 f :: (Eq a, Ord a) => blah -- Eq a unnecessary
2309 g :: (Eq a, a~b, Eq b) => blah -- Either Eq a or Eq b unnecessary
2310 b) It is not needed by the Wanted constraints covered by the
2311 implication E.g.
2312 f :: Eq a => a -> Bool
2313 f x = True -- Equality not used
2314
2315 * To find (a), when we have two Given constraints,
2316 we must be careful to drop the one that is a naked variable (if poss).
2317 So if we have
2318 f :: (Eq a, Ord a) => blah
2319 then we may find [G] sc_sel (d1::Ord a) :: Eq a
2320 [G] d2 :: Eq a
2321 We want to discard d2 in favour of the superclass selection from
2322 the Ord dictionary. This is done by GHC.Tc.Solver.Interact.solveOneFromTheOther
2323 See Note [Replacement vs keeping].
2324
2325 * To find (b) we need to know which evidence bindings are 'wanted';
2326 hence the eb_is_given field on an EvBind.
2327
2328 ----- How tracking works
2329
2330 * The ic_need fields of an Implic records in-scope (given) evidence
2331 variables bound by the context, that were needed to solve this
2332 implication (so far). See the declaration of Implication.
2333
2334 * When the constraint solver finishes solving all the wanteds in
2335 an implication, it sets its status to IC_Solved
2336
2337 - The ics_dead field, of IC_Solved, records the subset of this
2338 implication's ic_given that are redundant (not needed).
2339
2340 * We compute which evidence variables are needed by an implication
2341 in setImplicationStatus. A variable is needed if
2342 a) it is free in the RHS of a Wanted EvBind,
2343 b) it is free in the RHS of an EvBind whose LHS is needed,
2344 c) it is in the ics_need of a nested implication.
2345
2346 * We need to be careful not to discard an implication
2347 prematurely, even one that is fully solved, because we might
2348 thereby forget which variables it needs, and hence wrongly
2349 report a constraint as redundant. But we can discard it once
2350 its free vars have been incorporated into its parent; or if it
2351 simply has no free vars. This careful discarding is also
2352 handled in setImplicationStatus.
2353
2354 ----- Reporting redundant constraints
2355
2356 * GHC.Tc.Errors does the actual warning, in warnRedundantConstraints.
2357
2358 * We don't report redundant givens for *every* implication; only
2359 for those which reply True to GHC.Tc.Solver.warnRedundantGivens:
2360
2361 - For example, in a class declaration, the default method *can*
2362 use the class constraint, but it certainly doesn't *have* to,
2363 and we don't want to report an error there.
2364
2365 - More subtly, in a function definition
2366 f :: (Ord a, Ord a, Ix a) => a -> a
2367 f x = rhs
2368 we do an ambiguity check on the type (which would find that one
2369 of the Ord a constraints was redundant), and then we check that
2370 the definition has that type (which might find that both are
2371 redundant). We don't want to report the same error twice, so we
2372 disable it for the ambiguity check. Hence using two different
2373 FunSigCtxts, one with the warn-redundant field set True, and the
2374 other set False in
2375 - GHC.Tc.Gen.Bind.tcSpecPrag
2376 - GHC.Tc.Gen.Bind.tcTySig
2377
2378 This decision is taken in setImplicationStatus, rather than GHC.Tc.Errors
2379 so that we can discard implication constraints that we don't need.
2380 So ics_dead consists only of the *reportable* redundant givens.
2381
2382 ----- Shortcomings
2383
2384 Consider (see #9939)
2385 f2 :: (Eq a, Ord a) => a -> a -> Bool
2386 -- Ord a redundant, but Eq a is reported
2387 f2 x y = (x == y)
2388
2389 We report (Eq a) as redundant, whereas actually (Ord a) is. But it's
2390 really not easy to detect that!
2391
2392 -}
2393
2394 -- | Like 'defaultTyVar', but in the TcS monad.
2395 defaultTyVarTcS :: TcTyVar -> TcS Bool
2396 defaultTyVarTcS the_tv
2397 | isRuntimeRepVar the_tv
2398 , not (isTyVarTyVar the_tv)
2399 -- TyVarTvs should only be unified with a tyvar
2400 -- never with a type; c.f. GHC.Tc.Utils.TcMType.defaultTyVar
2401 -- and Note [Inferring kinds for type declarations] in GHC.Tc.TyCl
2402 = do { traceTcS "defaultTyVarTcS RuntimeRep" (ppr the_tv)
2403 ; unifyTyVar the_tv liftedRepTy
2404 ; return True }
2405 | isLevityVar the_tv
2406 , not (isTyVarTyVar the_tv)
2407 = do { traceTcS "defaultTyVarTcS Levity" (ppr the_tv)
2408 ; unifyTyVar the_tv liftedDataConTy
2409 ; return True }
2410 | isMultiplicityVar the_tv
2411 , not (isTyVarTyVar the_tv) -- TyVarTvs should only be unified with a tyvar
2412 -- never with a type; c.f. TcMType.defaultTyVar
2413 -- See Note [Kind generalisation and SigTvs]
2414 = do { traceTcS "defaultTyVarTcS Multiplicity" (ppr the_tv)
2415 ; unifyTyVar the_tv manyDataConTy
2416 ; return True }
2417 | otherwise
2418 = return False -- the common case
2419
2420 approximateWC :: Bool -> WantedConstraints -> Cts
2421 -- Postcondition: Wanted or Derived Cts
2422 -- See Note [ApproximateWC]
2423 -- See Note [floatKindEqualities vs approximateWC]
2424 approximateWC float_past_equalities wc
2425 = float_wc emptyVarSet wc
2426 where
2427 float_wc :: TcTyCoVarSet -> WantedConstraints -> Cts
2428 float_wc trapping_tvs (WC { wc_simple = simples, wc_impl = implics })
2429 = filterBag (is_floatable trapping_tvs) simples `unionBags`
2430 concatMapBag (float_implic trapping_tvs) implics
2431 float_implic :: TcTyCoVarSet -> Implication -> Cts
2432 float_implic trapping_tvs imp
2433 | float_past_equalities || ic_given_eqs imp /= MaybeGivenEqs
2434 = float_wc new_trapping_tvs (ic_wanted imp)
2435 | otherwise -- Take care with equalities
2436 = emptyCts -- See (1) under Note [ApproximateWC]
2437 where
2438 new_trapping_tvs = trapping_tvs `extendVarSetList` ic_skols imp
2439
2440 is_floatable skol_tvs ct
2441 | isGivenCt ct = False
2442 | insolubleEqCt ct = False
2443 | otherwise = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
2444
2445 {- Note [ApproximateWC]
2446 ~~~~~~~~~~~~~~~~~~~~~~~
2447 approximateWC takes a constraint, typically arising from the RHS of a
2448 let-binding whose type we are *inferring*, and extracts from it some
2449 *simple* constraints that we might plausibly abstract over. Of course
2450 the top-level simple constraints are plausible, but we also float constraints
2451 out from inside, if they are not captured by skolems.
2452
2453 The same function is used when doing type-class defaulting (see the call
2454 to applyDefaultingRules) to extract constraints that might be defaulted.
2455
2456 There is one caveat:
2457
2458 1. When inferring most-general types (in simplifyInfer), we do *not*
2459 float anything out if the implication binds equality constraints,
2460 because that defeats the OutsideIn story. Consider
2461 data T a where
2462 TInt :: T Int
2463 MkT :: T a
2464
2465 f TInt = 3::Int
2466
2467 We get the implication (a ~ Int => res ~ Int), where so far we've decided
2468 f :: T a -> res
2469 We don't want to float (res~Int) out because then we'll infer
2470 f :: T a -> Int
2471 which is only on of the possible types. (GHC 7.6 accidentally *did*
2472 float out of such implications, which meant it would happily infer
2473 non-principal types.)
2474
2475 HOWEVER (#12797) in findDefaultableGroups we are not worried about
2476 the most-general type; and we /do/ want to float out of equalities.
2477 Hence the boolean flag to approximateWC.
2478
2479 ------ Historical note -----------
2480 There used to be a second caveat, driven by #8155
2481
2482 2. We do not float out an inner constraint that shares a type variable
2483 (transitively) with one that is trapped by a skolem. Eg
2484 forall a. F a ~ beta, Integral beta
2485 We don't want to float out (Integral beta). Doing so would be bad
2486 when defaulting, because then we'll default beta:=Integer, and that
2487 makes the error message much worse; we'd get
2488 Can't solve F a ~ Integer
2489 rather than
2490 Can't solve Integral (F a)
2491
2492 Moreover, floating out these "contaminated" constraints doesn't help
2493 when generalising either. If we generalise over (Integral b), we still
2494 can't solve the retained implication (forall a. F a ~ b). Indeed,
2495 arguably that too would be a harder error to understand.
2496
2497 But this transitive closure stuff gives rise to a complex rule for
2498 when defaulting actually happens, and one that was never documented.
2499 Moreover (#12923), the more complex rule is sometimes NOT what
2500 you want. So I simply removed the extra code to implement the
2501 contamination stuff. There was zero effect on the testsuite (not even #8155).
2502 ------ End of historical note -----------
2503
2504
2505 Note [DefaultTyVar]
2506 ~~~~~~~~~~~~~~~~~~~
2507 defaultTyVar is used on any un-instantiated meta type variables to
2508 default any RuntimeRep variables to LiftedRep. This is important
2509 to ensure that instance declarations match. For example consider
2510
2511 instance Show (a->b)
2512 foo x = show (\_ -> True)
2513
2514 Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
2515 and that won't match the tcTypeKind (*) in the instance decl. See tests
2516 tc217 and tc175.
2517
2518 We look only at touchable type variables. No further constraints
2519 are going to affect these type variables, so it's time to do it by
2520 hand. However we aren't ready to default them fully to () or
2521 whatever, because the type-class defaulting rules have yet to run.
2522
2523 An alternate implementation would be to emit a derived constraint setting
2524 the RuntimeRep variable to LiftedRep, but this seems unnecessarily indirect.
2525
2526 Note [Promote _and_ default when inferring]
2527 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2528 When we are inferring a type, we simplify the constraint, and then use
2529 approximateWC to produce a list of candidate constraints. Then we MUST
2530
2531 a) Promote any meta-tyvars that have been floated out by
2532 approximateWC, to restore invariant (WantedInv) described in
2533 Note [TcLevel invariants] in GHC.Tc.Utils.TcType.
2534
2535 b) Default the kind of any meta-tyvars that are not mentioned in
2536 in the environment.
2537
2538 To see (b), suppose the constraint is (C ((a :: OpenKind) -> Int)), and we
2539 have an instance (C ((x:*) -> Int)). The instance doesn't match -- but it
2540 should! If we don't solve the constraint, we'll stupidly quantify over
2541 (C (a->Int)) and, worse, in doing so skolemiseQuantifiedTyVar will quantify over
2542 (b:*) instead of (a:OpenKind), which can lead to disaster; see #7332.
2543 #7641 is a simpler example.
2544
2545 Note [Promoting unification variables]
2546 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2547 When we float an equality out of an implication we must "promote" free
2548 unification variables of the equality, in order to maintain Invariant
2549 (WantedInv) from Note [TcLevel invariants] in GHC.Tc.Types.TcType.
2550
2551 This is absolutely necessary. Consider the following example. We start
2552 with two implications and a class with a functional dependency.
2553
2554 class C x y | x -> y
2555 instance C [a] [a]
2556
2557 (I1) [untch=beta]forall b. 0 => F Int ~ [beta]
2558 (I2) [untch=beta]forall c. 0 => F Int ~ [[alpha]] /\ C beta [c]
2559
2560 We float (F Int ~ [beta]) out of I1, and we float (F Int ~ [[alpha]]) out of I2.
2561 They may react to yield that (beta := [alpha]) which can then be pushed inwards
2562 the leftover of I2 to get (C [alpha] [a]) which, using the FunDep, will mean that
2563 (alpha := a). In the end we will have the skolem 'b' escaping in the untouchable
2564 beta! Concrete example is in indexed_types/should_fail/ExtraTcsUntch.hs:
2565
2566 class C x y | x -> y where
2567 op :: x -> y -> ()
2568
2569 instance C [a] [a]
2570
2571 type family F a :: *
2572
2573 h :: F Int -> ()
2574 h = undefined
2575
2576 data TEx where
2577 TEx :: a -> TEx
2578
2579 f (x::beta) =
2580 let g1 :: forall b. b -> ()
2581 g1 _ = h [x]
2582 g2 z = case z of TEx y -> (h [[undefined]], op x [y])
2583 in (g1 '3', g2 undefined)
2584
2585
2586 *********************************************************************************
2587 * *
2588 * Defaulting and disambiguation *
2589 * *
2590 *********************************************************************************
2591 -}
2592
2593 applyDefaultingRules :: WantedConstraints -> TcS Bool
2594 -- True <=> I did some defaulting, by unifying a meta-tyvar
2595 -- Input WantedConstraints are not necessarily zonked
2596
2597 applyDefaultingRules wanteds
2598 | isEmptyWC wanteds
2599 = return False
2600 | otherwise
2601 = do { info@(default_tys, _) <- getDefaultInfo
2602 ; wanteds <- TcS.zonkWC wanteds
2603
2604 ; tcg_env <- TcS.getGblEnv
2605 ; let plugins = tcg_defaulting_plugins tcg_env
2606
2607 ; plugin_defaulted <- if null plugins then return [] else
2608 do {
2609 ; traceTcS "defaultingPlugins {" (ppr wanteds)
2610 ; defaultedGroups <- mapM (run_defaulting_plugin wanteds) plugins
2611 ; traceTcS "defaultingPlugins }" (ppr defaultedGroups)
2612 ; return defaultedGroups
2613 }
2614
2615 ; let groups = findDefaultableGroups info wanteds
2616
2617 ; traceTcS "applyDefaultingRules {" $
2618 vcat [ text "wanteds =" <+> ppr wanteds
2619 , text "groups =" <+> ppr groups
2620 , text "info =" <+> ppr info ]
2621
2622 ; something_happeneds <- mapM (disambigGroup default_tys) groups
2623
2624 ; traceTcS "applyDefaultingRules }" (ppr something_happeneds)
2625
2626 ; return $ or something_happeneds || or plugin_defaulted }
2627 where run_defaulting_plugin wanteds p =
2628 do { groups <- runTcPluginTcS (p wanteds)
2629 ; defaultedGroups <-
2630 filterM (\g -> disambigGroup
2631 (deProposalCandidates g)
2632 (deProposalTyVar g, deProposalCts g))
2633 groups
2634 ; traceTcS "defaultingPlugin " $ ppr defaultedGroups
2635 ; case defaultedGroups of
2636 [] -> return False
2637 _ -> return True
2638 }
2639
2640
2641 findDefaultableGroups
2642 :: ( [Type]
2643 , (Bool,Bool) ) -- (Overloaded strings, extended default rules)
2644 -> WantedConstraints -- Unsolved (wanted or derived)
2645 -> [(TyVar, [Ct])]
2646 findDefaultableGroups (default_tys, (ovl_strings, extended_defaults)) wanteds
2647 | null default_tys
2648 = []
2649 | otherwise
2650 = [ (tv, map fstOf3 group)
2651 | group'@((_,_,tv) :| _) <- unary_groups
2652 , let group = toList group'
2653 , defaultable_tyvar tv
2654 , defaultable_classes (map sndOf3 group) ]
2655 where
2656 simples = approximateWC True wanteds
2657 (unaries, non_unaries) = partitionWith find_unary (bagToList simples)
2658 unary_groups = equivClasses cmp_tv unaries
2659
2660 unary_groups :: [NonEmpty (Ct, Class, TcTyVar)] -- (C tv) constraints
2661 unaries :: [(Ct, Class, TcTyVar)] -- (C tv) constraints
2662 non_unaries :: [Ct] -- and *other* constraints
2663
2664 -- Finds unary type-class constraints
2665 -- But take account of polykinded classes like Typeable,
2666 -- which may look like (Typeable * (a:*)) (#8931)
2667 find_unary :: Ct -> Either (Ct, Class, TyVar) Ct
2668 find_unary cc
2669 | Just (cls,tys) <- getClassPredTys_maybe (ctPred cc)
2670 , [ty] <- filterOutInvisibleTypes (classTyCon cls) tys
2671 -- Ignore invisible arguments for this purpose
2672 , Just tv <- tcGetTyVar_maybe ty
2673 , isMetaTyVar tv -- We might have runtime-skolems in GHCi, and
2674 -- we definitely don't want to try to assign to those!
2675 = Left (cc, cls, tv)
2676 find_unary cc = Right cc -- Non unary or non dictionary
2677
2678 bad_tvs :: TcTyCoVarSet -- TyVars mentioned by non-unaries
2679 bad_tvs = mapUnionVarSet tyCoVarsOfCt non_unaries
2680
2681 cmp_tv (_,_,tv1) (_,_,tv2) = tv1 `compare` tv2
2682
2683 defaultable_tyvar :: TcTyVar -> Bool
2684 defaultable_tyvar tv
2685 = let b1 = isTyConableTyVar tv -- Note [Avoiding spurious errors]
2686 b2 = not (tv `elemVarSet` bad_tvs)
2687 in b1 && (b2 || extended_defaults) -- Note [Multi-parameter defaults]
2688
2689 defaultable_classes :: [Class] -> Bool
2690 defaultable_classes clss
2691 | extended_defaults = any (isInteractiveClass ovl_strings) clss
2692 | otherwise = all is_std_class clss && (any (isNumClass ovl_strings) clss)
2693
2694 -- is_std_class adds IsString to the standard numeric classes,
2695 -- when -foverloaded-strings is enabled
2696 is_std_class cls = isStandardClass cls ||
2697 (ovl_strings && (cls `hasKey` isStringClassKey))
2698
2699 ------------------------------
2700 disambigGroup :: [Type] -- The default types
2701 -> (TcTyVar, [Ct]) -- All constraints sharing same type variable
2702 -> TcS Bool -- True <=> something happened, reflected in ty_binds
2703
2704 disambigGroup [] _
2705 = return False
2706 disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
2707 = do { traceTcS "disambigGroup {" (vcat [ ppr default_ty, ppr the_tv, ppr wanteds ])
2708 ; fake_ev_binds_var <- TcS.newTcEvBinds
2709 ; tclvl <- TcS.getTcLevel
2710 ; success <- nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) try_group
2711
2712 ; if success then
2713 -- Success: record the type variable binding, and return
2714 do { unifyTyVar the_tv default_ty
2715 ; wrapWarnTcS $ warnDefaulting the_tv wanteds default_ty
2716 ; traceTcS "disambigGroup succeeded }" (ppr default_ty)
2717 ; return True }
2718 else
2719 -- Failure: try with the next type
2720 do { traceTcS "disambigGroup failed, will try other default types }"
2721 (ppr default_ty)
2722 ; disambigGroup default_tys group } }
2723 where
2724 try_group
2725 | Just subst <- mb_subst
2726 = do { lcl_env <- TcS.getLclEnv
2727 ; tc_lvl <- TcS.getTcLevel
2728 ; let loc = mkGivenLoc tc_lvl UnkSkol lcl_env
2729 -- Equality constraints are possible due to type defaulting plugins
2730 ; wanted_evs <- mapM (newWantedNC loc . substTy subst . ctPred)
2731 wanteds
2732 ; fmap isEmptyWC $
2733 solveSimpleWanteds $ listToBag $
2734 map mkNonCanonical wanted_evs }
2735
2736 | otherwise
2737 = return False
2738
2739 the_ty = mkTyVarTy the_tv
2740 mb_subst = tcMatchTyKi the_ty default_ty
2741 -- Make sure the kinds match too; hence this call to tcMatchTyKi
2742 -- E.g. suppose the only constraint was (Typeable k (a::k))
2743 -- With the addition of polykinded defaulting we also want to reject
2744 -- ill-kinded defaulting attempts like (Eq []) or (Foldable Int) here.
2745
2746 -- In interactive mode, or with -XExtendedDefaultRules,
2747 -- we default Show a to Show () to avoid graututious errors on "show []"
2748 isInteractiveClass :: Bool -- -XOverloadedStrings?
2749 -> Class -> Bool
2750 isInteractiveClass ovl_strings cls
2751 = isNumClass ovl_strings cls || (classKey cls `elem` interactiveClassKeys)
2752
2753 -- isNumClass adds IsString to the standard numeric classes,
2754 -- when -foverloaded-strings is enabled
2755 isNumClass :: Bool -- -XOverloadedStrings?
2756 -> Class -> Bool
2757 isNumClass ovl_strings cls
2758 = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
2759
2760
2761 {-
2762 Note [Avoiding spurious errors]
2763 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2764 When doing the unification for defaulting, we check for skolem
2765 type variables, and simply don't default them. For example:
2766 f = (*) -- Monomorphic
2767 g :: Num a => a -> a
2768 g x = f x x
2769 Here, we get a complaint when checking the type signature for g,
2770 that g isn't polymorphic enough; but then we get another one when
2771 dealing with the (Num a) context arising from f's definition;
2772 we try to unify a with Int (to default it), but find that it's
2773 already been unified with the rigid variable from g's type sig.
2774
2775 Note [Multi-parameter defaults]
2776 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2777 With -XExtendedDefaultRules, we default only based on single-variable
2778 constraints, but do not exclude from defaulting any type variables which also
2779 appear in multi-variable constraints. This means that the following will
2780 default properly:
2781
2782 default (Integer, Double)
2783
2784 class A b (c :: Symbol) where
2785 a :: b -> Proxy c
2786
2787 instance A Integer c where a _ = Proxy
2788
2789 main = print (a 5 :: Proxy "5")
2790
2791 Note that if we change the above instance ("instance A Integer") to
2792 "instance A Double", we get an error:
2793
2794 No instance for (A Integer "5")
2795
2796 This is because the first defaulted type (Integer) has successfully satisfied
2797 its single-parameter constraints (in this case Num).
2798 -}