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