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