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                    -- See Note [Preparing inert set for implications]
 693            ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
 694            ; traceTcS "solveWanteds: doing nested implications {" $
 695                  vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
 696                       , text "implics =" <+> ppr implics ]
 697            ; (implic_eqs, unsolved_implics)
 698                 <- flatMapBagPairM (solveImplication inert_for_implics) implics
 699
 700            ; traceTcS "solveWanteds: done nested implications }" $
 701                  vcat [ text "implic_eqs =" <+> ppr implic_eqs
 702                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
 703
 704                 -- Apply defaulting rules if and only if there
 705                 -- no floated equalities.  If there are, they may
 706                 -- solve the remaining wanteds, so don't do defaulting.
 707            ; final_eqs <- if not (isEmptyBag implic_eqs)
 708                           then return implic_eqs
 709                           else applyDefaultingRules inert2 unsolved_flats
 710
 711                 -- default_eqs are *givens*, so simpl_loop may
 712                 -- recurse with givens in the argument
 713
 714            ; traceTcS "solveWanteds: simpl_loop end }" $
 715                  vcat [ text "final_eqs =" <+> ppr final_eqs
 716                       , text "unsolved_flats =" <+> ppr unsolved_flats
 717                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
 718
 719            ; if isEmptyBag final_eqs then
 720                  return (unsolved_flats, unsolved_implics)
 721              else
 722                  do { can_final_eqs <- canWanteds (Bag.bagToList final_eqs)
 723                        -- final eqs is *just* a bunch of WantedEvVars
 724                     ; simpl_loop (n+1) inert2
 725                           (can_final_eqs `andCCan` unsolved_flats) unsolved_implics
 726                        -- Important: reiterate with inert2, not plainly inert
 727                        -- because inert2 may contain more givens, as the result of solving
 728                        -- some wanteds in the incoming can_ws
 729                     }       }
 730
 731 solveImplication :: InertSet                 -- Given
 732                     -> Implication           -- Wanted
 733                     -> TcS (Bag WantedEvVar, -- Unsolved unification var = type
 734                             Bag Implication) -- Unsolved rest (always empty or singleton)
 735 -- Returns:
 736 --  1. A bag of floatable wanted constraints, not mentioning any skolems,
 737 --     that are of the form unification var = type
 738 --
 739 --  2. Maybe a unsolved implication, empty if entirely solved!
 740 --
 741 -- Precondition: everything is zonked by now
 742 solveImplication inert
 743      imp@(Implic { ic_untch  = untch
 744                  , ic_binds  = ev_binds
 745                  , ic_skols  = skols
 746                  , ic_given  = givens
 747                  , ic_wanted = wanteds
 748                  , ic_loc    = loc })
 749   = nestImplicTcS ev_binds untch $
 750     recoverTcS (return (emptyBag, emptyBag)) $
 751        -- Recover from nested failures.  Even the top level is
 752        -- just a bunch of implications, so failing at the first
 753        -- one is bad
 754     do { traceTcS "solveImplication {" (ppr imp)
 755
 756          -- Solve flat givens
 757        ; can_givens  <- canGivens loc givens
 758        ; given_inert <- solveInteract inert can_givens
 759
 760          -- Simplify the wanteds
 761        ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
 762
 763        ; let (res_flat_free, res_flat_bound)
 764                       = floatEqualities skols givens unsolved_flats
 765              unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
 766                               Bag.mapBag WcImplic unsolved_implics
 767
 768        ; traceTcS "solveImplication end }" $ vcat
 769              [ text "res_flat_free =" <+> ppr res_flat_free
 770              , text "res_flat_bound =" <+> ppr res_flat_bound
 771              , text "unsolved_implics =" <+> ppr unsolved_implics ]
 772
 773        ; let res_bag | isEmptyBag unsolved = emptyBag
 774                      | otherwise           = unitBag (imp { ic_wanted  = unsolved })
 775
 776        ; return (res_flat_free, res_bag) }
 777
 778 floatEqualities :: TcTyVarSet -> [EvVar]
 779                 -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
 780                    -- The CanonicalCts will be floated out to be used later, whereas
 781                    -- the remaining WantedEvVars will remain inside the implication.
 782 floatEqualities skols can_given wanteds
 783   | hasEqualities can_given = (emptyBag, wanteds)
 784           -- Note [Float Equalities out of Implications]
 785   | otherwise = partitionBag is_floatable wanteds
 786   where is_floatable :: WantedEvVar -> Bool
 787         is_floatable (WantedEvVar cv _)
 788           | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
 789         is_floatable _wv = False
 790
 791         tvs_under_fsks :: Type -> TyVarSet
 792         -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
 793         tvs_under_fsks (TyVarTy tv)
 794           | not (isTcTyVar tv)               = unitVarSet tv
 795           | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
 796           | otherwise                        = unitVarSet tv
 797         tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
 798         tvs_under_fsks (PredTy sty)     = predTvs_under_fsks sty
 799         tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
 800         tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
 801         tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder
 802                                       -- can mention type variables!
 803           | isTyVar tv                = inner_tvs `delVarSet` tv
 804           | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
 805                                         inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
 806           where
 807             inner_tvs = tvs_under_fsks ty
 808
 809         predTvs_under_fsks :: PredType -> TyVarSet
 810         predTvs_under_fsks (IParam _ ty)    = tvs_under_fsks ty
 811         predTvs_under_fsks (ClassP _ tys)   = unionVarSets (map tvs_under_fsks tys)
 812         predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2
 813
 814
 815
 816
 817 \end{code}
 818
 819 Note [Float Equalities out of Implications]
 820 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 821 We want to float equalities out of vanilla existentials, but *not* out
 822 of GADT pattern matches.
 823
 824 Note [Preparing inert set for implications]
 825 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 826 Before solving the nested implications, we convert any unsolved flat wanteds
 827 to givens, and add them to the inert set.  Reasons:
 828   a) In checking mode, suppresses unnecessary errors.  We already have
 829      on unsolved-wanted error; adding it to the givens prevents any
 830      consequential errors from showing uop
 831   b) More importantly, in inference mode, we are going to quantify over this
 832      constraint, and we *don't* want to quantify over any constraints that
 833      are deducible from it.
 834
 835 The unsolved wanteds are *canonical* but they may not be *inert*,
 836 because when made into a given they might interact with other givens.
 837 Hence the call to solveInteract.  Example:
 838
 839  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta])
 840
 841 We were not able to solve (a ~w [beta]) but we can't just assume it as
 842 given because the resulting set is not inert. Hence we have to do a
 843 'solveInteract' step first
 844
 845 \begin{code}
 846
 847 solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
 848 -- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
 849 -- See Note [Solving Family Equations]
 850 -- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
 851 --          where the newly generated equalities (alpha := F xi) have been substituted through.
 852 solveCTyFunEqs cts implics
 853  = do { untch   <- getUntouchables
 854       ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
 855       ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
 856                                           , ppr funeq_bnds
 857                                           ])
 858       ; mapM_ solve_one funeq_bnds
 859
 860              -- Apply the substitution through to eliminate the flatten
 861              -- unification variables we substituted both in the unsolved flats and implics
 862       ; let final_unsolved
 863               = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
 864             final_implics
 865               = Bag.mapBag (subst_impl funeq_bnds) implics
 866
 867       ; return (final_unsolved, final_implics) }
 868
 869   where solve_one (tv,(ty,cv,fl))
 870           | not (typeKind ty `isSubKind` tyVarKind tv)
 871           = addErrorTcS KindError fl (mkTyVarTy tv) ty
 872              -- Must do a small kind check since TcCanonical invariants
 873              -- on family equations only impose compatibility, not subkinding
 874           | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty
 875
 876         subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
 877         subst_wanted funeq_bnds (WcEvVar wv)    = WcEvVar  (subst_wevar funeq_bnds wv)
 878         subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)
 879
 880         subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar
 881         subst_wevar funeq_bnds (WantedEvVar v loc)
 882           = let orig_ty  = varType v
 883                 new_ty   = substFunEqBnds funeq_bnds orig_ty
 884             in WantedEvVar (setVarType v new_ty) loc
 885
 886         subst_impl :: FunEqBinds -> Implication -> Implication
 887         subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
 888           = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }
 889
 890
 891 type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
 892 -- Invariant: if it contains:
 893 --       [... a -> (ta,...) ... b -> (tb,...) ... ]
 894 -- then 'ta' cannot mention 'b'
 895
 896 getSolvableCTyFunEqs :: Untouchables
 897                      -> CanonicalCts                -- Precondition: all wanteds
 898                      -> (CanonicalCts, FunEqBinds)  -- Postcondition: returns the unsolvables
 899 getSolvableCTyFunEqs untch cts
 900   = Bag.foldlBag dflt_funeq (emptyCCan, []) cts
 901   where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
 902                                                        , cc_flavor = fl
 903                                                        , cc_fun = tc
 904                                                        , cc_tyargs = xis
 905                                                        , cc_rhs = xi })
 906           | Just tv <- tcGetTyVar_maybe xi
 907           , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable
 908           , Nothing <- lookup tv extra_binds      -- or in extra_binds
 909                -- See Note [Solving Family Equations], Point 1
 910           = ASSERT ( isWanted fl )
 911             let ty_orig   = mkTyConApp tc xis
 912                 ty_bind   = substFunEqBnds extra_binds ty_orig
 913             in if tv `elemVarSet` tyVarsOfType ty_bind
 914                then (cts_in `extendCCans` ct, extra_binds)
 915                       -- See Note [Solving Family Equations], Point 2
 916                else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds)
 917                       -- Postcondition met because extra_binds is already applied to ty_bind
 918
 919         dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)
 920
 921 substFunEqBnds :: FunEqBinds -> TcType -> TcType
 922 substFunEqBnds bnds ty
 923   = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
 924     -- foldr works because of the FunEqBinds invariant
 925
 926
 927 \end{code}
 928
 929 Note [Solving Family Equations]
 930 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 931 After we are done with simplification we may be left with constraints of the form:
 932      [Wanted] F xis ~ beta
 933 If 'beta' is a touchable unification variable not already bound in the TyBinds
 934 then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.
 935
 936 When is it ok to do so?
 937     1) 'beta' must not already be defaulted to something. Example:
 938
 939            [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
 940            [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We
 941                                        have to report this as unsolved.
 942
 943     2) However, we must still do an occurs check when defaulting (F xis ~ beta), to
 944        set [beta := F xis] only if beta is not among the free variables of xis.
 945
 946     3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS
 947        of type family equations. See Inert Set invariants in TcInteract.
 948
 949
 950 *********************************************************************************
 951 *                                                                               *
 952 *                          Defaulting and disamgiguation                        *
 953 *                                                                               *
 954 *********************************************************************************
 955
 956 Basic plan behind applyDefaulting rules:
 957
 958  Step 1:
 959     Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
 960     For each defaultable group, do:
 961       For each possible substitution for [alpha |-> tau] where `alpha' is the
 962       group's variable, do:
 963         1) Make up new TcEvBinds
 964         2) Extend TcS with (groupVariable
 965         3) given_inert <- solveOne inert (given : a ~ tau)
 966         4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
 967         5) if unsolved == empty then
 968                  sneakyUnify a |-> tau
 969                  write the evidence bins
 970                  return (final_inert ++ group_constraints,[])
 971                       -- will contain the info (alpha |-> tau)!!
 972                  goto next defaultable group
 973            if unsolved <> empty then
 974                  throw away evidence binds
 975                  try next substitution
 976      If you've run out of substitutions for this group, too bad, you failed
 977                  return (inert,group)
 978                  goto next defaultable group
 979
 980  Step 2:
 981    Collect all the (canonical-cts, wanteds) gathered this way.
 982    - Do a solveGiven over the canonical-cts to make sure they are inert
 983 ------------------------------------------------------------------------------------------
 984
 985
 986 \begin{code}
 987 applyDefaultingRules :: InertSet
 988                      -> CanonicalCts           -- All wanteds
 989                      -> TcS (Bag WantedEvVar)  -- All wanteds again!
 990 -- Return some *extra* givens, which express the
 991 -- type-class-default choice
 992
 993 applyDefaultingRules inert wanteds
 994   | isEmptyBag wanteds
 995   = return emptyBag
 996   | otherwise
 997   = do { untch <- getUntouchables
 998        ; tv_cts <- mapM (defaultTyVar untch) $
 999                    varSetElems (tyVarsOfCDicts wanteds)
1000
1001        ; info@(_, default_tys, _) <- getDefaultInfo
1002        ; let groups = findDefaultableGroups info untch wanteds
1003        ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1004
1005        ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
1006                                  , text "Type defaults =" <+> ppr deflt_cts])
1007
1008        ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1009
1010 ------------------
1011 defaultTyVar :: Untouchables -> TcTyVar -> TcS (Bag WantedEvVar)
1012 -- defaultTyVar is used on any un-instantiated meta type variables to
1013 -- default the kind of ? and ?? etc to *.  This is important to ensure
1014 -- that instance declarations match.  For example consider
1015 --      instance Show (a->b)
1016 --      foo x = show (\_ -> True)
1017 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
1018 -- and that won't match the typeKind (*) in the instance decl.
1019 -- See test tc217.
1020 --
1021 -- We look only at touchable type variables. No further constraints
1022 -- are going to affect these type variables, so it's time to do it by
1023 -- hand.  However we aren't ready to default them fully to () or
1024 -- whatever, because the type-class defaulting rules have yet to run.
1025
1026 defaultTyVar untch the_tv
1027   | isTouchableMetaTyVar_InRange untch the_tv
1028   , not (k `eqKind` default_k)
1029   = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1030        ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1031        ; return (unitBag (WantedEvVar ev loc)) }
1032   | otherwise
1033   = return emptyBag      -- The common case
1034   where
1035     k = tyVarKind the_tv
1036     default_k = defaultKind k
1037
1038
1039 ----------------
1040 findDefaultableGroups
1041     :: ( SimplContext
1042        , [Type]
1043        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1044     -> Untouchables     -- Untouchable
1045     -> CanonicalCts     -- Unsolved
1046     -> [[(CanonicalCt,TcTyVar)]]
1047 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
1048                       untch wanteds
1049   | not (performDefaulting ctxt) = []
1050   | null default_tys             = []
1051   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
1052   where
1053     unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
1054     non_unaries :: [CanonicalCt]             -- and *other* constraints
1055
1056     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
1057         -- Finds unary type-class constraints
1058     find_unary cc@(CDictCan { cc_tyargs = [ty] })
1059         | Just tv <- tcGetTyVar_maybe ty
1060         = Left (cc, tv)
1061     find_unary cc = Right cc  -- Non unary or non dictionary
1062
1063     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries
1064     bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
1065
1066     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
1067
1068     is_defaultable_group ds@((_,tv):_)
1069         = isTyConableTyVar tv   -- Note [Avoiding spurious errors]
1070         && not (tv `elemVarSet` bad_tvs)
1071         && isTouchableMetaTyVar_InRange untch tv
1072         && defaultable_classes [cc_class cc | (cc,_) <- ds]
1073     is_defaultable_group [] = panic "defaultable_group"
1074
1075     defaultable_classes clss
1076         | extended_defaults = any isInteractiveClass clss
1077         | otherwise         = all is_std_class clss && (any is_num_class clss)
1078
1079     -- In interactive mode, or with -XExtendedDefaultRules,
1080     -- we default Show a to Show () to avoid graututious errors on "show []"
1081     isInteractiveClass cls
1082         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
1083
1084     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1085     -- is_num_class adds IsString to the standard numeric classes,
1086     -- when -foverloaded-strings is enabled
1087
1088     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
1089     -- Similarly is_std_class
1090
1091 ------------------------------
1092 disambigGroup :: [Type]                    -- The default types
1093               -> InertSet                  -- Given inert
1094               -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
1095                                            --  sharing same type variable
1096               -> TcS (Bag WantedEvVar)
1097
1098 disambigGroup [] _inert _grp
1099   = return emptyBag
1100 disambigGroup (default_ty:default_tys) inert group
1101   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1102        ; let ct_loc = get_ct_loc (cc_flavor the_ct)
1103        ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
1104        ; let wanted_eq = CTyEqCan { cc_id = ev
1105                                   , cc_flavor = Wanted ct_loc
1106                                   , cc_tyvar  = the_tv
1107                                   , cc_rhs    = default_ty }
1108        ; success <- tryTcS $
1109                     do { final_inert <- solveInteract inert(listToBag $ wanted_eq:wanteds)
1110                        ; let (_, unsolved) = extractUnsolved final_inert
1111                        ; errs <- getTcSErrorsBag
1112                        ; return (isEmptyBag unsolved && isEmptyBag errs) }
1113
1114        ; case success of
1115            True  ->  -- Success: record the type variable binding, and return
1116                     do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
1117                        ; traceTcS "disambigGroup succeeded" (ppr default_ty)
1118                        ; return (unitBag $ WantedEvVar ev ct_loc) }
1119            False ->    -- Failure: try with the next type
1120                     do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty)
1121                        ; disambigGroup default_tys inert group } }
1122   where
1123     ((the_ct,the_tv):_) = group
1124     wanteds = map fst group
1125     wanted_ev_vars = map deCanonicaliseWanted wanteds
1126
1127     get_ct_loc (Wanted l) = l
1128     get_ct_loc _ = panic "Asked  to disambiguate given or derived!"
1129
1130
1131 \end{code}
1132
1133 Note [Avoiding spurious errors]
1134 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1135 When doing the unification for defaulting, we check for skolem
1136 type variables, and simply don't default them.  For example:
1137    f = (*)      -- Monomorphic
1138    g :: Num a => a -> a
1139    g x = f x x
1140 Here, we get a complaint when checking the type signature for g,
1141 that g isn't polymorphic enough; but then we get another one when
1142 dealing with the (Num a) context arising from f's definition;
1143 we try to unify a with Int (to default it), but find that it's
1144 already been unified with the rigid variable from g's type sig