compiler/typecheck/TcInteract.lhs

   1 \begin{code}
   2 module TcInteract (
   3      solveInteract, solveInteractGiven, solveInteractWanted,
   4      AtomicInert, tyVarsOfInert,
   5      InertSet, emptyInert, updInertSet, extractUnsolved, solveOne,
   6   ) where
   7
   8 #include "HsVersions.h"
   9
  10
  11 import BasicTypes
  12 import TcCanonical
  13 import VarSet
  14 import Type
  15 import Unify
  16
  17 import Id
  18 import Var
  19
  20 import TcType
  21 import HsBinds
  22
  23 import Inst( tyVarsOfEvVar )
  24 import Class
  25 import TyCon
  26 import Name
  27
  28 import FunDeps
  29
  30 import Coercion
  31 import Outputable
  32
  33 import TcRnTypes
  34 import TcMType ( isSilentEvVar )
  35 import TcErrors
  36 import TcSMonad
  37 import Bag
  38 import qualified Data.Map as Map
  39
  40 import Control.Monad( when )
  41
  42 import FastString ( sLit )
  43 import DynFlags
  44 \end{code}
  45
  46 Note [InertSet invariants]
  47 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
  48 An InertSet is a bag of canonical constraints, with the following invariants:
  49
  50   1 No two constraints react with each other.
  51
  52     A tricky case is when there exists a given (solved) dictionary
  53     constraint and a wanted identical constraint in the inert set, but do
  54     not react because reaction would create loopy dictionary evidence for
  55     the wanted. See note [Recursive dictionaries]
  56
  57   2 Given equalities form an idempotent substitution [none of the
  58     given LHS's occur in any of the given RHS's or reactant parts]
  59
  60   3 Wanted equalities also form an idempotent substitution
  61
  62   4 The entire set of equalities is acyclic.
  63
  64   5 Wanted dictionaries are inert with the top-level axiom set
  65
  66   6 Equalities of the form tv1 ~ tv2 always have a touchable variable
  67     on the left (if possible).
  68
  69   7 No wanted constraints tv1 ~ tv2 with tv1 touchable. Such constraints
  70     will be marked as solved right before being pushed into the inert set.
  71     See note [Touchables and givens].
  72
  73   8 No Given constraint mentions a touchable unification variable, but
  74     Given/Solved may do so.
  75
  76   9 Given constraints will also have their superclasses in the inert set,
  77     but Given/Solved will not.
  78
  79 Note that 6 and 7 are /not/ enforced by canonicalization but rather by
  80 insertion in the inert list, ie by TcInteract.
  81
  82 During the process of solving, the inert set will contain some
  83 previously given constraints, some wanted constraints, and some given
  84 constraints which have arisen from solving wanted constraints. For
  85 now we do not distinguish between given and solved constraints.
  86
  87 Note that we must switch wanted inert items to given when going under an
  88 implication constraint (when in top-level inference mode).
  89
  90 \begin{code}
  91
  92 data CCanMap a = CCanMap { cts_given   :: Map.Map a CanonicalCts
  93                                           -- Invariant: all Given
  94                          , cts_derived :: Map.Map a CanonicalCts
  95                                           -- Invariant: all Derived
  96                          , cts_wanted  :: Map.Map a CanonicalCts }
  97                                           -- Invariant: all Wanted
  98
  99 cCanMapToBag :: Ord a => CCanMap a -> CanonicalCts
 100 cCanMapToBag cmap = Map.fold unionBags rest_wder (cts_given cmap)
 101   where rest_wder = Map.fold unionBags rest_der  (cts_wanted cmap)
 102         rest_der  = Map.fold unionBags emptyCCan (cts_derived cmap)
 103
 104 emptyCCanMap :: CCanMap a
 105 emptyCCanMap = CCanMap { cts_given = Map.empty
 106                        , cts_derived = Map.empty, cts_wanted = Map.empty }
 107
 108 updCCanMap:: Ord a => (a,CanonicalCt) -> CCanMap a -> CCanMap a
 109 updCCanMap (a,ct) cmap
 110   = case cc_flavor ct of
 111       Wanted {}
 112           -> cmap { cts_wanted = Map.insertWith unionBags a this_ct (cts_wanted cmap) }
 113       Given {}
 114           -> cmap { cts_given = Map.insertWith unionBags a this_ct (cts_given cmap) }
 115       Derived {}
 116           -> cmap { cts_derived = Map.insertWith unionBags a this_ct (cts_derived cmap) }
 117   where this_ct = singleCCan ct
 118
 119 getRelevantCts :: Ord a => a -> CCanMap a -> (CanonicalCts, CCanMap a)
 120 -- Gets the relevant constraints and returns the rest of the CCanMap
 121 getRelevantCts a cmap
 122     = let relevant = unionManyBags [ Map.findWithDefault emptyCCan a (cts_wanted cmap)
 123                                    , Map.findWithDefault emptyCCan a (cts_given cmap)
 124                                    , Map.findWithDefault emptyCCan a (cts_derived cmap) ]
 125           residual_map = cmap { cts_wanted = Map.delete a (cts_wanted cmap)
 126                               , cts_given = Map.delete a (cts_given cmap)
 127                               , cts_derived = Map.delete a (cts_derived cmap) }
 128       in (relevant, residual_map)
 129
 130 extractUnsolvedCMap :: Ord a => CCanMap a -> (CanonicalCts, CCanMap a)
 131 -- Gets the wanted or derived constraints and returns a residual
 132 -- CCanMap with only givens.
 133 extractUnsolvedCMap cmap =
 134   let wntd = Map.fold unionBags emptyCCan (cts_wanted cmap)
 135       derd = Map.fold unionBags emptyCCan (cts_derived cmap)
 136   in (wntd `unionBags` derd,
 137            cmap { cts_wanted = Map.empty, cts_derived = Map.empty })
 138
 139
 140 -- See Note [InertSet invariants]
 141 data InertSet
 142   = IS { inert_eqs          :: CanonicalCts               -- Equalities only (CTyEqCan)
 143        , inert_dicts        :: CCanMap Class              -- Dictionaries only
 144        , inert_ips          :: CCanMap (IPName Name)      -- Implicit parameters
 145        , inert_frozen       :: CanonicalCts
 146        , inert_funeqs       :: CCanMap TyCon              -- Type family equalities only
 147                -- This representation allows us to quickly get to the relevant
 148                -- inert constraints when interacting a work item with the inert set.
 149        }
 150
 151 tyVarsOfInert :: InertSet -> TcTyVarSet
 152 tyVarsOfInert (IS { inert_eqs    = eqs
 153                   , inert_dicts  = dictmap
 154                   , inert_ips    = ipmap
 155                   , inert_frozen = frozen
 156                   , inert_funeqs = funeqmap }) = tyVarsOfCanonicals cts
 157   where
 158     cts = eqs `andCCan` frozen `andCCan` cCanMapToBag dictmap
 159               `andCCan` cCanMapToBag ipmap `andCCan` cCanMapToBag funeqmap
 160
 161 instance Outputable InertSet where
 162   ppr is = vcat [ vcat (map ppr (Bag.bagToList $ inert_eqs is))
 163                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_dicts is)))
 164                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_ips is)))
 165                 , vcat (map ppr (Bag.bagToList $ cCanMapToBag (inert_funeqs is)))
 166                 , text "Frozen errors =" <+> -- Clearly print frozen errors
 167                     vcat (map ppr (Bag.bagToList $ inert_frozen is))
 168                 ]
 169
 170 emptyInert :: InertSet
 171 emptyInert = IS { inert_eqs    = Bag.emptyBag
 172                 , inert_frozen = Bag.emptyBag
 173                 , inert_dicts  = emptyCCanMap
 174                 , inert_ips    = emptyCCanMap
 175                 , inert_funeqs = emptyCCanMap }
 176
 177 updInertSet :: InertSet -> AtomicInert -> InertSet
 178 updInertSet is item
 179   | isCTyEqCan item                     -- Other equality
 180   = let eqs' = inert_eqs is `Bag.snocBag` item
 181     in is { inert_eqs = eqs' }
 182   | Just cls <- isCDictCan_Maybe item   -- Dictionary
 183   = is { inert_dicts = updCCanMap (cls,item) (inert_dicts is) }
 184   | Just x  <- isCIPCan_Maybe item      -- IP
 185   = is { inert_ips   = updCCanMap (x,item) (inert_ips is) }
 186   | Just tc <- isCFunEqCan_Maybe item   -- Function equality
 187   = is { inert_funeqs = updCCanMap (tc,item) (inert_funeqs is) }
 188   | otherwise
 189   = is { inert_frozen = inert_frozen is `Bag.snocBag` item }
 190
 191 extractUnsolved :: InertSet -> (InertSet, CanonicalCts)
 192 -- Postcondition: the returned canonical cts are either Derived, or Wanted.
 193 extractUnsolved is@(IS {inert_eqs = eqs})
 194   = let is_solved  = is { inert_eqs    = solved_eqs
 195                         , inert_dicts  = solved_dicts
 196                         , inert_ips    = solved_ips
 197                         , inert_frozen = emptyCCan
 198                         , inert_funeqs = solved_funeqs }
 199     in (is_solved, unsolved)
 200
 201   where (unsolved_eqs, solved_eqs)       = Bag.partitionBag (not.isGivenOrSolvedCt) eqs
 202         (unsolved_ips, solved_ips)       = extractUnsolvedCMap (inert_ips is)
 203         (unsolved_dicts, solved_dicts)   = extractUnsolvedCMap (inert_dicts is)
 204         (unsolved_funeqs, solved_funeqs) = extractUnsolvedCMap (inert_funeqs is)
 205
 206         unsolved = unsolved_eqs `unionBags` inert_frozen is `unionBags`
 207                    unsolved_ips `unionBags` unsolved_dicts `unionBags` unsolved_funeqs
 208 \end{code}
 209
 210 %*********************************************************************
 211 %*                                                                   *
 212 *                      Main Interaction Solver                       *
 213 *                                                                    *
 214 **********************************************************************
 215
 216 Note [Basic plan]
 217 ~~~~~~~~~~~~~~~~~
 218 1. Canonicalise (unary)
 219 2. Pairwise interaction (binary)
 220     * Take one from work list
 221     * Try all pair-wise interactions with each constraint in inert
 222
 223    As an optimisation, we prioritize the equalities both in the
 224    worklist and in the inerts.
 225
 226 3. Try to solve spontaneously for equalities involving touchables
 227 4. Top-level interaction (binary wrt top-level)
 228    Superclass decomposition belongs in (4), see note [Superclasses]
 229
 230 \begin{code}
 231 type AtomicInert = CanonicalCt     -- constraint pulled from InertSet
 232 type WorkItem    = CanonicalCt     -- constraint pulled from WorkList
 233
 234 ------------------------
 235 data StopOrContinue
 236   = Stop                        -- Work item is consumed
 237   | ContinueWith WorkItem       -- Not consumed
 238
 239 instance Outputable StopOrContinue where
 240   ppr Stop             = ptext (sLit "Stop")
 241   ppr (ContinueWith w) = ptext (sLit "ContinueWith") <+> ppr w
 242
 243 -- Results after interacting a WorkItem as far as possible with an InertSet
 244 data StageResult
 245   = SR { sr_inerts     :: InertSet
 246            -- The new InertSet to use (REPLACES the old InertSet)
 247        , sr_new_work   :: WorkList
 248            -- Any new work items generated (should be ADDED to the old WorkList)
 249            -- Invariant:
 250            --    sr_stop = Just workitem => workitem is *not* in sr_inerts and
 251            --                               workitem is inert wrt to sr_inerts
 252        , sr_stop       :: StopOrContinue
 253        }
 254
 255 instance Outputable StageResult where
 256   ppr (SR { sr_inerts = inerts, sr_new_work = work, sr_stop = stop })
 257     = ptext (sLit "SR") <+>
 258       braces (sep [ ptext (sLit "inerts =") <+> ppr inerts <> comma
 259                   , ptext (sLit "new work =") <+> ppr work <> comma
 260                   , ptext (sLit "stop =") <+> ppr stop])
 261
 262 type SubGoalDepth = Int   -- Starts at zero; used to limit infinite
 263                           -- recursion of sub-goals
 264 type SimplifierStage = SubGoalDepth -> WorkItem -> InertSet -> TcS StageResult
 265
 266 -- Combine a sequence of simplifier 'stages' to create a pipeline
 267 runSolverPipeline :: SubGoalDepth
 268                   -> [(String, SimplifierStage)]
 269                   -> InertSet -> WorkItem
 270                   -> TcS (InertSet, WorkList)
 271 -- Precondition: non-empty list of stages
 272 runSolverPipeline depth pipeline inerts workItem
 273   = do { traceTcS "Start solver pipeline" $
 274             vcat [ ptext (sLit "work item =") <+> ppr workItem
 275                  , ptext (sLit "inerts    =") <+> ppr inerts]
 276
 277        ; let itr_in = SR { sr_inerts = inerts
 278                          , sr_new_work = emptyWorkList
 279                          , sr_stop = ContinueWith workItem }
 280        ; itr_out <- run_pipeline pipeline itr_in
 281        ; let new_inert
 282               = case sr_stop itr_out of
 283                   Stop              -> sr_inerts itr_out
 284                   ContinueWith item -> sr_inerts itr_out `updInertSet` item
 285        ; return (new_inert, sr_new_work itr_out) }
 286   where
 287     run_pipeline :: [(String, SimplifierStage)]
 288                  -> StageResult -> TcS StageResult
 289     run_pipeline [] itr                         = return itr
 290     run_pipeline _  itr@(SR { sr_stop = Stop }) = return itr
 291
 292     run_pipeline ((name,stage):stages)
 293                  (SR { sr_new_work = accum_work
 294                      , sr_inerts   = inerts
 295                      , sr_stop     = ContinueWith work_item })
 296       = do { itr <- stage depth work_item inerts
 297            ; traceTcS ("Stage result (" ++ name ++ ")") (ppr itr)
 298            ; let itr' = itr { sr_new_work = accum_work `unionWorkList` sr_new_work itr }
 299            ; run_pipeline stages itr' }
 300 \end{code}
 301
 302 Example 1:
 303   Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
 304   Reagent: a ~ [b] (given)
 305
 306 React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
 307 React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
 308 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []
 309
 310 Example 2:
 311   Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
 312   Reagent: a ~w [b]
 313
 314 React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
 315 React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
 316 etc.
 317
 318 Example 3:
 319   Inert:  {a ~ Int, F Int ~ b} (given)
 320   Reagent: F a ~ b (wanted)
 321
 322 React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
 323 React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing
 324
 325 \begin{code}
 326 -- Main interaction solver: we fully solve the worklist 'in one go',
 327 -- returning an extended inert set.
 328 --
 329 -- See Note [Touchables and givens].
 330 solveInteractGiven :: InertSet -> GivenLoc -> [EvVar] -> TcS InertSet
 331 solveInteractGiven inert gloc evs
 332   = do { (_, inert_ret) <- solveInteract inert $ listToBag $
 333                            map mk_given evs
 334        ; return inert_ret }
 335   where
 336     flav = Given gloc GivenOrig
 337     mk_given ev = mkEvVarX ev flav
 338
 339 solveInteractWanted :: InertSet -> [WantedEvVar] -> TcS InertSet
 340 solveInteractWanted inert wvs
 341   = do { (_,inert_ret) <- solveInteract inert $ listToBag $
 342                           map wantedToFlavored wvs
 343        ; return inert_ret }
 344
 345 solveInteract :: InertSet -> Bag FlavoredEvVar -> TcS (Bool, InertSet)
 346 -- Post: (True,  inert_set) means we managed to discharge all constraints
 347 --                          without actually doing any interactions!
 348 --       (False, inert_set) means some interactions occurred
 349 solveInteract inert ws
 350   = do { dyn_flags <- getDynFlags
 351        ; sctx <- getTcSContext
 352
 353        ; traceTcS "solveInteract, before clever canonicalization:" $
 354          vcat [ text "ws = " <+>  ppr (mapBag (\(EvVarX ev ct)
 355                                                    -> (ct,evVarPred ev)) ws)
 356               , text "inert = " <+> ppr inert ]
 357
 358        ; can_ws <- mkCanonicalFEVs ws
 359
 360        ; (flag, inert_ret)
 361            <- foldrWorkListM (tryPreSolveAndInteract sctx dyn_flags) (True,inert) can_ws
 362
 363        ; traceTcS "solveInteract, after clever canonicalization (and interaction):" $
 364          vcat [ text "No interaction happened = " <+> ppr flag
 365               , text "inert_ret = " <+> ppr inert_ret ]
 366
 367        ; return (flag, inert_ret) }
 368
 369 tryPreSolveAndInteract :: SimplContext
 370                        -> DynFlags
 371                        -> CanonicalCt
 372                        -> (Bool, InertSet)
 373                        -> TcS (Bool, InertSet)
 374 -- Returns: True if it was able to discharge this constraint AND all previous ones
 375 tryPreSolveAndInteract sctx dyn_flags ct (all_previous_discharged, inert)
 376   = do { let inert_cts = get_inert_cts (evVarPred ev_var)
 377
 378        ; this_one_discharged <-
 379            if isCFrozenErr ct then
 380                return False
 381            else
 382                dischargeFromCCans inert_cts ev_var fl
 383
 384        ; if this_one_discharged
 385          then return (all_previous_discharged, inert)
 386
 387          else do
 388        { inert_ret <- solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) ct inert
 389        ; return (False, inert_ret) } }
 390
 391   where
 392     ev_var = cc_id ct
 393     fl = cc_flavor ct
 394
 395     get_inert_cts (ClassP clas _)
 396       | simplEqsOnly sctx = emptyCCan
 397       | otherwise         = fst (getRelevantCts clas (inert_dicts inert))
 398     get_inert_cts (IParam {})
 399       = emptyCCan -- We must not do the same thing for IParams, because (contrary
 400                   -- to dictionaries), work items /must/ override inert items.
 401                  -- See Note [Overriding implicit parameters] in TcInteract.
 402     get_inert_cts (EqPred {})
 403       = inert_eqs inert `unionBags` cCanMapToBag (inert_funeqs inert)
 404
 405 dischargeFromCCans :: CanonicalCts -> EvVar -> CtFlavor -> TcS Bool
 406 -- See if this (pre-canonicalised) work-item is identical to a
 407 -- one already in the inert set. Reasons:
 408 --    a) Avoid creating superclass constraints for millions of incoming (Num a) constraints
 409 --    b) Termination for improve_eqs in TcSimplify.simpl_loop
 410 dischargeFromCCans cans ev fl
 411   = Bag.foldrBag discharge_ct (return False) cans
 412   where
 413     the_pred = evVarPred ev
 414
 415     discharge_ct :: CanonicalCt -> TcS Bool -> TcS Bool
 416     discharge_ct ct _rest
 417       | evVarPred (cc_id ct) `eqPred` the_pred
 418       , cc_flavor ct `canSolve` fl
 419       = do { when (isWanted fl) $ setEvBind ev (evVarTerm (cc_id ct))
 420                  -- Deriveds need no evidence
 421                  -- For Givens, we already have evidence, and we don't need it twice
 422            ; return True }
 423
 424     discharge_ct _ct rest = rest
 425 \end{code}
 426
 427 Note [Avoiding the superclass explosion]
 428 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 429 This note now is not as significant as it used to be because we no
 430 longer add the superclasses of Wanted as Derived, except only if they
 431 have equality superclasses or superclasses with functional
 432 dependencies. The fear was that hundreds of identical wanteds would
 433 give rise each to the same superclass or equality Derived's which
 434 would lead to a blo-up in the number of interactions.
 435
 436 Instead, what we do with tryPreSolveAndCanon, is when we encounter a
 437 new constraint, we very quickly see if it can be immediately
 438 discharged by a class constraint in our inert set or the previous
 439 canonicals. If so, we add nothing to the returned canonical
 440 constraints.
 441
 442 \begin{code}
 443 solveOne :: WorkItem -> InertSet -> TcS InertSet
 444 solveOne workItem inerts
 445   = do { dyn_flags <- getDynFlags
 446        ; solveOneWithDepth (ctxtStkDepth dyn_flags,0,[]) workItem inerts
 447        }
 448
 449 -----------------
 450 solveInteractWithDepth :: (Int, Int, [WorkItem])
 451                        -> WorkList -> InertSet -> TcS InertSet
 452 solveInteractWithDepth ctxt@(max_depth,n,stack) ws inert
 453   | isEmptyWorkList ws
 454   = return inert
 455
 456   | n > max_depth
 457   = solverDepthErrorTcS n stack
 458
 459   | otherwise
 460   = do { traceTcS "solveInteractWithDepth" $
 461               vcat [ text "Current depth =" <+> ppr n
 462                    , text "Max depth =" <+> ppr max_depth
 463                    , text "ws =" <+> ppr ws ]
 464
 465
 466        ; foldrWorkListM (solveOneWithDepth ctxt) inert ws }
 467               -- use foldr to preserve the order
 468
 469 ------------------
 470 -- Fully interact the given work item with an inert set, and return a
 471 -- new inert set which has assimilated the new information.
 472 solveOneWithDepth :: (Int, Int, [WorkItem])
 473                   -> WorkItem -> InertSet -> TcS InertSet
 474 solveOneWithDepth (max_depth, depth, stack) work inert
 475   = do { traceFireTcS depth (text "Solving {" <+> ppr work)
 476        ; (new_inert, new_work) <- runSolverPipeline depth thePipeline inert work
 477
 478          -- Recursively solve the new work generated
 479          -- from workItem, with a greater depth
 480        ; res_inert <- solveInteractWithDepth (max_depth, depth+1, work:stack) new_work new_inert
 481
 482        ; traceFireTcS depth (text "Done }" <+> ppr work)
 483
 484        ; return res_inert }
 485
 486 thePipeline :: [(String,SimplifierStage)]
 487 thePipeline = [ ("interact with inert eqs", interactWithInertEqsStage)
 488               , ("interact with inerts",    interactWithInertsStage)
 489               , ("spontaneous solve",       spontaneousSolveStage)
 490               , ("top-level reactions",     topReactionsStage) ]
 491 \end{code}
 492
 493 *********************************************************************************
 494 *                                                                               *
 495                        The spontaneous-solve Stage
 496 *                                                                               *
 497 *********************************************************************************
 498
 499 Note [Efficient Orientation]
 500 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 501
 502 There are two cases where we have to be careful about
 503 orienting equalities to get better efficiency.
 504
 505 Case 1: In Rewriting Equalities (function rewriteEqLHS)
 506
 507     When rewriting two equalities with the same LHS:
 508           (a)  (tv ~ xi1)
 509           (b)  (tv ~ xi2)
 510     We have a choice of producing work (xi1 ~ xi2) (up-to the
 511     canonicalization invariants) However, to prevent the inert items
 512     from getting kicked out of the inerts first, we prefer to
 513     canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
 514     ~ xi1) if (a) comes from the inert set.
 515
 516     This choice is implemented using the WhichComesFromInert flag.
 517
 518 Case 2: Functional Dependencies
 519     Again, we should prefer, if possible, the inert variables on the RHS
 520
 521 Case 3: IP improvement work
 522     We must always rewrite so that the inert type is on the right.
 523
 524 \begin{code}
 525 spontaneousSolveStage :: SimplifierStage
 526 spontaneousSolveStage depth workItem inerts
 527   = do { mSolve <- trySpontaneousSolve workItem
 528
 529        ; case mSolve of
 530            SPCantSolve -> -- No spontaneous solution for him, keep going
 531                return $ SR { sr_new_work   = emptyWorkList
 532                            , sr_inerts     = inerts
 533                            , sr_stop       = ContinueWith workItem }
 534
 535            SPSolved workItem'
 536                | not (isGivenOrSolvedCt workItem)
 537                  -- Original was wanted or derived but we have now made him
 538                  -- given so we have to interact him with the inerts due to
 539                  -- its status change. This in turn may produce more work.
 540                  -- We do this *right now* (rather than just putting workItem'
 541                  -- back into the work-list) because we've solved
 542                -> do { bumpStepCountTcS
 543                      ; traceFireTcS depth (ptext (sLit "Spontaneous (w/d)") <+> ppr workItem)
 544                      ; (new_inert, new_work) <- runSolverPipeline depth
 545                              [ ("recursive interact with inert eqs", interactWithInertEqsStage)
 546                              , ("recursive interact with inerts", interactWithInertsStage)
 547                              ] inerts workItem'
 548                      ; return $ SR { sr_new_work = new_work
 549                                    , sr_inerts   = new_inert -- will include workItem'
 550                                    , sr_stop     = Stop }
 551                      }
 552                | otherwise
 553                    -> -- Original was given; he must then be inert all right, and
 554                       -- workList' are all givens from flattening
 555                       do { bumpStepCountTcS
 556                          ; traceFireTcS depth (ptext (sLit "Spontaneous (g)") <+> ppr workItem)
 557                          ; return $ SR { sr_new_work = emptyWorkList
 558                                        , sr_inerts   = inerts `updInertSet` workItem'
 559                                        , sr_stop     = Stop } }
 560            SPError -> -- Return with no new work
 561                return $ SR { sr_new_work = emptyWorkList
 562                            , sr_inerts   = inerts
 563                            , sr_stop     = Stop }
 564        }
 565
 566 data SPSolveResult = SPCantSolve | SPSolved WorkItem | SPError
 567 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
 568 -- SPSolved workItem' gives us a new *given* to go on
 569 -- SPError means that it's completely impossible to solve this equality, eg due to a kind error
 570
 571
 572 -- @trySpontaneousSolve wi@ solves equalities where one side is a
 573 -- touchable unification variable.
 574 --          See Note [Touchables and givens]
 575 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
 576 trySpontaneousSolve workItem@(CTyEqCan { cc_id = cv, cc_flavor = gw, cc_tyvar = tv1, cc_rhs = xi })
 577   | isGivenOrSolved gw
 578   = return SPCantSolve
 579   | Just tv2 <- tcGetTyVar_maybe xi
 580   = do { tch1 <- isTouchableMetaTyVar tv1
 581        ; tch2 <- isTouchableMetaTyVar tv2
 582        ; case (tch1, tch2) of
 583            (True,  True)  -> trySpontaneousEqTwoWay cv gw tv1 tv2
 584            (True,  False) -> trySpontaneousEqOneWay cv gw tv1 xi
 585            (False, True)  -> trySpontaneousEqOneWay cv gw tv2 (mkTyVarTy tv1)
 586            _ -> return SPCantSolve }
 587   | otherwise
 588   = do { tch1 <- isTouchableMetaTyVar tv1
 589        ; if tch1 then trySpontaneousEqOneWay cv gw tv1 xi
 590                  else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:"
 591                                     (ppr workItem)
 592                          ; return SPCantSolve }
 593        }
 594
 595   -- No need for
 596   --      trySpontaneousSolve (CFunEqCan ...) = ...
 597   -- See Note [No touchables as FunEq RHS] in TcSMonad
 598 trySpontaneousSolve _ = return SPCantSolve
 599
 600 ----------------
 601 trySpontaneousEqOneWay :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
 602 -- tv is a MetaTyVar, not untouchable
 603 trySpontaneousEqOneWay cv gw tv xi
 604   | not (isSigTyVar tv) || isTyVarTy xi
 605   = do { let kxi = typeKind xi -- NB: 'xi' is fully rewritten according to the inerts
 606                                -- so we have its more specific kind in our hands
 607        ; if kxi `isSubKind` tyVarKind tv then
 608              solveWithIdentity cv gw tv xi
 609          else return SPCantSolve
 610 {-
 611          else if tyVarKind tv `isSubKind` kxi then
 612              return SPCantSolve -- kinds are compatible but we can't solveWithIdentity this way
 613                                 -- This case covers the  a_touchable :: * ~ b_untouchable :: ??
 614                                 -- which has to be deferred or floated out for someone else to solve
 615                                 -- it in a scope where 'b' is no longer untouchable.
 616          else do { addErrorTcS KindError gw (mkTyVarTy tv) xi -- See Note [Kind errors]
 617                  ; return SPError }
 618 -}
 619        }
 620   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
 621   = return SPCantSolve
 622
 623 ----------------
 624 trySpontaneousEqTwoWay :: CoVar -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
 625 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 626 trySpontaneousEqTwoWay cv gw tv1 tv2
 627   | k1 `isSubKind` k2
 628   , nicer_to_update_tv2 = solveWithIdentity cv gw tv2 (mkTyVarTy tv1)
 629   | k2 `isSubKind` k1
 630   = solveWithIdentity cv gw tv1 (mkTyVarTy tv2)
 631   | otherwise -- None is a subkind of the other, but they are both touchable!
 632   = return SPCantSolve
 633     -- do { addErrorTcS KindError gw (mkTyVarTy tv1) (mkTyVarTy tv2)
 634     --   ; return SPError }
 635   where
 636     k1 = tyVarKind tv1
 637     k2 = tyVarKind tv2
 638     nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
 639 \end{code}
 640
 641 Note [Kind errors]
 642 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 643 Consider the wanted problem:
 644       alpha ~ (# Int, Int #)
 645 where alpha :: ?? and (# Int, Int #) :: (#). We can't spontaneously solve this constraint,
 646 but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay'
 647 simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and
 648 get quantified over in inference mode. That's bad because we do know at this point that the
 649 constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
 650
 651 The same applies in canonicalization code in case of kind errors in the givens.
 652
 653 However, when we canonicalize givens we only check for compatibility (@compatKind@).
 654 If there were a kind error in the givens, this means some form of inconsistency or dead code.
 655
 656 You may think that when we spontaneously solve wanteds we may have to look through the
 657 bindings to determine the right kind of the RHS type. E.g one may be worried that xi is
 658 @alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
 659 But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
 660 so this situation can't happen.
 661
 662 Note [Spontaneous solving and kind compatibility]
 663 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 664 Note that our canonical constraints insist that *all* equalities (tv ~
 665 xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
 666 the same kinds.  ("compatible" means one is a subKind of the other.)
 667
 668   - It can't be *equal* kinds, because
 669      b) wanted constraints don't necessarily have identical kinds
 670                eg   alpha::? ~ Int
 671      b) a solved wanted constraint becomes a given
 672
 673   - SPJ thinks that *given* constraints (tv ~ tau) always have that
 674     tau has a sub-kind of tv; and when solving wanted constraints
 675     in trySpontaneousEqTwoWay we re-orient to achieve this.
 676
 677   - Note that the kind invariant is maintained by rewriting.
 678     Eg wanted1 rewrites wanted2; if both were compatible kinds before,
 679        wanted2 will be afterwards.  Similarly givens.
 680
 681 Caveat:
 682   - Givens from higher-rank, such as:
 683           type family T b :: * -> * -> *
 684           type instance T Bool = (->)
 685
 686           f :: forall a. ((T a ~ (->)) => ...) -> a -> ...
 687           flop = f (...) True
 688      Whereas we would be able to apply the type instance, we would not be able to
 689      use the given (T Bool ~ (->)) in the body of 'flop'
 690
 691
 692 Note [Avoid double unifications]
 693 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 694 The spontaneous solver has to return a given which mentions the unified unification
 695 variable *on the left* of the equality. Here is what happens if not:
 696   Original wanted:  (a ~ alpha),  (alpha ~ Int)
 697 We spontaneously solve the first wanted, without changing the order!
 698       given : a ~ alpha      [having unified alpha := a]
 699 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
 700 At the end we spontaneously solve that guy, *reunifying*  [alpha := Int]
 701
 702 We avoid this problem by orienting the resulting given so that the unification
 703 variable is on the left.  [Note that alternatively we could attempt to
 704 enforce this at canonicalization]
 705
 706 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
 707 double unifications is the main reason we disallow touchable
 708 unification variables as RHS of type family equations: F xis ~ alpha.
 709
 710 \begin{code}
 711 ----------------
 712
 713 solveWithIdentity :: CoVar -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
 714 -- Solve with the identity coercion
 715 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 716 -- Precondition: CtFlavor is Wanted or Derived
 717 -- See [New Wanted Superclass Work] to see why solveWithIdentity
 718 --     must work for Derived as well as Wanted
 719 -- Returns: workItem where
 720 --        workItem = the new Given constraint
 721 solveWithIdentity cv wd tv xi
 722   = do { traceTcS "Sneaky unification:" $
 723                        vcat [text "Coercion variable:  " <+> ppr wd,
 724                              text "Coercion:           " <+> pprEq (mkTyVarTy tv) xi,
 725                              text "Left  Kind is     : " <+> ppr (typeKind (mkTyVarTy tv)),
 726                              text "Right Kind is     : " <+> ppr (typeKind xi)
 727                   ]
 728
 729        ; setWantedTyBind tv xi
 730        ; let refl_xi = mkReflCo xi
 731        ; cv_given <- newGivenCoVar (mkTyVarTy tv) xi refl_xi
 732
 733        ; when (isWanted wd) (setCoBind cv refl_xi)
 734            -- We don't want to do this for Derived, that's why we use 'when (isWanted wd)'
 735        ; return $ SPSolved (CTyEqCan { cc_id = cv_given
 736                                      , cc_flavor = mkSolvedFlavor wd UnkSkol
 737                                      , cc_tyvar  = tv, cc_rhs = xi }) }
 738 \end{code}
 739
 740
 741 *********************************************************************************
 742 *                                                                               *
 743                        The interact-with-inert Stage
 744 *                                                                               *
 745 *********************************************************************************
 746
 747 Note [The Solver Invariant]
 748 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 749 We always add Givens first.  So you might think that the solver has
 750 the invariant
 751
 752    If the work-item is Given,
 753    then the inert item must Given
 754
 755 But this isn't quite true.  Suppose we have,
 756     c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
 757 After processing the first two, we get
 758      c1: [G] beta ~ [alpha], c2 : [W] blah
 759 Now, c3 does not interact with the the given c1, so when we spontaneously
 760 solve c3, we must re-react it with the inert set.  So we can attempt a
 761 reaction between inert c2 [W] and work-item c3 [G].
 762
 763 It *is* true that [Solver Invariant]
 764    If the work-item is Given,
 765    AND there is a reaction
 766    then the inert item must Given
 767 or, equivalently,
 768    If the work-item is Given,
 769    and the inert item is Wanted/Derived
 770    then there is no reaction
 771
 772 \begin{code}
 773 -- Interaction result of  WorkItem <~> AtomicInert
 774 data InteractResult
 775    = IR { ir_stop         :: StopOrContinue
 776             -- Stop
 777             --   => Reagent (work item) consumed.
 778             -- ContinueWith new_reagent
 779             --   => Reagent transformed but keep gathering interactions.
 780             --      The transformed item remains inert with respect
 781             --      to any previously encountered inerts.
 782
 783         , ir_inert_action :: InertAction
 784             -- Whether the inert item should remain in the InertSet.
 785
 786         , ir_new_work     :: WorkList
 787             -- new work items to add to the WorkList
 788
 789         , ir_fire :: Maybe String    -- Tells whether a rule fired, and if so what
 790         }
 791
 792 -- What to do with the inert reactant.
 793 data InertAction = KeepInert | DropInert
 794
 795 mkIRContinue :: String -> WorkItem -> InertAction -> WorkList -> TcS InteractResult
 796 mkIRContinue rule wi keep newWork
 797   = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = keep
 798                 , ir_new_work = newWork, ir_fire = Just rule }
 799
 800 mkIRStopK :: String -> WorkList -> TcS InteractResult
 801 mkIRStopK rule newWork
 802   = return $ IR { ir_stop = Stop, ir_inert_action = KeepInert
 803                 , ir_new_work = newWork, ir_fire = Just rule }
 804
 805 mkIRStopD :: String -> WorkList -> TcS InteractResult
 806 mkIRStopD rule newWork
 807   = return $ IR { ir_stop = Stop, ir_inert_action = DropInert
 808                 , ir_new_work = newWork, ir_fire = Just rule }
 809
 810 noInteraction :: Monad m => WorkItem -> m InteractResult
 811 noInteraction wi
 812   = return $ IR { ir_stop = ContinueWith wi, ir_inert_action = KeepInert
 813                 , ir_new_work = emptyWorkList, ir_fire = Nothing }
 814
 815 data WhichComesFromInert = LeftComesFromInert | RightComesFromInert
 816      -- See Note [Efficient Orientation]
 817
 818
 819 ---------------------------------------------------
 820 -- Interact a single WorkItem with the equalities of an inert set as
 821 -- far as possible, i.e. until we get a Stop result from an individual
 822 -- reaction (i.e. when the WorkItem is consumed), or until we've
 823 -- interact the WorkItem with the entire equalities of the InertSet
 824
 825 interactWithInertEqsStage :: SimplifierStage
 826 interactWithInertEqsStage depth workItem inert
 827   = Bag.foldrBagM (interactNext depth) initITR (inert_eqs inert)
 828                         -- use foldr to preserve the order
 829   where
 830     initITR = SR { sr_inerts   = inert { inert_eqs = emptyCCan }
 831                  , sr_new_work = emptyWorkList
 832                  , sr_stop     = ContinueWith workItem }
 833
 834 ---------------------------------------------------
 835 -- Interact a single WorkItem with *non-equality* constraints in the inert set.
 836 -- Precondition: equality interactions must have already happened, hence we have
 837 -- to pick up some information from the incoming inert, before folding over the
 838 -- "Other" constraints it contains!
 839
 840 interactWithInertsStage :: SimplifierStage
 841 interactWithInertsStage depth workItem inert
 842   = let (relevant, inert_residual) = getISRelevant workItem inert
 843         initITR = SR { sr_inerts   = inert_residual
 844                      , sr_new_work = emptyWorkList
 845                      , sr_stop     = ContinueWith workItem }
 846     in Bag.foldrBagM (interactNext depth) initITR relevant
 847                         -- use foldr to preserve the order
 848   where
 849     getISRelevant :: CanonicalCt -> InertSet -> (CanonicalCts, InertSet)
 850     getISRelevant (CFrozenErr {}) is = (emptyCCan, is)
 851                   -- Nothing s relevant; we have alread interacted
 852                   -- it with the equalities in the inert set
 853
 854     getISRelevant (CDictCan { cc_class = cls } ) is
 855       = let (relevant, residual_map) = getRelevantCts cls (inert_dicts is)
 856         in (relevant, is { inert_dicts = residual_map })
 857     getISRelevant (CFunEqCan { cc_fun = tc } ) is
 858       = let (relevant, residual_map) = getRelevantCts tc (inert_funeqs is)
 859         in (relevant, is { inert_funeqs = residual_map })
 860     getISRelevant (CIPCan { cc_ip_nm = nm }) is
 861       = let (relevant, residual_map) = getRelevantCts nm (inert_ips is)
 862         in (relevant, is { inert_ips = residual_map })
 863     -- An equality, finally, may kick everything except equalities out
 864     -- because we have already interacted the equalities in interactWithInertEqsStage
 865     getISRelevant _eq_ct is  -- Equality, everything is relevant for this one
 866                              -- TODO: if we were caching variables, we'd know that only
 867                              --       some are relevant. Experiment with this for now.
 868       = let cts = cCanMapToBag (inert_ips is) `unionBags`
 869                     cCanMapToBag (inert_dicts is) `unionBags` cCanMapToBag (inert_funeqs is)
 870         in (cts, is { inert_dicts  = emptyCCanMap
 871                     , inert_ips    = emptyCCanMap
 872                     , inert_funeqs = emptyCCanMap })
 873
 874 interactNext :: SubGoalDepth -> AtomicInert -> StageResult -> TcS StageResult
 875 interactNext depth inert it
 876   | ContinueWith work_item <- sr_stop it
 877   = do { let inerts = sr_inerts it
 878
 879        ; IR { ir_new_work = new_work, ir_inert_action = inert_action
 880             , ir_fire = fire_info, ir_stop = stop }
 881             <- interactWithInert inert work_item
 882
 883        ; let mk_msg rule
 884                = text rule <+> keep_doc
 885                  <+> vcat [ ptext (sLit "Inert =") <+> ppr inert
 886                           , ptext (sLit "Work =")  <+> ppr work_item
 887                           , ppUnless (isEmptyWorkList new_work) $
 888                             ptext (sLit "New =") <+> ppr new_work ]
 889              keep_doc = case inert_action of
 890                           KeepInert -> ptext (sLit "[keep]")
 891                           DropInert -> ptext (sLit "[drop]")
 892        ; case fire_info of
 893            Just rule -> do { bumpStepCountTcS
 894                            ; traceFireTcS depth (mk_msg rule) }
 895            Nothing  -> return ()
 896
 897        -- New inerts depend on whether we KeepInert or not
 898        ; let inerts_new = case inert_action of
 899                             KeepInert -> inerts `updInertSet` inert
 900                             DropInert -> inerts
 901
 902        ; return $ SR { sr_inerts   = inerts_new
 903                      , sr_new_work = sr_new_work it `unionWorkList` new_work
 904                      , sr_stop     = stop } }
 905   | otherwise
 906   = return $ it { sr_inerts = (sr_inerts it) `updInertSet` inert }
 907
 908 -- Do a single interaction of two constraints.
 909 interactWithInert :: AtomicInert -> WorkItem -> TcS InteractResult
 910 interactWithInert inert workItem
 911   = do { ctxt <- getTcSContext
 912        ; let is_allowed  = allowedInteraction (simplEqsOnly ctxt) inert workItem
 913
 914        ; if is_allowed then
 915               doInteractWithInert inert workItem
 916           else
 917               noInteraction workItem
 918        }
 919
 920 allowedInteraction :: Bool -> AtomicInert -> WorkItem -> Bool
 921 -- Allowed interactions
 922 allowedInteraction eqs_only (CDictCan {}) (CDictCan {}) = not eqs_only
 923 allowedInteraction eqs_only (CIPCan {})   (CIPCan {})   = not eqs_only
 924 allowedInteraction _ _ _ = True
 925
 926 --------------------------------------------
 927 doInteractWithInert :: CanonicalCt -> CanonicalCt -> TcS InteractResult
 928 -- Identical class constraints.
 929
 930 doInteractWithInert
 931   inertItem@(CDictCan { cc_id = d1, cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 })
 932    workItem@(CDictCan { cc_id = d2, cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
 933
 934   | cls1 == cls2
 935   = do { let pty1 = ClassP cls1 tys1
 936              pty2 = ClassP cls2 tys2
 937              inert_pred_loc     = (pty1, pprFlavorArising fl1)
 938              work_item_pred_loc = (pty2, pprFlavorArising fl2)
 939
 940        ; any_fundeps
 941            <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
 942               -- NB: We don't create fds for given (and even solved), have not seen a useful
 943               -- situation for these and even if we did we'd have to be very careful to only
 944               -- create Derived's and not Wanteds.
 945
 946               else let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
 947                        wloc    = get_workitem_wloc fl2
 948                    in rewriteWithFunDeps fd_eqns tys2 wloc
 949                       -- See Note [Efficient Orientation], [When improvement happens]
 950
 951        ; case any_fundeps of
 952            -- No Functional Dependencies
 953            Nothing
 954                | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" (EvId d1,fl1) workItem
 955                | otherwise         -> noInteraction workItem
 956
 957            -- Actual Functional Dependencies
 958            Just (rewritten_tys2,cos2,fd_work)
 959                | not (eqTypes tys1 rewritten_tys2)
 960                -- Standard thing: create derived fds and keep on going. Importantly we don't
 961                -- throw workitem back in the worklist because this can cause loops. See #5236.
 962                -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
 963                      ; mkIRContinue "Cls/Cls fundep (not solved)" workItem KeepInert fd_cans }
 964
 965                -- This WHOLE otherwise branch is an optimization where the fd made the things match
 966                | otherwise
 967                , let dict_co = mkTyConAppCo (classTyCon cls1) cos2
 968                -> case fl2 of
 969                     Given {}
 970                         -> pprPanic "Unexpected given!" (ppr inertItem $$ ppr workItem)
 971                            -- The only way to have created a fundep is if the inert was
 972                            -- wanted or derived, in which case the workitem can't be given!
 973                     Derived {}
 974                         -- The types were made to exactly match so we don't need
 975                         -- the workitem any longer.
 976                         -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
 977                                -- No rewriting really, so let's create deriveds fds
 978                               ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
 979                     Wanted  {}
 980                         | isDerived fl1
 981                             -> do { setDictBind d2 (EvCast d1 dict_co)
 982                                   ; let inert_w = inertItem { cc_flavor = fl2 }
 983                            -- A bit naughty: we take the inert Derived,
 984                            -- turn it into a Wanted, use it to solve the work-item
 985                            -- and put it back into the work-list
 986                            -- Maybe rather than starting again, we could keep going
 987                            -- with the rewritten workitem, having dropped the inert, but its
 988                            -- safe to restart.
 989
 990                            -- Also: we have rewriting so lets create wanted fds
 991                                   ; fd_cans <- mkCanonicalFDAsWanted fd_work
 992                                   ; mkIRStopD "Cls/Cls fundep (solved)" $
 993                                     workListFromNonEq inert_w `unionWorkList` fd_cans }
 994                         | otherwise
 995                         -> do { setDictBind d2 (EvCast d1 dict_co)
 996                           -- Rewriting is happening, so we have to create wanted fds
 997                               ; fd_cans <- mkCanonicalFDAsWanted fd_work
 998                               ; mkIRStopK "Cls/Cls fundep (solved)" fd_cans }
 999        }
1000   where get_workitem_wloc (Wanted wl)  = wl
1001         get_workitem_wloc (Derived wl) = wl
1002         get_workitem_wloc (Given {})   = panic "Unexpected given!"
1003
1004
1005 -- Class constraint and given equality: use the equality to rewrite
1006 -- the class constraint.
1007 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1008                     (CDictCan { cc_id = dv, cc_flavor = wfl, cc_class = cl, cc_tyargs = xis })
1009   | ifl `canRewrite` wfl
1010   , tv `elemVarSet` tyVarsOfTypes xis
1011   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,wfl,cl,xis)
1012             -- Continue with rewritten Dictionary because we can only be in the
1013             -- interactWithEqsStage, so the dictionary is inert.
1014        ; mkIRContinue "Eq/Cls" rewritten_dict KeepInert emptyWorkList }
1015
1016 doInteractWithInert (CDictCan { cc_id = dv, cc_flavor = ifl, cc_class = cl, cc_tyargs = xis })
1017            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1018   | wfl `canRewrite` ifl
1019   , tv `elemVarSet` tyVarsOfTypes xis
1020   = do { rewritten_dict <- rewriteDict (cv,tv,xi) (dv,ifl,cl,xis)
1021        ; mkIRContinue "Cls/Eq" workItem DropInert (workListFromNonEq rewritten_dict) }
1022
1023 -- Class constraint and given equality: use the equality to rewrite
1024 -- the class constraint.
1025 doInteractWithInert (CTyEqCan { cc_id = cv, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi })
1026                     (CIPCan { cc_id = ipid, cc_flavor = wfl, cc_ip_nm = nm, cc_ip_ty = ty })
1027   | ifl `canRewrite` wfl
1028   , tv `elemVarSet` tyVarsOfType ty
1029   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,wfl,nm,ty)
1030        ; mkIRContinue "Eq/IP" rewritten_ip KeepInert emptyWorkList }
1031
1032 doInteractWithInert (CIPCan { cc_id = ipid, cc_flavor = ifl, cc_ip_nm = nm, cc_ip_ty = ty })
1033            workItem@(CTyEqCan { cc_id = cv, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi })
1034   | wfl `canRewrite` ifl
1035   , tv `elemVarSet` tyVarsOfType ty
1036   = do { rewritten_ip <- rewriteIP (cv,tv,xi) (ipid,ifl,nm,ty)
1037        ; mkIRContinue "IP/Eq" workItem DropInert (workListFromNonEq rewritten_ip) }
1038
1039 -- Two implicit parameter constraints.  If the names are the same,
1040 -- but their types are not, we generate a wanted type equality
1041 -- that equates the type (this is "improvement").
1042 -- However, we don't actually need the coercion evidence,
1043 -- so we just generate a fresh coercion variable that isn't used anywhere.
1044 doInteractWithInert (CIPCan { cc_id = id1, cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 })
1045            workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
1046   | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
1047   =     -- See Note [Overriding implicit parameters]
1048         -- Dump the inert item, override totally with the new one
1049         -- Do not require type equality
1050         -- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
1051         --              we must *override* the outer one with the inner one
1052     mkIRContinue "IP/IP override" workItem DropInert emptyWorkList
1053
1054   | nm1 == nm2 && ty1 `eqType` ty2
1055   = solveOneFromTheOther "IP/IP" (EvId id1,ifl) workItem
1056
1057   | nm1 == nm2
1058   =     -- See Note [When improvement happens]
1059     do { co_var <- newCoVar ty2 ty1 -- See Note [Efficient Orientation]
1060        ; let flav = Wanted (combineCtLoc ifl wfl)
1061        ; cans <- mkCanonical flav co_var
1062        ; case wfl of
1063            Given   {} -> pprPanic "Unexpected given IP" (ppr workItem)
1064            Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
1065            Wanted  {} ->
1066                do { setIPBind (cc_id workItem) $
1067                     EvCast id1 (mkSymCo (mkCoVarCo co_var))
1068                   ; mkIRStopK "IP/IP interaction (solved)" cans }
1069        }
1070
1071 -- Never rewrite a given with a wanted equality, and a type function
1072 -- equality can never rewrite an equality. We rewrite LHS *and* RHS
1073 -- of function equalities so that our inert set exposes everything that
1074 -- we know about equalities.
1075
1076 -- Inert: equality, work item: function equality
1077 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = ifl, cc_tyvar = tv, cc_rhs = xi1 })
1078                     (CFunEqCan { cc_id = cv2, cc_flavor = wfl, cc_fun = tc
1079                                , cc_tyargs = args, cc_rhs = xi2 })
1080   | ifl `canRewrite` wfl
1081   , tv `elemVarSet` tyVarsOfTypes (xi2:args) -- Rewrite RHS as well
1082   = do { rewritten_funeq <- rewriteFunEq (cv1,tv,xi1) (cv2,wfl,tc,args,xi2)
1083        ; mkIRStopK "Eq/FunEq" (workListFromEq rewritten_funeq) }
1084          -- Must Stop here, because we may no longer be inert after the rewritting.
1085
1086 -- Inert: function equality, work item: equality
1087 doInteractWithInert (CFunEqCan {cc_id = cv1, cc_flavor = ifl, cc_fun = tc
1088                               , cc_tyargs = args, cc_rhs = xi1 })
1089            workItem@(CTyEqCan { cc_id = cv2, cc_flavor = wfl, cc_tyvar = tv, cc_rhs = xi2 })
1090   | wfl `canRewrite` ifl
1091   , tv `elemVarSet` tyVarsOfTypes (xi1:args) -- Rewrite RHS as well
1092   = do { rewritten_funeq <- rewriteFunEq (cv2,tv,xi2) (cv1,ifl,tc,args,xi1)
1093        ; mkIRContinue "FunEq/Eq" workItem DropInert (workListFromEq rewritten_funeq) }
1094          -- One may think that we could (KeepTransformedInert rewritten_funeq)
1095          -- but that is wrong, because it may end up not being inert with respect
1096          -- to future inerts. Example:
1097          -- Original inert = {    F xis ~  [a], b ~ Maybe Int }
1098          -- Work item comes along = a ~ [b]
1099          -- If we keep { F xis ~ [b] } in the inert set we will end up with:
1100          --      { F xis ~ [b], b ~ Maybe Int, a ~ [Maybe Int] }
1101          -- At the end, which is *not* inert. So we should unfortunately DropInert here.
1102
1103 doInteractWithInert (CFunEqCan { cc_id = cv1, cc_flavor = fl1, cc_fun = tc1
1104                                , cc_tyargs = args1, cc_rhs = xi1 })
1105            workItem@(CFunEqCan { cc_id = cv2, cc_flavor = fl2, cc_fun = tc2
1106                                , cc_tyargs = args2, cc_rhs = xi2 })
1107   | tc1 == tc2 && and (zipWith eqType args1 args2)
1108   , Just GivenSolved <- isGiven_maybe fl1
1109   = mkIRContinue "Funeq/Funeq" workItem DropInert emptyWorkList
1110   | tc1 == tc2 && and (zipWith eqType args1 args2)
1111   , Just GivenSolved <- isGiven_maybe fl2
1112   = mkIRStopK "Funeq/Funeq" emptyWorkList
1113
1114   | fl1 `canSolve` fl2 && lhss_match
1115   = do { cans <- rewriteEqLHS LeftComesFromInert  (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
1116        ; mkIRStopK "FunEq/FunEq" cans }
1117   | fl2 `canSolve` fl1 && lhss_match
1118   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
1119        ; mkIRContinue "FunEq/FunEq" workItem DropInert cans }
1120   where
1121     lhss_match = tc1 == tc2 && eqTypes args1 args2
1122
1123 doInteractWithInert (CTyEqCan { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1124            workItem@(CTyEqCan { cc_id = cv2, cc_flavor = fl2, cc_tyvar = tv2, cc_rhs = xi2 })
1125 -- Check for matching LHS
1126   | fl1 `canSolve` fl2 && tv1 == tv2
1127   = do { cans <- rewriteEqLHS LeftComesFromInert (mkCoVarCo cv1,xi1) (cv2,fl2,xi2)
1128        ; mkIRStopK "Eq/Eq lhs" cans }
1129
1130   | fl2 `canSolve` fl1 && tv1 == tv2
1131   = do { cans <- rewriteEqLHS RightComesFromInert (mkCoVarCo cv2,xi2) (cv1,fl1,xi1)
1132        ; mkIRContinue "Eq/Eq lhs" workItem DropInert cans }
1133
1134 -- Check for rewriting RHS
1135   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfType xi2
1136   = do { rewritten_eq <- rewriteEqRHS (cv1,tv1,xi1) (cv2,fl2,tv2,xi2)
1137        ; mkIRStopK "Eq/Eq rhs" rewritten_eq }
1138
1139   | fl2 `canRewrite` fl1 && tv2 `elemVarSet` tyVarsOfType xi1
1140   = do { rewritten_eq <- rewriteEqRHS (cv2,tv2,xi2) (cv1,fl1,tv1,xi1)
1141        ; mkIRContinue "Eq/Eq rhs" workItem DropInert rewritten_eq }
1142
1143 doInteractWithInert (CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1144                     (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1145   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1146   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1147        ; mkIRStopK "Frozen/Eq" rewritten_frozen }
1148
1149 doInteractWithInert (CFrozenErr { cc_id = cv2, cc_flavor = fl2 })
1150            workItem@(CTyEqCan   { cc_id = cv1, cc_flavor = fl1, cc_tyvar = tv1, cc_rhs = xi1 })
1151   | fl1 `canRewrite` fl2 && tv1 `elemVarSet` tyVarsOfEvVar cv2
1152   = do { rewritten_frozen <- rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1153        ; mkIRContinue "Frozen/Eq" workItem DropInert rewritten_frozen }
1154
1155 -- Fall-through case for all other situations
1156 doInteractWithInert _ workItem = noInteraction workItem
1157
1158 -------------------------
1159 -- Equational Rewriting
1160 rewriteDict  :: (CoVar, TcTyVar, Xi) -> (DictId, CtFlavor, Class, [Xi]) -> TcS CanonicalCt
1161 rewriteDict (cv,tv,xi) (dv,gw,cl,xis)
1162   = do { let cos  = map (liftCoSubstWith [tv] [mkCoVarCo cv]) xis   -- xis[tv] ~ xis[xi]
1163              args = substTysWith [tv] [xi] xis
1164              con  = classTyCon cl
1165              dict_co = mkTyConAppCo con cos
1166        ; dv' <- newDictVar cl args
1167        ; case gw of
1168            Wanted {}         -> setDictBind dv (EvCast dv' (mkSymCo dict_co))
1169            Given {}          -> setDictBind dv' (EvCast dv dict_co)
1170            Derived {}        -> return () -- Derived dicts we don't set any evidence
1171
1172        ; return (CDictCan { cc_id = dv'
1173                           , cc_flavor = gw
1174                           , cc_class = cl
1175                           , cc_tyargs = args }) }
1176
1177 rewriteIP :: (CoVar,TcTyVar,Xi) -> (EvVar,CtFlavor, IPName Name, TcType) -> TcS CanonicalCt
1178 rewriteIP (cv,tv,xi) (ipid,gw,nm,ty)
1179   = do { let ip_co = liftCoSubstWith [tv] [mkCoVarCo cv] ty     -- ty[tv] ~ t[xi]
1180              ty'   = substTyWith   [tv] [xi] ty
1181        ; ipid' <- newIPVar nm ty'
1182        ; case gw of
1183            Wanted {}         -> setIPBind ipid  (EvCast ipid' (mkSymCo ip_co))
1184            Given {}          -> setIPBind ipid' (EvCast ipid ip_co)
1185            Derived {}        -> return () -- Derived ips: we don't set any evidence
1186
1187        ; return (CIPCan { cc_id = ipid'
1188                         , cc_flavor = gw
1189                         , cc_ip_nm = nm
1190                         , cc_ip_ty = ty' }) }
1191
1192 rewriteFunEq :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TyCon, [Xi], Xi) -> TcS CanonicalCt
1193 rewriteFunEq (cv1,tv,xi1) (cv2,gw, tc,args,xi2)                   -- cv2 :: F args ~ xi2
1194   = do { let co_subst = liftCoSubstWith [tv] [mkCoVarCo cv1]
1195              arg_cos  = map co_subst args
1196              args'    = substTysWith [tv] [xi1] args
1197              fun_co   = mkTyConAppCo tc arg_cos                -- fun_co :: F args ~ F args'
1198
1199              xi2'    = substTyWith [tv] [xi1] xi2
1200              xi2_co  = co_subst xi2 -- xi2_co :: xi2 ~ xi2'
1201
1202        ; cv2' <- newCoVar (mkTyConApp tc args') xi2'
1203        ; case gw of
1204            Wanted {} -> setCoBind cv2  (fun_co         `mkTransCo`
1205                                         mkCoVarCo cv2' `mkTransCo`
1206                                         mkSymCo xi2_co)
1207            Given {}  -> setCoBind cv2' (mkSymCo fun_co `mkTransCo`
1208                                         mkCoVarCo cv2  `mkTransCo`
1209                                         xi2_co)
1210            Derived {} -> return ()
1211
1212        ; return (CFunEqCan { cc_id = cv2'
1213                            , cc_flavor = gw
1214                            , cc_tyargs = args'
1215                            , cc_fun = tc
1216                            , cc_rhs = xi2' }) }
1217
1218
1219 rewriteEqRHS :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor,TcTyVar,Xi) -> TcS WorkList
1220 -- Use the first equality to rewrite the second, flavors already checked.
1221 -- E.g.          c1 : tv1 ~ xi1   c2 : tv2 ~ xi2
1222 -- rewrites c2 to give
1223 --               c2' : tv2 ~ xi2[xi1/tv1]
1224 -- We must do an occurs check to sure the new constraint is canonical
1225 -- So we might return an empty bag
1226 rewriteEqRHS (cv1,tv1,xi1) (cv2,gw,tv2,xi2)
1227   | Just tv2' <- tcGetTyVar_maybe xi2'
1228   , tv2 == tv2'  -- In this case xi2[xi1/tv1] = tv2, so we have tv2~tv2
1229   = do { when (isWanted gw) (setCoBind cv2 (mkSymCo co2'))
1230        ; return emptyWorkList }
1231   | otherwise
1232   = do { cv2' <- newCoVar (mkTyVarTy tv2) xi2'
1233        ; case gw of
1234              Wanted {} -> setCoBind cv2 $ mkCoVarCo cv2' `mkTransCo`
1235                                           mkSymCo co2'
1236              Given {}  -> setCoBind cv2' $ mkCoVarCo cv2 `mkTransCo`
1237                                            co2'
1238              Derived {} -> return ()
1239        ; canEqToWorkList gw cv2' (mkTyVarTy tv2) xi2' }
1240   where
1241     xi2' = substTyWith [tv1] [xi1] xi2
1242     co2' = liftCoSubstWith [tv1] [mkCoVarCo cv1] xi2  -- xi2 ~ xi2[xi1/tv1]
1243
1244 rewriteEqLHS :: WhichComesFromInert -> (Coercion,Xi) -> (CoVar,CtFlavor,Xi) -> TcS WorkList
1245 -- Used to ineract two equalities of the following form:
1246 -- First Equality:   co1: (XXX ~ xi1)
1247 -- Second Equality:  cv2: (XXX ~ xi2)
1248 -- Where the cv1 `canRewrite` cv2 equality
1249 -- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1),
1250 --    See Note [Efficient Orientation] for that
1251 rewriteEqLHS LeftComesFromInert (co1,xi1) (cv2,gw,xi2)
1252   = do { cv2' <- newCoVar xi2 xi1
1253        ; case gw of
1254            Wanted {} -> setCoBind cv2 $
1255                         co1 `mkTransCo` mkSymCo (mkCoVarCo cv2')
1256            Given {}  -> setCoBind cv2' $
1257                         mkSymCo (mkCoVarCo cv2) `mkTransCo` co1
1258            Derived {} -> return ()
1259        ; mkCanonical gw cv2' }
1260
1261 rewriteEqLHS RightComesFromInert (co1,xi1) (cv2,gw,xi2)
1262   = do { cv2' <- newCoVar xi1 xi2
1263        ; case gw of
1264            Wanted {} -> setCoBind cv2 $
1265                         co1 `mkTransCo` mkCoVarCo cv2'
1266            Given {}  -> setCoBind cv2' $
1267                         mkSymCo co1 `mkTransCo` mkCoVarCo cv2
1268            Derived {} -> return ()
1269        ; mkCanonical gw cv2' }
1270
1271 rewriteFrozen :: (CoVar,TcTyVar,Xi) -> (CoVar,CtFlavor) -> TcS WorkList
1272 rewriteFrozen (cv1, tv1, xi1) (cv2, fl2)
1273   = do { cv2' <- newCoVar ty2a' ty2b'  -- ty2a[xi1/tv1] ~ ty2b[xi1/tv1]
1274        ; case fl2 of
1275              Wanted {} -> setCoBind cv2 $ co2a'                `mkTransCo`
1276                                           mkCoVarCo cv2' `mkTransCo`
1277                                           mkSymCo co2b'
1278
1279              Given {} -> setCoBind cv2' $ mkSymCo co2a'  `mkTransCo`
1280                                           mkCoVarCo cv2  `mkTransCo`
1281                                           co2b'
1282
1283              Derived {} -> return ()
1284
1285       ; return (workListFromNonEq $ CFrozenErr { cc_id = cv2', cc_flavor = fl2 }) }
1286   where
1287     (ty2a, ty2b) = coVarKind cv2          -- cv2 : ty2a ~ ty2b
1288     ty2a' = substTyWith [tv1] [xi1] ty2a
1289     ty2b' = substTyWith [tv1] [xi1] ty2b
1290
1291     co2a' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2a  -- ty2a ~ ty2a[xi1/tv1]
1292     co2b' = liftCoSubstWith [tv1] [mkCoVarCo cv1] ty2b  -- ty2b ~ ty2b[xi1/tv1]
1293
1294 solveOneFromTheOther_ExtraWork :: String -> (EvTerm, CtFlavor)
1295                                -> CanonicalCt -> WorkList -> TcS InteractResult
1296 -- First argument inert, second argument work-item. They both represent
1297 -- wanted/given/derived evidence for the *same* predicate so
1298 -- we can discharge one directly from the other.
1299 --
1300 -- Precondition: value evidence only (implicit parameters, classes)
1301 --               not coercion
1302 solveOneFromTheOther_ExtraWork info (ev_term,ifl) workItem extra_work
1303   | isDerived wfl
1304   = mkIRStopK ("Solved[DW] " ++ info) extra_work
1305
1306   | isDerived ifl -- The inert item is Derived, we can just throw it away,
1307                   -- The workItem is inert wrt earlier inert-set items,
1308                   -- so it's safe to continue on from this point
1309   = mkIRContinue ("Solved[DI] " ++ info) workItem DropInert extra_work
1310
1311   | Just GivenSolved <- isGiven_maybe ifl, isGivenOrSolved wfl
1312     -- Same if the inert is a GivenSolved -- just get rid of it
1313   = mkIRContinue ("Solved[SI] " ++ info) workItem DropInert extra_work
1314
1315   | otherwise
1316   = ASSERT( ifl `canSolve` wfl )
1317       -- Because of Note [The Solver Invariant], plus Derived dealt with
1318     do { when (isWanted wfl) $ setEvBind wid ev_term
1319            -- Overwrite the binding, if one exists
1320            -- If both are Given, we already have evidence; no need to duplicate
1321        ; mkIRStopK ("Solved " ++ info) extra_work }
1322   where
1323      wfl = cc_flavor workItem
1324      wid = cc_id workItem
1325
1326
1327 solveOneFromTheOther :: String -> (EvTerm, CtFlavor) -> CanonicalCt -> TcS InteractResult
1328 solveOneFromTheOther str evfl ct
1329   = solveOneFromTheOther_ExtraWork str evfl ct emptyWorkList -- extra work is empty
1330
1331 \end{code}
1332
1333 Note [Superclasses and recursive dictionaries]
1334 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1335     Overlaps with Note [SUPERCLASS-LOOP 1]
1336                   Note [SUPERCLASS-LOOP 2]
1337                   Note [Recursive instances and superclases]
1338     ToDo: check overlap and delete redundant stuff
1339
1340 Right before adding a given into the inert set, we must
1341 produce some more work, that will bring the superclasses
1342 of the given into scope. The superclass constraints go into
1343 our worklist.
1344
1345 When we simplify a wanted constraint, if we first see a matching
1346 instance, we may produce new wanted work. To (1) avoid doing this work
1347 twice in the future and (2) to handle recursive dictionaries we may ``cache''
1348 this item as given into our inert set WITHOUT adding its superclass constraints,
1349 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
1350 for doing the isGoodRecEv check in an older version of the type checker].
1351
1352 But now we have added partially solved constraints to the worklist which may
1353 interact with other wanteds. Consider the example:
1354
1355 Example 1:
1356
1357     class Eq b => Foo a b        --- 0-th selector
1358     instance Eq a => Foo [a] a   --- fooDFun
1359
1360 and wanted (Foo [t] t). We are first going to see that the instance matches
1361 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1362        d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3
1363 Our work list is going to contain a new *wanted* goal
1364        d3 :_w Eq t
1365
1366 Ok, so how do we get recursive dictionaries, at all:
1367
1368 Example 2:
1369
1370     data D r = ZeroD | SuccD (r (D r));
1371
1372     instance (Eq (r (D r))) => Eq (D r) where
1373         ZeroD     == ZeroD     = True
1374         (SuccD a) == (SuccD b) = a == b
1375         _         == _         = False;
1376
1377     equalDC :: D [] -> D [] -> Bool;
1378     equalDC = (==);
1379
1380 We need to prove (Eq (D [])). Here's how we go:
1381
1382         d1 :_w Eq (D [])
1383
1384 by instance decl, holds if
1385         d2 :_w Eq [D []]
1386         where   d1 = dfEqD d2
1387
1388 *BUT* we have an inert set which gives us (no superclasses):
1389         d1 :_g Eq (D [])
1390 By the instance declaration of Eq we can show the 'd2' goal if
1391         d3 :_w Eq (D [])
1392         where   d2 = dfEqList d3
1393                 d1 = dfEqD d2
1394 Now, however this wanted can interact with our inert d1 to set:
1395         d3 := d1
1396 and solve the goal. Why was this interaction OK? Because, if we chase the
1397 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
1398 are really setting
1399         d3 := dfEqD2 (dfEqList d3)
1400 which is FINE because the use of d3 is protected by the instance function
1401 applications.
1402
1403 So, our strategy is to try to put solved wanted dictionaries into the
1404 inert set along with their superclasses (when this is meaningful,
1405 i.e. when new wanted goals are generated) but solve a wanted dictionary
1406 from a given only in the case where the evidence variable of the
1407 wanted is mentioned in the evidence of the given (recursively through
1408 the evidence binds) in a protected way: more instance function applications
1409 than superclass selectors.
1410
1411 Here are some more examples from GHC's previous type checker
1412
1413
1414 Example 3:
1415 This code arises in the context of "Scrap Your Boilerplate with Class"
1416
1417     class Sat a
1418     class Data ctx a
1419     instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
1420     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
1421
1422     class Data Maybe a => Foo a
1423
1424     instance Foo t => Sat (Maybe t)                             -- dfunSat
1425
1426     instance Data Maybe a => Foo a                              -- dfunFoo1
1427     instance Foo a        => Foo [a]                            -- dfunFoo2
1428     instance                 Foo [Char]                         -- dfunFoo3
1429
1430 Consider generating the superclasses of the instance declaration
1431          instance Foo a => Foo [a]
1432
1433 So our problem is this
1434     d0 :_g Foo t
1435     d1 :_w Data Maybe [t]
1436
1437 We may add the given in the inert set, along with its superclasses
1438 [assuming we don't fail because there is a matching instance, see
1439  tryTopReact, given case ]
1440   Inert:
1441     d0 :_g Foo t
1442   WorkList
1443     d01 :_g Data Maybe t  -- d2 := EvDictSuperClass d0 0
1444     d1 :_w Data Maybe [t]
1445 Then d2 can readily enter the inert, and we also do solving of the wanted
1446   Inert:
1447     d0 :_g Foo t
1448     d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1449   WorkList
1450     d2 :_w Sat (Maybe [t])
1451     d3 :_w Data Maybe t
1452     d01 :_g Data Maybe t
1453 Now, we may simplify d2 more:
1454   Inert:
1455       d0 :_g Foo t
1456       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1457       d1 :_g Data Maybe [t]
1458       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1459   WorkList:
1460       d3 :_w Data Maybe t
1461       d4 :_w Foo [t]
1462       d01 :_g Data Maybe t
1463
1464 Now, we can just solve d3.
1465   Inert
1466       d0 :_g Foo t
1467       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1468       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1469   WorkList
1470       d4 :_w Foo [t]
1471       d01 :_g Data Maybe t
1472 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1473   Inert
1474       d0 :_g Foo t
1475       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1476       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1477       d4 :_g Foo [t]                  d4 := dfunFoo2 d5
1478   WorkList:
1479       d5 :_w Foo t
1480       d6 :_g Data Maybe [t]           d6 := EvDictSuperClass d4 0
1481       d01 :_g Data Maybe t
1482 Now, d5 can be solved! (and its superclass enter scope)
1483   Inert
1484       d0 :_g Foo t
1485       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1486       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1487       d4 :_g Foo [t]                  d4 := dfunFoo2 d5
1488       d5 :_g Foo t                    d5 := dfunFoo1 d7
1489   WorkList:
1490       d7 :_w Data Maybe t
1491       d6 :_g Data Maybe [t]
1492       d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
1493       d01 :_g Data Maybe t
1494
1495 Now, two problems:
1496    [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1497        we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1498        that must not be used (look at case interactInert where both inert and workitem
1499        are givens). So we have several options:
1500        - Drop the workitem always (this will drop d8)
1501               This feels very unsafe -- what if the work item was the "good" one
1502               that should be used later to solve another wanted?
1503        - Don't drop anyone: the inert set may contain multiple givens!
1504               [This is currently implemented]
1505
1506 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1507   [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1508       d7. Now the [isRecDictEv] function in the ineration solver
1509       [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1510       precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1511
1512       So, no interaction happens there. Then we meet d01 and there is no recursion
1513       problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1514
1515 Note [SUPERCLASS-LOOP 1]
1516 ~~~~~~~~~~~~~~~~~~~~~~~~
1517 We have to be very, very careful when generating superclasses, lest we
1518 accidentally build a loop. Here's an example:
1519
1520   class S a
1521
1522   class S a => C a where { opc :: a -> a }
1523   class S b => D b where { opd :: b -> b }
1524
1525   instance C Int where
1526      opc = opd
1527
1528   instance D Int where
1529      opd = opc
1530
1531 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1532 Simplifying, we may well get:
1533         $dfCInt = :C ds1 (opd dd)
1534         dd  = $dfDInt
1535         ds1 = $p1 dd
1536 Notice that we spot that we can extract ds1 from dd.
1537
1538 Alas!  Alack! We can do the same for (instance D Int):
1539
1540         $dfDInt = :D ds2 (opc dc)
1541         dc  = $dfCInt
1542         ds2 = $p1 dc
1543
1544 And now we've defined the superclass in terms of itself.
1545 Two more nasty cases are in
1546         tcrun021
1547         tcrun033
1548
1549 Solution:
1550   - Satisfy the superclass context *all by itself*
1551     (tcSimplifySuperClasses)
1552   - And do so completely; i.e. no left-over constraints
1553     to mix with the constraints arising from method declarations
1554
1555
1556 Note [SUPERCLASS-LOOP 2]
1557 ~~~~~~~~~~~~~~~~~~~~~~~~
1558 We need to be careful when adding "the constaint we are trying to prove".
1559 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1560
1561         class Ord a => C a where
1562         instance Ord [a] => C [a] where ...
1563
1564 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1565 superclasses of C [a] to avails.  But we must not overwrite the binding
1566 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1567 build a loop!
1568
1569 Here's another variant, immortalised in tcrun020
1570         class Monad m => C1 m
1571         class C1 m => C2 m x
1572         instance C2 Maybe Bool
1573 For the instance decl we need to build (C1 Maybe), and it's no good if
1574 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1575 before we search for C1 Maybe.
1576
1577 Here's another example
1578         class Eq b => Foo a b
1579         instance Eq a => Foo [a] a
1580 If we are reducing
1581         (Foo [t] t)
1582
1583 we'll first deduce that it holds (via the instance decl).  We must not
1584 then overwrite the Eq t constraint with a superclass selection!
1585
1586 At first I had a gross hack, whereby I simply did not add superclass constraints
1587 in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
1588 becuase it lost legitimate superclass sharing, and it still didn't do the job:
1589 I found a very obscure program (now tcrun021) in which improvement meant the
1590 simplifier got two bites a the cherry... so something seemed to be an Stop
1591 first time, but reducible next time.
1592
1593 Now we implement the Right Solution, which is to check for loops directly
1594 when adding superclasses.  It's a bit like the occurs check in unification.
1595
1596 Note [Recursive instances and superclases]
1597 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1598 Consider this code, which arises in the context of "Scrap Your
1599 Boilerplate with Class".
1600
1601     class Sat a
1602     class Data ctx a
1603     instance  Sat (ctx Char)             => Data ctx Char
1604     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1605
1606     class Data Maybe a => Foo a
1607
1608     instance Foo t => Sat (Maybe t)
1609
1610     instance Data Maybe a => Foo a
1611     instance Foo a        => Foo [a]
1612     instance                 Foo [Char]
1613
1614 In the instance for Foo [a], when generating evidence for the superclasses
1615 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1616 Using the instance for Data, we therefore need
1617         (Sat (Maybe [a], Data Maybe a)
1618 But we are given (Foo a), and hence its superclass (Data Maybe a).
1619 So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
1620 we need (Foo [a]).  And that is the very dictionary we are bulding
1621 an instance for!  So we must put that in the "givens".  So in this
1622 case we have
1623         Given:  Foo a, Foo [a]
1624         Wanted: Data Maybe [a]
1625
1626 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1627 the givens, which is what 'addGiven' would normally do. Why? Because
1628 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1629 by selecting a superclass from Foo [a], which simply makes a loop.
1630
1631 On the other hand we *must* put the superclasses of (Foo a) in
1632 the givens, as you can see from the derivation described above.
1633
1634 Conclusion: in the very special case of tcSimplifySuperClasses
1635 we have one 'given' (namely the "this" dictionary) whose superclasses
1636 must not be added to 'givens' by addGiven.
1637
1638 There is a complication though.  Suppose there are equalities
1639       instance (Eq a, a~b) => Num (a,b)
1640 Then we normalise the 'givens' wrt the equalities, so the original
1641 given "this" dictionary is cast to one of a different type.  So it's a
1642 bit trickier than before to identify the "special" dictionary whose
1643 superclasses must not be added. See test
1644    indexed-types/should_run/EqInInstance
1645
1646 We need a persistent property of the dictionary to record this
1647 special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
1648 but cool), which is maintained by dictionary normalisation.
1649 Specifically, the InstLocOrigin is
1650              NoScOrigin
1651 then the no-superclass thing kicks in.  WATCH OUT if you fiddle
1652 with InstLocOrigin!
1653
1654 Note [MATCHING-SYNONYMS]
1655 ~~~~~~~~~~~~~~~~~~~~~~~~
1656 When trying to match a dictionary (D tau) to a top-level instance, or a
1657 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1658 we do *not* need to expand type synonyms because the matcher will do that for us.
1659
1660
1661 Note [RHS-FAMILY-SYNONYMS]
1662 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1663 The RHS of a family instance is represented as yet another constructor which is
1664 like a type synonym for the real RHS the programmer declared. Eg:
1665     type instance F (a,a) = [a]
1666 Becomes:
1667     :R32 a = [a]      -- internal type synonym introduced
1668     F (a,a) ~ :R32 a  -- instance
1669
1670 When we react a family instance with a type family equation in the work list
1671 we keep the synonym-using RHS without expansion.
1672
1673
1674 *********************************************************************************
1675 *                                                                               *
1676                        The top-reaction Stage
1677 *                                                                               *
1678 *********************************************************************************
1679
1680 \begin{code}
1681 -- If a work item has any form of interaction with top-level we get this
1682 data TopInteractResult
1683   = NoTopInt         -- No top-level interaction
1684                      -- Equivalent to (SomeTopInt emptyWorkList (ContinueWith work_item))
1685   | SomeTopInt
1686       { tir_new_work  :: WorkList       -- Sub-goals or new work (could be given,
1687                                         --                        for superclasses)
1688       , tir_new_inert :: StopOrContinue -- The input work item, ready to become *inert* now:
1689       }                                 -- NB: in ``given'' (solved) form if the
1690                                         -- original was wanted or given and instance match
1691                                         -- was found, but may also be in wanted form if we
1692                                         -- only reacted with functional dependencies
1693                                         -- arising from top-level instances.
1694
1695 topReactionsStage :: SimplifierStage
1696 topReactionsStage depth workItem inerts
1697   = do { tir <- tryTopReact inerts workItem
1698              -- NB: we pass the inerts as well. See Note [Instance and Given overlap]
1699        ; case tir of
1700            NoTopInt ->
1701                return $ SR { sr_inerts   = inerts
1702                            , sr_new_work = emptyWorkList
1703                            , sr_stop     = ContinueWith workItem }
1704            SomeTopInt tir_new_work tir_new_inert ->
1705                do { bumpStepCountTcS
1706                   ; traceFireTcS depth (ptext (sLit "Top react")
1707                        <+> vcat [ ptext (sLit "Work =") <+> ppr workItem
1708                                 , ptext (sLit "New =") <+> ppr tir_new_work ])
1709                   ; return $ SR { sr_inerts   = inerts
1710                                 , sr_new_work = tir_new_work
1711                                 , sr_stop     = tir_new_inert
1712                                 } }
1713        }
1714
1715 tryTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1716 tryTopReact inerts workitem
1717   = do {  -- A flag controls the amount of interaction allowed
1718           -- See Note [Simplifying RULE lhs constraints]
1719          ctxt <- getTcSContext
1720        ; if allowedTopReaction (simplEqsOnly ctxt) workitem
1721          then do { traceTcS "tryTopReact / calling doTopReact" (ppr workitem)
1722                  ; doTopReact inerts workitem }
1723          else return NoTopInt
1724        }
1725
1726 allowedTopReaction :: Bool -> WorkItem -> Bool
1727 allowedTopReaction eqs_only (CDictCan {}) = not eqs_only
1728 allowedTopReaction _        _             = True
1729
1730 doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1731 -- The work item does not react with the inert set, so try interaction with top-level instances
1732 -- NB: The place to add superclasses in *not* in doTopReact stage. Instead superclasses are
1733 --     added in the worklist as part of the canonicalisation process.
1734 -- See Note [Adding superclasses] in TcCanonical.
1735
1736 -- Given dictionary
1737 -- See Note [Given constraint that matches an instance declaration]
1738 doTopReact _inerts (CDictCan { cc_flavor = Given {} })
1739   = return NoTopInt -- NB: Superclasses already added since it's canonical
1740
1741 -- Derived dictionary: just look for functional dependencies
1742 doTopReact _inerts workItem@(CDictCan { cc_flavor = Derived loc
1743                                       , cc_class = cls, cc_tyargs = xis })
1744   = do { instEnvs <- getInstEnvs
1745        ; let fd_eqns = improveFromInstEnv instEnvs
1746                                                 (ClassP cls xis, pprArisingAt loc)
1747        ; m <- rewriteWithFunDeps fd_eqns xis loc
1748        ; case m of
1749            Nothing -> return NoTopInt
1750            Just (xis',_,fd_work) ->
1751                let workItem' = workItem { cc_tyargs = xis' }
1752                    -- Deriveds are not supposed to have identity (cc_id is unused!)
1753                in do { fd_cans <- mkCanonicalFDAsDerived fd_work
1754                      ; return $ SomeTopInt { tir_new_work  = fd_cans
1755                                            , tir_new_inert = ContinueWith workItem' }
1756                      }
1757        }
1758
1759
1760 -- Wanted dictionary
1761 doTopReact inerts workItem@(CDictCan { cc_flavor = fl@(Wanted loc)
1762                                      , cc_class = cls, cc_tyargs = xis })
1763   -- See Note [MATCHING-SYNONYMS]
1764   = do { traceTcS "doTopReact" (ppr workItem)
1765        ; instEnvs <- getInstEnvs
1766        ; let fd_eqns = improveFromInstEnv instEnvs $ (ClassP cls xis, pprArisingAt loc)
1767
1768        ; any_fundeps <- rewriteWithFunDeps fd_eqns xis loc
1769        ; case any_fundeps of
1770            -- No Functional Dependencies
1771            Nothing ->
1772                do { lkup_inst_res  <- matchClassInst inerts cls xis loc
1773                   ; case lkup_inst_res of
1774                       GenInst wtvs ev_term
1775                           -> doSolveFromInstance wtvs ev_term workItem emptyWorkList
1776                       NoInstance
1777                           -> return NoTopInt
1778                   }
1779            -- Actual Functional Dependencies
1780            Just (xis',cos,fd_work) ->
1781                do { lkup_inst_res <- matchClassInst inerts cls xis' loc
1782                   ; case lkup_inst_res of
1783                       NoInstance
1784                           -> do { fd_cans <- mkCanonicalFDAsDerived fd_work
1785                                 ; return $
1786                                  SomeTopInt { tir_new_work  = fd_cans
1787                                              , tir_new_inert = ContinueWith workItem } }
1788                       -- This WHOLE branch is an optimization: we can immediately discharge the dictionary
1789                       GenInst wtvs ev_term
1790                           -> do { let dict_co = mkTyConAppCo (classTyCon cls) cos
1791                                 ; fd_cans <- mkCanonicalFDAsWanted fd_work
1792                                 ; dv' <- newDictVar cls xis'
1793                                 ; setDictBind dv' ev_term
1794                                 ; doSolveFromInstance wtvs (EvCast dv' dict_co) workItem fd_cans }
1795                   } }
1796
1797    where doSolveFromInstance :: [WantedEvVar]
1798                              -> EvTerm
1799                              -> CanonicalCt
1800                              -> WorkList -> TcS TopInteractResult
1801          -- Precondition: evidence term matches the predicate of cc_id of workItem
1802          doSolveFromInstance wtvs ev_term workItem extra_work
1803             | null wtvs
1804             = do { traceTcS "doTopReact/found nullary instance for" (ppr (cc_id workItem))
1805                  ; setDictBind (cc_id workItem) ev_term
1806                  ; return $ SomeTopInt { tir_new_work  = extra_work
1807                                        , tir_new_inert = Stop } }
1808             | otherwise
1809             = do { traceTcS "doTopReact/found non-nullary instance for" (ppr (cc_id workItem))
1810                  ; setDictBind (cc_id workItem) ev_term
1811                         -- Solved and new wanted work produced, you may cache the
1812                         -- (tentatively solved) dictionary as Solved given.
1813                  ; let solved    = workItem { cc_flavor = solved_fl }
1814                        solved_fl = mkSolvedFlavor fl UnkSkol
1815                  ; inst_work <- canWanteds wtvs
1816                  ; return $ SomeTopInt { tir_new_work  = inst_work `unionWorkList` extra_work
1817                                        , tir_new_inert = ContinueWith solved } }
1818
1819
1820 -- Type functions
1821 doTopReact _inerts (CFunEqCan { cc_flavor = fl })
1822   | Just GivenSolved <- isGiven_maybe fl
1823   = return NoTopInt -- If Solved, no more interactions should happen
1824
1825 -- Otherwise, it's a Given, Derived, or Wanted
1826 doTopReact _inerts workItem@(CFunEqCan { cc_id = cv, cc_flavor = fl
1827                                        , cc_fun = tc, cc_tyargs = args, cc_rhs = xi })
1828   = ASSERT (isSynFamilyTyCon tc)   -- No associated data families have reached that far
1829     do { match_res <- matchFam tc args -- See Note [MATCHING-SYNONYMS]
1830        ; case match_res of
1831            MatchInstNo -> return NoTopInt
1832            MatchInstSingle (rep_tc, rep_tys)
1833              -> do { let Just coe_tc = tyConFamilyCoercion_maybe rep_tc
1834                          Just rhs_ty = tcView (mkTyConApp rep_tc rep_tys)
1835                             -- Eagerly expand away the type synonym on the
1836                             -- RHS of a type function, so that it never
1837                             -- appears in an error message
1838                             -- See Note [Type synonym families] in TyCon
1839                          coe = mkAxInstCo coe_tc rep_tys
1840                    ; case fl of
1841                        Wanted {} -> do { cv' <- newCoVar rhs_ty xi
1842                                        ; setCoBind cv $ coe `mkTransCo` mkCoVarCo cv'
1843                                        ; can_cts <- mkCanonical fl cv'
1844                                        ; let solved = workItem { cc_flavor = solved_fl }
1845                                              solved_fl = mkSolvedFlavor fl UnkSkol
1846                                        ; if isEmptyWorkList can_cts then
1847                                               return (SomeTopInt can_cts Stop) -- No point in caching
1848                                          else return $
1849                                               SomeTopInt { tir_new_work = can_cts
1850                                                          , tir_new_inert = ContinueWith solved }
1851                                        }
1852                        Given {} -> do { cv' <- newGivenCoVar xi rhs_ty $
1853                                                mkSymCo (mkCoVarCo cv) `mkTransCo` coe
1854                                       ; can_cts <- mkCanonical fl cv'
1855                                       ; return $
1856                                         SomeTopInt { tir_new_work = can_cts
1857                                                    , tir_new_inert = Stop }
1858                                       }
1859                        Derived {} -> do { cv' <- newDerivedId (EqPred xi rhs_ty)
1860                                         ; can_cts <- mkCanonical fl cv'
1861                                         ; return $
1862                                           SomeTopInt { tir_new_work = can_cts
1863                                                      , tir_new_inert = Stop }
1864                                         }
1865                    }
1866            _
1867              -> panicTcS $ text "TcSMonad.matchFam returned multiple instances!"
1868        }
1869
1870
1871 -- Any other work item does not react with any top-level equations
1872 doTopReact _inerts _workItem = return NoTopInt
1873 \end{code}
1874
1875
1876 Note [FunDep and implicit parameter reactions]
1877 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1878 Currently, our story of interacting two dictionaries (or a dictionary
1879 and top-level instances) for functional dependencies, and implicit
1880 paramters, is that we simply produce new wanted equalities.  So for example
1881
1882         class D a b | a -> b where ...
1883     Inert:
1884         d1 :g D Int Bool
1885     WorkItem:
1886         d2 :w D Int alpha
1887
1888     We generate the extra work item
1889         cv :w alpha ~ Bool
1890     where 'cv' is currently unused.  However, this new item reacts with d2,
1891     discharging it in favour of a new constraint d2' thus:
1892         d2' :w D Int Bool
1893         d2 := d2' |> D Int cv
1894     Now d2' can be discharged from d1
1895
1896 We could be more aggressive and try to *immediately* solve the dictionary
1897 using those extra equalities. With the same inert set and work item we
1898 might dischard d2 directly:
1899
1900         cv :w alpha ~ Bool
1901         d2 := d1 |> D Int cv
1902
1903 But in general it's a bit painful to figure out the necessary coercion,
1904 so we just take the first approach. Here is a better example. Consider:
1905     class C a b c | a -> b
1906 And:
1907      [Given]  d1 : C T Int Char
1908      [Wanted] d2 : C T beta Int
1909 In this case, it's *not even possible* to solve the wanted immediately.
1910 So we should simply output the functional dependency and add this guy
1911 [but NOT its superclasses] back in the worklist. Even worse:
1912      [Given] d1 : C T Int beta
1913      [Wanted] d2: C T beta Int
1914 Then it is solvable, but its very hard to detect this on the spot.
1915
1916 It's exactly the same with implicit parameters, except that the
1917 "aggressive" approach would be much easier to implement.
1918
1919 Note [When improvement happens]
1920 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1921 We fire an improvement rule when
1922
1923   * Two constraints match (modulo the fundep)
1924       e.g. C t1 t2, C t1 t3    where C a b | a->b
1925     The two match because the first arg is identical
1926
1927   * At least one is not Given.  If they are both given, we don't fire
1928     the reaction because we have no way of constructing evidence for a
1929     new equality nor does it seem right to create a new wanted goal
1930     (because the goal will most likely contain untouchables, which
1931     can't be solved anyway)!
1932
1933 Note that we *do* fire the improvement if one is Given and one is Derived.
1934 The latter can be a superclass of a wanted goal. Example (tcfail138)
1935     class L a b | a -> b
1936     class (G a, L a b) => C a b
1937
1938     instance C a b' => G (Maybe a)
1939     instance C a b  => C (Maybe a) a
1940     instance L (Maybe a) a
1941
1942 When solving the superclasses of the (C (Maybe a) a) instance, we get
1943   Given:  C a b  ... and hance by superclasses, (G a, L a b)
1944   Wanted: G (Maybe a)
1945 Use the instance decl to get
1946   Wanted: C a b'
1947 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1948 and now we need improvement between that derived superclass an the Given (L a b)
1949
1950 Note [Overriding implicit parameters]
1951 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1952 Consider
1953    f :: (?x::a) -> Bool -> a
1954
1955    g v = let ?x::Int = 3
1956          in (f v, let ?x::Bool = True in f v)
1957
1958 This should probably be well typed, with
1959    g :: Bool -> (Int, Bool)
1960
1961 So the inner binding for ?x::Bool *overrides* the outer one.
1962 Hence a work-item Given overrides an inert-item Given.
1963
1964 Note [Given constraint that matches an instance declaration]
1965 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1966 What should we do when we discover that one (or more) top-level
1967 instances match a given (or solved) class constraint? We have
1968 two possibilities:
1969
1970   1. Reject the program. The reason is that there may not be a unique
1971      best strategy for the solver. Example, from the OutsideIn(X) paper:
1972        instance P x => Q [x]
1973        instance (x ~ y) => R [x] y
1974
1975        wob :: forall a b. (Q [b], R b a) => a -> Int
1976
1977        g :: forall a. Q [a] => [a] -> Int
1978        g x = wob x
1979
1980        will generate the impliation constraint:
1981             Q [a] => (Q [beta], R beta [a])
1982        If we react (Q [beta]) with its top-level axiom, we end up with a
1983        (P beta), which we have no way of discharging. On the other hand,
1984        if we react R beta [a] with the top-level we get  (beta ~ a), which
1985        is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1986        now solvable by the given Q [a].
1987
1988      However, this option is restrictive, for instance [Example 3] from
1989      Note [Recursive dictionaries] will fail to work.
1990
1991   2. Ignore the problem, hoping that the situations where there exist indeed
1992      such multiple strategies are rare: Indeed the cause of the previous
1993      problem is that (R [x] y) yields the new work (x ~ y) which can be
1994      *spontaneously* solved, not using the givens.
1995
1996 We are choosing option 2 below but we might consider having a flag as well.
1997
1998
1999 Note [New Wanted Superclass Work]
2000 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2001 Even in the case of wanted constraints, we may add some superclasses
2002 as new given work. The reason is:
2003
2004         To allow FD-like improvement for type families. Assume that
2005         we have a class
2006              class C a b | a -> b
2007         and we have to solve the implication constraint:
2008              C a b => C a beta
2009         Then, FD improvement can help us to produce a new wanted (beta ~ b)
2010
2011         We want to have the same effect with the type family encoding of
2012         functional dependencies. Namely, consider:
2013              class (F a ~ b) => C a b
2014         Now suppose that we have:
2015                given: C a b
2016                wanted: C a beta
2017         By interacting the given we will get given (F a ~ b) which is not
2018         enough by itself to make us discharge (C a beta). However, we
2019         may create a new derived equality from the super-class of the
2020         wanted constraint (C a beta), namely derived (F a ~ beta).
2021         Now we may interact this with given (F a ~ b) to get:
2022                   derived :  beta ~ b
2023         But 'beta' is a touchable unification variable, and hence OK to
2024         unify it with 'b', replacing the derived evidence with the identity.
2025
2026         This requires trySpontaneousSolve to solve *derived*
2027         equalities that have a touchable in their RHS, *in addition*
2028         to solving wanted equalities.
2029
2030 We also need to somehow use the superclasses to quantify over a minimal,
2031 constraint see note [Minimize by Superclasses] in TcSimplify.
2032
2033
2034 Finally, here is another example where this is useful.
2035
2036 Example 1:
2037 ----------
2038    class (F a ~ b) => C a b
2039 And we are given the wanteds:
2040       w1 : C a b
2041       w2 : C a c
2042       w3 : b ~ c
2043 We surely do *not* want to quantify over (b ~ c), since if someone provides
2044 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
2045 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
2046
2047      Step 1: We will get new *given* superclass work,
2048              provisionally to our solving of w1 and w2
2049
2050                g1: F a ~ b, g2 : F a ~ c,
2051                w1 : C a b, w2 : C a c, w3 : b ~ c
2052
2053              The evidence for g1 and g2 is a superclass evidence term:
2054
2055                g1 := sc w1, g2 := sc w2
2056
2057      Step 2: The givens will solve the wanted w3, so that
2058                w3 := sym (sc w1) ; sc w2
2059
2060      Step 3: Now, one may naively assume that then w2 can be solve from w1
2061              after rewriting with the (now solved equality) (b ~ c).
2062
2063              But this rewriting is ruled out by the isGoodRectDict!
2064
2065 Conclusion, we will (correctly) end up with the unsolved goals
2066     (C a b, C a c)
2067
2068 NB: The desugarer needs be more clever to deal with equalities
2069     that participate in recursive dictionary bindings.
2070
2071 \begin{code}
2072 data LookupInstResult
2073   = NoInstance
2074   | GenInst [WantedEvVar] EvTerm
2075
2076 matchClassInst :: InertSet -> Class -> [Type] -> WantedLoc -> TcS LookupInstResult
2077 matchClassInst inerts clas tys loc
2078    = do { let pred = mkClassPred clas tys
2079         ; mb_result <- matchClass clas tys
2080         ; untch <- getUntouchables
2081         ; case mb_result of
2082             MatchInstNo   -> return NoInstance
2083             MatchInstMany -> return NoInstance -- defer any reactions of a multitude until
2084                                                -- we learn more about the reagent
2085             MatchInstSingle (_,_)
2086               | given_overlap untch ->
2087                   do { traceTcS "Delaying instance application" $
2088                        vcat [ text "Workitem=" <+> pprPredTy (ClassP clas tys)
2089                             , text "Silents and their superclasses=" <+> ppr silents_and_their_scs
2090                             , text "All given dictionaries=" <+> ppr all_given_dicts ]
2091                      ; return NoInstance -- see Note [Instance and Given overlap]
2092                      }
2093
2094             MatchInstSingle (dfun_id, mb_inst_tys) ->
2095               do { checkWellStagedDFun pred dfun_id loc
2096
2097         -- It's possible that not all the tyvars are in
2098         -- the substitution, tenv. For example:
2099         --      instance C X a => D X where ...
2100         -- (presumably there's a functional dependency in class C)
2101         -- Hence mb_inst_tys :: Either TyVar TcType
2102
2103                  ; tys <- instDFunTypes mb_inst_tys
2104                  ; let (theta, _) = tcSplitPhiTy (applyTys (idType dfun_id) tys)
2105                  ; if null theta then
2106                        return (GenInst [] (EvDFunApp dfun_id tys []))
2107                    else do
2108                      { ev_vars <- instDFunConstraints theta
2109                      ; let wevs = [EvVarX w loc | w <- ev_vars]
2110                      ; return $ GenInst wevs (EvDFunApp dfun_id tys ev_vars) }
2111                  }
2112         }
2113    where given_overlap :: TcsUntouchables -> Bool
2114          given_overlap untch
2115            = foldlBag (\r d -> r || matchable untch d) False all_given_dicts
2116
2117          matchable untch (CDictCan { cc_class = clas', cc_tyargs = sys, cc_flavor = fl })
2118            | Just GivenOrig <- isGiven_maybe fl
2119            , clas' == clas
2120            , does_not_originate_in_a_silent clas' sys
2121            = case tcUnifyTys (\tv -> if isTouchableMetaTyVar_InRange untch tv &&
2122                                         tv `elemVarSet` tyVarsOfTypes tys
2123                                      then BindMe else Skolem) tys sys of
2124            -- We can't learn anything more about any variable at this point, so the only
2125            -- cause of overlap can be by an instantiation of a touchable unification
2126            -- variable. Hence we only bind touchable unification variables. In addition,
2127            -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
2128                 Nothing -> False
2129                 Just _  -> True
2130            | otherwise = False -- No overlap with a solved, already been taken care of
2131                                -- by the overlap check with the instance environment.
2132          matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
2133
2134          does_not_originate_in_a_silent clas sys
2135              -- UGLY: See Note [Silent parameters overlapping]
2136            = null $ filter (eqPred (ClassP clas sys)) silents_and_their_scs
2137
2138          silents_and_their_scs
2139            = foldlBag (\acc rvnt -> case rvnt of
2140                         CDictCan { cc_id = d, cc_class = c, cc_tyargs = s }
2141                          | isSilentEvVar d -> (ClassP c s) : (transSuperClasses c s) ++ acc
2142                         _ -> acc) [] all_given_dicts
2143
2144          -- TODO:
2145          -- When silent parameters will go away we should simply select from
2146          -- the given map of the inert set.
2147          all_given_dicts = Map.fold unionBags emptyCCan (cts_given $ inert_dicts inerts)
2148
2149 \end{code}
2150
2151 Note [Silent parameters overlapping]
2152 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2153 DV 12/05/2011:
2154 The long-term goal is to completely remove silent superclass
2155 parameters when checking instance declarations. But until then we must
2156 make sure that we never prevent the application of an instance
2157 declaration because of a potential match from a silent parameter --
2158 after all we are supposed to have solved that silent parameter from
2159 some instance, anyway! In effect silent parameters behave more like
2160 Solved than like Given.
2161
2162 A concrete example appears in typecheck/SilentParametersOverlapping.hs
2163
2164 Note [Instance and Given overlap]
2165 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2166 Assume that we have an inert set that looks as follows:
2167        [Given] D [Int]
2168 And an instance declaration:
2169        instance C a => D [a]
2170 A new wanted comes along of the form:
2171        [Wanted] D [alpha]
2172
2173 One possibility is to apply the instance declaration which will leave us
2174 with an unsolvable goal (C alpha). However, later on a new constraint may
2175 arise (for instance due to a functional dependency between two later dictionaries),
2176 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
2177 will be transformed to [Wanted] D [Int], which could have been discharged by the given.
2178
2179 The solution is that in matchClassInst and eventually in topReact, we get back with
2180 a matching instance, only when there is no Given in the inerts which is unifiable to
2181 this particular dictionary.
2182
2183 The end effect is that, much as we do for overlapping instances, we delay choosing a
2184 class instance if there is a possibility of another instance OR a given to match our
2185 constraint later on. This fixes bugs #4981 and #5002.
2186
2187 This is arguably not easy to appear in practice due to our aggressive prioritization
2188 of equality solving over other constraints, but it is possible. I've added a test case
2189 in typecheck/should-compile/GivenOverlapping.hs
2190
2191 Moreover notice that our goals here are different than the goals of the top-level
2192 overlapping checks. There we are interested in validating the following principle:
2193
2194     If we inline a function f at a site where the same global instance environment
2195     is available as the instance environment at the definition site of f then we
2196     should get the same behaviour.
2197
2198 But for the Given Overlap check our goal is just related to completeness of
2199 constraint solving.
2200
2201
2202
2203