compiler/typecheck/TcSimplify.lhs

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