compiler/typecheck/TcSimplify.lhs

   1 \begin{code}
   2 module TcSimplify(
   3        simplifyInfer,
   4        simplifyDefault, simplifyDeriv,
   5        simplifyRule, simplifyTop, simplifyInteractive
   6   ) where
   7
   8 #include "HsVersions.h"
   9
  10 import HsSyn
  11 import TcRnMonad
  12 import TcErrors
  13 import TcMType
  14 import TcType
  15 import TcSMonad
  16 import TcInteract
  17 import Inst
  18 import Unify( niFixTvSubst, niSubstTvSet )
  19 import Var
  20 import VarSet
  21 import VarEnv
  22 import TypeRep
  23
  24 import Name
  25 import NameEnv  ( emptyNameEnv )
  26 import Bag
  27 import ListSetOps
  28 import Util
  29 import PrelInfo
  30 import PrelNames
  31 import Class            ( classKey )
  32 import BasicTypes       ( RuleName, TopLevelFlag, isTopLevel )
  33 import Control.Monad    ( when )
  34 import Outputable
  35 import FastString
  36 \end{code}
  37
  38
  39 *********************************************************************************
  40 *                                                                               *
  41 *                           External interface                                  *
  42 *                                                                               *
  43 *********************************************************************************
  44
  45 \begin{code}
  46 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
  47 -- Simplify top-level constraints
  48 -- Usually these will be implications,
  49 -- but when there is nothing to quantify we don't wrap
  50 -- in a degenerate implication, so we do that here instead
  51 simplifyTop wanteds
  52   = simplifyCheck SimplCheck wanteds
  53
  54 ------------------
  55 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
  56 simplifyInteractive wanteds
  57   = simplifyCheck SimplInteractive wanteds
  58
  59 ------------------
  60 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
  61                 -> TcM ()       -- Succeeds iff the constraint is soluble
  62 simplifyDefault theta
  63   = do { wanted <- newFlatWanteds DefaultOrigin theta
  64        ; _ignored_ev_binds <- simplifyCheck SimplCheck (mkFlatWC wanted)
  65        ; return () }
  66 \end{code}
  67
  68
  69
  70 *********************************************************************************
  71 *                                                                                 *
  72 *                            Deriving
  73 *                                                                                 *
  74 ***********************************************************************************
  75
  76 \begin{code}
  77 simplifyDeriv :: CtOrigin
  78                 -> [TyVar]
  79                 -> ThetaType            -- Wanted
  80                 -> TcM ThetaType        -- Needed
  81 -- Given  instance (wanted) => C inst_ty
  82 -- Simplify 'wanted' as much as possibles
  83 -- Fail if not possible
  84 simplifyDeriv orig tvs theta
  85   = do { tvs_skols <- tcInstSuperSkolTyVars tvs -- Skolemize
  86                    -- One reason is that the constraint solving machinery
  87                    -- expects *TcTyVars* not TyVars.  Another is that
  88                    -- when looking up instances we don't want overlap
  89                    -- of type variables
  90
  91        ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
  92              subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
  93
  94        ; wanted <- newFlatWanteds orig (substTheta skol_subst theta)
  95
  96        ; traceTc "simplifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
  97        ; (residual_wanted, _binds)
  98              <- runTcS SimplInfer NoUntouchables $
  99                 solveWanteds emptyInert (mkFlatWC wanted)
 100
 101        ; let (good, bad) = partitionBagWith get_good (wc_flat residual_wanted)
 102                          -- See Note [Exotic derived instance contexts]
 103              get_good :: WantedEvVar -> Either PredType WantedEvVar
 104              get_good wev | validDerivPred p = Left p
 105                           | otherwise        = Right wev
 106                           where p = evVarOfPred wev
 107
 108        ; reportUnsolved (residual_wanted { wc_flat = bad })
 109
 110        ; let min_theta = mkMinimalBySCs (bagToList good)
 111        ; return (substTheta subst_skol min_theta) }
 112 \end{code}
 113
 114 Note [Exotic derived instance contexts]
 115 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 116 In a 'derived' instance declaration, we *infer* the context.  It's a
 117 bit unclear what rules we should apply for this; the Haskell report is
 118 silent.  Obviously, constraints like (Eq a) are fine, but what about
 119         data T f a = MkT (f a) deriving( Eq )
 120 where we'd get an Eq (f a) constraint.  That's probably fine too.
 121
 122 One could go further: consider
 123         data T a b c = MkT (Foo a b c) deriving( Eq )
 124         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
 125
 126 Notice that this instance (just) satisfies the Paterson termination
 127 conditions.  Then we *could* derive an instance decl like this:
 128
 129         instance (C Int a, Eq b, Eq c) => Eq (T a b c)
 130 even though there is no instance for (C Int a), because there just
 131 *might* be an instance for, say, (C Int Bool) at a site where we
 132 need the equality instance for T's.
 133
 134 However, this seems pretty exotic, and it's quite tricky to allow
 135 this, and yet give sensible error messages in the (much more common)
 136 case where we really want that instance decl for C.
 137
 138 So for now we simply require that the derived instance context
 139 should have only type-variable constraints.
 140
 141 Here is another example:
 142         data Fix f = In (f (Fix f)) deriving( Eq )
 143 Here, if we are prepared to allow -XUndecidableInstances we
 144 could derive the instance
 145         instance Eq (f (Fix f)) => Eq (Fix f)
 146 but this is so delicate that I don't think it should happen inside
 147 'deriving'. If you want this, write it yourself!
 148
 149 NB: if you want to lift this condition, make sure you still meet the
 150 termination conditions!  If not, the deriving mechanism generates
 151 larger and larger constraints.  Example:
 152   data Succ a = S a
 153   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
 154
 155 Note the lack of a Show instance for Succ.  First we'll generate
 156   instance (Show (Succ a), Show a) => Show (Seq a)
 157 and then
 158   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
 159 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
 160
 161 The bottom line
 162 ~~~~~~~~~~~~~~~
 163 Allow constraints which consist only of type variables, with no repeats.
 164
 165 *********************************************************************************
 166 *                                                                                 *
 167 *                            Inference
 168 *                                                                                 *
 169 ***********************************************************************************
 170
 171 \begin{code}
 172 simplifyInfer :: TopLevelFlag
 173               -> Bool                  -- Apply monomorphism restriction
 174               -> [(Name, TcTauType)]   -- Variables to be generalised,
 175                                        -- and their tau-types
 176               -> WantedConstraints
 177               -> TcM ([TcTyVar],    -- Quantify over these type variables
 178                       [EvVar],      -- ... and these constraints
 179                       TcEvBinds)    -- ... binding these evidence variables
 180 simplifyInfer top_lvl apply_mr name_taus wanteds
 181   | isEmptyWC wanteds
 182   = do { gbl_tvs     <- tcGetGlobalTyVars            -- Already zonked
 183        ; zonked_taus <- zonkTcTypes (map snd name_taus)
 184        ; let tvs_to_quantify = get_tau_tvs zonked_taus `minusVarSet` gbl_tvs
 185        ; qtvs <- zonkQuantifiedTyVars (varSetElems tvs_to_quantify)
 186        ; return (qtvs, [], emptyTcEvBinds) }
 187
 188   | otherwise
 189   = do { zonked_wanteds <- zonkWC wanteds
 190        ; zonked_taus    <- zonkTcTypes (map snd name_taus)
 191        ; gbl_tvs        <- tcGetGlobalTyVars
 192
 193        ; traceTc "simplifyInfer {"  $ vcat
 194              [ ptext (sLit "apply_mr =") <+> ppr apply_mr
 195              , ptext (sLit "zonked_taus =") <+> ppr zonked_taus
 196              , ptext (sLit "wanted =") <+> ppr zonked_wanteds
 197              ]
 198
 199              -- Step 1
 200              -- Make a guess at the quantified type variables
 201              -- Then split the constraints on the baisis of those tyvars
 202              -- to avoid unnecessarily simplifying a class constraint
 203              -- See Note [Avoid unecessary constraint simplification]
 204        ; let zonked_tau_tvs = get_tau_tvs zonked_taus
 205              proto_qtvs = growWanteds gbl_tvs zonked_wanteds $
 206                           zonked_tau_tvs `minusVarSet` gbl_tvs
 207              (perhaps_bound, surely_free)
 208                         = partitionBag (quantifyMe proto_qtvs) (wc_flat zonked_wanteds)
 209
 210        ; traceTc "simplifyInfer proto"  $ vcat
 211              [ ptext (sLit "zonked_tau_tvs =") <+> ppr zonked_tau_tvs
 212              , ptext (sLit "proto_qtvs =") <+> ppr proto_qtvs
 213              , ptext (sLit "surely_fref =") <+> ppr surely_free
 214              ]
 215
 216        ; emitFlats surely_free
 217        ; traceTc "sinf"  $ vcat
 218              [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
 219              , ptext (sLit "surely_free   =") <+> ppr surely_free
 220              ]
 221
 222             -- Step 2
 223             -- Now simplify the possibly-bound constraints
 224        ; (simpl_results, tc_binds0)
 225            <- runTcS SimplInfer NoUntouchables $
 226               simplifyWithApprox (zonked_wanteds { wc_flat = perhaps_bound })
 227
 228        ; when (insolubleWC simpl_results)  -- Fail fast if there is an insoluble constraint
 229               (do { reportUnsolved simpl_results; failM })
 230
 231             -- Step 3
 232             -- Split again simplified_perhaps_bound, because some unifications
 233             -- may have happened, and emit the free constraints.
 234        ; gbl_tvs        <- tcGetGlobalTyVars
 235        ; zonked_tau_tvs <- zonkTcTyVarsAndFV zonked_tau_tvs
 236        ; zonked_simples <- zonkWantedEvVars (wc_flat simpl_results)
 237        ; let init_tvs        = zonked_tau_tvs `minusVarSet` gbl_tvs
 238              mr_qtvs         = init_tvs `minusVarSet` constrained_tvs
 239              constrained_tvs = tyVarsOfEvVarXs zonked_simples
 240              qtvs            = growWantedEVs gbl_tvs zonked_simples init_tvs
 241              (final_qtvs, (bound, free))
 242                 | apply_mr  = (mr_qtvs, (emptyBag, zonked_simples))
 243                 | otherwise = (qtvs,    partitionBag (quantifyMe qtvs) zonked_simples)
 244        ; emitFlats free
 245
 246        ; if isEmptyVarSet final_qtvs && isEmptyBag bound
 247          then ASSERT( isEmptyBag (wc_insol simpl_results) )
 248               do { traceTc "} simplifyInfer/no quantification" empty
 249                  ; emitImplications (wc_impl simpl_results)
 250                  ; return ([], [], EvBinds tc_binds0) }
 251          else do
 252
 253             -- Step 4, zonk quantified variables
 254        { let minimal_flat_preds = mkMinimalBySCs $ map evVarOfPred $ bagToList bound
 255        ; let poly_ids = [ (name, mkSigmaTy [] minimal_flat_preds ty)
 256                         | (name, ty) <- name_taus ]
 257                         -- Don't add the quantified variables here, because
 258                         -- they are also bound in ic_skols and we want them to be
 259                         -- tidied uniformly
 260              skol_info = InferSkol poly_ids
 261
 262        ; gloc <- getCtLoc skol_info
 263        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs)
 264
 265             -- Step 5
 266             -- Minimize `bound' and emit an implication
 267        ; minimal_bound_ev_vars <- mapM TcMType.newEvVar minimal_flat_preds
 268        ; ev_binds_var <- newTcEvBinds
 269        ; mapBagM_ (\(EvBind evar etrm) -> addTcEvBind ev_binds_var evar etrm) tc_binds0
 270        ; lcl_env <- getLclTypeEnv
 271        ; let implic = Implic { ic_untch    = NoUntouchables
 272                              , ic_env      = lcl_env
 273                              , ic_skols    = mkVarSet qtvs_to_return
 274                              , ic_given    = minimal_bound_ev_vars
 275                              , ic_wanted   = simpl_results { wc_flat = bound }
 276                              , ic_insol    = False
 277                              , ic_binds    = ev_binds_var
 278                              , ic_loc      = gloc }
 279        ; emitImplication implic
 280        ; traceTc "} simplifyInfer/produced residual implication for quantification" $
 281              vcat [ ptext (sLit "implic =") <+> ppr implic
 282                        -- ic_skols, ic_given give rest of result
 283                   , ptext (sLit "qtvs =") <+> ppr final_qtvs
 284                   , ptext (sLit "spb =") <+> ppr zonked_simples
 285                   , ptext (sLit "bound =") <+> ppr bound ]
 286
 287
 288
 289        ; return (qtvs_to_return, minimal_bound_ev_vars, TcEvBinds ev_binds_var) } }
 290   where
 291     get_tau_tvs | isTopLevel top_lvl = tyVarsOfTypes
 292                 | otherwise          = exactTyVarsOfTypes
 293      -- See Note [Silly type synonym] in TcType
 294 \end{code}
 295
 296
 297 Note [Minimize by Superclasses]
 298 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 299
 300 When we quantify over a constraint, in simplifyInfer we need to
 301 quantify over a constraint that is minimal in some sense: For
 302 instance, if the final wanted constraint is (Eq alpha, Ord alpha),
 303 we'd like to quantify over Ord alpha, because we can just get Eq alpha
 304 from superclass selection from Ord alpha. This minimization is what
 305 mkMinimalBySCs does. Then, simplifyInfer uses the minimal constraint
 306 to check the original wanted.
 307
 308 \begin{code}
 309 simplifyWithApprox :: WantedConstraints -> TcS WantedConstraints
 310 simplifyWithApprox wanted
 311  = do { traceTcS "simplifyApproxLoop" (ppr wanted)
 312
 313       ; results <- solveWanteds emptyInert wanted
 314
 315       ; let (residual_implics, floats) = approximateImplications (wc_impl results)
 316
 317         -- If no new work was produced then we are done with simplifyApproxLoop
 318       ; if insolubleWC results || isEmptyBag floats
 319         then return results
 320
 321         else solveWanteds emptyInert
 322                 (WC { wc_flat = floats `unionBags` wc_flat results
 323                     , wc_impl = residual_implics
 324                     , wc_insol = emptyBag }) }
 325
 326 approximateImplications :: Bag Implication -> (Bag Implication, Bag WantedEvVar)
 327 -- Extracts any nested constraints that don't mention the skolems
 328 approximateImplications impls
 329   = do_bag (float_implic emptyVarSet) impls
 330   where
 331     do_bag :: forall a b c. (a -> (Bag b, Bag c)) -> Bag a -> (Bag b, Bag c)
 332     do_bag f = foldrBag (plus . f) (emptyBag, emptyBag)
 333     plus :: forall b c. (Bag b, Bag c) -> (Bag b, Bag c) -> (Bag b, Bag c)
 334     plus (a1,b1) (a2,b2) = (a1 `unionBags` a2, b1 `unionBags` b2)
 335
 336     float_implic :: TyVarSet -> Implication -> (Bag Implication, Bag WantedEvVar)
 337     float_implic skols imp
 338       = (unitBag (imp { ic_wanted = wanted' }), floats)
 339       where
 340         (wanted', floats) = float_wc (skols `unionVarSet` ic_skols imp) (ic_wanted imp)
 341
 342     float_wc skols wc@(WC { wc_flat = flat, wc_impl = implic })
 343       = (wc { wc_flat = flat', wc_impl = implic' }, floats1 `unionBags` floats2)
 344       where
 345         (flat',   floats1) = do_bag (float_flat   skols) flat
 346         (implic', floats2) = do_bag (float_implic skols) implic
 347
 348     float_flat :: TcTyVarSet -> WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
 349     float_flat skols wev
 350       | tyVarsOfEvVarX wev `disjointVarSet` skols = (emptyBag, unitBag wev)
 351       | otherwise                                 = (unitBag wev, emptyBag)
 352 \end{code}
 353
 354 \begin{code}
 355 -- (growX gbls wanted tvs) grows a seed 'tvs' against the
 356 -- X-constraint 'wanted', nuking the 'gbls' at each stage
 357 -- It's conservative in that if the seed could *possibly*
 358 -- grow to include a type variable, then it does
 359
 360 growWanteds :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
 361 growWanteds gbl_tvs wc = fixVarSet (growWC gbl_tvs wc)
 362
 363 growWantedEVs :: TyVarSet -> Bag WantedEvVar -> TyVarSet -> TyVarSet
 364 growWantedEVs gbl_tvs ws tvs
 365   | isEmptyBag ws = tvs
 366   | otherwise     = fixVarSet (growPreds gbl_tvs evVarOfPred ws) tvs
 367
 368 --------  Helper functions, do not do fixpoint ------------------------
 369 growWC :: TyVarSet -> WantedConstraints -> TyVarSet -> TyVarSet
 370 growWC gbl_tvs wc = growImplics gbl_tvs             (wc_impl wc) .
 371                     growPreds   gbl_tvs evVarOfPred (wc_flat wc) .
 372                     growPreds   gbl_tvs evVarOfPred (wc_insol wc)
 373
 374 growImplics :: TyVarSet -> Bag Implication -> TyVarSet -> TyVarSet
 375 growImplics gbl_tvs implics tvs
 376   = foldrBag grow_implic tvs implics
 377   where
 378     grow_implic implic tvs
 379       = grow tvs `minusVarSet` ic_skols implic
 380       where
 381         grow = growWC gbl_tvs (ic_wanted implic) .
 382                growPreds gbl_tvs evVarPred (listToBag (ic_given implic))
 383                -- We must grow from givens too; see test IPRun
 384
 385 growPreds :: TyVarSet -> (a -> PredType) -> Bag a -> TyVarSet -> TyVarSet
 386 growPreds gbl_tvs get_pred items tvs
 387   = foldrBag extend tvs items
 388   where
 389     extend item tvs = tvs `unionVarSet`
 390                       (growPredTyVars (get_pred item) tvs `minusVarSet` gbl_tvs)
 391
 392 --------------------
 393 quantifyMe :: TyVarSet      -- Quantifying over these
 394            -> WantedEvVar
 395            -> Bool          -- True <=> quantify over this wanted
 396 quantifyMe qtvs wev
 397   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
 398   | otherwise     = tyVarsOfPred pred `intersectsVarSet` qtvs
 399   where
 400     pred = evVarOfPred wev
 401 \end{code}
 402
 403 Note [Avoid unecessary constraint simplification]
 404 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 405 When inferring the type of a let-binding, with simplifyInfer,
 406 try to avoid unnecessariliy simplifying class constraints.
 407 Doing so aids sharing, but it also helps with delicate
 408 situations like
 409    instance C t => C [t] where ..
 410    f :: C [t] => ....
 411    f x = let g y = ...(constraint C [t])...
 412          in ...
 413 When inferring a type for 'g', we don't want to apply the
 414 instance decl, because then we can't satisfy (C t).  So we
 415 just notice that g isn't quantified over 't' and partition
 416 the contraints before simplifying.
 417
 418 This only half-works, but then let-generalisation only half-works.
 419
 420
 421 Note [Inheriting implicit parameters]
 422 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 423 Consider this:
 424
 425         f x = (x::Int) + ?y
 426
 427 where f is *not* a top-level binding.
 428 From the RHS of f we'll get the constraint (?y::Int).
 429 There are two types we might infer for f:
 430
 431         f :: Int -> Int
 432
 433 (so we get ?y from the context of f's definition), or
 434
 435         f :: (?y::Int) => Int -> Int
 436
 437 At first you might think the first was better, becuase then
 438 ?y behaves like a free variable of the definition, rather than
 439 having to be passed at each call site.  But of course, the WHOLE
 440 IDEA is that ?y should be passed at each call site (that's what
 441 dynamic binding means) so we'd better infer the second.
 442
 443 BOTTOM LINE: when *inferring types* you *must* quantify
 444 over implicit parameters. See the predicate isFreeWhenInferring.
 445
 446
 447 *********************************************************************************
 448 *                                                                                 *
 449 *                             RULES                                               *
 450 *                                                                                 *
 451 ***********************************************************************************
 452
 453 Note [Simplifying RULE lhs constraints]
 454 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 455 On the LHS of transformation rules we only simplify only equalities,
 456 but not dictionaries.  We want to keep dictionaries unsimplified, to
 457 serve as the available stuff for the RHS of the rule.  We *do* want to
 458 simplify equalities, however, to detect ill-typed rules that cannot be
 459 applied.
 460
 461 Implementation: the TcSFlags carried by the TcSMonad controls the
 462 amount of simplification, so simplifyRuleLhs just sets the flag
 463 appropriately.
 464
 465 Example.  Consider the following left-hand side of a rule
 466         f (x == y) (y > z) = ...
 467 If we typecheck this expression we get constraints
 468         d1 :: Ord a, d2 :: Eq a
 469 We do NOT want to "simplify" to the LHS
 470         forall x::a, y::a, z::a, d1::Ord a.
 471           f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
 472 Instead we want
 473         forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
 474           f ((==) d2 x y) ((>) d1 y z) = ...
 475
 476 Here is another example:
 477         fromIntegral :: (Integral a, Num b) => a -> b
 478         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
 479 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
 480 we *dont* want to get
 481         forall dIntegralInt.
 482            fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 483 because the scsel will mess up RULE matching.  Instead we want
 484         forall dIntegralInt, dNumInt.
 485           fromIntegral Int Int dIntegralInt dNumInt = id Int
 486
 487 Even if we have
 488         g (x == y) (y == z) = ..
 489 where the two dictionaries are *identical*, we do NOT WANT
 490         forall x::a, y::a, z::a, d1::Eq a
 491           f ((==) d1 x y) ((>) d1 y z) = ...
 492 because that will only match if the dict args are (visibly) equal.
 493 Instead we want to quantify over the dictionaries separately.
 494
 495 In short, simplifyRuleLhs must *only* squash equalities, leaving
 496 all dicts unchanged, with absolutely no sharing.
 497
 498 HOWEVER, under a nested implication things are different
 499 Consider
 500   f :: (forall a. Eq a => a->a) -> Bool -> ...
 501   {-# RULES "foo" forall (v::forall b. Eq b => b->b).
 502        f b True = ...
 503     #=}
 504 Here we *must* solve the wanted (Eq a) from the given (Eq a)
 505 resulting from skolemising the agument type of g.  So we
 506 revert to SimplCheck when going under an implication.
 507
 508 \begin{code}
 509 simplifyRule :: RuleName
 510              -> [TcTyVar]               -- Explicit skolems
 511              -> WantedConstraints       -- Constraints from LHS
 512              -> WantedConstraints       -- Constraints from RHS
 513              -> TcM ([EvVar],           -- LHS dicts
 514                      TcEvBinds,         -- Evidence for LHS
 515                      TcEvBinds)         -- Evidence for RHS
 516 -- See Note [Simplifying RULE lhs constraints]
 517 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
 518   = do { loc        <- getCtLoc (RuleSkol name)
 519        ; zonked_lhs <- zonkWC lhs_wanted
 520        ; let untch = NoUntouchables
 521                  -- We allow ourselves to unify environment
 522                  -- variables; hence *no untouchables*
 523
 524        ; (lhs_results, lhs_binds)
 525               <- runTcS SimplRuleLhs untch $
 526                  solveWanteds emptyInert lhs_wanted
 527
 528        ; traceTc "simplifyRule" $
 529          vcat [ text "zonked_lhs"   <+> ppr zonked_lhs
 530               , text "lhs_results" <+> ppr lhs_results
 531               , text "lhs_binds"    <+> ppr lhs_binds
 532               , text "rhs_wanted"   <+> ppr rhs_wanted ]
 533
 534
 535        -- Don't quantify over equalities (judgement call here)
 536        ; let (eqs, dicts) = partitionBag (isEqPred . evVarOfPred)
 537                                          (wc_flat lhs_results)
 538              lhs_dicts    = map evVarOf (bagToList dicts)
 539                                  -- Dicts and implicit parameters
 540
 541            -- Fail if we have not got down to unsolved flats
 542        ; ev_binds_var <- newTcEvBinds
 543        ; emitImplication $ Implic { ic_untch  = untch
 544                                   , ic_env    = emptyNameEnv
 545                                   , ic_skols  = mkVarSet tv_bndrs
 546                                   , ic_given  = lhs_dicts
 547                                   , ic_wanted = lhs_results { wc_flat = eqs }
 548                                   , ic_insol  = insolubleWC lhs_results
 549                                   , ic_binds  = ev_binds_var
 550                                   , ic_loc    = loc }
 551
 552              -- Notice that we simplify the RHS with only the explicitly
 553              -- introduced skolems, allowing the RHS to constrain any
 554              -- unification variables.
 555              -- Then, and only then, we call zonkQuantifiedTypeVariables
 556              -- Example   foo :: Ord a => a -> a
 557              --           foo_spec :: Int -> Int
 558              --           {-# RULE "foo"  foo = foo_spec #-}
 559              --     Here, it's the RHS that fixes the type variable
 560
 561              -- So we don't want to make untouchable the type
 562              -- variables in the envt of the RHS, because they include
 563              -- the template variables of the RULE
 564
 565              -- Hence the rather painful ad-hoc treatement here
 566        ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
 567        ; rhs_binds1 <- simplifyCheck SimplCheck $
 568             WC { wc_flat = emptyBag
 569                , wc_insol = emptyBag
 570                , wc_impl = unitBag $
 571                     Implic { ic_untch   = NoUntouchables
 572                             , ic_env    = emptyNameEnv
 573                             , ic_skols  = mkVarSet tv_bndrs
 574                             , ic_given  = lhs_dicts
 575                             , ic_wanted = rhs_wanted
 576                             , ic_insol  = insolubleWC rhs_wanted
 577                             , ic_binds  = rhs_binds_var
 578                             , ic_loc    = loc } }
 579        ; rhs_binds2 <- readTcRef evb_ref
 580
 581        ; return ( lhs_dicts
 582                 , EvBinds lhs_binds
 583                 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
 584 \end{code}
 585
 586
 587 *********************************************************************************
 588 *                                                                                 *
 589 *                                 Main Simplifier                                 *
 590 *                                                                                 *
 591 ***********************************************************************************
 592
 593 \begin{code}
 594 simplifyCheck :: SimplContext
 595               -> WantedConstraints      -- Wanted
 596               -> TcM (Bag EvBind)
 597 -- Solve a single, top-level implication constraint
 598 -- e.g. typically one created from a top-level type signature
 599 --          f :: forall a. [a] -> [a]
 600 --          f x = rhs
 601 -- We do this even if the function has no polymorphism:
 602 --          g :: Int -> Int
 603
 604 --          g y = rhs
 605 -- (whereas for *nested* bindings we would not create
 606 --  an implication constraint for g at all.)
 607 --
 608 -- Fails if can't solve something in the input wanteds
 609 simplifyCheck ctxt wanteds
 610   = do { wanteds <- zonkWC wanteds
 611
 612        ; traceTc "simplifyCheck {" (vcat
 613              [ ptext (sLit "wanted =") <+> ppr wanteds ])
 614
 615        ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
 616                                  solveWanteds emptyInert wanteds
 617
 618        ; traceTc "simplifyCheck }" $
 619          ptext (sLit "unsolved =") <+> ppr unsolved
 620
 621        ; reportUnsolved unsolved
 622
 623        ; return ev_binds }
 624
 625 ----------------
 626 solveWanteds :: InertSet                            -- Given
 627              -> WantedConstraints
 628              -> TcS WantedConstraints
 629 solveWanteds inert wanted
 630   = do { (unsolved_flats, unsolved_implics, insols)
 631              <- solve_wanteds inert wanted
 632        ; return (WC { wc_flat = keepWanted unsolved_flats   -- Discard Derived
 633                     , wc_impl = unsolved_implics
 634                     , wc_insol = insols }) }
 635
 636 solve_wanteds :: InertSet                            -- Given
 637               -> WantedConstraints
 638               -> TcS (Bag FlavoredEvVar, Bag Implication, Bag FlavoredEvVar)
 639 -- solve_wanteds iterates when it is able to float equalities
 640 -- out of one or more of the implications
 641 solve_wanteds inert wanted@(WC { wc_flat = flats, wc_impl = implics, wc_insol = insols })
 642   = do { traceTcS "solveWanteds {" (ppr wanted)
 643
 644                  -- Try the flat bit
 645        ; let all_flats = flats `unionBags` keepWanted insols
 646        ; inert1 <- solveInteractWanted inert (bagToList all_flats)
 647
 648        ; (unsolved_flats, unsolved_implics) <- simpl_loop 1 inert1 implics
 649
 650        ; bb <- getTcEvBindsBag
 651        ; tb <- getTcSTyBindsMap
 652        ; traceTcS "solveWanteds }" $
 653                  vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
 654                       , text "unsolved_implics =" <+> ppr unsolved_implics
 655                       , text "current evbinds  =" <+> vcat (map ppr (varEnvElts bb))
 656                       , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
 657                       ]
 658
 659        ; (subst, remaining_flats) <- solveCTyFunEqs unsolved_flats
 660                 -- See Note [Solving Family Equations]
 661                 -- NB: remaining_flats has already had subst applied
 662
 663        ; let (insoluble_flats, unsolved_flats) = partitionBag isCFrozenErr remaining_flats
 664
 665        ; return ( mapBag (substFlavoredEvVar subst . deCanonicalise) unsolved_flats
 666                 , mapBag (substImplication subst) unsolved_implics
 667                 , mapBag (substFlavoredEvVar subst . deCanonicalise) insoluble_flats ) }
 668
 669   where
 670     simpl_loop :: Int
 671                -> InertSet
 672                -> Bag Implication
 673                -> TcS (CanonicalCts, Bag Implication) -- CanonicalCts are Wanted or Derived
 674     simpl_loop n inert implics
 675       | n>10
 676       = trace "solveWanteds: loop" $                    -- Always bleat
 677         do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
 678            ; let (_, unsolved_cans) = extractUnsolved inert
 679            ; return (unsolved_cans, implics) }
 680
 681       | otherwise
 682       = do { traceTcS "solveWanteds: simpl_loop start {" $
 683                  vcat [ text "n =" <+> ppr n
 684                       , text "implics =" <+> ppr implics
 685                       , text "inert   =" <+> ppr inert ]
 686
 687            ; let (just_given_inert, unsolved_cans) = extractUnsolved inert
 688                      -- unsolved_ccans contains either Wanted or Derived!
 689
 690                 -- Go inside each implication
 691            ; (implic_eqs, unsolved_implics)
 692                   <- solveNestedImplications just_given_inert implics
 693
 694                 -- Apply defaulting rules if and only if there
 695                 -- no floated equalities.  If there are, they may
 696                 -- solve the remaining wanteds, so don't do defaulting.
 697            ; improve_eqs <- if not (isEmptyBag implic_eqs)
 698                             then return implic_eqs
 699                             else applyDefaultingRules just_given_inert unsolved_cans
 700
 701            ; traceTcS "solveWanteds: simpl_loop end }" $
 702                  vcat [ text "improve_eqs      =" <+> ppr improve_eqs
 703                       , text "unsolved_flats   =" <+> ppr unsolved_cans
 704                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
 705
 706            ; (improve_eqs_already_in_inert, inert_with_improvement)
 707                <- solveInteract inert improve_eqs
 708
 709            ; if improve_eqs_already_in_inert then
 710                  return (unsolved_cans, unsolved_implics)
 711              else
 712                  simpl_loop (n+1) inert_with_improvement
 713                                          -- Contain unsolved_cans and the improve_eqs
 714                                   unsolved_implics
 715            }
 716
 717 solveNestedImplications :: InertSet -> Bag Implication
 718                         -> TcS (Bag FlavoredEvVar, Bag Implication)
 719 solveNestedImplications inerts implics
 720   | isEmptyBag implics
 721   = return (emptyBag, emptyBag)
 722   | otherwise
 723   = do { -- See Note [Preparing inert set for implications]
 724          traceTcS "solveWanteds: preparing inerts for implications {"  empty
 725        ; let inert_for_implics = inerts
 726            -- DV: Used to be:
 727            -- inert_for_implics <- solveInteract inerts (makeGivens unsolved).
 728            -- But now the top-level simplifyInfer effectively converts the
 729            -- quantifiable wanteds to givens, and hence we don't need to add
 730            -- those unsolved as givens here; they will already be in the inert set.
 731
 732        ; traceTcS "}" empty
 733
 734        ; traceTcS "solveWanteds: doing nested implications {" $
 735          vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
 736               , text "implics =" <+> ppr implics ]
 737
 738        ; let tcs_untouchables = filterVarSet isFlexiTcsTv $
 739                                 tyVarsOfInert inert_for_implics
 740              -- See Note [Extra TcsTv untouchables]
 741
 742        ; (implic_eqs, unsolved_implics)
 743            <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics
 744
 745        ; traceTcS "solveWanteds: done nested implications }" $
 746                   vcat [ text "implic_eqs ="       <+> ppr implic_eqs
 747                        , text "unsolved_implics =" <+> ppr unsolved_implics ]
 748
 749        ; return (implic_eqs, unsolved_implics) }
 750
 751 solveImplication :: TcTyVarSet                -- Untouchable TcS unification variables
 752                  -> InertSet                  -- Given
 753                  -> Implication               -- Wanted
 754                  -> TcS (Bag FlavoredEvVar, -- All wanted or derived unifications: var = type
 755                          Bag Implication)     -- Unsolved rest (always empty or singleton)
 756 -- Returns:
 757 --  1. A bag of floatable wanted constraints, not mentioning any skolems,
 758 --     that are of the form unification var = type
 759 --
 760 --  2. Maybe a unsolved implication, empty if entirely solved!
 761 --
 762 -- Precondition: everything is zonked by now
 763 solveImplication tcs_untouchables inert
 764      imp@(Implic { ic_untch  = untch
 765                  , ic_binds  = ev_binds
 766                  , ic_skols  = skols
 767                  , ic_given  = givens
 768                  , ic_wanted = wanteds
 769                  , ic_loc    = loc })
 770   = nestImplicTcS ev_binds (untch, tcs_untouchables) $
 771     recoverTcS (return (emptyBag, emptyBag)) $
 772        -- Recover from nested failures.  Even the top level is
 773        -- just a bunch of implications, so failing at the first
 774        -- one is bad
 775     do { traceTcS "solveImplication {" (ppr imp)
 776
 777          -- Solve flat givens
 778        ; given_inert <- solveInteractGiven inert loc givens
 779
 780          -- Simplify the wanteds
 781        ; (unsolved_flats, unsolved_implics, insols)
 782              <- solve_wanteds given_inert wanteds
 783
 784        ; let (res_flat_free, res_flat_bound)
 785                  = floatEqualities skols givens unsolved_flats
 786              final_flat = keepWanted res_flat_bound
 787
 788        ; let res_wanted = WC { wc_flat = final_flat
 789                              , wc_impl = unsolved_implics
 790                              , wc_insol = insols }
 791              res_implic = unitImplication $
 792                           imp { ic_wanted = res_wanted
 793                               , ic_insol  = insolubleWC res_wanted }
 794
 795        ; traceTcS "solveImplication end }" $ vcat
 796              [ text "res_flat_free =" <+> ppr res_flat_free
 797              , text "res_implic =" <+> ppr res_implic ]
 798
 799        ; return (res_flat_free, res_implic) }
 800
 801
 802 floatEqualities :: TcTyVarSet -> [EvVar]
 803                 -> Bag FlavoredEvVar -> (Bag FlavoredEvVar, Bag FlavoredEvVar)
 804 -- Post: The returned FlavoredEvVar's are only Wanted or Derived
 805 -- and come from the input wanted ev vars or deriveds
 806 floatEqualities skols can_given wantders
 807   | hasEqualities can_given = (emptyBag, wantders)
 808           -- Note [Float Equalities out of Implications]
 809   | otherwise = partitionBag is_floatable wantders
 810
 811
 812   where is_floatable :: FlavoredEvVar -> Bool
 813         is_floatable (EvVarX cv _fl)
 814           | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
 815         is_floatable _flev = False
 816
 817         tvs_under_fsks :: Type -> TyVarSet
 818         -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
 819         tvs_under_fsks (TyVarTy tv)
 820           | not (isTcTyVar tv)               = unitVarSet tv
 821           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
 822           | otherwise                        = unitVarSet tv
 823         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
 824         tvs_under_fsks (PredTy sty)     = predTvs_under_fsks sty
 825         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
 826         tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
 827         tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
 828                                       -- can mention type variables!
 829           | isTyVar tv                = inner_tvs `delVarSet` tv
 830           | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
 831                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
 832           where
 833             inner_tvs = tvs_under_fsks ty
 834
 835         predTvs_under_fsks :: PredType -> TyVarSet
 836         predTvs_under_fsks (IParam _ ty)    = tvs_under_fsks ty
 837         predTvs_under_fsks (ClassP _ tys)   = unionVarSets (map tvs_under_fsks tys)
 838         predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
 839 \end{code}
 840
 841 Note [Float Equalities out of Implications]
 842 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 843 We want to float equalities out of vanilla existentials, but *not* out
 844 of GADT pattern matches.
 845
 846 Note [Preparing inert set for implications]
 847 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 848 Before solving the nested implications, we convert any unsolved flat wanteds
 849 to givens, and add them to the inert set.  Reasons:
 850
 851   a) In checking mode, suppresses unnecessary errors.  We already have
 852      on unsolved-wanted error; adding it to the givens prevents any
 853      consequential errors from showing uop
 854
 855   b) More importantly, in inference mode, we are going to quantify over this
 856      constraint, and we *don't* want to quantify over any constraints that
 857      are deducible from it.
 858
 859 The unsolved wanteds are *canonical* but they may not be *inert*,
 860 because when made into a given they might interact with other givens.
 861 Hence the call to solveInteract.  Example:
 862
 863  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta])
 864
 865 We were not able to solve (a ~w [beta]) but we can't just assume it as
 866 given because the resulting set is not inert. Hence we have to do a
 867 'solveInteract' step first.
 868
 869 Note [Extra TcsTv untouchables]
 870 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 871 Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv
 872 kind (such as variables from instance that have been applied, or unification flattens). These
 873 variables must be passed to the implications as extra untouchable variables. Otherwise
 874 we have the danger of double unifications. Example (from trac ticket #4494):
 875
 876    (F Int ~ uf)  /\  (forall a. C a => F Int ~ beta)
 877
 878 In this example, beta is touchable inside the implication. The first solveInteract step
 879 leaves 'uf' ununified. Then we move inside the implication where a new constraint
 880        uf  ~  beta
 881 emerges. We may spontaneously solve it to get uf := beta, so the whole implication disappears
 882 but when we pop out again we are left with (F Int ~ uf) which will be unified by our final
 883 solveCTyFunEqs stage and uf will get unified *once more* to  (F Int).
 884
 885 The solution is to record the TcsTvs (i.e. the simplifier-generated unification variables)
 886 that are generated when solving the flats, and make them untouchables for the nested
 887 implication. In the example above uf would become untouchable, so beta would be forced to
 888 be unified as beta := uf.
 889
 890 NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out
 891     of an implication becomes now untouchable next time we go inside that implication to
 892     solve any residual constraints. In effect, by floating an equality out of the implication
 893     we are committing to have it solved in the outside.
 894
 895
 896 \begin{code}
 897
 898 solveCTyFunEqs :: CanonicalCts -> TcS (TvSubst, CanonicalCts)
 899 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
 900 -- See Note [Solving Family Equations]
 901 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
 902 --          where the newly generated equalities (alpha := F xi) have been substituted through.
 903 solveCTyFunEqs cts
 904  = do { untch   <- getUntouchables
 905       ; let (unsolved_can_cts, (ni_subst, cv_binds))
 906                 = getSolvableCTyFunEqs untch cts
 907       ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
 908                                           , ppr ni_subst, ppr cv_binds
 909                                           ])
 910       ; mapM_ solve_one cv_binds
 911
 912       ; return (niFixTvSubst ni_subst, unsolved_can_cts) }
 913   where
 914     solve_one (cv,tv,ty) = setWantedTyBind tv ty >> setWantedCoBind cv ty
 915
 916 ------------
 917 type FunEqBinds = (TvSubstEnv, [(CoVar, TcTyVar, TcType)])
 918   -- The TvSubstEnv is not idempotent, but is loop-free
 919   -- See Note [Non-idempotent substitution] in Unify
 920 emptyFunEqBinds :: FunEqBinds
 921 emptyFunEqBinds = (emptyVarEnv, [])
 922
 923 extendFunEqBinds :: FunEqBinds -> CoVar -> TcTyVar -> TcType -> FunEqBinds
 924 extendFunEqBinds (tv_subst, cv_binds) cv tv ty
 925   = (extendVarEnv tv_subst tv ty, (cv, tv, ty):cv_binds)
 926
 927 ------------
 928 getSolvableCTyFunEqs :: TcsUntouchables
 929                      -> CanonicalCts                -- Precondition: all Wanteds or Derived!
 930                      -> (CanonicalCts, FunEqBinds)  -- Postcondition: returns the unsolvables
 931 getSolvableCTyFunEqs untch cts
 932   = Bag.foldlBag dflt_funeq (emptyCCan, emptyFunEqBinds) cts
 933   where
 934     dflt_funeq :: (CanonicalCts, FunEqBinds) -> CanonicalCt
 935                -> (CanonicalCts, FunEqBinds)
 936     dflt_funeq (cts_in, feb@(tv_subst, _))
 937                (CFunEqCan { cc_id = cv
 938                           , cc_flavor = fl
 939                           , cc_fun = tc
 940                           , cc_tyargs = xis
 941                           , cc_rhs = xi })
 942       | Just tv <- tcGetTyVar_maybe xi      -- RHS is a type variable
 943
 944       , isTouchableMetaTyVar_InRange untch tv
 945            -- And it's a *touchable* unification variable
 946
 947       , typeKind xi `isSubKind` tyVarKind tv
 948          -- Must do a small kind check since TcCanonical invariants
 949          -- on family equations only impose compatibility, not subkinding
 950
 951       , not (tv `elemVarEnv` tv_subst)
 952            -- Check not in extra_binds
 953            -- See Note [Solving Family Equations], Point 1
 954
 955       , not (tv `elemVarSet` niSubstTvSet tv_subst (tyVarsOfTypes xis))
 956            -- Occurs check: see Note [Solving Family Equations], Point 2
 957       = ASSERT ( not (isGiven fl) )
 958         (cts_in, extendFunEqBinds feb cv tv (mkTyConApp tc xis))
 959
 960     dflt_funeq (cts_in, fun_eq_binds) ct
 961       = (cts_in `extendCCans` ct, fun_eq_binds)
 962 \end{code}
 963
 964 Note [Solving Family Equations]
 965 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 966 After we are done with simplification we may be left with constraints of the form:
 967      [Wanted] F xis ~ beta
 968 If 'beta' is a touchable unification variable not already bound in the TyBinds
 969 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
 970
 971 When is it ok to do so?
 972     1) 'beta' must not already be defaulted to something. Example:
 973
 974            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
 975            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We
 976                                        have to report this as unsolved.
 977
 978     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
 979        set [beta := F xis] only if beta is not among the free variables of xis.
 980
 981     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
 982        of type family equations. See Inert Set invariants in TcInteract.
 983
 984
 985 *********************************************************************************
 986 *                                                                               *
 987 *                          Defaulting and disamgiguation                        *
 988 *                                                                               *
 989 *********************************************************************************
 990
 991 Basic plan behind applyDefaulting rules:
 992
 993  Step 1:
 994     Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
 995     For each defaultable group, do:
 996       For each possible substitution for [alpha |-> tau] where `alpha' is the
 997       group's variable, do:
 998         1) Make up new TcEvBinds
 999         2) Extend TcS with (groupVariable
1000         3) given_inert <- solveOne inert (given : a ~ tau)
1001         4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
1002         5) if unsolved == empty then
1003                  sneakyUnify a |-> tau
1004                  write the evidence bins
1005                  return (final_inert ++ group_constraints,[])
1006                       -- will contain the info (alpha |-> tau)!!
1007                  goto next defaultable group
1008            if unsolved <> empty then
1009                  throw away evidence binds
1010                  try next substitution
1011      If you've run out of substitutions for this group, too bad, you failed
1012                  return (inert,group)
1013                  goto next defaultable group
1014
1015  Step 2:
1016    Collect all the (canonical-cts, wanteds) gathered this way.
1017    - Do a solveGiven over the canonical-cts to make sure they are inert
1018 ------------------------------------------------------------------------------------------
1019
1020
1021 \begin{code}
1022 applyDefaultingRules :: InertSet
1023                      -> CanonicalCts             -- All wanteds
1024                      -> TcS (Bag FlavoredEvVar)  -- All wanteds again!
1025 -- Return some *extra* givens, which express the
1026 -- type-class-default choice
1027
1028 applyDefaultingRules inert wanteds
1029   | isEmptyBag wanteds
1030   = return emptyBag
1031   | otherwise
1032   = do { untch <- getUntouchables
1033        ; tv_cts <- mapM (defaultTyVar untch) $
1034                    varSetElems (tyVarsOfCDicts wanteds)
1035
1036        ; info@(_, default_tys, _) <- getDefaultInfo
1037        ; let groups = findDefaultableGroups info untch wanteds
1038        ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1039
1040        ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1041                                  , text "Type defaults =" <+> ppr deflt_cts])
1042
1043        ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1044
1045 ------------------
1046 defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag FlavoredEvVar)
1047 -- defaultTyVar is used on any un-instantiated meta type variables to
1048 -- default the kind of ? and ?? etc to *.  This is important to ensure
1049 -- that instance declarations match.  For example consider
1050 --      instance Show (a->b)
1051 --      foo x = show (\_ -> True)
1052 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1053 -- and that won't match the typeKind (*) in the instance decl.
1054 -- See test tc217.
1055 --
1056 -- We look only at touchable type variables. No further constraints
1057 -- are going to affect these type variables, so it's time to do it by
1058 -- hand.  However we aren't ready to default them fully to () or
1059 -- whatever, because the type-class defaulting rules have yet to run.
1060
1061 defaultTyVar untch the_tv
1062   | isTouchableMetaTyVar_InRange untch the_tv
1063   , not (k `eqKind` default_k)
1064   = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1065        ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1066        ; return (unitBag (mkEvVarX ev (Wanted loc))) }
1067   | otherwise
1068   = return emptyBag      -- The common case
1069   where
1070     k = tyVarKind the_tv
1071     default_k = defaultKind k
1072
1073
1074 ----------------
1075 findDefaultableGroups
1076     :: ( SimplContext
1077        , [Type]
1078        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1079     -> TcsUntouchables  -- Untouchable
1080     -> CanonicalCts     -- Unsolved
1081     -> [[(CanonicalCt,TcTyVar)]]
1082 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1083                       untch wanteds
1084   | not (performDefaulting ctxt) = []
1085   | null default_tys             = []
1086   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1087   where
1088     unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
1089     non_unaries :: [CanonicalCt]             -- and *other* constraints
1090
1091     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1092         -- Finds unary type-class constraints
1093     find_unary cc@(CDictCan { cc_tyargs = [ty] })
1094         | Just tv <- tcGetTyVar_maybe ty
1095         = Left (cc, tv)
1096     find_unary cc = Right cc  -- Non unary or non dictionary
1097
1098     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries
1099     bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1100
1101     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1102
1103     is_defaultable_group ds@((_,tv):_)
1104         = isTyConableTyVar tv   -- Note [Avoiding spurious errors]
1105         && not (tv `elemVarSet` bad_tvs)
1106         && isTouchableMetaTyVar_InRange untch tv
1107         && defaultable_classes [cc_class cc | (cc,_) <- ds]
1108     is_defaultable_group [] = panic "defaultable_group"
1109
1110     defaultable_classes clss
1111         | extended_defaults = any isInteractiveClass clss
1112         | otherwise         = all is_std_class clss && (any is_num_class clss)
1113
1114     -- In interactive mode, or with -XExtendedDefaultRules,
1115     -- we default Show a to Show () to avoid graututious errors on "show []"
1116     isInteractiveClass cls
1117         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1118
1119     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1120     -- is_num_class adds IsString to the standard numeric classes,
1121     -- when -foverloaded-strings is enabled
1122
1123     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1124     -- Similarly is_std_class
1125
1126 ------------------------------
1127 disambigGroup :: [Type]                    -- The default types
1128               -> InertSet                  -- Given inert
1129               -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
1130                                            --  sharing same type variable
1131               -> TcS (Bag FlavoredEvVar)
1132
1133 disambigGroup [] _inert _grp
1134   = return emptyBag
1135 disambigGroup (default_ty:default_tys) inert group
1136   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1137        ; ev <- TcSMonad.newCoVar (mkTyVarTy the_tv) default_ty
1138        ; let der_flav = mk_derived_flavor (cc_flavor the_ct)
1139              derived_eq = mkEvVarX ev der_flav
1140
1141        ; success <- tryTcS $
1142                     do { (_,final_inert) <- solveInteract inert $ listToBag $
1143                                             derived_eq : wanted_ev_vars
1144                        ; let (_, unsolved) = extractUnsolved final_inert
1145                        ; let wanted_unsolved = filterBag isWantedCt unsolved
1146                                             -- Don't care about Derived's
1147                        ; return (isEmptyBag wanted_unsolved) }
1148        ; case success of
1149            True  ->  -- Success: record the type variable binding, and return
1150                     do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1151                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1152                        ; return (unitBag derived_eq) }
1153            False ->    -- Failure: try with the next type
1154                     do { traceTcS "disambigGroup failed, will try other default types"
1155                                   (ppr default_ty)
1156                        ; disambigGroup default_tys inert group } }
1157   where
1158     ((the_ct,the_tv):_) = group
1159     wanteds             = map fst group
1160     wanted_ev_vars :: [FlavoredEvVar]
1161     wanted_ev_vars      = map deCanonicalise wanteds
1162
1163     mk_derived_flavor :: CtFlavor -> CtFlavor
1164     mk_derived_flavor (Wanted loc) = Derived loc
1165     mk_derived_flavor _ = panic "Asked  to disambiguate given or derived!"
1166 \end{code}
1167
1168 Note [Avoiding spurious errors]
1169 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1170 When doing the unification for defaulting, we check for skolem
1171 type variables, and simply don't default them.  For example:
1172    f = (*)      -- Monomorphic
1173    g :: Num a => a -> a
1174    g x = f x x
1175 Here, we get a complaint when checking the type signature for g,
1176 that g isn't polymorphic enough; but then we get another one when
1177 dealing with the (Num a) context arising from f's definition;
1178 we try to unify a with Int (to default it), but find that it's
1179 already been unified with the rigid variable from g's type sig
1180
1181
1182
1183 *********************************************************************************
1184 *                                                                               *
1185 *                   Utility functions
1186 *                                                                               *
1187 *********************************************************************************
1188
1189 \begin{code}
1190 newFlatWanteds :: CtOrigin -> ThetaType -> TcM (Bag WantedEvVar)
1191 newFlatWanteds orig theta
1192   = do { loc <- getCtLoc orig
1193        ; evs <- newWantedEvVars theta
1194        ; return (listToBag [EvVarX w loc | w <- evs]) }
1195 \end{code}