Revise the inert-set invariants again
[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
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 (vcat [ text "n-kicked =" <+> int (workListSize kicked_out)
956 , text "n-kept fun-eqs =" <+> int (sizeFunEqMap (inert_funeqs ics'))
957 , ppr kicked_out ])
958 ; return (workListSize kicked_out) }
959
960 kick_out :: CtEvidence -> TcTyVar -> InertCans -> (WorkList, InertCans)
961 kick_out new_ev new_tv (IC { inert_eqs = tv_eqs
962 , inert_dicts = dictmap
963 , inert_funeqs = funeqmap
964 , inert_irreds = irreds
965 , inert_insols = insols })
966 = (kicked_out, inert_cans_in)
967 where
968 -- NB: Notice that don't rewrite
969 -- inert_solved_dicts, and inert_solved_funeqs
970 -- optimistically. But when we lookup we have to
971 -- take the subsitution into account
972 inert_cans_in = IC { inert_eqs = tv_eqs_in
973 , inert_dicts = dicts_in
974 , inert_funeqs = feqs_in
975 , inert_irreds = irs_in
976 , inert_insols = insols_in }
977
978 kicked_out = WL { wl_eqs = tv_eqs_out
979 , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
980 , wl_rest = bagToList (dicts_out `andCts` irs_out
981 `andCts` insols_out)
982 , wl_implics = emptyBag }
983
984 (tv_eqs_out, tv_eqs_in) = foldVarEnv kick_out_eqs ([], emptyVarEnv) tv_eqs
985 (feqs_out, feqs_in) = partitionFunEqs kick_out_ct funeqmap
986 (dicts_out, dicts_in) = partitionDicts kick_out_ct dictmap
987 (irs_out, irs_in) = partitionBag kick_out_irred irreds
988 (insols_out, insols_in) = partitionBag kick_out_ct insols
989 -- Kick out even insolubles; see Note [Kick out insolubles]
990
991 kick_out_ct :: Ct -> Bool
992 kick_out_ct ct = kick_out_ctev (ctEvidence ct)
993
994 kick_out_ctev ev = eqCanRewrite new_ev ev
995 && new_tv `elemVarSet` tyVarsOfType (ctEvPred ev)
996 -- See Note [Kicking out inert constraints]
997
998 kick_out_irred :: Ct -> Bool
999 kick_out_irred ct = eqCanRewrite new_ev (ctEvidence ct)
1000 && new_tv `elemVarSet` closeOverKinds (tyVarsOfCt ct)
1001 -- See Note [Kicking out Irreds]
1002
1003 kick_out_eqs :: EqualCtList -> ([Ct], TyVarEnv EqualCtList)
1004 -> ([Ct], TyVarEnv EqualCtList)
1005 kick_out_eqs eqs (acc_out, acc_in)
1006 = (eqs_out ++ acc_out, case eqs_in of
1007 [] -> acc_in
1008 (eq1:_) -> extendVarEnv acc_in (cc_tyvar eq1) eqs_in)
1009 where
1010 (eqs_out, eqs_in) = partition kick_out_eq eqs
1011
1012 kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs_ty, cc_ev = ev })
1013 = eqCanRewrite new_ev ev
1014 && (tv == new_tv
1015 || (ev `eqCanRewrite` ev && new_tv `elemVarSet` tyVarsOfType rhs_ty)
1016 || case getTyVar_maybe rhs_ty of { Just tv_r -> tv_r == new_tv; Nothing -> False })
1017 kick_out_eq ct = pprPanic "kick_out_eq" (ppr ct)
1018 -- SLPJ new piece: Don't kick out a constraint unless it can rewrite itself,
1019 -- If not, it can't rewrite anything else, so no point in
1020 -- kicking it out
1021
1022 {-
1023 Note [Kicking out inert constraints]
1024 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1025 Given a new (a -> ty) inert, we want to kick out an existing inert
1026 constraint if
1027 a) the new constraint can rewrite the inert one
1028 b) 'a' is free in the inert constraint (so that it *will*)
1029 rewrite it if we kick it out.
1030
1031 For (b) we use tyVarsOfCt, which returns the type variables /and
1032 the kind variables/ that are directly visible in the type. Hence we
1033 will have exposed all the rewriting we care about to make the most
1034 precise kinds visible for matching classes etc. No need to kick out
1035 constraints that mention type variables whose kinds contain this
1036 variable! (Except see Note [Kicking out Irreds].)
1037
1038 Note [Kicking out Irreds]
1039 ~~~~~~~~~~~~~~~~~~~~~~~~~
1040 There is an awkward special case for Irreds. When we have a
1041 kind-mis-matched equality constraint (a:k1) ~ (ty:k2), we turn it into
1042 an Irred (see Note [Equalities with incompatible kinds] in
1043 TcCanonical). So in this case the free kind variables of k1 and k2
1044 are not visible. More precisely, the type looks like
1045 (~) k1 (a:k1) (ty:k2)
1046 because (~) has kind forall k. k -> k -> Constraint. So the constraint
1047 itself is ill-kinded. We can "see" k1 but not k2. That's why we use
1048 closeOverKinds to make sure we see k2.
1049
1050 This is not pretty. Maybe (~) should have kind
1051 (~) :: forall k1 k1. k1 -> k2 -> Constraint
1052
1053 Note [Kick out insolubles]
1054 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1055 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
1056 because an occurs check. And then we unify alpha := [Int].
1057 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
1058 Now it can be decomposed. Otherwise we end up with a "Can't match
1059 [Int] ~ [[Int]]" which is true, but a bit confusing because the
1060 outer type constructors match.
1061
1062 Note [Delicate equality kick-out]
1063 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1064 When adding an fully-rewritten work-item CTyEqCan (a ~ xi), we kick
1065 out an inert CTyEqCan (b ~ phi) when
1066
1067 a) the work item can rewrite the inert item
1068
1069 AND one of the following hold
1070
1071 (0) If the new tyvar is the same as the old one
1072 Work item: [G] a ~ blah
1073 Inert: [W] a ~ foo
1074 A particular case is when flatten-skolems get their value we must propagate
1075
1076 (1) If the new tyvar appears in the kind vars of the LHS or RHS of
1077 the inert. Example:
1078 Work item: [G] k ~ *
1079 Inert: [W] (a:k) ~ ty
1080 [W] (b:*) ~ c :: k
1081 We must kick out those blocked inerts so that we rewrite them
1082 and can subsequently unify.
1083
1084 (2) If the new tyvar appears in the RHS of the inert
1085 AND not (the inert can rewrite the work item) <---------------------------------
1086
1087 Work item: [G] a ~ b
1088 Inert: [W] b ~ [a]
1089 Now at this point the work item cannot be further rewritten by the
1090 inert (due to the weaker inert flavor). But we can't add the work item
1091 as-is because the inert set would then have a cyclic substitution,
1092 when rewriting a wanted type mentioning 'a'. So we must kick the inert out.
1093
1094 We have to do this only if the inert *cannot* rewrite the work item;
1095 it it can, then the work item will have been fully rewritten by the
1096 inert set during canonicalisation. So for example:
1097 Work item: [W] a ~ Int
1098 Inert: [W] b ~ [a]
1099 No need to kick out the inert, beause the inert substitution is not
1100 necessarily idemopotent. See Note [Non-idempotent inert substitution]
1101 in TcFlatten.
1102
1103 Work item: [G] a ~ Int
1104 Inert: [G] b ~ [a]
1105 See also Note [Detailed InertCans Invariants]
1106
1107 Note [Avoid double unifications]
1108 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1109 The spontaneous solver has to return a given which mentions the unified unification
1110 variable *on the left* of the equality. Here is what happens if not:
1111 Original wanted: (a ~ alpha), (alpha ~ Int)
1112 We spontaneously solve the first wanted, without changing the order!
1113 given : a ~ alpha [having unified alpha := a]
1114 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1115 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1116
1117 We avoid this problem by orienting the resulting given so that the unification
1118 variable is on the left. [Note that alternatively we could attempt to
1119 enforce this at canonicalization]
1120
1121 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1122 double unifications is the main reason we disallow touchable
1123 unification variables as RHS of type family equations: F xis ~ alpha.
1124
1125
1126
1127 Note [Superclasses and recursive dictionaries]
1128 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1129 Overlaps with Note [SUPERCLASS-LOOP 1]
1130 Note [SUPERCLASS-LOOP 2]
1131 Note [Recursive instances and superclases]
1132 ToDo: check overlap and delete redundant stuff
1133
1134 Right before adding a given into the inert set, we must
1135 produce some more work, that will bring the superclasses
1136 of the given into scope. The superclass constraints go into
1137 our worklist.
1138
1139 When we simplify a wanted constraint, if we first see a matching
1140 instance, we may produce new wanted work. To (1) avoid doing this work
1141 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1142 this item as given into our inert set WITHOUT adding its superclass constraints,
1143 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
1144 for doing the isGoodRecEv check in an older version of the type checker].
1145
1146 But now we have added partially solved constraints to the worklist which may
1147 interact with other wanteds. Consider the example:
1148
1149 Example 1:
1150
1151 class Eq b => Foo a b --- 0-th selector
1152 instance Eq a => Foo [a] a --- fooDFun
1153
1154 and wanted (Foo [t] t). We are first going to see that the instance matches
1155 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1156 d1 :_g Foo [t] t d1 := EvDFunApp fooDFun d3
1157 Our work list is going to contain a new *wanted* goal
1158 d3 :_w Eq t
1159
1160 Ok, so how do we get recursive dictionaries, at all:
1161
1162 Example 2:
1163
1164 data D r = ZeroD | SuccD (r (D r));
1165
1166 instance (Eq (r (D r))) => Eq (D r) where
1167 ZeroD == ZeroD = True
1168 (SuccD a) == (SuccD b) = a == b
1169 _ == _ = False;
1170
1171 equalDC :: D [] -> D [] -> Bool;
1172 equalDC = (==);
1173
1174 We need to prove (Eq (D [])). Here's how we go:
1175
1176 d1 :_w Eq (D [])
1177
1178 by instance decl, holds if
1179 d2 :_w Eq [D []]
1180 where d1 = dfEqD d2
1181
1182 *BUT* we have an inert set which gives us (no superclasses):
1183 d1 :_g Eq (D [])
1184 By the instance declaration of Eq we can show the 'd2' goal if
1185 d3 :_w Eq (D [])
1186 where d2 = dfEqList d3
1187 d1 = dfEqD d2
1188 Now, however this wanted can interact with our inert d1 to set:
1189 d3 := d1
1190 and solve the goal. Why was this interaction OK? Because, if we chase the
1191 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1192 are really setting
1193 d3 := dfEqD2 (dfEqList d3)
1194 which is FINE because the use of d3 is protected by the instance function
1195 applications.
1196
1197 So, our strategy is to try to put solved wanted dictionaries into the
1198 inert set along with their superclasses (when this is meaningful,
1199 i.e. when new wanted goals are generated) but solve a wanted dictionary
1200 from a given only in the case where the evidence variable of the
1201 wanted is mentioned in the evidence of the given (recursively through
1202 the evidence binds) in a protected way: more instance function applications
1203 than superclass selectors.
1204
1205 Here are some more examples from GHC's previous type checker
1206
1207
1208 Example 3:
1209 This code arises in the context of "Scrap Your Boilerplate with Class"
1210
1211 class Sat a
1212 class Data ctx a
1213 instance Sat (ctx Char) => Data ctx Char -- dfunData1
1214 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a] -- dfunData2
1215
1216 class Data Maybe a => Foo a
1217
1218 instance Foo t => Sat (Maybe t) -- dfunSat
1219
1220 instance Data Maybe a => Foo a -- dfunFoo1
1221 instance Foo a => Foo [a] -- dfunFoo2
1222 instance Foo [Char] -- dfunFoo3
1223
1224 Consider generating the superclasses of the instance declaration
1225 instance Foo a => Foo [a]
1226
1227 So our problem is this
1228 [G] d0 : Foo t
1229 [W] d1 : Data Maybe [t] -- Desired superclass
1230
1231 We may add the given in the inert set, along with its superclasses
1232 [assuming we don't fail because there is a matching instance, see
1233 topReactionsStage, given case ]
1234 Inert:
1235 [G] d0 : Foo t
1236 [G] d01 : Data Maybe t -- Superclass of d0
1237 WorkList
1238 [W] d1 : Data Maybe [t]
1239
1240 Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
1241 Inert:
1242 [G] d0 : Foo t
1243 [G] d01 : Data Maybe t -- Superclass of d0
1244 Solved:
1245 d1 : Data Maybe [t]
1246 WorkList
1247 [W] d2 : Sat (Maybe [t])
1248 [W] d3 : Data Maybe t
1249
1250 Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
1251 Inert:
1252 [G] d0 : Foo t
1253 [G] d01 : Data Maybe t -- Superclass of d0
1254 Solved:
1255 d1 : Data Maybe [t]
1256 d2 : Sat (Maybe [t])
1257 WorkList:
1258 [W] d3 : Data Maybe t
1259 [W] d4 : Foo [t]
1260
1261 Now, we can just solve d3 from d01; d3 := d01
1262 Inert
1263 [G] d0 : Foo t
1264 [G] d01 : Data Maybe t -- Superclass of d0
1265 Solved:
1266 d1 : Data Maybe [t]
1267 d2 : Sat (Maybe [t])
1268 WorkList
1269 [W] d4 : Foo [t]
1270
1271 Now, solve d4 using dfunFoo2; d4 := dfunFoo2 d5
1272 Inert
1273 [G] d0 : Foo t
1274 [G] d01 : Data Maybe t -- Superclass of d0
1275 Solved:
1276 d1 : Data Maybe [t]
1277 d2 : Sat (Maybe [t])
1278 d4 : Foo [t]
1279 WorkList:
1280 [W] d5 : Foo t
1281
1282 Now, d5 can be solved! d5 := d0
1283
1284 Result
1285 d1 := dfunData2 d2 d3
1286 d2 := dfunSat d4
1287 d3 := d01
1288 d4 := dfunFoo2 d5
1289 d5 := d0
1290
1291 d0 :_g Foo t
1292 d1 :_s Data Maybe [t] d1 := dfunData2 d2 d3
1293 d2 :_g Sat (Maybe [t]) d2 := dfunSat d4
1294 d4 :_g Foo [t] d4 := dfunFoo2 d5
1295 d5 :_g Foo t d5 := dfunFoo1 d7
1296 WorkList:
1297 d7 :_w Data Maybe t
1298 d6 :_g Data Maybe [t]
1299 d8 :_g Data Maybe t d8 := EvDictSuperClass d5 0
1300 d01 :_g Data Maybe t
1301
1302 Now, two problems:
1303 [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1304 we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1305 that must not be used (look at case interactInert where both inert and workitem
1306 are givens). So we have several options:
1307 - Drop the workitem always (this will drop d8)
1308 This feels very unsafe -- what if the work item was the "good" one
1309 that should be used later to solve another wanted?
1310 - Don't drop anyone: the inert set may contain multiple givens!
1311 [This is currently implemented]
1312
1313 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1314 [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1315 d7. Now the [isRecDictEv] function in the ineration solver
1316 [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1317 precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1318
1319 So, no interaction happens there. Then we meet d01 and there is no recursion
1320 problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1321
1322 Note [SUPERCLASS-LOOP 1]
1323 ~~~~~~~~~~~~~~~~~~~~~~~~
1324 We have to be very, very careful when generating superclasses, lest we
1325 accidentally build a loop. Here's an example:
1326
1327 class S a
1328
1329 class S a => C a where { opc :: a -> a }
1330 class S b => D b where { opd :: b -> b }
1331
1332 instance C Int where
1333 opc = opd
1334
1335 instance D Int where
1336 opd = opc
1337
1338 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1339 Simplifying, we may well get:
1340 $dfCInt = :C ds1 (opd dd)
1341 dd = $dfDInt
1342 ds1 = $p1 dd
1343 Notice that we spot that we can extract ds1 from dd.
1344
1345 Alas! Alack! We can do the same for (instance D Int):
1346
1347 $dfDInt = :D ds2 (opc dc)
1348 dc = $dfCInt
1349 ds2 = $p1 dc
1350
1351 And now we've defined the superclass in terms of itself.
1352 Two more nasty cases are in
1353 tcrun021
1354 tcrun033
1355
1356 Solution:
1357 - Satisfy the superclass context *all by itself*
1358 (tcSimplifySuperClasses)
1359 - And do so completely; i.e. no left-over constraints
1360 to mix with the constraints arising from method declarations
1361
1362
1363 Note [SUPERCLASS-LOOP 2]
1364 ~~~~~~~~~~~~~~~~~~~~~~~~
1365 We need to be careful when adding "the constaint we are trying to prove".
1366 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1367
1368 class Ord a => C a where
1369 instance Ord [a] => C [a] where ...
1370
1371 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1372 superclasses of C [a] to avails. But we must not overwrite the binding
1373 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1374 build a loop!
1375
1376 Here's another variant, immortalised in tcrun020
1377 class Monad m => C1 m
1378 class C1 m => C2 m x
1379 instance C2 Maybe Bool
1380 For the instance decl we need to build (C1 Maybe), and it's no good if
1381 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1382 before we search for C1 Maybe.
1383
1384 Here's another example
1385 class Eq b => Foo a b
1386 instance Eq a => Foo [a] a
1387 If we are reducing
1388 (Foo [t] t)
1389
1390 we'll first deduce that it holds (via the instance decl). We must not
1391 then overwrite the Eq t constraint with a superclass selection!
1392
1393 At first I had a gross hack, whereby I simply did not add superclass constraints
1394 in addWanted, though I did for addGiven and addIrred. This was sub-optimal,
1395 because it lost legitimate superclass sharing, and it still didn't do the job:
1396 I found a very obscure program (now tcrun021) in which improvement meant the
1397 simplifier got two bites a the cherry... so something seemed to be an Stop
1398 first time, but reducible next time.
1399
1400 Now we implement the Right Solution, which is to check for loops directly
1401 when adding superclasses. It's a bit like the occurs check in unification.
1402
1403 Note [Recursive instances and superclases]
1404 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1405 Consider this code, which arises in the context of "Scrap Your
1406 Boilerplate with Class".
1407
1408 class Sat a
1409 class Data ctx a
1410 instance Sat (ctx Char) => Data ctx Char
1411 instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1412
1413 class Data Maybe a => Foo a
1414
1415 instance Foo t => Sat (Maybe t)
1416
1417 instance Data Maybe a => Foo a
1418 instance Foo a => Foo [a]
1419 instance Foo [Char]
1420
1421 In the instance for Foo [a], when generating evidence for the superclasses
1422 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1423 Using the instance for Data, we therefore need
1424 (Sat (Maybe [a], Data Maybe a)
1425 But we are given (Foo a), and hence its superclass (Data Maybe a).
1426 So that leaves (Sat (Maybe [a])). Using the instance for Sat means
1427 we need (Foo [a]). And that is the very dictionary we are bulding
1428 an instance for! So we must put that in the "givens". So in this
1429 case we have
1430 Given: Foo a, Foo [a]
1431 Wanted: Data Maybe [a]
1432
1433 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1434 the givens, which is what 'addGiven' would normally do. Why? Because
1435 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1436 by selecting a superclass from Foo [a], which simply makes a loop.
1437
1438 On the other hand we *must* put the superclasses of (Foo a) in
1439 the givens, as you can see from the derivation described above.
1440
1441 Conclusion: in the very special case of tcSimplifySuperClasses
1442 we have one 'given' (namely the "this" dictionary) whose superclasses
1443 must not be added to 'givens' by addGiven.
1444
1445 There is a complication though. Suppose there are equalities
1446 instance (Eq a, a~b) => Num (a,b)
1447 Then we normalise the 'givens' wrt the equalities, so the original
1448 given "this" dictionary is cast to one of a different type. So it's a
1449 bit trickier than before to identify the "special" dictionary whose
1450 superclasses must not be added. See test
1451 indexed-types/should_run/EqInInstance
1452
1453 We need a persistent property of the dictionary to record this
1454 special-ness. Current I'm using the InstLocOrigin (a bit of a hack,
1455 but cool), which is maintained by dictionary normalisation.
1456 Specifically, the InstLocOrigin is
1457 NoScOrigin
1458 then the no-superclass thing kicks in. WATCH OUT if you fiddle
1459 with InstLocOrigin!
1460
1461
1462 ************************************************************************
1463 * *
1464 * Functional dependencies, instantiation of equations
1465 * *
1466 ************************************************************************
1467
1468 When we spot an equality arising from a functional dependency,
1469 we now use that equality (a "wanted") to rewrite the work-item
1470 constraint right away. This avoids two dangers
1471
1472 Danger 1: If we send the original constraint on down the pipeline
1473 it may react with an instance declaration, and in delicate
1474 situations (when a Given overlaps with an instance) that
1475 may produce new insoluble goals: see Trac #4952
1476
1477 Danger 2: If we don't rewrite the constraint, it may re-react
1478 with the same thing later, and produce the same equality
1479 again --> termination worries.
1480
1481 To achieve this required some refactoring of FunDeps.lhs (nicer
1482 now!).
1483 -}
1484
1485 rewriteWithFunDeps :: [Equation CtLoc] -> TcS ()
1486 -- NB: The returned constraints are all Derived
1487 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1488 rewriteWithFunDeps eqn_pred_locs
1489 = mapM_ instFunDepEqn eqn_pred_locs
1490
1491 instFunDepEqn :: Equation CtLoc -> TcS ()
1492 -- Post: Returns the position index as well as the corresponding FunDep equality
1493 instFunDepEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1494 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1495 ; mapM_ (do_one subst) eqs }
1496 where
1497 do_one subst (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
1498 = emitNewDerivedEq loc (Pair (Type.substTy subst ty1) (Type.substTy subst ty2))
1499
1500 {-
1501 *********************************************************************************
1502 * *
1503 The top-reaction Stage
1504 * *
1505 *********************************************************************************
1506 -}
1507
1508 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1509 topReactionsStage wi
1510 = do { inerts <- getTcSInerts
1511 ; tir <- doTopReact inerts wi
1512 ; case tir of
1513 ContinueWith wi -> return (ContinueWith wi)
1514 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1515
1516 doTopReact :: InertSet -> WorkItem -> TcS (StopOrContinue Ct)
1517 -- The work item does not react with the inert set, so try interaction with top-level
1518 -- instances. Note:
1519 --
1520 -- (a) The place to add superclasses in not here in doTopReact stage.
1521 -- Instead superclasses are added in the worklist as part of the
1522 -- canonicalization process. See Note [Adding superclasses].
1523 --
1524 -- (b) See Note [Given constraint that matches an instance declaration]
1525 -- for some design decisions for given dictionaries.
1526
1527 doTopReact inerts work_item
1528 = do { traceTcS "doTopReact" (ppr work_item)
1529 ; case work_item of
1530 CDictCan {} -> doTopReactDict inerts work_item
1531 CFunEqCan {} -> doTopReactFunEq work_item
1532 _ -> -- Any other work item does not react with any top-level equations
1533 return (ContinueWith work_item) }
1534
1535 --------------------
1536 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1537 -- Try to use type-class instance declarations to simplify the constraint
1538 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1539 , cc_tyargs = xis })
1540 | not (isWanted fl) -- Never use instances for Given or Derived constraints
1541 = try_fundeps_and_return
1542
1543 | Just ev <- lookupSolvedDict inerts loc cls xis -- Cached
1544 = do { setEvBind dict_id (ctEvTerm ev);
1545 ; stopWith fl "Dict/Top (cached)" }
1546
1547 | otherwise -- Not cached
1548 = do { lkup_inst_res <- matchClassInst inerts cls xis loc
1549 ; case lkup_inst_res of
1550 GenInst wtvs ev_term -> do { addSolvedDict fl cls xis
1551 ; solve_from_instance wtvs ev_term }
1552 NoInstance -> try_fundeps_and_return }
1553 where
1554 dict_id = ASSERT( isWanted fl ) ctEvId fl
1555 pred = mkClassPred cls xis
1556 loc = ctEvLoc fl
1557
1558 solve_from_instance :: [CtEvidence] -> EvTerm -> TcS (StopOrContinue Ct)
1559 -- Precondition: evidence term matches the predicate workItem
1560 solve_from_instance evs ev_term
1561 | null evs
1562 = do { traceTcS "doTopReact/found nullary instance for" $
1563 ppr dict_id
1564 ; setEvBind dict_id ev_term
1565 ; stopWith fl "Dict/Top (solved, no new work)" }
1566 | otherwise
1567 = do { traceTcS "doTopReact/found non-nullary instance for" $
1568 ppr dict_id
1569 ; setEvBind dict_id ev_term
1570 ; let mk_new_wanted ev
1571 = mkNonCanonical (ev {ctev_loc = bumpCtLocDepth CountConstraints loc })
1572 ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1573 ; stopWith fl "Dict/Top (solved, more work)" }
1574
1575 -- We didn't solve it; so try functional dependencies with
1576 -- the instance environment, and return
1577 -- NB: even if there *are* some functional dependencies against the
1578 -- instance environment, there might be a unique match, and if
1579 -- so we make sure we get on and solve it first. See Note [Weird fundeps]
1580 try_fundeps_and_return
1581 = do { instEnvs <- getInstEnvs
1582 ; let fd_eqns :: [Equation CtLoc]
1583 fd_eqns = [ fd { fd_loc = loc { ctl_origin = FunDepOrigin2 pred (ctl_origin loc)
1584 inst_pred inst_loc } }
1585 | fd@(FDEqn { fd_loc = inst_loc, fd_pred1 = inst_pred })
1586 <- improveFromInstEnv instEnvs pred ]
1587 ; rewriteWithFunDeps fd_eqns
1588 ; continueWith work_item }
1589
1590 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1591
1592 --------------------
1593 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1594 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1595 , cc_tyargs = args , cc_fsk = fsk })
1596 = ASSERT(isTypeFamilyTyCon fam_tc) -- No associated data families
1597 -- have reached this far
1598 ASSERT( not (isDerived old_ev) ) -- CFunEqCan is never Derived
1599 -- Look up in top-level instances, or built-in axiom
1600 do { match_res <- matchFam fam_tc args -- See Note [MATCHING-SYNONYMS]
1601 ; case match_res of {
1602 Nothing -> do { try_improvement; continueWith work_item } ;
1603 Just (ax_co, rhs_ty)
1604
1605 -- Found a top-level instance
1606
1607 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1608 , isTypeFamilyTyCon tc
1609 , tc_args `lengthIs` tyConArity tc -- Short-cut
1610 -> shortCutReduction old_ev fsk ax_co tc tc_args
1611 -- Try shortcut; see Note [Short cut for top-level reaction]
1612
1613 | isGiven old_ev -- Not shortcut
1614 -> do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1615 -- final_co :: fsk ~ rhs_ty
1616 ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
1617 EvCoercion final_co)
1618 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1619 ; stopWith old_ev "Fun/Top (given)" }
1620
1621 | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
1622 -> do { dischargeFmv (ctEvId old_ev) fsk ax_co rhs_ty
1623 ; traceTcS "doTopReactFunEq" $
1624 vcat [ text "old_ev:" <+> ppr old_ev
1625 , nest 2 (text ":=") <+> ppr ax_co ]
1626 ; stopWith old_ev "Fun/Top (wanted)" }
1627
1628 | otherwise -- We must not assign ufsk := ...ufsk...!
1629 -> do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1630 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred alpha_ty rhs_ty)
1631 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1632 -- ax_co :: fam_tc args ~ rhs_ty
1633 -- ev :: alpha ~ rhs_ty
1634 -- ufsk := alpha
1635 -- final_co :: fam_tc args ~ alpha
1636 ; dischargeFmv (ctEvId old_ev) fsk final_co alpha_ty
1637 ; traceTcS "doTopReactFunEq (occurs)" $
1638 vcat [ text "old_ev:" <+> ppr old_ev
1639 , nest 2 (text ":=") <+> ppr final_co
1640 , text "new_ev:" <+> ppr new_ev ]
1641 ; emitWorkNC [new_ev]
1642 -- By emitting this as non-canonical, we deal with all
1643 -- flattening, occurs-check, and ufsk := ufsk issues
1644 ; stopWith old_ev "Fun/Top (wanted)" } } }
1645 where
1646 loc = ctEvLoc old_ev
1647 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1648
1649 try_improvement
1650 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1651 = do { inert_eqs <- getInertEqs
1652 ; let eqns = sfInteractTop ops args (lookupFlattenTyVar inert_eqs fsk)
1653 ; mapM_ (emitNewDerivedEq loc) eqns }
1654 | otherwise
1655 = return ()
1656
1657 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1658
1659 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1660 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1661 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1662 | isGiven old_ev
1663 = do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
1664 -- ax_co :: F args ~ G tc_args
1665 -- cos :: xis ~ tc_args
1666 -- old_ev :: F args ~ fsk
1667 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1668
1669 ; new_ev <- newGivenEvVar deeper_loc
1670 ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1671 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1672 `mkTcTransCo` mkTcSymCo ax_co
1673 `mkTcTransCo` ctEvCoercion old_ev) )
1674
1675 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1676 ; updWorkListTcS (extendWorkListFunEq new_ct)
1677 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1678
1679 | otherwise
1680 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1681 do { (xis, cos) <- flattenMany (FE { fe_ev = old_ev, fe_mode = FM_FlattenAll }) tc_args
1682 -- ax_co :: F args ~ G tc_args
1683 -- cos :: xis ~ tc_args
1684 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1685 -- new_ev :: G xis ~ fsk
1686 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1687
1688 ; new_ev <- newWantedEvVarNC loc (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
1689 ; setEvBind (ctEvId old_ev)
1690 (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1691 `mkTcTransCo` ctEvCoercion new_ev))
1692
1693 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1694 ; updWorkListTcS (extendWorkListFunEq new_ct)
1695 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1696 where
1697 loc = ctEvLoc old_ev
1698 deeper_loc = bumpCtLocDepth CountTyFunApps loc
1699
1700 dischargeFmv :: EvVar -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1701 -- (dischargeFmv x fmv co ty)
1702 -- [W] x :: F tys ~ fuv
1703 -- co :: F tys ~ ty
1704 -- Precondition: fuv is not filled, and fuv `notElem` ty
1705 --
1706 -- Then set fuv := ty,
1707 -- set x := co
1708 -- kick out any inert things that are now rewritable
1709 dischargeFmv evar fmv co xi
1710 = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr evar $$ ppr fmv $$ ppr xi )
1711 do { setWantedTyBind fmv xi
1712 ; setEvBind evar (EvCoercion co)
1713 ; n_kicked <- kickOutRewritable givenFlavour fmv
1714 ; traceTcS "dischargeFuv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1715
1716 {-
1717 Note [Cached solved FunEqs]
1718 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1719 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1720 to see if we have reduced (FunExpensive big-type) before, lest we
1721 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1722 we must use `canRewriteOrSame` because both uses might (say) be Wanteds,
1723 and we *still* want to save the re-computation.
1724
1725 Note [MATCHING-SYNONYMS]
1726 ~~~~~~~~~~~~~~~~~~~~~~~~
1727 When trying to match a dictionary (D tau) to a top-level instance, or a
1728 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1729 we do *not* need to expand type synonyms because the matcher will do that for us.
1730
1731
1732 Note [RHS-FAMILY-SYNONYMS]
1733 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1734 The RHS of a family instance is represented as yet another constructor which is
1735 like a type synonym for the real RHS the programmer declared. Eg:
1736 type instance F (a,a) = [a]
1737 Becomes:
1738 :R32 a = [a] -- internal type synonym introduced
1739 F (a,a) ~ :R32 a -- instance
1740
1741 When we react a family instance with a type family equation in the work list
1742 we keep the synonym-using RHS without expansion.
1743
1744 Note [FunDep and implicit parameter reactions]
1745 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1746 Currently, our story of interacting two dictionaries (or a dictionary
1747 and top-level instances) for functional dependencies, and implicit
1748 paramters, is that we simply produce new Derived equalities. So for example
1749
1750 class D a b | a -> b where ...
1751 Inert:
1752 d1 :g D Int Bool
1753 WorkItem:
1754 d2 :w D Int alpha
1755
1756 We generate the extra work item
1757 cv :d alpha ~ Bool
1758 where 'cv' is currently unused. However, this new item can perhaps be
1759 spontaneously solved to become given and react with d2,
1760 discharging it in favour of a new constraint d2' thus:
1761 d2' :w D Int Bool
1762 d2 := d2' |> D Int cv
1763 Now d2' can be discharged from d1
1764
1765 We could be more aggressive and try to *immediately* solve the dictionary
1766 using those extra equalities, but that requires those equalities to carry
1767 evidence and derived do not carry evidence.
1768
1769 If that were the case with the same inert set and work item we might dischard
1770 d2 directly:
1771
1772 cv :w alpha ~ Bool
1773 d2 := d1 |> D Int cv
1774
1775 But in general it's a bit painful to figure out the necessary coercion,
1776 so we just take the first approach. Here is a better example. Consider:
1777 class C a b c | a -> b
1778 And:
1779 [Given] d1 : C T Int Char
1780 [Wanted] d2 : C T beta Int
1781 In this case, it's *not even possible* to solve the wanted immediately.
1782 So we should simply output the functional dependency and add this guy
1783 [but NOT its superclasses] back in the worklist. Even worse:
1784 [Given] d1 : C T Int beta
1785 [Wanted] d2: C T beta Int
1786 Then it is solvable, but its very hard to detect this on the spot.
1787
1788 It's exactly the same with implicit parameters, except that the
1789 "aggressive" approach would be much easier to implement.
1790
1791 Note [When improvement happens]
1792 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1793 We fire an improvement rule when
1794
1795 * Two constraints match (modulo the fundep)
1796 e.g. C t1 t2, C t1 t3 where C a b | a->b
1797 The two match because the first arg is identical
1798
1799 Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
1800 superclass of a Wanted goal) or if both are Given.
1801
1802 Example (tcfail138)
1803 class L a b | a -> b
1804 class (G a, L a b) => C a b
1805
1806 instance C a b' => G (Maybe a)
1807 instance C a b => C (Maybe a) a
1808 instance L (Maybe a) a
1809
1810 When solving the superclasses of the (C (Maybe a) a) instance, we get
1811 Given: C a b ... and hance by superclasses, (G a, L a b)
1812 Wanted: G (Maybe a)
1813 Use the instance decl to get
1814 Wanted: C a b'
1815 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1816 and now we need improvement between that derived superclass an the Given (L a b)
1817
1818 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
1819 emit Derived FDs for givens as well.
1820
1821 Note [Weird fundeps]
1822 ~~~~~~~~~~~~~~~~~~~~
1823 Consider class Het a b | a -> b where
1824 het :: m (f c) -> a -> m b
1825
1826 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1827 instance GHet (K a) (K [a])
1828 instance Het a b => GHet (K a) (K b)
1829
1830 The two instances don't actually conflict on their fundeps,
1831 although it's pretty strange. So they are both accepted. Now
1832 try [W] GHet (K Int) (K Bool)
1833 This triggers fudeps from both instance decls; but it also
1834 matches a *unique* instance decl, and we should go ahead and
1835 pick that one right now. Otherwise, if we don't, it ends up
1836 unsolved in the inert set and is reported as an error.
1837
1838 Trac #7875 is a case in point.
1839
1840 Note [Overriding implicit parameters]
1841 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1842 Consider
1843 f :: (?x::a) -> Bool -> a
1844
1845 g v = let ?x::Int = 3
1846 in (f v, let ?x::Bool = True in f v)
1847
1848 This should probably be well typed, with
1849 g :: Bool -> (Int, Bool)
1850
1851 So the inner binding for ?x::Bool *overrides* the outer one.
1852 Hence a work-item Given overrides an inert-item Given.
1853
1854 Note [Given constraint that matches an instance declaration]
1855 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1856 What should we do when we discover that one (or more) top-level
1857 instances match a given (or solved) class constraint? We have
1858 two possibilities:
1859
1860 1. Reject the program. The reason is that there may not be a unique
1861 best strategy for the solver. Example, from the OutsideIn(X) paper:
1862 instance P x => Q [x]
1863 instance (x ~ y) => R [x] y
1864
1865 wob :: forall a b. (Q [b], R b a) => a -> Int
1866
1867 g :: forall a. Q [a] => [a] -> Int
1868 g x = wob x
1869
1870 will generate the impliation constraint:
1871 Q [a] => (Q [beta], R beta [a])
1872 If we react (Q [beta]) with its top-level axiom, we end up with a
1873 (P beta), which we have no way of discharging. On the other hand,
1874 if we react R beta [a] with the top-level we get (beta ~ a), which
1875 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1876 now solvable by the given Q [a].
1877
1878 However, this option is restrictive, for instance [Example 3] from
1879 Note [Recursive instances and superclases] will fail to work.
1880
1881 2. Ignore the problem, hoping that the situations where there exist indeed
1882 such multiple strategies are rare: Indeed the cause of the previous
1883 problem is that (R [x] y) yields the new work (x ~ y) which can be
1884 *spontaneously* solved, not using the givens.
1885
1886 We are choosing option 2 below but we might consider having a flag as well.
1887
1888
1889 Note [New Wanted Superclass Work]
1890 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1891 Even in the case of wanted constraints, we may add some superclasses
1892 as new given work. The reason is:
1893
1894 To allow FD-like improvement for type families. Assume that
1895 we have a class
1896 class C a b | a -> b
1897 and we have to solve the implication constraint:
1898 C a b => C a beta
1899 Then, FD improvement can help us to produce a new wanted (beta ~ b)
1900
1901 We want to have the same effect with the type family encoding of
1902 functional dependencies. Namely, consider:
1903 class (F a ~ b) => C a b
1904 Now suppose that we have:
1905 given: C a b
1906 wanted: C a beta
1907 By interacting the given we will get given (F a ~ b) which is not
1908 enough by itself to make us discharge (C a beta). However, we
1909 may create a new derived equality from the super-class of the
1910 wanted constraint (C a beta), namely derived (F a ~ beta).
1911 Now we may interact this with given (F a ~ b) to get:
1912 derived : beta ~ b
1913 But 'beta' is a touchable unification variable, and hence OK to
1914 unify it with 'b', replacing the derived evidence with the identity.
1915
1916 This requires trySpontaneousSolve to solve *derived*
1917 equalities that have a touchable in their RHS, *in addition*
1918 to solving wanted equalities.
1919
1920 We also need to somehow use the superclasses to quantify over a minimal,
1921 constraint see note [Minimize by Superclasses] in TcSimplify.
1922
1923
1924 Finally, here is another example where this is useful.
1925
1926 Example 1:
1927 ----------
1928 class (F a ~ b) => C a b
1929 And we are given the wanteds:
1930 w1 : C a b
1931 w2 : C a c
1932 w3 : b ~ c
1933 We surely do *not* want to quantify over (b ~ c), since if someone provides
1934 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1935 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1936
1937 Step 1: We will get new *given* superclass work,
1938 provisionally to our solving of w1 and w2
1939
1940 g1: F a ~ b, g2 : F a ~ c,
1941 w1 : C a b, w2 : C a c, w3 : b ~ c
1942
1943 The evidence for g1 and g2 is a superclass evidence term:
1944
1945 g1 := sc w1, g2 := sc w2
1946
1947 Step 2: The givens will solve the wanted w3, so that
1948 w3 := sym (sc w1) ; sc w2
1949
1950 Step 3: Now, one may naively assume that then w2 can be solve from w1
1951 after rewriting with the (now solved equality) (b ~ c).
1952
1953 But this rewriting is ruled out by the isGoodRectDict!
1954
1955 Conclusion, we will (correctly) end up with the unsolved goals
1956 (C a b, C a c)
1957
1958 NB: The desugarer needs be more clever to deal with equalities
1959 that participate in recursive dictionary bindings.
1960 -}
1961
1962 data LookupInstResult
1963 = NoInstance
1964 | GenInst [CtEvidence] EvTerm
1965
1966 instance Outputable LookupInstResult where
1967 ppr NoInstance = text "NoInstance"
1968 ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
1969
1970
1971 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1972
1973 matchClassInst _ clas [ ty ] _
1974 | className clas == knownNatClassName
1975 , Just n <- isNumLitTy ty = makeDict (EvNum n)
1976
1977 | className clas == knownSymbolClassName
1978 , Just s <- isStrLitTy ty = makeDict (EvStr s)
1979
1980 where
1981 {- This adds a coercion that will convert the literal into a dictionary
1982 of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1983 in TcEvidence. The coercion happens in 2 steps:
1984
1985 Integer -> SNat n -- representation of literal to singleton
1986 SNat n -> KnownNat n -- singleton to dictionary
1987
1988 The process is mirrored for Symbols:
1989 String -> SSymbol n
1990 SSymbol n -> KnownSymbol n
1991 -}
1992 makeDict evLit
1993 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1994 -- co_dict :: KnownNat n ~ SNat n
1995 , [ meth ] <- classMethods clas
1996 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1997 $ funResultTy -- SNat n
1998 $ dropForAlls -- KnownNat n => SNat n
1999 $ idType meth -- forall n. KnownNat n => SNat n
2000 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
2001 -- SNat n ~ Integer
2002 = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep)))
2003
2004 | otherwise
2005 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
2006 $$ vcat (map (ppr . idType) (classMethods clas)))
2007
2008 matchClassInst _ clas [ _k, ty1, ty2 ] loc
2009 | clas == coercibleClass
2010 = do { traceTcS "matchClassInst for" $
2011 quotes (pprClassPred clas [ty1,ty2]) <+> text "at depth" <+> ppr (ctLocDepth loc)
2012 ; ev <- getCoercibleInst loc ty1 ty2
2013 ; traceTcS "matchClassInst returned" $ ppr ev
2014 ; return ev }
2015
2016 matchClassInst inerts clas tys loc
2017 = do { dflags <- getDynFlags
2018 ; tclvl <- getTcLevel
2019 ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
2020 , text "inerts=" <+> ppr inerts
2021 , text "untouchables=" <+> ppr tclvl ]
2022 ; instEnvs <- getInstEnvs
2023 ; case lookupInstEnv instEnvs clas tys of
2024 ([], _, _) -- Nothing matches
2025 -> do { traceTcS "matchClass not matching" $
2026 vcat [ text "dict" <+> ppr pred ]
2027 ; return NoInstance }
2028
2029 ([(ispec, inst_tys)], [], _) -- A single match
2030 | not (xopt Opt_IncoherentInstances dflags)
2031 , given_overlap tclvl
2032 -> -- See Note [Instance and Given overlap]
2033 do { traceTcS "Delaying instance application" $
2034 vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
2035 , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
2036 ; return NoInstance }
2037
2038 | otherwise
2039 -> do { let dfun_id = instanceDFunId ispec
2040 ; traceTcS "matchClass success" $
2041 vcat [text "dict" <+> ppr pred,
2042 text "witness" <+> ppr dfun_id
2043 <+> ppr (idType dfun_id) ]
2044 -- Record that this dfun is needed
2045 ; match_one dfun_id inst_tys }
2046
2047 (matches, _, _) -- More than one matches
2048 -- Defer any reactions of a multitude
2049 -- until we learn more about the reagent
2050 -> do { traceTcS "matchClass multiple matches, deferring choice" $
2051 vcat [text "dict" <+> ppr pred,
2052 text "matches" <+> ppr matches]
2053 ; return NoInstance } }
2054 where
2055 pred = mkClassPred clas tys
2056
2057 match_one :: DFunId -> [Maybe TcType] -> TcS LookupInstResult
2058 -- See Note [DFunInstType: instantiating types] in InstEnv
2059 match_one dfun_id mb_inst_tys
2060 = do { checkWellStagedDFun pred dfun_id loc
2061 ; (tys, dfun_phi) <- instDFunType dfun_id mb_inst_tys
2062 ; let (theta, _) = tcSplitPhiTy dfun_phi
2063 ; if null theta then
2064 return (GenInst [] (EvDFunApp dfun_id tys []))
2065 else do
2066 { evc_vars <- instDFunConstraints loc theta
2067 ; let new_ev_vars = freshGoals evc_vars
2068 -- new_ev_vars are only the real new variables that can be emitted
2069 dfun_app = EvDFunApp dfun_id tys (map (ctEvTerm . fst) evc_vars)
2070 ; return $ GenInst new_ev_vars dfun_app } }
2071
2072 givens_for_this_clas :: Cts
2073 givens_for_this_clas
2074 = filterBag isGivenCt (findDictsByClass (inert_dicts $ inert_cans inerts) clas)
2075
2076 given_overlap :: TcLevel -> Bool
2077 given_overlap tclvl = anyBag (matchable tclvl) givens_for_this_clas
2078
2079 matchable tclvl (CDictCan { cc_class = clas_g, cc_tyargs = sys
2080 , cc_ev = fl })
2081 | isGiven fl
2082 = ASSERT( clas_g == clas )
2083 case tcUnifyTys (\tv -> if isTouchableMetaTyVar tclvl tv &&
2084 tv `elemVarSet` tyVarsOfTypes tys
2085 then BindMe else Skolem) tys sys of
2086 -- We can't learn anything more about any variable at this point, so the only
2087 -- cause of overlap can be by an instantiation of a touchable unification
2088 -- variable. Hence we only bind touchable unification variables. In addition,
2089 -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
2090 Nothing -> False
2091 Just _ -> True
2092 | otherwise = False -- No overlap with a solved, already been taken care of
2093 -- by the overlap check with the instance environment.
2094 matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
2095
2096 -- See Note [Coercible Instances]
2097 -- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
2098 getCoercibleInst :: CtLoc -> TcType -> TcType -> TcS LookupInstResult
2099 getCoercibleInst loc ty1 ty2
2100 = do { -- Get some global stuff in scope, for nice pattern-guard based code in `go`
2101 rdr_env <- getGlobalRdrEnvTcS
2102 ; famenv <- getFamInstEnvs
2103 ; go famenv rdr_env }
2104 where
2105 go :: FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult
2106 go famenv rdr_env
2107 -- Also see [Order of Coercible Instances]
2108
2109 -- Coercible a a (see case 1 in [Coercible Instances])
2110 | ty1 `tcEqType` ty2
2111 = return $ GenInst []
2112 $ EvCoercion (TcRefl Representational ty1)
2113
2114 -- Coercible (forall a. ty) (forall a. ty') (see case 2 in [Coercible Instances])
2115 | tcIsForAllTy ty1
2116 , tcIsForAllTy ty2
2117 , let (tvs1,body1) = tcSplitForAllTys ty1
2118 (tvs2,body2) = tcSplitForAllTys ty2
2119 , equalLength tvs1 tvs2
2120 = do { ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2)
2121 ; return $ GenInst [] ev_term }
2122
2123 -- Coercible NT a (see case 3 in [Coercible Instances])
2124 | Just (rep_tc, conc_ty, nt_co) <- tcInstNewTyConTF_maybe famenv ty1
2125 , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon
2126 = do { markDataConsAsUsed rdr_env rep_tc
2127 ; (new_goals, residual_co) <- requestCoercible loc conc_ty ty2
2128 ; let final_co = nt_co `mkTcTransCo` residual_co
2129 -- nt_co :: ty1 ~R conc_ty
2130 -- residual_co :: conc_ty ~R ty2
2131 ; return $ GenInst new_goals (EvCoercion final_co) }
2132
2133 -- Coercible a NT (see case 3 in [Coercible Instances])
2134 | Just (rep_tc, conc_ty, nt_co) <- tcInstNewTyConTF_maybe famenv ty2
2135 , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon
2136 = do { markDataConsAsUsed rdr_env rep_tc
2137 ; (new_goals, residual_co) <- requestCoercible loc ty1 conc_ty
2138 ; let final_co = residual_co `mkTcTransCo` mkTcSymCo nt_co
2139 ; return $ GenInst new_goals (EvCoercion final_co) }
2140
2141 -- Coercible (D ty1 ty2) (D ty1' ty2') (see case 4 in [Coercible Instances])
2142 | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1
2143 , Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2
2144 , tc1 == tc2
2145 , nominalArgsAgree tc1 tyArgs1 tyArgs2
2146 = do { -- We want evidence for all type arguments of role R
2147 arg_stuff <- forM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \ (r,ta1,ta2) ->
2148 case r of
2149 Representational -> requestCoercible loc ta1 ta2
2150 Phantom -> return ([], TcPhantomCo ta1 ta2)
2151 Nominal -> return ([], mkTcNomReflCo ta1)
2152 -- ta1 == ta2, due to nominalArgsAgree
2153 ; let (new_goals_s, arg_cos) = unzip arg_stuff
2154 final_co = mkTcTyConAppCo Representational tc1 arg_cos
2155 ; return $ GenInst (concat new_goals_s) (EvCoercion final_co) }
2156
2157 -- Cannot solve this one
2158 | otherwise
2159 = return NoInstance
2160
2161 nominalArgsAgree :: TyCon -> [Type] -> [Type] -> Bool
2162 nominalArgsAgree tc tys1 tys2 = all ok $ zip3 (tyConRoles tc) tys1 tys2
2163 where ok (r,t1,t2) = r /= Nominal || t1 `tcEqType` t2
2164
2165 dataConsInScope :: GlobalRdrEnv -> TyCon -> Bool
2166 dataConsInScope rdr_env tc = not hidden_data_cons
2167 where
2168 data_con_names = map dataConName (tyConDataCons tc)
2169 hidden_data_cons = not (isWiredInName (tyConName tc)) &&
2170 (isAbstractTyCon tc || any not_in_scope data_con_names)
2171 not_in_scope dc = null (lookupGRE_Name rdr_env dc)
2172
2173 markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
2174 markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
2175 [ mkRdrQual (is_as (is_decl imp_spec)) occ
2176 | dc <- tyConDataCons tc
2177 , let dc_name = dataConName dc
2178 occ = nameOccName dc_name
2179 gres = lookupGRE_Name rdr_env dc_name
2180 , not (null gres)
2181 , Imported (imp_spec:_) <- [gre_prov (head gres)] ]
2182
2183 requestCoercible :: CtLoc -> TcType -> TcType
2184 -> TcS ( [CtEvidence] -- Fresh goals to solve
2185 , TcCoercion ) -- Coercion witnessing (Coercible t1 t2)
2186 requestCoercible loc ty1 ty2
2187 = ASSERT2( typeKind ty1 `tcEqKind` typeKind ty2, ppr ty1 <+> ppr ty2)
2188 do { (new_ev, freshness) <- newWantedEvVar loc' (mkCoerciblePred ty1 ty2)
2189 ; return ( case freshness of { Fresh -> [new_ev]; Cached -> [] }
2190 , ctEvCoercion new_ev) }
2191 -- Evidence for a Coercible constraint is always a coercion t1 ~R t2
2192 where
2193 loc' = bumpCtLocDepth CountConstraints loc
2194
2195 {-
2196 Note [Coercible Instances]
2197 ~~~~~~~~~~~~~~~~~~~~~~~~~~
2198 The class Coercible is special: There are no regular instances, and the user
2199 cannot even define them (it is listed as an `abstractClass` in TcValidity).
2200 Instead, the type checker will create instances and their evidence out of thin
2201 air, in getCoercibleInst. The following "instances" are present:
2202
2203 1. instance Coercible a a
2204 for any type a at any kind k.
2205
2206 2. instance (forall a. Coercible t1 t2) => Coercible (forall a. t1) (forall a. t2)
2207 (which would be illegal to write like that in the source code, but we have
2208 it nevertheless).
2209
2210 3. instance Coercible r b => Coercible (NT t1 t2 ...) b
2211 instance Coercible a r => Coercible a (NT t1 t2 ...)
2212 for a newtype constructor NT (or data family instance that resolves to a
2213 newtype) where
2214 * r is the concrete type of NT, instantiated with the arguments t1 t2 ...
2215 * the constructor of NT is in scope.
2216
2217 The newtype TyCon can appear undersaturated, but only if it has
2218 enough arguments to apply the newtype coercion (which is eta-reduced). Examples:
2219 newtype NT a = NT (Either a Int)
2220 Coercible (NT Int) (Either Int Int) -- ok
2221 newtype NT2 a b = NT2 (b -> a)
2222 newtype NT3 a b = NT3 (b -> a)
2223 Coercible (NT2 Int) (NT3 Int) -- cannot be derived
2224
2225 4. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) =>
2226 Coercible (C t1_r t2_r ... t1_p t2_p ... t1_n t2_n ...)
2227 (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...)
2228 for a type constructor C where
2229 * the nominal type arguments are not changed,
2230 * the phantom type arguments may change arbitrarily
2231 * the representational type arguments are again Coercible
2232
2233 The type constructor can be used undersaturated; then the Coercible
2234 instance is at a higher kind. This does not cause problems.
2235
2236
2237 The type checker generates evidence in the form of EvCoercion, but the
2238 TcCoercion therein has role Representational, which are turned into Core
2239 coercions by dsEvTerm in DsBinds.
2240
2241 The evidence for the second case is created by deferTcSForAllEq, for the other
2242 cases by getCoercibleInst.
2243
2244 When the constraint cannot be solved, it is treated as any other unsolved
2245 constraint, i.e. it can turn up in an inferred type signature, or reported to
2246 the user as a regular "Cannot derive instance ..." error. In the latter case,
2247 coercible_msg in TcErrors gives additional explanations of why GHC could not
2248 find a Coercible instance, so it duplicates some of the logic from
2249 getCoercibleInst (in negated form).
2250
2251 Note [Order of Coercible Instances]
2252 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2253 At first glance, the order of the various coercible instances doesn't matter, as
2254 incoherence is no issue here: We do not care how the evidence is constructed,
2255 as long as it is.
2256
2257 But because of role annotations, the order *can* matter:
2258
2259 newtype T a = MkT [a]
2260 type role T nominal
2261
2262 type family F a
2263 type instance F Int = Bool
2264
2265 Here T's declared role is more restrictive than its inferred role
2266 (representational) would be. If MkT is not in scope, so that the
2267 newtype-unwrapping instance is not available, then this coercible
2268 instance would fail:
2269 Coercible (T Bool) (T (F Int)
2270 But MkT was in scope, *and* if we used it before decomposing on T,
2271 we'd unwrap the newtype (on both sides) to get
2272 Coercible Bool (F Int)
2273 whic succeeds.
2274
2275 So our current decision is to apply case 3 (newtype-unwrapping) first,
2276 followed by decomposition (case 4). This is strictly more powerful
2277 if the newtype constructor is in scope. See Trac #9117 for a discussion.
2278
2279 Note [Instance and Given overlap]
2280 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2281 Assume that we have an inert set that looks as follows:
2282 [Given] D [Int]
2283 And an instance declaration:
2284 instance C a => D [a]
2285 A new wanted comes along of the form:
2286 [Wanted] D [alpha]
2287
2288 One possibility is to apply the instance declaration which will leave us
2289 with an unsolvable goal (C alpha). However, later on a new constraint may
2290 arise (for instance due to a functional dependency between two later dictionaries),
2291 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
2292 will be transformed to [Wanted] D [Int], which could have been discharged by the given.
2293
2294 The solution is that in matchClassInst and eventually in topReact, we get back with
2295 a matching instance, only when there is no Given in the inerts which is unifiable to
2296 this particular dictionary.
2297
2298 The end effect is that, much as we do for overlapping instances, we delay choosing a
2299 class instance if there is a possibility of another instance OR a given to match our
2300 constraint later on. This fixes bugs #4981 and #5002.
2301
2302 This is arguably not easy to appear in practice due to our aggressive prioritization
2303 of equality solving over other constraints, but it is possible. I've added a test case
2304 in typecheck/should-compile/GivenOverlapping.hs
2305
2306 We ignore the overlap problem if -XIncoherentInstances is in force: see
2307 Trac #6002 for a worked-out example where this makes a difference.
2308
2309 Moreover notice that our goals here are different than the goals of the top-level
2310 overlapping checks. There we are interested in validating the following principle:
2311
2312 If we inline a function f at a site where the same global instance environment
2313 is available as the instance environment at the definition site of f then we
2314 should get the same behaviour.
2315
2316 But for the Given Overlap check our goal is just related to completeness of
2317 constraint solving.
2318 -}