compiler/typecheck/TcInteract.lhs

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