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