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