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