b2be509b698a8569087cb83fc4380777353f7f2b
[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 = do { traceTcS "reactFunEq"
1436 (vcat [ppr from_this, ppr fsk1, ppr solve_this, ppr fsk2])
1437 ; dischargeFunEq solve_this fsk2 (ctEvCoercion from_this) (mkTyVarTy fsk1)
1438 ; traceTcS "reactFunEq done" (ppr from_this $$ ppr fsk1 $$
1439 ppr solve_this $$ ppr fsk2) }
1440
1441 {- Note [Type inference for type families with injectivity]
1442 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1443 Suppose we have a type family with an injectivity annotation:
1444 type family F a b = r | r -> b
1445
1446 Then if we have two CFunEqCan constraints for F with the same RHS
1447 F s1 t1 ~ rhs
1448 F s2 t2 ~ rhs
1449 then we can use the injectivity to get a new Derived constraint on
1450 the injective argument
1451 [D] t1 ~ t2
1452
1453 That in turn can help GHC solve constraints that would otherwise require
1454 guessing. For example, consider the ambiguity check for
1455 f :: F Int b -> Int
1456 We get the constraint
1457 [W] F Int b ~ F Int beta
1458 where beta is a unification variable. Injectivity lets us pick beta ~ b.
1459
1460 Injectivity information is also used at the call sites. For example:
1461 g = f True
1462 gives rise to
1463 [W] F Int b ~ Bool
1464 from which we can derive b. This requires looking at the defining equations of
1465 a type family, ie. finding equation with a matching RHS (Bool in this example)
1466 and infering values of type variables (b in this example) from the LHS patterns
1467 of the matching equation. For closed type families we have to perform
1468 additional apartness check for the selected equation to check that the selected
1469 is guaranteed to fire for given LHS arguments.
1470
1471 These new constraints are simply *Derived* constraints; they have no evidence.
1472 We could go further and offer evidence from decomposing injective type-function
1473 applications, but that would require new evidence forms, and an extension to
1474 FC, so we don't do that right now (Dec 14).
1475
1476 See also Note [Injective type families] in TyCon
1477
1478
1479 Note [Cache-caused loops]
1480 ~~~~~~~~~~~~~~~~~~~~~~~~~
1481 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
1482 solved cache (which is the default behaviour or xCtEvidence), because the interaction
1483 may not be contributing towards a solution. Here is an example:
1484
1485 Initial inert set:
1486 [W] g1 : F a ~ beta1
1487 Work item:
1488 [W] g2 : F a ~ beta2
1489 The work item will react with the inert yielding the _same_ inert set plus:
1490 (i) Will set g2 := g1 `cast` g3
1491 (ii) Will add to our solved cache that [S] g2 : F a ~ beta2
1492 (iii) Will emit [W] g3 : beta1 ~ beta2
1493 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
1494 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
1495 will set
1496 g1 := g ; sym g3
1497 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
1498 remember that we have this in our solved cache, and it is ... g2! In short we
1499 created the evidence loop:
1500
1501 g2 := g1 ; g3
1502 g3 := refl
1503 g1 := g2 ; sym g3
1504
1505 To avoid this situation we do not cache as solved any workitems (or inert)
1506 which did not really made a 'step' towards proving some goal. Solved's are
1507 just an optimization so we don't lose anything in terms of completeness of
1508 solving.
1509
1510
1511 Note [Efficient Orientation]
1512 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1513 Suppose we are interacting two FunEqCans with the same LHS:
1514 (inert) ci :: (F ty ~ xi_i)
1515 (work) cw :: (F ty ~ xi_w)
1516 We prefer to keep the inert (else we pass the work item on down
1517 the pipeline, which is a bit silly). If we keep the inert, we
1518 will (a) discharge 'cw'
1519 (b) produce a new equality work-item (xi_w ~ xi_i)
1520 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
1521 new_work :: xi_w ~ xi_i
1522 cw := ci ; sym new_work
1523 Why? Consider the simplest case when xi1 is a type variable. If
1524 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
1525 If we generate xi2~xi1, there is less chance of that happening.
1526 Of course it can and should still happen if xi1=a, xi1=Int, say.
1527 But we want to avoid it happening needlessly.
1528
1529 Similarly, if we *can't* keep the inert item (because inert is Wanted,
1530 and work is Given, say), we prefer to orient the new equality (xi_i ~
1531 xi_w).
1532
1533 Note [Carefully solve the right CFunEqCan]
1534 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1535 ---- OLD COMMENT, NOW NOT NEEDED
1536 ---- because we now allow multiple
1537 ---- wanted FunEqs with the same head
1538 Consider the constraints
1539 c1 :: F Int ~ a -- Arising from an application line 5
1540 c2 :: F Int ~ Bool -- Arising from an application line 10
1541 Suppose that 'a' is a unification variable, arising only from
1542 flattening. So there is no error on line 5; it's just a flattening
1543 variable. But there is (or might be) an error on line 10.
1544
1545 Two ways to combine them, leaving either (Plan A)
1546 c1 :: F Int ~ a -- Arising from an application line 5
1547 c3 :: a ~ Bool -- Arising from an application line 10
1548 or (Plan B)
1549 c2 :: F Int ~ Bool -- Arising from an application line 10
1550 c4 :: a ~ Bool -- Arising from an application line 5
1551
1552 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
1553 on the *totally innocent* line 5. An example is test SimpleFail16
1554 where the expected/actual message comes out backwards if we use
1555 the wrong plan.
1556
1557 The second is the right thing to do. Hence the isMetaTyVarTy
1558 test when solving pairwise CFunEqCan.
1559
1560
1561 **********************************************************************
1562 * *
1563 interactTyVarEq
1564 * *
1565 **********************************************************************
1566 -}
1567
1568 inertsCanDischarge :: InertCans -> TcTyVar -> TcType -> CtFlavourRole
1569 -> Maybe ( CtEvidence -- The evidence for the inert
1570 , SwapFlag -- Whether we need mkSymCo
1571 , Bool) -- True <=> keep a [D] version
1572 -- of the [WD] constraint
1573 inertsCanDischarge inerts tv rhs fr
1574 | (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
1575 , cc_eq_rel = eq_rel }
1576 <- findTyEqs inerts tv
1577 , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
1578 , rhs_i `tcEqType` rhs ]
1579 = -- Inert: a ~ ty
1580 -- Work item: a ~ ty
1581 Just (ev_i, NotSwapped, keep_deriv ev_i)
1582
1583 | Just tv_rhs <- getTyVar_maybe rhs
1584 , (ev_i : _) <- [ ev_i | CTyEqCan { cc_ev = ev_i, cc_rhs = rhs_i
1585 , cc_eq_rel = eq_rel }
1586 <- findTyEqs inerts tv_rhs
1587 , (ctEvFlavour ev_i, eq_rel) `eqCanDischargeFR` fr
1588 , rhs_i `tcEqType` mkTyVarTy tv ]
1589 = -- Inert: a ~ b
1590 -- Work item: b ~ a
1591 Just (ev_i, IsSwapped, keep_deriv ev_i)
1592
1593 | otherwise
1594 = Nothing
1595
1596 where
1597 keep_deriv ev_i
1598 | Wanted WOnly <- ctEvFlavour ev_i -- inert is [W]
1599 , (Wanted WDeriv, _) <- fr -- work item is [WD]
1600 = True -- Keep a derived verison of the work item
1601 | otherwise
1602 = False -- Work item is fully discharged
1603
1604 interactTyVarEq :: InertCans -> Ct -> TcS (StopOrContinue Ct)
1605 -- CTyEqCans are always consumed, so always returns Stop
1606 interactTyVarEq inerts workItem@(CTyEqCan { cc_tyvar = tv
1607 , cc_rhs = rhs
1608 , cc_ev = ev
1609 , cc_eq_rel = eq_rel })
1610 | Just (ev_i, swapped, keep_deriv)
1611 <- inertsCanDischarge inerts tv rhs (ctEvFlavour ev, eq_rel)
1612 = do { setEvBindIfWanted ev $
1613 evCoercion (maybeSym swapped $
1614 tcDowngradeRole (eqRelRole eq_rel)
1615 (ctEvRole ev_i)
1616 (ctEvCoercion ev_i))
1617
1618 ; let deriv_ev = CtDerived { ctev_pred = ctEvPred ev
1619 , ctev_loc = ctEvLoc ev }
1620 ; when keep_deriv $
1621 emitWork [workItem { cc_ev = deriv_ev }]
1622 -- As a Derived it might not be fully rewritten,
1623 -- so we emit it as new work
1624
1625 ; stopWith ev "Solved from inert" }
1626
1627 | ReprEq <- eq_rel -- See Note [Do not unify representational equalities]
1628 = unsolved_inert
1629
1630 | isGiven ev -- See Note [Touchables and givens]
1631 = unsolved_inert
1632
1633 | otherwise
1634 = do { tclvl <- getTcLevel
1635 ; if canSolveByUnification tclvl tv rhs
1636 then do { solveByUnification ev tv rhs
1637 ; n_kicked <- kickOutAfterUnification tv
1638 ; return (Stop ev (text "Solved by unification" <+> pprKicked n_kicked)) }
1639
1640 else unsolved_inert }
1641
1642 where
1643 unsolved_inert
1644 = do { traceTcS "Can't solve tyvar equality"
1645 (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
1646 , ppWhen (isMetaTyVar tv) $
1647 nest 4 (text "TcLevel of" <+> ppr tv
1648 <+> text "is" <+> ppr (metaTyVarTcLevel tv))
1649 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs) ])
1650 ; addInertEq workItem
1651 ; stopWith ev "Kept as inert" }
1652
1653 interactTyVarEq _ wi = pprPanic "interactTyVarEq" (ppr wi)
1654
1655 solveByUnification :: CtEvidence -> TcTyVar -> Xi -> TcS ()
1656 -- Solve with the identity coercion
1657 -- Precondition: kind(xi) equals kind(tv)
1658 -- Precondition: CtEvidence is Wanted or Derived
1659 -- Precondition: CtEvidence is nominal
1660 -- Returns: workItem where
1661 -- workItem = the new Given constraint
1662 --
1663 -- NB: No need for an occurs check here, because solveByUnification always
1664 -- arises from a CTyEqCan, a *canonical* constraint. Its invariants
1665 -- say that in (a ~ xi), the type variable a does not appear in xi.
1666 -- See TcRnTypes.Ct invariants.
1667 --
1668 -- Post: tv is unified (by side effect) with xi;
1669 -- we often write tv := xi
1670 solveByUnification wd tv xi
1671 = do { let tv_ty = mkTyVarTy tv
1672 ; traceTcS "Sneaky unification:" $
1673 vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
1674 text "Coercion:" <+> pprEq tv_ty xi,
1675 text "Left Kind is:" <+> ppr (typeKind tv_ty),
1676 text "Right Kind is:" <+> ppr (typeKind xi) ]
1677
1678 ; unifyTyVar tv xi
1679 ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
1680
1681 {- Note [Avoid double unifications]
1682 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1683 The spontaneous solver has to return a given which mentions the unified unification
1684 variable *on the left* of the equality. Here is what happens if not:
1685 Original wanted: (a ~ alpha), (alpha ~ Int)
1686 We spontaneously solve the first wanted, without changing the order!
1687 given : a ~ alpha [having unified alpha := a]
1688 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
1689 At the end we spontaneously solve that guy, *reunifying* [alpha := Int]
1690
1691 We avoid this problem by orienting the resulting given so that the unification
1692 variable is on the left. [Note that alternatively we could attempt to
1693 enforce this at canonicalization]
1694
1695 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
1696 double unifications is the main reason we disallow touchable
1697 unification variables as RHS of type family equations: F xis ~ alpha.
1698
1699 Note [Do not unify representational equalities]
1700 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1701 Consider [W] alpha ~R# b
1702 where alpha is touchable. Should we unify alpha := b?
1703
1704 Certainly not! Unifying forces alpha and be to be the same; but they
1705 only need to be representationally equal types.
1706
1707 For example, we might have another constraint [W] alpha ~# N b
1708 where
1709 newtype N b = MkN b
1710 and we want to get alpha := N b.
1711
1712 See also Trac #15144, which was caused by unifying a representational
1713 equality (in the unflattener).
1714
1715
1716 ************************************************************************
1717 * *
1718 * Functional dependencies, instantiation of equations
1719 * *
1720 ************************************************************************
1721
1722 When we spot an equality arising from a functional dependency,
1723 we now use that equality (a "wanted") to rewrite the work-item
1724 constraint right away. This avoids two dangers
1725
1726 Danger 1: If we send the original constraint on down the pipeline
1727 it may react with an instance declaration, and in delicate
1728 situations (when a Given overlaps with an instance) that
1729 may produce new insoluble goals: see Trac #4952
1730
1731 Danger 2: If we don't rewrite the constraint, it may re-react
1732 with the same thing later, and produce the same equality
1733 again --> termination worries.
1734
1735 To achieve this required some refactoring of FunDeps.hs (nicer
1736 now!).
1737
1738 Note [FunDep and implicit parameter reactions]
1739 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1740 Currently, our story of interacting two dictionaries (or a dictionary
1741 and top-level instances) for functional dependencies, and implicit
1742 parameters, is that we simply produce new Derived equalities. So for example
1743
1744 class D a b | a -> b where ...
1745 Inert:
1746 d1 :g D Int Bool
1747 WorkItem:
1748 d2 :w D Int alpha
1749
1750 We generate the extra work item
1751 cv :d alpha ~ Bool
1752 where 'cv' is currently unused. However, this new item can perhaps be
1753 spontaneously solved to become given and react with d2,
1754 discharging it in favour of a new constraint d2' thus:
1755 d2' :w D Int Bool
1756 d2 := d2' |> D Int cv
1757 Now d2' can be discharged from d1
1758
1759 We could be more aggressive and try to *immediately* solve the dictionary
1760 using those extra equalities, but that requires those equalities to carry
1761 evidence and derived do not carry evidence.
1762
1763 If that were the case with the same inert set and work item we might dischard
1764 d2 directly:
1765
1766 cv :w alpha ~ Bool
1767 d2 := d1 |> D Int cv
1768
1769 But in general it's a bit painful to figure out the necessary coercion,
1770 so we just take the first approach. Here is a better example. Consider:
1771 class C a b c | a -> b
1772 And:
1773 [Given] d1 : C T Int Char
1774 [Wanted] d2 : C T beta Int
1775 In this case, it's *not even possible* to solve the wanted immediately.
1776 So we should simply output the functional dependency and add this guy
1777 [but NOT its superclasses] back in the worklist. Even worse:
1778 [Given] d1 : C T Int beta
1779 [Wanted] d2: C T beta Int
1780 Then it is solvable, but its very hard to detect this on the spot.
1781
1782 It's exactly the same with implicit parameters, except that the
1783 "aggressive" approach would be much easier to implement.
1784
1785 Note [Weird fundeps]
1786 ~~~~~~~~~~~~~~~~~~~~
1787 Consider class Het a b | a -> b where
1788 het :: m (f c) -> a -> m b
1789
1790 class GHet (a :: * -> *) (b :: * -> *) | a -> b
1791 instance GHet (K a) (K [a])
1792 instance Het a b => GHet (K a) (K b)
1793
1794 The two instances don't actually conflict on their fundeps,
1795 although it's pretty strange. So they are both accepted. Now
1796 try [W] GHet (K Int) (K Bool)
1797 This triggers fundeps from both instance decls;
1798 [D] K Bool ~ K [a]
1799 [D] K Bool ~ K beta
1800 And there's a risk of complaining about Bool ~ [a]. But in fact
1801 the Wanted matches the second instance, so we never get as far
1802 as the fundeps.
1803
1804 Trac #7875 is a case in point.
1805 -}
1806
1807 emitFunDepDeriveds :: [FunDepEqn CtLoc] -> TcS ()
1808 -- See Note [FunDep and implicit parameter reactions]
1809 emitFunDepDeriveds fd_eqns
1810 = mapM_ do_one_FDEqn fd_eqns
1811 where
1812 do_one_FDEqn (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = loc })
1813 | null tvs -- Common shortcut
1814 = do { traceTcS "emitFunDepDeriveds 1" (ppr (ctl_depth loc) $$ ppr eqs $$ ppr (isGivenLoc loc))
1815 ; mapM_ (unifyDerived loc Nominal) eqs }
1816 | otherwise
1817 = do { traceTcS "emitFunDepDeriveds 2" (ppr (ctl_depth loc) $$ ppr eqs)
1818 ; subst <- instFlexi tvs -- Takes account of kind substitution
1819 ; mapM_ (do_one_eq loc subst) eqs }
1820
1821 do_one_eq loc subst (Pair ty1 ty2)
1822 = unifyDerived loc Nominal $
1823 Pair (Type.substTyUnchecked subst ty1) (Type.substTyUnchecked subst ty2)
1824
1825 {-
1826 **********************************************************************
1827 * *
1828 The top-reaction Stage
1829 * *
1830 **********************************************************************
1831 -}
1832
1833 topReactionsStage :: WorkItem -> TcS (StopOrContinue Ct)
1834 topReactionsStage wi
1835 = do { tir <- doTopReact wi
1836 ; case tir of
1837 ContinueWith wi -> continueWith wi
1838 Stop ev s -> return (Stop ev (text "Top react:" <+> s)) }
1839
1840 doTopReact :: WorkItem -> TcS (StopOrContinue Ct)
1841 -- The work item does not react with the inert set, so try interaction with top-level
1842 -- instances. Note:
1843 --
1844 -- (a) The place to add superclasses in not here in doTopReact stage.
1845 -- Instead superclasses are added in the worklist as part of the
1846 -- canonicalization process. See Note [Adding superclasses].
1847
1848 doTopReact work_item
1849 = do { traceTcS "doTopReact" (ppr work_item)
1850 ; case work_item of
1851 CDictCan {} -> do { inerts <- getTcSInerts
1852 ; doTopReactDict inerts work_item }
1853 CFunEqCan {} -> doTopReactFunEq work_item
1854 _ -> -- Any other work item does not react with any top-level equations
1855 continueWith work_item }
1856
1857
1858 --------------------
1859 doTopReactFunEq :: Ct -> TcS (StopOrContinue Ct)
1860 doTopReactFunEq work_item@(CFunEqCan { cc_ev = old_ev, cc_fun = fam_tc
1861 , cc_tyargs = args, cc_fsk = fsk })
1862
1863 | fsk `elemVarSet` tyCoVarsOfTypes args
1864 = no_reduction -- See Note [FunEq occurs-check principle]
1865
1866 | otherwise -- Note [Reduction for Derived CFunEqCans]
1867 = do { match_res <- matchFam fam_tc args
1868 -- Look up in top-level instances, or built-in axiom
1869 -- See Note [MATCHING-SYNONYMS]
1870 ; case match_res of
1871 Nothing -> no_reduction
1872 Just match_info -> reduce_top_fun_eq old_ev fsk match_info }
1873 where
1874 no_reduction
1875 = do { improveTopFunEqs old_ev fam_tc args fsk
1876 ; continueWith work_item }
1877
1878 doTopReactFunEq w = pprPanic "doTopReactFunEq" (ppr w)
1879
1880 reduce_top_fun_eq :: CtEvidence -> TcTyVar -> (TcCoercion, TcType)
1881 -> TcS (StopOrContinue Ct)
1882 -- We have found an applicable top-level axiom: use it to reduce
1883 -- Precondition: fsk is not free in rhs_ty
1884 reduce_top_fun_eq old_ev fsk (ax_co, rhs_ty)
1885 | not (isDerived old_ev) -- Precondition of shortCutReduction
1886 , Just (tc, tc_args) <- tcSplitTyConApp_maybe rhs_ty
1887 , isTypeFamilyTyCon tc
1888 , tc_args `lengthIs` tyConArity tc -- Short-cut
1889 = -- RHS is another type-family application
1890 -- Try shortcut; see Note [Top-level reductions for type functions]
1891 do { shortCutReduction old_ev fsk ax_co tc tc_args
1892 ; stopWith old_ev "Fun/Top (shortcut)" }
1893
1894 | otherwise
1895 = ASSERT2( not (fsk `elemVarSet` tyCoVarsOfType rhs_ty)
1896 , ppr old_ev $$ ppr rhs_ty )
1897 -- Guaranteed by Note [FunEq occurs-check principle]
1898 do { dischargeFunEq old_ev fsk ax_co rhs_ty
1899 ; traceTcS "doTopReactFunEq" $
1900 vcat [ text "old_ev:" <+> ppr old_ev
1901 , nest 2 (text ":=") <+> ppr ax_co ]
1902 ; stopWith old_ev "Fun/Top" }
1903
1904 improveTopFunEqs :: CtEvidence -> TyCon -> [TcType] -> TcTyVar -> TcS ()
1905 -- See Note [FunDep and implicit parameter reactions]
1906 improveTopFunEqs ev fam_tc args fsk
1907 | isGiven ev -- See Note [No FunEq improvement for Givens]
1908 || not (isImprovable ev)
1909 = return ()
1910
1911 | otherwise
1912 = do { ieqs <- getInertEqs
1913 ; fam_envs <- getFamInstEnvs
1914 ; eqns <- improve_top_fun_eqs fam_envs fam_tc args
1915 (lookupFlattenTyVar ieqs fsk)
1916 ; traceTcS "improveTopFunEqs" (vcat [ ppr fam_tc <+> ppr args <+> ppr fsk
1917 , ppr eqns ])
1918 ; mapM_ (unifyDerived loc Nominal) eqns }
1919 where
1920 loc = ctEvLoc ev -- ToDo: this location is wrong; it should be FunDepOrigin2
1921 -- See Trac #14778
1922
1923 improve_top_fun_eqs :: FamInstEnvs
1924 -> TyCon -> [TcType] -> TcType
1925 -> TcS [TypeEqn]
1926 improve_top_fun_eqs fam_envs fam_tc args rhs_ty
1927 | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc
1928 = return (sfInteractTop ops args rhs_ty)
1929
1930 -- see Note [Type inference for type families with injectivity]
1931 | isOpenTypeFamilyTyCon fam_tc
1932 , Injective injective_args <- tyConInjectivityInfo fam_tc
1933 , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc
1934 = -- it is possible to have several compatible equations in an open type
1935 -- family but we only want to derive equalities from one such equation.
1936 do { let improvs = buildImprovementData fam_insts
1937 fi_tvs fi_tys fi_rhs (const Nothing)
1938
1939 ; traceTcS "improve_top_fun_eqs2" (ppr improvs)
1940 ; concatMapM (injImproveEqns injective_args) $
1941 take 1 improvs }
1942
1943 | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc
1944 , Injective injective_args <- tyConInjectivityInfo fam_tc
1945 = concatMapM (injImproveEqns injective_args) $
1946 buildImprovementData (fromBranches (co_ax_branches ax))
1947 cab_tvs cab_lhs cab_rhs Just
1948
1949 | otherwise
1950 = return []
1951
1952 where
1953 buildImprovementData
1954 :: [a] -- axioms for a TF (FamInst or CoAxBranch)
1955 -> (a -> [TyVar]) -- get bound tyvars of an axiom
1956 -> (a -> [Type]) -- get LHS of an axiom
1957 -> (a -> Type) -- get RHS of an axiom
1958 -> (a -> Maybe CoAxBranch) -- Just => apartness check required
1959 -> [( [Type], TCvSubst, [TyVar], Maybe CoAxBranch )]
1960 -- Result:
1961 -- ( [arguments of a matching axiom]
1962 -- , RHS-unifying substitution
1963 -- , axiom variables without substitution
1964 -- , Maybe matching axiom [Nothing - open TF, Just - closed TF ] )
1965 buildImprovementData axioms axiomTVs axiomLHS axiomRHS wrap =
1966 [ (ax_args, subst, unsubstTvs, wrap axiom)
1967 | axiom <- axioms
1968 , let ax_args = axiomLHS axiom
1969 ax_rhs = axiomRHS axiom
1970 ax_tvs = axiomTVs axiom
1971 , Just subst <- [tcUnifyTyWithTFs False ax_rhs rhs_ty]
1972 , let notInSubst tv = not (tv `elemVarEnv` getTvSubstEnv subst)
1973 unsubstTvs = filter (notInSubst <&&> isTyVar) ax_tvs ]
1974 -- The order of unsubstTvs is important; it must be
1975 -- in telescope order e.g. (k:*) (a:k)
1976
1977 injImproveEqns :: [Bool]
1978 -> ([Type], TCvSubst, [TyCoVar], Maybe CoAxBranch)
1979 -> TcS [TypeEqn]
1980 injImproveEqns inj_args (ax_args, subst, unsubstTvs, cabr)
1981 = do { subst <- instFlexiX subst unsubstTvs
1982 -- If the current substitution bind [k -> *], and
1983 -- one of the un-substituted tyvars is (a::k), we'd better
1984 -- be sure to apply the current substitution to a's kind.
1985 -- Hence instFlexiX. Trac #13135 was an example.
1986
1987 ; return [ Pair (substTyUnchecked subst ax_arg) arg
1988 -- NB: the ax_arg part is on the left
1989 -- see Note [Improvement orientation]
1990 | case cabr of
1991 Just cabr' -> apartnessCheck (substTys subst ax_args) cabr'
1992 _ -> True
1993 , (ax_arg, arg, True) <- zip3 ax_args args inj_args ] }
1994
1995
1996 shortCutReduction :: CtEvidence -> TcTyVar -> TcCoercion
1997 -> TyCon -> [TcType] -> TcS ()
1998 -- See Note [Top-level reductions for type functions]
1999 -- Previously, we flattened the tc_args here, but there's no need to do so.
2000 -- And, if we did, this function would have all the complication of
2001 -- TcCanonical.canCFunEqCan. See Note [canCFunEqCan]
2002 shortCutReduction old_ev fsk ax_co fam_tc tc_args
2003 = ASSERT( ctEvEqRel old_ev == NomEq)
2004 -- ax_co :: F args ~ G tc_args
2005 -- old_ev :: F args ~ fsk
2006 do { new_ev <- case ctEvFlavour old_ev of
2007 Given -> newGivenEvVar deeper_loc
2008 ( mkPrimEqPred (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
2009 , evCoercion (mkTcSymCo ax_co
2010 `mkTcTransCo` ctEvCoercion old_ev) )
2011
2012 Wanted {} ->
2013 do { (new_ev, new_co) <- newWantedEq deeper_loc Nominal
2014 (mkTyConApp fam_tc tc_args) (mkTyVarTy fsk)
2015 ; setWantedEq (ctev_dest old_ev) $ ax_co `mkTcTransCo` new_co
2016 ; return new_ev }
2017
2018 Derived -> pprPanic "shortCutReduction" (ppr old_ev)
2019
2020 ; let new_ct = CFunEqCan { cc_ev = new_ev, cc_fun = fam_tc
2021 , cc_tyargs = tc_args, cc_fsk = fsk }
2022 ; updWorkListTcS (extendWorkListFunEq new_ct) }
2023 where
2024 deeper_loc = bumpCtLocDepth (ctEvLoc old_ev)
2025
2026 {- Note [Top-level reductions for type functions]
2027 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2028 c.f. Note [The flattening story] in TcFlatten
2029
2030 Suppose we have a CFunEqCan F tys ~ fmv/fsk, and a matching axiom.
2031 Here is what we do, in four cases:
2032
2033 * Wanteds: general firing rule
2034 (work item) [W] x : F tys ~ fmv
2035 instantiate axiom: ax_co : F tys ~ rhs
2036
2037 Then:
2038 Discharge fmv := rhs
2039 Discharge x := ax_co ; sym x2
2040 This is *the* way that fmv's get unified; even though they are
2041 "untouchable".
2042
2043 NB: Given Note [FunEq occurs-check principle], fmv does not appear
2044 in tys, and hence does not appear in the instantiated RHS. So
2045 the unification can't make an infinite type.
2046
2047 * Wanteds: short cut firing rule
2048 Applies when the RHS of the axiom is another type-function application
2049 (work item) [W] x : F tys ~ fmv
2050 instantiate axiom: ax_co : F tys ~ G rhs_tys
2051
2052 It would be a waste to create yet another fmv for (G rhs_tys).
2053 Instead (shortCutReduction):
2054 - Flatten rhs_tys (cos : rhs_tys ~ rhs_xis)
2055 - Add G rhs_xis ~ fmv to flat cache (note: the same old fmv)
2056 - New canonical wanted [W] x2 : G rhs_xis ~ fmv (CFunEqCan)
2057 - Discharge x := ax_co ; G cos ; x2
2058
2059 * Givens: general firing rule
2060 (work item) [G] g : F tys ~ fsk
2061 instantiate axiom: ax_co : F tys ~ rhs
2062
2063 Now add non-canonical given (since rhs is not flat)
2064 [G] (sym g ; ax_co) : fsk ~ rhs (Non-canonical)
2065
2066 * Givens: short cut firing rule
2067 Applies when the RHS of the axiom is another type-function application
2068 (work item) [G] g : F tys ~ fsk
2069 instantiate axiom: ax_co : F tys ~ G rhs_tys
2070
2071 It would be a waste to create yet another fsk for (G rhs_tys).
2072 Instead (shortCutReduction):
2073 - Flatten rhs_tys: flat_cos : tys ~ flat_tys
2074 - Add new Canonical given
2075 [G] (sym (G flat_cos) ; co ; g) : G flat_tys ~ fsk (CFunEqCan)
2076
2077 Note [FunEq occurs-check principle]
2078 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2079 I have spent a lot of time finding a good way to deal with
2080 CFunEqCan constraints like
2081 F (fuv, a) ~ fuv
2082 where flatten-skolem occurs on the LHS. Now in principle we
2083 might may progress by doing a reduction, but in practice its
2084 hard to find examples where it is useful, and easy to find examples
2085 where we fall into an infinite reduction loop. A rule that works
2086 very well is this:
2087
2088 *** FunEq occurs-check principle ***
2089
2090 Do not reduce a CFunEqCan
2091 F tys ~ fsk
2092 if fsk appears free in tys
2093 Instead we treat it as stuck.
2094
2095 Examples:
2096
2097 * Trac #5837 has [G] a ~ TF (a,Int), with an instance
2098 type instance TF (a,b) = (TF a, TF b)
2099 This readily loops when solving givens. But with the FunEq occurs
2100 check principle, it rapidly gets stuck which is fine.
2101
2102 * Trac #12444 is a good example, explained in comment:2. We have
2103 type instance F (Succ x) = Succ (F x)
2104 [W] alpha ~ Succ (F alpha)
2105 If we allow the reduction to happen, we get an infinite loop
2106
2107 Note [Cached solved FunEqs]
2108 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
2109 When trying to solve, say (FunExpensive big-type ~ ty), it's important
2110 to see if we have reduced (FunExpensive big-type) before, lest we
2111 simply repeat it. Hence the lookup in inert_solved_funeqs. Moreover
2112 we must use `funEqCanDischarge` because both uses might (say) be Wanteds,
2113 and we *still* want to save the re-computation.
2114
2115 Note [MATCHING-SYNONYMS]
2116 ~~~~~~~~~~~~~~~~~~~~~~~~
2117 When trying to match a dictionary (D tau) to a top-level instance, or a
2118 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
2119 we do *not* need to expand type synonyms because the matcher will do that for us.
2120
2121 Note [Improvement orientation]
2122 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2123 A very delicate point is the orientation of derived equalities
2124 arising from injectivity improvement (Trac #12522). Suppse we have
2125 type family F x = t | t -> x
2126 type instance F (a, Int) = (Int, G a)
2127 where G is injective; and wanted constraints
2128
2129 [W] TF (alpha, beta) ~ fuv
2130 [W] fuv ~ (Int, <some type>)
2131
2132 The injectivity will give rise to derived constraints
2133
2134 [D] gamma1 ~ alpha
2135 [D] Int ~ beta
2136
2137 The fresh unification variable gamma1 comes from the fact that we
2138 can only do "partial improvement" here; see Section 5.2 of
2139 "Injective type families for Haskell" (HS'15).
2140
2141 Now, it's very important to orient the equations this way round,
2142 so that the fresh unification variable will be eliminated in
2143 favour of alpha. If we instead had
2144 [D] alpha ~ gamma1
2145 then we would unify alpha := gamma1; and kick out the wanted
2146 constraint. But when we grough it back in, it'd look like
2147 [W] TF (gamma1, beta) ~ fuv
2148 and exactly the same thing would happen again! Infinite loop.
2149
2150 This all seems fragile, and it might seem more robust to avoid
2151 introducing gamma1 in the first place, in the case where the
2152 actual argument (alpha, beta) partly matches the improvement
2153 template. But that's a bit tricky, esp when we remember that the
2154 kinds much match too; so it's easier to let the normal machinery
2155 handle it. Instead we are careful to orient the new derived
2156 equality with the template on the left. Delicate, but it works.
2157
2158 Note [No FunEq improvement for Givens]
2159 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2160 We don't do improvements (injectivity etc) for Givens. Why?
2161
2162 * It generates Derived constraints on skolems, which don't do us
2163 much good, except perhaps identify inaccessible branches.
2164 (They'd be perfectly valid though.)
2165
2166 * For type-nat stuff the derived constraints include type families;
2167 e.g. (a < b), (b < c) ==> a < c If we generate a Derived for this,
2168 we'll generate a Derived/Wanted CFunEqCan; and, since the same
2169 InertCans (after solving Givens) are used for each iteration, that
2170 massively confused the unflattening step (TcFlatten.unflatten).
2171
2172 In fact it led to some infinite loops:
2173 indexed-types/should_compile/T10806
2174 indexed-types/should_compile/T10507
2175 polykinds/T10742
2176
2177 Note [Reduction for Derived CFunEqCans]
2178 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2179 You may wonder if it's important to use top-level instances to
2180 simplify [D] CFunEqCan's. But it is. Here's an example (T10226).
2181
2182 type instance F Int = Int
2183 type instance FInv Int = Int
2184
2185 Suppose we have to solve
2186 [WD] FInv (F alpha) ~ alpha
2187 [WD] F alpha ~ Int
2188
2189 --> flatten
2190 [WD] F alpha ~ fuv0
2191 [WD] FInv fuv0 ~ fuv1 -- (A)
2192 [WD] fuv1 ~ alpha
2193 [WD] fuv0 ~ Int -- (B)
2194
2195 --> Rewwrite (A) with (B), splitting it
2196 [WD] F alpha ~ fuv0
2197 [W] FInv fuv0 ~ fuv1
2198 [D] FInv Int ~ fuv1 -- (C)
2199 [WD] fuv1 ~ alpha
2200 [WD] fuv0 ~ Int
2201
2202 --> Reduce (C) with top-level instance
2203 **** This is the key step ***
2204 [WD] F alpha ~ fuv0
2205 [W] FInv fuv0 ~ fuv1
2206 [D] fuv1 ~ Int -- (D)
2207 [WD] fuv1 ~ alpha -- (E)
2208 [WD] fuv0 ~ Int
2209
2210 --> Rewrite (D) with (E)
2211 [WD] F alpha ~ fuv0
2212 [W] FInv fuv0 ~ fuv1
2213 [D] alpha ~ Int -- (F)
2214 [WD] fuv1 ~ alpha
2215 [WD] fuv0 ~ Int
2216
2217 --> unify (F) alpha := Int, and that solves it
2218
2219 Another example is indexed-types/should_compile/T10634
2220 -}
2221
2222 {- *******************************************************************
2223 * *
2224 Top-level reaction for class constraints (CDictCan)
2225 * *
2226 **********************************************************************-}
2227
2228 doTopReactDict :: InertSet -> Ct -> TcS (StopOrContinue Ct)
2229 -- Try to use type-class instance declarations to simplify the constraint
2230 doTopReactDict inerts work_item@(CDictCan { cc_ev = fl, cc_class = cls
2231 , cc_tyargs = xis })
2232 | isGiven fl -- Never use instances for Given constraints
2233 = do { try_fundep_improvement
2234 ; continueWith work_item }
2235
2236 | Just ev <- lookupSolvedDict inerts dict_loc cls xis -- Cached
2237 = do { setEvBindIfWanted fl (ctEvExpr ev)
2238 ; stopWith fl "Dict/Top (cached)" }
2239
2240 | otherwise -- Wanted or Derived, but not cached
2241 = do { dflags <- getDynFlags
2242 ; lkup_inst_res <- matchClassInst dflags inerts cls xis dict_loc
2243 ; case lkup_inst_res of
2244 GenInst { lir_new_theta = theta
2245 , lir_mk_ev = mk_ev
2246 , lir_safe_over = s } ->
2247 do { traceTcS "doTopReact/found instance for" $ ppr fl
2248 ; checkReductionDepth deeper_loc dict_pred
2249 ; unless s $ insertSafeOverlapFailureTcS work_item
2250 ; if isDerived fl then finish_derived theta
2251 else finish_wanted theta mk_ev }
2252 NoInstance ->
2253 do { when (isImprovable fl) $
2254 try_fundep_improvement
2255 ; continueWith work_item } }
2256 where
2257 dict_pred = mkClassPred cls xis
2258 dict_loc = ctEvLoc fl
2259 dict_origin = ctLocOrigin dict_loc
2260 deeper_loc = zap_origin (bumpCtLocDepth dict_loc)
2261
2262 zap_origin loc -- After applying an instance we can set ScOrigin to
2263 -- infinity, so that prohibitedSuperClassSolve never fires
2264 | ScOrigin {} <- dict_origin
2265 = setCtLocOrigin loc (ScOrigin infinity)
2266 | otherwise
2267 = loc
2268
2269 finish_wanted :: [TcPredType]
2270 -> ([EvExpr] -> EvTerm) -> TcS (StopOrContinue Ct)
2271 -- Precondition: evidence term matches the predicate workItem
2272 finish_wanted theta mk_ev
2273 = do { addSolvedDict fl cls xis
2274 ; evc_vars <- mapM (newWanted deeper_loc) theta
2275 ; setWantedEvBind (ctEvEvId fl) (mk_ev (map getEvExpr evc_vars))
2276 ; emitWorkNC (freshGoals evc_vars)
2277 ; stopWith fl "Dict/Top (solved wanted)" }
2278
2279 finish_derived theta -- Use type-class instances for Deriveds, in the hope
2280 = -- of generating some improvements
2281 -- C.f. Example 3 of Note [The improvement story]
2282 -- It's easy because no evidence is involved
2283 do { emitNewDeriveds deeper_loc theta
2284 ; traceTcS "finish_derived" (ppr (ctl_depth deeper_loc))
2285 ; stopWith fl "Dict/Top (solved derived)" }
2286
2287 -- We didn't solve it; so try functional dependencies with
2288 -- the instance environment, and return
2289 -- See also Note [Weird fundeps]
2290 try_fundep_improvement
2291 = do { traceTcS "try_fundeps" (ppr work_item)
2292 ; instEnvs <- getInstEnvs
2293 ; emitFunDepDeriveds $
2294 improveFromInstEnv instEnvs mk_ct_loc dict_pred }
2295
2296 mk_ct_loc :: PredType -- From instance decl
2297 -> SrcSpan -- also from instance deol
2298 -> CtLoc
2299 mk_ct_loc inst_pred inst_loc
2300 = dict_loc { ctl_origin = FunDepOrigin2 dict_pred dict_origin
2301 inst_pred inst_loc }
2302
2303 doTopReactDict _ w = pprPanic "doTopReactDict" (ppr w)
2304
2305
2306 {- *******************************************************************
2307 * *
2308 Class lookup
2309 * *
2310 **********************************************************************-}
2311
2312 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
2313 -- check.
2314 --
2315 -- See Note [Safe Haskell Overlapping Instances] in TcSimplify
2316 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
2317 type SafeOverlapping = Bool
2318
2319 data LookupInstResult
2320 = NoInstance
2321 | GenInst { lir_new_theta :: [TcPredType]
2322 , lir_mk_ev :: [EvExpr] -> EvTerm
2323 , lir_safe_over :: SafeOverlapping }
2324
2325 instance Outputable LookupInstResult where
2326 ppr NoInstance = text "NoInstance"
2327 ppr (GenInst { lir_new_theta = ev
2328 , lir_safe_over = s })
2329 = text "GenInst" <+> vcat [ppr ev, ss]
2330 where ss = text $ if s then "[safe]" else "[unsafe]"
2331
2332
2333 matchClassInst :: DynFlags -> InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
2334 matchClassInst dflags inerts clas tys loc
2335 -- First check whether there is an in-scope Given that could
2336 -- match this constraint. In that case, do not use top-level
2337 -- instances. See Note [Instance and Given overlap]
2338 | not (xopt LangExt.IncoherentInstances dflags)
2339 , not (naturallyCoherentClass clas)
2340 , let matchable_givens = matchableGivens loc pred inerts
2341 , not (isEmptyBag matchable_givens)
2342 = do { traceTcS "Delaying instance application" $
2343 vcat [ text "Work item=" <+> pprClassPred clas tys
2344 , text "Potential matching givens:" <+> ppr matchable_givens ]
2345 ; return NoInstance }
2346 where
2347 pred = mkClassPred clas tys
2348
2349 matchClassInst dflags _ clas tys loc
2350 = do { traceTcS "matchClassInst" $ text "pred =" <+> ppr (mkClassPred clas tys) <+> char '{'
2351 ; res <- match_class_inst dflags False clas tys loc
2352 ; traceTcS "} matchClassInst result" $ ppr res
2353 ; return res }
2354
2355 match_class_inst :: DynFlags
2356 -> Bool -- True <=> caller is the short-cut solver
2357 -- See Note [Shortcut solving: overlap]
2358 -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
2359 match_class_inst dflags short_cut clas tys loc
2360 | cls_name == knownNatClassName = matchKnownNat clas tys
2361 | cls_name == knownSymbolClassName = matchKnownSymbol clas tys
2362 | isCTupleClass clas = matchCTuple clas tys
2363 | cls_name == typeableClassName = matchTypeable clas tys
2364 | clas `hasKey` heqTyConKey = matchLiftedEquality tys
2365 | clas `hasKey` coercibleTyConKey = matchLiftedCoercible tys
2366 | cls_name == hasFieldClassName = matchHasField dflags short_cut clas tys loc
2367 | otherwise = matchInstEnv dflags short_cut clas tys loc
2368 where
2369 cls_name = className clas
2370
2371 -- | If a class is "naturally coherent", then we needn't worry at all, in any
2372 -- way, about overlapping/incoherent instances. Just solve the thing!
2373 -- See Note [Naturally coherent classes]
2374 -- See also Note [The equality class story] in TysPrim.
2375 naturallyCoherentClass :: Class -> Bool
2376 naturallyCoherentClass cls
2377 = isCTupleClass cls
2378 || cls `hasKey` heqTyConKey
2379 || cls `hasKey` eqTyConKey
2380 || cls `hasKey` coercibleTyConKey
2381
2382 {- Note [Instance and Given overlap]
2383 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2384 Example, from the OutsideIn(X) paper:
2385 instance P x => Q [x]
2386 instance (x ~ y) => R y [x]
2387
2388 wob :: forall a b. (Q [b], R b a) => a -> Int
2389
2390 g :: forall a. Q [a] => [a] -> Int
2391 g x = wob x
2392
2393 From 'g' we get the impliation constraint:
2394 forall a. Q [a] => (Q [beta], R beta [a])
2395 If we react (Q [beta]) with its top-level axiom, we end up with a
2396 (P beta), which we have no way of discharging. On the other hand,
2397 if we react R beta [a] with the top-level we get (beta ~ a), which
2398 is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
2399 now solvable by the given Q [a].
2400
2401 The partial solution is that:
2402 In matchClassInst (and thus in topReact), we return a matching
2403 instance only when there is no Given in the inerts which is
2404 unifiable to this particular dictionary.
2405
2406 We treat any meta-tyvar as "unifiable" for this purpose,
2407 *including* untouchable ones. But not skolems like 'a' in
2408 the implication constraint above.
2409
2410 The end effect is that, much as we do for overlapping instances, we
2411 delay choosing a class instance if there is a possibility of another
2412 instance OR a given to match our constraint later on. This fixes
2413 Trac #4981 and #5002.
2414
2415 Other notes:
2416
2417 * The check is done *first*, so that it also covers classes
2418 with built-in instance solving, such as
2419 - constraint tuples
2420 - natural numbers
2421 - Typeable
2422
2423 * Flatten-skolems: we do not treat a flatten-skolem as unifiable
2424 for this purpose.
2425 E.g. f :: Eq (F a) => [a] -> [a]
2426 f xs = ....(xs==xs).....
2427 Here we get [W] Eq [a], and we don't want to refrain from solving
2428 it because of the given (Eq (F a)) constraint!
2429
2430 * The given-overlap problem is arguably not easy to appear in practice
2431 due to our aggressive prioritization of equality solving over other
2432 constraints, but it is possible. I've added a test case in
2433 typecheck/should-compile/GivenOverlapping.hs
2434
2435 * Another "live" example is Trac #10195; another is #10177.
2436
2437 * We ignore the overlap problem if -XIncoherentInstances is in force:
2438 see Trac #6002 for a worked-out example where this makes a
2439 difference.
2440
2441 * Moreover notice that our goals here are different than the goals of
2442 the top-level overlapping checks. There we are interested in
2443 validating the following principle:
2444
2445 If we inline a function f at a site where the same global
2446 instance environment is available as the instance environment at
2447 the definition site of f then we should get the same behaviour.
2448
2449 But for the Given Overlap check our goal is just related to completeness of
2450 constraint solving.
2451
2452 * The solution is only a partial one. Consider the above example with
2453 g :: forall a. Q [a] => [a] -> Int
2454 g x = let v = wob x
2455 in v
2456 and suppose we have -XNoMonoLocalBinds, so that we attempt to find the most
2457 general type for 'v'. When generalising v's type we'll simplify its
2458 Q [alpha] constraint, but we don't have Q [a] in the 'givens', so we
2459 will use the instance declaration after all. Trac #11948 was a case
2460 in point.
2461
2462 All of this is disgustingly delicate, so to discourage people from writing
2463 simplifiable class givens, we warn about signatures that contain them;
2464 see TcValidity Note [Simplifiable given constraints].
2465
2466 Note [Naturally coherent classes]
2467 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2468 A few built-in classes are "naturally coherent". This term means that
2469 the "instance" for the class is bidirectional with its superclass(es).
2470 For example, consider (~~), which behaves as if it was defined like
2471 this:
2472 class a ~# b => a ~~ b
2473 instance a ~# b => a ~~ b
2474 (See Note [The equality types story] in TysPrim.)
2475
2476 Faced with [W] t1 ~~ t2, it's always OK to reduce it to [W] t1 ~# t2,
2477 without worrying about Note [Instance and Given overlap]. Why? Because
2478 if we had [G] s1 ~~ s2, then we'd get the superclass [G] s1 ~# s2, and
2479 so the reduction of the [W] constraint does not risk losing any solutions.
2480
2481 On the other hand, it can be fatal to /fail/ to reduce such
2482 equalities, on the grounds of Note [Instance and Given overlap],
2483 because many good things flow from [W] t1 ~# t2.
2484
2485 The same reasoning applies to
2486
2487 * (~~) heqTyCOn
2488 * (~) eqTyCon
2489 * Coercible coercibleTyCon
2490
2491 And less obviously to:
2492
2493 * Tuple classes. For reasons described in TcSMonad
2494 Note [Tuples hiding implicit parameters], we may have a constraint
2495 [W] (?x::Int, C a)
2496 with an exactly-matching Given constraint. We must decompose this
2497 tuple and solve the components separately, otherwise we won't solve
2498 it at all! It is perfectly safe to decompose it, because again the
2499 superclasses invert the instance; e.g.
2500 class (c1, c2) => (% c1, c2 %)
2501 instance (c1, c2) => (% c1, c2 %)
2502 Example in Trac #14218
2503
2504 Exammples: T5853, T10432, T5315, T9222, T2627b, T3028b
2505
2506 PS: the term "naturally coherent" doesn't really seem helpful.
2507 Perhaps "invertible" or something? I left it for now though.
2508 -}
2509
2510
2511 {- *******************************************************************
2512 * *
2513 Class lookup in the instance environment
2514 * *
2515 **********************************************************************-}
2516
2517 matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
2518 matchInstEnv dflags short_cut_solver clas tys loc
2519 = do { instEnvs <- getInstEnvs
2520 ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
2521 (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
2522 safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
2523 ; case (matches, unify, safeHaskFail) of
2524
2525 -- Nothing matches
2526 ([], _, _)
2527 -> do { traceTcS "matchClass not matching" (ppr pred)
2528 ; return NoInstance }
2529
2530 -- A single match (& no safe haskell failure)
2531 ([(ispec, inst_tys)], [], False)
2532 | short_cut_solver
2533 , isOverlappable ispec
2534 -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
2535 -- then don't let the short-cut solver choose it, because a
2536 -- later instance might overlap it. Trac #14434 is an example
2537 -- See Note [Shortcut solving: overlap]
2538 -> do { traceTcS "matchClass: ingnoring overlappable" (ppr pred)
2539 ; return NoInstance }
2540
2541 | otherwise
2542 -> do { let dfun_id = instanceDFunId ispec
2543 ; traceTcS "matchClass success" $
2544 vcat [text "dict" <+> ppr pred,
2545 text "witness" <+> ppr dfun_id
2546 <+> ppr (idType dfun_id) ]
2547 -- Record that this dfun is needed
2548 ; match_one (null unsafeOverlaps) dfun_id inst_tys }
2549
2550 -- More than one matches (or Safe Haskell fail!). Defer any
2551 -- reactions of a multitude until we learn more about the reagent
2552 (matches, _, _)
2553 -> do { traceTcS "matchClass multiple matches, deferring choice" $
2554 vcat [text "dict" <+> ppr pred,
2555 text "matches" <+> ppr matches]
2556 ; return NoInstance } }
2557 where
2558 pred = mkClassPred clas tys
2559
2560 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcS LookupInstResult
2561 -- See Note [DFunInstType: instantiating types] in InstEnv
2562 match_one so dfun_id mb_inst_tys
2563 = do { checkWellStagedDFun pred dfun_id loc
2564 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
2565 ; return $ GenInst { lir_new_theta = theta
2566 , lir_mk_ev = EvExpr . evDFunApp dfun_id tys
2567 , lir_safe_over = so } }
2568
2569
2570 {- ********************************************************************
2571 * *
2572 Class lookup for CTuples
2573 * *
2574 ***********************************************************************-}
2575
2576 matchCTuple :: Class -> [Type] -> TcS LookupInstResult
2577 matchCTuple clas tys -- (isCTupleClass clas) holds
2578 = return (GenInst { lir_new_theta = tys
2579 , lir_mk_ev = tuple_ev
2580 , lir_safe_over = True })
2581 -- The dfun *is* the data constructor!
2582 where
2583 data_con = tyConSingleDataCon (classTyCon clas)
2584 tuple_ev = EvExpr . evDFunApp (dataConWrapId data_con) tys
2585
2586 {- ********************************************************************
2587 * *
2588 Class lookup for Literals
2589 * *
2590 ***********************************************************************-}
2591
2592 {-
2593 Note [KnownNat & KnownSymbol and EvLit]
2594 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2595 A part of the type-level literals implementation are the classes
2596 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
2597 defining singleton values. Here is the key stuff from GHC.TypeLits
2598
2599 class KnownNat (n :: Nat) where
2600 natSing :: SNat n
2601
2602 newtype SNat (n :: Nat) = SNat Integer
2603
2604 Conceptually, this class has infinitely many instances:
2605
2606 instance KnownNat 0 where natSing = SNat 0
2607 instance KnownNat 1 where natSing = SNat 1
2608 instance KnownNat 2 where natSing = SNat 2
2609 ...
2610
2611 In practice, we solve `KnownNat` predicates in the type-checker
2612 (see typecheck/TcInteract.hs) because we can't have infinitely many instances.
2613 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
2614
2615 We make the following assumptions about dictionaries in GHC:
2616 1. The "dictionary" for classes with a single method---like `KnownNat`---is
2617 a newtype for the type of the method, so using a evidence amounts
2618 to a coercion, and
2619 2. Newtypes use the same representation as their definition types.
2620
2621 So, the evidence for `KnownNat` is just a value of the representation type,
2622 wrapped in two newtype constructors: one to make it into a `SNat` value,
2623 and another to make it into a `KnownNat` dictionary.
2624
2625 Also note that `natSing` and `SNat` are never actually exposed from the
2626 library---they are just an implementation detail. Instead, users see
2627 a more convenient function, defined in terms of `natSing`:
2628
2629 natVal :: KnownNat n => proxy n -> Integer
2630
2631 The reason we don't use this directly in the class is that it is simpler
2632 and more efficient to pass around an integer rather than an entire function,
2633 especially when the `KnowNat` evidence is packaged up in an existential.
2634
2635 The story for kind `Symbol` is analogous:
2636 * class KnownSymbol
2637 * newtype SSymbol
2638 * Evidence: a Core literal (e.g. mkNaturalExpr)
2639 -}
2640
2641 matchKnownNat :: Class -> [Type] -> TcS LookupInstResult
2642 matchKnownNat clas [ty] -- clas = KnownNat
2643 | Just n <- isNumLitTy ty = do
2644 et <- mkNaturalExpr n
2645 makeLitDict clas ty et
2646 matchKnownNat _ _ = return NoInstance
2647
2648 matchKnownSymbol :: Class -> [Type] -> TcS LookupInstResult
2649 matchKnownSymbol clas [ty] -- clas = KnownSymbol
2650 | Just s <- isStrLitTy ty = do
2651 et <- mkStringExprFS s
2652 makeLitDict clas ty et
2653 matchKnownSymbol _ _ = return NoInstance
2654
2655 makeLitDict :: Class -> Type -> EvExpr -> TcS LookupInstResult
2656 -- makeLitDict adds a coercion that will convert the literal into a dictionary
2657 -- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
2658 -- in TcEvidence. The coercion happens in 2 steps:
2659 --
2660 -- Integer -> SNat n -- representation of literal to singleton
2661 -- SNat n -> KnownNat n -- singleton to dictionary
2662 --
2663 -- The process is mirrored for Symbols:
2664 -- String -> SSymbol n
2665 -- SSymbol n -> KnownSymbol n
2666 makeLitDict clas ty et
2667 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
2668 -- co_dict :: KnownNat n ~ SNat n
2669 , [ meth ] <- classMethods clas
2670 , Just tcRep <- tyConAppTyCon_maybe -- SNat
2671 $ funResultTy -- SNat n
2672 $ dropForAlls -- KnownNat n => SNat n
2673 $ idType meth -- forall n. KnownNat n => SNat n
2674 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
2675 -- SNat n ~ Integer
2676 , let ev_tm = EvExpr $ mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
2677 = return $ GenInst { lir_new_theta = []
2678 , lir_mk_ev = \_ -> ev_tm
2679 , lir_safe_over = True }
2680
2681 | otherwise
2682 = panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
2683 $$ vcat (map (ppr . idType) (classMethods clas)))
2684
2685 {- ********************************************************************
2686 * *
2687 Class lookup for Typeable
2688 * *
2689 ***********************************************************************-}
2690
2691 -- | Assumes that we've checked that this is the 'Typeable' class,
2692 -- and it was applied to the correct argument.
2693 matchTypeable :: Class -> [Type] -> TcS LookupInstResult
2694 matchTypeable clas [k,t] -- clas = Typeable
2695 -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
2696 | isForAllTy k = return NoInstance -- Polytype
2697 | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type
2698
2699 -- Now cases that do work
2700 | k `eqType` typeNatKind = doTyLit knownNatClassName t
2701 | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t
2702 | isConstraintKind t = doTyConApp clas t constraintKindTyCon []
2703 | Just (arg,ret) <- splitFunTy_maybe t = doFunTy clas t arg ret
2704 | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
2705 , onlyNamedBndrsApplied tc ks = doTyConApp clas t tc ks
2706 | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt
2707
2708 matchTypeable _ _ = return NoInstance
2709
2710 -- | Representation for a type @ty@ of the form @arg -> ret@.
2711 doFunTy :: Class -> Type -> Type -> Type -> TcS LookupInstResult
2712 doFunTy clas ty arg_ty ret_ty
2713 = do { let preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
2714 build_ev [arg_ev, ret_ev] =
2715 evTypeable ty $ EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
2716 build_ev _ = panic "TcInteract.doFunTy"
2717 ; return $ GenInst preds build_ev True
2718 }
2719
2720 -- | Representation for type constructor applied to some kinds.
2721 -- 'onlyNamedBndrsApplied' has ensured that this application results in a type
2722 -- of monomorphic kind (e.g. all kind variables have been instantiated).
2723 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcS LookupInstResult
2724 doTyConApp clas ty tc kind_args
2725 | Just _ <- tyConRepName_maybe tc
2726 = return $ GenInst (map (mk_typeable_pred clas) kind_args)
2727 (\kinds -> evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds))
2728 True
2729 | otherwise
2730 = return NoInstance
2731
2732 -- | Representation for TyCon applications of a concrete kind. We just use the
2733 -- kind itself, but first we must make sure that we've instantiated all kind-
2734 -- polymorphism, but no more.
2735 onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
2736 onlyNamedBndrsApplied tc ks
2737 = all isNamedTyConBinder used_bndrs &&
2738 not (any isNamedTyConBinder leftover_bndrs)
2739 where
2740 bndrs = tyConBinders tc
2741 (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
2742
2743 doTyApp :: Class -> Type -> Type -> KindOrType -> TcS LookupInstResult
2744 -- Representation for an application of a type to a type-or-kind.
2745 -- This may happen when the type expression starts with a type variable.
2746 -- Example (ignoring kind parameter):
2747 -- Typeable (f Int Char) -->
2748 -- (Typeable (f Int), Typeable Char) -->
2749 -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
2750 -- Typeable f
2751 doTyApp clas ty f tk
2752 | isForAllTy (typeKind f)
2753 = return NoInstance -- We can't solve until we know the ctr.
2754 | otherwise
2755 = return $ GenInst (map (mk_typeable_pred clas) [f, tk])
2756 (\[t1,t2] -> evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2))
2757 True
2758
2759 -- Emit a `Typeable` constraint for the given type.
2760 mk_typeable_pred :: Class -> Type -> PredType
2761 mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
2762
2763 -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
2764 -- we generate a sub-goal for the appropriate class. See #10348 for what
2765 -- happens when we fail to do this.
2766 doTyLit :: Name -> Type -> TcS LookupInstResult
2767 doTyLit kc t = do { kc_clas <- tcLookupClass kc
2768 ; let kc_pred = mkClassPred kc_clas [ t ]
2769 mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
2770 mk_ev _ = panic "doTyLit"
2771 ; return (GenInst [kc_pred] mk_ev True) }
2772
2773 {- Note [Typeable (T a b c)]
2774 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2775 For type applications we always decompose using binary application,
2776 via doTyApp, until we get to a *kind* instantiation. Example
2777 Proxy :: forall k. k -> *
2778
2779 To solve Typeable (Proxy (* -> *) Maybe) we
2780 - First decompose with doTyApp,
2781 to get (Typeable (Proxy (* -> *))) and Typeable Maybe
2782 - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
2783
2784 If we attempt to short-cut by solving it all at once, via
2785 doTyConApp
2786
2787 (this note is sadly truncated FIXME)
2788
2789
2790 Note [No Typeable for polytypes or qualified types]
2791 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2792 We do not support impredicative typeable, such as
2793 Typeable (forall a. a->a)
2794 Typeable (Eq a => a -> a)
2795 Typeable (() => Int)
2796 Typeable (((),()) => Int)
2797
2798 See Trac #9858. For forall's the case is clear: we simply don't have
2799 a TypeRep for them. For qualified but not polymorphic types, like
2800 (Eq a => a -> a), things are murkier. But:
2801
2802 * We don't need a TypeRep for these things. TypeReps are for
2803 monotypes only.
2804
2805 * Perhaps we could treat `=>` as another type constructor for `Typeable`
2806 purposes, and thus support things like `Eq Int => Int`, however,
2807 at the current state of affairs this would be an odd exception as
2808 no other class works with impredicative types.
2809 For now we leave it off, until we have a better story for impredicativity.
2810 -}
2811
2812 {- ********************************************************************
2813 * *
2814 Class lookup for lifted equality
2815 * *
2816 ***********************************************************************-}
2817
2818 -- See also Note [The equality types story] in TysPrim
2819 matchLiftedEquality :: [Type] -> TcS LookupInstResult
2820 matchLiftedEquality args
2821 = return (GenInst { lir_new_theta = [ mkTyConApp eqPrimTyCon args ]
2822 , lir_mk_ev = EvExpr . evDFunApp (dataConWrapId heqDataCon) args
2823 , lir_safe_over = True })
2824
2825 -- See also Note [The equality types story] in TysPrim
2826 matchLiftedCoercible :: [Type] -> TcS LookupInstResult
2827 matchLiftedCoercible args@[k, t1, t2]
2828 = return (GenInst { lir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
2829 , lir_mk_ev = EvExpr . evDFunApp (dataConWrapId coercibleDataCon)
2830 args
2831 , lir_safe_over = True })
2832 where
2833 args' = [k, k, t1, t2]
2834 matchLiftedCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
2835
2836
2837 {- ********************************************************************
2838 * *
2839 Class lookup for overloaded record fields
2840 * *
2841 ***********************************************************************-}
2842
2843 {-
2844 Note [HasField instances]
2845 ~~~~~~~~~~~~~~~~~~~~~~~~~
2846 Suppose we have
2847
2848 data T y = MkT { foo :: [y] }
2849
2850 and `foo` is in scope. Then GHC will automatically solve a constraint like
2851
2852 HasField "foo" (T Int) b
2853
2854 by emitting a new wanted
2855
2856 T alpha -> [alpha] ~# T Int -> b
2857
2858 and building a HasField dictionary out of the selector function `foo`,
2859 appropriately cast.
2860
2861 The HasField class is defined (in GHC.Records) thus:
2862
2863 class HasField (x :: k) r a | x r -> a where
2864 getField :: r -> a
2865
2866 Since this is a one-method class, it is represented as a newtype.
2867 Hence we can solve `HasField "foo" (T Int) b` by taking an expression
2868 of type `T Int -> b` and casting it using the newtype coercion.
2869 Note that
2870
2871 foo :: forall y . T y -> [y]
2872
2873 so the expression we construct is
2874
2875 foo @alpha |> co
2876
2877 where
2878
2879 co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b
2880
2881 is built from
2882
2883 co1 :: (T alpha -> [alpha]) ~# (T Int -> b)
2884
2885 which is the new wanted, and
2886
2887 co2 :: (T Int -> b) ~# HasField "foo" (T Int) b
2888
2889 which can be derived from the newtype coercion.
2890
2891 If `foo` is not in scope, or has a higher-rank or existentially
2892 quantified type, then the constraint is not solved automatically, but
2893 may be solved by a user-supplied HasField instance. Similarly, if we
2894 encounter a HasField constraint where the field is not a literal
2895 string, or does not belong to the type, then we fall back on the
2896 normal constraint solver behaviour.
2897 -}
2898
2899 -- See Note [HasField instances]
2900 matchHasField :: DynFlags -> Bool -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
2901 matchHasField dflags short_cut clas tys loc
2902 = do { fam_inst_envs <- getFamInstEnvs
2903 ; rdr_env <- getGlobalRdrEnvTcS
2904 ; case tys of
2905 -- We are matching HasField {k} x r a...
2906 [_k_ty, x_ty, r_ty, a_ty]
2907 -- x should be a literal string
2908 | Just x <- isStrLitTy x_ty
2909 -- r should be an applied type constructor
2910 , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
2911 -- use representation tycon (if data family); it has the fields
2912 , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
2913 -- x should be a field of r
2914 , Just fl <- lookupTyConFieldLabel x r_tc
2915 -- the field selector should be in scope
2916 , Just gre <- lookupGRE_FieldLabel rdr_env fl
2917
2918 -> do { sel_id <- tcLookupId (flSelector fl)
2919 ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id
2920
2921 -- The first new wanted constraint equates the actual
2922 -- type of the selector with the type (r -> a) within
2923 -- the HasField x r a dictionary. The preds will
2924 -- typically be empty, but if the datatype has a
2925 -- "stupid theta" then we have to include it here.
2926 ; let theta = mkPrimEqPred sel_ty (mkFunTy r_ty a_ty) : preds
2927
2928 -- Use the equality proof to cast the selector Id to
2929 -- type (r -> a), then use the newtype coercion to cast
2930 -- it to a HasField dictionary.
2931 mk_ev (ev1:evs) = EvExpr $ evSelector sel_id tvs evs `evCast` co
2932 where
2933 co = mkTcSubCo (evTermCoercion (EvExpr ev1))
2934 `mkTcTransCo` mkTcSymCo co2
2935 mk_ev [] = panic "matchHasField.mk_ev"
2936
2937 Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
2938 tys
2939
2940 tvs = mkTyVarTys (map snd tv_prs)
2941
2942 -- The selector must not be "naughty" (i.e. the field
2943 -- cannot have an existentially quantified type), and
2944 -- it must not be higher-rank.
2945 ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
2946 then do { addUsedGRE True gre
2947 ; return GenInst { lir_new_theta = theta
2948 , lir_mk_ev = mk_ev
2949 , lir_safe_over = True
2950 } }
2951 else matchInstEnv dflags short_cut clas tys loc }
2952
2953 _ -> matchInstEnv dflags short_cut clas tys loc }