Expose enabled language extensions to TH
[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 FastString
15 import TcCanonical
16 import TcFlatten
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 )
28 import TysWiredIn ( ipClass, 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 [ ptext (sLit "iterations =") <+> ppr n
158 , ptext (sLit "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 (ptext (sLit "solveSimpleWanteds: too many iterations")
165 <+> parens (ptext (sLit "limit =") <+> ppr limit))
166 2 (vcat [ ptext (sLit "Set limit with -fsolver-iterations=n; n=0 for no limit")
167 , ptext (sLit "Simples =") <+> ppr simples
168 , ptext (sLit "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 [ ptext (sLit "work item = ") <+> ppr workItem
382 , ptext (sLit "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 (ptext (sLit "inerts =") <+> ppr final_is)
392 ; return () }
393 ContinueWith ct -> do { traceFireTcS (ctEvidence ct) (ptext (sLit "Kept as inert"))
394 ; traceTcS "End solver pipeline (kept as inert) }" $
395 vcat [ ptext (sLit "final_item =") <+> ppr ct
396 , pprTvBndrs (varSetElems $ tyCoVarsOfCt ct)
397 , ptext (sLit "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 = ptext (sLit "keep")
501 ppr IRReplace = ptext (sLit "replace")
502 ppr IRDelete = ptext (sLit "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 evidence (no coercions) only
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 (ptext (sLit "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 <- isCallStackCt 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 (ptext (sLit "Dict equal") <+> parens (ppr inert_effect)))
716 else
717 continueWith workItem }
718
719 | cls == ipClass
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 {-
783 Note [Shadowing of Implicit Parameters]
784 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
785 Consider the following example:
786
787 f :: (?x :: Char) => Char
788 f = let ?x = 'a' in ?x
789
790 The "let ?x = ..." generates an implication constraint of the form:
791
792 ?x :: Char => ?x :: Char
793
794 Furthermore, the signature for `f` also generates an implication
795 constraint, so we end up with the following nested implication:
796
797 ?x :: Char => (?x :: Char => ?x :: Char)
798
799 Note that the wanted (?x :: Char) constraint may be solved in
800 two incompatible ways: either by using the parameter from the
801 signature, or by using the local definition. Our intention is
802 that the local definition should "shadow" the parameter of the
803 signature, and we implement this as follows: when we add a new
804 *given* implicit parameter to the inert set, it replaces any existing
805 givens for the same implicit parameter.
806
807 This works for the normal cases but it has an odd side effect
808 in some pathological programs like this:
809
810 -- This is accepted, the second parameter shadows
811 f1 :: (?x :: Int, ?x :: Char) => Char
812 f1 = ?x
813
814 -- This is rejected, the second parameter shadows
815 f2 :: (?x :: Int, ?x :: Char) => Int
816 f2 = ?x
817
818 Both of these are actually wrong: when we try to use either one,
819 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
820 which would lead to an error.
821
822 I can think of two ways to fix this:
823
824 1. Simply disallow multiple constratits for the same implicit
825 parameter---this is never useful, and it can be detected completely
826 syntactically.
827
828 2. Move the shadowing machinery to the location where we nest
829 implications, and add some code here that will produce an
830 error if we get multiple givens for the same implicit parameter.
831
832
833 **********************************************************************
834 * *
835 interactFunEq
836 * *
837 **********************************************************************
838 -}
839
840 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
841 -- Try interacting the work item with the inert set
842 interactFunEq inerts workItem@(CFunEqCan { cc_ev = ev, cc_fun = tc
843 , cc_tyargs = args, cc_fsk = fsk })
844 | Just (CFunEqCan { cc_ev = ev_i
845 , cc_fsk = fsk_i }) <- matching_inerts
846 = if ev_i `canDischarge` ev
847 then -- Rewrite work-item using inert
848 do { traceTcS "reactFunEq (discharge work item):" $
849 vcat [ text "workItem =" <+> ppr workItem
850 , text "inertItem=" <+> ppr ev_i ]
851 ; reactFunEq ev_i fsk_i ev fsk
852 ; stopWith ev "Inert rewrites work item" }
853 else -- Rewrite inert using work-item
854 ASSERT2( ev `canDischarge` ev_i, ppr ev $$ ppr ev_i )
855 do { traceTcS "reactFunEq (rewrite inert item):" $
856 vcat [ text "workItem =" <+> ppr workItem
857 , text "inertItem=" <+> ppr ev_i ]
858 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args workItem
859 -- Do the updInertFunEqs before the reactFunEq, so that
860 -- we don't kick out the inertItem as well as consuming it!
861 ; reactFunEq ev fsk ev_i fsk_i
862 ; stopWith ev "Work item rewrites inert" }
863
864 | otherwise -- Try improvement
865 = do { improveLocalFunEqs loc inerts tc args fsk
866 ; continueWith workItem }
867 where
868 loc = ctEvLoc ev
869 funeqs = inert_funeqs inerts
870 matching_inerts = findFunEq funeqs tc args
871
872 interactFunEq _ workItem = pprPanic "interactFunEq" (ppr workItem)
873
874 improveLocalFunEqs :: CtLoc -> InertCans -> TyCon -> [TcType] -> TcTyVar
875 -> TcS ()
876 -- Generate derived improvement equalities, by comparing
877 -- the current work item with inert CFunEqs
878 -- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y'
879 improveLocalFunEqs loc inerts fam_tc args fsk
880 | not (null improvement_eqns)
881 = do { traceTcS "interactFunEq improvements: " $
882 vcat [ ptext (sLit "Eqns:") <+> ppr improvement_eqns
883 , ptext (sLit "Candidates:") <+> ppr funeqs_for_tc
884 , ptext (sLit "TvEqs:") <+> ppr tv_eqs ]
885 ; mapM_ (unifyDerived loc Nominal) improvement_eqns }
886 | otherwise
887 = return ()
888 where
889 tv_eqs = inert_model inerts
890 funeqs = inert_funeqs inerts
891 funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
892 rhs = lookupFlattenTyVar tv_eqs fsk
893
894 --------------------
895 improvement_eqns
896 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
897 = -- Try built-in families, notably for arithmethic
898 concatMap (do_one_built_in ops) funeqs_for_tc
899
900 | Injective injective_args <- familyTyConInjectivityInfo fam_tc
901 = -- Try improvement from type families with injectivity annotations
902 concatMap (do_one_injective injective_args) funeqs_for_tc
903
904 | otherwise
905 = []
906
907 --------------------
908 do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
909 = sfInteractInert ops args rhs iargs (lookupFlattenTyVar tv_eqs ifsk)
910 do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
911
912 --------------------
913 -- See Note [Type inference for type families with injectivity]
914 do_one_injective injective_args
915 (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk })
916 | rhs `tcEqType` lookupFlattenTyVar tv_eqs ifsk
917 = [Pair arg iarg | (arg, iarg, True)
918 <- zip3 args iargs injective_args ]
919 | otherwise
920 = []
921 do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
922
923 -------------
924 lookupFlattenTyVar :: InertModel -> TcTyVar -> TcType
925 -- ^ Look up a flatten-tyvar in the inert nominal TyVarEqs;
926 -- this is used only when dealing with a CFunEqCan
927 lookupFlattenTyVar model ftv
928 = case lookupVarEnv model ftv of
929 Just (CTyEqCan { cc_rhs = rhs, cc_eq_rel = NomEq }) -> rhs
930 _ -> mkTyVarTy ftv
931
932 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F args1 ~ fsk1
933 -> CtEvidence -> TcTyVar -- Solve this :: F args2 ~ fsk2
934 -> TcS ()
935 reactFunEq from_this fsk1 solve_this fsk2
936 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- solve_this
937 = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar) `mkTcTransCo`
938 ctEvCoercion from_this
939 -- :: fsk2 ~ fsk1
940 fsk_eq_pred = mkTcEqPredLikeEv solve_this
941 (mkTyVarTy fsk2) (mkTyVarTy fsk1)
942
943 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
944 ; emitWorkNC [new_ev] }
945
946 | otherwise
947 = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
948 ppr solve_this $$ ppr fsk2)
949 ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
950 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
951 ppr solve_this $$ ppr fsk2) }
952
953 {-
954 Note [Type inference for type families with injectivity]
955 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
956 Suppose we have a type family with an injectivity annotation:
957 type family F a b = r | r -> b
958
959 Then if we have two CFunEqCan constraints for F with the same RHS
960 F s1 t1 ~ rhs
961 F s2 t2 ~ rhs
962 then we can use the injectivity to get a new Derived constraint on
963 the injective argument
964 [D] t1 ~ t2
965
966 That in turn can help GHC solve constraints that would otherwise require
967 guessing. For example, consider the ambiguity check for
968 f :: F Int b -> Int
969 We get the constraint
970 [W] F Int b ~ F Int beta
971 where beta is a unification variable. Injectivity lets us pick beta ~ b.
972
973 Injectivity information is also used at the call sites. For example:
974 g = f True
975 gives rise to
976 [W] F Int b ~ Bool
977 from which we can derive b. This requires looking at the defining equations of
978 a type family, ie. finding equation with a matching RHS (Bool in this example)
979 and infering values of type variables (b in this example) from the LHS patterns
980 of the matching equation. For closed type families we have to perform
981 additional apartness check for the selected equation to check that the selected
982 is guaranteed to fire for given LHS arguments.
983
984 These new constraints are simply *Derived* constraints; they have no evidence.
985 We could go further and offer evidence from decomposing injective type-function
986 applications, but that would require new evidence forms, and an extension to
987 FC, so we don't do that right now (Dec 14).
988
989 See also Note [Injective type families] in TyCon
990
991
992 Note [Cache-caused loops]
993 ~~~~~~~~~~~~~~~~~~~~~~~~~
994 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
995 solved cache (which is the default behaviour or xCtEvidence), because the interaction
996 may not be contributing towards a solution. Here is an example:
997
998 Initial inert set:
999 [W] g1 : F a ~ beta1
1000 Work item:
1001 [W] g2 : F a ~ beta2
1002 The work item will react with the inert yielding the _same_ inert set plus:
1003 i) Will set g2 := g1 `cast` g3
1004 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
1005 iii) Will emit [W] g3 : beta1 ~ beta2
1006 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
1007 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
1008 will set
1009 g1 := g ; sym g3
1010 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
1011 remember that we have this in our solved cache, and it is ... g2! In short we
1012 created the evidence loop:
1013
1014 g2 := g1 ; g3
1015 g3 := refl
1016 g1 := g2 ; sym g3
1017
1018 To avoid this situation we do not cache as solved any workitems (or inert)
1019 which did not really made a 'step' towards proving some goal. Solved's are
1020 just an optimization so we don't lose anything in terms of completeness of
1021 solving.
1022
1023
1024 Note [Efficient Orientation]
1025 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1026 Suppose we are interacting two FunEqCans with the same LHS:
1027 (inert) ci :: (F ty ~ xi_i)
1028 (work) cw :: (F ty ~ xi_w)
1029 We prefer to keep the inert (else we pass the work item on down
1030 the pipeline, which is a bit silly). If we keep the inert, we
1031 will (a) discharge 'cw'
1032 (b) produce a new equality work-item (xi_w ~ xi_i)
1033 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
1034 new_work :: xi_w ~ xi_i
1035 cw := ci ; sym new_work
1036 Why? Consider the simplest case when xi1 is a type variable. If
1037 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
1038 If we generate xi2~xi1, there is less chance of that happening.
1039 Of course it can and should still happen if xi1=a, xi1=Int, say.
1040 But we want to avoid it happening needlessly.
1041
1042 Similarly, if we *can't* keep the inert item (because inert is Wanted,
1043 and work is Given, say), we prefer to orient the new equality (xi_i ~
1044 xi_w).
1045
1046 Note [Carefully solve the right CFunEqCan]
1047 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1048 ---- OLD COMMENT, NOW NOT NEEDED
1049 ---- because we now allow multiple
1050 ---- wanted FunEqs with the same head
1051 Consider the constraints
1052 c1 :: F Int ~ a -- Arising from an application line 5
1053 c2 :: F Int ~ Bool -- Arising from an application line 10
1054 Suppose that 'a' is a unification variable, arising only from
1055 flattening. So there is no error on line 5; it's just a flattening
1056 variable. But there is (or might be) an error on line 10.
1057
1058 Two ways to combine them, leaving either (Plan A)
1059 c1 :: F Int ~ a -- Arising from an application line 5
1060 c3 :: a ~ Bool -- Arising from an application line 10
1061 or (Plan B)
1062 c2 :: F Int ~ Bool -- Arising from an application line 10
1063 c4 :: a ~ Bool -- Arising from an application line 5
1064
1065 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
1066 on the *totally innocent* line 5. An example is test SimpleFail16
1067 where the expected/actual message comes out backwards if we use
1068 the wrong plan.
1069
1070 The second is the right thing to do. Hence the isMetaTyVarTy
1071 test when solving pairwise CFunEqCan.
1072
1073
1074 **********************************************************************
1075 * *
1076 interactTyVarEq
1077 * *
1078 **********************************************************************
1079 -}
1080
1081 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1082 -- CTyEqCans are always consumed, so always returns Stop
1083 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
1084 , cc_rhs = rhs
1085 , cc_ev = ev
1086 , cc_eq_rel = eq_rel })
1087 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1088 <- findTyEqs inerts tv
1089 , ev_i `canDischarge` ev
1090 , rhs_i `tcEqType` rhs ]
1091 = -- Inert: a ~ b
1092 -- Work item: a ~ b
1093 do { setEvBindIfWanted ev $
1094 EvCoercion (tcDowngradeRole (eqRelRole eq_rel)
1095 (ctEvRole ev_i)
1096 (ctEvCoercion ev_i))
1097
1098 ; stopWith ev "Solved from inert" }
1099
1100 | Just tv_rhs <- getTyVar_maybe rhs
1101 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1102 <- findTyEqs inerts tv_rhs
1103 , ev_i `canDischarge` ev
1104 , rhs_i `tcEqType` mkTyVarTy tv ]
1105 = -- Inert: a ~ b
1106 -- Work item: b ~ a
1107 do { setEvBindIfWanted ev $
1108 EvCoercion (mkTcSymCo $
1109 tcDowngradeRole (eqRelRole eq_rel)
1110 (ctEvRole ev_i)
1111 (ctEvCoercion ev_i))
1112
1113 ; stopWith ev "Solved from inert (r)" }
1114
1115 | otherwise
1116 = do { tclvl <- getTcLevel
1117 ; if canSolveByUnification tclvl ev eq_rel tv rhs
1118 then do { solveByUnification ev tv rhs
1119 ; n_kicked <- kickOutAfterUnification tv
1120 ; return (Stop ev (ptext (sLit "Solved by unification") <+> ppr_kicked n_kicked)) }
1121
1122 else do { traceTcS "Can't solve tyvar equality"
1123 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1124 , ppWhen (isMetaTyVar tv) $
1125 nest 4 (text "TcLevel of" <+> ppr tv
1126 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
1127 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
1128 , text "TcLevel =" <+> ppr tclvl ])
1129 ; addInertEq workItem
1130 ; return (Stop ev (ptext (sLit "Kept as inert"))) } }
1131
1132 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1133
1134 -- @trySpontaneousSolve wi@ solves equalities where one side is a
1135 -- touchable unification variable.
1136 -- Returns True <=> spontaneous solve happened
1137 canSolveByUnification :: TcLevel -> CtEvidence -> EqRel
1138 -> TcTyVar -> Xi -> Bool
1139 canSolveByUnification tclvl gw eq_rel tv xi
1140 | ReprEq <- eq_rel -- we never solve representational equalities this way.
1141 = False
1142
1143 | isGiven gw -- See Note [Touchables and givens]
1144 = False
1145
1146 | isTouchableMetaTyVar tclvl tv
1147 = case metaTyVarInfo tv of
1148 SigTv -> is_tyvar xi
1149 _ -> True
1150
1151 | otherwise -- Untouchable
1152 = False
1153 where
1154 is_tyvar xi
1155 = case tcGetTyVar_maybe xi of
1156 Nothing -> False
1157 Just tv -> case tcTyVarDetails tv of
1158 MetaTv { mtv_info = info }
1159 -> case info of
1160 SigTv -> True
1161 _ -> False
1162 SkolemTv {} -> True
1163 FlatSkol {} -> False
1164 RuntimeUnk -> True
1165
1166 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1167 -- Solve with the identity coercion
1168 -- Precondition: kind(xi) equals kind(tv)
1169 -- Precondition: CtEvidence is Wanted or Derived
1170 -- Precondition: CtEvidence is nominal
1171 -- Returns: workItem where
1172 -- workItem = the new Given constraint
1173 --
1174 -- NB: No need for an occurs check here, because solveByUnification always
1175 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1176 -- say that in (a ~ xi), the type variable a does not appear in xi.
1177 -- See TcRnTypes.Ct invariants.
1178 --
1179 -- Post: tv is unified (by side effect) with xi;
1180 -- we often write tv := xi
1181 solveByUnification wd tv xi
1182 = do { let tv_ty = mkTyVarTy tv
1183 ; traceTcS "Sneaky unification:" $
1184 vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
1185 text "Coercion:" <+> pprEq tv_ty xi,
1186 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1187 text "Right Kind is:" <+> ppr (typeKind xi) ]
1188
1189 ; unifyTyVar tv xi
1190 ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi)) }
1191
1192 ppr_kicked :: Int -> SDoc
1193 ppr_kicked 0 = empty
1194 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
1195
1196 {- Note [Avoid double unifications]
1197 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1198 The spontaneous solver has to return a given which mentions the unified unification
1199 variable *on the left* of the equality. Here is what happens if not:
1200 Original wanted: (a ~ alpha), (alpha ~ Int)
1201 We spontaneously solve the first wanted, without changing the order!
1202 given : a ~ alpha [having unified alpha := a]
1203 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1204 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1205
1206 We avoid this problem by orienting the resulting given so that the unification
1207 variable is on the left. [Note that alternatively we could attempt to
1208 enforce this at canonicalization]
1209
1210 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1211 double unifications is the main reason we disallow touchable
1212 unification variables as RHS of type family equations: F xis ~ alpha.
1213
1214
1215 ************************************************************************
1216 * *
1217 * Functional dependencies, instantiation of equations
1218 * *
1219 ************************************************************************
1220
1221 When we spot an equality arising from a functional dependency,
1222 we now use that equality (a "wanted") to rewrite the work-item
1223 constraint right away. This avoids two dangers
1224
1225 Danger 1: If we send the original constraint on down the pipeline
1226 it may react with an instance declaration, and in delicate
1227 situations (when a Given overlaps with an instance) that
1228 may produce new insoluble goals: see Trac #4952
1229
1230 Danger 2: If we don't rewrite the constraint, it may re-react
1231 with the same thing later, and produce the same equality
1232 again --> termination worries.
1233
1234 To achieve this required some refactoring of FunDeps.hs (nicer
1235 now!).
1236 -}
1237
1238 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1239 emitFunDepDeriveds fd_eqns
1240 = mapM_ do_one_FDEqn fd_eqns
1241 where
1242 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1243 | null tvs -- Common shortcut
1244 = mapM_ (unifyDerived loc Nominal) eqs
1245 | otherwise
1246 = do { (subst, _) <- instFlexiTcS tvs -- Takes account of kind substitution
1247 ; mapM_ (do_one_eq loc subst) eqs }
1248
1249 do_one_eq loc subst (Pair ty1 ty2)
1250 = unifyDerived loc Nominal $
1251 Pair (Type.substTy subst ty1) (Type.substTy subst ty2)
1252
1253 {-
1254 **********************************************************************
1255 * *
1256 The top-reaction Stage
1257 * *
1258 **********************************************************************
1259 -}
1260
1261 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1262 topReactionsStage wi
1263 = do { tir <- doTopReact wi
1264 ; case tir of
1265 ContinueWith wi -> continueWith wi
1266 Stop ev s -> return (Stop ev (ptext (sLit "Top react:") <+> s)) }
1267
1268 doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
1269 -- The work item does not react with the inert set, so try interaction with top-level
1270 -- instances. Note:
1271 --
1272 -- (a) The place to add superclasses in not here in doTopReact stage.
1273 -- Instead superclasses are added in the worklist as part of the
1274 -- canonicalization process. See Note [Adding superclasses].
1275
1276 doTopReact work_item
1277 = do { traceTcS "doTopReact" (ppr work_item)
1278 ; case work_item of
1279 CDictCan {} -> do { inerts <- getTcSInerts
1280 ; doTopReactDict inerts work_item }
1281 CFunEqCan {} -> doTopReactFunEq work_item
1282 _ -> -- Any other work item does not react with any top-level equations
1283 continueWith work_item }
1284
1285 --------------------
1286 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
1287 -- Try to use type-class instance declarations to simplify the constraint
1288 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
1289 , cc_tyargs = xis })
1290 | isGiven fl -- Never use instances for Given constraints
1291 = do { try_fundep_improvement
1292 ; continueWith work_item }
1293
1294 | Just ev <- lookupSolvedDict inerts cls xis -- Cached
1295 = do { setEvBindIfWanted fl (ctEvTerm ev)
1296 ; stopWith fl "Dict/Top (cached)" }
1297
1298 | isDerived fl -- Use type-class instances for Deriveds, in the hope
1299 -- of generating some improvements
1300 -- C.f. Example 3 of Note [The improvement story]
1301 -- It's easy because no evidence is involved
1302 = do { dflags <- getDynFlags
1303 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
1304 ; case lkup_inst_res of
1305 GenInst { lir_new_theta = preds
1306 , lir_safe_over = s } ->
1307 do { emitNewDeriveds dict_loc preds
1308 ; unless s $ insertSafeOverlapFailureTcS work_item
1309 ; stopWith fl "Dict/Top (solved)" }
1310
1311 NoInstance ->
1312 do { -- If there is no instance, try improvement
1313 try_fundep_improvement
1314 ; continueWith work_item } }
1315
1316 | otherwise -- Wanted, but not cached
1317 = do { dflags <- getDynFlags
1318 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
1319 ; case lkup_inst_res of
1320 GenInst { lir_new_theta = theta
1321 , lir_mk_ev = mk_ev
1322 , lir_safe_over = s } ->
1323 do { addSolvedDict fl cls xis
1324 ; unless s $ insertSafeOverlapFailureTcS work_item
1325 ; solve_from_instance theta mk_ev }
1326 NoInstance ->
1327 do { try_fundep_improvement
1328 ; continueWith work_item } }
1329 where
1330 dict_pred = mkClassPred cls xis
1331 dict_loc = ctEvLoc fl
1332 dict_origin = ctLocOrigin dict_loc
1333 deeper_loc = zap_origin (bumpCtLocDepth dict_loc)
1334
1335 zap_origin loc -- After applying an instance we can set ScOrigin to
1336 -- infinity, so that prohibitedSuperClassSolve never fires
1337 | ScOrigin {} <- dict_origin
1338 = setCtLocOrigin loc (ScOrigin infinity)
1339 | otherwise
1340 = loc
1341
1342 solve_from_instance :: [TcPredType]
1343 -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
1344 -- Precondition: evidence term matches the predicate workItem
1345 solve_from_instance theta mk_ev
1346 | null theta
1347 = do { traceTcS "doTopReact/found nullary instance for" $ ppr fl
1348 ; setWantedEvBind (ctEvId fl) (mk_ev [])
1349 ; stopWith fl "Dict/Top (solved, no new work)" }
1350 | otherwise
1351 = do { checkReductionDepth deeper_loc dict_pred
1352 ; traceTcS "doTopReact/found non-nullary instance for" $ ppr fl
1353 ; evc_vars <- mapM (newWanted deeper_loc) theta
1354 ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars))
1355 ; emitWorkNC (freshGoals evc_vars)
1356 ; stopWith fl "Dict/Top (solved, more work)" }
1357
1358 -- We didn't solve it; so try functional dependencies with
1359 -- the instance environment, and return
1360 -- See also Note [Weird fundeps]
1361 try_fundep_improvement
1362 = do { traceTcS "try_fundeps" (ppr work_item)
1363 ; instEnvs <- getInstEnvs
1364 ; emitFunDepDeriveds $
1365 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
1366
1367 mk_ct_loc :: PredType -- From instance decl
1368 -> SrcSpan -- also from instance deol
1369 -> CtLoc
1370 mk_ct_loc inst_pred inst_loc
1371 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
1372 inst_pred inst_loc }
1373
1374 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
1375
1376 --------------------
1377 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1378 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1379 , cc_tyargs = args, cc_fsk = fsk })
1380 = do { match_res <- matchFam fam_tc args
1381 -- Look up in top-level instances, or built-in axiom
1382 -- See Note [MATCHING-SYNONYMS]
1383 ; case match_res of
1384 Nothing -> do { improveTopFunEqs (ctEvLoc old_ev) fam_tc args fsk
1385 ; continueWith work_item }
1386 Just (ax_co, rhs_ty)
1387 -> reduce_top_fun_eq old_ev fsk ax_co rhs_ty }
1388
1389 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1390
1391 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> TcCoercion -> TcType
1392 -> TcS (StopOrContinue Ct)
1393 -- Found an applicable top-level axiom: use it to reduce
1394 reduce_top_fun_eq old_ev fsk ax_co rhs_ty
1395 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1396 , isTypeFamilyTyCon tc
1397 , tc_args `lengthIs` tyConArity tc -- Short-cut
1398 = shortCutReduction old_ev fsk ax_co tc tc_args
1399 -- Try shortcut; see Note [Short cut for top-level reaction]
1400
1401 | isGiven old_ev -- Not shortcut
1402 = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1403 -- final_co :: fsk ~ rhs_ty
1404 ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty,
1405 EvCoercion final_co)
1406 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1407 ; stopWith old_ev "Fun/Top (given)" }
1408
1409 -- So old_ev is Wanted or Derived
1410 | not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
1411 = do { dischargeFmv old_ev fsk ax_co rhs_ty
1412 ; traceTcS "doTopReactFunEq" $
1413 vcat [ text "old_ev:" <+> ppr old_ev
1414 , nest 2 (text ":=") <+> ppr ax_co ]
1415 ; stopWith old_ev "Fun/Top (wanted)" }
1416
1417 | otherwise -- We must not assign ufsk := ...ufsk...!
1418 = do { alpha_ty <- newFlexiTcSTy (tyVarKind fsk)
1419 ; new_ev <- case old_ev of
1420 CtWanted {} -> do { (ev, _) <- newWantedEq loc Nominal alpha_ty rhs_ty
1421 ; updWorkListTcS $
1422 extendWorkListEq (mkNonCanonical ev)
1423 ; return ev }
1424 CtDerived {} -> do { ev <- newDerivedNC loc pred
1425 ; updWorkListTcS (extendWorkListDerived loc ev)
1426 ; return ev }
1427 where pred = mkPrimEqPred alpha_ty rhs_ty
1428 _ -> pprPanic "reduce_top_fun_eq" (ppr old_ev)
1429
1430 -- By emitting this as non-canonical, we deal with all
1431 -- flattening, occurs-check, and ufsk := ufsk issues
1432 ; let final_co = ax_co `mkTcTransCo` mkTcSymCo (ctEvCoercion new_ev)
1433 -- ax_co :: fam_tc args ~ rhs_ty
1434 -- ev :: alpha ~ rhs_ty
1435 -- ufsk := alpha
1436 -- final_co :: fam_tc args ~ alpha
1437 ; dischargeFmv old_ev fsk final_co alpha_ty
1438 ; traceTcS "doTopReactFunEq (occurs)" $
1439 vcat [ text "old_ev:" <+> ppr old_ev
1440 , nest 2 (text ":=") <+> ppr final_co
1441 , text "new_ev:" <+> ppr new_ev ]
1442 ; stopWith old_ev "Fun/Top (wanted)" }
1443 where
1444 loc = ctEvLoc old_ev
1445 deeper_loc = bumpCtLocDepth loc
1446
1447 improveTopFunEqs :: CtLoc -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1448 improveTopFunEqs loc fam_tc args fsk
1449 = do { model <- getInertModel
1450 ; fam_envs <- getFamInstEnvs
1451 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1452 (lookupFlattenTyVar model fsk)
1453 ; mapM_ (unifyDerived loc Nominal) eqns }
1454
1455 improve_top_fun_eqs :: FamInstEnvs
1456 -> TyCon -> [TcType] -> TcType
1457 -> TcS [Eqn]
1458 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1459 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1460 = return (sfInteractTop ops args rhs_ty)
1461
1462 -- see Note [Type inference for type families with injectivity]
1463 | isOpenTypeFamilyTyCon fam_tc
1464 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1465 = -- it is possible to have several compatible equations in an open type
1466 -- family but we only want to derive equalities from one such equation.
1467 concatMapM (injImproveEqns injective_args) (take 1 $
1468 buildImprovementData (lookupFamInstEnvByTyCon fam_envs fam_tc)
1469 fi_tys fi_rhs (const Nothing))
1470
1471 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1472 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1473 = concatMapM (injImproveEqns injective_args) $
1474 buildImprovementData (fromBranches (co_ax_branches ax))
1475 cab_lhs cab_rhs Just
1476
1477 | otherwise
1478 = return []
1479 where
1480 buildImprovementData
1481 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1482 -> (a -> [Type]) -- get LHS of an axiom
1483 -> (a -> Type) -- get RHS of an axiom
1484 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1485 -> [( [Type], TCvSubst, TyVarSet, Maybe CoAxBranch )]
1486 -- Result:
1487 -- ( [arguments of a matching axiom]
1488 -- , RHS-unifying substitution
1489 -- , axiom variables without substitution
1490 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1491 buildImprovementData axioms axiomLHS axiomRHS wrap =
1492 [ (ax_args, subst, unsubstTvs, wrap axiom)
1493 | axiom <- axioms
1494 , let ax_args = axiomLHS axiom
1495 , let ax_rhs = axiomRHS axiom
1496 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1497 , let tvs = tyCoVarsOfTypes ax_args
1498 notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1499 unsubstTvs = filterVarSet (notInSubst <&&> isTyVar) tvs ]
1500
1501 injImproveEqns :: [Bool]
1502 -> ([Type], TCvSubst, TyCoVarSet, Maybe CoAxBranch)
1503 -> TcS [Eqn]
1504 injImproveEqns inj_args (ax_args, theta, unsubstTvs, cabr) = do
1505 (theta', _) <- instFlexiTcS (varSetElems unsubstTvs)
1506 let subst = theta `unionTCvSubst` theta'
1507 return [ Pair arg (substTy subst ax_arg)
1508 | case cabr of
1509 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
1510 _ -> True
1511 , (arg, ax_arg, True) <- zip3 args ax_args inj_args ]
1512
1513
1514 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1515 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1516 -- See Note [Top-level reductions for type functions]
1517 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1518 | isGiven old_ev
1519 = ASSERT( ctEvEqRel old_ev == NomEq )
1520 do { (xis, cos) <- flattenManyNom old_ev tc_args
1521 -- ax_co :: F args ~ G tc_args
1522 -- cos :: xis ~ tc_args
1523 -- old_ev :: F args ~ fsk
1524 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1525
1526 ; new_ev <- newGivenEvVar deeper_loc
1527 ( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1528 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1529 `mkTcTransCo` mkTcSymCo ax_co
1530 `mkTcTransCo` ctEvCoercion old_ev) )
1531
1532 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1533 ; emitWorkCt new_ct
1534 ; stopWith old_ev "Fun/Top (given, shortcut)" }
1535
1536 | otherwise
1537 = ASSERT( not (isDerived old_ev) ) -- Caller ensures this
1538 ASSERT( ctEvEqRel old_ev == NomEq )
1539 do { (xis, cos) <- flattenManyNom old_ev tc_args
1540 -- ax_co :: F args ~ G tc_args
1541 -- cos :: xis ~ tc_args
1542 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1543 -- new_ev :: G xis ~ fsk
1544 -- old_ev :: F args ~ fsk := ax_co ; sym (G cos) ; new_ev
1545
1546 ; (new_ev, new_co) <- newWantedEq deeper_loc Nominal
1547 (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1548 ; setWantedEq (ctev_dest old_ev)
1549 (ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal fam_tc cos)
1550 `mkTcTransCo` new_co)
1551
1552 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc, cc_tyargs = xis, cc_fsk = fsk }
1553 ; emitWorkCt new_ct
1554 ; stopWith old_ev "Fun/Top (wanted, shortcut)" }
1555 where
1556 loc = ctEvLoc old_ev
1557 deeper_loc = bumpCtLocDepth loc
1558
1559 dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1560 -- (dischargeFmv x fmv co ty)
1561 -- [W] ev :: F tys ~ fmv
1562 -- co :: F tys ~ xi
1563 -- Precondition: fmv is not filled, and fuv `notElem` xi
1564 --
1565 -- Then set fmv := xi,
1566 -- set ev := co
1567 -- kick out any inert things that are now rewritable
1568 --
1569 -- Does not evaluate 'co' if 'ev' is Derived
1570 dischargeFmv ev fmv co xi
1571 = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
1572 do { setEvBindIfWanted ev (EvCoercion co)
1573 ; unflattenFmv fmv xi
1574 ; n_kicked <- kickOutAfterUnification fmv
1575 ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1576
1577 {- Note [Top-level reductions for type functions]
1578 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1579 c.f. Note [The flattening story] in TcFlatten
1580
1581 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
1582 Here is what we do, in four cases:
1583
1584 * Wanteds: general firing rule
1585 (work item) [W] x : F tys ~ fmv
1586 instantiate axiom: ax_co : F tys ~ rhs
1587
1588 Then:
1589 Discharge fmv := alpha
1590 Discharge x := ax_co ; sym x2
1591 New wanted [W] x2 : alpha ~ rhs (Non-canonical)
1592 This is *the* way that fmv's get unified; even though they are
1593 "untouchable".
1594
1595 NB: it can be the case that fmv appears in the (instantiated) rhs.
1596 In that case the new Non-canonical wanted will be loopy, but that's
1597 ok. But it's good reason NOT to claim that it is canonical!
1598
1599 * Wanteds: short cut firing rule
1600 Applies when the RHS of the axiom is another type-function application
1601 (work item) [W] x : F tys ~ fmv
1602 instantiate axiom: ax_co : F tys ~ G rhs_tys
1603
1604 It would be a waste to create yet another fmv for (G rhs_tys).
1605 Instead (shortCutReduction):
1606 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
1607 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
1608 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
1609 - Discharge x := ax_co ; G cos ; x2
1610
1611 * Givens: general firing rule
1612 (work item) [G] g : F tys ~ fsk
1613 instantiate axiom: ax_co : F tys ~ rhs
1614
1615 Now add non-canonical given (since rhs is not flat)
1616 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
1617
1618 * Givens: short cut firing rule
1619 Applies when the RHS of the axiom is another type-function application
1620 (work item) [G] g : F tys ~ fsk
1621 instantiate axiom: ax_co : F tys ~ G rhs_tys
1622
1623 It would be a waste to create yet another fsk for (G rhs_tys).
1624 Instead (shortCutReduction):
1625 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
1626 - Add new Canonical given
1627 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
1628
1629 Note [Cached solved FunEqs]
1630 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1631 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1632 to see if we have reduced (FunExpensive big-type) before, lest we
1633 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1634 we must use `canDischarge` because both uses might (say) be Wanteds,
1635 and we *still* want to save the re-computation.
1636
1637 Note [MATCHING-SYNONYMS]
1638 ~~~~~~~~~~~~~~~~~~~~~~~~
1639 When trying to match a dictionary (D tau) to a top-level instance, or a
1640 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1641 we do *not* need to expand type synonyms because the matcher will do that for us.
1642
1643
1644 Note [RHS-FAMILY-SYNONYMS]
1645 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1646 The RHS of a family instance is represented as yet another constructor which is
1647 like a type synonym for the real RHS the programmer declared. Eg:
1648 type instance F (a,a) = [a]
1649 Becomes:
1650 :R32 a = [a] -- internal type synonym introduced
1651 F (a,a) ~ :R32 a -- instance
1652
1653 When we react a family instance with a type family equation in the work list
1654 we keep the synonym-using RHS without expansion.
1655
1656 Note [FunDep and implicit parameter reactions]
1657 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1658 Currently, our story of interacting two dictionaries (or a dictionary
1659 and top-level instances) for functional dependencies, and implicit
1660 paramters, is that we simply produce new Derived equalities. So for example
1661
1662 class D a b | a -> b where ...
1663 Inert:
1664 d1 :g D Int Bool
1665 WorkItem:
1666 d2 :w D Int alpha
1667
1668 We generate the extra work item
1669 cv :d alpha ~ Bool
1670 where 'cv' is currently unused. However, this new item can perhaps be
1671 spontaneously solved to become given and react with d2,
1672 discharging it in favour of a new constraint d2' thus:
1673 d2' :w D Int Bool
1674 d2 := d2' |> D Int cv
1675 Now d2' can be discharged from d1
1676
1677 We could be more aggressive and try to *immediately* solve the dictionary
1678 using those extra equalities, but that requires those equalities to carry
1679 evidence and derived do not carry evidence.
1680
1681 If that were the case with the same inert set and work item we might dischard
1682 d2 directly:
1683
1684 cv :w alpha ~ Bool
1685 d2 := d1 |> D Int cv
1686
1687 But in general it's a bit painful to figure out the necessary coercion,
1688 so we just take the first approach. Here is a better example. Consider:
1689 class C a b c | a -> b
1690 And:
1691 [Given] d1 : C T Int Char
1692 [Wanted] d2 : C T beta Int
1693 In this case, it's *not even possible* to solve the wanted immediately.
1694 So we should simply output the functional dependency and add this guy
1695 [but NOT its superclasses] back in the worklist. Even worse:
1696 [Given] d1 : C T Int beta
1697 [Wanted] d2: C T beta Int
1698 Then it is solvable, but its very hard to detect this on the spot.
1699
1700 It's exactly the same with implicit parameters, except that the
1701 "aggressive" approach would be much easier to implement.
1702
1703
1704 Note [Weird fundeps]
1705 ~~~~~~~~~~~~~~~~~~~~
1706 Consider class Het a b | a -> b where
1707 het :: m (f c) -> a -> m b
1708
1709 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1710 instance GHet (K a) (K [a])
1711 instance Het a b => GHet (K a) (K b)
1712
1713 The two instances don't actually conflict on their fundeps,
1714 although it's pretty strange. So they are both accepted. Now
1715 try [W] GHet (K Int) (K Bool)
1716 This triggers fundeps from both instance decls;
1717 [D] K Bool ~ K [a]
1718 [D] K Bool ~ K beta
1719 And there's a risk of complaining about Bool ~ [a]. But in fact
1720 the Wanted matches the second instance, so we never get as far
1721 as the fundeps.
1722
1723 Trac #7875 is a case in point.
1724
1725 Note [Overriding implicit parameters]
1726 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1727 Consider
1728 f :: (?x::a) -> Bool -> a
1729
1730 g v = let ?x::Int = 3
1731 in (f v, let ?x::Bool = True in f v)
1732
1733 This should probably be well typed, with
1734 g :: Bool -> (Int, Bool)
1735
1736 So the inner binding for ?x::Bool *overrides* the outer one.
1737 Hence a work-item Given overrides an inert-item Given.
1738 -}
1739
1740 {- *******************************************************************
1741 * *
1742 Class lookup
1743 * *
1744 **********************************************************************-}
1745
1746 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
1747 -- check.
1748 --
1749 -- See Note [Safe Haskell Overlapping Instances] in TcSimplify
1750 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
1751 type SafeOverlapping = Bool
1752
1753 data LookupInstResult
1754 = NoInstance
1755 | GenInst { lir_new_theta :: [TcPredType]
1756 , lir_mk_ev :: [EvTerm] -> EvTerm
1757 , lir_safe_over :: SafeOverlapping }
1758
1759 instance Outputable LookupInstResult where
1760 ppr NoInstance = text "NoInstance"
1761 ppr (GenInst { lir_new_theta = ev
1762 , lir_safe_over = s })
1763 = text "GenInst" <+> vcat [ppr ev, ss]
1764 where ss = text $ if s then "[safe]" else "[unsafe]"
1765
1766
1767 matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1768 matchClassInst dflags inerts clas tys loc
1769 -- First check whether there is an in-scope Given that could
1770 -- match this constraint. In that case, do not use top-level
1771 -- instances. See Note [Instance and Given overlap]
1772 | not (xopt LangExt.IncoherentInstances dflags)
1773 , not (naturallyCoherentClass clas)
1774 , let matchable_givens = matchableGivens loc pred inerts
1775 , not (isEmptyBag matchable_givens)
1776 = do { traceTcS "Delaying instance application" $
1777 vcat [ text "Work item=" <+> pprClassPred clas tys
1778 , text "Potential matching givens:" <+> ppr matchable_givens ]
1779 ; return NoInstance }
1780 where
1781 pred = mkClassPred clas tys
1782
1783 matchClassInst dflags _ clas tys loc
1784 = do { traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr (mkClassPred clas tys) ]
1785 ; res <- match_class_inst dflags clas tys loc
1786 ; traceTcS "matchClassInst result" $ ppr res
1787 ; return res }
1788
1789 match_class_inst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1790 match_class_inst dflags clas tys loc
1791 | cls_name == knownNatClassName = matchKnownNat clas tys
1792 | cls_name == knownSymbolClassName = matchKnownSymbol clas tys
1793 | isCTupleClass clas = matchCTuple clas tys
1794 | cls_name == typeableClassName = matchTypeable clas tys
1795 | clas `hasKey` heqTyConKey = matchLiftedEquality tys
1796 | clas `hasKey` coercibleTyConKey = matchLiftedCoercible tys
1797 | otherwise = matchInstEnv dflags clas tys loc
1798 where
1799 cls_name = className clas
1800
1801 {- Note [Instance and Given overlap]
1802 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1803 Example, from the OutsideIn(X) paper:
1804 instance P x => Q [x]
1805 instance (x ~ y) => R y [x]
1806
1807 wob :: forall a b. (Q [b], R b a) => a -> Int
1808
1809 g :: forall a. Q [a] => [a] -> Int
1810 g x = wob x
1811
1812 This will generate the impliation constraint:
1813 Q [a] => (Q [beta], R beta [a])
1814 If we react (Q [beta]) with its top-level axiom, we end up with a
1815 (P beta), which we have no way of discharging. On the other hand,
1816 if we react R beta [a] with the top-level we get (beta ~ a), which
1817 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1818 now solvable by the given Q [a].
1819
1820 The solution is that:
1821 In matchClassInst (and thus in topReact), we return a matching
1822 instance only when there is no Given in the inerts which is
1823 unifiable to this particular dictionary.
1824
1825 We treat any meta-tyvar as "unifiable" for this purpose,
1826 *including* untouchable ones
1827
1828 The end effect is that, much as we do for overlapping instances, we
1829 delay choosing a class instance if there is a possibility of another
1830 instance OR a given to match our constraint later on. This fixes
1831 Trac #4981 and #5002.
1832
1833 Other notes:
1834
1835 * The check is done *first*, so that it also covers classes
1836 with built-in instance solving, such as
1837 - constraint tuples
1838 - natural numbers
1839 - Typeable
1840
1841 * The given-overlap problem is arguably not easy to appear in practice
1842 due to our aggressive prioritization of equality solving over other
1843 constraints, but it is possible. I've added a test case in
1844 typecheck/should-compile/GivenOverlapping.hs
1845
1846 * Another "live" example is Trac #10195; another is #10177.
1847
1848 * We ignore the overlap problem if -XIncoherentInstances is in force:
1849 see Trac #6002 for a worked-out example where this makes a
1850 difference.
1851
1852 * Moreover notice that our goals here are different than the goals of
1853 the top-level overlapping checks. There we are interested in
1854 validating the following principle:
1855
1856 If we inline a function f at a site where the same global
1857 instance environment is available as the instance environment at
1858 the definition site of f then we should get the same behaviour.
1859
1860 But for the Given Overlap check our goal is just related to completeness of
1861 constraint solving.
1862 -}
1863
1864
1865 {- *******************************************************************
1866 * *
1867 Class lookup in the instance environment
1868 * *
1869 **********************************************************************-}
1870
1871 matchInstEnv :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1872 matchInstEnv dflags clas tys loc
1873 = do { instEnvs <- getInstEnvs
1874 ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
1875 (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
1876 safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
1877 ; case (matches, unify, safeHaskFail) of
1878
1879 -- Nothing matches
1880 ([], _, _)
1881 -> do { traceTcS "matchClass not matching" $
1882 vcat [ text "dict" <+> ppr pred ]
1883 ; return NoInstance }
1884
1885 -- A single match (& no safe haskell failure)
1886 ([(ispec, inst_tys)], [], False)
1887 -> do { let dfun_id = instanceDFunId ispec
1888 ; traceTcS "matchClass success" $
1889 vcat [text "dict" <+> ppr pred,
1890 text "witness" <+> ppr dfun_id
1891 <+> ppr (idType dfun_id) ]
1892 -- Record that this dfun is needed
1893 ; match_one (null unsafeOverlaps) dfun_id inst_tys }
1894
1895 -- More than one matches (or Safe Haskell fail!). Defer any
1896 -- reactions of a multitude until we learn more about the reagent
1897 (matches, _, _)
1898 -> do { traceTcS "matchClass multiple matches, deferring choice" $
1899 vcat [text "dict" <+> ppr pred,
1900 text "matches" <+> ppr matches]
1901 ; return NoInstance } }
1902 where
1903 pred = mkClassPred clas tys
1904
1905 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
1906 -- See Note [DFunInstType: instantiating types] in InstEnv
1907 match_one so dfun_id mb_inst_tys
1908 = do { checkWellStagedDFun pred dfun_id loc
1909 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
1910 ; return $ GenInst { lir_new_theta = theta
1911 , lir_mk_ev = EvDFunApp dfun_id tys
1912 , lir_safe_over = so } }
1913
1914
1915 {- ********************************************************************
1916 * *
1917 Class lookup for CTuples
1918 * *
1919 ***********************************************************************-}
1920
1921 matchCTuple :: Class -> [Type] -> TcS LookupInstResult
1922 matchCTuple clas tys -- (isCTupleClass clas) holds
1923 = return (GenInst { lir_new_theta = tys
1924 , lir_mk_ev = tuple_ev
1925 , lir_safe_over = True })
1926 -- The dfun *is* the data constructor!
1927 where
1928 data_con = tyConSingleDataCon (classTyCon clas)
1929 tuple_ev = EvDFunApp (dataConWrapId data_con) tys
1930
1931 {- ********************************************************************
1932 * *
1933 Class lookup for Literals
1934 * *
1935 ***********************************************************************-}
1936
1937 matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
1938 matchKnownNat clas [ty] -- clas = KnownNat
1939 | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n)
1940 matchKnownNat _ _ = return NoInstance
1941
1942 matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
1943 matchKnownSymbol clas [ty] -- clas = KnownSymbol
1944 | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n)
1945 matchKnownSymbol _ _ = return NoInstance
1946
1947
1948 makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
1949 -- makeLitDict adds a coercion that will convert the literal into a dictionary
1950 -- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
1951 -- in TcEvidence. The coercion happens in 2 steps:
1952 --
1953 -- Integer -> SNat n -- representation of literal to singleton
1954 -- SNat n -> KnownNat n -- singleton to dictionary
1955 --
1956 -- The process is mirrored for Symbols:
1957 -- String -> SSymbol n
1958 -- SSymbol n -> KnownSymbol n -}
1959 makeLitDict clas ty evLit
1960 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
1961 -- co_dict :: KnownNat n ~ SNat n
1962 , [ meth ] <- classMethods clas
1963 , Just tcRep <- tyConAppTyCon_maybe -- SNat
1964 $ funResultTy -- SNat n
1965 $ dropForAlls -- KnownNat n => SNat n
1966 $ idType meth -- forall n. KnownNat n => SNat n
1967 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
1968 -- SNat n ~ Integer
1969 , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
1970 = return $ GenInst { lir_new_theta = []
1971 , lir_mk_ev = \_ -> ev_tm
1972 , lir_safe_over = True }
1973
1974 | otherwise
1975 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1976 $$ vcat (map (ppr . idType) (classMethods clas)))
1977
1978
1979 {- ********************************************************************
1980 * *
1981 Class lookup for Typeable
1982 * *
1983 ***********************************************************************-}
1984
1985 -- | Assumes that we've checked that this is the 'Typeable' class,
1986 -- and it was applied to the correct argument.
1987 matchTypeable :: Class -> [Type] -> TcS LookupInstResult
1988 matchTypeable clas [k,t] -- clas = Typeable
1989 -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
1990 | isForAllTy k = return NoInstance -- Polytype
1991 | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type
1992
1993 -- Now cases that do work
1994 | k `eqType` typeNatKind = doTyLit knownNatClassName t
1995 | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t
1996 | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
1997 , onlyNamedBndrsApplied tc ks = doTyConApp clas t ks
1998 | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt
1999
2000 matchTypeable _ _ = return NoInstance
2001
2002 doTyConApp :: Class -> Type -> [Kind] -> TcS LookupInstResult
2003 -- Representation for type constructor applied to some kinds
2004 doTyConApp clas ty args
2005 = return $ GenInst (map (mk_typeable_pred clas) args)
2006 (\tms -> EvTypeable ty $ EvTypeableTyCon tms)
2007 True
2008
2009 -- Representation for concrete kinds. We just use the kind itself,
2010 -- but first we must make sure that we've instantiated all kind-
2011 -- polymorphism, but no more.
2012 onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
2013 onlyNamedBndrsApplied tc ks
2014 = all isNamedBinder used_bndrs &&
2015 not (any isNamedBinder leftover_bndrs)
2016 where
2017 (bndrs, _) = splitPiTys (tyConKind tc)
2018 (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
2019
2020 doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
2021 -- Representation for an application of a type to a type-or-kind.
2022 -- This may happen when the type expression starts with a type variable.
2023 -- Example (ignoring kind parameter):
2024 -- Typeable (f Int Char) -->
2025 -- (Typeable (f Int), Typeable Char) -->
2026 -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
2027 -- Typeable f
2028 doTyApp clas ty f tk
2029 | isForAllTy (typeKind f)
2030 = return NoInstance -- We can't solve until we know the ctr.
2031 | otherwise
2032 = return $ GenInst [mk_typeable_pred clas f, mk_typeable_pred clas tk]
2033 (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp t1 t2)
2034 True
2035
2036 -- Emit a `Typeable` constraint for the given type.
2037 mk_typeable_pred :: Class -> Type -> PredType
2038 mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
2039
2040 -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
2041 -- we generate a sub-goal for the appropriate class. See #10348 for what
2042 -- happens when we fail to do this.
2043 doTyLit :: Name -> Type -> TcS LookupInstResult
2044 doTyLit kc t = do { kc_clas <- tcLookupClass kc
2045 ; let kc_pred = mkClassPred kc_clas [ t ]
2046 mk_ev [ev] = EvTypeable t $ EvTypeableTyLit ev
2047 mk_ev _ = panic "doTyLit"
2048 ; return (GenInst [kc_pred] mk_ev True) }
2049
2050 {- Note [Typeable (T a b c)]
2051 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2052 For type applications we always decompose using binary application,
2053 vai doTyApp, until we get to a *kind* instantiation. Exmaple
2054 Proxy :: forall k. k -> *
2055
2056 To solve Typeable (Proxy (* -> *) Maybe) we
2057 - First decompose with doTyApp,
2058 to get (Typeable (Proxy (* -> *))) and Typeable Maybe
2059 - Then sovle (Typeable (Proxy (* -> *))) with doTyConApp
2060
2061 If we attempt to short-cut by solving it all at once, via
2062 doTyCOnAPp
2063
2064
2065 Note [No Typeable for polytypes or qualified types]
2066 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2067 We do not support impredicative typeable, such as
2068 Typeable (forall a. a->a)
2069 Typeable (Eq a => a -> a)
2070 Typeable (() => Int)
2071 Typeable (((),()) => Int)
2072
2073 See Trac #9858. For forall's the case is clear: we simply don't have
2074 a TypeRep for them. For qualified but not polymorphic types, like
2075 (Eq a => a -> a), things are murkier. But:
2076
2077 * We don't need a TypeRep for these things. TypeReps are for
2078 monotypes only.
2079
2080 * Perhaps we could treat `=>` as another type constructor for `Typeable`
2081 purposes, and thus support things like `Eq Int => Int`, however,
2082 at the current state of affairs this would be an odd exception as
2083 no other class works with impredicative types.
2084 For now we leave it off, until we have a better story for impredicativity.
2085 -}
2086
2087 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
2088 solveCallStack ev ev_cs = do
2089 -- We're given ev_cs :: CallStack, but the evidence term should be a
2090 -- dictionary, so we have to coerce ev_cs to a dictionary for
2091 -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
2092 let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
2093 setWantedEvBind (ctEvId ev) ev_tm
2094
2095 {- ********************************************************************
2096 * *
2097 Class lookup for lifted equality
2098 * *
2099 ***********************************************************************-}
2100
2101 matchLiftedEquality :: [Type] -> TcS LookupInstResult
2102 matchLiftedEquality args
2103 = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
2104 , lir_mk_ev = EvDFunApp (dataConWrapId heqDataCon) args
2105 , lir_safe_over = True })
2106
2107 matchLiftedCoercible :: [Type] -> TcS LookupInstResult
2108 matchLiftedCoercible args@[k, t1, t2]
2109 = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
2110 , lir_mk_ev = EvDFunApp (dataConWrapId coercibleDataCon)
2111 args
2112 , lir_safe_over = True })
2113 where
2114 args' = [k, k, t1, t2]
2115 matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)