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