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