compiler/typecheck/TcInteract.lhs

   1 \begin{code}
   2 {-# OPTIONS -fno-warn-tabs #-}
   3 -- The above warning supression flag is a temporary kludge.
   4 -- While working on this module you are encouraged to remove it and
   5 -- detab the module (please do the detabbing in a separate patch). See
   6 --     http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
   7 -- for details
   8
   9 module TcInteract (
  10      solveInteractGiven,  -- Solves [EvVar],GivenLoc
  11      solveInteract,       -- Solves Cts
  12   ) where
  13
  14 #include "HsVersions.h"
  15
  16 import BasicTypes ()
  17 import TcCanonical
  18 import VarSet
  19 import Type
  20 import Unify
  21 import FamInst(TcBuiltInSynFamily(..))
  22 import InstEnv( lookupInstEnv, instanceDFunId )
  23
  24 import Var
  25 import TcType
  26 import PrelNames (knownNatClassName, knownSymbolClassName, ipClassNameKey )
  27 import TysWiredIn ( coercibleClass )
  28 import Id( idType )
  29 import Class
  30 import TyCon
  31 import DataCon
  32 import Name
  33 import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as,
  34                  is_decl, Provenance(Imported), gre_prov )
  35 import FunDeps
  36
  37 import TcEvidence
  38 import Outputable
  39
  40 import TcMType ( zonkTcPredType )
  41
  42 import TcRnTypes
  43 import TcErrors
  44 import TcSMonad
  45 import Maybes( orElse )
  46 import Bag
  47
  48 import Control.Monad ( foldM )
  49 import Data.Maybe ( catMaybes, mapMaybe )
  50
  51 import VarEnv
  52
  53 import Control.Monad( when, unless )
  54 import Pair (Pair(..))
  55 import Unique( hasKey )
  56 import UniqFM
  57 import FastString ( sLit )
  58 import DynFlags
  59 import Util
  60 \end{code}
  61 **********************************************************************
  62 *                                                                    *
  63 *                      Main Interaction Solver                       *
  64 *                                                                    *
  65 **********************************************************************
  66
  67 Note [Basic Simplifier Plan]
  68 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  69
  70 1. Pick an element from the WorkList if there exists one with depth
  71    less thanour context-stack depth.
  72
  73 2. Run it down the 'stage' pipeline. Stages are:
  74       - canonicalization
  75       - inert reactions
  76       - spontaneous reactions
  77       - top-level intreactions
  78    Each stage returns a StopOrContinue and may have sideffected
  79    the inerts or worklist.
  80
  81    The threading of the stages is as follows:
  82       - If (Stop) is returned by a stage then we start again from Step 1.
  83       - If (ContinueWith ct) is returned by a stage, we feed 'ct' on to
  84         the next stage in the pipeline.
  85 4. If the element has survived (i.e. ContinueWith x) the last stage
  86    then we add him in the inerts and jump back to Step 1.
  87
  88 If in Step 1 no such element exists, we have exceeded our context-stack
  89 depth and will simply fail.
  90 \begin{code}
  91 solveInteractGiven :: CtLoc -> [TcTyVar] -> [EvVar] -> TcS ()
  92 -- In principle the givens can kick out some wanteds from the inert
  93 -- resulting in solving some more wanted goals here which could emit
  94 -- implications. That's why I return a bag of implications. Not sure
  95 -- if this can happen in practice though.
  96 solveInteractGiven loc fsks givens
  97   = do { implics <- solveInteract (fsk_bag `unionBags` given_bag)
  98        ; ASSERT( isEmptyBag implics )
  99          return () }  -- We do not decompose *given* polymorphic equalities
 100                       --    (forall a. t1 ~ forall a. t2)
 101                       -- What would the evidence look like?!
 102                       -- See Note [Do not decompose given polytype equalities]
 103                       -- in TcCanonical
 104   where
 105     given_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvId ev_id
 106                                                          , ctev_pred = evVarPred ev_id }
 107                           | ev_id <- givens ]
 108
 109     fsk_bag = listToBag [ mkNonCanonical loc $ CtGiven { ctev_evtm = EvCoercion (mkTcReflCo tv_ty)
 110                                                        , ctev_pred = pred  }
 111                         | tv <- fsks
 112                         , let FlatSkol fam_ty = tcTyVarDetails tv
 113                               tv_ty = mkTyVarTy tv
 114                               pred  = mkTcEqPred fam_ty tv_ty
 115                         ]
 116
 117 -- The main solver loop implements Note [Basic Simplifier Plan]
 118 ---------------------------------------------------------------
 119 solveInteract :: Cts -> TcS (Bag Implication)
 120 -- Returns the final InertSet in TcS
 121 -- Has no effect on work-list or residual-iplications
 122 solveInteract cts
 123   = {-# SCC "solveInteract" #-}
 124     withWorkList cts $
 125     do { dyn_flags <- getDynFlags
 126        ; solve_loop (ctxtStkDepth dyn_flags) }
 127   where
 128     solve_loop max_depth
 129       = {-# SCC "solve_loop" #-}
 130         do { sel <- selectNextWorkItem max_depth
 131            ; case sel of
 132               NoWorkRemaining     -- Done, successfuly (modulo frozen)
 133                 -> return ()
 134               MaxDepthExceeded ct -- Failure, depth exceeded
 135                 -> wrapErrTcS $ solverDepthErrorTcS ct
 136               NextWorkItem ct     -- More work, loop around!
 137                 -> do { runSolverPipeline thePipeline ct; solve_loop max_depth } }
 138
 139 type WorkItem = Ct
 140 type SimplifierStage = WorkItem -> TcS StopOrContinue
 141
 142 continueWith :: WorkItem -> TcS StopOrContinue
 143 continueWith work_item = return (ContinueWith work_item)
 144
 145 data SelectWorkItem
 146        = NoWorkRemaining      -- No more work left (effectively we're done!)
 147        | MaxDepthExceeded Ct  -- More work left to do but this constraint has exceeded
 148                               -- the max subgoal depth and we must stop
 149        | NextWorkItem Ct      -- More work left, here's the next item to look at
 150
 151 selectNextWorkItem :: SubGoalDepth -- Max depth allowed
 152                    -> TcS SelectWorkItem
 153 selectNextWorkItem max_depth
 154   = updWorkListTcS_return pick_next
 155   where
 156     pick_next :: WorkList -> (SelectWorkItem, WorkList)
 157     pick_next wl
 158       = case selectWorkItem wl of
 159           (Nothing,_)
 160               -> (NoWorkRemaining,wl)           -- No more work
 161           (Just ct, new_wl)
 162               | ctLocDepth (cc_loc ct) > max_depth  -- Depth exceeded
 163               -> (MaxDepthExceeded ct,new_wl)
 164           (Just ct, new_wl)
 165               -> (NextWorkItem ct, new_wl)      -- New workitem and worklist
 166
 167 runSolverPipeline :: [(String,SimplifierStage)] -- The pipeline
 168                   -> WorkItem                   -- The work item
 169                   -> TcS ()
 170 -- Run this item down the pipeline, leaving behind new work and inerts
 171 runSolverPipeline pipeline workItem
 172   = do { initial_is <- getTcSInerts
 173        ; traceTcS "Start solver pipeline {" $
 174                   vcat [ ptext (sLit "work item = ") <+> ppr workItem
 175                        , ptext (sLit "inerts    = ") <+> ppr initial_is]
 176
 177        ; bumpStepCountTcS    -- One step for each constraint processed
 178        ; final_res  <- run_pipeline pipeline (ContinueWith workItem)
 179
 180        ; final_is <- getTcSInerts
 181        ; case final_res of
 182            Stop            -> do { traceTcS "End solver pipeline (discharged) }"
 183                                        (ptext (sLit "inerts    = ") <+> ppr final_is)
 184                                  ; return () }
 185            ContinueWith ct -> do { traceFireTcS ct (ptext (sLit "Kept as inert:") <+> ppr ct)
 186                                  ; traceTcS "End solver pipeline (not discharged) }" $
 187                                        vcat [ ptext (sLit "final_item = ") <+> ppr ct
 188                                             , pprTvBndrs (varSetElems $ tyVarsOfCt ct)
 189                                             , ptext (sLit "inerts     = ") <+> ppr final_is]
 190                                  ; insertInertItemTcS ct }
 191        }
 192   where run_pipeline :: [(String,SimplifierStage)] -> StopOrContinue -> TcS StopOrContinue
 193         run_pipeline [] res = return res
 194         run_pipeline _ Stop = return Stop
 195         run_pipeline ((stg_name,stg):stgs) (ContinueWith ct)
 196           = do { traceTcS ("runStage " ++ stg_name ++ " {")
 197                           (text "workitem   = " <+> ppr ct)
 198                ; res <- stg ct
 199                ; traceTcS ("end stage " ++ stg_name ++ " }") empty
 200                ; run_pipeline stgs res
 201                }
 202 \end{code}
 203
 204 Example 1:
 205   Inert:   {c ~ d, F a ~ t, b ~ Int, a ~ ty} (all given)
 206   Reagent: a ~ [b] (given)
 207
 208 React with (c~d)     ==> IR (ContinueWith (a~[b]))  True    []
 209 React with (F a ~ t) ==> IR (ContinueWith (a~[b]))  False   [F [b] ~ t]
 210 React with (b ~ Int) ==> IR (ContinueWith (a~[Int]) True    []
 211
 212 Example 2:
 213   Inert:  {c ~w d, F a ~g t, b ~w Int, a ~w ty}
 214   Reagent: a ~w [b]
 215
 216 React with (c ~w d)   ==> IR (ContinueWith (a~[b]))  True    []
 217 React with (F a ~g t) ==> IR (ContinueWith (a~[b]))  True    []    (can't rewrite given with wanted!)
 218 etc.
 219
 220 Example 3:
 221   Inert:  {a ~ Int, F Int ~ b} (given)
 222   Reagent: F a ~ b (wanted)
 223
 224 React with (a ~ Int)   ==> IR (ContinueWith (F Int ~ b)) True []
 225 React with (F Int ~ b) ==> IR Stop True []    -- after substituting we re-canonicalize and get nothing
 226
 227 \begin{code}
 228 thePipeline :: [(String,SimplifierStage)]
 229 thePipeline = [ ("canonicalization",        TcCanonical.canonicalize)
 230               , ("spontaneous solve",       spontaneousSolveStage)
 231               , ("interact with inerts",    interactWithInertsStage)
 232               , ("top-level reactions",     topReactionsStage) ]
 233 \end{code}
 234
 235
 236 *********************************************************************************
 237 *                                                                               *
 238                        The spontaneous-solve Stage
 239 *                                                                               *
 240 *********************************************************************************
 241
 242 \begin{code}
 243 spontaneousSolveStage :: SimplifierStage
 244 -- CTyEqCans are always consumed, returning Stop
 245 spontaneousSolveStage workItem
 246   = do { mb_solved <- trySpontaneousSolve workItem
 247        ; case mb_solved of
 248            SPCantSolve
 249               | CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = fl } <- workItem
 250               -- Unsolved equality
 251               -> do { untch <- getUntouchables
 252                     ; traceTcS "Can't solve tyvar equality"
 253                           (vcat [ text "LHS:" <+> ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 254                                 , text "RHS:" <+> ppr rhs <+> dcolon <+> ppr (typeKind rhs)
 255                                 , text "Untouchables =" <+> ppr untch ])
 256                     ; n_kicked <- kickOutRewritable (ctEvFlavour fl) tv
 257                     ; traceFireTcS workItem $
 258                       ptext (sLit "Kept as inert") <+> ppr_kicked n_kicked <> colon
 259                       <+> ppr workItem
 260                     ; insertInertItemTcS workItem
 261                     ; return Stop }
 262               | otherwise
 263               -> continueWith workItem
 264
 265            SPSolved new_tv
 266               -- Post: tv ~ xi is now in TyBinds, no need to put in inerts as well
 267               -- see Note [Spontaneously solved in TyBinds]
 268               -> do { n_kicked <- kickOutRewritable Given new_tv
 269                     ; traceFireTcS workItem $
 270                       ptext (sLit "Spontaneously solved") <+> ppr_kicked n_kicked <> colon
 271                       <+> ppr workItem
 272                     ; return Stop } }
 273
 274 ppr_kicked :: Int -> SDoc
 275 ppr_kicked 0 = empty
 276 ppr_kicked n = parens (int n <+> ptext (sLit "kicked out"))
 277 \end{code}
 278 Note [Spontaneously solved in TyBinds]
 279 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 280 When we encounter a constraint ([W] alpha ~ tau) which can be spontaneously solved,
 281 we record the equality on the TyBinds of the TcSMonad. In the past, we used to also
 282 add a /given/ version of the constraint ([G] alpha ~ tau) to the inert
 283 canonicals -- and potentially kick out other equalities that mention alpha.
 284
 285 Then, the flattener only had to look in the inert equalities during flattening of a
 286 type (TcCanonical.flattenTyVar).
 287
 288 However it is a bit silly to record these equalities /both/ in the inerts AND the
 289 TyBinds, so we have now eliminated spontaneously solved equalities from the inerts,
 290 and only record them in the TyBinds of the TcS monad. The flattener is now consulting
 291 these binds /and/ the inerts for potentially unsolved or other given equalities.
 292
 293 \begin{code}
 294 kickOutRewritable :: CtFlavour    -- Flavour of the equality that is
 295                                   -- being added to the inert set
 296                   -> TcTyVar      -- The new equality is tv ~ ty
 297                   -> TcS Int
 298 kickOutRewritable new_flav new_tv
 299   = do { wl <- modifyInertTcS kick_out
 300        ; traceTcS "kickOutRewritable" $
 301             vcat [ text "tv = " <+> ppr new_tv
 302                  , ptext (sLit "Kicked out =") <+> ppr wl]
 303        ; updWorkListTcS (appendWorkList wl)
 304        ; return (workListSize wl)  }
 305   where
 306     kick_out :: InertSet -> (WorkList, InertSet)
 307     kick_out (is@(IS { inert_cans = IC { inert_eqs = tv_eqs
 308                      , inert_dicts  = dictmap
 309                      , inert_funeqs = funeqmap
 310                      , inert_irreds = irreds
 311                      , inert_insols = insols } }))
 312        = (kicked_out, is { inert_cans = inert_cans_in })
 313                 -- NB: Notice that don't rewrite
 314                 -- inert_solved_dicts, and inert_solved_funeqs
 315                 -- optimistically. But when we lookup we have to take the
 316                 -- subsitution into account
 317        where
 318          inert_cans_in = IC { inert_eqs = tv_eqs_in
 319                             , inert_dicts = dicts_in
 320                             , inert_funeqs = feqs_in
 321                             , inert_irreds = irs_in
 322                             , inert_insols = insols_in }
 323
 324          kicked_out = WorkList { wl_eqs    = varEnvElts tv_eqs_out
 325                                , wl_funeqs = foldrBag insertDeque emptyDeque feqs_out
 326                                , wl_rest   = bagToList (dicts_out `andCts` irs_out
 327                                                         `andCts` insols_out) }
 328
 329          (tv_eqs_out,  tv_eqs_in) = partitionVarEnv  kick_out_eq tv_eqs
 330          (feqs_out,   feqs_in)    = partCtFamHeadMap kick_out_ct funeqmap
 331          (dicts_out,  dicts_in)   = partitionCCanMap kick_out_ct dictmap
 332          (irs_out,    irs_in)     = partitionBag     kick_out_ct irreds
 333          (insols_out, insols_in)  = partitionBag     kick_out_ct insols
 334            -- Kick out even insolubles; see Note [Kick out insolubles]
 335
 336     kick_out_ct inert_ct = new_flav `canRewrite` (ctFlavour inert_ct) &&
 337                           (new_tv `elemVarSet` tyVarsOfCt inert_ct)
 338                     -- NB: tyVarsOfCt will return the type
 339                     --     variables /and the kind variables/ that are
 340                     --     directly visible in the type. Hence we will
 341                     --     have exposed all the rewriting we care about
 342                     --     to make the most precise kinds visible for
 343                     --     matching classes etc. No need to kick out
 344                     --     constraints that mention type variables whose
 345                     --     kinds could contain this variable!
 346
 347     kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = ev })
 348       =  (new_flav `canRewrite` inert_flav)  -- See Note [Delicate equality kick-out]
 349       && (new_tv `elemVarSet` kind_vars ||              -- (1)
 350           (not (inert_flav `canRewrite` new_flav) &&    -- (2)
 351            new_tv `elemVarSet` (extendVarSet (tyVarsOfType rhs) tv)))
 352       where
 353         inert_flav = ctEvFlavour ev
 354         kind_vars = tyVarsOfType (tyVarKind tv) `unionVarSet`
 355                     tyVarsOfType (typeKind rhs)
 356
 357     kick_out_eq other_ct = pprPanic "kick_out_eq" (ppr other_ct)
 358 \end{code}
 359
 360 Note [Kick out insolubles]
 361 ~~~~~~~~~~~~~~~~~~~~~~~~~~
 362 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
 363 because an occurs check.  And then we unify alpha := [Int].
 364 Then we really want to rewrite the insouluble to [Int] ~ [[Int]].
 365 Now it can be decomposed.  Otherwise we end up with a "Can't match
 366 [Int] ~ [[Int]]" which is true, but a bit confusing because the
 367 outer type constructors match.
 368
 369 Note [Delicate equality kick-out]
 370 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 371 When adding an equality (a ~ xi), we kick out an inert type-variable
 372 equality (b ~ phi) in two cases
 373
 374 (1) If the new tyvar can rewrite the kind LHS or RHS of the inert
 375     equality.  Example:
 376     Work item: [W] k ~ *
 377     Inert:     [W] (a:k) ~ ty
 378                [W] (b:*) ~ c :: k
 379     We must kick out those blocked inerts so that we rewrite them
 380     and can subsequently unify.
 381
 382 (2) If the new tyvar can
 383           Work item:  [G] a ~ b
 384           Inert:      [W] b ~ [a]
 385     Now at this point the work item cannot be further rewritten by the
 386     inert (due to the weaker inert flavor). But we can't add the work item
 387     as-is because the inert set would then have a cyclic substitution,
 388     when rewriting a wanted type mentioning 'a'. So we must kick the inert out.
 389
 390     We have to do this only if the inert *cannot* rewrite the work item;
 391     it it can, then the work item will have been fully rewritten by the
 392     inert during canonicalisation.  So for example:
 393          Work item: [W] a ~ Int
 394          Inert:     [W] b ~ [a]
 395     No need to kick out the inert, beause the inert substitution is not
 396     necessarily idemopotent.  See Note [Non-idempotent inert substitution].
 397
 398 See also point (8) of Note [Detailed InertCans Invariants]
 399
 400 \begin{code}
 401 data SPSolveResult = SPCantSolve
 402                    | SPSolved TcTyVar
 403                      -- We solved this /unification/ variable to some type using reflexivity
 404
 405 -- SPCantSolve means that we can't do the unification because e.g. the variable is untouchable
 406 -- SPSolved workItem' gives us a new *given* to go on
 407
 408 -- @trySpontaneousSolve wi@ solves equalities where one side is a
 409 -- touchable unification variable.
 410 --          See Note [Touchables and givens]
 411 trySpontaneousSolve :: WorkItem -> TcS SPSolveResult
 412 trySpontaneousSolve workItem@(CTyEqCan { cc_ev = gw
 413                                        , cc_tyvar = tv1, cc_rhs = xi, cc_loc = d })
 414   | isGiven gw
 415   = do { traceTcS "No spontaneous solve for given" (ppr workItem)
 416        ; return SPCantSolve }
 417   | Just tv2 <- tcGetTyVar_maybe xi
 418   = do { tch1 <- isTouchableMetaTyVarTcS tv1
 419        ; tch2 <- isTouchableMetaTyVarTcS tv2
 420        ; case (tch1, tch2) of
 421            (True,  True)  -> trySpontaneousEqTwoWay d gw tv1 tv2
 422            (True,  False) -> trySpontaneousEqOneWay d gw tv1 xi
 423            (False, True)  -> trySpontaneousEqOneWay d gw tv2 (mkTyVarTy tv1)
 424            _              -> return SPCantSolve }
 425   | otherwise
 426   = do { tch1 <- isTouchableMetaTyVarTcS tv1
 427        ; if tch1 then trySpontaneousEqOneWay d gw tv1 xi
 428                  else return SPCantSolve }
 429
 430   -- No need for
 431   --      trySpontaneousSolve (CFunEqCan ...) = ...
 432   -- See Note [No touchables as FunEq RHS] in TcSMonad
 433 trySpontaneousSolve item = do { traceTcS "Spont: no tyvar on lhs" (ppr item)
 434                               ; return SPCantSolve }
 435
 436 ----------------
 437 trySpontaneousEqOneWay :: CtLoc -> CtEvidence
 438                        -> TcTyVar -> Xi -> TcS SPSolveResult
 439 -- tv is a MetaTyVar, not untouchable
 440 trySpontaneousEqOneWay d gw tv xi
 441   | not (isSigTyVar tv) || isTyVarTy xi
 442   , typeKind xi `tcIsSubKind` tyVarKind tv
 443   = solveWithIdentity d gw tv xi
 444   | otherwise -- Still can't solve, sig tyvar and non-variable rhs
 445   = return SPCantSolve
 446
 447 ----------------
 448 trySpontaneousEqTwoWay :: CtLoc -> CtEvidence
 449                        -> TcTyVar -> TcTyVar -> TcS SPSolveResult
 450 -- Both tyvars are *touchable* MetaTyvars so there is only a chance for kind error here
 451
 452 trySpontaneousEqTwoWay d gw tv1 tv2
 453   | k1 `tcIsSubKind` k2 && nicer_to_update_tv2
 454   = solveWithIdentity d gw tv2 (mkTyVarTy tv1)
 455   | k2 `tcIsSubKind` k1
 456   = solveWithIdentity d gw tv1 (mkTyVarTy tv2)
 457   | otherwise
 458   = return SPCantSolve
 459   where
 460     k1 = tyVarKind tv1
 461     k2 = tyVarKind tv2
 462     nicer_to_update_tv2 = isSigTyVar tv1 || isSystemName (Var.varName tv2)
 463 \end{code}
 464
 465 Note [Avoid double unifications]
 466 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 467 The spontaneous solver has to return a given which mentions the unified unification
 468 variable *on the left* of the equality. Here is what happens if not:
 469   Original wanted:  (a ~ alpha),  (alpha ~ Int)
 470 We spontaneously solve the first wanted, without changing the order!
 471       given : a ~ alpha      [having unified alpha := a]
 472 Now the second wanted comes along, but he cannot rewrite the given, so we simply continue.
 473 At the end we spontaneously solve that guy, *reunifying*  [alpha := Int]
 474
 475 We avoid this problem by orienting the resulting given so that the unification
 476 variable is on the left.  [Note that alternatively we could attempt to
 477 enforce this at canonicalization]
 478
 479 See also Note [No touchables as FunEq RHS] in TcSMonad; avoiding
 480 double unifications is the main reason we disallow touchable
 481 unification variables as RHS of type family equations: F xis ~ alpha.
 482
 483 \begin{code}
 484 solveWithIdentity :: CtLoc -> CtEvidence -> TcTyVar -> Xi -> TcS SPSolveResult
 485 -- Solve with the identity coercion
 486 -- Precondition: kind(xi) is a sub-kind of kind(tv)
 487 -- Precondition: CtEvidence is Wanted or Derived
 488 -- See [New Wanted Superclass Work] to see why solveWithIdentity
 489 --     must work for Derived as well as Wanted
 490 -- Returns: workItem where
 491 --        workItem = the new Given constraint
 492 --
 493 -- NB: No need for an occurs check here, because solveWithIdentity always
 494 --     arises from a CTyEqCan, a *canonical* constraint.  Its invariants
 495 --     say that in (a ~ xi), the type variable a does not appear in xi.
 496 --     See TcRnTypes.Ct invariants.
 497 solveWithIdentity _d wd tv xi
 498   = do { let tv_ty = mkTyVarTy tv
 499        ; traceTcS "Sneaky unification:" $
 500                        vcat [text "Unifies:" <+> ppr tv <+> ptext (sLit ":=") <+> ppr xi,
 501                              text "Coercion:" <+> pprEq tv_ty xi,
 502                              text "Left Kind is:" <+> ppr (typeKind tv_ty),
 503                              text "Right Kind is:" <+> ppr (typeKind xi) ]
 504
 505        ; let xi' = defaultKind xi
 506                -- We only instantiate kind unification variables
 507                -- with simple kinds like *, not OpenKind or ArgKind
 508                -- cf TcUnify.uUnboundKVar
 509
 510        ; setWantedTyBind tv xi'
 511        ; let refl_evtm = EvCoercion (mkTcReflCo xi')
 512
 513        ; when (isWanted wd) $
 514               setEvBind (ctev_evar wd) refl_evtm
 515
 516        ; return (SPSolved tv) }
 517 \end{code}
 518
 519
 520 *********************************************************************************
 521 *                                                                               *
 522                        The interact-with-inert Stage
 523 *                                                                               *
 524 *********************************************************************************
 525
 526 Note [
 527
 528 Note [The Solver Invariant]
 529 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 530 We always add Givens first.  So you might think that the solver has
 531 the invariant
 532
 533    If the work-item is Given,
 534    then the inert item must Given
 535
 536 But this isn't quite true.  Suppose we have,
 537     c1: [W] beta ~ [alpha], c2 : [W] blah, c3 :[W] alpha ~ Int
 538 After processing the first two, we get
 539      c1: [G] beta ~ [alpha], c2 : [W] blah
 540 Now, c3 does not interact with the the given c1, so when we spontaneously
 541 solve c3, we must re-react it with the inert set.  So we can attempt a
 542 reaction between inert c2 [W] and work-item c3 [G].
 543
 544 It *is* true that [Solver Invariant]
 545    If the work-item is Given,
 546    AND there is a reaction
 547    then the inert item must Given
 548 or, equivalently,
 549    If the work-item is Given,
 550    and the inert item is Wanted/Derived
 551    then there is no reaction
 552
 553 \begin{code}
 554 -- Interaction result of  WorkItem <~> Ct
 555
 556 data InteractResult
 557     = IRWorkItemConsumed { ir_fire :: String }    -- Work item discharged by interaction; stop
 558     | IRReplace          { ir_fire :: String }    -- Inert item replaced by work item; stop
 559     | IRInertConsumed    { ir_fire :: String }    -- Inert item consumed, keep going with work item
 560     | IRKeepGoing        { ir_fire :: String }    -- Inert item remains, keep going with work item
 561
 562 interactWithInertsStage :: WorkItem -> TcS StopOrContinue
 563 -- Precondition: if the workitem is a CTyEqCan then it will not be able to
 564 -- react with anything at this stage.
 565 interactWithInertsStage wi
 566   = do { traceTcS "interactWithInerts" $ text "workitem = " <+> ppr wi
 567        ; rels <- extractRelevantInerts wi
 568        ; traceTcS "relevant inerts are:" $ ppr rels
 569        ; builtInInteractions
 570        ; foldlBagM interact_next (ContinueWith wi) rels }
 571
 572   where interact_next Stop atomic_inert
 573           = do { insertInertItemTcS atomic_inert; return Stop }
 574         interact_next (ContinueWith wi) atomic_inert
 575           = do { ir <- doInteractWithInert atomic_inert wi
 576                ; let mk_msg rule keep_doc
 577                        = vcat [ text rule <+> keep_doc
 578                               , ptext (sLit "InertItem =") <+> ppr atomic_inert
 579                               , ptext (sLit "WorkItem  =") <+> ppr wi ]
 580                ; case ir of
 581                    IRWorkItemConsumed { ir_fire = rule }
 582                        -> do { traceFireTcS wi (mk_msg rule (text "WorkItemConsumed"))
 583                              ; insertInertItemTcS atomic_inert
 584                              ; return Stop }
 585                    IRReplace { ir_fire = rule }
 586                        -> do { traceFireTcS atomic_inert
 587                                             (mk_msg rule (text "InertReplace"))
 588                              ; insertInertItemTcS wi
 589                              ; return Stop }
 590                    IRInertConsumed { ir_fire = rule }
 591                        -> do { traceFireTcS atomic_inert
 592                                             (mk_msg rule (text "InertItemConsumed"))
 593                              ; return (ContinueWith wi) }
 594                    IRKeepGoing {}
 595                        -> do { insertInertItemTcS atomic_inert
 596                              ; return (ContinueWith wi) }
 597                }
 598
 599         -- See if we can compute some new derived work for built-ins.
 600         builtInInteractions
 601           | CFunEqCan { cc_fun = tc, cc_tyargs = args, cc_rhs = xi } <- wi
 602           , Just ops <- isBuiltInSynFamTyCon_maybe tc =
 603             do is <- getInertsFunEqTyCon tc
 604                traceTcS "builtInCandidates: " $ ppr is
 605                let interact = sfInteractInert ops args xi
 606                impMbs <- sequence
 607                  [ do mb <- newDerived (mkTcEqPred lhs rhs)
 608                       case mb of
 609                         Just x -> return $ Just $ mkNonCanonical d x
 610                         Nothing -> return Nothing
 611                  | CFunEqCan { cc_tyargs = iargs
 612                              , cc_rhs = ixi
 613                              , cc_loc = d } <- is
 614                  , Pair lhs rhs <- interact iargs ixi
 615                  ]
 616                let imps = catMaybes impMbs
 617                unless (null imps) $ updWorkListTcS (extendWorkListEqs imps)
 618           | otherwise = return ()
 619
 620
 621
 622
 623 \end{code}
 624
 625 \begin{code}
 626 --------------------------------------------
 627
 628 doInteractWithInert :: Ct -> Ct -> TcS InteractResult
 629 -- Identical class constraints.
 630 doInteractWithInert inertItem@(CDictCan { cc_ev = fl1, cc_class = cls1, cc_tyargs = tys1, cc_loc = loc1 })
 631                      workItem@(CDictCan { cc_ev = fl2, cc_class = cls2, cc_tyargs = tys2, cc_loc = loc2 })
 632   | cls1 == cls2
 633   = do { let pty1 = mkClassPred cls1 tys1
 634              pty2 = mkClassPred cls2 tys2
 635              inert_pred_loc     = (pty1, pprArisingAt loc1)
 636              work_item_pred_loc = (pty2, pprArisingAt loc2)
 637
 638        ; let fd_eqns = improveFromAnother inert_pred_loc work_item_pred_loc
 639        ; fd_work <- rewriteWithFunDeps fd_eqns loc2
 640                 -- We don't really rewrite tys2, see below _rewritten_tys2, so that's ok
 641                 -- NB: We do create FDs for given to report insoluble equations that arise
 642                 -- from pairs of Givens, and also because of floating when we approximate
 643                 -- implications. The relevant test is: typecheck/should_fail/FDsFromGivens.hs
 644                 -- Also see Note [When improvement happens]
 645
 646        ; traceTcS "doInteractWithInert:dict"
 647                   (vcat [ text "inertItem =" <+> ppr inertItem
 648                         , text "workItem  =" <+> ppr workItem
 649                         , text "fundeps =" <+> ppr fd_work ])
 650
 651        ; case fd_work of
 652            -- No Functional Dependencies
 653            []  | eqTypes tys1 tys2 -> solveOneFromTheOther "Cls/Cls" fl1 workItem
 654                | otherwise         -> return (IRKeepGoing "NOP")
 655
 656            -- Actual Functional Dependencies
 657            _   | cls1 `hasKey` ipClassNameKey
 658                , isGiven fl1, isGiven fl2  -- See Note [Shadowing of Implicit Parameters]
 659                -> return (IRReplace ("Replace IP"))
 660
 661                -- Standard thing: create derived fds and keep on going. Importantly we don't
 662                -- throw workitem back in the worklist because this can cause loops. See #5236.
 663                | otherwise
 664                -> do { updWorkListTcS (extendWorkListEqs fd_work)
 665                      ; return (IRKeepGoing "Cls/Cls (new fundeps)") } -- Just keep going without droping the inert
 666        }
 667
 668 -- Two pieces of irreducible evidence: if their types are *exactly identical*
 669 -- we can rewrite them. We can never improve using this:
 670 -- if we want ty1 :: Constraint and have ty2 :: Constraint it clearly does not
 671 -- mean that (ty1 ~ ty2)
 672 doInteractWithInert (CIrredEvCan { cc_ev = ifl })
 673            workItem@(CIrredEvCan { cc_ev = wfl })
 674   | ctEvPred ifl `eqType` ctEvPred wfl
 675   = solveOneFromTheOther "Irred/Irred" ifl workItem
 676
 677 doInteractWithInert ii@(CFunEqCan { cc_ev = ev1, cc_fun = tc1
 678                                   , cc_tyargs = args1, cc_rhs = xi1, cc_loc = d1 })
 679                     wi@(CFunEqCan { cc_ev = ev2, cc_fun = tc2
 680                                   , cc_tyargs = args2, cc_rhs = xi2, cc_loc = d2 })
 681   | i_solves_w && (not (w_solves_i && isMetaTyVarTy xi1))
 682                -- See Note [Carefully solve the right CFunEqCan]
 683   = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
 684     do { traceTcS "interact with inerts: FunEq/FunEq" $
 685          vcat [ text "workItem =" <+> ppr wi
 686               , text "inertItem=" <+> ppr ii ]
 687
 688        ; let xev = XEvTerm xcomp xdecomp
 689              -- xcomp : [(xi2 ~ xi1)] -> (F args ~ xi2)
 690              xcomp [x] = EvCoercion (co1 `mkTcTransCo` mk_sym_co x)
 691              xcomp _   = panic "No more goals!"
 692              -- xdecomp : (F args ~ xi2) -> [(xi2 ~ xi1)]
 693              xdecomp x = [EvCoercion (mk_sym_co x `mkTcTransCo` co1)]
 694
 695        ; ctevs <- xCtFlavor ev2 [mkTcEqPred xi2 xi1] xev
 696              -- No caching!  See Note [Cache-caused loops]
 697              -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
 698        ; emitWorkNC d2 ctevs
 699        ; return (IRWorkItemConsumed "FunEq/FunEq") }
 700
 701   | fl2 `canSolve` fl1
 702   = ASSERT( lhss_match )   -- extractRelevantInerts ensures this
 703     do { traceTcS "interact with inerts: FunEq/FunEq" $
 704          vcat [ text "workItem =" <+> ppr wi
 705               , text "inertItem=" <+> ppr ii ]
 706
 707        ; let xev = XEvTerm xcomp xdecomp
 708               -- xcomp : [(xi2 ~ xi1)] -> [(F args ~ xi1)]
 709              xcomp [x] = EvCoercion (co2 `mkTcTransCo` evTermCoercion x)
 710              xcomp _ = panic "No more goals!"
 711              -- xdecomp : (F args ~ xi1) -> [(xi2 ~ xi1)]
 712              xdecomp x = [EvCoercion (mkTcSymCo co2 `mkTcTransCo` evTermCoercion x)]
 713
 714        ; ctevs <- xCtFlavor ev1 [mkTcEqPred xi2 xi1] xev
 715              -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
 716
 717        ; emitWorkNC d1 ctevs
 718        ; return (IRInertConsumed "FunEq/FunEq") }
 719   where
 720     lhss_match = tc1 == tc2 && eqTypes args1 args2
 721     co1 = evTermCoercion $ ctEvTerm ev1
 722     co2 = evTermCoercion $ ctEvTerm ev2
 723     mk_sym_co x = mkTcSymCo (evTermCoercion x)
 724     fl1 = ctEvFlavour ev1
 725     fl2 = ctEvFlavour ev2
 726
 727     i_solves_w = fl1 `canSolve` fl2
 728     w_solves_i = fl2 `canSolve` fl1
 729
 730
 731 doInteractWithInert _ _ = return (IRKeepGoing "NOP")
 732 \end{code}
 733
 734 Note [Efficient Orientation]
 735 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 736 Suppose we are interacting two FunEqCans with the same LHS:
 737           (inert)  ci :: (F ty ~ xi_i)
 738           (work)   cw :: (F ty ~ xi_w)
 739 We prefer to keep the inert (else we pass the work item on down
 740 the pipeline, which is a bit silly).  If we keep the inert, we
 741 will (a) discharge 'cw'
 742      (b) produce a new equality work-item (xi_w ~ xi_i)
 743 Notice the orientation (xi_w ~ xi_i) NOT (xi_i ~ xi_w):
 744     new_work :: xi_w ~ xi_i
 745     cw := ci ; sym new_work
 746 Why?  Consider the simplest case when xi1 is a type variable.  If
 747 we generate xi1~xi2, porcessing that constraint will kick out 'ci'.
 748 If we generate xi2~xi1, there is less chance of that happening.
 749 Of course it can and should still happen if xi1=a, xi1=Int, say.
 750 But we want to avoid it happening needlessly.
 751
 752 Similarly, if we *can't* keep the inert item (because inert is Wanted,
 753 and work is Given, say), we prefer to orient the new equality (xi_i ~
 754 xi_w).
 755
 756 Note [Carefully solve the right CFunEqCan]
 757 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 758 Consider the constraints
 759   c1 :: F Int ~ a      -- Arising from an application line 5
 760   c2 :: F Int ~ Bool   -- Arising from an application line 10
 761 Suppose that 'a' is a unification variable, arising only from
 762 flattening.  So there is no error on line 5; it's just a flattening
 763 variable.  But there is (or might be) an error on line 10.
 764
 765 Two ways to combine them, leaving either (Plan A)
 766   c1 :: F Int ~ a      -- Arising from an application line 5
 767   c3 :: a ~ Bool       -- Arising from an application line 10
 768 or (Plan B)
 769   c2 :: F Int ~ Bool   -- Arising from an application line 10
 770   c4 :: a ~ Bool       -- Arising from an application line 5
 771
 772 Plan A will unify c3, leaving c1 :: F Int ~ Bool as an error
 773 on the *totally innocent* line 5.  An example is test SimpleFail16
 774 where the expected/actual message comes out backwards if we use
 775 the wrong plan.
 776
 777 The second is the right thing to do.  Hence the isMetaTyVarTy
 778 test when solving pairwise CFunEqCan.
 779
 780 Note [Shadowing of Implicit Parameters]
 781 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 782
 783 Consider the following example:
 784
 785 f :: (?x :: Char) => Char
 786 f = let ?x = 'a' in ?x
 787
 788 The "let ?x = ..." generates an implication constraint of the form:
 789
 790 ?x :: Char => ?x :: Char
 791
 792 Furthermore, the signature for `f` also generates an implication
 793 constraint, so we end up with the following nested implication:
 794
 795 ?x :: Char => (?x :: Char => ?x :: Char)
 796
 797 Note that the wanted (?x :: Char) constraint may be solved in
 798 two incompatible ways:  either by using the parameter from the
 799 signature, or by using the local definition.  Our intention is
 800 that the local definition should "shadow" the parameter of the
 801 signature, and we implement this as follows: when we add a new
 802 given implicit parameter to the inert set, it replaces any existing
 803 givens for the same implicit parameter.
 804
 805 This works for the normal cases but it has an odd side effect
 806 in some pathological programs like this:
 807
 808 -- This is accepted, the second parameter shadows
 809 f1 :: (?x :: Int, ?x :: Char) => Char
 810 f1 = ?x
 811
 812 -- This is rejected, the second parameter shadows
 813 f2 :: (?x :: Int, ?x :: Char) => Int
 814 f2 = ?x
 815
 816 Both of these are actually wrong:  when we try to use either one,
 817 we'll get two incompatible wnated constraints (?x :: Int, ?x :: Char),
 818 which would lead to an error.
 819
 820 I can think of two ways to fix this:
 821
 822   1. Simply disallow multiple constratits for the same implicit
 823     parameter---this is never useful, and it can be detected completely
 824     syntactically.
 825
 826   2. Move the shadowing machinery to the location where we nest
 827      implications, and add some code here that will produce an
 828      error if we get multiple givens for the same implicit parameter.
 829
 830
 831 Note [Cache-caused loops]
 832 ~~~~~~~~~~~~~~~~~~~~~~~~~
 833 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
 834 solved cache (which is the default behaviour or xCtFlavor), because the interaction
 835 may not be contributing towards a solution. Here is an example:
 836
 837 Initial inert set:
 838   [W] g1 : F a ~ beta1
 839 Work item:
 840   [W] g2 : F a ~ beta2
 841 The work item will react with the inert yielding the _same_ inert set plus:
 842     i)   Will set g2 := g1 `cast` g3
 843     ii)  Will add to our solved cache that [S] g2 : F a ~ beta2
 844     iii) Will emit [W] g3 : beta1 ~ beta2
 845 Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2
 846 and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it
 847 will set
 848       g1 := g ; sym g3
 849 and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but
 850 remember that we have this in our solved cache, and it is ... g2! In short we
 851 created the evidence loop:
 852
 853         g2 := g1 ; g3
 854         g3 := refl
 855         g1 := g2 ; sym g3
 856
 857 To avoid this situation we do not cache as solved any workitems (or inert)
 858 which did not really made a 'step' towards proving some goal. Solved's are
 859 just an optimization so we don't lose anything in terms of completeness of
 860 solving.
 861
 862 \begin{code}
 863 solveOneFromTheOther :: String    -- Info
 864                      -> CtEvidence  -- Inert
 865                      -> Ct        -- WorkItem
 866                      -> TcS InteractResult
 867 -- Preconditions:
 868 -- 1) inert and work item represent evidence for the /same/ predicate
 869 -- 2) ip/class/irred evidence (no coercions) only
 870 solveOneFromTheOther info ifl workItem
 871   | isDerived wfl
 872   = return (IRWorkItemConsumed ("Solved[DW] " ++ info))
 873
 874   | isDerived ifl -- The inert item is Derived, we can just throw it away,
 875                   -- The workItem is inert wrt earlier inert-set items,
 876                   -- so it's safe to continue on from this point
 877   = return (IRInertConsumed ("Solved[DI] " ++ info))
 878
 879   | CtWanted { ctev_evar = ev_id } <- wfl
 880   = do { setEvBind ev_id (ctEvTerm ifl); return (IRWorkItemConsumed ("Solved(w) " ++ info)) }
 881
 882   | CtWanted { ctev_evar = ev_id } <- ifl
 883   = do { setEvBind ev_id (ctEvTerm wfl); return (IRInertConsumed ("Solved(g) " ++ info)) }
 884
 885   | otherwise      -- If both are Given, we already have evidence; no need to duplicate
 886                    -- But the work item *overrides* the inert item (hence IRReplace)
 887                    -- See Note [Shadowing of Implicit Parameters]
 888   = return (IRReplace ("Replace(gg) " ++ info))
 889   where
 890      wfl = cc_ev workItem
 891 \end{code}
 892
 893 Note [Shadowing of Implicit Parameters]
 894 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 895 Consider the following example:
 896
 897 f :: (?x :: Char) => Char
 898 f = let ?x = 'a' in ?x
 899
 900 The "let ?x = ..." generates an implication constraint of the form:
 901
 902 ?x :: Char => ?x :: Char
 903
 904
 905 Furthermore, the signature for `f` also generates an implication
 906 constraint, so we end up with the following nested implication:
 907
 908 ?x :: Char => (?x :: Char => ?x :: Char)
 909
 910 Note that the wanted (?x :: Char) constraint may be solved in
 911 two incompatible ways:  either by using the parameter from the
 912 signature, or by using the local definition.  Our intention is
 913 that the local definition should "shadow" the parameter of the
 914 signature, and we implement this as follows: when we nest implications,
 915 we remove any implicit parameters in the outer implication, that
 916 have the same name as givens of the inner implication.
 917
 918 Here is another variation of the example:
 919
 920 f :: (?x :: Int) => Char
 921 f = let ?x = 'x' in ?x
 922
 923 This program should also be accepted: the two constraints `?x :: Int`
 924 and `?x :: Char` never exist in the same context, so they don't get to
 925 interact to cause failure.
 926
 927 Note [Superclasses and recursive dictionaries]
 928 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 929     Overlaps with Note [SUPERCLASS-LOOP 1]
 930                   Note [SUPERCLASS-LOOP 2]
 931                   Note [Recursive instances and superclases]
 932     ToDo: check overlap and delete redundant stuff
 933
 934 Right before adding a given into the inert set, we must
 935 produce some more work, that will bring the superclasses
 936 of the given into scope. The superclass constraints go into
 937 our worklist.
 938
 939 When we simplify a wanted constraint, if we first see a matching
 940 instance, we may produce new wanted work. To (1) avoid doing this work
 941 twice in the future and (2) to handle recursive dictionaries we may ``cache''
 942 this item as given into our inert set WITHOUT adding its superclass constraints,
 943 otherwise we'd be in danger of creating a loop [In fact this was the exact reason
 944 for doing the isGoodRecEv check in an older version of the type checker].
 945
 946 But now we have added partially solved constraints to the worklist which may
 947 interact with other wanteds. Consider the example:
 948
 949 Example 1:
 950
 951     class Eq b => Foo a b        --- 0-th selector
 952     instance Eq a => Foo [a] a   --- fooDFun
 953
 954 and wanted (Foo [t] t). We are first going to see that the instance matches
 955 and create an inert set that includes the solved (Foo [t] t) but not its superclasses:
 956        d1 :_g Foo [t] t                 d1 := EvDFunApp fooDFun d3
 957 Our work list is going to contain a new *wanted* goal
 958        d3 :_w Eq t
 959
 960 Ok, so how do we get recursive dictionaries, at all:
 961
 962 Example 2:
 963
 964     data D r = ZeroD | SuccD (r (D r));
 965
 966     instance (Eq (r (D r))) => Eq (D r) where
 967         ZeroD     == ZeroD     = True
 968         (SuccD a) == (SuccD b) = a == b
 969         _         == _         = False;
 970
 971     equalDC :: D [] -> D [] -> Bool;
 972     equalDC = (==);
 973
 974 We need to prove (Eq (D [])). Here's how we go:
 975
 976         d1 :_w Eq (D [])
 977
 978 by instance decl, holds if
 979         d2 :_w Eq [D []]
 980         where   d1 = dfEqD d2
 981
 982 *BUT* we have an inert set which gives us (no superclasses):
 983         d1 :_g Eq (D [])
 984 By the instance declaration of Eq we can show the 'd2' goal if
 985         d3 :_w Eq (D [])
 986         where   d2 = dfEqList d3
 987                 d1 = dfEqD d2
 988 Now, however this wanted can interact with our inert d1 to set:
 989         d3 := d1
 990 and solve the goal. Why was this interaction OK? Because, if we chase the
 991 evidence of d1 ~~> dfEqD d2 ~~-> dfEqList d3, so by setting d3 := d1 we
 992 are really setting
 993         d3 := dfEqD2 (dfEqList d3)
 994 which is FINE because the use of d3 is protected by the instance function
 995 applications.
 996
 997 So, our strategy is to try to put solved wanted dictionaries into the
 998 inert set along with their superclasses (when this is meaningful,
 999 i.e. when new wanted goals are generated) but solve a wanted dictionary
1000 from a given only in the case where the evidence variable of the
1001 wanted is mentioned in the evidence of the given (recursively through
1002 the evidence binds) in a protected way: more instance function applications
1003 than superclass selectors.
1004
1005 Here are some more examples from GHC's previous type checker
1006
1007
1008 Example 3:
1009 This code arises in the context of "Scrap Your Boilerplate with Class"
1010
1011     class Sat a
1012     class Data ctx a
1013     instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
1014     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
1015
1016     class Data Maybe a => Foo a
1017
1018     instance Foo t => Sat (Maybe t)                             -- dfunSat
1019
1020     instance Data Maybe a => Foo a                              -- dfunFoo1
1021     instance Foo a        => Foo [a]                            -- dfunFoo2
1022     instance                 Foo [Char]                         -- dfunFoo3
1023
1024 Consider generating the superclasses of the instance declaration
1025          instance Foo a => Foo [a]
1026
1027 So our problem is this
1028     d0 :_g Foo t
1029     d1 :_w Data Maybe [t]
1030
1031 We may add the given in the inert set, along with its superclasses
1032 [assuming we don't fail because there is a matching instance, see
1033  topReactionsStage, given case ]
1034   Inert:
1035     d0 :_g Foo t
1036   WorkList
1037     d01 :_g Data Maybe t  -- d2 := EvDictSuperClass d0 0
1038     d1 :_w Data Maybe [t]
1039 Then d2 can readily enter the inert, and we also do solving of the wanted
1040   Inert:
1041     d0 :_g Foo t
1042     d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1043   WorkList
1044     d2 :_w Sat (Maybe [t])
1045     d3 :_w Data Maybe t
1046     d01 :_g Data Maybe t
1047 Now, we may simplify d2 more:
1048   Inert:
1049       d0 :_g Foo t
1050       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1051       d1 :_g Data Maybe [t]
1052       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1053   WorkList:
1054       d3 :_w Data Maybe t
1055       d4 :_w Foo [t]
1056       d01 :_g Data Maybe t
1057
1058 Now, we can just solve d3.
1059   Inert
1060       d0 :_g Foo t
1061       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1062       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1063   WorkList
1064       d4 :_w Foo [t]
1065       d01 :_g Data Maybe t
1066 And now we can simplify d4 again, but since it has superclasses we *add* them to the worklist:
1067   Inert
1068       d0 :_g Foo t
1069       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1070       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1071       d4 :_g Foo [t]                  d4 := dfunFoo2 d5
1072   WorkList:
1073       d5 :_w Foo t
1074       d6 :_g Data Maybe [t]           d6 := EvDictSuperClass d4 0
1075       d01 :_g Data Maybe t
1076 Now, d5 can be solved! (and its superclass enter scope)
1077   Inert
1078       d0 :_g Foo t
1079       d1 :_s Data Maybe [t]           d1 := dfunData2 d2 d3
1080       d2 :_g Sat (Maybe [t])          d2 := dfunSat d4
1081       d4 :_g Foo [t]                  d4 := dfunFoo2 d5
1082       d5 :_g Foo t                    d5 := dfunFoo1 d7
1083   WorkList:
1084       d7 :_w Data Maybe t
1085       d6 :_g Data Maybe [t]
1086       d8 :_g Data Maybe t            d8 := EvDictSuperClass d5 0
1087       d01 :_g Data Maybe t
1088
1089 Now, two problems:
1090    [1] Suppose we pick d8 and we react him with d01. Which of the two givens should
1091        we keep? Well, we *MUST NOT* drop d01 because d8 contains recursive evidence
1092        that must not be used (look at case interactInert where both inert and workitem
1093        are givens). So we have several options:
1094        - Drop the workitem always (this will drop d8)
1095               This feels very unsafe -- what if the work item was the "good" one
1096               that should be used later to solve another wanted?
1097        - Don't drop anyone: the inert set may contain multiple givens!
1098               [This is currently implemented]
1099
1100 The "don't drop anyone" seems the most safe thing to do, so now we come to problem 2:
1101   [2] We have added both d6 and d01 in the inert set, and we are interacting our wanted
1102       d7. Now the [isRecDictEv] function in the ineration solver
1103       [case inert-given workitem-wanted] will prevent us from interacting d7 := d8
1104       precisely because chasing the evidence of d8 leads us to an unguarded use of d7.
1105
1106       So, no interaction happens there. Then we meet d01 and there is no recursion
1107       problem there [isRectDictEv] gives us the OK to interact and we do solve d7 := d01!
1108
1109 Note [SUPERCLASS-LOOP 1]
1110 ~~~~~~~~~~~~~~~~~~~~~~~~
1111 We have to be very, very careful when generating superclasses, lest we
1112 accidentally build a loop. Here's an example:
1113
1114   class S a
1115
1116   class S a => C a where { opc :: a -> a }
1117   class S b => D b where { opd :: b -> b }
1118
1119   instance C Int where
1120      opc = opd
1121
1122   instance D Int where
1123      opd = opc
1124
1125 From (instance C Int) we get the constraint set {ds1:S Int, dd:D Int}
1126 Simplifying, we may well get:
1127         $dfCInt = :C ds1 (opd dd)
1128         dd  = $dfDInt
1129         ds1 = $p1 dd
1130 Notice that we spot that we can extract ds1 from dd.
1131
1132 Alas!  Alack! We can do the same for (instance D Int):
1133
1134         $dfDInt = :D ds2 (opc dc)
1135         dc  = $dfCInt
1136         ds2 = $p1 dc
1137
1138 And now we've defined the superclass in terms of itself.
1139 Two more nasty cases are in
1140         tcrun021
1141         tcrun033
1142
1143 Solution:
1144   - Satisfy the superclass context *all by itself*
1145     (tcSimplifySuperClasses)
1146   - And do so completely; i.e. no left-over constraints
1147     to mix with the constraints arising from method declarations
1148
1149
1150 Note [SUPERCLASS-LOOP 2]
1151 ~~~~~~~~~~~~~~~~~~~~~~~~
1152 We need to be careful when adding "the constaint we are trying to prove".
1153 Suppose we are *given* d1:Ord a, and want to deduce (d2:C [a]) where
1154
1155         class Ord a => C a where
1156         instance Ord [a] => C [a] where ...
1157
1158 Then we'll use the instance decl to deduce C [a] from Ord [a], and then add the
1159 superclasses of C [a] to avails.  But we must not overwrite the binding
1160 for Ord [a] (which is obtained from Ord a) with a superclass selection or we'll just
1161 build a loop!
1162
1163 Here's another variant, immortalised in tcrun020
1164         class Monad m => C1 m
1165         class C1 m => C2 m x
1166         instance C2 Maybe Bool
1167 For the instance decl we need to build (C1 Maybe), and it's no good if
1168 we run around and add (C2 Maybe Bool) and its superclasses to the avails
1169 before we search for C1 Maybe.
1170
1171 Here's another example
1172         class Eq b => Foo a b
1173         instance Eq a => Foo [a] a
1174 If we are reducing
1175         (Foo [t] t)
1176
1177 we'll first deduce that it holds (via the instance decl).  We must not
1178 then overwrite the Eq t constraint with a superclass selection!
1179
1180 At first I had a gross hack, whereby I simply did not add superclass constraints
1181 in addWanted, though I did for addGiven and addIrred.  This was sub-optimal,
1182 because it lost legitimate superclass sharing, and it still didn't do the job:
1183 I found a very obscure program (now tcrun021) in which improvement meant the
1184 simplifier got two bites a the cherry... so something seemed to be an Stop
1185 first time, but reducible next time.
1186
1187 Now we implement the Right Solution, which is to check for loops directly
1188 when adding superclasses.  It's a bit like the occurs check in unification.
1189
1190 Note [Recursive instances and superclases]
1191 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1192 Consider this code, which arises in the context of "Scrap Your
1193 Boilerplate with Class".
1194
1195     class Sat a
1196     class Data ctx a
1197     instance  Sat (ctx Char)             => Data ctx Char
1198     instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
1199
1200     class Data Maybe a => Foo a
1201
1202     instance Foo t => Sat (Maybe t)
1203
1204     instance Data Maybe a => Foo a
1205     instance Foo a        => Foo [a]
1206     instance                 Foo [Char]
1207
1208 In the instance for Foo [a], when generating evidence for the superclasses
1209 (ie in tcSimplifySuperClasses) we need a superclass (Data Maybe [a]).
1210 Using the instance for Data, we therefore need
1211         (Sat (Maybe [a], Data Maybe a)
1212 But we are given (Foo a), and hence its superclass (Data Maybe a).
1213 So that leaves (Sat (Maybe [a])).  Using the instance for Sat means
1214 we need (Foo [a]).  And that is the very dictionary we are bulding
1215 an instance for!  So we must put that in the "givens".  So in this
1216 case we have
1217         Given:  Foo a, Foo [a]
1218         Wanted: Data Maybe [a]
1219
1220 BUT we must *not not not* put the *superclasses* of (Foo [a]) in
1221 the givens, which is what 'addGiven' would normally do. Why? Because
1222 (Data Maybe [a]) is the superclass, so we'd "satisfy" the wanted
1223 by selecting a superclass from Foo [a], which simply makes a loop.
1224
1225 On the other hand we *must* put the superclasses of (Foo a) in
1226 the givens, as you can see from the derivation described above.
1227
1228 Conclusion: in the very special case of tcSimplifySuperClasses
1229 we have one 'given' (namely the "this" dictionary) whose superclasses
1230 must not be added to 'givens' by addGiven.
1231
1232 There is a complication though.  Suppose there are equalities
1233       instance (Eq a, a~b) => Num (a,b)
1234 Then we normalise the 'givens' wrt the equalities, so the original
1235 given "this" dictionary is cast to one of a different type.  So it's a
1236 bit trickier than before to identify the "special" dictionary whose
1237 superclasses must not be added. See test
1238    indexed-types/should_run/EqInInstance
1239
1240 We need a persistent property of the dictionary to record this
1241 special-ness.  Current I'm using the InstLocOrigin (a bit of a hack,
1242 but cool), which is maintained by dictionary normalisation.
1243 Specifically, the InstLocOrigin is
1244              NoScOrigin
1245 then the no-superclass thing kicks in.  WATCH OUT if you fiddle
1246 with InstLocOrigin!
1247
1248 Note [MATCHING-SYNONYMS]
1249 ~~~~~~~~~~~~~~~~~~~~~~~~
1250 When trying to match a dictionary (D tau) to a top-level instance, or a
1251 type family equation (F taus_1 ~ tau_2) to a top-level family instance,
1252 we do *not* need to expand type synonyms because the matcher will do that for us.
1253
1254
1255 Note [RHS-FAMILY-SYNONYMS]
1256 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1257 The RHS of a family instance is represented as yet another constructor which is
1258 like a type synonym for the real RHS the programmer declared. Eg:
1259     type instance F (a,a) = [a]
1260 Becomes:
1261     :R32 a = [a]      -- internal type synonym introduced
1262     F (a,a) ~ :R32 a  -- instance
1263
1264 When we react a family instance with a type family equation in the work list
1265 we keep the synonym-using RHS without expansion.
1266
1267
1268 %************************************************************************
1269 %*                                                                      *
1270 %*          Functional dependencies, instantiation of equations
1271 %*                                                                      *
1272 %************************************************************************
1273
1274 When we spot an equality arising from a functional dependency,
1275 we now use that equality (a "wanted") to rewrite the work-item
1276 constraint right away.  This avoids two dangers
1277
1278  Danger 1: If we send the original constraint on down the pipeline
1279            it may react with an instance declaration, and in delicate
1280            situations (when a Given overlaps with an instance) that
1281            may produce new insoluble goals: see Trac #4952
1282
1283  Danger 2: If we don't rewrite the constraint, it may re-react
1284            with the same thing later, and produce the same equality
1285            again --> termination worries.
1286
1287 To achieve this required some refactoring of FunDeps.lhs (nicer
1288 now!).
1289
1290 \begin{code}
1291 rewriteWithFunDeps :: [Equation] -> CtLoc -> TcS [Ct]
1292 -- NB: The returned constraints are all Derived
1293 -- Post: returns no trivial equalities (identities) and all EvVars returned are fresh
1294 rewriteWithFunDeps eqn_pred_locs loc
1295  = do { fd_cts <- mapM (instFunDepEqn loc) eqn_pred_locs
1296       ; return (concat fd_cts) }
1297
1298 instFunDepEqn :: CtLoc -> Equation -> TcS [Ct]
1299 -- Post: Returns the position index as well as the corresponding FunDep equality
1300 instFunDepEqn loc (FDEqn { fd_qtvs = tvs, fd_eqs = eqs
1301                          , fd_pred1 = d1, fd_pred2 = d2 })
1302   = do { (subst, _) <- instFlexiTcS tvs  -- Takes account of kind substitution
1303        ; foldM (do_one subst) [] eqs }
1304   where
1305     der_loc = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
1306
1307     do_one subst ievs (FDEq { fd_ty_left = ty1, fd_ty_right = ty2 })
1308        | eqType sty1 sty2
1309        = return ievs -- Return no trivial equalities
1310        | otherwise
1311        = do { mb_eqv <- newDerived (mkTcEqPred sty1 sty2)
1312             ; case mb_eqv of
1313                  Just ev -> return (mkNonCanonical der_loc ev : ievs)
1314                  Nothing -> return ievs }
1315                    -- We are eventually going to emit FD work back in the work list so
1316                    -- it is important that we only return the /freshly created/ and not
1317                    -- some existing equality!
1318        where
1319          sty1 = Type.substTy subst ty1
1320          sty2 = Type.substTy subst ty2
1321
1322 mkEqnMsg :: (TcPredType, SDoc)
1323          -> (TcPredType, SDoc) -> TidyEnv -> TcM (TidyEnv, SDoc)
1324 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1325   = do  { zpred1 <- zonkTcPredType pred1
1326         ; zpred2 <- zonkTcPredType pred2
1327         ; let { tpred1 = tidyType tidy_env zpred1
1328               ; tpred2 = tidyType tidy_env zpred2 }
1329         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1330                           nest 2 (sep [ppr tpred1 <> comma, nest 2 from1]),
1331                           nest 2 (sep [ppr tpred2 <> comma, nest 2 from2])]
1332         ; return (tidy_env, msg) }
1333 \end{code}
1334
1335
1336
1337
1338 *********************************************************************************
1339 *                                                                               *
1340                        The top-reaction Stage
1341 *                                                                               *
1342 *********************************************************************************
1343
1344 \begin{code}
1345 topReactionsStage :: WorkItem -> TcS StopOrContinue
1346 topReactionsStage wi
1347  = do { inerts <- getTcSInerts
1348       ; tir <- doTopReact inerts wi
1349       ; case tir of
1350           NoTopInt -> return (ContinueWith wi)
1351           SomeTopInt rule what_next
1352                    -> do { traceFireTcS wi $
1353                            vcat [ ptext (sLit "Top react:") <+> text rule
1354                                 , text "WorkItem =" <+> ppr wi ]
1355                          ; return what_next } }
1356
1357 data TopInteractResult
1358  = NoTopInt
1359  | SomeTopInt { tir_rule :: String, tir_new_item :: StopOrContinue }
1360
1361
1362 doTopReact :: InertSet -> WorkItem -> TcS TopInteractResult
1363 -- The work item does not react with the inert set, so try interaction with top-level
1364 -- instances. Note:
1365 --
1366 --   (a) The place to add superclasses in not here in doTopReact stage.
1367 --       Instead superclasses are added in the worklist as part of the
1368 --       canonicalization process. See Note [Adding superclasses].
1369 --
1370 --   (b) See Note [Given constraint that matches an instance declaration]
1371 --       for some design decisions for given dictionaries.
1372
1373 doTopReact inerts workItem
1374   = do { traceTcS "doTopReact" (ppr workItem)
1375        ; case workItem of
1376            CDictCan { cc_ev = fl, cc_class = cls, cc_tyargs = xis
1377                     , cc_loc = d }
1378               -> doTopReactDict inerts fl cls xis d
1379
1380            CFunEqCan { cc_ev = fl, cc_fun = tc, cc_tyargs = args
1381                      , cc_rhs = xi, cc_loc = d }
1382               -> doTopReactFunEq workItem fl tc args xi d
1383
1384            _  -> -- Any other work item does not react with any top-level equations
1385                  return NoTopInt  }
1386
1387 --------------------
1388 doTopReactDict :: InertSet -> CtEvidence -> Class -> [Xi]
1389                -> CtLoc -> TcS TopInteractResult
1390 doTopReactDict inerts fl cls xis loc
1391   | not (isWanted fl)
1392   = try_fundeps_and_return
1393
1394   | Just ev <- lookupSolvedDict inerts pred   -- Cached
1395   = do { setEvBind dict_id (ctEvTerm ev);
1396        ; return $ SomeTopInt { tir_rule = "Dict/Top (cached)"
1397                              , tir_new_item = Stop } }
1398
1399   | otherwise  -- Not cached
1400    = do { lkup_inst_res <- matchClassInst inerts cls xis loc
1401          ; case lkup_inst_res of
1402                GenInst wtvs ev_term -> do { addSolvedDict fl
1403                                           ; solve_from_instance wtvs ev_term }
1404                NoInstance -> try_fundeps_and_return }
1405    where
1406      arising_sdoc = pprArisingAt loc
1407      dict_id = ctEvId fl
1408      pred = mkClassPred cls xis
1409
1410      solve_from_instance :: [CtEvidence] -> EvTerm -> TcS TopInteractResult
1411       -- Precondition: evidence term matches the predicate workItem
1412      solve_from_instance evs ev_term
1413         | null evs
1414         = do { traceTcS "doTopReact/found nullary instance for" $
1415                ppr dict_id
1416              ; setEvBind dict_id ev_term
1417              ; return $
1418                SomeTopInt { tir_rule = "Dict/Top (solved, no new work)"
1419                           , tir_new_item = Stop } }
1420         | otherwise
1421         = do { traceTcS "doTopReact/found non-nullary instance for" $
1422                ppr dict_id
1423              ; setEvBind dict_id ev_term
1424              ; let mk_new_wanted ev
1425                        = CNonCanonical { cc_ev  = ev
1426                                        , cc_loc = bumpCtLocDepth loc }
1427              ; updWorkListTcS (extendWorkListCts (map mk_new_wanted evs))
1428              ; return $
1429                SomeTopInt { tir_rule     = "Dict/Top (solved, more work)"
1430                           , tir_new_item = Stop } }
1431
1432      -- We didn't solve it; so try functional dependencies with
1433      -- the instance environment, and return
1434      -- NB: even if there *are* some functional dependencies against the
1435      -- instance environment, there might be a unique match, and if
1436      -- so we make sure we get on and solve it first. See Note [Weird fundeps]
1437      try_fundeps_and_return
1438        = do { instEnvs <- getInstEnvs
1439             ; let fd_eqns = improveFromInstEnv instEnvs (pred, arising_sdoc)
1440             ; fd_work <- rewriteWithFunDeps fd_eqns loc
1441             ; unless (null fd_work) (updWorkListTcS (extendWorkListEqs fd_work))
1442             ; return NoTopInt }
1443
1444 --------------------
1445 doTopReactFunEq :: Ct -> CtEvidence -> TyCon -> [Xi] -> Xi
1446                 -> CtLoc -> TcS TopInteractResult
1447 doTopReactFunEq _ct fl fun_tc args xi loc
1448   = ASSERT(isSynFamilyTyCon fun_tc) -- No associated data families have
1449                                      -- reached this far
1450     -- Look in the cache of solved funeqs
1451     do { fun_eq_cache <- getTcSInerts >>= (return . inert_solved_funeqs)
1452        ; case lookupFamHead fun_eq_cache fam_ty of {
1453            Just (ctev, rhs_ty)
1454              | ctEvFlavour ctev `canRewrite` ctEvFlavour fl
1455              -> ASSERT( not (isDerived ctev) )
1456                 succeed_with "Fun/Cache" (evTermCoercion (ctEvTerm ctev)) rhs_ty ;
1457            _other ->
1458
1459     -- Look up in top-level instances, or built-in axiom
1460     do { match_res <- matchFam fun_tc args   -- See Note [MATCHING-SYNONYMS]
1461        ; case match_res of {
1462            Nothing -> try_improve_and_return ;
1463            Just (co, ty) ->
1464
1465     -- Found a top-level instance
1466     do {    -- Add it to the solved goals
1467          unless (isDerived fl) (addSolvedFunEq fam_ty fl xi)
1468
1469        ; succeed_with "Fun/Top" co ty } } } } }
1470   where
1471     fam_ty = mkTyConApp fun_tc args
1472
1473     try_improve_and_return =
1474       do { case isBuiltInSynFamTyCon_maybe fun_tc of
1475              Just ops ->
1476                do { let eqns = sfInteractTop ops args xi
1477                   ; impsMb <- mapM (\(Pair x y) -> newDerived (mkTcEqPred x y))
1478                                    eqns
1479                   ; let work = map (mkNonCanonical loc) (catMaybes impsMb)
1480                   ; unless (null work) (updWorkListTcS (extendWorkListEqs work))
1481                   }
1482              _ -> return ()
1483          ; return NoTopInt
1484          }
1485
1486     succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
1487     succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
1488       = do { ctevs <- xCtFlavor fl [mkTcEqPred rhs_ty xi] xev
1489            ; traceTcS ("doTopReactFunEq " ++ str) (ppr ctevs)
1490            ; case ctevs of
1491                [ctev] -> updWorkListTcS $ extendWorkListEq $
1492                          CNonCanonical { cc_ev = ctev
1493                                        , cc_loc  = bumpCtLocDepth loc }
1494                ctevs -> -- No subgoal (because it's cached)
1495                         ASSERT( null ctevs) return ()
1496            ; return $ SomeTopInt { tir_rule = str
1497                                  , tir_new_item = Stop } }
1498       where
1499         xdecomp x = [EvCoercion (mkTcSymCo co `mkTcTransCo` evTermCoercion x)]
1500         xcomp [x] = EvCoercion (co `mkTcTransCo` evTermCoercion x)
1501         xcomp _   = panic "No more goals!"
1502         xev = XEvTerm xcomp xdecomp
1503 \end{code}
1504
1505
1506 Note [FunDep and implicit parameter reactions]
1507 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1508 Currently, our story of interacting two dictionaries (or a dictionary
1509 and top-level instances) for functional dependencies, and implicit
1510 paramters, is that we simply produce new Derived equalities.  So for example
1511
1512         class D a b | a -> b where ...
1513     Inert:
1514         d1 :g D Int Bool
1515     WorkItem:
1516         d2 :w D Int alpha
1517
1518     We generate the extra work item
1519         cv :d alpha ~ Bool
1520     where 'cv' is currently unused.  However, this new item can perhaps be
1521     spontaneously solved to become given and react with d2,
1522     discharging it in favour of a new constraint d2' thus:
1523         d2' :w D Int Bool
1524         d2 := d2' |> D Int cv
1525     Now d2' can be discharged from d1
1526
1527 We could be more aggressive and try to *immediately* solve the dictionary
1528 using those extra equalities, but that requires those equalities to carry
1529 evidence and derived do not carry evidence.
1530
1531 If that were the case with the same inert set and work item we might dischard
1532 d2 directly:
1533
1534         cv :w alpha ~ Bool
1535         d2 := d1 |> D Int cv
1536
1537 But in general it's a bit painful to figure out the necessary coercion,
1538 so we just take the first approach. Here is a better example. Consider:
1539     class C a b c | a -> b
1540 And:
1541      [Given]  d1 : C T Int Char
1542      [Wanted] d2 : C T beta Int
1543 In this case, it's *not even possible* to solve the wanted immediately.
1544 So we should simply output the functional dependency and add this guy
1545 [but NOT its superclasses] back in the worklist. Even worse:
1546      [Given] d1 : C T Int beta
1547      [Wanted] d2: C T beta Int
1548 Then it is solvable, but its very hard to detect this on the spot.
1549
1550 It's exactly the same with implicit parameters, except that the
1551 "aggressive" approach would be much easier to implement.
1552
1553 Note [When improvement happens]
1554 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1555 We fire an improvement rule when
1556
1557   * Two constraints match (modulo the fundep)
1558       e.g. C t1 t2, C t1 t3    where C a b | a->b
1559     The two match because the first arg is identical
1560
1561 Note that we *do* fire the improvement if one is Given and one is Derived (e.g. a
1562 superclass of a Wanted goal) or if both are Given.
1563
1564 Example (tcfail138)
1565     class L a b | a -> b
1566     class (G a, L a b) => C a b
1567
1568     instance C a b' => G (Maybe a)
1569     instance C a b  => C (Maybe a) a
1570     instance L (Maybe a) a
1571
1572 When solving the superclasses of the (C (Maybe a) a) instance, we get
1573   Given:  C a b  ... and hance by superclasses, (G a, L a b)
1574   Wanted: G (Maybe a)
1575 Use the instance decl to get
1576   Wanted: C a b'
1577 The (C a b') is inert, so we generate its Derived superclasses (L a b'),
1578 and now we need improvement between that derived superclass an the Given (L a b)
1579
1580 Test typecheck/should_fail/FDsFromGivens also shows why it's a good idea to
1581 emit Derived FDs for givens as well.
1582
1583 Note [Weird fundeps]
1584 ~~~~~~~~~~~~~~~~~~~~
1585 Consider   class Het a b | a -> b where
1586               het :: m (f c) -> a -> m b
1587
1588            class GHet (a :: * -> *) (b :: * -> *) | a -> b
1589            instance            GHet (K a) (K [a])
1590            instance Het a b => GHet (K a) (K b)
1591
1592 The two instances don't actually conflict on their fundeps,
1593 although it's pretty strange.  So they are both accepted. Now
1594 try   [W] GHet (K Int) (K Bool)
1595 This triggers fudeps from both instance decls; but it also
1596 matches a *unique* instance decl, and we should go ahead and
1597 pick that one right now.  Otherwise, if we don't, it ends up
1598 unsolved in the inert set and is reported as an error.
1599
1600 Trac #7875 is a case in point.
1601
1602 Note [Overriding implicit parameters]
1603 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1604 Consider
1605    f :: (?x::a) -> Bool -> a
1606
1607    g v = let ?x::Int = 3
1608          in (f v, let ?x::Bool = True in f v)
1609
1610 This should probably be well typed, with
1611    g :: Bool -> (Int, Bool)
1612
1613 So the inner binding for ?x::Bool *overrides* the outer one.
1614 Hence a work-item Given overrides an inert-item Given.
1615
1616 Note [Given constraint that matches an instance declaration]
1617 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1618 What should we do when we discover that one (or more) top-level
1619 instances match a given (or solved) class constraint? We have
1620 two possibilities:
1621
1622   1. Reject the program. The reason is that there may not be a unique
1623      best strategy for the solver. Example, from the OutsideIn(X) paper:
1624        instance P x => Q [x]
1625        instance (x ~ y) => R [x] y
1626
1627        wob :: forall a b. (Q [b], R b a) => a -> Int
1628
1629        g :: forall a. Q [a] => [a] -> Int
1630        g x = wob x
1631
1632        will generate the impliation constraint:
1633             Q [a] => (Q [beta], R beta [a])
1634        If we react (Q [beta]) with its top-level axiom, we end up with a
1635        (P beta), which we have no way of discharging. On the other hand,
1636        if we react R beta [a] with the top-level we get  (beta ~ a), which
1637        is solvable and can help us rewrite (Q [beta]) to (Q [a]) which is
1638        now solvable by the given Q [a].
1639
1640      However, this option is restrictive, for instance [Example 3] from
1641      Note [Recursive instances and superclases] will fail to work.
1642
1643   2. Ignore the problem, hoping that the situations where there exist indeed
1644      such multiple strategies are rare: Indeed the cause of the previous
1645      problem is that (R [x] y) yields the new work (x ~ y) which can be
1646      *spontaneously* solved, not using the givens.
1647
1648 We are choosing option 2 below but we might consider having a flag as well.
1649
1650
1651 Note [New Wanted Superclass Work]
1652 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1653 Even in the case of wanted constraints, we may add some superclasses
1654 as new given work. The reason is:
1655
1656         To allow FD-like improvement for type families. Assume that
1657         we have a class
1658              class C a b | a -> b
1659         and we have to solve the implication constraint:
1660              C a b => C a beta
1661         Then, FD improvement can help us to produce a new wanted (beta ~ b)
1662
1663         We want to have the same effect with the type family encoding of
1664         functional dependencies. Namely, consider:
1665              class (F a ~ b) => C a b
1666         Now suppose that we have:
1667                given: C a b
1668                wanted: C a beta
1669         By interacting the given we will get given (F a ~ b) which is not
1670         enough by itself to make us discharge (C a beta). However, we
1671         may create a new derived equality from the super-class of the
1672         wanted constraint (C a beta), namely derived (F a ~ beta).
1673         Now we may interact this with given (F a ~ b) to get:
1674                   derived :  beta ~ b
1675         But 'beta' is a touchable unification variable, and hence OK to
1676         unify it with 'b', replacing the derived evidence with the identity.
1677
1678         This requires trySpontaneousSolve to solve *derived*
1679         equalities that have a touchable in their RHS, *in addition*
1680         to solving wanted equalities.
1681
1682 We also need to somehow use the superclasses to quantify over a minimal,
1683 constraint see note [Minimize by Superclasses] in TcSimplify.
1684
1685
1686 Finally, here is another example where this is useful.
1687
1688 Example 1:
1689 ----------
1690    class (F a ~ b) => C a b
1691 And we are given the wanteds:
1692       w1 : C a b
1693       w2 : C a c
1694       w3 : b ~ c
1695 We surely do *not* want to quantify over (b ~ c), since if someone provides
1696 dictionaries for (C a b) and (C a c), these dictionaries can provide a proof
1697 of (b ~ c), hence no extra evidence is necessary. Here is what will happen:
1698
1699      Step 1: We will get new *given* superclass work,
1700              provisionally to our solving of w1 and w2
1701
1702                g1: F a ~ b, g2 : F a ~ c,
1703                w1 : C a b, w2 : C a c, w3 : b ~ c
1704
1705              The evidence for g1 and g2 is a superclass evidence term:
1706
1707                g1 := sc w1, g2 := sc w2
1708
1709      Step 2: The givens will solve the wanted w3, so that
1710                w3 := sym (sc w1) ; sc w2
1711
1712      Step 3: Now, one may naively assume that then w2 can be solve from w1
1713              after rewriting with the (now solved equality) (b ~ c).
1714
1715              But this rewriting is ruled out by the isGoodRectDict!
1716
1717 Conclusion, we will (correctly) end up with the unsolved goals
1718     (C a b, C a c)
1719
1720 NB: The desugarer needs be more clever to deal with equalities
1721     that participate in recursive dictionary bindings.
1722
1723 \begin{code}
1724 data LookupInstResult
1725   = NoInstance
1726   | GenInst [CtEvidence] EvTerm
1727
1728 instance Outputable LookupInstResult where
1729   ppr NoInstance = text "NoInstance"
1730   ppr (GenInst ev t) = text "GenInst" <+> ppr ev <+> ppr t
1731
1732
1733 matchClassInst :: InertSet -> Class -> [Type] -> CtLoc -> TcS LookupInstResult
1734
1735 matchClassInst _ clas [ ty ] _
1736   | className clas == knownNatClassName
1737   , Just n <- isNumLitTy ty = makeDict (EvNum n)
1738
1739   | className clas == knownSymbolClassName
1740   , Just s <- isStrLitTy ty = makeDict (EvStr s)
1741
1742   where
1743   {- This adds a coercion that will convert the literal into a dictionary
1744      of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]
1745      in TcEvidence.  The coercion happens in 2 steps:
1746
1747      Integer -> SNat n     -- representation of literal to singleton
1748      SNat n  -> KnownNat n -- singleton to dictionary
1749
1750      The process is mirrored for Symbols:
1751      String    -> SSymbol n
1752      SSymbol n -> KnownSymbol n
1753   -}
1754   makeDict evLit =
1755     case unwrapNewTyCon_maybe (classTyCon clas) of
1756       Just (_,_, axDict)
1757         | [ meth ]   <- classMethods clas
1758         , Just tcRep <- tyConAppTyCon_maybe -- SNat
1759                       $ funResultTy         -- SNat n
1760                       $ dropForAlls         -- KnownNat n => SNat n
1761                       $ idType meth         -- forall n. KnownNat n => SNat n
1762         , Just (_,_,axRep) <- unwrapNewTyCon_maybe tcRep
1763         -> return $
1764            let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo axRep  [ty]
1765                co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo axDict [ty]
1766            in GenInst [] $ EvCast (EvLit evLit) (mkTcTransCo co1 co2)
1767
1768       _ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas)
1769                      $$ vcat (map (ppr . idType) (classMethods clas)))
1770
1771 matchClassInst _ clas [ ty1, ty2 ] _
1772   | clas == coercibleClass =  do
1773       traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2
1774       rdr_env <- getGlobalRdrEnvTcS
1775       safeMode <- safeLanguageOn `fmap` getDynFlags
1776       ev <- getCoercibleInst safeMode rdr_env ty1 ty2
1777       traceTcS "matchClassInst returned" $ ppr ev
1778       return ev
1779
1780 matchClassInst inerts clas tys loc
1781    = do { dflags <- getDynFlags
1782         ; untch <- getUntouchables
1783         ; traceTcS "matchClassInst" $ vcat [ text "pred =" <+> ppr pred
1784                                            , text "inerts=" <+> ppr inerts
1785                                            , text "untouchables=" <+> ppr untch ]
1786         ; instEnvs <- getInstEnvs
1787         ; case lookupInstEnv instEnvs clas tys of
1788             ([], _, _)               -- Nothing matches
1789                 -> do { traceTcS "matchClass not matching" $
1790                         vcat [ text "dict" <+> ppr pred ]
1791                       ; return NoInstance }
1792
1793             ([(ispec, inst_tys)], [], _) -- A single match
1794                 | not (xopt Opt_IncoherentInstances dflags)
1795                 , given_overlap untch
1796                 -> -- See Note [Instance and Given overlap]
1797                    do { traceTcS "Delaying instance application" $
1798                           vcat [ text "Workitem=" <+> pprType (mkClassPred clas tys)
1799                                , text "Relevant given dictionaries=" <+> ppr givens_for_this_clas ]
1800                       ; return NoInstance  }
1801
1802                 | otherwise
1803                 -> do   { let dfun_id = instanceDFunId ispec
1804                         ; traceTcS "matchClass success" $
1805                           vcat [text "dict" <+> ppr pred,
1806                                 text "witness" <+> ppr dfun_id
1807                                                <+> ppr (idType dfun_id) ]
1808                                   -- Record that this dfun is needed
1809                         ; match_one dfun_id inst_tys }
1810
1811             (matches, _, _)    -- More than one matches
1812                                -- Defer any reactions of a multitude
1813                                -- until we learn more about the reagent
1814                 -> do   { traceTcS "matchClass multiple matches, deferring choice" $
1815                           vcat [text "dict" <+> ppr pred,
1816                                 text "matches" <+> ppr matches]
1817                         ; return NoInstance } }
1818    where
1819      pred = mkClassPred clas tys
1820
1821      match_one :: DFunId -> [Maybe TcType] -> TcS LookupInstResult
1822                   -- See Note [DFunInstType: instantiating types] in InstEnv
1823      match_one dfun_id mb_inst_tys
1824        = do { checkWellStagedDFun pred dfun_id loc
1825             ; (tys, dfun_phi) <- instDFunType dfun_id mb_inst_tys
1826             ; let (theta, _) = tcSplitPhiTy dfun_phi
1827             ; if null theta then
1828                   return (GenInst [] (EvDFunApp dfun_id tys []))
1829               else do
1830             { evc_vars <- instDFunConstraints theta
1831             ; let new_ev_vars = freshGoals evc_vars
1832                       -- new_ev_vars are only the real new variables that can be emitted
1833                   dfun_app = EvDFunApp dfun_id tys (getEvTerms evc_vars)
1834             ; return $ GenInst new_ev_vars dfun_app } }
1835
1836      givens_for_this_clas :: Cts
1837      givens_for_this_clas
1838          = lookupUFM (cts_given (inert_dicts $ inert_cans inerts)) clas
1839              `orElse` emptyCts
1840
1841      given_overlap :: Untouchables -> Bool
1842      given_overlap untch = anyBag (matchable untch) givens_for_this_clas
1843
1844      matchable untch (CDictCan { cc_class = clas_g, cc_tyargs = sys
1845                                , cc_ev = fl })
1846        | isGiven fl
1847        = ASSERT( clas_g == clas )
1848          case tcUnifyTys (\tv -> if isTouchableMetaTyVar untch tv &&
1849                                     tv `elemVarSet` tyVarsOfTypes tys
1850                                  then BindMe else Skolem) tys sys of
1851        -- We can't learn anything more about any variable at this point, so the only
1852        -- cause of overlap can be by an instantiation of a touchable unification
1853        -- variable. Hence we only bind touchable unification variables. In addition,
1854        -- we use tcUnifyTys instead of tcMatchTys to rule out cyclic substitutions.
1855             Nothing -> False
1856             Just _  -> True
1857        | otherwise = False -- No overlap with a solved, already been taken care of
1858                            -- by the overlap check with the instance environment.
1859      matchable _tys ct = pprPanic "Expecting dictionary!" (ppr ct)
1860
1861 -- See Note [Coercible Instances]
1862 -- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
1863 getCoercibleInst :: Bool -> GlobalRdrEnv -> TcType -> TcType -> TcS LookupInstResult
1864 getCoercibleInst safeMode rdr_env ty1 ty2
1865   | ty1 `eqType` ty2
1866   = do return $ GenInst []
1867               $ EvCoercible (EvCoercibleRefl ty1)
1868
1869   | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
1870     Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
1871     tc1 == tc2,
1872     nominalArgsAgree tc1 tyArgs1 tyArgs2,
1873     not safeMode || all (dataConsInScope rdr_env) (tyConsOfTyCon tc1)
1874   = do -- Mark all used data constructors as used
1875        when safeMode $ mapM_ (markDataConsAsUsed rdr_env) (tyConsOfTyCon tc1)
1876        -- We want evidence for all type arguments of role R
1877        arg_evs <- flip mapM (zip3 (tyConRoles tc1) tyArgs1 tyArgs2) $ \(r,ta1,ta2) ->
1878          case r of Nominal -> return (Nothing, EvCoercibleArgN ta1 {- == ta2, due to nominalArgsAgree -})
1879                    Representational -> do
1880                         ct_ev <- requestCoercible ta1 ta2
1881                         return (freshGoal ct_ev, EvCoercibleArgR (getEvTerm ct_ev))
1882                    Phantom -> do
1883                         return (Nothing, EvCoercibleArgP ta1 ta2)
1884        return $ GenInst (mapMaybe fst arg_evs)
1885               $ EvCoercible (EvCoercibleTyCon tc1 (map snd arg_evs))
1886
1887   | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
1888     Just (_, _, _) <- unwrapNewTyCon_maybe tc,
1889     not (isRecursiveTyCon tc),
1890     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
1891   = do markDataConsAsUsed rdr_env tc
1892        let concTy = newTyConInstRhs tc tyArgs
1893        ct_ev <- requestCoercible concTy ty2
1894        return $ GenInst (freshGoals [ct_ev])
1895               $ EvCoercible (EvCoercibleNewType CLeft tc tyArgs (getEvTerm ct_ev))
1896
1897   | Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
1898     Just (_, _, _) <- unwrapNewTyCon_maybe tc,
1899     not (isRecursiveTyCon tc),
1900     dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
1901   = do markDataConsAsUsed rdr_env tc
1902        let concTy = newTyConInstRhs tc tyArgs
1903        ct_ev <- requestCoercible ty1 concTy
1904        return $ GenInst (freshGoals [ct_ev])
1905               $ EvCoercible (EvCoercibleNewType CRight tc tyArgs (getEvTerm ct_ev))
1906
1907   | otherwise
1908   = return NoInstance
1909
1910
1911 nominalArgsAgree :: TyCon -> [Type] -> [Type] -> Bool
1912 nominalArgsAgree tc tys1 tys2 = all ok $ zip3 (tyConRoles tc) tys1 tys2
1913   where ok (r,t1,t2) = r /= Nominal || t1 `eqType` t2
1914
1915 dataConsInScope :: GlobalRdrEnv -> TyCon -> Bool
1916 dataConsInScope rdr_env tc = not hidden_data_cons
1917   where
1918     data_con_names = map dataConName (tyConDataCons tc)
1919     hidden_data_cons = not (isWiredInName (tyConName tc)) &&
1920                        (isAbstractTyCon tc || any not_in_scope data_con_names)
1921     not_in_scope dc  = null (lookupGRE_Name rdr_env dc)
1922
1923 markDataConsAsUsed :: GlobalRdrEnv -> TyCon -> TcS ()
1924 markDataConsAsUsed rdr_env tc = addUsedRdrNamesTcS
1925   [ mkRdrQual (is_as (is_decl imp_spec)) occ
1926   | dc <- tyConDataCons tc
1927   , let dc_name = dataConName dc
1928         occ  = nameOccName dc_name
1929         gres = lookupGRE_Name rdr_env dc_name
1930   , not (null gres)
1931   , Imported (imp_spec:_) <- [gre_prov (head gres)] ]
1932
1933 requestCoercible :: TcType -> TcType -> TcS MaybeNew
1934 requestCoercible ty1 ty2 = newWantedEvVar (coercibleClass `mkClassPred` [ty1, ty2])
1935
1936 \end{code}
1937
1938 Note [Coercible Instances]
1939 ~~~~~~~~~~~~~~~~~~~~~~~~~~
1940 The class Coercible is special: There are no regular instances, and the user
1941 cannot even define them. Instead, the type checker will create instances and
1942 their evidence out of thin air, in getCoercibleInst. The following “instances”
1943 are present:
1944
1945  1. instance Coercible a a
1946     for any type a.
1947  2. instance (Coercible t1_r t1'_r, Coercible t2_r t2_r',...) =>
1948        Coercible (C t1_r  t2_r  ... t1_p  t2_p  ... t1_n t2_n ...)
1949                  (C t1_r' t2_r' ... t1_p' t2_p' ... t1_n t2_n ...)
1950     for a type constructor C where
1951      * the nominal type arguments are not changed,
1952      * the phantom type arguments may change arbitrarily
1953      * the representational type arguments are again Coercible
1954     Furthermore in Safe Haskell code, we check that
1955      * the data constructors of C are in scope and
1956      * the data constructors of all type constructors used in the definition of C are in scope.
1957        This is required as otherwise the previous check can be circumvented by
1958        just adding a local data type around C.
1959  3. instance Coercible r b => Coercible (NT t1 t2 ...) b
1960     instance Coercible a r => Coercible a (NT t1 t2 ...)
1961     for a newtype constructor NT where
1962      * NT is not recursive
1963      * r is the concrete type of NT, instantiated with the arguments t1 t2 ...
1964      * the data constructors of NT are in scope.
1965
1966 These three shapes of instances correspond to the three constructors of
1967 EvCoercible (defined in EvEvidence). They are assembled here and turned to Core
1968 by dsEvTerm in DsBinds.
1969
1970
1971 Note [Instance and Given overlap]
1972 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1973 Assume that we have an inert set that looks as follows:
1974        [Given] D [Int]
1975 And an instance declaration:
1976        instance C a => D [a]
1977 A new wanted comes along of the form:
1978        [Wanted] D [alpha]
1979
1980 One possibility is to apply the instance declaration which will leave us
1981 with an unsolvable goal (C alpha). However, later on a new constraint may
1982 arise (for instance due to a functional dependency between two later dictionaries),
1983 that will add the equality (alpha ~ Int), in which case our ([Wanted] D [alpha])
1984 will be transformed to [Wanted] D [Int], which could have been discharged by the given.
1985
1986 The solution is that in matchClassInst and eventually in topReact, we get back with
1987 a matching instance, only when there is no Given in the inerts which is unifiable to
1988 this particular dictionary.
1989
1990 The end effect is that, much as we do for overlapping instances, we delay choosing a
1991 class instance if there is a possibility of another instance OR a given to match our
1992 constraint later on. This fixes bugs #4981 and #5002.
1993
1994 This is arguably not easy to appear in practice due to our aggressive prioritization
1995 of equality solving over other constraints, but it is possible. I've added a test case
1996 in typecheck/should-compile/GivenOverlapping.hs
1997
1998 We ignore the overlap problem if -XIncoherentInstances is in force: see
1999 Trac #6002 for a worked-out example where this makes a difference.
2000
2001 Moreover notice that our goals here are different than the goals of the top-level
2002 overlapping checks. There we are interested in validating the following principle:
2003
2004     If we inline a function f at a site where the same global instance environment
2005     is available as the instance environment at the definition site of f then we
2006     should get the same behaviour.
2007
2008 But for the Given Overlap check our goal is just related to completeness of
2009 constraint solving.