compiler/typecheck/TcInteract.lhs

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