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