compiler/typecheck/TcSimplify.lhs

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