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