TcInteract.lhs 88.3 KB
Newer Older
1
\begin{code}
Ian Lynagh's avatar
Ian Lynagh committed
2 3 4 5 6 7 8
{-# OPTIONS -fno-warn-tabs #-}
-- The above warning supression flag is a temporary kludge.
-- While working on this module you are encouraged to remove it and
-- detab the module (please do the detabbing in a separate patch). See
--     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
-- for details

9
module TcInteract ( 
10 11
     solveInteractGiven,  -- Solves [EvVar],GivenLoc
     solveInteractCts,    -- Solves [Cts]
12 13 14 15
  ) where  

#include "HsVersions.h"

16

17
import BasicTypes ()
18 19 20
import TcCanonical
import VarSet
import Type
dimitris's avatar
dimitris committed
21
import Unify
22 23
import FamInstEnv
import Coercion( mkAxInstRHS )
24 25 26 27 28

import Id 
import Var

import TcType
29
import PrelNames (typeNatClassName, typeStringClassName)
30

31 32
import Class
import TyCon
33
import Name
34
import IParam
35

dimitris's avatar
dimitris committed
36
import TysWiredIn ( eqTyCon )
37 38
import FunDeps

39
import TcEvidence
40 41
import Outputable

42 43
import TcMType ( zonkTcPredType )

44
import TcRnTypes
45
import TcErrors
46
import TcSMonad
47
import Maybes( orElse )
48
import Bag
49

50 51 52
import Control.Monad ( foldM )
import TrieMap

dimitris's avatar
dimitris committed
53 54 55
import VarEnv
import qualified Data.Traversable as Traversable

56
import Control.Monad( when )
57
import Pair ( pSnd )
58
import UniqFM
59 60 61
import FastString ( sLit ) 
import DynFlags
\end{code}
62 63
**********************************************************************
*                                                                    * 
64 65 66 67
*                      Main Interaction Solver                       *
*                                                                    *
**********************************************************************

68 69
Note [Basic Simplifier Plan] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
70

71 72
1. Pick an element from the WorkList if there exists one with depth 
   less thanour context-stack depth. 
73

74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
2. Run it down the 'stage' pipeline. Stages are: 
      - canonicalization
      - inert reactions
      - spontaneous reactions
      - top-level intreactions
   Each stage returns a StopOrContinue and may have sideffected 
   the inerts or worklist.
  
   The threading of the stages is as follows: 
      - If (Stop) is returned by a stage then we start again from Step 1. 
      - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to 
        the next stage in the pipeline. 
4. If the element has survived (i.e. ContinueWith x) the last stage 
   then we add him in the inerts and jump back to Step 1.

If in Step 1 no such element exists, we have exceeded our context-stack 
depth and will simply fail.
91 92
\begin{code}

93 94
solveInteractCts :: [Ct] -> TcS ()
solveInteractCts cts 
dimitris's avatar
dimitris committed
95 96 97 98
  = do { traceTcS "solveInteractCtS" (vcat [ text "cts =" <+> ppr cts ]) 
       ; updWorkListTcS (appendWorkListCt cts) >> solveInteract }

{- DELETEME 
99 100 101 102 103 104 105 106
  = do { evvar_cache <- getTcSEvVarCacheMap
       ; (cts_thinner, new_evvar_cache) <- add_cts_in_cache evvar_cache cts
       ; traceTcS "solveInteractCts" (vcat [ text "cts_original =" <+> ppr cts, 
                                             text "cts_thinner  =" <+> ppr cts_thinner
                                           ])
       ; setTcSEvVarCacheMap new_evvar_cache 
       ; updWorkListTcS (appendWorkListCt cts_thinner) >> solveInteract }
 
107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
  where 
    add_cts_in_cache evvar_cache cts
      = do { ctxt <- getTcSContext
           ; foldM (solve_or_cache (simplEqsOnly ctxt)) ([],evvar_cache) cts }

    solve_or_cache :: Bool    -- Solve equalities only, not classes etc
                   -> ([Ct],TypeMap (EvVar,CtFlavor)) 
                   -> Ct
                   -> TcS ([Ct],TypeMap (EvVar,CtFlavor))
    solve_or_cache eqs_only (acc_cts,acc_cache) ct
      | dont_cache eqs_only (classifyPredType pred_ty)
      = return (ct:acc_cts,acc_cache) 

      | Just (ev',fl') <- lookupTM pred_ty acc_cache
      , fl' `canSolve` fl
      , isWanted fl
      = do { _ <- setEvBind ev (EvId ev') fl
           ; return (acc_cts,acc_cache) }

      | otherwise -- If it's a given keep it in the work list, even if it exists in the cache!
      = return (ct:acc_cts, alterTM pred_ty (\_ -> Just (ev,fl)) acc_cache)
      where fl = cc_flavor ct
            ev = cc_id ct
            pred_ty = ctPred ct

    dont_cache :: Bool -> PredTree -> Bool
    -- Do not use the cache, not update it, if this is true
    dont_cache _ (IPPred {}) = True    -- IPPreds have subtle shadowing
    dont_cache _ (EqPred ty1 ty2)      -- Report Int ~ Bool errors separately
      | Just tc1 <- tyConAppTyCon_maybe ty1
      , Just tc2 <- tyConAppTyCon_maybe ty2
      , tc1 /= tc2
      = isDecomposableTyCon tc1 && isDecomposableTyCon tc2
      | otherwise = False
    dont_cache eqs_only _ = eqs_only
            -- If we are simplifying equalities only, 
            -- do not cache non-equalities
            -- See Note [Simplifying RULE lhs constraints] in TcSimplify
dimitris's avatar
dimitris committed
145
-}
146 147 148 149

solveInteractGiven :: GivenLoc -> [EvVar] -> TcS () 
solveInteractGiven gloc evs
  = solveInteractCts (map mk_noncan evs)
dimitris's avatar
dimitris committed
150
  where mk_noncan ev = CNonCanonical { cc_flavor = Given gloc ev
151 152 153 154 155 156 157
                                     , cc_depth = 0 }

-- The main solver loop implements Note [Basic Simplifier Plan]
---------------------------------------------------------------
solveInteract :: TcS ()
-- Returns the final InertSet in TcS, WorkList will be eventually empty.
solveInteract
158 159
  = {-# SCC "solveInteract" #-}
    do { dyn_flags <- getDynFlags
160 161
       ; let max_depth = ctxtStkDepth dyn_flags
             solve_loop
162 163
              = {-# SCC "solve_loop" #-}
                do { sel <- selectNextWorkItem max_depth
164 165 166 167
                   ; case sel of 
                      NoWorkRemaining     -- Done, successfuly (modulo frozen)
                        -> return ()
                      MaxDepthExceeded ct -- Failure, depth exceeded
168
                        -> wrapErrTcS $ solverDepthErrorTcS (cc_depth ct) [ct]
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188
                      NextWorkItem ct     -- More work, loop around!
                        -> runSolverPipeline thePipeline ct >> solve_loop }
       ; solve_loop }

type WorkItem = Ct
type SimplifierStage = WorkItem -> TcS StopOrContinue

continueWith :: WorkItem -> TcS StopOrContinue
continueWith work_item = return (ContinueWith work_item) 

data SelectWorkItem 
       = NoWorkRemaining      -- No more work left (effectively we're done!)
       | MaxDepthExceeded Ct  -- More work left to do but this constraint has exceeded
                              -- the max subgoal depth and we must stop 
       | NextWorkItem Ct      -- More work left, here's the next item to look at 

selectNextWorkItem :: SubGoalDepth -- Max depth allowed
                   -> TcS SelectWorkItem
selectNextWorkItem max_depth
  = updWorkListTcS_return pick_next
189
  where 
190
    pick_next :: WorkList -> (SelectWorkItem, WorkList)
dimitris's avatar
dimitris committed
191 192 193 194 195 196 197 198
    pick_next wl = case selectWorkItem wl of
                     (Nothing,_) 
                         -> (NoWorkRemaining,wl)           -- No more work
                     (Just ct, new_wl) 
                         | cc_depth ct > max_depth         -- Depth exceeded
                         -> (MaxDepthExceeded ct,new_wl)
                     (Just ct, new_wl) 
                         -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231

runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline 
                  -> WorkItem                   -- The work item 
                  -> TcS () 
-- Run this item down the pipeline, leaving behind new work and inerts
runSolverPipeline pipeline workItem 
  = do { initial_is <- getTcSInerts 
       ; traceTcS "Start solver pipeline {" $ 
                  vcat [ ptext (sLit "work item = ") <+> ppr workItem 
                       , ptext (sLit "inerts    = ") <+> ppr initial_is]

       ; final_res  <- run_pipeline pipeline (ContinueWith workItem)

       ; final_is <- getTcSInerts
       ; case final_res of 
           Stop            -> do { traceTcS "End solver pipeline (discharged) }" 
                                       (ptext (sLit "inerts    = ") <+> ppr final_is)
                                 ; return () }
           ContinueWith ct -> do { traceTcS "End solver pipeline (not discharged) }" $
                                       vcat [ ptext (sLit "final_item = ") <+> ppr ct
                                            , ptext (sLit "inerts     = ") <+> ppr final_is]
                                 ; updInertSetTcS ct }
       }
  where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
        run_pipeline [] res = return res 
        run_pipeline _ Stop = return Stop 
        run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
          = do { traceTcS ("runStage " ++ stg_name ++ " {")
                          (text "workitem   = " <+> ppr ct) 
               ; res <- stg ct 
               ; traceTcS ("end stage " ++ stg_name ++ " }") empty
               ; run_pipeline stgs res 
               }
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257
\end{code}

Example 1:
  Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
  Reagent: a ~ [b] (given)

React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []

Example 2:
  Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
  Reagent: a ~w [b]

React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
etc.

Example 3:
  Inert:  {a ~ Int, F Int ~ b} (given)
  Reagent: F a ~ b (wanted)

React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing

\begin{code}
258 259 260 261 262
thePipeline :: [(String,SimplifierStage)]
thePipeline = [ ("canonicalization",        canonicalizationStage)
              , ("spontaneous solve",       spontaneousSolveStage)
              , ("interact with inerts",    interactWithInertsStage)
              , ("top-level reactions",     topReactionsStage) ]
263 264 265 266
\end{code}


\begin{code}
267

dimitris's avatar
dimitris committed
268

269 270 271 272
-- The canonicalization stage, see TcCanonical for details
----------------------------------------------------------
canonicalizationStage :: SimplifierStage
canonicalizationStage = TcCanonical.canonicalize 
273

274 275 276 277 278 279 280 281
\end{code}

*********************************************************************************
*                                                                               * 
                       The spontaneous-solve Stage
*                                                                               *
*********************************************************************************

282 283 284 285 286 287
Note [Efficient Orientation] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

There are two cases where we have to be careful about 
orienting equalities to get better efficiency. 

288
Case 1: In Rewriting Equalities (function rewriteEqLHS) 
289

290 291 292 293 294 295 296 297 298 299
    When rewriting two equalities with the same LHS:
          (a)  (tv ~ xi1) 
          (b)  (tv ~ xi2) 
    We have a choice of producing work (xi1 ~ xi2) (up-to the
    canonicalization invariants) However, to prevent the inert items
    from getting kicked out of the inerts first, we prefer to
    canonicalize (xi1 ~ xi2) if (b) comes from the inert set, or (xi2
    ~ xi1) if (a) comes from the inert set.
    
    This choice is implemented using the WhichComesFromInert flag. 
300

301 302 303 304 305
Case 2: Functional Dependencies 
    Again, we should prefer, if possible, the inert variables on the RHS

Case 3: IP improvement work
    We must always rewrite so that the inert type is on the right. 
306

307 308
\begin{code}
spontaneousSolveStage :: SimplifierStage 
309
spontaneousSolveStage workItem
310
  = do { mSolve <- trySpontaneousSolve workItem
311
       ; spont_solve mSolve } 
312 313 314 315 316 317 318
  where spont_solve SPCantSolve 
          | isCTyEqCan workItem                    -- Unsolved equality
          = do { kickOutRewritableInerts workItem  -- NB: will add workItem in inerts
               ; return Stop }
          | otherwise
          = continueWith workItem
        spont_solve (SPSolved workItem')           -- Post: workItem' must be equality
319 320 321 322
          = do { bumpStepCountTcS
               ; traceFireTcS (cc_depth workItem) $
                 ptext (sLit "Spontaneous") 
                           <+> parens (ppr (cc_flavor workItem)) <+> ppr workItem
323 324 325 326

                 -- NB: will add the item in the inerts
               ; kickOutRewritableInerts workItem'
               -- .. and Stop
327 328 329 330
               ; return Stop }

kickOutRewritableInerts :: Ct -> TcS () 
-- Pre:  ct is a CTyEqCan 
331 332 333
-- Post: The TcS monad is left with the thinner non-rewritable inerts; but which
--       contains the new constraint.
--       The rewritable end up in the worklist
dimitris's avatar
dimitris committed
334
kickOutRewritableInerts ct
335
  = {-# SCC "kickOutRewritableInerts" #-}
dimitris's avatar
dimitris committed
336 337
    do { traceTcS "kickOutRewritableInerts" $ text "workitem = " <+> ppr ct
       ; (wl,ieqs) <- {-# SCC "kick_out_rewritable" #-}
338
                      modifyInertTcS (kick_out_rewritable ct)
dimitris's avatar
dimitris committed
339 340 341
       ; traceTcS "Kicked out the following constraints" $ ppr wl
       ; is <- getTcSInerts 
       ; traceTcS "Remaining inerts are" $ ppr is
342

dimitris's avatar
dimitris committed
343 344 345 346 347
       -- Step 1: Rewrite as many of the inert_eqs on the spot!
       -- NB: if it is a given constraint just use the cached evidence
       -- to optimize e.g. mkRefl coercions from spontaneously solved cts.
       ; bnds <- getTcEvBindsMap
       ; let ct_coercion = getCtCoercion bnds ct 
348 349

       ; new_ieqs <- {-# SCC "rewriteInertEqsFromInertEq" #-}
dimitris's avatar
dimitris committed
350 351 352 353 354 355 356 357 358 359 360
                     rewriteInertEqsFromInertEq (cc_tyvar ct,
                                                 ct_coercion,cc_flavor ct) ieqs
       ; let upd_eqs is = is { inert_cans = new_ics }
                        where ics     = inert_cans is
                              new_ics = ics { inert_eqs = new_ieqs }
       ; modifyInertTcS (\is -> ((), upd_eqs is)) 
         
       ; is <- getTcSInerts 
       ; traceTcS "Final inerts are" $ ppr is
       
         -- Step 2: Add the new guy in
361
       ; updInertSetTcS ct
362 363 364

       ; traceTcS "Kick out" (ppr ct $$ ppr wl)
       ; updWorkListTcS (unionWorkList wl) }
dimitris's avatar
dimitris committed
365

366
rewriteInertEqsFromInertEq :: (TcTyVar, TcCoercion, CtFlavor) -- A new substitution
dimitris's avatar
dimitris committed
367 368
                           -> TyVarEnv Ct                     -- All the inert equalities
                           -> TcS (TyVarEnv Ct)               -- The new inert equalities
369
rewriteInertEqsFromInertEq (subst_tv, subst_co, subst_fl) ieqs
370 371 372 373 374
-- The goal: traverse the inert equalities and rewrite some of them, dropping some others
-- back to the worklist. This is delicate, see Note [Delicate equality kick-out]
 = do { mieqs <- Traversable.mapM do_one ieqs 
      ; traceTcS "Original inert equalities:" (ppr ieqs)
      ; let flatten_justs elem venv
dimitris's avatar
dimitris committed
375
              | Just act <- elem = extendVarEnv venv (cc_tyvar act) act
376 377 378 379
              | otherwise = venv                                     
            final_ieqs = foldVarEnv flatten_justs emptyVarEnv mieqs
      ; traceTcS "Remaining inert equalities:" (ppr final_ieqs)
      ; return final_ieqs }
380

dimitris's avatar
dimitris committed
381
 where do_one ct
382
         | subst_fl `canRewrite` fl && (subst_tv `elemVarSet` tyVarsOfCt ct) 
dimitris's avatar
dimitris committed
383 384 385
           -- Annoyingly inefficient, but we can't simply check 
           -- that isReflCo co because of cached solved ReflCo evidence.
         = if fl `canRewrite` subst_fl then
386 387
               -- If also the inert can rewrite the subst it's totally safe 
               -- to rewrite on the spot
dimitris's avatar
dimitris committed
388 389
               do { ct' <- rewrite_on_the_spot ct
                  ; return $ Just ct' }
390 391 392 393
           else -- We have to throw inert back to worklist for occurs checks 
              do { updWorkListTcS (extendWorkListEq ct)
                 ; return Nothing }
         | otherwise -- Just keep it there
dimitris's avatar
dimitris committed
394
         = return $ Just ct
395
         where 
dimitris's avatar
dimitris committed
396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424
           -- We have that:    subst_co :: subst_tv ~ tau
           -- An an old inert: tv ~ rhs
           -- That we want to rewrite on-the-spot to tv ~ rhs[tau/subst_tv]
           fl  = cc_flavor ct
           tv  = cc_tyvar ct
           rhs = cc_rhs ct
           
           rewrite_on_the_spot ct
             = do { let rhs_co = liftTcCoSubstWith [subst_tv] [subst_co] rhs
                        eq_co  = mkTcTyConAppCo eqTyCon $ 
                                   [ mkTcReflCo (typeKind rhs)
                                   , mkTcReflCo (mkTyVarTy tv)
                                   , mkTcSymCo rhs_co ]
                        new_rhs = pSnd (tcCoercionKind rhs_co)
                        new_eq_pred = mkTcEqPred (mkTyVarTy tv) new_rhs
                        -- eq_co ::  (tv ~ rhs[s/x]) ~ (tv ~ rhs[x])
                        
                  ; mb_fl <- rewriteCtFlavor fl new_eq_pred eq_co
                  ; case mb_fl of
                       Just new_fl -> return $
                                      ct {cc_flavor=new_fl,cc_rhs=new_rhs}
                       Nothing -> -- Weird, rewritten constraint was solved
                                  -- before -- I am uncertain about what to do
                         pprPanic "Interesting: \
                                   rewrote inert equality to existing!" $ 
                                   vcat [ text "original   ="<+>ppr ct
                                        , text "new eqpred ="<+>ppr new_eq_pred ]
                  }
{- DELETEME 
425
             = do { let rhs' = pSnd (tcCoercionKind co)
426 427
                  ; delCachedEvVar ev fl
                  ; evc <- newEqVar fl (mkTyVarTy tv) rhs'
428 429
                  ; let ev'   = evc_the_evvar evc
                  ; let evco' = mkTcCoVarCo ev' 
430 431 432
                  ; fl' <- if isNewEvVar evc then
                               do { case fl of 
                                      Wanted {} 
433
                                        -> setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl
434
                                      Given {} 
435
                                        -> setEqBind ev' (mkTcCoVarCo ev `mkTcTransCo` co) fl
436 437 438 439
                                      Derived {}
                                        -> return fl }
                           else
                               if isWanted fl then 
440
                                   setEqBind ev (evco' `mkTcTransCo` mkTcSymCo co) fl
441 442 443 444
                               else return fl
                  ; let ct' = ct { cc_id = ev', cc_flavor = fl', cc_rhs = rhs' }
                  ; return (ct',evco') }
           ev  = cc_id ct
dimitris's avatar
dimitris committed
445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460
-}

kick_out_rewritable :: Ct 
                    -> InertSet 
                    -> ((WorkList, TyVarEnv Ct),InertSet)
-- Post: returns ALL inert equalities, to be dealt with later
-- 
kick_out_rewritable ct is@(IS { inert_cans = 
                                   IC { inert_eqs    = eqmap
                                      , inert_eq_tvs = inscope
                                      , inert_dicts  = dictmap
                                      , inert_ips    = ipmap
                                      , inert_funeqs = funeqmap
                                      , inert_irreds = irreds }
                              , inert_frozen = frozen })
  = ((kicked_out,eqmap), remaining)
461
  where
462
    kicked_out = WorkList { wl_eqs    = []
dimitris's avatar
dimitris committed
463 464 465
                          , wl_funeqs = bagToList feqs_out
                          , wl_rest   = bagToList (fro_out `andCts` dicts_out 
                                          `andCts` ips_out `andCts` irs_out) }
466
  
dimitris's avatar
dimitris committed
467 468 469 470 471 472 473 474 475 476 477 478
    remaining = is { inert_cans = IC { inert_eqs = emptyVarEnv
                                     , inert_eq_tvs = inscope 
                                       -- keep the same, safe and cheap
                                     , inert_dicts = dicts_in
                                     , inert_ips = ips_in
                                     , inert_funeqs = feqs_in
                                     , inert_irreds = irs_in }
                   , inert_frozen = fro_in } 
                -- NB: Notice that don't rewrite 
                -- inert_solved, inert_flat_cache and inert_solved_funeqs
                -- optimistically. But when we lookup we have to take the 
                -- subsitution into account
479 480
    fl = cc_flavor ct
    tv = cc_tyvar ct
481 482
                               
    (ips_out,   ips_in)     = partitionCCanMap rewritable ipmap
483

dimitris's avatar
dimitris committed
484
    (feqs_out,  feqs_in)    = partCtFamHeadMap rewritable funeqmap
485
    (dicts_out, dicts_in)   = partitionCCanMap rewritable dictmap
486 487 488

    (irs_out,   irs_in)   = partitionBag rewritable irreds
    (fro_out,   fro_in)   = partitionBag rewritable frozen
dimitris's avatar
dimitris committed
489 490

    rewritable ct = (fl `canRewrite` cc_flavor ct)  &&
491 492 493 494 495 496 497 498 499 500
                    (tv `elemVarSet` tyVarsOfCt ct) 
                    -- NB: tyVarsOfCt will return the type 
                    --     variables /and the kind variables/ that are 
                    --     directly visible in the type. Hence we will
                    --     have exposed all the rewriting we care about
                    --     to make the most precise kinds visible for 
                    --     matching classes etc. No need to kick out 
                    --     constraints that mention type variables whose
                    --     kinds could contain this variable!

501
\end{code}
502

503 504
Note [Delicate equality kick-out]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
dimitris's avatar
dimitris committed
505

506 507 508 509 510
Delicate:
When kicking out rewritable constraints, it would be safe to simply
kick out all rewritable equalities, but instead we only kick out those
that, when rewritten, may result in occur-check errors. We rewrite the
rest on the spot. Example:
511

512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529
          WorkItem =   [S] a ~ b
          Inerts   = { [W] b ~ [a] }
Now at this point the work item cannot be further rewritten by the
inert (due to the weaker inert flavor), so we are examining if we can
instead rewrite the inert from the workitem. But if we rewrite it on
the spot we have to recanonicalize because of the danger of occurs
errors.  On the other hand if the inert flavor was just as powerful or
more powerful than the workitem flavor, the work-item could not have
reached this stage (because it would have already been rewritten by
the inert).

The coclusion is: we kick out the 'dangerous' equalities that may
require recanonicalization (occurs checks) and the rest we rewrite
unconditionally without further checks, on-the-spot with function
rewriteInertEqsFromInertEq.


\begin{code}
530 531
data SPSolveResult = SPCantSolve
                   | SPSolved WorkItem 
532

533 534 535
-- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
-- SPSolved workItem' gives us a new *given* to go on 

536
-- @trySpontaneousSolve wi@ solves equalities where one side is a
537
-- touchable unification variable.
538
--     	    See Note [Touchables and givens] 
539
trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
dimitris's avatar
dimitris committed
540
trySpontaneousSolve workItem@(CTyEqCan { cc_flavor = gw
541
                                       , cc_tyvar = tv1, cc_rhs = xi, cc_depth = d })
dimitris's avatar
dimitris committed
542
  | isGivenOrSolved gw
543
  = return SPCantSolve
544 545 546 547
  | Just tv2 <- tcGetTyVar_maybe xi
  = do { tch1 <- isTouchableMetaTyVar tv1
       ; tch2 <- isTouchableMetaTyVar tv2
       ; case (tch1, tch2) of
dimitris's avatar
dimitris committed
548 549 550
           (True,  True)  -> trySpontaneousEqTwoWay d gw tv1 tv2
           (True,  False) -> trySpontaneousEqOneWay d gw tv1 xi
           (False, True)  -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
551
	   _ -> return SPCantSolve }
552 553
  | otherwise
  = do { tch1 <- isTouchableMetaTyVar tv1
dimitris's avatar
dimitris committed
554
       ; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
555 556
                 else do { traceTcS "Untouchable LHS, can't spontaneously solve workitem:" $
                           ppr workItem 
557
                         ; return SPCantSolve }
558
       }
559 560 561 562

  -- No need for 
  --      trySpontaneousSolve (CFunEqCan ...) = ...
  -- See Note [No touchables as FunEq RHS] in TcSMonad
563
trySpontaneousSolve _ = return SPCantSolve
564 565

----------------
566
trySpontaneousEqOneWay :: SubGoalDepth 
dimitris's avatar
dimitris committed
567
                       -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
568
-- tv is a MetaTyVar, not untouchable
dimitris's avatar
dimitris committed
569
trySpontaneousEqOneWay d gw tv xi
570
  | not (isSigTyVar tv) || isTyVarTy xi
dimitris's avatar
dimitris committed
571
  = solveWithIdentity d gw tv xi
572
  | otherwise -- Still can't solve, sig tyvar and non-variable rhs
573
  = return SPCantSolve
574 575

----------------
576
trySpontaneousEqTwoWay :: SubGoalDepth 
dimitris's avatar
dimitris committed
577
                       -> CtFlavor -> TcTyVar -> TcTyVar -> TcS SPSolveResult
578
-- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
579

dimitris's avatar
dimitris committed
580
trySpontaneousEqTwoWay d gw tv1 tv2
Simon Peyton Jones's avatar
Simon Peyton Jones committed
581
  = do { let k1_sub_k2 = k1 `tcIsSubKind` k2
dreixel's avatar
dreixel committed
582
       ; if k1_sub_k2 && nicer_to_update_tv2
dimitris's avatar
dimitris committed
583 584
         then solveWithIdentity d gw tv2 (mkTyVarTy tv1)
         else solveWithIdentity d gw tv1 (mkTyVarTy tv2) }
585 586 587 588 589 590
  where
    k1 = tyVarKind tv1
    k2 = tyVarKind tv2
    nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
\end{code}

591 592 593 594
Note [Kind errors] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider the wanted problem: 
      alpha ~ (# Int, Int #) 
595
where alpha :: ArgKind and (# Int, Int #) :: (#). We can't spontaneously solve this constraint, 
596
but we should rather reject the program that give rise to it. If 'trySpontaneousEqTwoWay' 
597
simply returns @CantSolve@ then that wanted constraint is going to propagate all the way and 
598
get quantified over in inference mode. That's bad because we do know at this point that the 
599
constraint is insoluble. Instead, we call 'recKindErrorTcS' here, which will fail later on.
600 601

The same applies in canonicalization code in case of kind errors in the givens. 
602

603
However, when we canonicalize givens we only check for compatibility (@compatKind@). 
604
If there were a kind error in the givens, this means some form of inconsistency or dead code.
605

606 607 608 609 610
You may think that when we spontaneously solve wanteds we may have to look through the 
bindings to determine the right kind of the RHS type. E.g one may be worried that xi is 
@alpha@ where alpha :: ? and a previous spontaneous solving has set (alpha := f) with (f :: *).
But we orient our constraints so that spontaneously solved ones can rewrite all other constraint
so this situation can't happen. 
611

612 613
Note [Spontaneous solving and kind compatibility] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
614 615 616
Note that our canonical constraints insist that *all* equalities (tv ~
xi) or (F xis ~ rhs) require the LHS and the RHS to have *compatible*
the same kinds.  ("compatible" means one is a subKind of the other.)
617

618 619 620 621 622 623 624 625 626 627 628 629 630 631
  - It can't be *equal* kinds, because
     b) wanted constraints don't necessarily have identical kinds
               eg   alpha::? ~ Int
     b) a solved wanted constraint becomes a given

  - SPJ thinks that *given* constraints (tv ~ tau) always have that
    tau has a sub-kind of tv; and when solving wanted constraints
    in trySpontaneousEqTwoWay we re-orient to achieve this.

  - Note that the kind invariant is maintained by rewriting.
    Eg wanted1 rewrites wanted2; if both were compatible kinds before,
       wanted2 will be afterwards.  Similarly givens.

Caveat:
632 633 634 635 636 637 638 639 640
  - Givens from higher-rank, such as: 
          type family T b :: * -> * -> * 
          type instance T Bool = (->) 

          f :: forall a. ((T a ~ (->)) => ...) -> a -> ... 
          flop = f (...) True 
     Whereas we would be able to apply the type instance, we would not be able to 
     use the given (T Bool ~ (->)) in the body of 'flop' 

641 642 643 644 645 646 647

Note [Avoid double unifications] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The spontaneous solver has to return a given which mentions the unified unification
variable *on the left* of the equality. Here is what happens if not: 
  Original wanted:  (a ~ alpha),  (alpha ~ Int) 
We spontaneously solve the first wanted, without changing the order! 
648
      given : a ~ alpha      [having unified alpha := a] 
649 650 651
Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
At the end we spontaneously solve that guy, *reunifying*  [alpha := Int] 

652
We avoid this problem by orienting the resulting given so that the unification
653 654
variable is on the left.  [Note that alternatively we could attempt to
enforce this at canonicalization]
655

656 657 658
See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
double unifications is the main reason we disallow touchable
unification variables as RHS of type family equations: F xis ~ alpha.
659 660 661

\begin{code}
----------------
662

663
solveWithIdentity :: SubGoalDepth 
dimitris's avatar
dimitris committed
664
                  -> CtFlavor -> TcTyVar -> Xi -> TcS SPSolveResult
665 666
-- Solve with the identity coercion 
-- Precondition: kind(xi) is a sub-kind of kind(tv)
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
667 668 669
-- Precondition: CtFlavor is Wanted or Derived
-- See [New Wanted Superclass Work] to see why solveWithIdentity 
--     must work for Derived as well as Wanted
670
-- Returns: workItem where 
671
--        workItem = the new Given constraint
dimitris's avatar
dimitris committed
672 673 674 675 676 677 678
solveWithIdentity d wd tv xi 
  = do { let tv_ty = mkTyVarTy tv
       ; traceTcS "Sneaky unification:" $ 
                       vcat [text "Constraint:" <+> ppr wd,
                             text "Coercion:" <+> pprEq tv_ty xi,
                             text "Left Kind is:" <+> ppr (typeKind tv_ty),
                             text "Right Kind is:" <+> ppr (typeKind xi) ]
679

680 681 682 683 684 685 686
       ; let xi' = defaultKind xi      
               -- We only instantiate kind unification variables
               -- with simple kinds like *, not OpenKind or ArgKind
               -- cf TcUnify.uUnboundKVar

       ; setWantedTyBind tv xi'
       ; let refl_xi = mkTcReflCo xi'
687

dimitris's avatar
dimitris committed
688 689
       ; when (isWanted wd) $ 
              setEvBind (flav_evar wd) (EvCoercion refl_xi)
690

dimitris's avatar
dimitris committed
691 692 693 694 695 696 697
       ; ev_given <- newGivenEvVar (mkTcEqPred tv_ty xi') 
                                   (EvCoercion refl_xi) >>= (return . mn_thing)
       ; let given_fl = Given (mkGivenLoc (flav_wloc wd) UnkSkol) ev_given
             
       ; return $ 
         SPSolved (CTyEqCan { cc_flavor = given_fl
                            , cc_tyvar  = tv, cc_rhs = xi', cc_depth = d }) }
698 699
\end{code}

700 701 702 703 704 705 706

*********************************************************************************
*                                                                               * 
                       The interact-with-inert Stage
*                                                                               *
*********************************************************************************

707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731
Note [The Solver Invariant]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
We always add Givens first.  So you might think that the solver has
the invariant

   If the work-item is Given, 
   then the inert item must Given

But this isn't quite true.  Suppose we have, 
    c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
After processing the first two, we get
     c1: [G] beta ~ [alpha], c2 : [W] blah
Now, c3 does not interact with the the given c1, so when we spontaneously
solve c3, we must re-react it with the inert set.  So we can attempt a 
reaction between inert c2 [W] and work-item c3 [G].

It *is* true that [Solver Invariant]
   If the work-item is Given, 
   AND there is a reaction
   then the inert item must Given
or, equivalently,
   If the work-item is Given, 
   and the inert item is Wanted/Derived
   then there is no reaction

732 733 734
\begin{code}
-- Interaction result of  WorkItem <~> AtomicInert

735 736 737 738
data InteractResult 
    = IRWorkItemConsumed { ir_fire :: String } 
    | IRInertConsumed    { ir_fire :: String } 
    | IRKeepGoing        { ir_fire :: String }
739

740 741
irWorkItemConsumed :: String -> TcS InteractResult
irWorkItemConsumed str = return (IRWorkItemConsumed str) 
742

743 744
irInertConsumed :: String -> TcS InteractResult
irInertConsumed str = return (IRInertConsumed str) 
745

746 747 748 749
irKeepGoing :: String -> TcS InteractResult 
irKeepGoing str = return (IRKeepGoing str) 
-- You can't discard neither workitem or inert, but you must keep 
-- going. It's possible that new work is waiting in the TcS worklist. 
750 751


752 753 754 755
interactWithInertsStage :: WorkItem -> TcS StopOrContinue 
-- Precondition: if the workitem is a CTyEqCan then it will not be able to 
-- react with anything at this stage. 
interactWithInertsStage wi 
756
  = do { ctxt <- getTcSContext
757 758 759
       ; if simplEqsOnly ctxt then 
             return (ContinueWith wi)
         else 
dimitris's avatar
dimitris committed
760 761 762 763
           do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
              ; rels <- extractRelevantInerts wi 
              ; traceTcS "relevant inerts are:" $ ppr rels
              ; foldlBagM interact_next (ContinueWith wi) rels } }
764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789

  where interact_next Stop atomic_inert 
          = updInertSetTcS atomic_inert >> return Stop
        interact_next (ContinueWith wi) atomic_inert 
          = do { ir <- doInteractWithInert atomic_inert wi
               ; let mk_msg rule keep_doc 
                       = text rule <+> keep_doc
      	                 <+> vcat [ ptext (sLit "Inert =") <+> ppr atomic_inert
      	                          , ptext (sLit "Work =")  <+> ppr wi ]
               ; case ir of 
                   IRWorkItemConsumed { ir_fire = rule } 
                       -> do { bumpStepCountTcS
                             ; traceFireTcS (cc_depth wi) 
                                            (mk_msg rule (text "WorkItemConsumed"))
                             ; updInertSetTcS atomic_inert
                             ; return Stop } 
                   IRInertConsumed { ir_fire = rule }
                       -> do { bumpStepCountTcS
                             ; traceFireTcS (cc_depth atomic_inert) 
                                            (mk_msg rule (text "InertItemConsumed"))
                             ; return (ContinueWith wi) }
                   IRKeepGoing {} -- Should we do a bumpStepCountTcS? No for now.
                       -> do { updInertSetTcS atomic_inert
                             ; return (ContinueWith wi) }
               }
   
790 791
--------------------------------------------

792 793
doInteractWithInert :: Ct -> Ct -> TcS InteractResult
-- Identical class constraints.
794
doInteractWithInert
dimitris's avatar
dimitris committed
795 796
  inertItem@(CDictCan { cc_flavor = fl1, cc_class = cls1, cc_tyargs = tys1 }) 
   workItem@(CDictCan { cc_flavor = fl2, cc_class = cls2, cc_tyargs = tys2 })
797

798
  | cls1 == cls2  
batterseapower's avatar
batterseapower committed
799 800
  = do { let pty1 = mkClassPred cls1 tys1
             pty2 = mkClassPred cls2 tys2
801
             inert_pred_loc     = (pty1, pprFlavorArising fl1)
802
             work_item_pred_loc = (pty2, pprFlavorArising fl2)
803

804 805 806
       ; traceTcS "doInteractWithInert" (vcat [ text "inertItem = " <+> ppr inertItem
                                              , text "workItem  = " <+> ppr workItem ])

807 808 809 810 811 812
       ; any_fundeps 
           <- if isGivenOrSolved fl1 && isGivenOrSolved fl2 then return Nothing
              -- NB: We don't create fds for given (and even solved), have not seen a useful
              -- situation for these and even if we did we'd have to be very careful to only
              -- create Derived's and not Wanteds. 

813 814 815
              else do { let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
                      ; wloc  <- get_workitem_wloc fl2 
                      ; rewriteWithFunDeps fd_eqns tys2 wloc }
816 817 818 819 820
                      -- See Note [Efficient Orientation], [When improvement happens]

       ; case any_fundeps of
           -- No Functional Dependencies 
           Nothing             
dimitris's avatar
dimitris committed
821
               | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
822
               | otherwise         -> irKeepGoing "NOP"
823 824

           -- Actual Functional Dependencies
825 826
           Just (_rewritten_tys2,_cos2,fd_work)
              -- Standard thing: create derived fds and keep on going. Importantly we don't
827
               -- throw workitem back in the worklist because this can cause loops. See #5236.
828 829
               -> do { emitFDWorkAsDerived fd_work (cc_depth workItem)
                     ; irKeepGoing "Cls/Cls (new fundeps)" } -- Just keep going without droping the inert 
830
       }
dimitris's avatar
dimitris committed
831 832 833 834 835 836 837 838 839 840 841
  where get_workitem_wloc (Wanted wl _)  = return wl 
        get_workitem_wloc (Derived wl _) = return wl
        get_workitem_wloc _ = pprPanic "Unexpected given workitem!" $
                              vcat [ text "Work item =" <+> ppr workItem
                                   , text "Inert item=" <+> ppr inertItem]

-- Two pieces of irreducible evidence: if their types are *exactly identical* 
-- we can rewrite them. We can never improve using this: 
-- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not 
-- mean that (ty1 ~ ty2)
doInteractWithInert (CIrredEvCan { cc_flavor = ifl, cc_ty = ty1 })
842 843
           workItem@(CIrredEvCan { cc_ty = ty2 })
  | ty1 `eqType` ty2
dimitris's avatar
dimitris committed
844
  = solveOneFromTheOther "Irred/Irred" ifl workItem
845

846 847 848 849 850
-- Two implicit parameter constraints.  If the names are the same,
-- but their types are not, we generate a wanted type equality 
-- that equates the type (this is "improvement").  
-- However, we don't actually need the coercion evidence,
-- so we just generate a fresh coercion variable that isn't used anywhere.
dimitris's avatar
dimitris committed
851
doInteractWithInert (CIPCan { cc_flavor = ifl, cc_ip_nm = nm1, cc_ip_ty = ty1 }) 
852
           workItem@(CIPCan { cc_flavor = wfl, cc_ip_nm = nm2, cc_ip_ty = ty2 })
dimitris's avatar
dimitris committed
853
  | nm1 == nm2 && isGivenOrSolved wfl && isGivenOrSolved ifl
854 855 856
  = 	-- See Note [Overriding implicit parameters]
        -- Dump the inert item, override totally with the new one
	-- Do not require type equality
857 858
	-- For example, given let ?x::Int = 3 in let ?x::Bool = True in ...
	--              we must *override* the outer one with the inner one
859
    irInertConsumed "IP/IP (override inert)"
860

861
  | nm1 == nm2 && ty1 `eqType` ty2 
dimitris's avatar
dimitris committed
862
  = solveOneFromTheOther "IP/IP" ifl workItem 
863

864
  | nm1 == nm2
865
  =  	-- See Note [When improvement happens]
dimitris's avatar
dimitris committed
866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911
    do { mb_eqv <- newWantedEvVar (mkEqPred ty2 ty1)
         -- co :: ty2 ~ ty1, see Note [Efficient orientation]
       ; cv <- case mb_eqv of
                 Fresh eqv  -> 
                   do { updWorkListTcS $ extendWorkListEq $ 
                        CNonCanonical { cc_flavor = Wanted new_wloc eqv
                                      , cc_depth = cc_depth workItem }
                      ; return eqv }
                 Cached eqv -> return eqv
       ; case wfl of
            Wanted  {} ->
              let ip_co = mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo cv]
              in do { setEvBind (ctId "doInteractWithInert" workItem) $
                      mkEvCast (flav_evar ifl) (mkTcSymCo ip_co)
                    ; irWorkItemConsumed "IP/IP (solved by rewriting)" }
            _ -> pprPanic "Unexpected IP constraint" (ppr workItem) }
  where new_wloc
          | Wanted wl _  <- wfl = wl
          | Derived wl _ <- wfl = wl
          | Wanted wl _  <- ifl = wl
          | Derived wl _ <- ifl = wl
          | otherwise = panic "Solve IP: no WantedLoc!"
    
  {-- DELETEME
       ; when (isWanted  wfl) $
             do { setEvBind (flav_evar wfl) (mkEvCast (flav_evar ifl)

                 
       ; mb_new_fl <- rewriteCtFlavor wfl 
                        (mkTyConApp (ipTyCon nm1) [ty1]) -- IP x ty1
                        (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo cv])
                                                          -- IP x ty1 ~ IP x ty2
       ; case mb_new_fl of
            Nothing -> pprPanic "Unexpected cached IP constraint!" empty
            Just new_fl -> irWorkItemConsumed "IP/IP (solved by rewriting)" }
  where new_wloc
          | Wanted wl _  <- wfl = wl
          | Derived wl _ <- wfl = wl
          | Wanted wl _  <- ifl = wl
          | Derived wl _ <- ifl = wl
          | otherwise = panic "Solve IP: no WantedLoc!"

      eqv <- newWantedEvVar (mkEqPred ty2 ty1) 
                -- See Note [Efficient Orientation]
       ; 
      let flav = Wanted (combineCtLoc ifl wfl)
912 913 914 915 916 917 918
       ; eqv <- newEqVar flav ty2 ty1 -- See Note [Efficient Orientation]
       ; when (isNewEvVar eqv) $
              (let ct = CNonCanonical { cc_id     = evc_the_evvar eqv 
                                      , cc_flavor = flav
                                      , cc_depth  = cc_depth workItem }
              in updWorkListTcS (extendWorkListEq ct))

919 920 921 922
       ; case wfl of
           Given   {} -> pprPanic "Unexpected given IP" (ppr workItem)
           Derived {} -> pprPanic "Unexpected derived IP" (ppr workItem)
           Wanted  {} ->
923
               do { _ <- setEvBind (cc_id workItem) 
924
                            (mkEvCast id1 (mkTcSymCo (mkTcTyConAppCo (ipTyCon nm1) [mkTcCoVarCo (evc_the_evvar eqv)]))) wfl
925
                  ; irWorkItemConsumed "IP/IP (solved by rewriting)" } }
dimitris's avatar
dimitris committed
926 927
-}

928

dimitris's avatar
dimitris committed
929 930 931 932
doInteractWithInert ii@(CFunEqCan { cc_flavor = fl1, cc_fun = tc1
                                  , cc_tyargs = args1, cc_rhs = xi1, cc_depth = d1 }) 
                    wi@(CFunEqCan { cc_flavor = fl2, cc_fun = tc2
                                  , cc_tyargs = args2, cc_rhs = xi2, cc_depth = d2 })
933
  | lhss_match  
dimitris's avatar
dimitris committed
934 935
  , isSolved fl1 -- Inert is solved and we can simply ignore it
                 -- when workitem is given/solved
936 937
  , isGivenOrSolved fl2
  = irInertConsumed "FunEq/FunEq"
dimitris's avatar
dimitris committed
938 939 940
  | lhss_match
  , isSolved fl2 -- Workitem is solved and we can ignore it when
                 -- the inert is given/solved
941 942
  , isGivenOrSolved fl1                 
  = irWorkItemConsumed "FunEq/FunEq" 
943
  | fl1 `canSolve` fl2 && lhss_match
dimitris's avatar
dimitris committed
944 945 946 947 948
  = do { traceTcS "interact with inerts: FunEq/FunEq" $ 
         vcat [ text "workitem =" <+> ppr wi
              , text "inertitem=" <+> ppr ii ]
         
       ; xCtFlavor fl2 [mkTcEqPred xi2 xi1] (xev co1) $ what_next d2
949
       ; irWorkItemConsumed "FunEq/FunEq" }
950
  | fl2 `canSolve` fl1 && lhss_match
dimitris's avatar
dimitris committed
951
  = do { xCtFlavor fl1 [mkTcEqPred xi1 xi2] (xev co2) $ what_next d1
952
       ; irInertConsumed "FunEq/FunEq"}
953
  where
954
    lhss_match = tc1 == tc2 && eqTypes args1 args2 
dimitris's avatar
dimitris committed
955 956 957 958 959 960 961 962 963 964 965 966
    what_next d [new_fl] 
      = updWorkListTcS $ 
        extendWorkListEq (CNonCanonical {cc_flavor=new_fl,cc_depth = d})
    what_next _ _ = return ()
    co1 = mkTcCoVarCo $ flav_evar fl1
    co2 = mkTcCoVarCo $ flav_evar fl2
    mk_sym_co x = mkTcSymCo (mkTcCoVarCo x)
    xev co = XEvTerm xcomp xdecomp
           where xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co)]
                 xcomp [x] = EvCoercion (co `mkTcTransCo` mk_sym_co x)
                 xcomp _   = panic "No more goals!"
    
967 968
doInteractWithInert _ _ = irKeepGoing "NOP"

dimitris's avatar
dimitris committed
969
{- DELETE 
970
rewriteEqLHS :: WhichComesFromInert -> (EqVar,Xi) -> (EqVar,SubGoalDepth,CtFlavor,Xi) -> TcS ()
971
-- Used to ineract two equalities of the following form: 
972 973
-- First Equality:   co1: (XXX ~ xi1)  
-- Second Equality:  cv2: (XXX ~ xi2) 
974
-- Where the cv1 `canRewrite` cv2 equality 
975 976
-- We have an option of creating new work (xi1 ~ xi2) OR (xi2 ~ xi1), 
--    See Note [Efficient Orientation] for that 
977
rewriteEqLHS LeftComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
978
  = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
979 980
       ; evc <- newEqVar gw xi2 xi1
       ; let eqv2' = evc_the_evvar evc
981
       ; gw' <- case gw of 
982
           Wanted {} 
983
               -> setEqBind eqv2 
984
                    (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcSymCo (mkTcCoVarCo eqv2')) gw
985 986
           Given {}
               -> setEqBind eqv2'
987
                    (mkTcSymCo (mkTcCoVarCo eqv2) `mkTcTransCo` mkTcCoVarCo eqv1) gw
988
           Derived {} 
989
               -> return gw
990 991
       ; when (isNewEvVar evc) $ 
              updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id     = eqv2'
992
                                                              , cc_flavor = gw'
993 994 995
                                                              , cc_depth  = d } ) ) }

rewriteEqLHS RightComesFromInert (eqv1,xi1) (eqv2,d,gw,xi2) 
996
  = do { delCachedEvVar eqv2 gw -- Similarly to canonicalization!
997 998
       ; evc <- newEqVar gw xi1 xi2
       ; let eqv2' = evc_the_evvar evc
999
       ; gw' <- case gw of
1000
           Wanted {} 
1001
               -> setEqBind eqv2
1002
                    (mkTcCoVarCo eqv1 `mkTcTransCo` mkTcCoVarCo eqv2') gw
1003
           Given {}  
1004
               -> setEqBind eqv2'
1005
                    (mkTcSymCo (mkTcCoVarCo eqv1) `mkTcTransCo` mkTcCoVarCo eqv2) gw
1006
           Derived {} 
1007
               -> return gw
1008 1009 1010

       ; when (isNewEvVar evc) $
              updWorkListTcS (extendWorkListEq (CNonCanonical { cc_id = eqv2'
1011
                                                              , cc_flavor = gw'
1012 1013
                                                              , cc_depth  = d } ) ) }

dimitris's avatar
dimitris committed
1014 1015 1016 1017 1018
-}


solveOneFromTheOther :: String    -- Info 
                     -> CtFlavor  -- Inert 
1019 1020 1021 1022 1023
                     -> Ct        -- WorkItem 
                     -> TcS InteractResult
-- Preconditions: 
-- 1) inert and work item represent evidence for the /same/ predicate
-- 2) ip/class/irred evidence (no coercions) only
dimitris's avatar
dimitris committed
1024
solveOneFromTheOther info ifl workItem
1025
  | isDerived wfl
1026
  = irWorkItemConsumed ("Solved[DW] " ++ info)
1027

1028 1029 1030
  | isDerived ifl -- The inert item is Derived, we can just throw it away, 
    	      	  -- The workItem is inert wrt earlier inert-set items, 
		  -- so it's safe to continue on from this point
1031
  = irInertConsumed ("Solved[DI] " ++ info)
1032
  
dimitris's avatar
dimitris committed
1033
  | isSolved ifl, isGivenOrSolved wfl
dimitris's avatar
dimitris committed
1034
    -- Same if the inert is a GivenSolved -- just get rid of it
1035
  = irInertConsumed ("Solved[SI] " ++ info)
dimitris's avatar
dimitris committed
1036

1037 1038 1039
  | otherwise
  = ASSERT( ifl `canSolve` wfl )
      -- Because of Note [The Solver Invariant], plus Derived dealt with
dimitris's avatar
dimitris committed
1040
    do { when (isWanted wfl) $ setEvBind wid (EvId iid)
1041 1042
           -- Overwrite the binding, if one exists
	   -- If both are Given, we already have evidence; no need to duplicate
1043
       ; irWorkItemConsumed ("Solved " ++ info) }
1044 1045
  where 
     wfl = cc_flavor workItem
dimitris's avatar
dimitris committed
1046 1047
     wid = ctId "solveOneFromtheOther" workItem
     iid = flav_evar ifl
1048

1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065
\end{code}

Note [Superclasses and recursive dictionaries]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
    Overlaps with Note [SUPERCLASS-LOOP 1]
                  Note [SUPERCLASS-LOOP 2]
                  Note [Recursive instances and superclases]
    ToDo: check overlap and delete redundant stuff

Right before adding a given into the inert set, we must
produce some more work, that will bring the superclasses 
of the given into scope. The superclass constraints go into 
our worklist. 

When we simplify a wanted constraint, if we first see a matching
instance, we may produce new wanted work. To (1) avoid doing this work 
twice in the future and (2) to handle recursive dictionaries we may ``cache'' 
1066 1067 1068
this item as given into our inert set WITHOUT adding its superclass constraints, 
otherwise we'd be in danger of creating a loop [In fact this was the exact reason
for doing the isGoodRecEv check in an older version of the type checker]. 
1069 1070 1071 1072 1073 1074 1075 1076 1077 1078

But now we have added partially solved constraints to the worklist which may 
interact with other wanteds. Consider the example: 

Example 1: 

    class Eq b => Foo a b        --- 0-th selector
    instance Eq a => Foo [a] a   --- fooDFun

and wanted (Foo [t] t). We are first going to see that the instance matches 
1079
and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
1080 1081 1082 1083
       d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3 
Our work list is going to contain a new *wanted* goal
       d3 :_w Eq t 

1084
Ok, so how do we get recursive dictionaries, at all: 
1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391

Example 2:

    data D r = ZeroD | SuccD (r (D r));
    
    instance (Eq (r (D r))) => Eq (D r) where
        ZeroD     == ZeroD     = True
        (SuccD a) == (SuccD b) = a == b
        _         == _         = False;
    
    equalDC :: D [] -> D [] -> Bool;
    equalDC = (==);

We need to prove (Eq (D [])). Here's how we go:

	d1 :_w Eq (D [])

by instance decl, holds if
	d2 :_w Eq [D []]
	where 	d1 = dfEqD d2

*BUT* we have an inert set which gives us (no superclasses): 
        d1 :_g Eq (D []) 
By the instance declaration of Eq we can show the 'd2' goal if 
	d3 :_w Eq (D [])
	where	d2 = dfEqList d3
		d1 = dfEqD d2
Now, however this wanted can interact with our inert d1 to set: 
        d3 := d1 
and solve the goal. Why was this interaction OK? Because, if we chase the 
evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we 
are really setting
        d3 := dfEqD2 (dfEqList d3) 
which is FINE because the use of d3 is protected by the instance function 
applications. 

So, our strategy is to try to put solved wanted dictionaries into the
inert set along with their superclasses (when this is meaningful,
i.e. when new wanted goals are generated) but solve a wanted dictionary
from a given only in the case where the evidence variable of the
wanted is mentioned in the evidence of the given (recursively through
the evidence binds) in a protected way: more instance function applications 
than superclass selectors.

Here are some more examples from GHC's previous type checker


Example 3: 
This code arises in the context of "Scrap Your Boilerplate with Class"

    class Sat a
    class Data ctx a
    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2

    class Data Maybe a => Foo a    

    instance Foo t => Sat (Maybe t)                             -- dfunSat

    instance Data Maybe a => Foo a                              -- dfunFoo1
    instance Foo a        => Foo [a]                            -- dfunFoo2
    instance                 Foo [Char]                         -- dfunFoo3

Consider generating the superclasses of the instance declaration
	 instance Foo a => Foo [a]

So our problem is this
    d0 :_g Foo t
    d1 :_w Data Maybe [t] 

We may add the given in the inert set, along with its superclasses
[assuming we don't fail because there is a matching instance, see 
 tryTopReact, given case ]
  Inert:
    d0 :_g Foo t 
  WorkList 
    d01 :_g Data Maybe t  -- d2 := EvDictSuperClass d0 0 
    d1 :_w Data Maybe [t] 
Then d2 can readily enter the inert, and we also do solving of the wanted
  Inert: 
    d0 :_g Foo t 
    d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
  WorkList
    d2 :_w Sat (Maybe [t])          
    d3 :_w Data Maybe t
    d01 :_g Data Maybe t 
Now, we may simplify d2 more: 
  Inert:
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d1 :_g Data Maybe [t] 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
  WorkList: 
      d3 :_w Data Maybe t 
      d4 :_w Foo [t] 
      d01 :_g Data Maybe t 

Now, we can just solve d3.
  Inert
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
  WorkList
      d4 :_w Foo [t] 
      d01 :_g Data Maybe t 
And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
  Inert
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
      d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
  WorkList:
      d5 :_w Foo t 
      d6 :_g Data Maybe [t]           d6 := EvDictSuperClass d4 0
      d01 :_g Data Maybe t 
Now, d5 can be solved! (and its superclass enter scope) 
  Inert
      d0 :_g Foo t 
      d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3 
      d2 :_g Sat (Maybe [t])          d2 := dfunSat d4 
      d4 :_g Foo [t]                  d4 := dfunFoo2 d5 
      d5 :_g Foo t                    d5 := dfunFoo1 d7
  WorkList:
      d7 :_w Data Maybe t
      d6 :_g Data Maybe [t]
      d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
      d01 :_g Data Maybe t 

Now, two problems: 
   [1] Suppose we pick d8 and we react him with d01. Which of the two givens should 
       we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence 
       that must not be used (look at case interactInert where both inert and workitem
       are givens). So we have several options: 
       - Drop the workitem always (this will drop d8)
              This feels very unsafe -- what if the work item was the "good" one
              that should be used later to solve another wanted?
       - Don't drop anyone: the inert set may contain multiple givens! 
              [This is currently implemented] 

The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2: 
  [2] We have added both d6 and d01 in the inert set, and we are interacting ou