Generate Typeable info at definition sites
[ghc.git] / compiler / typecheck / TcInteract.hs
1 {-# LANGUAGE CPP #-}
2
3 module TcInteract (
4 solveSimpleGivens, -- Solves [EvVar],GivenLoc
5 solveSimpleWanteds -- Solves Cts
6 ) where
7
8 #include "HsVersions.h"
9
10 import BasicTypes ( infinity, IntWithInf, intGtLimit )
11 import HsTypes ( hsIPNameFS )
12 import FastString
13 import TcCanonical
14 import TcFlatten
15 import VarSet
16 import Type
17 import Kind ( isKind )
18 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
19 import CoAxiom( sfInteractTop, sfInteractInert )
20
21 import Var
22 import TcType
23 import Name
24 import PrelNames ( knownNatClassName, knownSymbolClassName,
25 callStackTyConKey, typeableClassName )
26 import TysWiredIn ( ipClass, typeNatKind, typeSymbolKind )
27 import Id( idType )
28 import CoAxiom ( Eqn, CoAxiom(..), CoAxBranch(..), fromBranches )
29 import Class
30 import TyCon
31 import DataCon( dataConWrapId )
32 import FunDeps
33 import FamInst
34 import FamInstEnv
35 import Inst( tyVarsOfCt )
36 import Unify ( tcUnifyTyWithTFs )
37
38 import TcEvidence
39 import Outputable
40
41 import TcRnTypes
42 import TcSMonad
43 import Bag
44 import MonadUtils ( concatMapM )
45
46 import Data.List( partition, foldl', deleteFirstsBy )
47 import SrcLoc
48 import VarEnv
49
50 import Control.Monad
51 import Maybes( isJust )
52 import Pair (Pair(..))
53 import Unique( hasKey )
54 import DynFlags
55 import Util
56
57 {-
58 **********************************************************************
59 * *
60 * Main Interaction Solver *
61 * *
62 **********************************************************************
63
64 Note [Basic Simplifier Plan]
65 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
66 1. Pick an element from the WorkList if there exists one with depth
67 less than our context-stack depth.
68
69 2. Run it down the 'stage' pipeline. Stages are:
70 - canonicalization
71 - inert reactions
72 - spontaneous reactions
73 - top-level intreactions
74 Each stage returns a StopOrContinue and may have sideffected
75 the inerts or worklist.
76
77 The threading of the stages is as follows:
78 - If (Stop) is returned by a stage then we start again from Step 1.
79 - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
80 the next stage in the pipeline.
81 4. If the element has survived (i.e. ContinueWith x) the last stage
82 then we add him in the inerts and jump back to Step 1.
83
84 If in Step 1 no such element exists, we have exceeded our context-stack
85 depth and will simply fail.
86
87 Note [Unflatten after solving the simple wanteds]
88 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
89 We unflatten after solving the wc_simples of an implication, and before attempting
90 to float. This means that
91
92 * The fsk/fmv flatten-skolems only survive during solveSimples. We don't
93 need to worry about them across successive passes over the constraint tree.
94 (E.g. we don't need the old ic_fsk field of an implication.
95
96 * When floating an equality outwards, we don't need to worry about floating its
97 associated flattening constraints.
98
99 * Another tricky case becomes easy: Trac #4935
100 type instance F True a b = a
101 type instance F False a b = b
102
103 [w] F c a b ~ gamma
104 (c ~ True) => a ~ gamma
105 (c ~ False) => b ~ gamma
106
107 Obviously this is soluble with gamma := F c a b, and unflattening
108 will do exactly that after solving the simple constraints and before
109 attempting the implications. Before, when we were not unflattening,
110 we had to push Wanted funeqs in as new givens. Yuk!
111
112 Another example that becomes easy: indexed_types/should_fail/T7786
113 [W] BuriedUnder sub k Empty ~ fsk
114 [W] Intersect fsk inv ~ s
115 [w] xxx[1] ~ s
116 [W] forall[2] . (xxx[1] ~ Empty)
117 => Intersect (BuriedUnder sub k Empty) inv ~ Empty
118
119 Note [Running plugins on unflattened wanteds]
120 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
121 There is an annoying mismatch between solveSimpleGivens and
122 solveSimpleWanteds, because the latter needs to fiddle with the inert
123 set, unflatten and zonk the wanteds. It passes the zonked wanteds
124 to runTcPluginsWanteds, which produces a replacement set of wanteds,
125 some additional insolubles and a flag indicating whether to go round
126 the loop again. If so, prepareInertsForImplications is used to remove
127 the previous wanteds (which will still be in the inert set). Note
128 that prepareInertsForImplications will discard the insolubles, so we
129 must keep track of them separately.
130 -}
131
132 solveSimpleGivens :: CtLoc -> [EvVar] -> TcS Cts
133 -- Solves the givens, adding them to the inert set
134 -- Returns any insoluble givens, which represent inaccessible code,
135 -- taking those ones out of the inert set
136 solveSimpleGivens loc givens
137 | null givens -- Shortcut for common case
138 = return emptyCts
139 | otherwise
140 = do { go (map mk_given_ct givens)
141 ; takeGivenInsolubles }
142 where
143 mk_given_ct ev_id = mkNonCanonical (CtGiven { ctev_evar = ev_id
144 , ctev_pred = evVarPred ev_id
145 , ctev_loc = loc })
146 go givens = do { solveSimples (listToBag givens)
147 ; new_givens <- runTcPluginsGiven
148 ; when (notNull new_givens) (go new_givens)
149 }
150
151 solveSimpleWanteds :: Cts -> TcS WantedConstraints
152 -- NB: 'simples' may contain /derived/ equalities, floated
153 -- out from a nested implication. So don't discard deriveds!
154 solveSimpleWanteds simples
155 = do { traceTcS "solveSimples {" (ppr simples)
156 ; dflags <- getDynFlags
157 ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
158 ; traceTcS "solveSimples end }" $
159 vcat [ ptext (sLit "iterations =") <+> ppr n
160 , ptext (sLit "residual =") <+> ppr wc ]
161 ; return wc }
162 where
163 go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
164 go n limit wc
165 | n `intGtLimit` limit
166 = failTcS (hang (ptext (sLit "solveSimpleWanteds: too many iterations")
167 <+> parens (ptext (sLit "limit =") <+> ppr limit))
168 2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
169 , ptext (sLit "Simples =") <+> ppr simples
170 , ptext (sLit "WC =") <+> ppr wc ]))
171
172 | isEmptyBag (wc_simple wc)
173 = return (n,wc)
174
175 | otherwise
176 = do { -- Solve
177 (unif_count, wc1) <- solve_simple_wanteds wc
178
179 -- Run plugins
180 ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
181 -- See Note [Running plugins on unflattened wanteds]
182
183 ; if unif_count == 0 && not rerun_plugin
184 then return (n, wc2) -- Done
185 else do { traceTcS "solveSimple going round again:" (ppr rerun_plugin)
186 ; go (n+1) limit wc2 } } -- Loop
187
188
189 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
190 -- Try solving these constraints
191 -- Affects the unification state (of course) but not the inert set
192 solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
193 = nestTcS $
194 do { solveSimples simples1
195 ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
196 ; (unif_count, unflattened_eqs) <- reportUnifications $
197 unflatten tv_eqs fun_eqs
198 -- See Note [Unflatten after solving the simple wanteds]
199 ; return ( unif_count
200 , WC { wc_simple = others `andCts` unflattened_eqs
201 , wc_insol = insols1 `andCts` insols2
202 , wc_impl = implics1 `unionBags` implics2 }) }
203
204 {- Note [The solveSimpleWanteds loop]
205 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
206 Solving a bunch of simple constraints is done in a loop,
207 (the 'go' loop of 'solveSimpleWanteds'):
208 1. Try to solve them; unflattening may lead to improvement that
209 was not exploitable during solving
210 2. Try the plugin
211 3. If step 1 did improvement during unflattening; or if the plugin
212 wants to run again, go back to step 1
213
214 Non-obviously, improvement can also take place during
215 the unflattening that takes place in step (1). See TcFlatten,
216 See Note [Unflattening can force the solver to iterate]
217 -}
218
219 -- The main solver loop implements Note [Basic Simplifier Plan]
220 ---------------------------------------------------------------
221 solveSimples :: Cts -> TcS ()
222 -- Returns the final InertSet in TcS
223 -- Has no effect on work-list or residual-implications
224 -- The constraints are initially examined in left-to-right order
225
226 solveSimples cts
227 = {-# SCC "solveSimples" #-}
228 do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
229 ; solve_loop }
230 where
231 solve_loop
232 = {-# SCC "solve_loop" #-}
233 do { sel <- selectNextWorkItem
234 ; case sel of
235 Nothing -> return ()
236 Just ct -> do { runSolverPipeline thePipeline ct
237 ; solve_loop } }
238
239 -- | Extract the (inert) givens and invoke the plugins on them.
240 -- Remove solved givens from the inert set and emit insolubles, but
241 -- return new work produced so that 'solveSimpleGivens' can feed it back
242 -- into the main solver.
243 runTcPluginsGiven :: TcS [Ct]
244 runTcPluginsGiven
245 = do { plugins <- getTcPlugins
246 ; if null plugins then return [] else
247 do { givens <- getInertGivens
248 ; if null givens then return [] else
249 do { p <- runTcPlugins plugins (givens,[],[])
250 ; let (solved_givens, _, _) = pluginSolvedCts p
251 ; updInertCans (removeInertCts solved_givens)
252 ; mapM_ emitInsoluble (pluginBadCts p)
253 ; return (pluginNewCts p) } } }
254
255 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
256 -- them and produce an updated bag of wanteds (possibly with some new
257 -- work) and a bag of insolubles. The boolean indicates whether
258 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
259 -- main solver.
260 runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
261 runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
262 | isEmptyBag simples1
263 = return (False, wc)
264 | otherwise
265 = do { plugins <- getTcPlugins
266 ; if null plugins then return (False, wc) else
267
268 do { given <- getInertGivens
269 ; simples1 <- zonkSimples simples1 -- Plugin requires zonked inputs
270 ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
271 ; p <- runTcPlugins plugins (given, derived, wanted)
272 ; let (_, _, solved_wanted) = pluginSolvedCts p
273 (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
274 new_wanted = pluginNewCts p
275
276 -- SLPJ: I'm deeply suspicious of this
277 -- ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
278
279 ; mapM_ setEv solved_wanted
280 ; return ( notNull (pluginNewCts p)
281 , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
282 `andCts` listToBag unsolved_derived
283 , wc_insol = listToBag (pluginBadCts p) `andCts` insols1
284 , wc_impl = implics1 } ) } }
285 where
286 setEv :: (EvTerm,Ct) -> TcS ()
287 setEv (ev,ct) = case ctEvidence ct of
288 CtWanted {ctev_evar = evar} -> setWantedEvBind evar ev
289 _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
290
291 -- | A triple of (given, derived, wanted) constraints to pass to plugins
292 type SplitCts = ([Ct], [Ct], [Ct])
293
294 -- | A solved triple of constraints, with evidence for wanteds
295 type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])
296
297 -- | Represents collections of constraints generated by typechecker
298 -- plugins
299 data TcPluginProgress = TcPluginProgress
300 { pluginInputCts :: SplitCts
301 -- ^ Original inputs to the plugins with solved/bad constraints
302 -- removed, but otherwise unmodified
303 , pluginSolvedCts :: SolvedCts
304 -- ^ Constraints solved by plugins
305 , pluginBadCts :: [Ct]
306 -- ^ Constraints reported as insoluble by plugins
307 , pluginNewCts :: [Ct]
308 -- ^ New constraints emitted by plugins
309 }
310
311 getTcPlugins :: TcS [TcPluginSolver]
312 getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }
313
314 -- | Starting from a triple of (given, derived, wanted) constraints,
315 -- invoke each of the typechecker plugins in turn and return
316 --
317 -- * the remaining unmodified constraints,
318 -- * constraints that have been solved,
319 -- * constraints that are insoluble, and
320 -- * new work.
321 --
322 -- Note that new work generated by one plugin will not be seen by
323 -- other plugins on this pass (but the main constraint solver will be
324 -- re-invoked and they will see it later). There is no check that new
325 -- work differs from the original constraints supplied to the plugin:
326 -- the plugin itself should perform this check if necessary.
327 runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
328 runTcPlugins plugins all_cts
329 = foldM do_plugin initialProgress plugins
330 where
331 do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
332 do_plugin p solver = do
333 result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
334 return $ progress p result
335
336 progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
337 progress p (TcPluginContradiction bad_cts) =
338 p { pluginInputCts = discard bad_cts (pluginInputCts p)
339 , pluginBadCts = bad_cts ++ pluginBadCts p
340 }
341 progress p (TcPluginOk solved_cts new_cts) =
342 p { pluginInputCts = discard (map snd solved_cts) (pluginInputCts p)
343 , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
344 , pluginNewCts = new_cts ++ pluginNewCts p
345 }
346
347 initialProgress = TcPluginProgress all_cts ([], [], []) [] []
348
349 discard :: [Ct] -> SplitCts -> SplitCts
350 discard cts (xs, ys, zs) =
351 (xs `without` cts, ys `without` cts, zs `without` cts)
352
353 without :: [Ct] -> [Ct] -> [Ct]
354 without = deleteFirstsBy eqCt
355
356 eqCt :: Ct -> Ct -> Bool
357 eqCt c c' = case (ctEvidence c, ctEvidence c') of
358 (CtGiven pred _ _, CtGiven pred' _ _) -> pred `eqType` pred'
359 (CtWanted pred _ _, CtWanted pred' _ _) -> pred `eqType` pred'
360 (CtDerived pred _ , CtDerived pred' _ ) -> pred `eqType` pred'
361 (_ , _ ) -> False
362
363 add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
364 add xs scs = foldl' addOne scs xs
365
366 addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
367 addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
368 CtGiven {} -> (ct:givens, deriveds, wanteds)
369 CtDerived{} -> (givens, ct:deriveds, wanteds)
370 CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)
371
372
373 type WorkItem = Ct
374 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
375
376 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
377 -> WorkItem -- The work item
378 -> TcS ()
379 -- Run this item down the pipeline, leaving behind new work and inerts
380 runSolverPipeline pipeline workItem
381 = do { initial_is <- getTcSInerts
382 ; traceTcS "Start solver pipeline {" $
383 vcat [ ptext (sLit "work item = ") <+> ppr workItem
384 , ptext (sLit "inerts = ") <+> ppr initial_is]
385
386 ; bumpStepCountTcS -- One step for each constraint processed
387 ; final_res <- run_pipeline pipeline (ContinueWith workItem)
388
389 ; final_is <- getTcSInerts
390 ; case final_res of
391 Stop ev s -> do { traceFireTcS ev s
392 ; traceTcS "End solver pipeline (discharged) }"
393 (ptext (sLit "inerts =") <+> ppr final_is)
394 ; return () }
395 ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
396 ; traceTcS "End solver pipeline (kept as inert) }" $
397 vcat [ ptext (sLit "final_item =") <+> ppr ct
398 , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
399 , ptext (sLit "inerts =") <+> ppr final_is]
400 ; addInertCan ct }
401 }
402 where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue Ct
403 -> TcS (StopOrContinue Ct)
404 run_pipeline [] res = return res
405 run_pipeline _ (Stop ev s) = return (Stop ev s)
406 run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
407 = do { traceTcS ("runStage " ++ stg_name ++ " {")
408 (text "workitem = " <+> ppr ct)
409 ; res <- stg ct
410 ; traceTcS ("end stage " ++ stg_name ++ " }") empty
411 ; run_pipeline stgs res }
412
413 {-
414 Example 1:
415 Inert: {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
416 Reagent: a ~ [b] (given)
417
418 React with (c~d) ==> IR (ContinueWith (a~[b])) True []
419 React with (F a ~ t) ==> IR (ContinueWith (a~[b])) False [F [b] ~ t]
420 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True []
421
422 Example 2:
423 Inert: {c ~w d, F a ~g t, b ~w Int, a ~w ty}
424 Reagent: a ~w [b]
425
426 React with (c ~w d) ==> IR (ContinueWith (a~[b])) True []
427 React with (F a ~g t) ==> IR (ContinueWith (a~[b])) True [] (can't rewrite given with wanted!)
428 etc.
429
430 Example 3:
431 Inert: {a ~ Int, F Int ~ b} (given)
432 Reagent: F a ~ b (wanted)
433
434 React with (a ~ Int) ==> IR (ContinueWith (F Int ~ b)) True []
435 React with (F Int ~ b) ==> IR Stop True [] -- after substituting we re-canonicalize and get nothing
436 -}
437
438 thePipeline :: [(String,SimplifierStage)]
439 thePipeline = [ ("canonicalization", TcCanonical.canonicalize)
440 , ("interact with inerts", interactWithInertsStage)
441 , ("top-level reactions", topReactionsStage) ]
442
443 {-
444 *********************************************************************************
445 * *
446 The interact-with-inert Stage
447 * *
448 *********************************************************************************
449
450 Note [The Solver Invariant]
451 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
452 We always add Givens first. So you might think that the solver has
453 the invariant
454
455 If the work-item is Given,
456 then the inert item must Given
457
458 But this isn't quite true. Suppose we have,
459 c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
460 After processing the first two, we get
461 c1: [G] beta ~ [alpha], c2 : [W] blah
462 Now, c3 does not interact with the the given c1, so when we spontaneously
463 solve c3, we must re-react it with the inert set. So we can attempt a
464 reaction between inert c2 [W] and work-item c3 [G].
465
466 It *is* true that [Solver Invariant]
467 If the work-item is Given,
468 AND there is a reaction
469 then the inert item must Given
470 or, equivalently,
471 If the work-item is Given,
472 and the inert item is Wanted/Derived
473 then there is no reaction
474 -}
475
476 -- Interaction result of WorkItem <~> Ct
477
478 type StopNowFlag = Bool -- True <=> stop after this interaction
479
480 interactWithInertsStage :: WorkItem -> TcS (StopOrContinue Ct)
481 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
482 -- react with anything at this stage.
483
484 interactWithInertsStage wi
485 = do { inerts <- getTcSInerts
486 ; let ics = inert_cans inerts
487 ; case wi of
488 CTyEqCan {} -> interactTyVarEq ics wi
489 CFunEqCan {} -> interactFunEq ics wi
490 CIrredEvCan {} -> interactIrred ics wi
491 CDictCan {} -> interactDict ics wi
492 _ -> pprPanic "interactWithInerts" (ppr wi) }
493 -- CHoleCan are put straight into inert_frozen, so never get here
494 -- CNonCanonical have been canonicalised
495
496 data InteractResult
497 = IRKeep -- Keep the existing inert constraint in the inert set
498 | IRReplace -- Replace the existing inert constraint with the work item
499 | IRDelete -- Delete the existing inert constraint from the inert set
500
501 instance Outputable InteractResult where
502 ppr IRKeep = ptext (sLit "keep")
503 ppr IRReplace = ptext (sLit "replace")
504 ppr IRDelete = ptext (sLit "delete")
505
506 solveOneFromTheOther :: CtEvidence -- Inert
507 -> CtEvidence -- WorkItem
508 -> TcS (InteractResult, StopNowFlag)
509 -- Preconditions:
510 -- 1) inert and work item represent evidence for the /same/ predicate
511 -- 2) ip/class/irred evidence (no coercions) only
512 solveOneFromTheOther ev_i ev_w
513 | isDerived ev_w -- Work item is Derived; just discard it
514 = return (IRKeep, True)
515
516 | isDerived ev_i -- The inert item is Derived, we can just throw it away,
517 = return (IRDelete, False) -- The ev_w is inert wrt earlier inert-set items,
518 -- so it's safe to continue on from this point
519
520 | CtWanted { ctev_loc = loc_w } <- ev_w
521 , prohibitedSuperClassSolve (ctEvLoc ev_i) loc_w
522 = return (IRDelete, False)
523
524 | CtWanted { ctev_evar = ev_id } <- ev_w -- Inert is Given or Wanted
525 = do { setWantedEvBind ev_id (ctEvTerm ev_i)
526 ; return (IRKeep, True) }
527
528 | CtWanted { ctev_loc = loc_i } <- ev_i -- Work item is Given
529 , prohibitedSuperClassSolve (ctEvLoc ev_w) loc_i
530 = return (IRKeep, False) -- Just discard the un-usable Given
531 -- This never actually happens because
532 -- Givens get processed first
533
534 | CtWanted { ctev_evar = ev_id } <- ev_i -- Work item is Given
535 = do { setWantedEvBind ev_id (ctEvTerm ev_w)
536 ; return (IRReplace, True) }
537
538 -- So they are both Given
539 -- See Note [Replacement vs keeping]
540 | lvl_i == lvl_w
541 = do { binds <- getTcEvBindsMap
542 ; return (same_level_strategy binds, True) }
543
544 | otherwise -- Both are Given, levels differ
545 = return (different_level_strategy, True)
546 where
547 pred = ctEvPred ev_i
548 loc_i = ctEvLoc ev_i
549 loc_w = ctEvLoc ev_w
550 lvl_i = ctLocLevel loc_i
551 lvl_w = ctLocLevel loc_w
552
553 different_level_strategy
554 | isIPPred pred, lvl_w > lvl_i = IRReplace
555 | lvl_w < lvl_i = IRReplace
556 | otherwise = IRKeep
557
558 same_level_strategy binds -- Both Given
559 | GivenOrigin (InstSC s_i) <- ctLocOrigin loc_i
560 = case ctLocOrigin loc_w of
561 GivenOrigin (InstSC s_w) | s_w < s_i -> IRReplace
562 | otherwise -> IRKeep
563 _ -> IRReplace
564
565 | GivenOrigin (InstSC {}) <- ctLocOrigin loc_w
566 = IRKeep
567
568 | has_binding binds ev_w
569 , not (has_binding binds ev_i)
570 = IRReplace
571
572 | otherwise = IRKeep
573
574 has_binding binds ev = isJust (lookupEvBind binds (ctEvId ev))
575
576 {-
577 Note [Replacement vs keeping]
578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
579 When we have two Given constraints both of type (C tys), say, which should
580 we keep? More subtle than you might think!
581
582 * Constraints come from different levels (different_level_strategy)
583
584 - For implicit parameters we want to keep the innermost (deepest)
585 one, so that it overrides the outer one.
586 See Note [Shadowing of Implicit Parameters]
587
588 - For everything else, we want to keep the outermost one. Reason: that
589 makes it more likely that the inner one will turn out to be unused,
590 and can be reported as redundant. See Note [Tracking redundant constraints]
591 in TcSimplify.
592
593 It transpires that using the outermost one is reponsible for an
594 8% performance improvement in nofib cryptarithm2, compared to
595 just rolling the dice. I didn't investigate why.
596
597 * Constaints coming from the same level (i.e. same implication)
598
599 - Always get rid of InstSC ones if possible, since they are less
600 useful for solving. If both are InstSC, choose the one with
601 the smallest TypeSize
602 See Note [Solving superclass constraints] in TcInstDcls
603
604 - Keep the one that has a non-trivial evidence binding.
605 Note [Tracking redundant constraints] again.
606 Example: f :: (Eq a, Ord a) => blah
607 then we may find [G] sc_sel (d1::Ord a) :: Eq a
608 [G] d2 :: Eq a
609 We want to discard d2 in favour of the superclass selection from
610 the Ord dictionary.
611
612 * Finally, when there is still a choice, use IRKeep rather than
613 IRReplace, to avoid unnecessary munging of the inert set.
614
615 Doing the depth-check for implicit parameters, rather than making the work item
616 always overrride, is important. Consider
617
618 data T a where { T1 :: (?x::Int) => T Int; T2 :: T a }
619
620 f :: (?x::a) => T a -> Int
621 f T1 = ?x
622 f T2 = 3
623
624 We have a [G] (?x::a) in the inert set, and at the pattern match on T1 we add
625 two new givens in the work-list: [G] (?x::Int)
626 [G] (a ~ Int)
627 Now consider these steps
628 - process a~Int, kicking out (?x::a)
629 - process (?x::Int), the inner given, adding to inert set
630 - process (?x::a), the outer given, overriding the inner given
631 Wrong! The depth-check ensures that the inner implicit parameter wins.
632 (Actually I think that the order in which the work-list is processed means
633 that this chain of events won't happen, but that's very fragile.)
634
635 *********************************************************************************
636 * *
637 interactIrred
638 * *
639 *********************************************************************************
640 -}
641
642 -- Two pieces of irreducible evidence: if their types are *exactly identical*
643 -- we can rewrite them. We can never improve using this:
644 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
645 -- mean that (ty1 ~ ty2)
646 interactIrred :: InertCans -> Ct -> TcS (StopOrContinue Ct)
647
648 interactIrred inerts workItem@(CIrredEvCan { cc_ev = ev_w })
649 | let pred = ctEvPred ev_w
650 (matching_irreds, others) = partitionBag (\ct -> ctPred ct `tcEqType` pred)
651 (inert_irreds inerts)
652 , (ct_i : rest) <- bagToList matching_irreds
653 , let ctev_i = ctEvidence ct_i
654 = ASSERT( null rest )
655 do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
656 ; case inert_effect of
657 IRKeep -> return ()
658 IRDelete -> updInertIrreds (\_ -> others)
659 IRReplace -> updInertIrreds (\_ -> others `snocCts` workItem)
660 -- These const upd's assume that solveOneFromTheOther
661 -- has no side effects on InertCans
662 ; if stop_now then
663 return (Stop ev_w (ptext (sLit "Irred equal") <+> parens (ppr inert_effect)))
664 ; else
665 continueWith workItem }
666
667 | otherwise
668 = continueWith workItem
669
670 interactIrred _ wi = pprPanic "interactIrred" (ppr wi)
671
672 {-
673 *********************************************************************************
674 * *
675 interactDict
676 * *
677 *********************************************************************************
678 -}
679
680 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
681 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
682 -- don't ever try to solve CallStack IPs directly from other dicts,
683 -- we always build new dicts instead.
684 -- See Note [Overview of implicit CallStacks]
685 | Just mkEvCs <- isCallStackIP (ctEvLoc ev_w) cls tys
686 , isWanted ev_w
687 = do let ev_cs =
688 case lookupInertDict inerts cls tys of
689 Just ev | isGiven ev -> mkEvCs (ctEvTerm ev)
690 _ -> mkEvCs (EvCallStack EvCsEmpty)
691
692 -- now we have ev_cs :: CallStack, but the evidence term should
693 -- be a dictionary, so we have to coerce ev_cs to a
694 -- dictionary for `IP ip CallStack`
695 let ip_ty = mkClassPred cls tys
696 let ev_tm = mkEvCast (EvCallStack ev_cs) (TcCoercion $ wrapIP ip_ty)
697 addSolvedDict ev_w cls tys
698 setWantedEvBind (ctEvId ev_w) ev_tm
699 stopWith ev_w "Wanted CallStack IP"
700
701 | Just ctev_i <- lookupInertDict inerts cls tys
702 = do { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
703 ; case inert_effect of
704 IRKeep -> return ()
705 IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
706 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
707 ; if stop_now then
708 return (Stop ev_w (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
709 else
710 continueWith workItem }
711
712 | cls == ipClass
713 , isGiven ev_w
714 = interactGivenIP inerts workItem
715
716 | otherwise
717 = do { addFunDepWork inerts ev_w cls
718 ; continueWith workItem }
719
720 interactDict _ wi = pprPanic "interactDict" (ppr wi)
721
722 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
723 -- Add derived constraints from type-class functional dependencies.
724 addFunDepWork inerts work_ev cls
725 = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
726 -- No need to check flavour; fundeps work between
727 -- any pair of constraints, regardless of flavour
728 -- Importantly we don't throw workitem back in the
729 -- worklist because this can cause loops (see #5236)
730 where
731 work_pred = ctEvPred work_ev
732 work_loc = ctEvLoc work_ev
733 add_fds inert_ct
734 = emitFunDepDeriveds $
735 improveFromAnother derived_loc inert_pred work_pred
736 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
737 -- NB: We do create FDs for given to report insoluble equations that arise
738 -- from pairs of Givens, and also because of floating when we approximate
739 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
740 where
741 inert_pred = ctPred inert_ct
742 inert_loc = ctLoc inert_ct
743 derived_loc = work_loc { ctl_origin = FunDepOrigin1 work_pred work_loc
744 inert_pred inert_loc }
745
746 {-
747 **********************************************************************
748 * *
749 Implicit parameters
750 * *
751 **********************************************************************
752 -}
753
754 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
755 -- Work item is Given (?x:ty)
756 -- See Note [Shadowing of Implicit Parameters]
757 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
758 , cc_tyargs = tys@(ip_str:_) })
759 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
760 ; stopWith ev "Given IP" }
761 where
762 dicts = inert_dicts inerts
763 ip_dicts = findDictsByClass dicts cls
764 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
765 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
766
767 -- Pick out any Given constraints for the same implicit parameter
768 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
769 = isGiven ev && ip_str `tcEqType` ip_str'
770 is_this_ip _ = False
771
772 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
773
774 -- | Is the constraint for an implicit CallStack parameter?
775 -- i.e. (IP "name" CallStack)
776 isCallStackIP :: CtLoc -> Class -> [Type] -> Maybe (EvTerm -> EvCallStack)
777 isCallStackIP loc cls tys
778 | cls == ipClass
779 , [_ip_name, ty] <- tys
780 , Just (tc, _) <- splitTyConApp_maybe ty
781 , tc `hasKey` callStackTyConKey
782 = occOrigin (ctLocOrigin loc)
783 | otherwise
784 = Nothing
785 where
786 locSpan = ctLocSpan loc
787
788 -- We only want to grab constraints that arose due to the use of an IP or a
789 -- function call. See Note [Overview of implicit CallStacks]
790 occOrigin (OccurrenceOf n) = Just (EvCsPushCall n locSpan)
791 occOrigin (IPOccOrigin n) = Just (EvCsTop ('?' `consFS` hsIPNameFS n) locSpan)
792 occOrigin _ = Nothing
793
794 {-
795 Note [Shadowing of Implicit Parameters]
796 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
797 Consider the following example:
798
799 f :: (?x :: Char) => Char
800 f = let ?x = 'a' in ?x
801
802 The "let ?x = ..." generates an implication constraint of the form:
803
804 ?x :: Char => ?x :: Char
805
806 Furthermore, the signature for `f` also generates an implication
807 constraint, so we end up with the following nested implication:
808
809 ?x :: Char => (?x :: Char => ?x :: Char)
810
811 Note that the wanted (?x :: Char) constraint may be solved in
812 two incompatible ways: either by using the parameter from the
813 signature, or by using the local definition. Our intention is
814 that the local definition should "shadow" the parameter of the
815 signature, and we implement this as follows: when we add a new
816 *given* implicit parameter to the inert set, it replaces any existing
817 givens for the same implicit parameter.
818
819 This works for the normal cases but it has an odd side effect
820 in some pathological programs like this:
821
822 -- This is accepted, the second parameter shadows
823 f1 :: (?x :: Int, ?x :: Char) => Char
824 f1 = ?x
825
826 -- This is rejected, the second parameter shadows
827 f2 :: (?x :: Int, ?x :: Char) => Int
828 f2 = ?x
829
830 Both of these are actually wrong: when we try to use either one,
831 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
832 which would lead to an error.
833
834 I can think of two ways to fix this:
835
836 1. Simply disallow multiple constratits for the same implicit
837 parameter---this is never useful, and it can be detected completely
838 syntactically.
839
840 2. Move the shadowing machinery to the location where we nest
841 implications, and add some code here that will produce an
842 error if we get multiple givens for the same implicit parameter.
843
844
845 **********************************************************************
846 * *
847 interactFunEq
848 * *
849 **********************************************************************
850 -}
851
852 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
853 -- Try interacting the work item with the inert set
854 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
855 , cc_tyargs = args, cc_fsk = fsk })
856 | Just (CFunEqCan { cc_ev = ev_i, cc_fsk = fsk_i }) <- matching_inerts
857 = if ev_i `canDischarge` ev
858 then -- Rewrite work-item using inert
859 do { traceTcS "reactFunEq (discharge work item):" $
860 vcat [ text "workItem =" <+> ppr workItem
861 , text "inertItem=" <+> ppr ev_i ]
862 ; reactFunEq ev_i fsk_i ev fsk
863 ; stopWith ev "Inert rewrites work item" }
864 else -- Rewrite inert using work-item
865 ASSERT2( ev `canDischarge` ev_i, ppr ev $$ ppr ev_i )
866 do { traceTcS "reactFunEq (rewrite inert item):" $
867 vcat [ text "workItem =" <+> ppr workItem
868 , text "inertItem=" <+> ppr ev_i ]
869 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
870 -- Do the updInertFunEqs before the reactFunEq, so that
871 -- we don't kick out the inertItem as well as consuming it!
872 ; reactFunEq ev fsk ev_i fsk_i
873 ; stopWith ev "Work item rewrites inert" }
874
875 | otherwise -- Try improvement
876 = do { improveLocalFunEqs loc inerts tc args fsk
877 ; continueWith workItem }
878 where
879 loc = ctEvLoc ev
880 funeqs = inert_funeqs inerts
881 matching_inerts = findFunEqs funeqs tc args
882
883 interactFunEq _ workItem = pprPanic "interactFunEq" (ppr workItem)
884
885 improveLocalFunEqs :: CtLoc -> InertCans -> TyCon -> [TcType] -> TcTyVar
886 -> TcS ()
887 -- Generate derived improvement equalities, by comparing
888 -- the current work item with inert CFunEqs
889 -- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y'
890 improveLocalFunEqs loc inerts fam_tc args fsk
891 | not (null improvement_eqns)
892 = do { traceTcS "interactFunEq improvements: " $
893 vcat [ ptext (sLit "Eqns:") <+> ppr improvement_eqns
894 , ptext (sLit "Candidates:") <+> ppr funeqs_for_tc
895 , ptext (sLit "TvEqs:") <+> ppr tv_eqs ]
896 ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
897 | otherwise
898 = return ()
899 where
900 tv_eqs = inert_model inerts
901 funeqs = inert_funeqs inerts
902 funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
903 rhs = lookupFlattenTyVar tv_eqs fsk
904
905 --------------------
906 improvement_eqns
907 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
908 = -- Try built-in families, notably for arithmethic
909 concatMap (do_one_built_in ops) funeqs_for_tc
910
911 | Injective injective_args <- familyTyConInjectivityInfo fam_tc
912 = -- Try improvement from type families with injectivity annotations
913 concatMap (do_one_injective injective_args) funeqs_for_tc
914
915 | otherwise
916 = []
917
918 --------------------
919 do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
920 = sfInteractInert ops args rhs iargs (lookupFlattenTyVar tv_eqs ifsk)
921 do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
922
923 --------------------
924 -- See Note [Type inference for type families with injectivity]
925 do_one_injective injective_args
926 (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
927 | rhs `tcEqType` lookupFlattenTyVar tv_eqs ifsk
928 = [Pair arg iarg | (arg, iarg, True)
929 <- zip3 args iargs injective_args ]
930 | otherwise
931 = []
932 do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
933
934 -------------
935 lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
936 -- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
937 -- this is used only when dealing with a CFunEqCan
938 lookupFlattenTyVar model ftv
939 = case lookupVarEnv model ftv of
940 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
941 _ -> mkTyVarTy ftv
942
943 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F tys ~ fsk1
944 -> CtEvidence -> TcTyVar -- Solve this :: F tys ~ fsk2
945 -> TcS ()
946 reactFunEq from_this fsk1 (CtGiven { ctev_evar = evar, ctev_loc = loc }) fsk2
947 = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar)
948 `mkTcTransCo` ctEvCoercion from_this
949 -- :: fsk2 ~ fsk1
950 fsk_eq_pred = mkTcEqPred (mkTyVarTy fsk2) (mkTyVarTy fsk1)
951 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
952 ; emitWorkNC [new_ev] }
953
954 reactFunEq from_this fuv1 ev fuv2
955 = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2)
956 ; dischargeFmv ev fuv2 (ctEvCoercion from_this) (mkTyVarTy fuv1)
957 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fuv1 $$ ppr ev $$ ppr fuv2) }
958
959 {-
960 Note [Type inference for type families with injectivity]
961 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
962 Suppose we have a type family with an injectivity annotation:
963 type family F a b = r | r -> b
964
965 Then if we have two CFunEqCan constraints for F with the same RHS
966 F s1 t1 ~ rhs
967 F s2 t2 ~ rhs
968 then we can use the injectivity to get a new Derived constraint on
969 the injective argument
970 [D] t1 ~ t2
971
972 That in turn can help GHC solve constraints that would otherwise require
973 guessing. For example, consider the ambiguity check for
974 f :: F Int b -> Int
975 We get the constraint
976 [W] F Int b ~ F Int beta
977 where beta is a unification variable. Injectivity lets us pick beta ~ b.
978
979 Injectivity information is also used at the call sites. For example:
980 g = f True
981 gives rise to
982 [W] F Int b ~ Bool
983 from which we can derive b. This requires looking at the defining equations of
984 a type family, ie. finding equation with a matching RHS (Bool in this example)
985 and infering values of type variables (b in this example) from the LHS patterns
986 of the matching equation. For closed type families we have to perform
987 additional apartness check for the selected equation to check that the selected
988 is guaranteed to fire for given LHS arguments.
989
990 These new constraints are simply *Derived* constraints; they have no evidence.
991 We could go further and offer evidence from decomposing injective type-function
992 applications, but that would require new evidence forms, and an extension to
993 FC, so we don't do that right now (Dec 14).
994
995 See also Note [Injective type families] in TyCon
996
997
998 Note [Cache-caused loops]
999 ~~~~~~~~~~~~~~~~~~~~~~~~~
1000 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1001 solved cache (which is the default behaviour or xCtEvidence), because the interaction
1002 may not be contributing towards a solution. Here is an example:
1003
1004 Initial inert set:
1005 [W] g1 : F a ~ beta1
1006 Work item:
1007 [W] g2 : F a ~ beta2
1008 The work item will react with the inert yielding the _same_ inert set plus:
1009 i) Will set g2 := g1 `cast` g3
1010 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
1011 iii) Will emit [W] g3 : beta1 ~ beta2
1012 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
1013 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
1014 will set
1015 g1 := g ; sym g3
1016 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
1017 remember that we have this in our solved cache, and it is ... g2! In short we
1018 created the evidence loop:
1019
1020 g2 := g1 ; g3
1021 g3 := refl
1022 g1 := g2 ; sym g3
1023
1024 To avoid this situation we do not cache as solved any workitems (or inert)
1025 which did not really made a 'step' towards proving some goal. Solved's are
1026 just an optimization so we don't lose anything in terms of completeness of
1027 solving.
1028
1029
1030 Note [Efficient Orientation]
1031 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1032 Suppose we are interacting two FunEqCans with the same LHS:
1033 (inert) ci :: (F ty ~ xi_i)
1034 (work) cw :: (F ty ~ xi_w)
1035 We prefer to keep the inert (else we pass the work item on down
1036 the pipeline, which is a bit silly). If we keep the inert, we
1037 will (a) discharge 'cw'
1038 (b) produce a new equality work-item (xi_w ~ xi_i)
1039 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
1040 new_work :: xi_w ~ xi_i
1041 cw := ci ; sym new_work
1042 Why? Consider the simplest case when xi1 is a type variable. If
1043 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
1044 If we generate xi2~xi1, there is less chance of that happening.
1045 Of course it can and should still happen if xi1=a, xi1=Int, say.
1046 But we want to avoid it happening needlessly.
1047
1048 Similarly, if we *can't* keep the inert item (because inert is Wanted,
1049 and work is Given, say), we prefer to orient the new equality (xi_i ~
1050 xi_w).
1051
1052 Note [Carefully solve the right CFunEqCan]
1053 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1054 ---- OLD COMMENT, NOW NOT NEEDED
1055 ---- because we now allow multiple
1056 ---- wanted FunEqs with the same head
1057 Consider the constraints
1058 c1 :: F Int ~ a -- Arising from an application line 5
1059 c2 :: F Int ~ Bool -- Arising from an application line 10
1060 Suppose that 'a' is a unification variable, arising only from
1061 flattening. So there is no error on line 5; it's just a flattening
1062 variable. But there is (or might be) an error on line 10.
1063
1064 Two ways to combine them, leaving either (Plan A)
1065 c1 :: F Int ~ a -- Arising from an application line 5
1066 c3 :: a ~ Bool -- Arising from an application line 10
1067 or (Plan B)
1068 c2 :: F Int ~ Bool -- Arising from an application line 10
1069 c4 :: a ~ Bool -- Arising from an application line 5
1070
1071 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
1072 on the *totally innocent* line 5. An example is test SimpleFail16
1073 where the expected/actual message comes out backwards if we use
1074 the wrong plan.
1075
1076 The second is the right thing to do. Hence the isMetaTyVarTy
1077 test when solving pairwise CFunEqCan.
1078
1079
1080 **********************************************************************
1081 * *
1082 interactTyVarEq
1083 * *
1084 **********************************************************************
1085 -}
1086
1087 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1088 -- CTyEqCans are always consumed, so always returns Stop
1089 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
1090 , cc_rhs = rhs
1091 , cc_ev = ev
1092 , cc_eq_rel = eq_rel })
1093 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1094 <- findTyEqs inerts tv
1095 , ev_i `canDischarge` ev
1096 , rhs_i `tcEqType` rhs ]
1097 = -- Inert: a ~ b
1098 -- Work item: a ~ b
1099 do { setEvBindIfWanted ev (ctEvTerm ev_i)
1100 ; stopWith ev "Solved from inert" }
1101
1102 | Just tv_rhs <- getTyVar_maybe rhs
1103 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1104 <- findTyEqs inerts tv_rhs
1105 , ev_i `canDischarge` ev
1106 , rhs_i `tcEqType` mkTyVarTy tv ]
1107 = -- Inert: a ~ b
1108 -- Work item: b ~ a
1109 do { setEvBindIfWanted ev
1110 (EvCoercion (mkTcSymCo (ctEvCoercion ev_i)))
1111 ; stopWith ev "Solved from inert (r)" }
1112
1113 | otherwise
1114 = do { tclvl <- getTcLevel
1115 ; if canSolveByUnification tclvl ev eq_rel tv rhs
1116 then do { solveByUnification ev tv rhs
1117 ; n_kicked <- kickOutAfterUnification tv
1118 ; return (Stop ev (ptext (sLit "Solved by unification") <+> ppr_kicked n_kicked)) }
1119
1120 else do { traceTcS "Can't solve tyvar equality"
1121 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1122 , ppWhen (isMetaTyVar tv) $
1123 nest 4 (text "TcLevel of" <+> ppr tv
1124 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
1125 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
1126 , text "TcLevel =" <+> ppr tclvl ])
1127 ; addInertEq workItem
1128 ; return (Stop ev (ptext (sLit "Kept as inert"))) } }
1129
1130 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1131
1132 -- @trySpontaneousSolve wi@ solves equalities where one side is a
1133 -- touchable unification variable.
1134 -- Returns True <=> spontaneous solve happened
1135 canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
1136 -> TcTyVar -> Xi -> Bool
1137 canSolveByUnification tclvl gw eq_rel tv xi
1138 | ReprEq <- eq_rel -- we never solve representational equalities this way.
1139 = False
1140
1141 | isGiven gw -- See Note [Touchables and givens]
1142 = False
1143
1144 | isTouchableMetaTyVar tclvl tv
1145 = case metaTyVarInfo tv of
1146 SigTv -> is_tyvar xi
1147 _ -> True
1148
1149 | otherwise -- Untouchable
1150 = False
1151 where
1152 is_tyvar xi
1153 = case tcGetTyVar_maybe xi of
1154 Nothing -> False
1155 Just tv -> case tcTyVarDetails tv of
1156 MetaTv { mtv_info = info }
1157 -> case info of
1158 SigTv -> True
1159 _ -> False
1160 SkolemTv {} -> True
1161 FlatSkol {} -> False
1162 RuntimeUnk -> True
1163
1164 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1165 -- Solve with the identity coercion
1166 -- Precondition: kind(xi) is a sub-kind of kind(tv)
1167 -- Precondition: CtEvidence is Wanted or Derived
1168 -- Precondition: CtEvidence is nominal
1169 -- Returns: workItem where
1170 -- workItem = the new Given constraint
1171 --
1172 -- NB: No need for an occurs check here, because solveByUnification always
1173 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1174 -- say that in (a ~ xi), the type variable a does not appear in xi.
1175 -- See TcRnTypes.Ct invariants.
1176 --
1177 -- Post: tv is unified (by side effect) with xi;
1178 -- we often write tv := xi
1179 solveByUnification wd tv xi
1180 = do { let tv_ty = mkTyVarTy tv
1181 ; traceTcS "Sneaky unification:" $
1182 vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
1183 text "Coercion:" <+> pprEq tv_ty xi,
1184 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1185 text "Right Kind is:" <+> ppr (typeKind xi) ]
1186
1187 ; let xi' = defaultKind xi
1188 -- We only instantiate kind unification variables
1189 -- with simple kinds like *, not OpenKind or ArgKind
1190 -- cf TcUnify.uUnboundKVar
1191
1192 ; unifyTyVar tv xi'
1193 ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi')) }
1194
1195 ppr_kicked :: Int -> SDoc
1196 ppr_kicked 0 = empty
1197 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
1198
1199 {- Note [Avoid double unifications]
1200 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1201 The spontaneous solver has to return a given which mentions the unified unification
1202 variable *on the left* of the equality. Here is what happens if not:
1203 Original wanted: (a ~ alpha), (alpha ~ Int)
1204 We spontaneously solve the first wanted, without changing the order!
1205 given : a ~ alpha [having unified alpha := a]
1206 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1207 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1208
1209 We avoid this problem by orienting the resulting given so that the unification
1210 variable is on the left. [Note that alternatively we could attempt to
1211 enforce this at canonicalization]
1212
1213 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1214 double unifications is the main reason we disallow touchable
1215 unification variables as RHS of type family equations: F xis ~ alpha.
1216
1217
1218 ************************************************************************
1219 * *
1220 * Functional dependencies, instantiation of equations
1221 * *
1222 ************************************************************************
1223
1224 When we spot an equality arising from a functional dependency,
1225 we now use that equality (a "wanted") to rewrite the work-item
1226 constraint right away. This avoids two dangers
1227
1228 Danger 1: If we send the original constraint on down the pipeline
1229 it may react with an instance declaration, and in delicate
1230 situations (when a Given overlaps with an instance) that
1231 may produce new insoluble goals: see Trac #4952
1232
1233 Danger 2: If we don't rewrite the constraint, it may re-react
1234 with the same thing later, and produce the same equality
1235 again --> termination worries.
1236
1237 To achieve this required some refactoring of FunDeps.hs (nicer
1238 now!).
1239 -}
1240
1241 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1242 emitFunDepDeriveds fd_eqns
1243 = mapM_ do_one_FDEqn fd_eqns
1244 where
1245 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1246 | null tvs -- Common shortcut
1247 = mapM_ (unifyDerived loc Nominal) eqs
1248 | otherwise
1249 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1250 ; mapM_ (do_one_eq loc subst) eqs }
1251
1252 do_one_eq loc subst (Pair ty1 ty2)
1253 = unifyDerived loc Nominal $
1254 Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
1255
1256 {-
1257 **********************************************************************
1258 * *
1259 The top-reaction Stage
1260 * *
1261 **********************************************************************
1262 -}
1263
1264 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1265 topReactionsStage wi
1266 = do { tir <- doTopReact wi
1267 ; case tir of
1268 ContinueWith wi -> continueWith wi
1269 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1270
1271 doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
1272 -- The work item does not react with the inert set, so try interaction with top-level
1273 -- instances. Note:
1274 --
1275 -- (a) The place to add superclasses in not here in doTopReact stage.
1276 -- Instead superclasses are added in the worklist as part of the
1277 -- canonicalization process. See Note [Adding superclasses].
1278
1279 doTopReact work_item
1280 = do { traceTcS "doTopReact" (ppr work_item)
1281 ; case work_item of
1282 CDictCan {} -> do { inerts <- getTcSInerts
1283 ; doTopReactDict inerts work_item }
1284 CFunEqCan {} -> doTopReactFunEq work_item
1285 _ -> -- Any other work item does not react with any top-level equations
1286 continueWith work_item }
1287
1288 --------------------
1289 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1290 -- Try to use type-class instance declarations to simplify the constraint
1291 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1292 , cc_tyargs = xis })
1293 | isGiven fl -- Never use instances for Given constraints
1294 = do { try_fundep_improvement
1295 ; continueWith work_item }
1296
1297 | Just ev <- lookupSolvedDict inerts cls xis -- Cached
1298 = do { setEvBindIfWanted fl (ctEvTerm ev);
1299 ; stopWith fl "Dict/Top (cached)" }
1300
1301 | isDerived fl -- Use type-class instances for Deriveds, in the hope
1302 -- of generating some improvements
1303 -- C.f. Example 3 of Note [The improvement story]
1304 -- It's easy because no evidence is involved
1305 = do { dflags <- getDynFlags
1306 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
1307 ; case lkup_inst_res of
1308 GenInst preds _ s -> do { emitNewDeriveds dict_loc preds
1309 ; unless s $
1310 insertSafeOverlapFailureTcS work_item
1311 ; stopWith fl "Dict/Top (solved)" }
1312
1313 NoInstance -> do { -- If there is no instance, try improvement
1314 try_fundep_improvement
1315 ; continueWith work_item } }
1316
1317 | otherwise -- Wanted, but not cached
1318 = do { dflags <- getDynFlags
1319 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
1320 ; case lkup_inst_res of
1321 GenInst theta mk_ev s -> do { addSolvedDict fl cls xis
1322 ; unless s $
1323 insertSafeOverlapFailureTcS work_item
1324 ; solve_from_instance theta mk_ev }
1325 NoInstance -> do { try_fundep_improvement
1326 ; continueWith work_item } }
1327 where
1328 dict_pred = mkClassPred cls xis
1329 dict_loc = ctEvLoc fl
1330 dict_origin = ctLocOrigin dict_loc
1331 deeper_loc = zap_origin (bumpCtLocDepth dict_loc)
1332
1333 zap_origin loc -- After applying an instance we can set ScOrigin to
1334 -- infinity, so that prohibitedSuperClassSolve never fires
1335 | ScOrigin {} <- dict_origin
1336 = setCtLocOrigin loc (ScOrigin infinity)
1337 | otherwise
1338 = loc
1339
1340 solve_from_instance :: [TcPredType] -> ([EvId] -> EvTerm) -> TcS (StopOrContinue Ct)
1341 -- Precondition: evidence term matches the predicate workItem
1342 solve_from_instance theta mk_ev
1343 | null theta
1344 = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
1345 ; setWantedEvBind (ctEvId fl) (mk_ev [])
1346 ; stopWith fl "Dict/Top (solved, no new work)" }
1347 | otherwise
1348 = do { checkReductionDepth deeper_loc dict_pred
1349 ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
1350 ; evc_vars <- mapM (newWantedEvVar deeper_loc) theta
1351 ; setWantedEvBind (ctEvId fl) (mk_ev (map (ctEvId . fst) evc_vars))
1352 ; emitWorkNC (freshGoals evc_vars)
1353 ; stopWith fl "Dict/Top (solved, more work)" }
1354
1355 -- We didn't solve it; so try functional dependencies with
1356 -- the instance environment, and return
1357 -- See also Note [Weird fundeps]
1358 try_fundep_improvement
1359 = do { traceTcS "try_fundeps" (ppr work_item)
1360 ; instEnvs <- getInstEnvs
1361 ; emitFunDepDeriveds $
1362 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
1363
1364 mk_ct_loc :: PredType -- From instance decl
1365 -> SrcSpan -- also from instance deol
1366 -> CtLoc
1367 mk_ct_loc inst_pred inst_loc
1368 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
1369 inst_pred inst_loc }
1370
1371 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1372
1373 --------------------
1374 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1375 doTopReactFunEq work_item = do { fam_envs <- getFamInstEnvs
1376 ; do_top_fun_eq fam_envs work_item }
1377
1378 do_top_fun_eq :: FamInstEnvs -> Ct -> TcS (StopOrContinue Ct)
1379 do_top_fun_eq fam_envs work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1380 , cc_tyargs = args , cc_fsk = fsk })
1381 | Just (ax_co, rhs_ty) <- reduceTyFamApp_maybe fam_envs Nominal fam_tc args
1382 -- Look up in top-level instances, or built-in axiom
1383 -- See Note [MATCHING-SYNONYMS]
1384 = reduce_top_fun_eq old_ev fsk (TcCoercion ax_co) rhs_ty
1385
1386 | otherwise
1387 = do { improveTopFunEqs (ctEvLoc old_ev) fam_envs fam_tc args fsk
1388 ; continueWith work_item }
1389
1390 do_top_fun_eq _ w = pprPanic "doTopReactFunEq" (ppr w)
1391
1392 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType
1393 -> TcS (StopOrContinue Ct)
1394 -- Found an applicable top-level axiom: use it to reduce
1395 reduce_top_fun_eq old_ev fsk ax_co rhs_ty
1396 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1397 , isTypeFamilyTyCon tc
1398 , tc_args `lengthIs` tyConArity tc -- Short-cut
1399 = shortCutReduction old_ev fsk ax_co tc tc_args
1400 -- Try shortcut; see Note [Short cut for top-level reaction]
1401
1402 | isGiven old_ev -- Not shortcut
1403 = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1404 -- final_co :: fsk ~ rhs_ty
1405 ; new_ev <- newGivenEvVar deeper_loc (mkTcEqPred (mkTyVarTy fsk) rhs_ty,
1406 EvCoercion final_co)
1407 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1408 ; stopWith old_ev "Fun/Top (given)" }
1409
1410 -- So old_ev is Wanted or Derived
1411 | not (fsk `elemVarSet` tyVarsOfType rhs_ty)
1412 = do { dischargeFmv old_ev fsk ax_co rhs_ty
1413 ; traceTcS "doTopReactFunEq" $
1414 vcat [ text "old_ev:" <+> ppr old_ev
1415 , nest 2 (text ":=") <+> ppr ax_co ]
1416 ; stopWith old_ev "Fun/Top (wanted)" }
1417
1418 | otherwise -- We must not assign ufsk := ...ufsk...!
1419 = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1420 ; let pred = mkTcEqPred alpha_ty rhs_ty
1421 ; new_ev <- case old_ev of
1422 CtWanted {} -> do { ev <- newWantedEvVarNC loc pred
1423 ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev))
1424 ; return ev }
1425 CtDerived {} -> do { ev <- newDerivedNC loc pred
1426 ; updWorkListTcS (extendWorkListDerived loc ev)
1427 ; return ev }
1428 _ -> pprPanic "reduce_top_fun_eq" (ppr old_ev)
1429
1430 -- By emitting this as non-canonical, we deal with all
1431 -- flattening, occurs-check, and ufsk := ufsk issues
1432 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1433 -- ax_co :: fam_tc args ~ rhs_ty
1434 -- ev :: alpha ~ rhs_ty
1435 -- ufsk := alpha
1436 -- final_co :: fam_tc args ~ alpha
1437 ; dischargeFmv old_ev fsk final_co alpha_ty
1438 ; traceTcS "doTopReactFunEq (occurs)" $
1439 vcat [ text "old_ev:" <+> ppr old_ev
1440 , nest 2 (text ":=") <+> ppr final_co
1441 , text "new_ev:" <+> ppr new_ev ]
1442 ; stopWith old_ev "Fun/Top (wanted)" }
1443 where
1444 loc = ctEvLoc old_ev
1445 deeper_loc = bumpCtLocDepth loc
1446
1447 improveTopFunEqs :: CtLoc -> FamInstEnvs
1448 -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1449 improveTopFunEqs loc fam_envs fam_tc args fsk
1450 = do { model <- getInertModel
1451 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1452 (lookupFlattenTyVar model fsk)
1453 ; mapM_ (unifyDerived loc Nominal) eqns }
1454
1455 improve_top_fun_eqs :: FamInstEnvs
1456 -> TyCon -> [TcType] -> TcType
1457 -> TcS [Eqn]
1458 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1459 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1460 = return (sfInteractTop ops args rhs_ty)
1461
1462 -- see Note [Type inference for type families with injectivity]
1463 | isOpenTypeFamilyTyCon fam_tc
1464 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1465 = -- it is possible to have several compatible equations in an open type
1466 -- family but we only want to derive equalities from one such equation.
1467 concatMapM (injImproveEqns injective_args) (take 1 $
1468 buildImprovementData (lookupFamInstEnvByTyCon fam_envs fam_tc)
1469 fi_tys fi_rhs (const Nothing))
1470
1471 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1472 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1473 = concatMapM (injImproveEqns injective_args) $
1474 buildImprovementData (fromBranches (co_ax_branches ax))
1475 cab_lhs cab_rhs Just
1476
1477 | otherwise
1478 = return []
1479 where
1480 buildImprovementData
1481 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1482 -> (a -> [Type]) -- get LHS of an axiom
1483 -> (a -> Type) -- get RHS of an axiom
1484 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1485 -> [( [Type], TvSubst, TyVarSet, Maybe CoAxBranch )]
1486 -- Result:
1487 -- ( [arguments of a matching axiom]
1488 -- , RHS-unifying substitution
1489 -- , axiom variables without substitution
1490 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1491 buildImprovementData axioms axiomLHS axiomRHS wrap =
1492 [ (ax_args, subst, unsubstTvs, wrap axiom)
1493 | axiom <- axioms
1494 , let ax_args = axiomLHS axiom
1495 , let ax_rhs = axiomRHS axiom
1496 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1497 , let tvs = tyVarsOfTypes ax_args
1498 notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1499 unsubstTvs = filterVarSet notInSubst tvs ]
1500
1501 injImproveEqns :: [Bool]
1502 -> ([Type], TvSubst, TyVarSet, Maybe CoAxBranch)
1503 -> TcS [Eqn]
1504 injImproveEqns inj_args (ax_args, theta, unsubstTvs, cabr) = do
1505 (theta', _) <- instFlexiTcS (varSetElems unsubstTvs)
1506 let subst = theta `unionTvSubst` theta'
1507 return [ Pair arg (substTy subst ax_arg)
1508 | case cabr of
1509 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
1510 _ -> True
1511 , (arg, ax_arg, True) <- zip3 args ax_args inj_args ]
1512
1513
1514 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1515 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1516 -- See Note [Top-level reductions for type functions]
1517 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1518 | isGiven old_ev
1519 = ASSERT( ctEvEqRel old_ev == NomEq )
1520 do { (xis, cos) <- flattenManyNom old_ev tc_args
1521 -- ax_co :: F args ~ G tc_args
1522 -- cos :: xis ~ tc_args
1523 -- old_ev :: F args ~ fsk
1524 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1525
1526 ; new_ev <- newGivenEvVar deeper_loc
1527 ( mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1528 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1529 `mkTcTransCo` mkTcSymCo ax_co
1530 `mkTcTransCo` ctEvCoercion old_ev) )
1531
1532 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1533 ; emitWorkCt new_ct
1534 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1535
1536 | otherwise
1537 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1538 ASSERT( ctEvEqRel old_ev == NomEq )
1539 do { (xis, cos) <- flattenManyNom old_ev tc_args
1540 -- ax_co :: F args ~ G tc_args
1541 -- cos :: xis ~ tc_args
1542 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1543 -- new_ev :: G xis ~ fsk
1544 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1545
1546 ; new_ev <- newWantedEvVarNC deeper_loc
1547 (mkTcEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk))
1548 ; setWantedEvBind (ctEvId old_ev)
1549 (EvCoercion (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1550 `mkTcTransCo` ctEvCoercion new_ev))
1551
1552 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1553 ; emitWorkCt new_ct
1554 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1555 where
1556 loc = ctEvLoc old_ev
1557 deeper_loc = bumpCtLocDepth loc
1558
1559 dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1560 -- (dischargeFmv x fmv co ty)
1561 -- [W] ev :: F tys ~ fmv
1562 -- co :: F tys ~ xi
1563 -- Precondition: fmv is not filled, and fuv `notElem` xi
1564 --
1565 -- Then set fmv := xi,
1566 -- set ev := co
1567 -- kick out any inert things that are now rewritable
1568 --
1569 -- Does not evaluate 'co' if 'ev' is Derived
1570 dischargeFmv ev fmv co xi
1571 = ASSERT2( not (fmv `elemVarSet` tyVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
1572 do { setEvBindIfWanted ev (EvCoercion co)
1573 ; unflattenFmv fmv xi
1574 ; n_kicked <- kickOutAfterUnification fmv
1575 ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1576
1577 {- Note [Top-level reductions for type functions]
1578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1579 c.f. Note [The flattening story] in TcFlatten
1580
1581 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
1582 Here is what we do, in four cases:
1583
1584 * Wanteds: general firing rule
1585 (work item) [W] x : F tys ~ fmv
1586 instantiate axiom: ax_co : F tys ~ rhs
1587
1588 Then:
1589 Discharge fmv := alpha
1590 Discharge x := ax_co ; sym x2
1591 New wanted [W] x2 : alpha ~ rhs (Non-canonical)
1592 This is *the* way that fmv's get unified; even though they are
1593 "untouchable".
1594
1595 NB: it can be the case that fmv appears in the (instantiated) rhs.
1596 In that case the new Non-canonical wanted will be loopy, but that's
1597 ok. But it's good reason NOT to claim that it is canonical!
1598
1599 * Wanteds: short cut firing rule
1600 Applies when the RHS of the axiom is another type-function application
1601 (work item) [W] x : F tys ~ fmv
1602 instantiate axiom: ax_co : F tys ~ G rhs_tys
1603
1604 It would be a waste to create yet another fmv for (G rhs_tys).
1605 Instead (shortCutReduction):
1606 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
1607 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
1608 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
1609 - Discharge x := ax_co ; G cos ; x2
1610
1611 * Givens: general firing rule
1612 (work item) [G] g : F tys ~ fsk
1613 instantiate axiom: ax_co : F tys ~ rhs
1614
1615 Now add non-canonical given (since rhs is not flat)
1616 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
1617
1618 * Givens: short cut firing rule
1619 Applies when the RHS of the axiom is another type-function application
1620 (work item) [G] g : F tys ~ fsk
1621 instantiate axiom: ax_co : F tys ~ G rhs_tys
1622
1623 It would be a waste to create yet another fsk for (G rhs_tys).
1624 Instead (shortCutReduction):
1625 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
1626 - Add new Canonical given
1627 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
1628
1629 Note [Cached solved FunEqs]
1630 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1631 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1632 to see if we have reduced (FunExpensive big-type) before, lest we
1633 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1634 we must use `canDischarge` because both uses might (say) be Wanteds,
1635 and we *still* want to save the re-computation.
1636
1637 Note [MATCHING-SYNONYMS]
1638 ~~~~~~~~~~~~~~~~~~~~~~~~
1639 When trying to match a dictionary (D tau) to a top-level instance, or a
1640 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1641 we do *not* need to expand type synonyms because the matcher will do that for us.
1642
1643
1644 Note [RHS-FAMILY-SYNONYMS]
1645 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1646 The RHS of a family instance is represented as yet another constructor which is
1647 like a type synonym for the real RHS the programmer declared. Eg:
1648 type instance F (a,a) = [a]
1649 Becomes:
1650 :R32 a = [a] -- internal type synonym introduced
1651 F (a,a) ~ :R32 a -- instance
1652
1653 When we react a family instance with a type family equation in the work list
1654 we keep the synonym-using RHS without expansion.
1655
1656 Note [FunDep and implicit parameter reactions]
1657 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1658 Currently, our story of interacting two dictionaries (or a dictionary
1659 and top-level instances) for functional dependencies, and implicit
1660 paramters, is that we simply produce new Derived equalities. So for example
1661
1662 class D a b | a -> b where ...
1663 Inert:
1664 d1 :g D Int Bool
1665 WorkItem:
1666 d2 :w D Int alpha
1667
1668 We generate the extra work item
1669 cv :d alpha ~ Bool
1670 where 'cv' is currently unused. However, this new item can perhaps be
1671 spontaneously solved to become given and react with d2,
1672 discharging it in favour of a new constraint d2' thus:
1673 d2' :w D Int Bool
1674 d2 := d2' |> D Int cv
1675 Now d2' can be discharged from d1
1676
1677 We could be more aggressive and try to *immediately* solve the dictionary
1678 using those extra equalities, but that requires those equalities to carry
1679 evidence and derived do not carry evidence.
1680
1681 If that were the case with the same inert set and work item we might dischard
1682 d2 directly:
1683
1684 cv :w alpha ~ Bool
1685 d2 := d1 |> D Int cv
1686
1687 But in general it's a bit painful to figure out the necessary coercion,
1688 so we just take the first approach. Here is a better example. Consider:
1689 class C a b c | a -> b
1690 And:
1691 [Given] d1 : C T Int Char
1692 [Wanted] d2 : C T beta Int
1693 In this case, it's *not even possible* to solve the wanted immediately.
1694 So we should simply output the functional dependency and add this guy
1695 [but NOT its superclasses] back in the worklist. Even worse:
1696 [Given] d1 : C T Int beta
1697 [Wanted] d2: C T beta Int
1698 Then it is solvable, but its very hard to detect this on the spot.
1699
1700 It's exactly the same with implicit parameters, except that the
1701 "aggressive" approach would be much easier to implement.
1702
1703
1704 Note [Weird fundeps]
1705 ~~~~~~~~~~~~~~~~~~~~
1706 Consider class Het a b | a -> b where
1707 het :: m (f c) -> a -> m b
1708
1709 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1710 instance GHet (K a) (K [a])
1711 instance Het a b => GHet (K a) (K b)
1712
1713 The two instances don't actually conflict on their fundeps,
1714 although it's pretty strange. So they are both accepted. Now
1715 try [W] GHet (K Int) (K Bool)
1716 This triggers fundeps from both instance decls;
1717 [D] K Bool ~ K [a]
1718 [D] K Bool ~ K beta
1719 And there's a risk of complaining about Bool ~ [a]. But in fact
1720 the Wanted matches the second instance, so we never get as far
1721 as the fundeps.
1722
1723 Trac #7875 is a case in point.
1724
1725 Note [Overriding implicit parameters]
1726 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1727 Consider
1728 f :: (?x::a) -> Bool -> a
1729
1730 g v = let ?x::Int = 3
1731 in (f v, let ?x::Bool = True in f v)
1732
1733 This should probably be well typed, with
1734 g :: Bool -> (Int, Bool)
1735
1736 So the inner binding for ?x::Bool *overrides* the outer one.
1737 Hence a work-item Given overrides an inert-item Given.
1738 -}
1739
1740 {- *******************************************************************
1741 * *
1742 Class lookup
1743 * *
1744 **********************************************************************-}
1745
1746 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
1747 -- check.
1748 --
1749 -- See Note [Safe Haskell Overlapping Instances] in TcSimplify
1750 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1751 type SafeOverlapping = Bool
1752
1753 data LookupInstResult
1754 = NoInstance
1755 | GenInst [TcPredType] ([EvId] -> EvTerm) SafeOverlapping
1756
1757 instance Outputable LookupInstResult where
1758 ppr NoInstance = text "NoInstance"
1759 ppr (GenInst ev _ s) = text "GenInst" <+> ppr ev <+> ss
1760 where ss = text $ if s then "[safe]" else "[unsafe]"
1761
1762
1763 matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1764 matchClassInst dflags inerts clas tys loc
1765 -- First check whether there is an in-scope Given that could
1766 -- match this constraint. In that case, do not use top-level
1767 -- instances. See Note [Instance and Given overlap]
1768 | not (xopt Opt_IncoherentInstances dflags)
1769 , let matchable_givens = matchableGivens loc pred inerts
1770 , not (isEmptyBag matchable_givens)
1771 = do { traceTcS "Delaying instance application" $
1772 vcat [ text "Work item=" <+> pprClassPred clas tys
1773 , text "Potential matching givens:" <+> ppr matchable_givens ]
1774 ; return NoInstance }
1775 where
1776 pred = mkClassPred clas tys
1777
1778 matchClassInst dflags _ clas tys loc
1779 = do { traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr (mkClassPred clas tys) ]
1780 ; res <- match_class_inst dflags clas tys loc
1781 ; traceTcS "matchClassInst result" $ ppr res
1782 ; return res }
1783
1784 match_class_inst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1785 match_class_inst dflags clas tys loc
1786 | cls_name == knownNatClassName = matchKnownNat clas tys
1787 | cls_name == knownSymbolClassName = matchKnownSymbol clas tys
1788 | isCTupleClass clas = matchCTuple clas tys
1789 | cls_name == typeableClassName = matchTypeable clas tys
1790 | otherwise = matchInstEnv dflags clas tys loc
1791 where
1792 cls_name = className clas
1793
1794 {- Note [Instance and Given overlap]
1795 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1796 Example, from the OutsideIn(X) paper:
1797 instance P x => Q [x]
1798 instance (x ~ y) => R y [x]
1799
1800 wob :: forall a b. (Q [b], R b a) => a -> Int
1801
1802 g :: forall a. Q [a] => [a] -> Int
1803 g x = wob x
1804
1805 This will generate the impliation constraint:
1806 Q [a] => (Q [beta], R beta [a])
1807 If we react (Q [beta]) with its top-level axiom, we end up with a
1808 (P beta), which we have no way of discharging. On the other hand,
1809 if we react R beta [a] with the top-level we get (beta ~ a), which
1810 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1811 now solvable by the given Q [a].
1812
1813 The solution is that:
1814 In matchClassInst (and thus in topReact), we return a matching
1815 instance only when there is no Given in the inerts which is
1816 unifiable to this particular dictionary.
1817
1818 We treat any meta-tyvar as "unifiable" for this purpose,
1819 *including* untouchable ones
1820
1821 The end effect is that, much as we do for overlapping instances, we
1822 delay choosing a class instance if there is a possibility of another
1823 instance OR a given to match our constraint later on. This fixes
1824 Trac #4981 and #5002.
1825
1826 Other notes:
1827
1828 * The check is done *first*, so that it also covers classes
1829 with built-in instance solving, such as
1830 - constraint tuples
1831 - natural numbers
1832 - Typeable
1833
1834 * The given-overlap problem is arguably not easy to appear in practice
1835 due to our aggressive prioritization of equality solving over other
1836 constraints, but it is possible. I've added a test case in
1837 typecheck/should-compile/GivenOverlapping.hs
1838
1839 * Another "live" example is Trac #10195; another is #10177.
1840
1841 * We ignore the overlap problem if -XIncoherentInstances is in force:
1842 see Trac #6002 for a worked-out example where this makes a
1843 difference.
1844
1845 * Moreover notice that our goals here are different than the goals of
1846 the top-level overlapping checks. There we are interested in
1847 validating the following principle:
1848
1849 If we inline a function f at a site where the same global
1850 instance environment is available as the instance environment at
1851 the definition site of f then we should get the same behaviour.
1852
1853 But for the Given Overlap check our goal is just related to completeness of
1854 constraint solving.
1855 -}
1856
1857
1858 {- *******************************************************************
1859 * *
1860 Class lookup in the instance environment
1861 * *
1862 **********************************************************************-}
1863
1864 matchInstEnv :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1865 matchInstEnv dflags clas tys loc
1866 = do { instEnvs <- getInstEnvs
1867 ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
1868 (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
1869 safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
1870 ; case (matches, unify, safeHaskFail) of
1871
1872 -- Nothing matches
1873 ([], _, _)
1874 -> do { traceTcS "matchClass not matching" $
1875 vcat [ text "dict" <+> ppr pred ]
1876 ; return NoInstance }
1877
1878 -- A single match (& no safe haskell failure)
1879 ([(ispec, inst_tys)], [], False)
1880 -> do { let dfun_id = instanceDFunId ispec
1881 ; traceTcS "matchClass success" $
1882 vcat [text "dict" <+> ppr pred,
1883 text "witness" <+> ppr dfun_id
1884 <+> ppr (idType dfun_id) ]
1885 -- Record that this dfun is needed
1886 ; match_one (null unsafeOverlaps) dfun_id inst_tys }
1887
1888 -- More than one matches (or Safe Haskell fail!). Defer any
1889 -- reactions of a multitude until we learn more about the reagent
1890 (matches, _, _)
1891 -> do { traceTcS "matchClass multiple matches, deferring choice" $
1892 vcat [text "dict" <+> ppr pred,
1893 text "matches" <+> ppr matches]
1894 ; return NoInstance } }
1895 where
1896 pred = mkClassPred clas tys
1897
1898 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
1899 -- See Note [DFunInstType: instantiating types] in InstEnv
1900 match_one so dfun_id mb_inst_tys
1901 = do { checkWellStagedDFun pred dfun_id loc
1902 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
1903 ; return $ GenInst theta (EvDFunApp dfun_id tys) so }
1904
1905
1906 {- ********************************************************************
1907 * *
1908 Class lookup for CTuples
1909 * *
1910 ***********************************************************************-}
1911
1912 matchCTuple :: Class -> [Type] -> TcS LookupInstResult
1913 matchCTuple clas tys -- (isCTupleClass clas) holds
1914 = return (GenInst tys tuple_ev True)
1915 -- The dfun *is* the data constructor!
1916 where
1917 data_con = tyConSingleDataCon (classTyCon clas)
1918 tuple_ev = EvDFunApp (dataConWrapId data_con) tys
1919
1920 {- ********************************************************************
1921 * *
1922 Class lookup for Literals
1923 * *
1924 ***********************************************************************-}
1925
1926 matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
1927 matchKnownNat clas [ty] -- clas = KnownNat
1928 | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n)
1929 matchKnownNat _ _ = return NoInstance
1930
1931 matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
1932 matchKnownSymbol clas [ty] -- clas = KnownSymbol
1933 | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n)
1934 matchKnownSymbol _ _ = return NoInstance
1935
1936
1937 makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
1938 -- makeLitDict adds a coercion that will convert the literal into a dictionary
1939 -- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1940 -- in TcEvidence. The coercion happens in 2 steps:
1941 --
1942 -- Integer -> SNat n -- representation of literal to singleton
1943 -- SNat n -> KnownNat n -- singleton to dictionary
1944 --
1945 -- The process is mirrored for Symbols:
1946 -- String -> SSymbol n
1947 -- SSymbol n -> KnownSymbol n -}
1948 makeLitDict clas ty evLit
1949 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1950 -- co_dict :: KnownNat n ~ SNat n
1951 , [ meth ] <- classMethods clas
1952 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1953 $ funResultTy -- SNat n
1954 $ dropForAlls -- KnownNat n => SNat n
1955 $ idType meth -- forall n. KnownNat n => SNat n
1956 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
1957 -- SNat n ~ Integer
1958 , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
1959 = return $ GenInst [] (\_ -> ev_tm) True
1960
1961 | otherwise
1962 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1963 $$ vcat (map (ppr . idType) (classMethods clas)))
1964
1965
1966 {- ********************************************************************
1967 * *
1968 Class lookup for Typeable
1969 * *
1970 ***********************************************************************-}
1971
1972 -- | Assumes that we've checked that this is the 'Typeable' class,
1973 -- and it was applied to the correct argument.
1974 matchTypeable :: Class -> [Type] -> TcS LookupInstResult
1975 matchTypeable clas [k,t] -- clas = Typeable
1976 -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
1977 | isForAllTy k = return NoInstance -- Polytype
1978 | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type
1979
1980 -- Now cases that do work
1981 | k `eqType` typeNatKind = doTyLit knownNatClassName t
1982 | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t
1983 | Just (_, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
1984 , all isGroundKind ks = doTyConApp t
1985 | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt
1986
1987 matchTypeable _ _ = return NoInstance
1988
1989 doTyConApp :: Type -> TcS LookupInstResult
1990 -- Representation for type constructor applied to some (ground) kinds
1991 doTyConApp ty = return $ GenInst [] (\_ -> EvTypeable ty EvTypeableTyCon) True
1992
1993 -- Representation for concrete kinds. We just use the kind itself,
1994 -- but first check to make sure that it is "simple" (i.e., made entirely
1995 -- out of kind constructors).
1996 isGroundKind :: KindOrType -> Bool
1997 -- Return True if (a) k is a kind and (b) it is a ground kind
1998 isGroundKind k
1999 = isKind k && is_ground k
2000 where
2001 is_ground k | Just (_, ks) <- splitTyConApp_maybe k
2002 = all is_ground ks
2003 | otherwise
2004 = False
2005
2006 doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
2007 -- Representation for an application of a type to a type-or-kind.
2008 -- This may happen when the type expression starts with a type variable.
2009 -- Example (ignoring kind parameter):
2010 -- Typeable (f Int Char) -->
2011 -- (Typeable (f Int), Typeable Char) -->
2012 -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
2013 -- Typeable f
2014 doTyApp clas ty f tk
2015 | isKind tk
2016 = return NoInstance -- We can't solve until we know the ctr.
2017 | otherwise
2018 = return $ GenInst [mk_typeable_pred clas f, mk_typeable_pred clas tk]
2019 (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp (EvId t1) (EvId t2))
2020 True
2021
2022 -- Emit a `Typeable` constraint for the given type.
2023 mk_typeable_pred :: Class -> Type -> PredType
2024 mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
2025
2026 -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
2027 -- we generate a sub-goal for the appropriate class. See #10348 for what
2028 -- happens when we fail to do this.
2029 doTyLit :: Name -> Type -> TcS LookupInstResult
2030 doTyLit kc t = do { kc_clas <- tcLookupClass kc
2031 ; let kc_pred = mkClassPred kc_clas [ t ]
2032 mk_ev [ev] = EvTypeable t $ EvTypeableTyLit $ EvId ev
2033 mk_ev _ = panic "doTyLit"
2034 ; return (GenInst [kc_pred] mk_ev True) }
2035
2036 {- Note [Typeable (T a b c)]
2037 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2038 For type applications we always decompose using binary application,
2039 vai doTyApp, until we get to a *kind* instantiation. Exmaple
2040 Proxy :: forall k. k -> *
2041
2042 To solve Typeable (Proxy (* -> *) Maybe) we
2043 - First decompose with doTyApp,
2044 to get (Typeable (Proxy (* -> *))) and Typeable Maybe
2045 - Then sovle (Typeable (Proxy (* -> *))) with doTyConApp
2046
2047 If we attempt to short-cut by solving it all at once, via
2048 doTyCOnAPp
2049
2050
2051 Note [No Typeable for polytypes or qualified types]
2052 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2053 We do not support impredicative typeable, such as
2054 Typeable (forall a. a->a)
2055 Typeable (Eq a => a -> a)
2056 Typeable (() => Int)
2057 Typeable (((),()) => Int)
2058
2059 See Trac #9858. For forall's the case is clear: we simply don't have
2060 a TypeRep for them. For qualified but not polymorphic types, like
2061 (Eq a => a -> a), things are murkier. But:
2062
2063 * We don't need a TypeRep for these things. TypeReps are for
2064 monotypes only.
2065
2066 * Perhaps we could treat `=>` as another type constructor for `Typeable`
2067 purposes, and thus support things like `Eq Int => Int`, however,
2068 at the current state of affairs this would be an odd exception as
2069 no other class works with impredicative types.
2070 For now we leave it off, until we have a better story for impredicativity.
2071 -}