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