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