compiler/typecheck/TcInteract.lhs

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