Use top-level instances to solve superclasses where possible
[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 ( SwapFlag(..), isSwapped,
13 infinity, IntWithInf, intGtLimit )
14 import HsTypes ( HsIPName(..) )
15 import TcCanonical
16 import TcFlatten
17 import TcUnify( canSolveByUnification )
18 import VarSet
19 import Type
20 import InstEnv( DFunInstType, lookupInstEnv, instanceDFunId )
21 import CoAxiom( sfInteractTop, sfInteractInert )
22
23 import Var
24 import TcType
25 import Name
26 import PrelNames ( knownNatClassName, knownSymbolClassName,
27 typeableClassName, coercibleTyConKey,
28 heqTyConKey, ipClassKey )
29 import TysWiredIn ( typeNatKind, typeSymbolKind, heqDataCon,
30 coercibleDataCon )
31 import TysPrim ( eqPrimTyCon, eqReprPrimTyCon )
32 import Id( idType )
33 import CoAxiom ( TypeEqn, CoAxiom(..), CoAxBranch(..), fromBranches )
34 import Class
35 import TyCon
36 import DataCon( dataConWrapId )
37 import FunDeps
38 import FamInst
39 import FamInstEnv
40 import Unify ( tcUnifyTyWithTFs )
41
42 import TcEvidence
43 import Outputable
44
45 import TcRnTypes
46 import TcSMonad
47 import Bag
48 import MonadUtils ( concatMapM )
49
50 import Data.List( partition, foldl', deleteFirstsBy )
51 import SrcLoc
52 import VarEnv
53
54 import Control.Monad
55 import Maybes( isJust )
56 import Pair (Pair(..))
57 import Unique( hasKey )
58 import DynFlags
59 import Util
60 import qualified GHC.LanguageExtensions as LangExt
61
62 import Control.Monad.Trans.Class
63 import Control.Monad.Trans.Maybe
64
65 {-
66 **********************************************************************
67 * *
68 * Main Interaction Solver *
69 * *
70 **********************************************************************
71
72 Note [Basic Simplifier Plan]
73 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
74 1. Pick an element from the WorkList if there exists one with depth
75 less than our context-stack depth.
76
77 2. Run it down the 'stage' pipeline. Stages are:
78 - canonicalization
79 - inert reactions
80 - spontaneous reactions
81 - top-level intreactions
82 Each stage returns a StopOrContinue and may have sideffected
83 the inerts or worklist.
84
85 The threading of the stages is as follows:
86 - If (Stop) is returned by a stage then we start again from Step 1.
87 - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
88 the next stage in the pipeline.
89 4. If the element has survived (i.e. ContinueWith x) the last stage
90 then we add him in the inerts and jump back to Step 1.
91
92 If in Step 1 no such element exists, we have exceeded our context-stack
93 depth and will simply fail.
94
95 Note [Unflatten after solving the simple wanteds]
96 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
97 We unflatten after solving the wc_simples of an implication, and before attempting
98 to float. This means that
99
100 * The fsk/fmv flatten-skolems only survive during solveSimples. We don't
101 need to worry about them across successive passes over the constraint tree.
102 (E.g. we don't need the old ic_fsk field of an implication.
103
104 * When floating an equality outwards, we don't need to worry about floating its
105 associated flattening constraints.
106
107 * Another tricky case becomes easy: Trac #4935
108 type instance F True a b = a
109 type instance F False a b = b
110
111 [w] F c a b ~ gamma
112 (c ~ True) => a ~ gamma
113 (c ~ False) => b ~ gamma
114
115 Obviously this is soluble with gamma := F c a b, and unflattening
116 will do exactly that after solving the simple constraints and before
117 attempting the implications. Before, when we were not unflattening,
118 we had to push Wanted funeqs in as new givens. Yuk!
119
120 Another example that becomes easy: indexed_types/should_fail/T7786
121 [W] BuriedUnder sub k Empty ~ fsk
122 [W] Intersect fsk inv ~ s
123 [w] xxx[1] ~ s
124 [W] forall[2] . (xxx[1] ~ Empty)
125 => Intersect (BuriedUnder sub k Empty) inv ~ Empty
126
127 Note [Running plugins on unflattened wanteds]
128 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
129 There is an annoying mismatch between solveSimpleGivens and
130 solveSimpleWanteds, because the latter needs to fiddle with the inert
131 set, unflatten and zonk the wanteds. It passes the zonked wanteds
132 to runTcPluginsWanteds, which produces a replacement set of wanteds,
133 some additional insolubles and a flag indicating whether to go round
134 the loop again. If so, prepareInertsForImplications is used to remove
135 the previous wanteds (which will still be in the inert set). Note
136 that prepareInertsForImplications will discard the insolubles, so we
137 must keep track of them separately.
138 -}
139
140 solveSimpleGivens :: [Ct] -> TcS ()
141 solveSimpleGivens givens
142 | null givens -- Shortcut for common case
143 = return ()
144 | otherwise
145 = do { traceTcS "solveSimpleGivens {" (ppr givens)
146 ; go givens
147 ; traceTcS "End solveSimpleGivens }" empty }
148 where
149 go givens = do { solveSimples (listToBag givens)
150 ; new_givens <- runTcPluginsGiven
151 ; when (notNull new_givens) $
152 go new_givens }
153
154 solveSimpleWanteds :: Cts -> TcS WantedConstraints
155 -- NB: 'simples' may contain /derived/ equalities, floated
156 -- out from a nested implication. So don't discard deriveds!
157 solveSimpleWanteds simples
158 = do { traceTcS "solveSimpleWanteds {" (ppr simples)
159 ; dflags <- getDynFlags
160 ; (n,wc) <- go 1 (solverIterations dflags) (emptyWC { wc_simple = simples })
161 ; traceTcS "solveSimpleWanteds end }" $
162 vcat [ text "iterations =" <+> ppr n
163 , text "residual =" <+> ppr wc ]
164 ; return wc }
165 where
166 go :: Int -> IntWithInf -> WantedConstraints -> TcS (Int, WantedConstraints)
167 go n limit wc
168 | n `intGtLimit` limit
169 = failTcS (hang (text "solveSimpleWanteds: too many iterations"
170 <+> parens (text "limit =" <+> ppr limit))
171 2 (vcat [ text "Set limit with -fconstraint-solver-iterations=n; n=0 for no limit"
172 , text "Simples =" <+> ppr simples
173 , text "WC =" <+> ppr wc ]))
174
175 | isEmptyBag (wc_simple wc)
176 = return (n,wc)
177
178 | otherwise
179 = do { -- Solve
180 (unif_count, wc1) <- solve_simple_wanteds wc
181
182 -- Run plugins
183 ; (rerun_plugin, wc2) <- runTcPluginsWanted wc1
184 -- See Note [Running plugins on unflattened wanteds]
185
186 ; if unif_count == 0 && not rerun_plugin
187 then return (n, wc2) -- Done
188 else do { traceTcS "solveSimple going round again:" $
189 ppr unif_count $$ ppr rerun_plugin
190 ; go (n+1) limit wc2 } } -- Loop
191
192
193 solve_simple_wanteds :: WantedConstraints -> TcS (Int, WantedConstraints)
194 -- Try solving these constraints
195 -- Affects the unification state (of course) but not the inert set
196 solve_simple_wanteds (WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
197 = nestTcS $
198 do { solveSimples simples1
199 ; (implics2, tv_eqs, fun_eqs, insols2, others) <- getUnsolvedInerts
200 ; (unif_count, unflattened_eqs) <- reportUnifications $
201 unflatten tv_eqs fun_eqs
202 -- See Note [Unflatten after solving the simple wanteds]
203 ; return ( unif_count
204 , WC { wc_simple = others `andCts` unflattened_eqs
205 , wc_insol = insols1 `andCts` insols2
206 , wc_impl = implics1 `unionBags` implics2 }) }
207
208 {- Note [The solveSimpleWanteds loop]
209 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
210 Solving a bunch of simple constraints is done in a loop,
211 (the 'go' loop of 'solveSimpleWanteds'):
212 1. Try to solve them; unflattening may lead to improvement that
213 was not exploitable during solving
214 2. Try the plugin
215 3. If step 1 did improvement during unflattening; or if the plugin
216 wants to run again, go back to step 1
217
218 Non-obviously, improvement can also take place during
219 the unflattening that takes place in step (1). See TcFlatten,
220 See Note [Unflattening can force the solver to iterate]
221 -}
222
223 -- The main solver loop implements Note [Basic Simplifier Plan]
224 ---------------------------------------------------------------
225 solveSimples :: Cts -> TcS ()
226 -- Returns the final InertSet in TcS
227 -- Has no effect on work-list or residual-implications
228 -- The constraints are initially examined in left-to-right order
229
230 solveSimples cts
231 = {-# SCC "solveSimples" #-}
232 do { updWorkListTcS (\wl -> foldrBag extendWorkListCt wl cts)
233 ; solve_loop }
234 where
235 solve_loop
236 = {-# SCC "solve_loop" #-}
237 do { sel <- selectNextWorkItem
238 ; case sel of
239 Nothing -> return ()
240 Just ct -> do { runSolverPipeline thePipeline ct
241 ; solve_loop } }
242
243 -- | Extract the (inert) givens and invoke the plugins on them.
244 -- Remove solved givens from the inert set and emit insolubles, but
245 -- return new work produced so that 'solveSimpleGivens' can feed it back
246 -- into the main solver.
247 runTcPluginsGiven :: TcS [Ct]
248 runTcPluginsGiven
249 = do { plugins <- getTcPlugins
250 ; if null plugins then return [] else
251 do { givens <- getInertGivens
252 ; if null givens then return [] else
253 do { p <- runTcPlugins plugins (givens,[],[])
254 ; let (solved_givens, _, _) = pluginSolvedCts p
255 ; updInertCans (removeInertCts solved_givens)
256 ; mapM_ emitInsoluble (pluginBadCts p)
257 ; return (pluginNewCts p) } } }
258
259 -- | Given a bag of (flattened, zonked) wanteds, invoke the plugins on
260 -- them and produce an updated bag of wanteds (possibly with some new
261 -- work) and a bag of insolubles. The boolean indicates whether
262 -- 'solveSimpleWanteds' should feed the updated wanteds back into the
263 -- main solver.
264 runTcPluginsWanted :: WantedConstraints -> TcS (Bool, WantedConstraints)
265 runTcPluginsWanted wc@(WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 })
266 | isEmptyBag simples1
267 = return (False, wc)
268 | otherwise
269 = do { plugins <- getTcPlugins
270 ; if null plugins then return (False, wc) else
271
272 do { given <- getInertGivens
273 ; simples1 <- zonkSimples simples1 -- Plugin requires zonked inputs
274 ; let (wanted, derived) = partition isWantedCt (bagToList simples1)
275 ; p <- runTcPlugins plugins (given, derived, wanted)
276 ; let (_, _, solved_wanted) = pluginSolvedCts p
277 (_, unsolved_derived, unsolved_wanted) = pluginInputCts p
278 new_wanted = pluginNewCts p
279
280 -- SLPJ: I'm deeply suspicious of this
281 -- ; updInertCans (removeInertCts $ solved_givens ++ solved_deriveds)
282
283 ; mapM_ setEv solved_wanted
284 ; return ( notNull (pluginNewCts p)
285 , WC { wc_simple = listToBag new_wanted `andCts` listToBag unsolved_wanted
286 `andCts` listToBag unsolved_derived
287 , wc_insol = listToBag (pluginBadCts p) `andCts` insols1
288 , wc_impl = implics1 } ) } }
289 where
290 setEv :: (EvTerm,Ct) -> TcS ()
291 setEv (ev,ct) = case ctEvidence ct of
292 CtWanted { ctev_dest = dest } -> setWantedEvTerm dest ev
293 _ -> panic "runTcPluginsWanted.setEv: attempt to solve non-wanted!"
294
295 -- | A triple of (given, derived, wanted) constraints to pass to plugins
296 type SplitCts = ([Ct], [Ct], [Ct])
297
298 -- | A solved triple of constraints, with evidence for wanteds
299 type SolvedCts = ([Ct], [Ct], [(EvTerm,Ct)])
300
301 -- | Represents collections of constraints generated by typechecker
302 -- plugins
303 data TcPluginProgress = TcPluginProgress
304 { pluginInputCts :: SplitCts
305 -- ^ Original inputs to the plugins with solved/bad constraints
306 -- removed, but otherwise unmodified
307 , pluginSolvedCts :: SolvedCts
308 -- ^ Constraints solved by plugins
309 , pluginBadCts :: [Ct]
310 -- ^ Constraints reported as insoluble by plugins
311 , pluginNewCts :: [Ct]
312 -- ^ New constraints emitted by plugins
313 }
314
315 getTcPlugins :: TcS [TcPluginSolver]
316 getTcPlugins = do { tcg_env <- getGblEnv; return (tcg_tc_plugins tcg_env) }
317
318 -- | Starting from a triple of (given, derived, wanted) constraints,
319 -- invoke each of the typechecker plugins in turn and return
320 --
321 -- * the remaining unmodified constraints,
322 -- * constraints that have been solved,
323 -- * constraints that are insoluble, and
324 -- * new work.
325 --
326 -- Note that new work generated by one plugin will not be seen by
327 -- other plugins on this pass (but the main constraint solver will be
328 -- re-invoked and they will see it later). There is no check that new
329 -- work differs from the original constraints supplied to the plugin:
330 -- the plugin itself should perform this check if necessary.
331 runTcPlugins :: [TcPluginSolver] -> SplitCts -> TcS TcPluginProgress
332 runTcPlugins plugins all_cts
333 = foldM do_plugin initialProgress plugins
334 where
335 do_plugin :: TcPluginProgress -> TcPluginSolver -> TcS TcPluginProgress
336 do_plugin p solver = do
337 result <- runTcPluginTcS (uncurry3 solver (pluginInputCts p))
338 return $ progress p result
339
340 progress :: TcPluginProgress -> TcPluginResult -> TcPluginProgress
341 progress p (TcPluginContradiction bad_cts) =
342 p { pluginInputCts = discard bad_cts (pluginInputCts p)
343 , pluginBadCts = bad_cts ++ pluginBadCts p
344 }
345 progress p (TcPluginOk solved_cts new_cts) =
346 p { pluginInputCts = discard (map snd solved_cts) (pluginInputCts p)
347 , pluginSolvedCts = add solved_cts (pluginSolvedCts p)
348 , pluginNewCts = new_cts ++ pluginNewCts p
349 }
350
351 initialProgress = TcPluginProgress all_cts ([], [], []) [] []
352
353 discard :: [Ct] -> SplitCts -> SplitCts
354 discard cts (xs, ys, zs) =
355 (xs `without` cts, ys `without` cts, zs `without` cts)
356
357 without :: [Ct] -> [Ct] -> [Ct]
358 without = deleteFirstsBy eqCt
359
360 eqCt :: Ct -> Ct -> Bool
361 eqCt c c' = ctFlavour c == ctFlavour c'
362 && ctPred c `tcEqType` ctPred c'
363
364 add :: [(EvTerm,Ct)] -> SolvedCts -> SolvedCts
365 add xs scs = foldl' addOne scs xs
366
367 addOne :: SolvedCts -> (EvTerm,Ct) -> SolvedCts
368 addOne (givens, deriveds, wanteds) (ev,ct) = case ctEvidence ct of
369 CtGiven {} -> (ct:givens, deriveds, wanteds)
370 CtDerived{} -> (givens, ct:deriveds, wanteds)
371 CtWanted {} -> (givens, deriveds, (ev,ct):wanteds)
372
373
374 type WorkItem = Ct
375 type SimplifierStage = WorkItem -> TcS (StopOrContinue Ct)
376
377 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
378 -> WorkItem -- The work item
379 -> TcS ()
380 -- Run this item down the pipeline, leaving behind new work and inerts
381 runSolverPipeline pipeline workItem
382 = do { wl <- getWorkList
383 ; inerts <- getTcSInerts
384 ; traceTcS "----------------------------- " empty
385 ; traceTcS "Start solver pipeline {" $
386 vcat [ text "work item =" <+> ppr workItem
387 , text "inerts =" <+> ppr inerts
388 , text "rest of worklist =" <+> ppr wl ]
389
390 ; bumpStepCountTcS -- One step for each constraint processed
391 ; final_res <- run_pipeline pipeline (ContinueWith workItem)
392
393 ; case final_res of
394 Stop ev s -> do { traceFireTcS ev s
395 ; traceTcS "End solver pipeline (discharged) }" empty
396 ; return () }
397 ContinueWith ct -> do { addInertCan ct
398 ; traceFireTcS (ctEvidence ct) (text "Kept as inert")
399 ; traceTcS "End solver pipeline (kept as inert) }" $
400 (text "final_item =" <+> ppr 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 Note [Solving from instances when interacting Dicts]
683 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
684 When we interact a [W] constraint with a [G] constraint that solves it, there is
685 a possibility that we could produce better code if instead we solved from a
686 top-level instance declaration (See #12791, #5835). For example:
687
688 class M a b where m :: a -> b
689
690 type C a b = (Num a, M a b)
691
692 f :: C Int b => b -> Int -> Int
693 f _ x = x + 1
694
695 The body of `f` requires a [W] `Num Int` instance. We could solve this
696 constraint from the givens because we have `C Int b` and that provides us a
697 solution for `Num Int`. This would let us produce core like the following
698 (with -O2):
699
700 f :: forall b. C Int b => b -> Int -> Int
701 f = \ (@ b) ($d(%,%) :: C Int b) _ (eta1 :: Int) ->
702 + @ Int
703 (GHC.Classes.$p1(%,%) @ (Num Int) @ (M Int b) $d(%,%))
704 eta1
705 A.f1
706
707 This is bad! We could do much better if we solved [W] `Num Int` directly from
708 the instance that we have in scope:
709
710 f :: forall b. C Int b => b -> Int -> Int
711 f = \ (@ b) _ _ (x :: Int) ->
712 case x of { GHC.Types.I# x1 -> GHC.Types.I# (GHC.Prim.+# x1 1#) }
713
714 However, there is a reason why the solver does not simply try to solve such
715 constraints with top-level instances. If the solver finds a relevant instance
716 declaration in scope, that instance may require a context that can't be solved
717 for. A good example of this is:
718
719 f :: Ord [a] => ...
720 f x = ..Need Eq [a]...
721
722 If we have instance `Eq a => Eq [a]` in scope and we tried to use it, we would
723 be left with the obligation to solve the constraint Eq a, which we cannot. So we
724 must be conservative in our attempt to use an instance declaration to solve the
725 [W] constraint we're interested in. Our rule is that we try to solve all of the
726 instance's subgoals recursively all at once. Precisely: We only attempt to
727 solve constraints of the form `C1, ... Cm => C t1 ... t n`, where all the Ci are
728 themselves class constraints of the form `C1', ... Cm' => C' t1' ... tn'` and we
729 only succeed if the entire tree of constraints is solvable from instances.
730
731 An example that succeeds:
732
733 class Eq a => C a b | b -> a where
734 m :: b -> a
735
736 f :: C [Int] b => b -> Bool
737 f x = m x == []
738
739 We solve for `Eq [Int]`, which requires `Eq Int`, which we also have. This
740 produces the following core:
741
742 f :: forall b. C [Int] b => b -> Bool
743 f = \ (@ b) ($dC :: C [Int] b) (x :: b) ->
744 GHC.Classes.$fEq[]_$s$c==
745 (m @ [Int] @ b $dC x) (GHC.Types.[] @ Int)
746
747 An example that fails:
748
749 class Eq a => C a b | b -> a where
750 m :: b -> a
751
752 f :: C [a] b => b -> Bool
753 f x = m x == []
754
755 Which, because solving `Eq [a]` demands `Eq a` which we cannot solve, produces:
756
757 f :: forall a b. C [a] b => b -> Bool
758 f = \ (@ a) (@ b) ($dC :: C [a] b) (eta :: b) ->
759 ==
760 @ [a]
761 (A.$p1C @ [a] @ b $dC)
762 (m @ [a] @ b $dC eta)
763 (GHC.Types.[] @ a)
764
765 This optimization relies on coherence of dictionaries to be correct. When we
766 cannot assume coherence because of IncoherentInstances then this optimization
767 can change the behavior of the users code.
768
769 The following four modules produce a program whose output would change depending
770 on whether we apply this optimization when IncoherentInstances is in effect:
771
772 #########
773 {-# LANGUAGE MultiParamTypeClasses #-}
774 module A where
775
776 class A a where
777 int :: a -> Int
778
779 class A a => C a b where
780 m :: b -> a -> a
781
782 #########
783 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
784 module B where
785
786 import A
787
788 instance A a where
789 int _ = 1
790
791 instance C a [b] where
792 m _ = id
793
794 #########
795 {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}
796 {-# LANGUAGE IncoherentInstances #-}
797 module C where
798
799 import A
800
801 instance A Int where
802 int _ = 2
803
804 instance C Int [Int] where
805 m _ = id
806
807 intC :: C Int a => a -> Int -> Int
808 intC _ x = int x
809
810 #########
811 module Main where
812
813 import A
814 import B
815 import C
816
817 main :: IO ()
818 main = print (intC [] (0::Int))
819
820 The output of `main` if we avoid the optimization under the effect of
821 IncoherentInstances is `1`. If we were to do the optimization, the output of
822 `main` would be `2`.
823
824 It is important to emphasize that failure means that we don't produce more
825 efficient code, NOT that we fail to typecheck at all! This is purely an
826 an optimization: exactly the same programs should typecheck with or without this
827 procedure.
828
829 -}
830
831 interactDict :: InertCans -> Ct -> TcS (StopOrContinue Ct)
832 interactDict inerts workItem@(CDictCan { cc_ev = ev_w, cc_class = cls, cc_tyargs = tys })
833 | isWanted ev_w
834 , Just ip_name <- isCallStackPred (ctPred workItem)
835 , OccurrenceOf func <- ctLocOrigin (ctEvLoc ev_w)
836 -- If we're given a CallStack constraint that arose from a function
837 -- call, we need to push the current call-site onto the stack instead
838 -- of solving it directly from a given.
839 -- See Note [Overview of implicit CallStacks]
840 = do { let loc = ctEvLoc ev_w
841
842 -- First we emit a new constraint that will capture the
843 -- given CallStack.
844 ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
845 -- We change the origin to IPOccOrigin so
846 -- this rule does not fire again.
847 -- See Note [Overview of implicit CallStacks]
848
849 ; mb_new <- newWantedEvVar new_loc (ctEvPred ev_w)
850 ; emitWorkNC (freshGoals [mb_new])
851
852 -- Then we solve the wanted by pushing the call-site onto the
853 -- newly emitted CallStack.
854 ; let ev_cs = EvCsPushCall func (ctLocSpan loc) (getEvTerm mb_new)
855 ; solveCallStack ev_w ev_cs
856 ; stopWith ev_w "Wanted CallStack IP" }
857 | Just ctev_i <- lookupInertDict inerts cls tys
858 = do
859 { dflags <- getDynFlags
860 -- See Note [Solving from instances when interacting Dicts]
861 ; try_inst_res <- trySolveFromInstance dflags ev_w ctev_i
862 ; case try_inst_res of
863 Just evs -> do
864 { flip mapM_ evs $ \(ev_t, ct_ev, cls, typ) -> do
865 { setWantedEvBind (ctEvId ct_ev) ev_t
866 ; addSolvedDict ct_ev cls typ }
867 ; stopWith ev_w "interactDict/solved from instance" }
868 -- We were unable to solve the [W] constraint from in-scope instances so
869 -- we solve it from the solution in the inerts we just retrieved.
870 Nothing -> do
871 { (inert_effect, stop_now) <- solveOneFromTheOther ctev_i ev_w
872 ; case inert_effect of
873 IRKeep -> return ()
874 IRDelete -> updInertDicts $ \ ds -> delDict ds cls tys
875 IRReplace -> updInertDicts $ \ ds -> addDict ds cls tys workItem
876 ; if stop_now then
877 return $ Stop ev_w (text "Dict equal" <+> parens (ppr inert_effect))
878 else
879 continueWith workItem } }
880 | cls `hasKey` ipClassKey
881 , isGiven ev_w
882 = interactGivenIP inerts workItem
883
884 | otherwise
885 = do { addFunDepWork inerts ev_w cls
886 ; continueWith workItem }
887
888 interactDict _ wi = pprPanic "interactDict" (ppr wi)
889
890 -- See Note [Solving from instances when interacting Dicts]
891 trySolveFromInstance :: DynFlags
892 -> CtEvidence -- Work item
893 -> CtEvidence -- Inert we want to try to replace
894 -> TcS (Maybe [(EvTerm, CtEvidence, Class, [TcPredType])])
895 -- Everything we need to bind a solution for the work item
896 -- and add the solved Dict to the cache in the main solver.
897 trySolveFromInstance dflags ev_w ctev_i
898 | isWanted ev_w
899 && isGiven ctev_i
900 -- We are about to solve a [W] constraint from a [G] constraint. We take
901 -- a moment to see if we can get a better solution using an instance.
902 -- Note that we only do this for the sake of performance. Exactly the same
903 -- programs should typecheck regardless of whether we take this step or
904 -- not. See Note [Solving from instances when interacting Dicts]
905 && not (xopt LangExt.IncoherentInstances dflags)
906 -- If IncoherentInstances is on then we cannot rely on coherence of proofs
907 -- in order to justify this optimization: The proof provided by the
908 -- [G] constraint's superclass may be different from the top-level proof.
909 && gopt Opt_SolveConstantDicts dflags
910 -- Enabled by the -fsolve-constant-dicts flag
911 = runMaybeT $ try_solve_from_instance emptyDictMap ev_w
912
913 | otherwise = return Nothing
914 where
915 -- This `CtLoc` is used only to check the well-staged condition of any
916 -- candidate DFun. Our subgoals all have the same stage as our root
917 -- [W] constraint so it is safe to use this while solving them.
918 loc_w = ctEvLoc ev_w
919
920 -- Use a local cache of solved dicts while emitting EvVars for new work
921 -- We bail out of the entire computation if we need to emit an EvVar for
922 -- a subgoal that isn't a ClassPred.
923 new_wanted_cached :: DictMap CtEvidence -> TcPredType -> MaybeT TcS MaybeNew
924 new_wanted_cached cache pty
925 | ClassPred cls tys <- classifyPredType pty
926 = lift $ case findDict cache cls tys of
927 Just ctev -> return $ Cached (ctEvTerm ctev)
928 Nothing -> Fresh <$> newWantedNC loc_w pty
929 | otherwise = mzero
930
931 -- MaybeT manages early failure if we find a subgoal that cannot be solved
932 -- from instances.
933 -- Why do we need a local cache here?
934 -- 1. We can't use the global cache because it contains givens that
935 -- we specifically don't want to use to solve.
936 -- 2. We need to be able to handle recursive super classes. The
937 -- cache ensures that we remember what we have already tried to
938 -- solve to avoid looping.
939 try_solve_from_instance
940 :: DictMap CtEvidence -> CtEvidence
941 -> MaybeT TcS [(EvTerm, CtEvidence, Class, [TcPredType])]
942 try_solve_from_instance cache ev
943 | ClassPred cls tys <- classifyPredType (ctEvPred ev) = do
944 -- It is important that we add our goal to the cache before we solve!
945 -- Otherwise we may end up in a loop while solving recursive dictionaries.
946 { let cache' = addDict cache cls tys ev
947 ; inst_res <- lift $ match_class_inst dflags cls tys loc_w
948 ; case inst_res of
949 GenInst { lir_new_theta = preds
950 , lir_mk_ev = mk_ev
951 , lir_safe_over = safeOverlap }
952 | safeOverlap -> do
953 -- emit work for subgoals but use our local cache so that we can
954 -- solve recursive dictionaries.
955 { evc_vs <- mapM (new_wanted_cached cache') preds
956 ; subgoalBinds <- mapM (try_solve_from_instance cache')
957 (freshGoals evc_vs)
958 ; return $ (mk_ev (map getEvTerm evc_vs), ev, cls, preds)
959 : concat subgoalBinds }
960
961 | otherwise -> mzero
962 _ -> mzero }
963 | otherwise = mzero
964
965 addFunDepWork :: InertCans -> CtEvidence -> Class -> TcS ()
966 -- Add derived constraints from type-class functional dependencies.
967 addFunDepWork inerts work_ev cls
968 | isImprovable work_ev
969 = mapBagM_ add_fds (findDictsByClass (inert_dicts inerts) cls)
970 -- No need to check flavour; fundeps work between
971 -- any pair of constraints, regardless of flavour
972 -- Importantly we don't throw workitem back in the
973 -- worklist because this can cause loops (see #5236)
974 | otherwise
975 = return ()
976 where
977 work_pred = ctEvPred work_ev
978 work_loc = ctEvLoc work_ev
979
980 add_fds inert_ct
981 | isImprovable inert_ev
982 = emitFunDepDeriveds $
983 improveFromAnother derived_loc inert_pred work_pred
984 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
985 -- NB: We do create FDs for given to report insoluble equations that arise
986 -- from pairs of Givens, and also because of floating when we approximate
987 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
988 | otherwise
989 = return ()
990 where
991 inert_ev = ctEvidence inert_ct
992 inert_pred = ctEvPred inert_ev
993 inert_loc = ctEvLoc inert_ev
994 derived_loc = work_loc { ctl_depth = ctl_depth work_loc `maxSubGoalDepth`
995 ctl_depth inert_loc
996 , ctl_origin = FunDepOrigin1 work_pred work_loc
997 inert_pred inert_loc }
998
999 {-
1000 **********************************************************************
1001 * *
1002 Implicit parameters
1003 * *
1004 **********************************************************************
1005 -}
1006
1007 interactGivenIP :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1008 -- Work item is Given (?x:ty)
1009 -- See Note [Shadowing of Implicit Parameters]
1010 interactGivenIP inerts workItem@(CDictCan { cc_ev = ev, cc_class = cls
1011 , cc_tyargs = tys@(ip_str:_) })
1012 = do { updInertCans $ \cans -> cans { inert_dicts = addDict filtered_dicts cls tys workItem }
1013 ; stopWith ev "Given IP" }
1014 where
1015 dicts = inert_dicts inerts
1016 ip_dicts = findDictsByClass dicts cls
1017 other_ip_dicts = filterBag (not . is_this_ip) ip_dicts
1018 filtered_dicts = addDictsByClass dicts cls other_ip_dicts
1019
1020 -- Pick out any Given constraints for the same implicit parameter
1021 is_this_ip (CDictCan { cc_ev = ev, cc_tyargs = ip_str':_ })
1022 = isGiven ev && ip_str `tcEqType` ip_str'
1023 is_this_ip _ = False
1024
1025 interactGivenIP _ wi = pprPanic "interactGivenIP" (ppr wi)
1026
1027
1028 {- Note [Shadowing of Implicit Parameters]
1029 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1030 Consider the following example:
1031
1032 f :: (?x :: Char) => Char
1033 f = let ?x = 'a' in ?x
1034
1035 The "let ?x = ..." generates an implication constraint of the form:
1036
1037 ?x :: Char => ?x :: Char
1038
1039 Furthermore, the signature for `f` also generates an implication
1040 constraint, so we end up with the following nested implication:
1041
1042 ?x :: Char => (?x :: Char => ?x :: Char)
1043
1044 Note that the wanted (?x :: Char) constraint may be solved in
1045 two incompatible ways: either by using the parameter from the
1046 signature, or by using the local definition. Our intention is
1047 that the local definition should "shadow" the parameter of the
1048 signature, and we implement this as follows: when we add a new
1049 *given* implicit parameter to the inert set, it replaces any existing
1050 givens for the same implicit parameter.
1051
1052 Similarly, consider
1053 f :: (?x::a) => Bool -> a
1054
1055 g v = let ?x::Int = 3
1056 in (f v, let ?x::Bool = True in f v)
1057
1058 This should probably be well typed, with
1059 g :: Bool -> (Int, Bool)
1060
1061 So the inner binding for ?x::Bool *overrides* the outer one.
1062
1063 All this works for the normal cases but it has an odd side effect in
1064 some pathological programs like this:
1065 -- This is accepted, the second parameter shadows
1066 f1 :: (?x :: Int, ?x :: Char) => Char
1067 f1 = ?x
1068
1069 -- This is rejected, the second parameter shadows
1070 f2 :: (?x :: Int, ?x :: Char) => Int
1071 f2 = ?x
1072
1073 Both of these are actually wrong: when we try to use either one,
1074 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
1075 which would lead to an error.
1076
1077 I can think of two ways to fix this:
1078
1079 1. Simply disallow multiple constraints for the same implicit
1080 parameter---this is never useful, and it can be detected completely
1081 syntactically.
1082
1083 2. Move the shadowing machinery to the location where we nest
1084 implications, and add some code here that will produce an
1085 error if we get multiple givens for the same implicit parameter.
1086
1087
1088 **********************************************************************
1089 * *
1090 interactFunEq
1091 * *
1092 **********************************************************************
1093 -}
1094
1095 interactFunEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1096 -- Try interacting the work item with the inert set
1097 interactFunEq inerts work_item@(CFunEqCan { cc_ev = ev, cc_fun = tc
1098 , cc_tyargs = args, cc_fsk = fsk })
1099 | Just inert_ct@(CFunEqCan { cc_ev = ev_i
1100 , cc_fsk = fsk_i })
1101 <- findFunEq (inert_funeqs inerts) tc args
1102 , pr@(swap_flag, upgrade_flag) <- ev_i `funEqCanDischarge` ev
1103 = do { traceTcS "reactFunEq (rewrite inert item):" $
1104 vcat [ text "work_item =" <+> ppr work_item
1105 , text "inertItem=" <+> ppr ev_i
1106 , text "(swap_flag, upgrade)" <+> ppr pr ]
1107 ; if isSwapped swap_flag
1108 then do { -- Rewrite inert using work-item
1109 let work_item' | upgrade_flag = upgradeWanted work_item
1110 | otherwise = work_item
1111 ; updInertFunEqs $ \ feqs -> insertFunEq feqs tc args work_item'
1112 -- Do the updInertFunEqs before the reactFunEq, so that
1113 -- we don't kick out the inertItem as well as consuming it!
1114 ; reactFunEq ev fsk ev_i fsk_i
1115 ; stopWith ev "Work item rewrites inert" }
1116 else do { -- Rewrite work-item using inert
1117 ; when upgrade_flag $
1118 updInertFunEqs $ \ feqs -> insertFunEq feqs tc args
1119 (upgradeWanted inert_ct)
1120 ; reactFunEq ev_i fsk_i ev fsk
1121 ; stopWith ev "Inert rewrites work item" } }
1122
1123 | otherwise -- Try improvement
1124 = do { improveLocalFunEqs ev inerts tc args fsk
1125 ; continueWith work_item }
1126
1127 interactFunEq _ work_item = pprPanic "interactFunEq" (ppr work_item)
1128
1129 upgradeWanted :: Ct -> Ct
1130 -- We are combining a [W] F tys ~ fmv1 and [D] F tys ~ fmv2
1131 -- so upgrade the [W] to [WD] before putting it in the inert set
1132 upgradeWanted ct = ct { cc_ev = upgrade_ev (cc_ev ct) }
1133 where
1134 upgrade_ev ev = ASSERT2( isWanted ev, ppr ct )
1135 ev { ctev_nosh = WDeriv }
1136
1137 improveLocalFunEqs :: CtEvidence -> InertCans -> TyCon -> [TcType] -> TcTyVar
1138 -> TcS ()
1139 -- Generate derived improvement equalities, by comparing
1140 -- the current work item with inert CFunEqs
1141 -- E.g. x + y ~ z, x + y' ~ z => [D] y ~ y'
1142 --
1143 -- See Note [FunDep and implicit parameter reactions]
1144 improveLocalFunEqs work_ev inerts fam_tc args fsk
1145 | isGiven work_ev -- See Note [No FunEq improvement for Givens]
1146 || not (isImprovable work_ev)
1147 = return ()
1148
1149 | not (null improvement_eqns)
1150 = do { traceTcS "interactFunEq improvements: " $
1151 vcat [ text "Eqns:" <+> ppr improvement_eqns
1152 , text "Candidates:" <+> ppr funeqs_for_tc
1153 , text "Inert eqs:" <+> ppr ieqs ]
1154 ; emitFunDepDeriveds improvement_eqns }
1155
1156 | otherwise
1157 = return ()
1158
1159 where
1160 ieqs = inert_eqs inerts
1161 funeqs = inert_funeqs inerts
1162 funeqs_for_tc = findFunEqsByTyCon funeqs fam_tc
1163 rhs = lookupFlattenTyVar ieqs fsk
1164 work_loc = ctEvLoc work_ev
1165 work_pred = ctEvPred work_ev
1166 fam_inj_info = familyTyConInjectivityInfo fam_tc
1167
1168 --------------------
1169 improvement_eqns :: [FunDepEqn CtLoc]
1170 improvement_eqns
1171 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1172 = -- Try built-in families, notably for arithmethic
1173 concatMap (do_one_built_in ops) funeqs_for_tc
1174
1175 | Injective injective_args <- fam_inj_info
1176 = -- Try improvement from type families with injectivity annotations
1177 concatMap (do_one_injective injective_args) funeqs_for_tc
1178
1179 | otherwise
1180 = []
1181
1182 --------------------
1183 do_one_built_in ops (CFunEqCan { cc_tyargs = iargs, cc_fsk = ifsk, cc_ev = inert_ev })
1184 = mk_fd_eqns inert_ev (sfInteractInert ops args rhs iargs
1185 (lookupFlattenTyVar ieqs ifsk))
1186
1187 do_one_built_in _ _ = pprPanic "interactFunEq 1" (ppr fam_tc)
1188
1189 --------------------
1190 -- See Note [Type inference for type families with injectivity]
1191 do_one_injective inj_args (CFunEqCan { cc_tyargs = inert_args
1192 , cc_fsk = ifsk, cc_ev = inert_ev })
1193 | isImprovable inert_ev
1194 , rhs `tcEqType` lookupFlattenTyVar ieqs ifsk
1195 = mk_fd_eqns inert_ev $
1196 [ Pair arg iarg
1197 | (arg, iarg, True) <- zip3 args inert_args inj_args ]
1198 | otherwise
1199 = []
1200
1201 do_one_injective _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)
1202
1203 --------------------
1204 mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn CtLoc]
1205 mk_fd_eqns inert_ev eqns
1206 | null eqns = []
1207 | otherwise = [ FDEqn { fd_qtvs = [], fd_eqs = eqns
1208 , fd_pred1 = work_pred
1209 , fd_pred2 = ctEvPred inert_ev
1210 , fd_loc = loc } ]
1211 where
1212 inert_loc = ctEvLoc inert_ev
1213 loc = inert_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`
1214 ctl_depth work_loc }
1215
1216 -------------
1217 reactFunEq :: CtEvidence -> TcTyVar -- From this :: F args1 ~ fsk1
1218 -> CtEvidence -> TcTyVar -- Solve this :: F args2 ~ fsk2
1219 -> TcS ()
1220 reactFunEq from_this fsk1 solve_this fsk2
1221 | CtGiven { ctev_evar = evar, ctev_loc = loc } <- solve_this
1222 = do { let fsk_eq_co = mkTcSymCo (mkTcCoVarCo evar) `mkTcTransCo`
1223 ctEvCoercion from_this
1224 -- :: fsk2 ~ fsk1
1225 fsk_eq_pred = mkTcEqPredLikeEv solve_this
1226 (mkTyVarTy fsk2) (mkTyVarTy fsk1)
1227
1228 ; new_ev <- newGivenEvVar loc (fsk_eq_pred, EvCoercion fsk_eq_co)
1229 ; emitWorkNC [new_ev] }
1230
1231 | CtDerived { ctev_loc = loc } <- solve_this
1232 = do { traceTcS "reactFunEq (Derived)" (ppr from_this $$ ppr fsk1 $$
1233 ppr solve_this $$ ppr fsk2)
1234 ; emitNewDerivedEq loc Nominal (mkTyVarTy fsk1) (mkTyVarTy fsk2) }
1235 -- FunEqs are always at Nominal role
1236
1237 | otherwise -- Wanted
1238 = do { traceTcS "reactFunEq" (ppr from_this $$ ppr fsk1 $$
1239 ppr solve_this $$ ppr fsk2)
1240 ; dischargeFmv solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
1241 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
1242 ppr solve_this $$ ppr fsk2) }
1243
1244 {- Note [Type inference for type families with injectivity]
1245 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1246 Suppose we have a type family with an injectivity annotation:
1247 type family F a b = r | r -> b
1248
1249 Then if we have two CFunEqCan constraints for F with the same RHS
1250 F s1 t1 ~ rhs
1251 F s2 t2 ~ rhs
1252 then we can use the injectivity to get a new Derived constraint on
1253 the injective argument
1254 [D] t1 ~ t2
1255
1256 That in turn can help GHC solve constraints that would otherwise require
1257 guessing. For example, consider the ambiguity check for
1258 f :: F Int b -> Int
1259 We get the constraint
1260 [W] F Int b ~ F Int beta
1261 where beta is a unification variable. Injectivity lets us pick beta ~ b.
1262
1263 Injectivity information is also used at the call sites. For example:
1264 g = f True
1265 gives rise to
1266 [W] F Int b ~ Bool
1267 from which we can derive b. This requires looking at the defining equations of
1268 a type family, ie. finding equation with a matching RHS (Bool in this example)
1269 and infering values of type variables (b in this example) from the LHS patterns
1270 of the matching equation. For closed type families we have to perform
1271 additional apartness check for the selected equation to check that the selected
1272 is guaranteed to fire for given LHS arguments.
1273
1274 These new constraints are simply *Derived* constraints; they have no evidence.
1275 We could go further and offer evidence from decomposing injective type-function
1276 applications, but that would require new evidence forms, and an extension to
1277 FC, so we don't do that right now (Dec 14).
1278
1279 See also Note [Injective type families] in TyCon
1280
1281
1282 Note [Cache-caused loops]
1283 ~~~~~~~~~~~~~~~~~~~~~~~~~
1284 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1285 solved cache (which is the default behaviour or xCtEvidence), because the interaction
1286 may not be contributing towards a solution. Here is an example:
1287
1288 Initial inert set:
1289 [W] g1 : F a ~ beta1
1290 Work item:
1291 [W] g2 : F a ~ beta2
1292 The work item will react with the inert yielding the _same_ inert set plus:
1293 i) Will set g2 := g1 `cast` g3
1294 ii) Will add to our solved cache that [S] g2 : F a ~ beta2
1295 iii) Will emit [W] g3 : beta1 ~ beta2
1296 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
1297 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
1298 will set
1299 g1 := g ; sym g3
1300 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
1301 remember that we have this in our solved cache, and it is ... g2! In short we
1302 created the evidence loop:
1303
1304 g2 := g1 ; g3
1305 g3 := refl
1306 g1 := g2 ; sym g3
1307
1308 To avoid this situation we do not cache as solved any workitems (or inert)
1309 which did not really made a 'step' towards proving some goal. Solved's are
1310 just an optimization so we don't lose anything in terms of completeness of
1311 solving.
1312
1313
1314 Note [Efficient Orientation]
1315 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1316 Suppose we are interacting two FunEqCans with the same LHS:
1317 (inert) ci :: (F ty ~ xi_i)
1318 (work) cw :: (F ty ~ xi_w)
1319 We prefer to keep the inert (else we pass the work item on down
1320 the pipeline, which is a bit silly). If we keep the inert, we
1321 will (a) discharge 'cw'
1322 (b) produce a new equality work-item (xi_w ~ xi_i)
1323 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
1324 new_work :: xi_w ~ xi_i
1325 cw := ci ; sym new_work
1326 Why? Consider the simplest case when xi1 is a type variable. If
1327 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
1328 If we generate xi2~xi1, there is less chance of that happening.
1329 Of course it can and should still happen if xi1=a, xi1=Int, say.
1330 But we want to avoid it happening needlessly.
1331
1332 Similarly, if we *can't* keep the inert item (because inert is Wanted,
1333 and work is Given, say), we prefer to orient the new equality (xi_i ~
1334 xi_w).
1335
1336 Note [Carefully solve the right CFunEqCan]
1337 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1338 ---- OLD COMMENT, NOW NOT NEEDED
1339 ---- because we now allow multiple
1340 ---- wanted FunEqs with the same head
1341 Consider the constraints
1342 c1 :: F Int ~ a -- Arising from an application line 5
1343 c2 :: F Int ~ Bool -- Arising from an application line 10
1344 Suppose that 'a' is a unification variable, arising only from
1345 flattening. So there is no error on line 5; it's just a flattening
1346 variable. But there is (or might be) an error on line 10.
1347
1348 Two ways to combine them, leaving either (Plan A)
1349 c1 :: F Int ~ a -- Arising from an application line 5
1350 c3 :: a ~ Bool -- Arising from an application line 10
1351 or (Plan B)
1352 c2 :: F Int ~ Bool -- Arising from an application line 10
1353 c4 :: a ~ Bool -- Arising from an application line 5
1354
1355 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
1356 on the *totally innocent* line 5. An example is test SimpleFail16
1357 where the expected/actual message comes out backwards if we use
1358 the wrong plan.
1359
1360 The second is the right thing to do. Hence the isMetaTyVarTy
1361 test when solving pairwise CFunEqCan.
1362
1363
1364 **********************************************************************
1365 * *
1366 interactTyVarEq
1367 * *
1368 **********************************************************************
1369 -}
1370
1371 inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtEvidence
1372 -> Maybe ( CtEvidence -- The evidence for the inert
1373 , SwapFlag -- Whether we need mkSymCo
1374 , Bool) -- True <=> keep a [D] version
1375 -- of the [WD] constraint
1376 inertsCanDischarge inerts tv rhs ev
1377 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1378 <- findTyEqs inerts tv
1379 , ev_i `eqCanDischarge` ev
1380 , rhs_i `tcEqType` rhs ]
1381 = -- Inert: a ~ ty
1382 -- Work item: a ~ ty
1383 Just (ev_i, NotSwapped, keep_deriv ev_i)
1384
1385 | Just tv_rhs <- getTyVar_maybe rhs
1386 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i }
1387 <- findTyEqs inerts tv_rhs
1388 , ev_i `eqCanDischarge` ev
1389 , rhs_i `tcEqType` mkTyVarTy tv ]
1390 = -- Inert: a ~ b
1391 -- Work item: b ~ a
1392 Just (ev_i, IsSwapped, keep_deriv ev_i)
1393
1394 | otherwise
1395 = Nothing
1396
1397 where
1398 keep_deriv ev_i
1399 | Wanted WOnly <- ctEvFlavour ev_i -- inert is [W]
1400 , Wanted WDeriv <- ctEvFlavour ev -- work item is [WD]
1401 = True -- Keep a derived verison of the work item
1402 | otherwise
1403 = False -- Work item is fully discharged
1404
1405 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1406 -- CTyEqCans are always consumed, so always returns Stop
1407 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
1408 , cc_rhs = rhs
1409 , cc_ev = ev
1410 , cc_eq_rel = eq_rel })
1411 | Just (ev_i, swapped, keep_deriv)
1412 <- inertsCanDischarge inerts tv rhs ev
1413 = do { setEvBindIfWanted ev $
1414 EvCoercion (maybeSym swapped $
1415 tcDowngradeRole (eqRelRole eq_rel)
1416 (ctEvRole ev_i)
1417 (ctEvCoercion ev_i))
1418
1419 ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev
1420 , ctev_loc = ctEvLoc ev }
1421 ; when keep_deriv $
1422 emitWork [workItem { cc_ev = deriv_ev }]
1423 -- As a Derived it might not be fully rewritten,
1424 -- so we emit it as new work
1425
1426 ; stopWith ev "Solved from inert" }
1427
1428 | ReprEq <- eq_rel -- We never solve representational
1429 = unsolved_inert -- equalities by unification
1430
1431 | isGiven ev -- See Note [Touchables and givens]
1432 = unsolved_inert
1433
1434 | otherwise
1435 = do { tclvl <- getTcLevel
1436 ; if canSolveByUnification tclvl tv rhs
1437 then do { solveByUnification ev tv rhs
1438 ; n_kicked <- kickOutAfterUnification tv
1439 ; return (Stop ev (text "Solved by unification" <+> ppr_kicked n_kicked)) }
1440
1441 else unsolved_inert }
1442
1443 where
1444 unsolved_inert
1445 = do { traceTcS "Can't solve tyvar equality"
1446 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1447 , ppWhen (isMetaTyVar tv) $
1448 nest 4 (text "TcLevel of" <+> ppr tv
1449 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
1450 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
1451 ; addInertEq workItem
1452 ; stopWith ev "Kept as inert" }
1453
1454 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1455
1456 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1457 -- Solve with the identity coercion
1458 -- Precondition: kind(xi) equals kind(tv)
1459 -- Precondition: CtEvidence is Wanted or Derived
1460 -- Precondition: CtEvidence is nominal
1461 -- Returns: workItem where
1462 -- workItem = the new Given constraint
1463 --
1464 -- NB: No need for an occurs check here, because solveByUnification always
1465 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1466 -- say that in (a ~ xi), the type variable a does not appear in xi.
1467 -- See TcRnTypes.Ct invariants.
1468 --
1469 -- Post: tv is unified (by side effect) with xi;
1470 -- we often write tv := xi
1471 solveByUnification wd tv xi
1472 = do { let tv_ty = mkTyVarTy tv
1473 ; traceTcS "Sneaky unification:" $
1474 vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
1475 text "Coercion:" <+> pprEq tv_ty xi,
1476 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1477 text "Right Kind is:" <+> ppr (typeKind xi) ]
1478
1479 ; unifyTyVar tv xi
1480 ; setEvBindIfWanted wd (EvCoercion (mkTcNomReflCo xi)) }
1481
1482 ppr_kicked :: Int -> SDoc
1483 ppr_kicked 0 = empty
1484 ppr_kicked n = parens (int n <+> text "kicked out")
1485
1486 {- Note [Avoid double unifications]
1487 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1488 The spontaneous solver has to return a given which mentions the unified unification
1489 variable *on the left* of the equality. Here is what happens if not:
1490 Original wanted: (a ~ alpha), (alpha ~ Int)
1491 We spontaneously solve the first wanted, without changing the order!
1492 given : a ~ alpha [having unified alpha := a]
1493 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1494 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1495
1496 We avoid this problem by orienting the resulting given so that the unification
1497 variable is on the left. [Note that alternatively we could attempt to
1498 enforce this at canonicalization]
1499
1500 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1501 double unifications is the main reason we disallow touchable
1502 unification variables as RHS of type family equations: F xis ~ alpha.
1503
1504
1505 ************************************************************************
1506 * *
1507 * Functional dependencies, instantiation of equations
1508 * *
1509 ************************************************************************
1510
1511 When we spot an equality arising from a functional dependency,
1512 we now use that equality (a "wanted") to rewrite the work-item
1513 constraint right away. This avoids two dangers
1514
1515 Danger 1: If we send the original constraint on down the pipeline
1516 it may react with an instance declaration, and in delicate
1517 situations (when a Given overlaps with an instance) that
1518 may produce new insoluble goals: see Trac #4952
1519
1520 Danger 2: If we don't rewrite the constraint, it may re-react
1521 with the same thing later, and produce the same equality
1522 again --> termination worries.
1523
1524 To achieve this required some refactoring of FunDeps.hs (nicer
1525 now!).
1526
1527 Note [FunDep and implicit parameter reactions]
1528 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1529 Currently, our story of interacting two dictionaries (or a dictionary
1530 and top-level instances) for functional dependencies, and implicit
1531 parameters, is that we simply produce new Derived equalities. So for example
1532
1533 class D a b | a -> b where ...
1534 Inert:
1535 d1 :g D Int Bool
1536 WorkItem:
1537 d2 :w D Int alpha
1538
1539 We generate the extra work item
1540 cv :d alpha ~ Bool
1541 where 'cv' is currently unused. However, this new item can perhaps be
1542 spontaneously solved to become given and react with d2,
1543 discharging it in favour of a new constraint d2' thus:
1544 d2' :w D Int Bool
1545 d2 := d2' |> D Int cv
1546 Now d2' can be discharged from d1
1547
1548 We could be more aggressive and try to *immediately* solve the dictionary
1549 using those extra equalities, but that requires those equalities to carry
1550 evidence and derived do not carry evidence.
1551
1552 If that were the case with the same inert set and work item we might dischard
1553 d2 directly:
1554
1555 cv :w alpha ~ Bool
1556 d2 := d1 |> D Int cv
1557
1558 But in general it's a bit painful to figure out the necessary coercion,
1559 so we just take the first approach. Here is a better example. Consider:
1560 class C a b c | a -> b
1561 And:
1562 [Given] d1 : C T Int Char
1563 [Wanted] d2 : C T beta Int
1564 In this case, it's *not even possible* to solve the wanted immediately.
1565 So we should simply output the functional dependency and add this guy
1566 [but NOT its superclasses] back in the worklist. Even worse:
1567 [Given] d1 : C T Int beta
1568 [Wanted] d2: C T beta Int
1569 Then it is solvable, but its very hard to detect this on the spot.
1570
1571 It's exactly the same with implicit parameters, except that the
1572 "aggressive" approach would be much easier to implement.
1573
1574 Note [Weird fundeps]
1575 ~~~~~~~~~~~~~~~~~~~~
1576 Consider class Het a b | a -> b where
1577 het :: m (f c) -> a -> m b
1578
1579 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1580 instance GHet (K a) (K [a])
1581 instance Het a b => GHet (K a) (K b)
1582
1583 The two instances don't actually conflict on their fundeps,
1584 although it's pretty strange. So they are both accepted. Now
1585 try [W] GHet (K Int) (K Bool)
1586 This triggers fundeps from both instance decls;
1587 [D] K Bool ~ K [a]
1588 [D] K Bool ~ K beta
1589 And there's a risk of complaining about Bool ~ [a]. But in fact
1590 the Wanted matches the second instance, so we never get as far
1591 as the fundeps.
1592
1593 Trac #7875 is a case in point.
1594 -}
1595
1596 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1597 -- See Note [FunDep and implicit parameter reactions]
1598 emitFunDepDeriveds fd_eqns
1599 = mapM_ do_one_FDEqn fd_eqns
1600 where
1601 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1602 | null tvs -- Common shortcut
1603 = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs)
1604 ; mapM_ (unifyDerived loc Nominal) eqs }
1605 | otherwise
1606 = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr eqs)
1607 ; subst <- instFlexi tvs -- Takes account of kind substitution
1608 ; mapM_ (do_one_eq loc subst) eqs }
1609
1610 do_one_eq loc subst (Pair ty1 ty2)
1611 = unifyDerived loc Nominal $
1612 Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
1613
1614 {-
1615 **********************************************************************
1616 * *
1617 The top-reaction Stage
1618 * *
1619 **********************************************************************
1620 -}
1621
1622 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1623 topReactionsStage wi
1624 = do { tir <- doTopReact wi
1625 ; case tir of
1626 ContinueWith wi -> continueWith wi
1627 Stop ev s -> return (Stop ev (text "Top react:" <+> s)) }
1628
1629 doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
1630 -- The work item does not react with the inert set, so try interaction with top-level
1631 -- instances. Note:
1632 --
1633 -- (a) The place to add superclasses in not here in doTopReact stage.
1634 -- Instead superclasses are added in the worklist as part of the
1635 -- canonicalization process. See Note [Adding superclasses].
1636
1637 doTopReact work_item
1638 = do { traceTcS "doTopReact" (ppr work_item)
1639 ; case work_item of
1640 CDictCan {} -> do { inerts <- getTcSInerts
1641 ; doTopReactDict inerts work_item }
1642 CFunEqCan {} -> doTopReactFunEq work_item
1643 _ -> -- Any other work item does not react with any top-level equations
1644 continueWith work_item }
1645
1646
1647 --------------------
1648 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1649 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1650 , cc_tyargs = args, cc_fsk = fsk })
1651
1652 | fsk `elemVarSet` tyCoVarsOfTypes args
1653 = no_reduction -- See Note [FunEq occurs-check principle]
1654
1655 | otherwise -- Note [Reduction for Derived CFunEqCans]
1656 = do { match_res <- matchFam fam_tc args
1657 -- Look up in top-level instances, or built-in axiom
1658 -- See Note [MATCHING-SYNONYMS]
1659 ; case match_res of
1660 Nothing -> no_reduction
1661 Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
1662 where
1663 no_reduction
1664 = do { improveTopFunEqs old_ev fam_tc args fsk
1665 ; continueWith work_item }
1666
1667 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1668
1669 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
1670 -> TcS (StopOrContinue Ct)
1671 -- We have found an applicable top-level axiom: use it to reduce
1672 -- Precondition: fsk is not free in rhs_ty
1673 -- old_ev is not Derived
1674 reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
1675 | isDerived old_ev
1676 = do { emitNewDerivedEq loc Nominal (mkTyVarTy fsk) rhs_ty
1677 ; stopWith old_ev "Fun/Top (derived)" }
1678
1679 | Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1680 , isTypeFamilyTyCon tc
1681 , tc_args `lengthIs` tyConArity tc -- Short-cut
1682 = -- RHS is another type-family application
1683 -- Try shortcut; see Note [Top-level reductions for type functions]
1684 shortCutReduction old_ev fsk ax_co tc tc_args
1685
1686 | isGiven old_ev -- Not shortcut
1687 = do { let final_co = mkTcSymCo (ctEvCoercion old_ev) `mkTcTransCo` ax_co
1688 -- final_co :: fsk ~ rhs_ty
1689 ; new_ev <- newGivenEvVar deeper_loc (mkPrimEqPred (mkTyVarTy fsk) rhs_ty,
1690 EvCoercion final_co)
1691 ; emitWorkNC [new_ev] -- Non-cannonical; that will mean we flatten rhs_ty
1692 ; stopWith old_ev "Fun/Top (given)" }
1693
1694 | otherwise -- So old_ev is Wanted (cannot be Derived)
1695 = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
1696 , ppr old_ev $$ ppr rhs_ty )
1697 -- Guaranteed by Note [FunEq occurs-check principle]
1698 do { dischargeFmv old_ev fsk ax_co rhs_ty
1699 ; traceTcS "doTopReactFunEq" $
1700 vcat [ text "old_ev:" <+> ppr old_ev
1701 , nest 2 (text ":=") <+> ppr ax_co ]
1702 ; stopWith old_ev "Fun/Top (wanted)" }
1703
1704 where
1705 loc = ctEvLoc old_ev
1706 deeper_loc = bumpCtLocDepth loc
1707
1708 improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1709 -- See Note [FunDep and implicit parameter reactions]
1710 improveTopFunEqs ev fam_tc args fsk
1711 | isGiven ev -- See Note [No FunEq improvement for Givens]
1712 || not (isImprovable ev)
1713 = return ()
1714
1715 | otherwise
1716 = do { ieqs <- getInertEqs
1717 ; fam_envs <- getFamInstEnvs
1718 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1719 (lookupFlattenTyVar ieqs fsk)
1720 ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
1721 , ppr eqns ])
1722 ; mapM_ (unifyDerived loc Nominal) eqns }
1723 where
1724 loc = ctEvLoc ev
1725
1726 improve_top_fun_eqs :: FamInstEnvs
1727 -> TyCon -> [TcType] -> TcType
1728 -> TcS [TypeEqn]
1729 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1730 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1731 = return (sfInteractTop ops args rhs_ty)
1732
1733 -- see Note [Type inference for type families with injectivity]
1734 | isOpenTypeFamilyTyCon fam_tc
1735 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1736 = -- it is possible to have several compatible equations in an open type
1737 -- family but we only want to derive equalities from one such equation.
1738 concatMapM (injImproveEqns injective_args) (take 1 $
1739 buildImprovementData (lookupFamInstEnvByTyCon fam_envs fam_tc)
1740 fi_tvs fi_tys fi_rhs (const Nothing))
1741
1742 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1743 , Injective injective_args <- familyTyConInjectivityInfo fam_tc
1744 = concatMapM (injImproveEqns injective_args) $
1745 buildImprovementData (fromBranches (co_ax_branches ax))
1746 cab_tvs cab_lhs cab_rhs Just
1747
1748 | otherwise
1749 = return []
1750
1751 where
1752 buildImprovementData
1753 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1754 -> (a -> [TyVar]) -- get bound tyvars of an axiom
1755 -> (a -> [Type]) -- get LHS of an axiom
1756 -> (a -> Type) -- get RHS of an axiom
1757 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1758 -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
1759 -- Result:
1760 -- ( [arguments of a matching axiom]
1761 -- , RHS-unifying substitution
1762 -- , axiom variables without substitution
1763 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1764 buildImprovementData axioms axiomTVs axiomLHS axiomRHS wrap =
1765 [ (ax_args, subst, unsubstTvs, wrap axiom)
1766 | axiom <- axioms
1767 , let ax_args = axiomLHS axiom
1768 ax_rhs = axiomRHS axiom
1769 ax_tvs = axiomTVs axiom
1770 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1771 , let notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1772 unsubstTvs = filter (notInSubst <&&> isTyVar) ax_tvs ]
1773 -- The order of unsubstTvs is important; it must be
1774 -- in telescope order e.g. (k:*) (a:k)
1775
1776 injImproveEqns :: [Bool]
1777 -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
1778 -> TcS [TypeEqn]
1779 injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
1780 = do { subst <- instFlexiX subst unsubstTvs
1781 -- If the current substitution bind [k -> *], and
1782 -- one of the un-substituted tyvars is (a::k), we'd better
1783 -- be sure to apply the current substitution to a's kind.
1784 -- Hence instFlexiX. Trac #13135 was an example.
1785
1786 ; return [ Pair (substTyUnchecked subst ax_arg) arg
1787 -- NB: the ax_arg part is on the left
1788 -- see Note [Improvement orientation]
1789 | case cabr of
1790 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
1791 _ -> True
1792 , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
1793
1794
1795 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1796 -> TyCon -> [TcType] -> TcS (StopOrContinue Ct)
1797 -- See Note [Top-level reductions for type functions]
1798 shortCutReduction old_ev fsk ax_co fam_tc tc_args
1799 = ASSERT( ctEvEqRel old_ev == NomEq)
1800 do { (xis, cos) <- flattenManyNom old_ev tc_args
1801 -- ax_co :: F args ~ G tc_args
1802 -- cos :: xis ~ tc_args
1803 -- old_ev :: F args ~ fsk
1804 -- G cos ; sym ax_co ; old_ev :: G xis ~ fsk
1805
1806 ; new_ev <- case ctEvFlavour old_ev of
1807 Given -> newGivenEvVar deeper_loc
1808 ( mkPrimEqPred (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1809 , EvCoercion (mkTcTyConAppCo Nominal fam_tc cos
1810 `mkTcTransCo` mkTcSymCo ax_co
1811 `mkTcTransCo` ctEvCoercion old_ev) )
1812
1813 Wanted {} ->
1814 do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
1815 (mkTyConApp fam_tc xis) (mkTyVarTy fsk)
1816 ; setWantedEq (ctev_dest old_ev) $
1817 ax_co `mkTcTransCo` mkTcSymCo (mkTcTyConAppCo Nominal
1818 fam_tc cos)
1819 `mkTcTransCo` new_co
1820 ; return new_ev }
1821
1822 Derived -> pprPanic "shortCutReduction" (ppr old_ev)
1823
1824 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
1825 , cc_tyargs = xis, cc_fsk = fsk }
1826 ; updWorkListTcS (extendWorkListFunEq new_ct)
1827 ; stopWith old_ev "Fun/Top (shortcut)" }
1828 where
1829 deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
1830
1831 dischargeFmv :: CtEvidence -> TcTyVar -> TcCoercion -> TcType -> TcS ()
1832 -- (dischargeFmv x fmv co ty)
1833 -- [W] ev :: F tys ~ fmv
1834 -- co :: F tys ~ xi
1835 -- Precondition: fmv is not filled, and fmv `notElem` xi
1836 -- ev is Wanted
1837 --
1838 -- Then set fmv := xi,
1839 -- set ev := co
1840 -- kick out any inert things that are now rewritable
1841 --
1842 -- Does not evaluate 'co' if 'ev' is Derived
1843 dischargeFmv ev@(CtWanted { ctev_dest = dest }) fmv co xi
1844 = ASSERT2( not (fmv `elemVarSet` tyCoVarsOfType xi), ppr ev $$ ppr fmv $$ ppr xi )
1845 do { setWantedEvTerm dest (EvCoercion co)
1846 ; unflattenFmv fmv xi
1847 ; n_kicked <- kickOutAfterUnification fmv
1848 ; traceTcS "dischargeFmv" (ppr fmv <+> equals <+> ppr xi $$ ppr_kicked n_kicked) }
1849 dischargeFmv ev _ _ _ = pprPanic "dischargeFmv" (ppr ev)
1850
1851 {- Note [Top-level reductions for type functions]
1852 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1853 c.f. Note [The flattening story] in TcFlatten
1854
1855 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
1856 Here is what we do, in four cases:
1857
1858 * Wanteds: general firing rule
1859 (work item) [W] x : F tys ~ fmv
1860 instantiate axiom: ax_co : F tys ~ rhs
1861
1862 Then:
1863 Discharge fmv := rhs
1864 Discharge x := ax_co ; sym x2
1865 This is *the* way that fmv's get unified; even though they are
1866 "untouchable".
1867
1868 NB: Given Note [FunEq occurs-check principle], fmv does not appear
1869 in tys, and hence does not appear in the instantiated RHS. So
1870 the unification can't make an infinite type.
1871
1872 * Wanteds: short cut firing rule
1873 Applies when the RHS of the axiom is another type-function application
1874 (work item) [W] x : F tys ~ fmv
1875 instantiate axiom: ax_co : F tys ~ G rhs_tys
1876
1877 It would be a waste to create yet another fmv for (G rhs_tys).
1878 Instead (shortCutReduction):
1879 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
1880 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
1881 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
1882 - Discharge x := ax_co ; G cos ; x2
1883
1884 * Givens: general firing rule
1885 (work item) [G] g : F tys ~ fsk
1886 instantiate axiom: ax_co : F tys ~ rhs
1887
1888 Now add non-canonical given (since rhs is not flat)
1889 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
1890
1891 * Givens: short cut firing rule
1892 Applies when the RHS of the axiom is another type-function application
1893 (work item) [G] g : F tys ~ fsk
1894 instantiate axiom: ax_co : F tys ~ G rhs_tys
1895
1896 It would be a waste to create yet another fsk for (G rhs_tys).
1897 Instead (shortCutReduction):
1898 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
1899 - Add new Canonical given
1900 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
1901
1902 Note [FunEq occurs-check principle]
1903 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1904 I have spent a lot of time finding a good way to deal with
1905 CFunEqCan constraints like
1906 F (fuv, a) ~ fuv
1907 where flatten-skolem occurs on the LHS. Now in principle we
1908 might may progress by doing a reduction, but in practice its
1909 hard to find examples where it is useful, and easy to find examples
1910 where we fall into an infinite reduction loop. A rule that works
1911 very well is this:
1912
1913 *** FunEq occurs-check principle ***
1914
1915 Do not reduce a CFunEqCan
1916 F tys ~ fsk
1917 if fsk appears free in tys
1918 Instead we treat it as stuck.
1919
1920 Examples:
1921
1922 * Trac #5837 has [G] a ~ TF (a,Int), with an instance
1923 type instance TF (a,b) = (TF a, TF b)
1924 This readily loops when solving givens. But with the FunEq occurs
1925 check principle, it rapidly gets stuck which is fine.
1926
1927 * Trac #12444 is a good example, explained in comment:2. We have
1928 type instance F (Succ x) = Succ (F x)
1929 [W] alpha ~ Succ (F alpha)
1930 If we allow the reduction to happen, we get an infinite loop
1931
1932 Note [Cached solved FunEqs]
1933 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
1934 When trying to solve, say (FunExpensive big-type ~ ty), it's important
1935 to see if we have reduced (FunExpensive big-type) before, lest we
1936 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
1937 we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
1938 and we *still* want to save the re-computation.
1939
1940 Note [MATCHING-SYNONYMS]
1941 ~~~~~~~~~~~~~~~~~~~~~~~~
1942 When trying to match a dictionary (D tau) to a top-level instance, or a
1943 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1944 we do *not* need to expand type synonyms because the matcher will do that for us.
1945
1946 Note [Improvement orientation]
1947 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1948 A very delicate point is the orientation of derived equalities
1949 arising from injectivity improvement (Trac #12522). Suppse we have
1950 type family F x = t | t -> x
1951 type instance F (a, Int) = (Int, G a)
1952 where G is injective; and wanted constraints
1953
1954 [W] TF (alpha, beta) ~ fuv
1955 [W] fuv ~ (Int, <some type>)
1956
1957 The injectivity will give rise to derived constraints
1958
1959 [D] gamma1 ~ alpha
1960 [D] Int ~ beta
1961
1962 The fresh unification variable gamma1 comes from the fact that we
1963 can only do "partial improvement" here; see Section 5.2 of
1964 "Injective type families for Haskell" (HS'15).
1965
1966 Now, it's very important to orient the equations this way round,
1967 so that the fresh unification variable will be eliminated in
1968 favour of alpha. If we instead had
1969 [D] alpha ~ gamma1
1970 then we would unify alpha := gamma1; and kick out the wanted
1971 constraint. But when we grough it back in, it'd look like
1972 [W] TF (gamma1, beta) ~ fuv
1973 and exactly the same thing would happen again! Infnite loop.
1974
1975 This all sesms fragile, and it might seem more robust to avoid
1976 introducing gamma1 in the first place, in the case where the
1977 actual argument (alpha, beta) partly matches the improvement
1978 template. But that's a bit tricky, esp when we remember that the
1979 kinds much match too; so it's easier to let the normal machinery
1980 handle it. Instead we are careful to orient the new derived
1981 equality with the template on the left. Delicate, but it works.
1982
1983 Note [No FunEq improvement for Givens]
1984 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1985 We don't do improvements (injectivity etc) for Givens. Why?
1986
1987 * It generates Derived constraints on skolems, which don't do us
1988 much good, except perhaps identify inaccessible branches.
1989 (They'd be perfectly valid though.)
1990
1991 * For type-nat stuff the derived constraints include type families;
1992 e.g. (a < b), (b < c) ==> a < c If we generate a Derived for this,
1993 we'll generate a Derived/Wanted CFunEqCan; and, since the same
1994 InertCans (after solving Givens) are used for each iteration, that
1995 massively confused the unflattening step (TcFlatten.unflatten).
1996
1997 In fact it led to some infinite loops:
1998 indexed-types/should_compile/T10806
1999 indexed-types/should_compile/T10507
2000 polykinds/T10742
2001
2002 Note [Reduction for Derived CFunEqCans]
2003 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2004 You may wonder if it's important to use top-level instances to
2005 simplify [D] CFunEqCan's. But it is. Here's an example (T10226).
2006
2007 type instance F Int = Int
2008 type instance FInv Int = Int
2009
2010 Suppose we have to solve
2011 [WD] FInv (F alpha) ~ alpha
2012 [WD] F alpha ~ Int
2013
2014 --> flatten
2015 [WD] F alpha ~ fuv0
2016 [WD] FInv fuv0 ~ fuv1 -- (A)
2017 [WD] fuv1 ~ alpha
2018 [WD] fuv0 ~ Int -- (B)
2019
2020 --> Rewwrite (A) with (B), splitting it
2021 [WD] F alpha ~ fuv0
2022 [W] FInv fuv0 ~ fuv1
2023 [D] FInv Int ~ fuv1 -- (C)
2024 [WD] fuv1 ~ alpha
2025 [WD] fuv0 ~ Int
2026
2027 --> Reduce (C) with top-level instance
2028 **** This is the key step ***
2029 [WD] F alpha ~ fuv0
2030 [W] FInv fuv0 ~ fuv1
2031 [D] fuv1 ~ Int -- (D)
2032 [WD] fuv1 ~ alpha -- (E)
2033 [WD] fuv0 ~ Int
2034
2035 --> Rewrite (D) with (E)
2036 [WD] F alpha ~ fuv0
2037 [W] FInv fuv0 ~ fuv1
2038 [D] alpha ~ Int -- (F)
2039 [WD] fuv1 ~ alpha
2040 [WD] fuv0 ~ Int
2041
2042 --> unify (F) alpha := Int, and that solves it
2043
2044 Another example is indexed-types/should_compile/T10634
2045 -}
2046
2047 {- *******************************************************************
2048 * *
2049 Top-level reaction for class constraints (CDictCan)
2050 * *
2051 **********************************************************************-}
2052
2053 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
2054 -- Try to use type-class instance declarations to simplify the constraint
2055 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
2056 , cc_tyargs = xis })
2057 | isGiven fl -- Never use instances for Given constraints
2058 = do { try_fundep_improvement
2059 ; continueWith work_item }
2060
2061 | Just ev <- lookupSolvedDict inerts cls xis -- Cached
2062 = do { setEvBindIfWanted fl (ctEvTerm ev)
2063 ; stopWith fl "Dict/Top (cached)" }
2064
2065 | otherwise -- Wanted or Derived, but not cached
2066 = do { dflags <- getDynFlags
2067 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
2068 ; case lkup_inst_res of
2069 GenInst { lir_new_theta = theta
2070 , lir_mk_ev = mk_ev
2071 , lir_safe_over = s } ->
2072 do { traceTcS "doTopReact/found instance for" $ ppr fl
2073 ; checkReductionDepth deeper_loc dict_pred
2074 ; unless s $ insertSafeOverlapFailureTcS work_item
2075 ; if isDerived fl then finish_derived theta
2076 else finish_wanted theta mk_ev }
2077 NoInstance ->
2078 do { when (isImprovable fl) $
2079 try_fundep_improvement
2080 ; continueWith work_item } }
2081 where
2082 dict_pred = mkClassPred cls xis
2083 dict_loc = ctEvLoc fl
2084 dict_origin = ctLocOrigin dict_loc
2085 deeper_loc = zap_origin (bumpCtLocDepth dict_loc)
2086
2087 zap_origin loc -- After applying an instance we can set ScOrigin to
2088 -- infinity, so that prohibitedSuperClassSolve never fires
2089 | ScOrigin {} <- dict_origin
2090 = setCtLocOrigin loc (ScOrigin infinity)
2091 | otherwise
2092 = loc
2093
2094 finish_wanted :: [TcPredType]
2095 -> ([EvTerm] -> EvTerm) -> TcS (StopOrContinue Ct)
2096 -- Precondition: evidence term matches the predicate workItem
2097 finish_wanted theta mk_ev
2098 = do { addSolvedDict fl cls xis
2099 ; evc_vars <- mapM (newWanted deeper_loc) theta
2100 ; setWantedEvBind (ctEvId fl) (mk_ev (map getEvTerm evc_vars))
2101 ; emitWorkNC (freshGoals evc_vars)
2102 ; stopWith fl "Dict/Top (solved wanted)" }
2103
2104 finish_derived theta -- Use type-class instances for Deriveds, in the hope
2105 = -- of generating some improvements
2106 -- C.f. Example 3 of Note [The improvement story]
2107 -- It's easy because no evidence is involved
2108 do { emitNewDeriveds deeper_loc theta
2109 ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
2110 ; stopWith fl "Dict/Top (solved derived)" }
2111
2112 -- We didn't solve it; so try functional dependencies with
2113 -- the instance environment, and return
2114 -- See also Note [Weird fundeps]
2115 try_fundep_improvement
2116 = do { traceTcS "try_fundeps" (ppr work_item)
2117 ; instEnvs <- getInstEnvs
2118 ; emitFunDepDeriveds $
2119 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
2120
2121 mk_ct_loc :: PredType -- From instance decl
2122 -> SrcSpan -- also from instance deol
2123 -> CtLoc
2124 mk_ct_loc inst_pred inst_loc
2125 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
2126 inst_pred inst_loc }
2127
2128 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
2129
2130
2131 {- *******************************************************************
2132 * *
2133 Class lookup
2134 * *
2135 **********************************************************************-}
2136
2137 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
2138 -- check.
2139 --
2140 -- See Note [Safe Haskell Overlapping Instances] in TcSimplify
2141 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
2142 type SafeOverlapping = Bool
2143
2144 data LookupInstResult
2145 = NoInstance
2146 | GenInst { lir_new_theta :: [TcPredType]
2147 , lir_mk_ev :: [EvTerm] -> EvTerm
2148 , lir_safe_over :: SafeOverlapping }
2149
2150 instance Outputable LookupInstResult where
2151 ppr NoInstance = text "NoInstance"
2152 ppr (GenInst { lir_new_theta = ev
2153 , lir_safe_over = s })
2154 = text "GenInst" <+> vcat [ppr ev, ss]
2155 where ss = text $ if s then "[safe]" else "[unsafe]"
2156
2157
2158 matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
2159 matchClassInst dflags inerts clas tys loc
2160 -- First check whether there is an in-scope Given that could
2161 -- match this constraint. In that case, do not use top-level
2162 -- instances. See Note [Instance and Given overlap]
2163 | not (xopt LangExt.IncoherentInstances dflags)
2164 , not (naturallyCoherentClass clas)
2165 , let matchable_givens = matchableGivens loc pred inerts
2166 , not (isEmptyBag matchable_givens)
2167 = do { traceTcS "Delaying instance application" $
2168 vcat [ text "Work item=" <+> pprClassPred clas tys
2169 , text "Potential matching givens:" <+> ppr matchable_givens ]
2170 ; return NoInstance }
2171 where
2172 pred = mkClassPred clas tys
2173
2174 matchClassInst dflags _ clas tys loc
2175 = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr (mkClassPred clas tys) <+> char '{'
2176 ; res <- match_class_inst dflags clas tys loc
2177 ; traceTcS "} matchClassInst result" $ ppr res
2178 ; return res }
2179
2180 match_class_inst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
2181 match_class_inst dflags clas tys loc
2182 | cls_name == knownNatClassName = matchKnownNat clas tys
2183 | cls_name == knownSymbolClassName = matchKnownSymbol clas tys
2184 | isCTupleClass clas = matchCTuple clas tys
2185 | cls_name == typeableClassName = matchTypeable clas tys
2186 | clas `hasKey` heqTyConKey = matchLiftedEquality tys
2187 | clas `hasKey` coercibleTyConKey = matchLiftedCoercible tys
2188 | otherwise = matchInstEnv dflags clas tys loc
2189 where
2190 cls_name = className clas
2191
2192 {- Note [Instance and Given overlap]
2193 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2194 Example, from the OutsideIn(X) paper:
2195 instance P x => Q [x]
2196 instance (x ~ y) => R y [x]
2197
2198 wob :: forall a b. (Q [b], R b a) => a -> Int
2199
2200 g :: forall a. Q [a] => [a] -> Int
2201 g x = wob x
2202
2203 From 'g' we get the impliation constraint:
2204 forall a. Q [a] => (Q [beta], R beta [a])
2205 If we react (Q [beta]) with its top-level axiom, we end up with a
2206 (P beta), which we have no way of discharging. On the other hand,
2207 if we react R beta [a] with the top-level we get (beta ~ a), which
2208 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2209 now solvable by the given Q [a].
2210
2211 The partial solution is that:
2212 In matchClassInst (and thus in topReact), we return a matching
2213 instance only when there is no Given in the inerts which is
2214 unifiable to this particular dictionary.
2215
2216 We treat any meta-tyvar as "unifiable" for this purpose,
2217 *including* untouchable ones. But not skolems like 'a' in
2218 the implication constraint above.
2219
2220 The end effect is that, much as we do for overlapping instances, we
2221 delay choosing a class instance if there is a possibility of another
2222 instance OR a given to match our constraint later on. This fixes
2223 Trac #4981 and #5002.
2224
2225 Other notes:
2226
2227 * The check is done *first*, so that it also covers classes
2228 with built-in instance solving, such as
2229 - constraint tuples
2230 - natural numbers
2231 - Typeable
2232
2233 * The given-overlap problem is arguably not easy to appear in practice
2234 due to our aggressive prioritization of equality solving over other
2235 constraints, but it is possible. I've added a test case in
2236 typecheck/should-compile/GivenOverlapping.hs
2237
2238 * Another "live" example is Trac #10195; another is #10177.
2239
2240 * We ignore the overlap problem if -XIncoherentInstances is in force:
2241 see Trac #6002 for a worked-out example where this makes a
2242 difference.
2243
2244 * Moreover notice that our goals here are different than the goals of
2245 the top-level overlapping checks. There we are interested in
2246 validating the following principle:
2247
2248 If we inline a function f at a site where the same global
2249 instance environment is available as the instance environment at
2250 the definition site of f then we should get the same behaviour.
2251
2252 But for the Given Overlap check our goal is just related to completeness of
2253 constraint solving.
2254
2255 * The solution is only a partial one. Consider the above example with
2256 g :: forall a. Q [a] => [a] -> Int
2257 g x = let v = wob x
2258 in v
2259 and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
2260 general type for 'v'. When generalising v's type we'll simplify its
2261 Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
2262 will use the instance declaration after all. Trac #11948 was a case
2263 in point.
2264
2265 All of this is disgustingly delicate, so to discourage people from writing
2266 simplifiable class givens, we warn about signatures that contain them;#
2267 see TcValidity Note [Simplifiable given constraints].
2268 -}
2269
2270
2271 {- *******************************************************************
2272 * *
2273 Class lookup in the instance environment
2274 * *
2275 **********************************************************************-}
2276
2277 matchInstEnv :: DynFlags -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
2278 matchInstEnv dflags clas tys loc
2279 = do { instEnvs <- getInstEnvs
2280 ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
2281 (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
2282 safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
2283 ; case (matches, unify, safeHaskFail) of
2284
2285 -- Nothing matches
2286 ([], _, _)
2287 -> do { traceTcS "matchClass not matching" $
2288 vcat [ text "dict" <+> ppr pred ]
2289 ; return NoInstance }
2290
2291 -- A single match (& no safe haskell failure)
2292 ([(ispec, inst_tys)], [], False)
2293 -> do { let dfun_id = instanceDFunId ispec
2294 ; traceTcS "matchClass success" $
2295 vcat [text "dict" <+> ppr pred,
2296 text "witness" <+> ppr dfun_id
2297 <+> ppr (idType dfun_id) ]
2298 -- Record that this dfun is needed
2299 ; match_one (null unsafeOverlaps) dfun_id inst_tys }
2300
2301 -- More than one matches (or Safe Haskell fail!). Defer any
2302 -- reactions of a multitude until we learn more about the reagent
2303 (matches, _, _)
2304 -> do { traceTcS "matchClass multiple matches, deferring choice" $
2305 vcat [text "dict" <+> ppr pred,
2306 text "matches" <+> ppr matches]
2307 ; return NoInstance } }
2308 where
2309 pred = mkClassPred clas tys
2310
2311 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
2312 -- See Note [DFunInstType: instantiating types] in InstEnv
2313 match_one so dfun_id mb_inst_tys
2314 = do { checkWellStagedDFun pred dfun_id loc
2315 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
2316 ; return $ GenInst { lir_new_theta = theta
2317 , lir_mk_ev = EvDFunApp dfun_id tys
2318 , lir_safe_over = so } }
2319
2320
2321 {- ********************************************************************
2322 * *
2323 Class lookup for CTuples
2324 * *
2325 ***********************************************************************-}
2326
2327 matchCTuple :: Class -> [Type] -> TcS LookupInstResult
2328 matchCTuple clas tys -- (isCTupleClass clas) holds
2329 = return (GenInst { lir_new_theta = tys
2330 , lir_mk_ev = tuple_ev
2331 , lir_safe_over = True })
2332 -- The dfun *is* the data constructor!
2333 where
2334 data_con = tyConSingleDataCon (classTyCon clas)
2335 tuple_ev = EvDFunApp (dataConWrapId data_con) tys
2336
2337 {- ********************************************************************
2338 * *
2339 Class lookup for Literals
2340 * *
2341 ***********************************************************************-}
2342
2343 matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
2344 matchKnownNat clas [ty] -- clas = KnownNat
2345 | Just n <- isNumLitTy ty = makeLitDict clas ty (EvNum n)
2346 matchKnownNat _ _ = return NoInstance
2347
2348 matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
2349 matchKnownSymbol clas [ty] -- clas = KnownSymbol
2350 | Just n <- isStrLitTy ty = makeLitDict clas ty (EvStr n)
2351 matchKnownSymbol _ _ = return NoInstance
2352
2353
2354 makeLitDict :: Class -> Type -> EvLit -> TcS LookupInstResult
2355 -- makeLitDict adds a coercion that will convert the literal into a dictionary
2356 -- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
2357 -- in TcEvidence. The coercion happens in 2 steps:
2358 --
2359 -- Integer -> SNat n -- representation of literal to singleton
2360 -- SNat n -> KnownNat n -- singleton to dictionary
2361 --
2362 -- The process is mirrored for Symbols:
2363 -- String -> SSymbol n
2364 -- SSymbol n -> KnownSymbol n -}
2365 makeLitDict clas ty evLit
2366 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
2367 -- co_dict :: KnownNat n ~ SNat n
2368 , [ meth ] <- classMethods clas
2369 , Just tcRep <- tyConAppTyCon_maybe -- SNat
2370 $ funResultTy -- SNat n
2371 $ dropForAlls -- KnownNat n => SNat n
2372 $ idType meth -- forall n. KnownNat n => SNat n
2373 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
2374 -- SNat n ~ Integer
2375 , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))
2376 = return $ GenInst { lir_new_theta = []
2377 , lir_mk_ev = \_ -> ev_tm
2378 , lir_safe_over = True }
2379
2380 | otherwise
2381 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
2382 $$ vcat (map (ppr . idType) (classMethods clas)))
2383
2384
2385 {- ********************************************************************
2386 * *
2387 Class lookup for Typeable
2388 * *
2389 ***********************************************************************-}
2390
2391 -- | Assumes that we've checked that this is the 'Typeable' class,
2392 -- and it was applied to the correct argument.
2393 matchTypeable :: Class -> [Type] -> TcS LookupInstResult
2394 matchTypeable clas [k,t] -- clas = Typeable
2395 -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
2396 | isForAllTy k = return NoInstance -- Polytype
2397 | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type
2398
2399 -- Now cases that do work
2400 | k `eqType` typeNatKind = doTyLit knownNatClassName t
2401 | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t
2402 | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
2403 , onlyNamedBndrsApplied tc ks = doTyConApp clas t ks
2404 | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt
2405
2406 matchTypeable _ _ = return NoInstance
2407
2408 doTyConApp :: Class -> Type -> [Kind] -> TcS LookupInstResult
2409 -- Representation for type constructor applied to some kinds
2410 doTyConApp clas ty args
2411 = return $ GenInst (map (mk_typeable_pred clas) args)
2412 (\tms -> EvTypeable ty $ EvTypeableTyCon tms)
2413 True
2414
2415 -- Representation for concrete kinds. We just use the kind itself,
2416 -- but first we must make sure that we've instantiated all kind-
2417 -- polymorphism, but no more.
2418 onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
2419 onlyNamedBndrsApplied tc ks
2420 = all isNamedTyConBinder used_bndrs &&
2421 all (not . isNamedTyConBinder) leftover_bndrs
2422 where
2423 bndrs = tyConBinders tc
2424 (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
2425
2426 doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
2427 -- Representation for an application of a type to a type-or-kind.
2428 -- This may happen when the type expression starts with a type variable.
2429 -- Example (ignoring kind parameter):
2430 -- Typeable (f Int Char) -->
2431 -- (Typeable (f Int), Typeable Char) -->
2432 -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
2433 -- Typeable f
2434 doTyApp clas ty f tk
2435 | isForAllTy (typeKind f)
2436 = return NoInstance -- We can't solve until we know the ctr.
2437 | otherwise
2438 = do { traceTcS "doTyApp" (ppr clas $$ ppr ty $$ ppr f $$ ppr tk)
2439 ; return $ GenInst [mk_typeable_pred clas f, mk_typeable_pred clas tk]
2440 (\[t1,t2] -> EvTypeable ty $ EvTypeableTyApp t1 t2)
2441 True }
2442
2443 -- Emit a `Typeable` constraint for the given type.
2444 mk_typeable_pred :: Class -> Type -> PredType
2445 mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
2446
2447 -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
2448 -- we generate a sub-goal for the appropriate class. See #10348 for what
2449 -- happens when we fail to do this.
2450 doTyLit :: Name -> Type -> TcS LookupInstResult
2451 doTyLit kc t = do { kc_clas <- tcLookupClass kc
2452 ; let kc_pred = mkClassPred kc_clas [ t ]
2453 mk_ev [ev] = EvTypeable t $ EvTypeableTyLit ev
2454 mk_ev _ = panic "doTyLit"
2455 ; return (GenInst [kc_pred] mk_ev True) }
2456
2457 {- Note [Typeable (T a b c)]
2458 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2459 For type applications we always decompose using binary application,
2460 via doTyApp, until we get to a *kind* instantiation. Exmaple
2461 Proxy :: forall k. k -> *
2462
2463 To solve Typeable (Proxy (* -> *) Maybe) we
2464 - First decompose with doTyApp,
2465 to get (Typeable (Proxy (* -> *))) and Typeable Maybe
2466 - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
2467
2468 If we attempt to short-cut by solving it all at once, via
2469 doTyCOnAPp
2470
2471
2472 Note [No Typeable for polytypes or qualified types]
2473 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2474 We do not support impredicative typeable, such as
2475 Typeable (forall a. a->a)
2476 Typeable (Eq a => a -> a)
2477 Typeable (() => Int)
2478 Typeable (((),()) => Int)
2479
2480 See Trac #9858. For forall's the case is clear: we simply don't have
2481 a TypeRep for them. For qualified but not polymorphic types, like
2482 (Eq a => a -> a), things are murkier. But:
2483
2484 * We don't need a TypeRep for these things. TypeReps are for
2485 monotypes only.
2486
2487 * Perhaps we could treat `=>` as another type constructor for `Typeable`
2488 purposes, and thus support things like `Eq Int => Int`, however,
2489 at the current state of affairs this would be an odd exception as
2490 no other class works with impredicative types.
2491 For now we leave it off, until we have a better story for impredicativity.
2492 -}
2493
2494 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
2495 solveCallStack ev ev_cs = do
2496 -- We're given ev_cs :: CallStack, but the evidence term should be a
2497 -- dictionary, so we have to coerce ev_cs to a dictionary for
2498 -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]
2499 let ev_tm = mkEvCast (EvCallStack ev_cs) (wrapIP (ctEvPred ev))
2500 setWantedEvBind (ctEvId ev) ev_tm
2501
2502 {- ********************************************************************
2503 * *
2504 Class lookup for lifted equality
2505 * *
2506 ***********************************************************************-}
2507
2508 -- See also Note [The equality types story] in TysPrim
2509 matchLiftedEquality :: [Type] -> TcS LookupInstResult
2510 matchLiftedEquality args
2511 = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
2512 , lir_mk_ev = EvDFunApp (dataConWrapId heqDataCon) args
2513 , lir_safe_over = True })
2514
2515 -- See also Note [The equality types story] in TysPrim
2516 matchLiftedCoercible :: [Type] -> TcS LookupInstResult
2517 matchLiftedCoercible args@[k, t1, t2]
2518 = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
2519 , lir_mk_ev = EvDFunApp (dataConWrapId coercibleDataCon)
2520 args
2521 , lir_safe_over = True })
2522 where
2523 args' = [k, k, t1, t2]
2524 matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)