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