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