Flat constraint --> Simple constraint
[ghc.git] / compiler / typecheck / TcInteract.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcInteract (
4 solveSimpleGivens, -- Solves [EvVar],GivenLoc
5 solveSimpleWanteds -- Solves Cts
6 ) where
7
8 #include "HsVersions.h"
9
10 import BasicTypes ()
11 import TcCanonical
12 import TcFlatten
13 import VarSet
14 import Type
15 import Unify
16 import InstEnv( lookupInstEnv, instanceDFunId )
17 import CoAxiom(sfInteractTop, sfInteractInert)
18
19 import Var
20 import TcType
21 import PrelNames (knownNatClassName, knownSymbolClassName, ipClassNameKey )
22 import Id( idType )
23 import Class
24 import TyCon
25 import FunDeps
26 import FamInst
27 import Inst( tyVarsOfCt )
28
29 import TcEvidence
30 import Outputable
31
32 import TcRnTypes
33 import TcErrors
34 import TcSMonad
35 import Bag
36
37 import Data.List( partition, foldl', deleteFirstsBy )
38
39 import VarEnv
40
41 import Control.Monad
42 import Pair (Pair(..))
43 import Unique( hasKey )
44 import FastString ( sLit )
45 import DynFlags
46 import Util
47
48 {-
49 **********************************************************************
50 * *
51 * Main Interaction Solver *
52 * *
53 **********************************************************************
54
55 Note [Basic Simplifier Plan]
56 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
57 1. Pick an element from the WorkList if there exists one with depth
58 less than our context-stack depth.
59
60 2. Run it down the 'stage' pipeline. Stages are:
61 - canonicalization
62 - inert reactions
63 - spontaneous reactions
64 - top-level intreactions
65 Each stage returns a StopOrContinue and may have sideffected
66 the inerts or worklist.
67
68 The threading of the stages is as follows:
69 - If (Stop) is returned by a stage then we start again from Step 1.
70 - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
71 the next stage in the pipeline.
72 4. If the element has survived (i.e. ContinueWith x) the last stage
73 then we add him in the inerts and jump back to Step 1.
74
75 If in Step 1 no such element exists, we have exceeded our context-stack
76 depth and will simply fail.
77
78 Note [Unflatten after solving the simple wanteds]
79 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
80 We unflatten after solving the wc_simples of an implication, and before attempting
81 to float. This means that
82
83 * The fsk/fmv flatten-skolems only survive during solveSimples. We don't
84 need to worry about then across successive passes over the constraint tree.
85 (E.g. we don't need the old ic_fsk field of an implication.
86
87 * When floating an equality outwards, we don't need to worry about floating its
88 associated flattening constraints.
89
90 * Another tricky case becomes easy: Trac #4935
91 type instance F True a b = a
92 type instance F False a b = b
93
94 [w] F c a b ~ gamma
95 (c ~ True) => a ~ gamma
96 (c ~ False) => b ~ gamma
97
98 Obviously this is soluble with gamma := F c a b, and unflattening
99 will do exactly that after solving the simple constraints and before
100 attempting the implications. Before, when we were not unflattening,
101 we had to push Wanted funeqs in as new givens. Yuk!
102
103 Another example that becomes easy: indexed_types/should_fail/T7786
104 [W] BuriedUnder sub k Empty ~ fsk
105 [W] Intersect fsk inv ~ s
106 [w] xxx[1] ~ s
107 [W] forall[2] . (xxx[1] ~ Empty)
108 => Intersect (BuriedUnder sub k Empty) inv ~ Empty
109
110 Note [Running plugins on unflattened wanteds]
111 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
112
113 There is an annoying mismatch between solveSimpleGivens and
114 solveSimpleWanteds, because the latter needs to fiddle with the inert
115 set, unflatten and and zonk the wanteds. It passes the zonked wanteds
116 to runTcPluginsWanteds, which produces a replacement set of wanteds,
117 some additional insolubles and a flag indicating whether to go round
118 the loop again. If so, prepareInertsForImplications is used to remove
119 the previous wanteds (which will still be in the inert set). Note
120 that prepareInertsForImplications will discard the insolubles, so we
121 must keep track of them separately.
122 -}
123
124 solveSimpleGivens :: CtLoc -> [EvVar] -> TcS ()
125 solveSimpleGivens loc givens
126 | null givens -- Shortcut for common case
127 = return ()
128 | otherwise
129 = go (map mk_given_ct givens)
130 where
131 mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evtm = EvId ev_id
132 , ctev_pred = evVarPred ev_id
133 , ctev_loc = loc })
134 go givens = do { solveSimples (listToBag givens)
135 ; new_givens <- runTcPluginsGiven
136 ; when (notNull new_givens) (go new_givens)
137 }
138
139 solveSimpleWanteds :: Cts -> TcS WantedConstraints
140 solveSimpleWanteds = go emptyBag
141 where
142 go insols0 wanteds
143 = do { solveSimples wanteds
144 ; (implics, tv_eqs, fun_eqs, insols, others) <- getUnsolvedInerts
145 ; unflattened_eqs <- unflatten tv_eqs fun_eqs
146 -- See Note [Unflatten after solving the simple wanteds]
147
148 ; zonked <- zonkSimples (others `andCts` unflattened_eqs)
149 -- Postcondition is that the wl_simples are zonked
150
151 ; (wanteds', insols', rerun) <- runTcPluginsWanted zonked
152 -- See Note [Running plugins on unflattened wanteds]
153 ; let all_insols = insols0 `unionBags` insols `unionBags` insols'
154 ; if rerun then do { updInertTcS prepareInertsForImplications
155 ; go all_insols wanteds' }
156 else return (WC { wc_simple = wanteds'
157 , wc_insol = all_insols
158 , wc_impl = implics }) }
159
160
161 -- The main solver loop implements Note [Basic Simplifier Plan]
162 ---------------------------------------------------------------
163 solveSimples :: Cts -> TcS ()
164 -- Returns the final InertSet in TcS
165 -- Has no effect on work-list or residual-iplications
166 -- The constraints are initially examined in left-to-right order
167
168 solveSimples cts
169 = {-# SCC "solveSimples" #-}
170 do { dyn_flags <- getDynFlags
171 ; updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
172 ; solve_loop (maxSubGoalDepth dyn_flags) }
173 where
174 solve_loop max_depth
175 = {-# SCC "solve_loop" #-}
176 do { sel <- selectNextWorkItem max_depth
177 ; case sel of
178 NoWorkRemaining -- Done, successfuly (modulo frozen)
179 -> return ()
180 MaxDepthExceeded cnt ct -- Failure, depth exceeded
181 -> wrapErrTcS $ solverDepthErrorTcS cnt (ctEvidence ct)
182 NextWorkItem ct -- More work, loop around!
183 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
184
185
186 -- | Extract the (inert) givens and invoke the plugins on them.
187 -- Remove solved givens from the inert set and emit insolubles, but
188 -- return new work produced so that 'solveSimpleGivens' can feed it back
189 -- into the main solver.
190 runTcPluginsGiven :: TcS [Ct]
191 runTcPluginsGiven = do
192 (givens,_,_) <- fmap splitInertCans getInertCans
193 if null givens
194 then return []
195 else do
196 p <- runTcPlugins (givens,[],[])
197 let (solved_givens, _, _) = pluginSolvedCts p
198 updInertCans (removeInertCts solved_givens)
199 mapM_ emitInsoluble (pluginBadCts p)
200 return (pluginNewCts p)
201
202 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
203 -- them and produce an updated bag of wanteds (possibly with some new
204 -- work) and a bag of insolubles. The boolean indicates whether
205 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
206 -- main solver.
207 runTcPluginsWanted :: Cts -> TcS (Cts, Cts, Bool)
208 runTcPluginsWanted zonked_wanteds
209 | isEmptyBag zonked_wanteds = return (zonked_wanteds, emptyBag, False)
210 | otherwise = do
211 (given,derived,_) <- fmap splitInertCans getInertCans
212 p <- runTcPlugins (given, derived, bagToList zonked_wanteds)
213 let (solved_givens, solved_deriveds, solved_wanteds) = pluginSolvedCts p
214 (_, _, wanteds) = pluginInputCts p
215 updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
216 mapM_ setEv solved_wanteds
217 return ( listToBag $ pluginNewCts p ++ wanteds
218 , listToBag $ pluginBadCts p
219 , notNull (pluginNewCts p) )
220 where
221 setEv :: (EvTerm,Ct) -> TcS ()
222 setEv (ev,ct) = case ctEvidence ct of
223 CtWanted {ctev_evar = evar} -> setEvBind evar ev
224 _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
225
226 -- | A triple of (given, derived, wanted) constraints to pass to plugins
227 type SplitCts = ([Ct], [Ct], [Ct])
228
229 -- | A solved triple of constraints, with evidence for wanteds
230 type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])
231
232 -- | Represents collections of constraints generated by typechecker
233 -- plugins
234 data TcPluginProgress = TcPluginProgress
235 { pluginInputCts :: SplitCts
236 -- ^ Original inputs to the plugins with solved/bad constraints
237 -- removed, but otherwise unmodified
238 , pluginSolvedCts :: SolvedCts
239 -- ^ Constraints solved by plugins
240 , pluginBadCts :: [Ct]
241 -- ^ Constraints reported as insoluble by plugins
242 , pluginNewCts :: [Ct]
243 -- ^ New constraints emitted by plugins
244 }
245
246 -- | Starting from a triple of (given, derived, wanted) constraints,
247 -- invoke each of the typechecker plugins in turn and return
248 --
249 -- * the remaining unmodified constraints,
250 -- * constraints that have been solved,
251 -- * constraints that are insoluble, and
252 -- * new work.
253 --
254 -- Note that new work generated by one plugin will not be seen by
255 -- other plugins on this pass (but the main constraint solver will be
256 -- re-invoked and they will see it later). There is no check that new
257 -- work differs from the original constraints supplied to the plugin:
258 -- the plugin itself should perform this check if necessary.
259 runTcPlugins :: SplitCts -> TcS TcPluginProgress
260 runTcPlugins all_cts = do
261 gblEnv <- getGblEnv
262 foldM do_plugin initialProgress (tcg_tc_plugins gblEnv)
263 where
264 do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
265 do_plugin p solver = do
266 result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
267 return $ progress p result
268
269 progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
270 progress p (TcPluginContradiction bad_cts) =
271 p { pluginInputCts = discard bad_cts (pluginInputCts p)
272 , pluginBadCts = bad_cts ++ pluginBadCts p
273 }
274 progress p (TcPluginOk solved_cts new_cts) =
275 p { pluginInputCts = discard (map snd solved_cts) (pluginInputCts p)
276 , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
277 , pluginNewCts = new_cts ++ pluginNewCts p
278 }
279
280 initialProgress = TcPluginProgress all_cts ([], [], []) [] []
281
282 discard :: [Ct] -> SplitCts -> SplitCts
283 discard cts (xs, ys, zs) =
284 (xs `without` cts, ys `without` cts, zs `without` cts)
285
286 without :: [Ct] -> [Ct] -> [Ct]
287 without = deleteFirstsBy eqCt
288
289 eqCt :: Ct -> Ct -> Bool
290 eqCt c c' = case (ctEvidence c, ctEvidence c') of
291 (CtGiven pred _ _, CtGiven pred' _ _) -> pred `eqType` pred'
292 (CtWanted pred _ _, CtWanted pred' _ _) -> pred `eqType` pred'
293 (CtDerived pred _ , CtDerived pred' _ ) -> pred `eqType` pred'
294 (_ , _ ) -> False
295
296 add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
297 add xs scs = foldl' addOne scs xs
298
299 addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
300 addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
301 CtGiven {} -> (ct:givens, deriveds, wanteds)
302 CtDerived{} -> (givens, ct:deriveds, wanteds)
303 CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)
304
305
306 type WorkItem = Ct
307 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
308
309 data SelectWorkItem
310 = NoWorkRemaining -- No more work left (effectively we're done!)
311 | MaxDepthExceeded SubGoalCounter Ct
312 -- More work left to do but this constraint has exceeded
313 -- the maximum depth for one of the subgoal counters and we
314 -- must stop
315 | NextWorkItem Ct -- More work left, here's the next item to look at
316
317 selectNextWorkItem :: SubGoalDepth -- Max depth allowed
318 -> TcS SelectWorkItem
319 selectNextWorkItem max_depth
320 = updWorkListTcS_return pick_next
321 where
322 pick_next :: WorkList -> (SelectWorkItem, WorkList)
323 pick_next wl
324 = case selectWorkItem wl of
325 (Nothing,_)
326 -> (NoWorkRemaining,wl) -- No more work
327 (Just ct, new_wl)
328 | Just cnt <- subGoalDepthExceeded max_depth (ctLocDepth (ctLoc ct)) -- Depth exceeded
329 -> (MaxDepthExceeded cnt ct,new_wl)
330 (Just ct, new_wl)
331 -> (NextWorkItem ct, new_wl) -- New workitem and worklist
332
333 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
334 -> WorkItem -- The work item
335 -> TcS ()
336 -- Run this item down the pipeline, leaving behind new work and inerts
337 runSolverPipeline pipeline workItem
338 = do { initial_is <- getTcSInerts
339 ; traceTcS "Start solver pipeline {" $
340 vcat [ ptext (sLit "work item = ") <+> ppr workItem
341 , ptext (sLit "inerts = ") <+> ppr initial_is]
342
343 ; bumpStepCountTcS -- One step for each constraint processed
344 ; final_res <- run_pipeline pipeline (ContinueWith workItem)
345
346 ; final_is <- getTcSInerts
347 ; case final_res of
348 Stop ev s -> do { traceFireTcS ev s
349 ; traceTcS "End solver pipeline (discharged) }"
350 (ptext (sLit "inerts =") <+> ppr final_is)
351 ; return () }
352 ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
353 ; traceTcS "End solver pipeline (not discharged) }" $
354 vcat [ ptext (sLit "final_item =") <+> ppr ct
355 , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
356 , ptext (sLit "inerts =") <+> ppr final_is]
357 ; insertInertItemTcS ct }
358 }
359 where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
360 -> TcS (StopOrContinue Ct)
361 run_pipeline [] res = return res
362 run_pipeline _ (Stop ev s) = return (Stop ev s)
363 run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
364 = do { traceTcS ("runStage " ++ stg_name ++ " {")
365 (text "workitem = " <+> ppr ct)
366 ; res <- stg ct
367 ; traceTcS ("end stage " ++ stg_name ++ " }") empty
368 ; run_pipeline stgs res }
369
370 {-
371 Example 1:
372 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
373 Reagent: a ~ [b] (given)
374
375 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
376 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
377 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
378
379 Example 2:
380 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
381 Reagent: a ~w [b]
382
383 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
384 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
385 etc.
386
387 Example 3:
388 Inert: {a ~ Int, F Int ~ b} (given)
389 Reagent: F a ~ b (wanted)
390
391 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
392 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
393 -}
394
395 thePipeline :: [(String,SimplifierStage)]
396 thePipeline = [ ("canonicalization", TcCanonical.canonicalize)
397 , ("interact with inerts", interactWithInertsStage)
398 , ("top-level reactions", topReactionsStage) ]
399
400 {-
401 *********************************************************************************
402 * *
403 The interact-with-inert Stage
404 * *
405 *********************************************************************************
406
407 Note [The Solver Invariant]
408 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
409 We always add Givens first. So you might think that the solver has
410 the invariant
411
412 If the work-item is Given,
413 then the inert item must Given
414
415 But this isn't quite true. Suppose we have,
416 c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
417 After processing the first two, we get
418 c1: [G] beta ~ [alpha], c2 : [W] blah
419 Now, c3 does not interact with the the given c1, so when we spontaneously
420 solve c3, we must re-react it with the inert set. So we can attempt a
421 reaction between inert c2 [W] and work-item c3 [G].
422
423 It *is* true that [Solver Invariant]
424 If the work-item is Given,
425 AND there is a reaction
426 then the inert item must Given
427 or, equivalently,
428 If the work-item is Given,
429 and the inert item is Wanted/Derived
430 then there is no reaction
431 -}
432
433 -- Interaction result of WorkItem <~> Ct
434
435 type StopNowFlag = Bool -- True <=> stop after this interaction
436
437 interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
438 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
439 -- react with anything at this stage.
440
441 interactWithInertsStage wi
442 = do { inerts <- getTcSInerts
443 ; let ics = inert_cans inerts
444 ; case wi of
445 CTyEqCan {} -> interactTyVarEq ics wi
446 CFunEqCan {} -> interactFunEq ics wi
447 CIrredEvCan {} -> interactIrred ics wi
448 CDictCan {} -> interactDict ics wi
449 _ -> pprPanic "interactWithInerts" (ppr wi) }
450 -- CHoleCan are put straight into inert_frozen, so never get here
451 -- CNonCanonical have been canonicalised
452
453 data InteractResult = IRKeep | IRReplace | IRDelete
454 instance Outputable InteractResult where
455 ppr IRKeep = ptext (sLit "keep")
456 ppr IRReplace = ptext (sLit "replace")
457 ppr IRDelete = ptext (sLit "delete")
458
459 solveOneFromTheOther :: CtEvidence -- Inert
460 -> CtEvidence -- WorkItem
461 -> TcS (InteractResult, StopNowFlag)
462 -- Preconditions:
463 -- 1) inert and work item represent evidence for the /same/ predicate
464 -- 2) ip/class/irred evidence (no coercions) only
465 solveOneFromTheOther ev_i ev_w
466 | isDerived ev_w
467 = return (IRKeep, True)
468
469 | isDerived ev_i -- The inert item is Derived, we can just throw it away,
470 -- The ev_w is inert wrt earlier inert-set items,
471 -- so it's safe to continue on from this point
472 = return (IRDelete, False)
473
474 | CtWanted { ctev_evar = ev_id } <- ev_w
475 = do { setEvBind ev_id (ctEvTerm ev_i)
476 ; return (IRKeep, True) }
477
478 | CtWanted { ctev_evar = ev_id } <- ev_i
479 = do { setEvBind ev_id (ctEvTerm ev_w)
480 ; return (IRReplace, True) }
481
482 | otherwise -- If both are Given, we already have evidence; no need to duplicate
483 -- But the work item *overrides* the inert item (hence IRReplace)
484 -- See Note [Shadowing of Implicit Parameters]
485 = return (IRReplace, True)
486
487 {-
488 *********************************************************************************
489 * *
490 interactIrred
491 * *
492 *********************************************************************************
493 -}
494
495 -- Two pieces of irreducible evidence: if their types are *exactly identical*
496 -- we can rewrite them. We can never improve using this:
497 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
498 -- mean that (ty1 ~ ty2)
499 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
500
501 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
502 | let pred = ctEvPred ev_w
503 (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
504 (inert_irreds inerts)
505 , (ct_i : rest) <- bagToList matching_irreds
506 , let ctev_i = ctEvidence ct_i
507 = ASSERT( null rest )
508 do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
509 ; case inert_effect of
510 IRKeep -> return ()
511 IRDelete -> updInertIrreds (\_ -> others)
512 IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
513 -- These const upd's assume that solveOneFromTheOther
514 -- has no side effects on InertCans
515 ; if stop_now then
516 return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
517 ; else
518 continueWith workItem }
519
520 | otherwise
521 = continueWith workItem
522
523 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
524
525 {-
526 *********************************************************************************
527 * *
528 interactDict
529 * *
530 *********************************************************************************
531 -}
532
533 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
534 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
535 | Just ctev_i <- lookupInertDict inerts (ctEvLoc ev_w) cls tys
536 = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
537 ; case inert_effect of
538 IRKeep -> return ()
539 IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
540 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
541 ; if stop_now then
542 return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
543 else
544 continueWith workItem }
545
546 | cls `hasKey` ipClassNameKey
547 , isGiven ev_w
548 = interactGivenIP inerts workItem
549
550 | otherwise
551 = do { mapBagM_ (addFunDepWork workItem) (findDictsByClass (inert_dicts inerts) cls)
552 -- Standard thing: create derived fds and keep on going. Importantly we don't
553 -- throw workitem back in the worklist because this can cause loops (see #5236)
554 ; continueWith workItem }
555
556 interactDict _ wi = pprPanic "interactDict" (ppr wi)
557
558 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
559 -- Work item is Given (?x:ty)
560 -- See Note [Shadowing of Implicit Parameters]
561 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
562 , cc_tyargs = tys@(ip_str:_) })
563 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
564 ; stopWith ev "Given IP" }
565 where
566 dicts = inert_dicts inerts
567 ip_dicts = findDictsByClass dicts cls
568 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
569 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
570
571 -- Pick out any Given constraints for the same implicit parameter
572 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
573 = isGiven ev && ip_str `tcEqType` ip_str'
574 is_this_ip _ = False
575
576 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
577
578 addFunDepWork :: Ct -> Ct -> TcS ()
579 addFunDepWork work_ct inert_ct
580 = do { let fd_eqns :: [Equation CtLoc]
581 fd_eqns = [ eqn { fd_loc = derived_loc }
582 | eqn <- improveFromAnother inert_pred work_pred ]
583 ; rewriteWithFunDeps fd_eqns
584 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
585 -- NB: We do create FDs for given to report insoluble equations that arise
586 -- from pairs of Givens, and also because of floating when we approximate
587 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
588 -- Also see Note [When improvement happens]
589 }
590 where
591 work_pred = ctPred work_ct
592 inert_pred = ctPred inert_ct
593 work_loc = ctLoc work_ct
594 inert_loc = ctLoc inert_ct
595 derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc
596 inert_pred inert_loc }
597
598 {-
599 Note [Shadowing of Implicit Parameters]
600 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
601 Consider the following example:
602
603 f :: (?x :: Char) => Char
604 f = let ?x = 'a' in ?x
605
606 The "let ?x = ..." generates an implication constraint of the form:
607
608 ?x :: Char => ?x :: Char
609
610 Furthermore, the signature for `f` also generates an implication
611 constraint, so we end up with the following nested implication:
612
613 ?x :: Char => (?x :: Char => ?x :: Char)
614
615 Note that the wanted (?x :: Char) constraint may be solved in
616 two incompatible ways: either by using the parameter from the
617 signature, or by using the local definition. Our intention is
618 that the local definition should "shadow" the parameter of the
619 signature, and we implement this as follows: when we add a new
620 *given* implicit parameter to the inert set, it replaces any existing
621 givens for the same implicit parameter.
622
623 This works for the normal cases but it has an odd side effect
624 in some pathological programs like this:
625
626 -- This is accepted, the second parameter shadows
627 f1 :: (?x :: Int, ?x :: Char) => Char
628 f1 = ?x
629
630 -- This is rejected, the second parameter shadows
631 f2 :: (?x :: Int, ?x :: Char) => Int
632 f2 = ?x
633
634 Both of these are actually wrong: when we try to use either one,
635 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
636 which would lead to an error.
637
638 I can think of two ways to fix this:
639
640 1. Simply disallow multiple constratits for the same implicit
641 parameter---this is never useful, and it can be detected completely
642 syntactically.
643
644 2. Move the shadowing machinery to the location where we nest
645 implications, and add some code here that will produce an
646 error if we get multiple givens for the same implicit parameter.
647
648
649 *********************************************************************************
650 * *
651 interactFunEq
652 * *
653 *********************************************************************************
654 -}
655
656 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
657 -- Try interacting the work item with the inert set
658 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
659 , cc_tyargs = args, cc_fsk = fsk })
660 | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
661 = if ev_i `canRewriteOrSame` ev
662 then -- Rewrite work-item using inert
663 do { traceTcS "reactFunEq (discharge work item):" $
664 vcat [ text "workItem =" <+> ppr workItem
665 , text "inertItem=" <+> ppr ev_i ]
666 ; reactFunEq ev_i fsk_i ev fsk
667 ; stopWith ev "Inert rewrites work item" }
668 else -- Rewrite intert using work-item
669 do { traceTcS "reactFunEq (rewrite inert item):" $
670 vcat [ text "workItem =" <+> ppr workItem
671 , text "inertItem=" <+> ppr ev_i ]
672 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
673 -- Do the updInertFunEqs before the reactFunEq, so that
674 -- we don't kick out the inertItem as well as consuming it!
675 ; reactFunEq ev fsk ev_i fsk_i
676 ; stopWith ev "Work item rewrites inert" }
677
678 | Just ops <- isBuiltInSynFamTyCon_maybe tc
679 = do { let matching_funeqs = findFunEqsByTyCon funeqs tc
680 ; let interact = sfInteractInert ops args (lookupFlattenTyVar eqs fsk)
681 do_one (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = iev })
682 = mapM_ (unifyDerived (ctEvLoc iev) Nominal)
683 (interact iargs (lookupFlattenTyVar eqs ifsk))
684 do_one ct = pprPanic "interactFunEq" (ppr ct)
685 ; mapM_ do_one matching_funeqs
686 ; traceTcS "builtInCandidates 1: " $ vcat [ ptext (sLit "Candidates:") <+> ppr matching_funeqs
687 , ptext (sLit "TvEqs:") <+> ppr eqs ]
688 ; return (ContinueWith workItem) }
689
690 | otherwise
691 = return (ContinueWith workItem)
692 where
693 eqs = inert_eqs inerts
694 funeqs = inert_funeqs inerts
695 matching_inerts = findFunEqs funeqs tc args
696
697 interactFunEq _ wi = pprPanic "interactFunEq" (ppr wi)
698
699 lookupFlattenTyVar :: TyVarEnv EqualCtList -> TcTyVar -> TcType
700 -- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
701 -- this is used only when dealing with a CFunEqCan
702 lookupFlattenTyVar inert_eqs ftv
703 = case lookupVarEnv inert_eqs ftv of
704 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq } : _) -> rhs
705 _ -> mkTyVarTy ftv
706
707 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1
708 -> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2
709 -> TcS ()
710 reactFunEq from_this fsk1 (CtGiven { ctev_evtm = tm, ctev_loc = loc }) fsk2
711 = do { let fsk_eq_co = mkTcSymCo (evTermCoercion tm)
712 `mkTcTransCo` ctEvCoercion from_this
713 -- :: fsk2 ~ fsk1
714 fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
715 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
716 ; emitWorkNC [new_ev] }
717
718 reactFunEq from_this fuv1 (CtWanted { ctev_evar = evar }) fuv2
719 = dischargeFmv evar fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
720
721 reactFunEq _ _ solve_this@(CtDerived {}) _
722 = pprPanic "reactFunEq" (ppr solve_this)
723
724 {-
725 Note [Cache-caused loops]
726 ~~~~~~~~~~~~~~~~~~~~~~~~~
727 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
728 solved cache (which is the default behaviour or xCtEvidence), because the interaction
729 may not be contributing towards a solution. Here is an example:
730
731 Initial inert set:
732 [W] g1 : F a ~ beta1
733 Work item:
734 [W] g2 : F a ~ beta2
735 The work item will react with the inert yielding the _same_ inert set plus:
736 i) Will set g2 := g1 `cast` g3
737 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
738 iii) Will emit [W] g3 : beta1 ~ beta2
739 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
740 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
741 will set
742 g1 := g ; sym g3
743 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
744 remember that we have this in our solved cache, and it is ... g2! In short we
745 created the evidence loop:
746
747 g2 := g1 ; g3
748 g3 := refl
749 g1 := g2 ; sym g3
750
751 To avoid this situation we do not cache as solved any workitems (or inert)
752 which did not really made a 'step' towards proving some goal. Solved's are
753 just an optimization so we don't lose anything in terms of completeness of
754 solving.
755
756
757 Note [Efficient Orientation]
758 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
759 Suppose we are interacting two FunEqCans with the same LHS:
760 (inert) ci :: (F ty ~ xi_i)
761 (work) cw :: (F ty ~ xi_w)
762 We prefer to keep the inert (else we pass the work item on down
763 the pipeline, which is a bit silly). If we keep the inert, we
764 will (a) discharge 'cw'
765 (b) produce a new equality work-item (xi_w ~ xi_i)
766 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
767 new_work :: xi_w ~ xi_i
768 cw := ci ; sym new_work
769 Why? Consider the simplest case when xi1 is a type variable. If
770 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
771 If we generate xi2~xi1, there is less chance of that happening.
772 Of course it can and should still happen if xi1=a, xi1=Int, say.
773 But we want to avoid it happening needlessly.
774
775 Similarly, if we *can't* keep the inert item (because inert is Wanted,
776 and work is Given, say), we prefer to orient the new equality (xi_i ~
777 xi_w).
778
779 Note [Carefully solve the right CFunEqCan]
780 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
781 ---- OLD COMMENT, NOW NOT NEEDED
782 ---- because we now allow multiple
783 ---- wanted FunEqs with the same head
784 Consider the constraints
785 c1 :: F Int ~ a -- Arising from an application line 5
786 c2 :: F Int ~ Bool -- Arising from an application line 10
787 Suppose that 'a' is a unification variable, arising only from
788 flattening. So there is no error on line 5; it's just a flattening
789 variable. But there is (or might be) an error on line 10.
790
791 Two ways to combine them, leaving either (Plan A)
792 c1 :: F Int ~ a -- Arising from an application line 5
793 c3 :: a ~ Bool -- Arising from an application line 10
794 or (Plan B)
795 c2 :: F Int ~ Bool -- Arising from an application line 10
796 c4 :: a ~ Bool -- Arising from an application line 5
797
798 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
799 on the *totally innocent* line 5. An example is test SimpleFail16
800 where the expected/actual message comes out backwards if we use
801 the wrong plan.
802
803 The second is the right thing to do. Hence the isMetaTyVarTy
804 test when solving pairwise CFunEqCan.
805
806
807 *********************************************************************************
808 * *
809 interactTyVarEq
810 * *
811 *********************************************************************************
812 -}
813
814 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
815 -- CTyEqCans are always consumed, so always returns Stop
816 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
817 , cc_rhs = rhs
818 , cc_ev = ev
819 , cc_eq_rel = eq_rel })
820 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
821 <- findTyEqs inerts tv
822 , ev_i `canRewriteOrSame` ev
823 , rhs_i `tcEqType` rhs ]
824 = -- Inert: a ~ b
825 -- Work item: a ~ b
826 do { when (isWanted ev) $
827 setEvBind (ctev_evar ev) (ctEvTerm ev_i)
828 ; stopWith ev "Solved from inert" }
829
830 | Just tv_rhs <- getTyVar_maybe rhs
831 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
832 <- findTyEqs inerts tv_rhs
833 , ev_i `canRewriteOrSame` ev
834 , rhs_i `tcEqType` mkTyVarTy tv ]
835 = -- Inert: a ~ b
836 -- Work item: b ~ a
837 do { when (isWanted ev) $
838 setEvBind (ctev_evar ev)
839 (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
840 ; stopWith ev "Solved from inert (r)" }
841
842 | otherwise
843 = do { tclvl <- getTcLevel
844 ; if canSolveByUnification tclvl ev eq_rel tv rhs
845 then do { solveByUnification ev tv rhs
846 ; n_kicked <- kickOutRewritable Given NomEq tv
847 -- Given because the tv := xi is given
848 -- NomEq because only nom. equalities are solved
849 -- by unification
850 ; return (Stop ev (ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked)) }
851
852 else do { traceTcS "Can't solve tyvar equality"
853 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
854 , ppWhen (isMetaTyVar tv) $
855 nest 4 (text "TcLevel of" <+> ppr tv
856 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
857 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
858 , text "TcLevel =" <+> ppr tclvl ])
859 ; n_kicked <- kickOutRewritable (ctEvFlavour ev)
860 (ctEvEqRel ev)
861 tv
862 ; updInertCans (\ ics -> addInertCan ics workItem)
863 ; return (Stop ev (ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked)) } }
864
865 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
866
867 -- @trySpontaneousSolve wi@ solves equalities where one side is a
868 -- touchable unification variable.
869 -- Returns True <=> spontaneous solve happened
870 canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
871 -> TcTyVar -> Xi -> Bool
872 canSolveByUnification tclvl gw eq_rel tv xi
873 | ReprEq <- eq_rel -- we never solve representational equalities this way.
874 = False
875
876 | isGiven gw -- See Note [Touchables and givens]
877 = False
878
879 | isTouchableMetaTyVar tclvl tv
880 = case metaTyVarInfo tv of
881 SigTv -> is_tyvar xi
882 _ -> True
883
884 | otherwise -- Untouchable
885 = False
886 where
887 is_tyvar xi
888 = case tcGetTyVar_maybe xi of
889 Nothing -> False
890 Just tv -> case tcTyVarDetails tv of
891 MetaTv { mtv_info = info }
892 -> case info of
893 SigTv -> True
894 _ -> False
895 SkolemTv {} -> True
896 FlatSkol {} -> False
897 RuntimeUnk -> True
898
899 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
900 -- Solve with the identity coercion
901 -- Precondition: kind(xi) is a sub-kind of kind(tv)
902 -- Precondition: CtEvidence is Wanted or Derived
903 -- Precondition: CtEvidence is nominal
904 -- See [New Wanted Superclass Work] to see why solveByUnification
905 -- must work for Derived as well as Wanted
906 -- Returns: workItem where
907 -- workItem = the new Given constraint
908 --
909 -- NB: No need for an occurs check here, because solveByUnification always
910 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
911 -- say that in (a ~ xi), the type variable a does not appear in xi.
912 -- See TcRnTypes.Ct invariants.
913 --
914 -- Post: tv is unified (by side effect) with xi;
915 -- we often write tv := xi
916 solveByUnification wd tv xi
917 = do { let tv_ty = mkTyVarTy tv
918 ; traceTcS "Sneaky unification:" $
919 vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
920 text "Coercion:" <+> pprEq tv_ty xi,
921 text "Left Kind is:" <+> ppr (typeKind tv_ty),
922 text "Right Kind is:" <+> ppr (typeKind xi) ]
923
924 ; let xi' = defaultKind xi
925 -- We only instantiate kind unification variables
926 -- with simple kinds like *, not OpenKind or ArgKind
927 -- cf TcUnify.uUnboundKVar
928
929 ; setWantedTyBind tv xi'
930 ; when (isWanted wd) $
931 setEvBind (ctEvId wd) (EvCoercion (mkTcNomReflCo xi')) }
932
933
934 ppr_kicked :: Int -> SDoc
935 ppr_kicked 0 = empty
936 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
937
938 kickOutRewritable :: CtFlavour -- Flavour of the equality that is
939 -- being added to the inert set
940 -> EqRel -- of the new equality
941 -> TcTyVar -- The new equality is tv ~ ty
942 -> TcS Int
943 kickOutRewritable new_flavour new_eq_rel new_tv
944 | not ((new_flavour, new_eq_rel) `eqCanRewriteFR` (new_flavour, new_eq_rel))
945 = return 0 -- If new_flavour can't rewrite itself, it can't rewrite
946 -- anything else, so no need to kick out anything
947 -- This is a common case: wanteds can't rewrite wanteds
948
949 | otherwise
950 = do { ics <- getInertCans
951 ; let (kicked_out, ics') = kick_out new_flavour new_eq_rel new_tv ics
952 ; setInertCans ics'
953 ; updWorkListTcS (appendWorkList kicked_out)
954
955 ; unless (isEmptyWorkList kicked_out) $
956 csTraceTcS $
957 hang (ptext (sLit "Kick out, tv =") <+> ppr new_tv)
958 2 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
959 , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
960 , ppr kicked_out ])
961 ; return (workListSize kicked_out) }
962
963 kick_out :: CtFlavour -> EqRel -> TcTyVar -> InertCans -> (WorkList, InertCans)
964 kick_out new_flavour new_eq_rel new_tv (IC { inert_eqs = tv_eqs
965 , inert_dicts = dictmap
966 , inert_funeqs = funeqmap
967 , inert_irreds = irreds
968 , inert_insols = insols })
969 = (kicked_out, inert_cans_in)
970 where
971 -- NB: Notice that don't rewrite
972 -- inert_solved_dicts, and inert_solved_funeqs
973 -- optimistically. But when we lookup we have to
974 -- take the substitution into account
975 inert_cans_in = IC { inert_eqs = tv_eqs_in
976 , inert_dicts = dicts_in
977 , inert_funeqs = feqs_in
978 , inert_irreds = irs_in
979 , inert_insols = insols_in }
980
981 kicked_out = WL { wl_eqs = tv_eqs_out
982 , wl_funeqs = feqs_out
983 , wl_rest = bagToList (dicts_out `andCts` irs_out
984 `andCts` insols_out)
985 , wl_implics = emptyBag }
986
987 (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
988 (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
989 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
990 (irs_out, irs_in) = partitionBag kick_out_irred irreds
991 (insols_out, insols_in) = partitionBag kick_out_ct insols
992 -- Kick out even insolubles; see Note [Kick out insolubles]
993
994 can_rewrite :: CtEvidence -> Bool
995 can_rewrite = ((new_flavour, new_eq_rel) `eqCanRewriteFR`) . ctEvFlavourRole
996
997 kick_out_ct :: Ct -> Bool
998 kick_out_ct ct = kick_out_ctev (ctEvidence ct)
999
1000 kick_out_ctev :: CtEvidence -> Bool
1001 kick_out_ctev ev = can_rewrite ev
1002 && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
1003 -- See Note [Kicking out inert constraints]
1004
1005 kick_out_irred :: Ct -> Bool
1006 kick_out_irred ct = can_rewrite (cc_ev ct)
1007 && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
1008 -- See Note [Kicking out Irreds]
1009
1010 kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
1011 -> ([Ct], TyVarEnv EqualCtList)
1012 kick_out_eqs eqs (acc_out, acc_in)
1013 = (eqs_out ++ acc_out, case eqs_in of
1014 [] -> acc_in
1015 (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
1016 where
1017 (eqs_in, eqs_out) = partition keep_eq eqs
1018
1019 -- implements criteria K1-K3 in Note [The inert equalities] in TcFlatten
1020 keep_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev
1021 , cc_eq_rel = eq_rel })
1022 | tv == new_tv
1023 = not (can_rewrite ev) -- (K1)
1024
1025 | otherwise
1026 = check_k2 && check_k3
1027 where
1028 check_k2 = not (ev `eqCanRewrite` ev)
1029 || not (can_rewrite ev)
1030 || not (new_tv `elemVarSet` tyVarsOfType rhs_ty)
1031
1032 check_k3
1033 | can_rewrite ev
1034 = case eq_rel of
1035 NomEq -> not (rhs_ty `eqType` mkTyVarTy new_tv)
1036 ReprEq -> isTyVarExposed new_tv rhs_ty
1037
1038 | otherwise
1039 = True
1040
1041 keep_eq ct = pprPanic "keep_eq" (ppr ct)
1042
1043 {-
1044 Note [Kicking out inert constraints]
1045 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1046 Given a new (a -> ty) inert, we want to kick out an existing inert
1047 constraint if
1048 a) the new constraint can rewrite the inert one
1049 b) 'a' is free in the inert constraint (so that it *will*)
1050 rewrite it if we kick it out.
1051
1052 For (b) we use tyVarsOfCt, which returns the type variables /and
1053 the kind variables/ that are directly visible in the type. Hence we
1054 will have exposed all the rewriting we care about to make the most
1055 precise kinds visible for matching classes etc. No need to kick out
1056 constraints that mention type variables whose kinds contain this
1057 variable! (Except see Note [Kicking out Irreds].)
1058
1059 Note [Kicking out Irreds]
1060 ~~~~~~~~~~~~~~~~~~~~~~~~~
1061 There is an awkward special case for Irreds. When we have a
1062 kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
1063 an Irred (see Note [Equalities with incompatible kinds] in
1064 TcCanonical). So in this case the free kind variables of k1 and k2
1065 are not visible. More precisely, the type looks like
1066 (~) k1 (a:k1) (ty:k2)
1067 because (~) has kind forall k. k -> k -> Constraint. So the constraint
1068 itself is ill-kinded. We can "see" k1 but not k2. That's why we use
1069 closeOverKinds to make sure we see k2.
1070
1071 This is not pretty. Maybe (~) should have kind
1072 (~) :: forall k1 k1. k1 -> k2 -> Constraint
1073
1074 Note [Kick out insolubles]
1075 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1076 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1077 because an occurs check. And then we unify alpha := [Int].
1078 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
1079 Now it can be decomposed. Otherwise we end up with a "Can't match
1080 [Int] ~ [[Int]]" which is true, but a bit confusing because the
1081 outer type constructors match.
1082
1083
1084 Note [Avoid double unifications]
1085 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1086 The spontaneous solver has to return a given which mentions the unified unification
1087 variable *on the left* of the equality. Here is what happens if not:
1088 Original wanted: (a ~ alpha), (alpha ~ Int)
1089 We spontaneously solve the first wanted, without changing the order!
1090 given : a ~ alpha [having unified alpha := a]
1091 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1092 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1093
1094 We avoid this problem by orienting the resulting given so that the unification
1095 variable is on the left. [Note that alternatively we could attempt to
1096 enforce this at canonicalization]
1097
1098 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1099 double unifications is the main reason we disallow touchable
1100 unification variables as RHS of type family equations: F xis ~ alpha.
1101
1102
1103
1104 Note [Superclasses and recursive dictionaries]
1105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1106 Overlaps with Note [SUPERCLASS-LOOP 1]
1107 Note [SUPERCLASS-LOOP 2]
1108 Note [Recursive instances and superclases]
1109 ToDo: check overlap and delete redundant stuff
1110
1111 Right before adding a given into the inert set, we must
1112 produce some more work, that will bring the superclasses
1113 of the given into scope. The superclass constraints go into
1114 our worklist.
1115
1116 When we simplify a wanted constraint, if we first see a matching
1117 instance, we may produce new wanted work. To (1) avoid doing this work
1118 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1119 this item as given into our inert set WITHOUT adding its superclass constraints,
1120 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
1121 for doing the isGoodRecEv check in an older version of the type checker].
1122
1123 But now we have added partially solved constraints to the worklist which may
1124 interact with other wanteds. Consider the example:
1125
1126 Example 1:
1127
1128 class Eq b => Foo a b --- 0-th selector
1129 instance Eq a => Foo [a] a --- fooDFun
1130
1131 and wanted (Foo [t] t). We are first going to see that the instance matches
1132 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1133 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1134 Our work list is going to contain a new *wanted* goal
1135 d3 :_w Eq t
1136
1137 Ok, so how do we get recursive dictionaries, at all:
1138
1139 Example 2:
1140
1141 data D r = ZeroD | SuccD (r (D r));
1142
1143 instance (Eq (r (D r))) => Eq (D r) where
1144 ZeroD == ZeroD = True
1145 (SuccD a) == (SuccD b) = a == b
1146 _ == _ = False;
1147
1148 equalDC :: D [] -> D [] -> Bool;
1149 equalDC = (==);
1150
1151 We need to prove (Eq (D [])). Here's how we go:
1152
1153 d1 :_w Eq (D [])
1154
1155 by instance decl, holds if
1156 d2 :_w Eq [D []]
1157 where d1 = dfEqD d2
1158
1159 *BUT* we have an inert set which gives us (no superclasses):
1160 d1 :_g Eq (D [])
1161 By the instance declaration of Eq we can show the 'd2' goal if
1162 d3 :_w Eq (D [])
1163 where d2 = dfEqList d3
1164 d1 = dfEqD d2
1165 Now, however this wanted can interact with our inert d1 to set:
1166 d3 := d1
1167 and solve the goal. Why was this interaction OK? Because, if we chase the
1168 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1169 are really setting
1170 d3 := dfEqD2 (dfEqList d3)
1171 which is FINE because the use of d3 is protected by the instance function
1172 applications.
1173
1174 So, our strategy is to try to put solved wanted dictionaries into the
1175 inert set along with their superclasses (when this is meaningful,
1176 i.e. when new wanted goals are generated) but solve a wanted dictionary
1177 from a given only in the case where the evidence variable of the
1178 wanted is mentioned in the evidence of the given (recursively through
1179 the evidence binds) in a protected way: more instance function applications
1180 than superclass selectors.
1181
1182 Here are some more examples from GHC's previous type checker
1183
1184
1185 Example 3:
1186 This code arises in the context of "Scrap Your Boilerplate with Class"
1187
1188 class Sat a
1189 class Data ctx a
1190 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1191 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1192
1193 class Data Maybe a => Foo a
1194
1195 instance Foo t => Sat (Maybe t) -- dfunSat
1196
1197 instance Data Maybe a => Foo a -- dfunFoo1
1198 instance Foo a => Foo [a] -- dfunFoo2
1199 instance Foo [Char] -- dfunFoo3
1200
1201 Consider generating the superclasses of the instance declaration
1202 instance Foo a => Foo [a]
1203
1204 So our problem is this
1205 [G] d0 : Foo t
1206 [W] d1 : Data Maybe [t] -- Desired superclass
1207
1208 We may add the given in the inert set, along with its superclasses
1209 [assuming we don't fail because there is a matching instance, see
1210 topReactionsStage, given case ]
1211 Inert:
1212 [G] d0 : Foo t
1213 [G] d01 : Data Maybe t -- Superclass of d0
1214 WorkList
1215 [W] d1 : Data Maybe [t]
1216
1217 Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
1218 Inert:
1219 [G] d0 : Foo t
1220 [G] d01 : Data Maybe t -- Superclass of d0
1221 Solved:
1222 d1 : Data Maybe [t]
1223 WorkList
1224 [W] d2 : Sat (Maybe [t])
1225 [W] d3 : Data Maybe t
1226
1227 Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
1228 Inert:
1229 [G] d0 : Foo t
1230 [G] d01 : Data Maybe t -- Superclass of d0
1231 Solved:
1232 d1 : Data Maybe [t]
1233 d2 : Sat (Maybe [t])
1234 WorkList:
1235 [W] d3 : Data Maybe t
1236 [W] d4 : Foo [t]
1237
1238 Now, we can just solve d3 from d01; d3 := d01
1239 Inert
1240 [G] d0 : Foo t
1241 [G] d01 : Data Maybe t -- Superclass of d0
1242 Solved:
1243 d1 : Data Maybe [t]
1244 d2 : Sat (Maybe [t])
1245 WorkList
1246 [W] d4 : Foo [t]
1247
1248 Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5
1249 Inert
1250 [G] d0 : Foo t
1251 [G] d01 : Data Maybe t -- Superclass of d0
1252 Solved:
1253 d1 : Data Maybe [t]
1254 d2 : Sat (Maybe [t])
1255 d4 : Foo [t]
1256 WorkList:
1257 [W] d5 : Foo t
1258
1259 Now, d5 can be solved! d5 := d0
1260
1261 Result
1262 d1 := dfunData2 d2 d3
1263 d2 := dfunSat d4
1264 d3 := d01
1265 d4 := dfunFoo2 d5
1266 d5 := d0
1267
1268 d0 :_g Foo t
1269 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1270 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1271 d4 :_g Foo [t] d4 := dfunFoo2 d5
1272 d5 :_g Foo t d5 := dfunFoo1 d7
1273 WorkList:
1274 d7 :_w Data Maybe t
1275 d6 :_g Data Maybe [t]
1276 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1277 d01 :_g Data Maybe t
1278
1279 Now, two problems:
1280 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1281 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1282 that must not be used (look at case interactInert where both inert and workitem
1283 are givens). So we have several options:
1284 - Drop the workitem always (this will drop d8)
1285 This feels very unsafe -- what if the work item was the "good" one
1286 that should be used later to solve another wanted?
1287 - Don't drop anyone: the inert set may contain multiple givens!
1288 [This is currently implemented]
1289
1290 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1291 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1292 d7. Now the [isRecDictEv] function in the ineration solver
1293 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1294 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1295
1296 So, no interaction happens there. Then we meet d01 and there is no recursion
1297 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1298
1299 Note [SUPERCLASS-LOOP 1]
1300 ~~~~~~~~~~~~~~~~~~~~~~~~
1301 We have to be very, very careful when generating superclasses, lest we
1302 accidentally build a loop. Here's an example:
1303
1304 class S a
1305
1306 class S a => C a where { opc :: a -> a }
1307 class S b => D b where { opd :: b -> b }
1308
1309 instance C Int where
1310 opc = opd
1311
1312 instance D Int where
1313 opd = opc
1314
1315 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1316 Simplifying, we may well get:
1317 $dfCInt = :C ds1 (opd dd)
1318 dd = $dfDInt
1319 ds1 = $p1 dd
1320 Notice that we spot that we can extract ds1 from dd.
1321
1322 Alas! Alack! We can do the same for (instance D Int):
1323
1324 $dfDInt = :D ds2 (opc dc)
1325 dc = $dfCInt
1326 ds2 = $p1 dc
1327
1328 And now we've defined the superclass in terms of itself.
1329 Two more nasty cases are in
1330 tcrun021
1331 tcrun033
1332
1333 Solution:
1334 - Satisfy the superclass context *all by itself*
1335 (tcSimplifySuperClasses)
1336 - And do so completely; i.e. no left-over constraints
1337 to mix with the constraints arising from method declarations
1338
1339
1340 Note [SUPERCLASS-LOOP 2]
1341 ~~~~~~~~~~~~~~~~~~~~~~~~
1342 We need to be careful when adding "the constaint we are trying to prove".
1343 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1344
1345 class Ord a => C a where
1346 instance Ord [a] => C [a] where ...
1347
1348 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1349 superclasses of C [a] to avails. But we must not overwrite the binding
1350 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1351 build a loop!
1352
1353 Here's another variant, immortalised in tcrun020
1354 class Monad m => C1 m
1355 class C1 m => C2 m x
1356 instance C2 Maybe Bool
1357 For the instance decl we need to build (C1 Maybe), and it's no good if
1358 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1359 before we search for C1 Maybe.
1360
1361 Here's another example
1362 class Eq b => Foo a b
1363 instance Eq a => Foo [a] a
1364 If we are reducing
1365 (Foo [t] t)
1366
1367 we'll first deduce that it holds (via the instance decl). We must not
1368 then overwrite the Eq t constraint with a superclass selection!
1369
1370 At first I had a gross hack, whereby I simply did not add superclass constraints
1371 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1372 because it lost legitimate superclass sharing, and it still didn't do the job:
1373 I found a very obscure program (now tcrun021) in which improvement meant the
1374 simplifier got two bites a the cherry... so something seemed to be an Stop
1375 first time, but reducible next time.
1376
1377 Now we implement the Right Solution, which is to check for loops directly
1378 when adding superclasses. It's a bit like the occurs check in unification.
1379
1380 Note [Recursive instances and superclases]
1381 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1382 Consider this code, which arises in the context of "Scrap Your
1383 Boilerplate with Class".
1384
1385 class Sat a
1386 class Data ctx a
1387 instance Sat (ctx Char) => Data ctx Char
1388 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1389
1390 class Data Maybe a => Foo a
1391
1392 instance Foo t => Sat (Maybe t)
1393
1394 instance Data Maybe a => Foo a
1395 instance Foo a => Foo [a]
1396 instance Foo [Char]
1397
1398 In the instance for Foo [a], when generating evidence for the superclasses
1399 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1400 Using the instance for Data, we therefore need
1401 (Sat (Maybe [a], Data Maybe a)
1402 But we are given (Foo a), and hence its superclass (Data Maybe a).
1403 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1404 we need (Foo [a]). And that is the very dictionary we are bulding
1405 an instance for! So we must put that in the "givens". So in this
1406 case we have
1407 Given: Foo a, Foo [a]
1408 Wanted: Data Maybe [a]
1409
1410 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1411 the givens, which is what 'addGiven' would normally do. Why? Because
1412 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1413 by selecting a superclass from Foo [a], which simply makes a loop.
1414
1415 On the other hand we *must* put the superclasses of (Foo a) in
1416 the givens, as you can see from the derivation described above.
1417
1418 Conclusion: in the very special case of tcSimplifySuperClasses
1419 we have one 'given' (namely the "this" dictionary) whose superclasses
1420 must not be added to 'givens' by addGiven.
1421
1422 There is a complication though. Suppose there are equalities
1423 instance (Eq a, a~b) => Num (a,b)
1424 Then we normalise the 'givens' wrt the equalities, so the original
1425 given "this" dictionary is cast to one of a different type. So it's a
1426 bit trickier than before to identify the "special" dictionary whose
1427 superclasses must not be added. See test
1428 indexed-types/should_run/EqInInstance
1429
1430 We need a persistent property of the dictionary to record this
1431 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1432 but cool), which is maintained by dictionary normalisation.
1433 Specifically, the InstLocOrigin is
1434 NoScOrigin
1435 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1436 with InstLocOrigin!
1437
1438
1439 ************************************************************************
1440 * *
1441 * Functional dependencies, instantiation of equations
1442 * *
1443 ************************************************************************
1444
1445 When we spot an equality arising from a functional dependency,
1446 we now use that equality (a "wanted") to rewrite the work-item
1447 constraint right away. This avoids two dangers
1448
1449 Danger 1: If we send the original constraint on down the pipeline
1450 it may react with an instance declaration, and in delicate
1451 situations (when a Given overlaps with an instance) that
1452 may produce new insoluble goals: see Trac #4952
1453
1454 Danger 2: If we don't rewrite the constraint, it may re-react
1455 with the same thing later, and produce the same equality
1456 again --> termination worries.
1457
1458 To achieve this required some refactoring of FunDeps.lhs (nicer
1459 now!).
1460 -}
1461
1462 rewriteWithFunDeps :: [Equation CtLoc] -> TcS ()
1463 -- NB: The returned constraints are all Derived
1464 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1465 rewriteWithFunDeps eqn_pred_locs
1466 = mapM_ instFunDepEqn eqn_pred_locs
1467
1468 instFunDepEqn :: Equation CtLoc -> TcS ()
1469 -- Post: Returns the position index as well as the corresponding FunDep equality
1470 instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1471 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1472 ; mapM_ (do_one subst) eqs }
1473 where
1474 do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
1475 = unifyDerived loc Nominal $
1476 Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
1477
1478 {-
1479 *********************************************************************************
1480 * *
1481 The top-reaction Stage
1482 * *
1483 *********************************************************************************
1484 -}
1485
1486 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1487 topReactionsStage wi
1488 = do { inerts <- getTcSInerts
1489 ; tir <- doTopReact inerts wi
1490 ; case tir of
1491 ContinueWith wi -> return (ContinueWith wi)
1492 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1493
1494 doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
1495 -- The work item does not react with the inert set, so try interaction with top-level
1496 -- instances. Note:
1497 --
1498 -- (a) The place to add superclasses in not here in doTopReact stage.
1499 -- Instead superclasses are added in the worklist as part of the
1500 -- canonicalization process. See Note [Adding superclasses].
1501 --
1502 -- (b) See Note [Given constraint that matches an instance declaration]
1503 -- for some design decisions for given dictionaries.
1504
1505 doTopReact inerts work_item
1506 = do { traceTcS "doTopReact" (ppr work_item)
1507 ; case work_item of
1508 CDictCan {} -> doTopReactDict inerts work_item
1509 CFunEqCan {} -> doTopReactFunEq work_item
1510 _ -> -- Any other work item does not react with any top-level equations
1511 return (ContinueWith work_item) }
1512
1513 --------------------
1514 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1515 -- Try to use type-class instance declarations to simplify the constraint
1516 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1517 , cc_tyargs = xis })
1518 | not (isWanted fl) -- Never use instances for Given or Derived constraints
1519 = try_fundeps_and_return
1520
1521 | Just ev <- lookupSolvedDict inerts loc cls xis -- Cached
1522 = do { setEvBind dict_id (ctEvTerm ev);
1523 ; stopWith fl "Dict/Top (cached)" }
1524
1525 | otherwise -- Not cached
1526 = do { lkup_inst_res <- matchClassInst inerts cls xis loc
1527 ; case lkup_inst_res of
1528 GenInst wtvs ev_term -> do { addSolvedDict fl cls xis
1529 ; solve_from_instance wtvs ev_term }
1530 NoInstance -> try_fundeps_and_return }
1531 where
1532 dict_id = ASSERT( isWanted fl ) ctEvId fl
1533 pred = mkClassPred cls xis
1534 loc = ctEvLoc fl
1535
1536 solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
1537 -- Precondition: evidence term matches the predicate workItem
1538 solve_from_instance evs ev_term
1539 | null evs
1540 = do { traceTcS "doTopReact/found nullary instance for" $
1541 ppr dict_id
1542 ; setEvBind dict_id ev_term
1543 ; stopWith fl "Dict/Top (solved, no new work)" }
1544 | otherwise
1545 = do { traceTcS "doTopReact/found non-nullary instance for" $
1546 ppr dict_id
1547 ; setEvBind dict_id ev_term
1548 ; let mk_new_wanted ev
1549 = mkNonCanonical (ev {ctev_loc = bumpCtLocDepth CountConstraints loc })
1550 ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1551 ; stopWith fl "Dict/Top (solved, more work)" }
1552
1553 -- We didn't solve it; so try functional dependencies with
1554 -- the instance environment, and return
1555 -- NB: even if there *are* some functional dependencies against the
1556 -- instance environment, there might be a unique match, and if
1557 -- so we make sure we get on and solve it first. See Note [Weird fundeps]
1558 try_fundeps_and_return
1559 = do { instEnvs <- getInstEnvs
1560 ; let fd_eqns :: [Equation CtLoc]
1561 fd_eqns = [ fd { fd_loc = loc { ctl_origin = FunDepOrigin2 pred (ctl_origin loc)
1562 inst_pred inst_loc } }
1563 | fd@(FDEqn { fd_loc = inst_loc, fd_pred1 = inst_pred })
1564 <- improveFromInstEnv instEnvs pred ]
1565 ; rewriteWithFunDeps fd_eqns
1566 ; continueWith work_item }
1567
1568 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1569
1570 --------------------
1571 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1572 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1573 , cc_tyargs = args , cc_fsk = fsk })
1574 = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families
1575 -- have reached this far
1576 ASSERT( not (isDerived old_ev) ) -- CFunEqCan is never Derived
1577 -- Look up in top-level instances, or built-in axiom
1578 do { match_res <- matchFam fam_tc args -- See Note [MATCHING-SYNONYMS]
1579 ; case match_res of {
1580 Nothing -> do { try_improvement; continueWith work_item } ;
1581 Just (ax_co, rhs_ty)
1582
1583 -- Found a top-level instance
1584
1585 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1586 , isTypeFamilyTyCon tc
1587 , tc_args `lengthIs` tyConArity tc -- Short-cut
1588 -> shortCutReduction old_ev fsk ax_co tc tc_args
1589 -- Try shortcut; see Note [Short cut for top-level reaction]
1590
1591 | isGiven old_ev -- Not shortcut
1592 -> do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1593 -- final_co :: fsk ~ rhs_ty
1594 ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
1595 EvCoercion final_co)
1596 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1597 ; stopWith old_ev "Fun/Top (given)" }
1598
1599 | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
1600 -> do { dischargeFmv (ctEvId old_ev) fsk ax_co rhs_ty
1601 ; traceTcS "doTopReactFunEq" $
1602 vcat [ text "old_ev:" <+> ppr old_ev
1603 , nest 2 (text ":=") <+> ppr ax_co ]
1604 ; stopWith old_ev "Fun/Top (wanted)" }
1605
1606 | otherwise -- We must not assign ufsk := ...ufsk...!
1607 -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1608 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
1609 ; emitWorkNC [new_ev]
1610 -- By emitting this as non-canonical, we deal with all
1611 -- flattening, occurs-check, and ufsk := ufsk issues
1612 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1613 -- ax_co :: fam_tc args ~ rhs_ty
1614 -- ev :: alpha ~ rhs_ty
1615 -- ufsk := alpha
1616 -- final_co :: fam_tc args ~ alpha
1617 ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty
1618 ; traceTcS "doTopReactFunEq (occurs)" $
1619 vcat [ text "old_ev:" <+> ppr old_ev
1620 , nest 2 (text ":=") <+> ppr final_co
1621 , text "new_ev:" <+> ppr new_ev ]
1622 ; stopWith old_ev "Fun/Top (wanted)" } } }
1623 where
1624 loc = ctEvLoc old_ev
1625 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1626
1627 try_improvement
1628 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1629 = do { inert_eqs <- getInertEqs
1630 ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
1631 ; mapM_ (unifyDerived loc Nominal) eqns }
1632 | otherwise
1633 = return ()
1634
1635 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1636
1637 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1638 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1639 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1640 | isGiven old_ev
1641 = ASSERT( ctEvEqRel old_ev == NomEq )
1642 runFlatten $
1643 do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
1644 ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
1645 -- ax_co :: F args ~ G tc_args
1646 -- cos :: xis ~ tc_args
1647 -- old_ev :: F args ~ fsk
1648 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1649
1650 ; new_ev <- newGivenEvVar deeper_loc
1651 ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1652 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1653 `mkTcTransCo` mkTcSymCo ax_co
1654 `mkTcTransCo` ctEvCoercion old_ev) )
1655
1656 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1657 ; emitFlatWork new_ct
1658 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1659
1660 | otherwise
1661 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1662 ASSERT( ctEvEqRel old_ev == NomEq )
1663 runFlatten $
1664 do { let fmode = mkFlattenEnv FM_FlattenAll old_ev
1665 ; (xis, cos) <- flatten_many fmode (repeat Nominal) tc_args
1666 -- ax_co :: F args ~ G tc_args
1667 -- cos :: xis ~ tc_args
1668 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1669 -- new_ev :: G xis ~ fsk
1670 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1671
1672 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
1673 ; setEvBind (ctEvId old_ev)
1674 (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1675 `mkTcTransCo` ctEvCoercion new_ev))
1676
1677 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1678 ; emitFlatWork new_ct
1679 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1680 where
1681 loc = ctEvLoc old_ev
1682 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1683
1684 dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1685 -- (dischargeFmv x fmv co ty)
1686 -- [W] x :: F tys ~ fuv
1687 -- co :: F tys ~ ty
1688 -- Precondition: fuv is not filled, and fuv `notElem` ty
1689 --
1690 -- Then set fuv := ty,
1691 -- set x := co
1692 -- kick out any inert things that are now rewritable
1693 dischargeFmv evar fmv co xi
1694 = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi )
1695 do { setWantedTyBind fmv xi
1696 ; setEvBind evar (EvCoercion co)
1697 ; n_kicked <- kickOutRewritable Given NomEq fmv
1698 ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1699
1700 {-
1701 Note [Cached solved FunEqs]
1702 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1703 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1704 to see if we have reduced (FunExpensive big-type) before, lest we
1705 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1706 we must use `canRewriteOrSame` because both uses might (say) be Wanteds,
1707 and we *still* want to save the re-computation.
1708
1709 Note [MATCHING-SYNONYMS]
1710 ~~~~~~~~~~~~~~~~~~~~~~~~
1711 When trying to match a dictionary (D tau) to a top-level instance, or a
1712 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1713 we do *not* need to expand type synonyms because the matcher will do that for us.
1714
1715
1716 Note [RHS-FAMILY-SYNONYMS]
1717 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1718 The RHS of a family instance is represented as yet another constructor which is
1719 like a type synonym for the real RHS the programmer declared. Eg:
1720 type instance F (a,a) = [a]
1721 Becomes:
1722 :R32 a = [a] -- internal type synonym introduced
1723 F (a,a) ~ :R32 a -- instance
1724
1725 When we react a family instance with a type family equation in the work list
1726 we keep the synonym-using RHS without expansion.
1727
1728 Note [FunDep and implicit parameter reactions]
1729 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1730 Currently, our story of interacting two dictionaries (or a dictionary
1731 and top-level instances) for functional dependencies, and implicit
1732 paramters, is that we simply produce new Derived equalities. So for example
1733
1734 class D a b | a -> b where ...
1735 Inert:
1736 d1 :g D Int Bool
1737 WorkItem:
1738 d2 :w D Int alpha
1739
1740 We generate the extra work item
1741 cv :d alpha ~ Bool
1742 where 'cv' is currently unused. However, this new item can perhaps be
1743 spontaneously solved to become given and react with d2,
1744 discharging it in favour of a new constraint d2' thus:
1745 d2' :w D Int Bool
1746 d2 := d2' |> D Int cv
1747 Now d2' can be discharged from d1
1748
1749 We could be more aggressive and try to *immediately* solve the dictionary
1750 using those extra equalities, but that requires those equalities to carry
1751 evidence and derived do not carry evidence.
1752
1753 If that were the case with the same inert set and work item we might dischard
1754 d2 directly:
1755
1756 cv :w alpha ~ Bool
1757 d2 := d1 |> D Int cv
1758
1759 But in general it's a bit painful to figure out the necessary coercion,
1760 so we just take the first approach. Here is a better example. Consider:
1761 class C a b c | a -> b
1762 And:
1763 [Given] d1 : C T Int Char
1764 [Wanted] d2 : C T beta Int
1765 In this case, it's *not even possible* to solve the wanted immediately.
1766 So we should simply output the functional dependency and add this guy
1767 [but NOT its superclasses] back in the worklist. Even worse:
1768 [Given] d1 : C T Int beta
1769 [Wanted] d2: C T beta Int
1770 Then it is solvable, but its very hard to detect this on the spot.
1771
1772 It's exactly the same with implicit parameters, except that the
1773 "aggressive" approach would be much easier to implement.
1774
1775 Note [When improvement happens]
1776 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1777 We fire an improvement rule when
1778
1779 * Two constraints match (modulo the fundep)
1780 e.g. C t1 t2, C t1 t3 where C a b | a->b
1781 The two match because the first arg is identical
1782
1783 Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
1784 superclass of a Wanted goal) or if both are Given.
1785
1786 Example (tcfail138)
1787 class L a b | a -> b
1788 class (G a, L a b) => C a b
1789
1790 instance C a b' => G (Maybe a)
1791 instance C a b => C (Maybe a) a
1792 instance L (Maybe a) a
1793
1794 When solving the superclasses of the (C (Maybe a) a) instance, we get
1795 Given: C a b ... and hance by superclasses, (G a, L a b)
1796 Wanted: G (Maybe a)
1797 Use the instance decl to get
1798 Wanted: C a b'
1799 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1800 and now we need improvement between that derived superclass an the Given (L a b)
1801
1802 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
1803 emit Derived FDs for givens as well.
1804
1805 Note [Weird fundeps]
1806 ~~~~~~~~~~~~~~~~~~~~
1807 Consider class Het a b | a -> b where
1808 het :: m (f c) -> a -> m b
1809
1810 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1811 instance GHet (K a) (K [a])
1812 instance Het a b => GHet (K a) (K b)
1813
1814 The two instances don't actually conflict on their fundeps,
1815 although it's pretty strange. So they are both accepted. Now
1816 try [W] GHet (K Int) (K Bool)
1817 This triggers fudeps from both instance decls; but it also
1818 matches a *unique* instance decl, and we should go ahead and
1819 pick that one right now. Otherwise, if we don't, it ends up
1820 unsolved in the inert set and is reported as an error.
1821
1822 Trac #7875 is a case in point.
1823
1824 Note [Overriding implicit parameters]
1825 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1826 Consider
1827 f :: (?x::a) -> Bool -> a
1828
1829 g v = let ?x::Int = 3
1830 in (f v, let ?x::Bool = True in f v)
1831
1832 This should probably be well typed, with
1833 g :: Bool -> (Int, Bool)
1834
1835 So the inner binding for ?x::Bool *overrides* the outer one.
1836 Hence a work-item Given overrides an inert-item Given.
1837
1838 Note [Given constraint that matches an instance declaration]
1839 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1840 What should we do when we discover that one (or more) top-level
1841 instances match a given (or solved) class constraint? We have
1842 two possibilities:
1843
1844 1. Reject the program. The reason is that there may not be a unique
1845 best strategy for the solver. Example, from the OutsideIn(X) paper:
1846 instance P x => Q [x]
1847 instance (x ~ y) => R [x] y
1848
1849 wob :: forall a b. (Q [b], R b a) => a -> Int
1850
1851 g :: forall a. Q [a] => [a] -> Int
1852 g x = wob x
1853
1854 will generate the impliation constraint:
1855 Q [a] => (Q [beta], R beta [a])
1856 If we react (Q [beta]) with its top-level axiom, we end up with a
1857 (P beta), which we have no way of discharging. On the other hand,
1858 if we react R beta [a] with the top-level we get (beta ~ a), which
1859 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1860 now solvable by the given Q [a].
1861
1862 However, this option is restrictive, for instance [Example 3] from
1863 Note [Recursive instances and superclases] will fail to work.
1864
1865 2. Ignore the problem, hoping that the situations where there exist indeed
1866 such multiple strategies are rare: Indeed the cause of the previous
1867 problem is that (R [x] y) yields the new work (x ~ y) which can be
1868 *spontaneously* solved, not using the givens.
1869
1870 We are choosing option 2 below but we might consider having a flag as well.
1871
1872
1873 Note [New Wanted Superclass Work]
1874 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1875 Even in the case of wanted constraints, we may add some superclasses
1876 as new given work. The reason is:
1877
1878 To allow FD-like improvement for type families. Assume that
1879 we have a class
1880 class C a b | a -> b
1881 and we have to solve the implication constraint:
1882 C a b => C a beta
1883 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1884
1885 We want to have the same effect with the type family encoding of
1886 functional dependencies. Namely, consider:
1887 class (F a ~ b) => C a b
1888 Now suppose that we have:
1889 given: C a b
1890 wanted: C a beta
1891 By interacting the given we will get given (F a ~ b) which is not
1892 enough by itself to make us discharge (C a beta). However, we
1893 may create a new derived equality from the super-class of the
1894 wanted constraint (C a beta), namely derived (F a ~ beta).
1895 Now we may interact this with given (F a ~ b) to get:
1896 derived : beta ~ b
1897 But 'beta' is a touchable unification variable, and hence OK to
1898 unify it with 'b', replacing the derived evidence with the identity.
1899
1900 This requires trySpontaneousSolve to solve *derived*
1901 equalities that have a touchable in their RHS, *in addition*
1902 to solving wanted equalities.
1903
1904 We also need to somehow use the superclasses to quantify over a minimal,
1905 constraint see note [Minimize by Superclasses] in TcSimplify.
1906
1907
1908 Finally, here is another example where this is useful.
1909
1910 Example 1:
1911 ----------
1912 class (F a ~ b) => C a b
1913 And we are given the wanteds:
1914 w1 : C a b
1915 w2 : C a c
1916 w3 : b ~ c
1917 We surely do *not* want to quantify over (b ~ c), since if someone provides
1918 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1919 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1920
1921 Step 1: We will get new *given* superclass work,
1922 provisionally to our solving of w1 and w2
1923
1924 g1: F a ~ b, g2 : F a ~ c,
1925 w1 : C a b, w2 : C a c, w3 : b ~ c
1926
1927 The evidence for g1 and g2 is a superclass evidence term:
1928
1929 g1 := sc w1, g2 := sc w2
1930
1931 Step 2: The givens will solve the wanted w3, so that
1932 w3 := sym (sc w1) ; sc w2
1933
1934 Step 3: Now, one may naively assume that then w2 can be solve from w1
1935 after rewriting with the (now solved equality) (b ~ c).
1936
1937 But this rewriting is ruled out by the isGoodRectDict!
1938
1939 Conclusion, we will (correctly) end up with the unsolved goals
1940 (C a b, C a c)
1941
1942 NB: The desugarer needs be more clever to deal with equalities
1943 that participate in recursive dictionary bindings.
1944 -}
1945
1946 data LookupInstResult
1947 = NoInstance
1948 | GenInst [CtEvidence] EvTerm
1949
1950 instance Outputable LookupInstResult where
1951 ppr NoInstance = text "NoInstance"
1952 ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
1953
1954
1955 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1956
1957 matchClassInst _ clas [ ty ] _
1958 | className clas == knownNatClassName
1959 , Just n <- isNumLitTy ty = makeDict (EvNum n)
1960
1961 | className clas == knownSymbolClassName
1962 , Just s <- isStrLitTy ty = makeDict (EvStr s)
1963
1964 where
1965 {- This adds a coercion that will convert the literal into a dictionary
1966 of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1967 in TcEvidence. The coercion happens in 2 steps:
1968
1969 Integer -> SNat n -- representation of literal to singleton
1970 SNat n -> KnownNat n -- singleton to dictionary
1971
1972 The process is mirrored for Symbols:
1973 String -> SSymbol n
1974 SSymbol n -> KnownSymbol n
1975 -}
1976 makeDict evLit
1977 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1978 -- co_dict :: KnownNat n ~ SNat n
1979 , [ meth ] <- classMethods clas
1980 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1981 $ funResultTy -- SNat n
1982 $ dropForAlls -- KnownNat n => SNat n
1983 $ idType meth -- forall n. KnownNat n => SNat n
1984 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
1985 -- SNat n ~ Integer
1986 = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)))
1987
1988 | otherwise
1989 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1990 $$ vcat (map (ppr . idType) (classMethods clas)))
1991
1992 matchClassInst inerts clas tys loc
1993 = do { dflags <- getDynFlags
1994 ; tclvl <- getTcLevel
1995 ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
1996 , text "inerts=" <+> ppr inerts
1997 , text "untouchables=" <+> ppr tclvl ]
1998 ; instEnvs <- getInstEnvs
1999 ; case lookupInstEnv instEnvs clas tys of
2000 ([], _, _) -- Nothing matches
2001 -> do { traceTcS "matchClass not matching" $
2002 vcat [ text "dict" <+> ppr pred ]
2003 ; return NoInstance }
2004
2005 ([(ispec, inst_tys)], [], _) -- A single match
2006 | not (xopt Opt_IncoherentInstances dflags)
2007 , given_overlap tclvl
2008 -> -- See Note [Instance and Given overlap]
2009 do { traceTcS "Delaying instance application" $
2010 vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
2011 , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
2012 ; return NoInstance }
2013
2014 | otherwise
2015 -> do { let dfun_id = instanceDFunId ispec
2016 ; traceTcS "matchClass success" $
2017 vcat [text "dict" <+> ppr pred,
2018 text "witness" <+> ppr dfun_id
2019 <+> ppr (idType dfun_id) ]
2020 -- Record that this dfun is needed
2021 ; match_one dfun_id inst_tys }
2022
2023 (matches, _, _) -- More than one matches
2024 -- Defer any reactions of a multitude
2025 -- until we learn more about the reagent
2026 -> do { traceTcS "matchClass multiple matches, deferring choice" $
2027 vcat [text "dict" <+> ppr pred,
2028 text "matches" <+> ppr matches]
2029 ; return NoInstance } }
2030 where
2031 pred = mkClassPred clas tys
2032
2033 match_one :: DFunId -> [Maybe TcType] -> TcS LookupInstResult
2034 -- See Note [DFunInstType: instantiating types] in InstEnv
2035 match_one dfun_id mb_inst_tys
2036 = do { checkWellStagedDFun pred dfun_id loc
2037 ; (tys, dfun_phi) <- instDFunType dfun_id mb_inst_tys
2038 ; let (theta, _) = tcSplitPhiTy dfun_phi
2039 ; if null theta then
2040 return (GenInst [] (EvDFunApp dfun_id tys []))
2041 else do
2042 { evc_vars <- instDFunConstraints loc theta
2043 ; let new_ev_vars = freshGoals evc_vars
2044 -- new_ev_vars are only the real new variables that can be emitted
2045 dfun_app = EvDFunApp dfun_id tys (map (ctEvTerm . fst) evc_vars)
2046 ; return $ GenInst new_ev_vars dfun_app } }
2047
2048 givens_for_this_clas :: Cts
2049 givens_for_this_clas
2050 = filterBag isGivenCt (findDictsByClass (inert_dicts $ inert_cans inerts) clas)
2051
2052 given_overlap :: TcLevel -> Bool
2053 given_overlap tclvl = anyBag (matchable tclvl) givens_for_this_clas
2054
2055 matchable tclvl (CDictCan { cc_class = clas_g, cc_tyargs = sys
2056 , cc_ev = fl })
2057 | isGiven fl
2058 = ASSERT( clas_g == clas )
2059 case tcUnifyTys (\tv -> if isTouchableMetaTyVar tclvl tv &&
2060 tv `elemVarSet` tyVarsOfTypes tys
2061 then BindMe else Skolem) tys sys of
2062 -- We can't learn anything more about any variable at this point, so the only
2063 -- cause of overlap can be by an instantiation of a touchable unification
2064 -- variable. Hence we only bind touchable unification variables. In addition,
2065 -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
2066 Nothing -> False
2067 Just _ -> True
2068 | otherwise = False -- No overlap with a solved, already been taken care of
2069 -- by the overlap check with the instance environment.
2070 matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
2071
2072 {-
2073 Note [Instance and Given overlap]
2074 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2075 Assume that we have an inert set that looks as follows:
2076 [Given] D [Int]
2077 And an instance declaration:
2078 instance C a => D [a]
2079 A new wanted comes along of the form:
2080 [Wanted] D [alpha]
2081
2082 One possibility is to apply the instance declaration which will leave us
2083 with an unsolvable goal (C alpha). However, later on a new constraint may
2084 arise (for instance due to a functional dependency between two later dictionaries),
2085 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
2086 will be transformed to [Wanted] D [Int], which could have been discharged by the given.
2087
2088 The solution is that in matchClassInst and eventually in topReact, we get back with
2089 a matching instance, only when there is no Given in the inerts which is unifiable to
2090 this particular dictionary.
2091
2092 The end effect is that, much as we do for overlapping instances, we delay choosing a
2093 class instance if there is a possibility of another instance OR a given to match our
2094 constraint later on. This fixes bugs #4981 and #5002.
2095
2096 This is arguably not easy to appear in practice due to our aggressive prioritization
2097 of equality solving over other constraints, but it is possible. I've added a test case
2098 in typecheck/should-compile/GivenOverlapping.hs
2099
2100 We ignore the overlap problem if -XIncoherentInstances is in force: see
2101 Trac #6002 for a worked-out example where this makes a difference.
2102
2103 Moreover notice that our goals here are different than the goals of the top-level
2104 overlapping checks. There we are interested in validating the following principle:
2105
2106 If we inline a function f at a site where the same global instance environment
2107 is available as the instance environment at the definition site of f then we
2108 should get the same behaviour.
2109
2110 But for the Given Overlap check our goal is just related to completeness of
2111 constraint solving.
2112 -}