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