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