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 Name
  22 import NameEnv  ( emptyNameEnv )
  23 import Bag
  24 import ListSetOps
  25 import Util
  26 import PrelInfo
  27 import PrelNames
  28 import Class            ( classKey )
  29 import BasicTypes       ( RuleName )
  30 import Data.List        ( partition )
  31 import Outputable
  32 import FastString
  33 \end{code}
  34
  35
  36 *********************************************************************************
  37 *                                                                               *
  38 *                           External interface                                  *
  39 *                                                                               *
  40 *********************************************************************************
  41
  42 \begin{code}
  43 simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
  44 -- Simplify top-level constraints
  45 -- Usually these will be implications, when there is
  46 --   nothing to quanitfy we don't wrap in a degenerate implication,
  47 --   so we do that here instead
  48 simplifyTop wanteds
  49   = simplifyCheck SimplCheck wanteds
  50
  51 ------------------
  52 simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
  53 simplifyInteractive wanteds
  54   = simplifyCheck SimplInteractive wanteds
  55
  56 ------------------
  57 simplifyDefault :: ThetaType    -- Wanted; has no type variables in it
  58                 -> TcM ()       -- Succeeds iff the constraint is soluble
  59 simplifyDefault theta
  60   = do { loc <- getCtLoc DefaultOrigin
  61        ; wanted <- newWantedEvVars theta
  62        ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
  63        ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
  64        ; return () }
  65 \end{code}
  66
  67 simplifyBracket is used when simplifying the constraints arising from
  68 a Template Haskell bracket [| ... |].  We want to check that there aren't
  69 any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
  70 Show instance), but we aren't otherwise interested in the results.
  71 Nor do we care about ambiguous dictionaries etc.  We will type check
  72 this bracket again at its usage site.
  73
  74 \begin{code}
  75 simplifyBracket :: WantedConstraints -> TcM ()
  76 simplifyBracket wanteds
  77   = do  { zonked_wanteds <- mapBagM zonkWanted wanteds
  78         ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
  79         ; return () }
  80 \end{code}
  81
  82
  83 *********************************************************************************
  84 *                                                                                 *
  85 *                            Deriving
  86 *                                                                                 *
  87 ***********************************************************************************
  88
  89 \begin{code}
  90 simplifyDeriv :: CtOrigin
  91                 -> [TyVar]
  92                 -> ThetaType            -- Wanted
  93                 -> TcM ThetaType        -- Needed
  94 -- Given  instance (wanted) => C inst_ty
  95 -- Simplify 'wanted' as much as possibles
  96 simplifyDeriv orig tvs theta
  97   = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize
  98                    -- One reason is that the constraint solving machinery
  99                    -- expects *TcTyVars* not TyVars.  Another is that
 100                    -- when looking up instances we don't want overlap
 101                    -- of type variables
 102
 103        ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
 104
 105        ; loc    <- getCtLoc orig
 106        ; wanted <- newWantedEvVars (substTheta skol_subst theta)
 107        ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
 108
 109        ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
 110        ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag
 111
 112        ; let (good, bad) = partition validDerivPred $
 113                            foldrBag ((:) . wantedEvVarPred) [] unsolved
 114                 -- See Note [Exotic derived instance contexts]
 115              subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs
 116
 117        ; reportUnsolvedDeriv bad loc
 118        ; return $ substTheta subst_skol good }
 119 \end{code}
 120
 121 Note [Exotic derived instance contexts]
 122 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 123 In a 'derived' instance declaration, we *infer* the context.  It's a
 124 bit unclear what rules we should apply for this; the Haskell report is
 125 silent.  Obviously, constraints like (Eq a) are fine, but what about
 126         data T f a = MkT (f a) deriving( Eq )
 127 where we'd get an Eq (f a) constraint.  That's probably fine too.
 128
 129 One could go further: consider
 130         data T a b c = MkT (Foo a b c) deriving( Eq )
 131         instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
 132
 133 Notice that this instance (just) satisfies the Paterson termination
 134 conditions.  Then we *could* derive an instance decl like this:
 135
 136         instance (C Int a, Eq b, Eq c) => Eq (T a b c)
 137 even though there is no instance for (C Int a), because there just
 138 *might* be an instance for, say, (C Int Bool) at a site where we
 139 need the equality instance for T's.
 140
 141 However, this seems pretty exotic, and it's quite tricky to allow
 142 this, and yet give sensible error messages in the (much more common)
 143 case where we really want that instance decl for C.
 144
 145 So for now we simply require that the derived instance context
 146 should have only type-variable constraints.
 147
 148 Here is another example:
 149         data Fix f = In (f (Fix f)) deriving( Eq )
 150 Here, if we are prepared to allow -XUndecidableInstances we
 151 could derive the instance
 152         instance Eq (f (Fix f)) => Eq (Fix f)
 153 but this is so delicate that I don't think it should happen inside
 154 'deriving'. If you want this, write it yourself!
 155
 156 NB: if you want to lift this condition, make sure you still meet the
 157 termination conditions!  If not, the deriving mechanism generates
 158 larger and larger constraints.  Example:
 159   data Succ a = S a
 160   data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show
 161
 162 Note the lack of a Show instance for Succ.  First we'll generate
 163   instance (Show (Succ a), Show a) => Show (Seq a)
 164 and then
 165   instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
 166 and so on.  Instead we want to complain of no instance for (Show (Succ a)).
 167
 168 The bottom line
 169 ~~~~~~~~~~~~~~~
 170 Allow constraints which consist only of type variables, with no repeats.
 171
 172 *********************************************************************************
 173 *                                                                                 *
 174 *                            Inference
 175 *                                                                                 *
 176 ***********************************************************************************
 177
 178 \begin{code}
 179 simplifyInfer :: Bool               -- Apply monomorphism restriction
 180               -> TcTyVarSet         -- These type variables are free in the
 181                                     -- types to be generalised
 182               -> WantedConstraints
 183               -> TcM ([TcTyVar],    -- Quantify over these type variables
 184                       [EvVar],      -- ... and these constraints
 185                       TcEvBinds)    -- ... binding these evidence variables
 186 simplifyInfer apply_mr tau_tvs wanted
 187   | isEmptyBag wanted     -- Trivial case is quite common
 188   = do { zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
 189        ; gbl_tvs        <- tcGetGlobalTyVars         -- Already zonked
 190        ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
 191        ; return (qtvs, [], emptyTcEvBinds) }
 192
 193   | otherwise
 194   = do { zonked_wanted <- mapBagM zonkWanted wanted
 195        ; traceTc "simplifyInfer {"  $ vcat
 196              [ ptext (sLit "apply_mr =") <+> ppr apply_mr
 197              , ptext (sLit "wanted =") <+> ppr zonked_wanted
 198              , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
 199              ]
 200
 201        ; (simple_wanted, tc_binds)
 202               <- simplifyAsMuchAsPossible SimplInfer zonked_wanted
 203
 204        ; gbl_tvs <- tcGetGlobalTyVars
 205        ; zonked_tau_tvs <- zonkTcTyVarsAndFV (varSetElems tau_tvs)
 206        ; zonked_simples <- mapBagM zonkWantedEvVar simple_wanted
 207        ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
 208              (bound, free) | apply_mr  = (emptyBag, zonked_simples)
 209                            | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
 210
 211        ; traceTc "end simplifyInfer }" $
 212               vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
 213                    , text "wanted = " <+> ppr zonked_wanted
 214                    , text "qtvs =   " <+> ppr qtvs
 215                    , text "free =   " <+> ppr free
 216                    , text "bound =  " <+> ppr bound ]
 217
 218        -- Turn the quantified meta-type variables into real type variables
 219        ; emitConstraints (mapBag WcEvVar free)
 220        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
 221        ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
 222        ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
 223
 224 ------------------------
 225 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
 226                          -> TcM (Bag WantedEvVar, Bag EvBind)
 227 -- We use this function when inferring the type of a function
 228 -- The wanted constraints are already zonked
 229 simplifyAsMuchAsPossible ctxt wanteds
 230   = do { let untch = emptyVarSet
 231                  -- We allow ourselves to unify environment
 232                  -- variables; hence *no untouchables*
 233
 234        ; ((unsolved_flats, unsolved_implics), ev_binds)
 235            <- runTcS ctxt untch $
 236               simplifyApproxLoop 0 wanteds
 237
 238               -- Report any errors
 239        ; mapBagM_ reportUnsolvedImplication unsolved_implics
 240
 241        ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
 242        ; return (final_wanted_evvars, ev_binds) }
 243
 244   where
 245     simplifyApproxLoop :: Int -> WantedConstraints
 246                        -> TcS (CanonicalCts, Bag Implication)
 247     simplifyApproxLoop n wanteds
 248      | n > 10
 249      = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
 250      | otherwise
 251      = do { traceTcS "simplifyApproxLoop" (vcat
 252                [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
 253           ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
 254
 255           ; let (extra_flats, thiner_unsolved_implics)
 256                     = approximateImplications unsolved_implics
 257                 unsolved
 258                     = mkWantedConstraints unsolved_flats thiner_unsolved_implics
 259
 260           ;-- If no new work was produced then we are done with simplifyApproxLoop
 261             if isEmptyBag extra_flats
 262             then do { traceTcS "simplifyApproxLoopRes" (vcat
 263                               [ ptext (sLit "Wanted = ") <+> ppr wanteds
 264                               , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
 265                     ; return (unsolved_flats, unsolved_implics) }
 266
 267             else -- Produced new flat work wanteds, go round the loop
 268                 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
 269           }
 270
 271 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
 272 -- (wc1, impls2) <- approximateImplications impls
 273 -- splits 'impls' into two parts
 274 --    wc1:    a bag of constraints that do not mention any skolems
 275 --    impls2: a bag of *thiner* implication constraints
 276 approximateImplications impls
 277   = splitBag (do_implic emptyVarSet) impls
 278   where
 279     ------------------
 280     do_wanted :: TcTyVarSet -> WantedConstraint
 281               -> (WantedConstraints, WantedConstraints)
 282     do_wanted skols (WcImplic impl)
 283         = let (fl_w, mb_impl) = do_implic skols impl
 284           in (fl_w, mapBag WcImplic mb_impl)
 285     do_wanted skols wc@(WcEvVar wev)
 286       | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
 287       | otherwise                                      = (emptyBag, unitBag wc)
 288
 289     ------------------
 290     do_implic :: TcTyVarSet -> Implication
 291               -> (WantedConstraints, Bag Implication)
 292     do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
 293      = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
 294                           else unitBag impl{ ic_wanted = rest_wanted } )
 295      where
 296         (floatable_wanted, rest_wanted)
 297             = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
 298
 299     ------------------
 300     splitBag :: (a -> (WantedConstraints, Bag a))
 301              -> Bag a -> (WantedConstraints, Bag a)
 302     splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
 303        where
 304          do_one x (b1,b2)
 305            = (wcs `unionBags` b1, imps `unionBags` b2)
 306            where
 307               (wcs, imps) = f x
 308 \end{code}
 309
 310 \begin{code}
 311 findQuantifiedTyVars :: Bool            -- Apply the MR
 312                      -> Bag WantedEvVar -- Simplified constraints from RHS
 313                      -> TyVarSet        -- Free in tau-type of definition
 314                      -> TyVarSet        -- Free in the envt
 315                      -> TyVarSet        -- Quantify over these
 316
 317 findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs
 318   | isEmptyBag wanteds = init_tvs
 319   | apply_mr           = init_tvs `minusVarSet` constrained_tvs
 320   | otherwise          = fixVarSet mk_next init_tvs
 321   where
 322     init_tvs    = tau_tvs `minusVarSet` gbl_tvs
 323     mk_next tvs = foldrBag grow_one tvs wanteds
 324
 325     grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
 326        where
 327          extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
 328
 329     constrained_tvs = tyVarsOfWantedEvVars wanteds
 330
 331 --------------------
 332 quantifyMe :: TyVarSet      -- Quantifying over these
 333            -> WantedEvVar
 334            -> Bool          -- True <=> quantify over this wanted
 335 quantifyMe qtvs wev
 336   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
 337   | otherwise     = tyVarsOfPred pred `intersectsVarSet` qtvs
 338   where
 339     pred = wantedEvVarPred wev
 340 \end{code}
 341
 342 Note [Inheriting implicit parameters]
 343 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 344 Consider this:
 345
 346         f x = (x::Int) + ?y
 347
 348 where f is *not* a top-level binding.
 349 From the RHS of f we'll get the constraint (?y::Int).
 350 There are two types we might infer for f:
 351
 352         f :: Int -> Int
 353
 354 (so we get ?y from the context of f's definition), or
 355
 356         f :: (?y::Int) => Int -> Int
 357
 358 At first you might think the first was better, becuase then
 359 ?y behaves like a free variable of the definition, rather than
 360 having to be passed at each call site.  But of course, the WHOLE
 361 IDEA is that ?y should be passed at each call site (that's what
 362 dynamic binding means) so we'd better infer the second.
 363
 364 BOTTOM LINE: when *inferring types* you *must* quantify
 365 over implicit parameters. See the predicate isFreeWhenInferring.
 366
 367
 368 *********************************************************************************
 369 *                                                                                 *
 370 *                             Superclasses                                        *
 371 *                                                                                 *
 372 ***********************************************************************************
 373
 374 When constructing evidence for superclasses in an instance declaration,
 375   * we MUST have the "self" dictionary available, but
 376   * we must NOT have its superclasses derived from "self"
 377
 378 Moreover, we must *completely* solve the constraints right now,
 379 not wrap them in an implication constraint to solve later.  Why?
 380 Because when that implication constraint is solved there may
 381 be some unrelated other solved top-level constraints that
 382 recursively depend on the superclass we are building. Consider
 383    class Ord a => C a where
 384    instance C [Int] where ...
 385 Then we get
 386    dCListInt :: C [Int]
 387    dCListInt = MkC $cNum ...
 388
 389    $cNum :: Ord [Int] -- The superclass
 390    $cNum = let self = dCListInt in <solve Ord [Int]>
 391
 392 Now, if there is some *other* top-level constraint solved
 393 looking like
 394         foo :: Ord [Int]
 395         foo = scsel dCInt
 396 we must not solve the (Ord [Int]) wanted from foo!!
 397
 398 \begin{code}
 399 simplifySuperClass :: EvVar     -- The "self" dictionary
 400                    -> WantedConstraints
 401                    -> TcM ()
 402 simplifySuperClass self wanteds
 403   = do { wanteds <- mapBagM zonkWanted wanteds
 404        ; loc <- getCtLoc NoScSkol
 405        ; (unsolved, ev_binds)
 406              <- runTcS SimplCheck emptyVarSet $
 407                 do { can_self <- canGivens loc [self]
 408                    ; let inert = foldlBag extendInertSet emptyInert can_self
 409                      -- No need for solveInteract; we know it's inert
 410
 411                    ; solveWanteds inert wanteds }
 412
 413        ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
 414          reportUnsolved unsolved }
 415 \end{code}
 416
 417
 418 *********************************************************************************
 419 *                                                                                 *
 420 *                             RULES                                               *
 421 *                                                                                 *
 422 ***********************************************************************************
 423
 424 Note [Simplifying RULE lhs constraints]
 425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 426 On the LHS of transformation rules we only simplify only equalitis,
 427 but not dictionaries.  We want to keep dictionaries unsimplified, to
 428 serve as the available stuff for the RHS of the rule.  We *do* want to
 429 simplify equalities, however, to detect ill-typed rules that cannot be
 430 applied.
 431
 432 Implementation: the TcSFlags carried by the TcSMonad controls the
 433 amount of simplification, so simplifyRuleLhs just sets the flag
 434 appropriately.
 435
 436 Example.  Consider the following left-hand side of a rule
 437         f (x == y) (y > z) = ...
 438 If we typecheck this expression we get constraints
 439         d1 :: Ord a, d2 :: Eq a
 440 We do NOT want to "simplify" to the LHS
 441         forall x::a, y::a, z::a, d1::Ord a.
 442           f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
 443 Instead we want
 444         forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
 445           f ((==) d2 x y) ((>) d1 y z) = ...
 446
 447 Here is another example:
 448         fromIntegral :: (Integral a, Num b) => a -> b
 449         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
 450 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
 451 we *dont* want to get
 452         forall dIntegralInt.
 453            fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 454 because the scsel will mess up RULE matching.  Instead we want
 455         forall dIntegralInt, dNumInt.
 456           fromIntegral Int Int dIntegralInt dNumInt = id Int
 457
 458 Even if we have
 459         g (x == y) (y == z) = ..
 460 where the two dictionaries are *identical*, we do NOT WANT
 461         forall x::a, y::a, z::a, d1::Eq a
 462           f ((==) d1 x y) ((>) d1 y z) = ...
 463 because that will only match if the dict args are (visibly) equal.
 464 Instead we want to quantify over the dictionaries separately.
 465
 466 In short, simplifyRuleLhs must *only* squash equalities, leaving
 467 all dicts unchanged, with absolutely no sharing.
 468
 469 HOWEVER, under a nested implication things are different
 470 Consider
 471   f :: (forall a. Eq a => a->a) -> Bool -> ...
 472   {-# RULES "foo" forall (v::forall b. Eq b => b->b).
 473        f b True = ...
 474     #=}
 475 Here we *must* solve the wanted (Eq a) from the given (Eq a)
 476 resulting from skolemising the agument type of g.  So we
 477 revert to SimplCheck when going under an implication.
 478
 479 \begin{code}
 480 simplifyRule :: RuleName
 481              -> [TcTyVar]               -- Explicit skolems
 482              -> WantedConstraints       -- Constraints from LHS
 483              -> WantedConstraints       -- Constraints from RHS
 484              -> TcM ([EvVar],           -- LHS dicts
 485                      TcEvBinds,         -- Evidence for LHS
 486                      TcEvBinds)         -- Evidence for RHS
 487 -- See Note [Simplifying RULE lhs constraints]
 488 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
 489   = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
 490        ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
 491
 492        -- Don't quantify over equalities (judgement call here)
 493        ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
 494              lhs_dicts    = map wantedEvVarToVar (bagToList dicts)
 495                                  -- Dicts and implicit parameters
 496        ; reportUnsolvedWantedEvVars eqs
 497
 498              -- Notice that we simplify the RHS with only the explicitly
 499              -- introduced skolems, allowing the RHS to constrain any
 500              -- unification variables.
 501              -- Then, and only then, we call zonkQuantifiedTypeVariables
 502              -- Example   foo :: Ord a => a -> a
 503              --           foo_spec :: Int -> Int
 504              --           {-# RULE "foo"  foo = foo_spec #-}
 505              --     Here, it's the RHS that fixes the type variable
 506
 507              -- So we don't want to make untouchable the type
 508              -- variables in the envt of the RHS, because they include
 509              -- the template variables of the RULE
 510
 511              -- Hence the rather painful ad-hoc treatement here
 512        ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
 513        ; loc        <- getCtLoc (RuleSkol name)
 514        ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
 515              Implic { ic_env_tvs = emptyVarSet    -- No untouchables
 516                     , ic_env = emptyNameEnv
 517                     , ic_skols = mkVarSet tv_bndrs
 518                     , ic_scoped = panic "emitImplication"
 519                     , ic_given = lhs_dicts
 520                     , ic_wanted = rhs_wanted
 521                     , ic_binds = rhs_binds_var
 522                     , ic_loc = loc }
 523        ; rhs_binds2 <- readTcRef evb_ref
 524
 525        ; return ( lhs_dicts
 526                 , EvBinds lhs_binds
 527                 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
 528 \end{code}
 529
 530
 531 *********************************************************************************
 532 *                                                                                 *
 533 *                                 Main Simplifier                                 *
 534 *                                                                                 *
 535 ***********************************************************************************
 536
 537 \begin{code}
 538 simplifyCheck :: SimplContext
 539               -> WantedConstraints      -- Wanted
 540               -> TcM (Bag EvBind)
 541 -- Solve a single, top-level implication constraint
 542 -- e.g. typically one created from a top-level type signature
 543 --          f :: forall a. [a] -> [a]
 544 --          f x = rhs
 545 -- We do this even if the function has no polymorphism:
 546 --          g :: Int -> Int
 547
 548 --          g y = rhs
 549 -- (whereas for *nested* bindings we would not create
 550 --  an implication constraint for g at all.)
 551 --
 552 -- Fails if can't solve something in the input wanteds
 553 simplifyCheck ctxt wanteds
 554   = do { wanteds <- mapBagM zonkWanted wanteds
 555
 556        ; traceTc "simplifyCheck {" (vcat
 557              [ ptext (sLit "wanted =") <+> ppr wanteds ])
 558
 559        ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $
 560                                  solveWanteds emptyInert wanteds
 561
 562        ; traceTc "simplifyCheck }" $
 563              ptext (sLit "unsolved =") <+> ppr unsolved
 564
 565        ; reportUnsolved unsolved
 566
 567        ; return ev_binds }
 568
 569 ----------------
 570 solveWanteds :: InertSet               -- Given
 571              -> WantedConstraints      -- Wanted
 572              -> TcS (CanonicalCts,     -- Unsolved flats
 573                      Bag Implication)  -- Unsolved implications
 574 -- solveWanteds iterates when it is able to float equalities
 575 -- out of one or more of the implications
 576 solveWanteds inert wanteds
 577   = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
 578        ; can_flats <- canWanteds $ bagToList flat_wanteds
 579        ; traceTcS "solveWanteds {" $
 580                  vcat [ text "wanteds =" <+> ppr wanteds
 581                       , text "inert =" <+> ppr inert ]
 582        ; (unsolved_flats, unsolved_implics)
 583                <- simpl_loop 1 can_flats implic_wanteds
 584        ; traceTcS "solveWanteds }" $
 585                  vcat [ text "wanteds =" <+> ppr wanteds
 586                       , text "unsolved_flats =" <+> ppr unsolved_flats
 587                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
 588        ; return (unsolved_flats, unsolved_implics)  }
 589   where
 590     simpl_loop :: Int
 591                -> CanonicalCts  -- May inlude givens (in the recursive call)
 592                -> Bag Implication
 593                -> TcS (CanonicalCts, Bag Implication)
 594     simpl_loop n can_ws implics
 595       | n>10
 596       = trace "solveWanteds: loop" $    -- Always bleat
 597         do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
 598            ; return (can_ws, implics) }
 599
 600       | otherwise
 601       = do { inert1 <- solveInteract inert can_ws
 602            ; let (inert2, unsolved_flats) = extractUnsolved inert1
 603
 604            ; traceTcS "solveWanteds/done flats"  $
 605                  vcat [ text "inerts =" <+> ppr inert2
 606                       , text "unsolved =" <+> ppr unsolved_flats ]
 607
 608                    -- See Note [Preparing inert set for implications]
 609            ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
 610            ; (implic_eqs, unsolved_implics)
 611                 <- flatMapBagPairM (solveImplication inert_for_implics) implics
 612
 613                 -- Apply defaulting rules if and only if there
 614                 -- no floated equalities.  If there are, they may
 615                 -- solve the remaining wanteds, so don't do defaulting.
 616            ; final_eqs <- if not (isEmptyBag implic_eqs)
 617                           then return implic_eqs
 618                           else applyDefaultingRules inert2 unsolved_flats
 619                 -- default_eqs are *givens*, so simpl_loop may
 620                 -- recurse with givens in the argument
 621
 622            ; if isEmptyBag final_eqs then
 623                  return (unsolved_flats, unsolved_implics)
 624              else
 625                  do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
 626                         [ text "floated_unsolved_eqs =" <+> ppr final_eqs
 627                         , text "unsolved_implics = " <+> ppr unsolved_implics ]
 628                     ; simpl_loop (n+1)
 629                                  (unsolved_flats `unionBags` final_eqs)
 630                                  unsolved_implics
 631            }        }
 632
 633 solveImplication :: InertSet     -- Given
 634                     -> Implication  -- Wanted
 635                     -> TcS (CanonicalCts,       -- Unsolved unification var = type
 636                             Bag Implication)    -- Unsolved rest (always empty or singleton)
 637 -- Returns:
 638 --  1. A bag of floatable wanted constraints, not mentioning any skolems,
 639 --     that are of the form unification var = type
 640 --
 641 --  2. Maybe a unsolved implication, empty if entirely solved!
 642 --
 643 -- Precondition: everything is zonked by now
 644 solveImplication inert
 645      imp@(Implic { ic_env_tvs = untch
 646                  , ic_binds   = ev_binds
 647                  , ic_skols   = skols
 648                  , ic_given   = givens
 649                  , ic_wanted = wanteds
 650                  , ic_loc = loc })
 651   = nestImplicTcS ev_binds untch $
 652     do { traceTcS "solveImplication {" (ppr imp)
 653
 654          -- Solve flat givens
 655        ; can_givens  <- canGivens loc givens
 656        ; given_inert <- solveInteract inert can_givens
 657
 658          -- Simplify the wanteds
 659        ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
 660
 661        ; let (res_flat_free, res_flat_bound)
 662                       = floatEqualities skols givens unsolved_flats
 663              unsolved = mkWantedConstraints res_flat_bound unsolved_implics
 664
 665        ; traceTcS "solveImplication end }" $ vcat
 666              [ text "res_flat_free =" <+> ppr res_flat_free
 667              , text "res_flat_bound =" <+> ppr res_flat_bound
 668              , text "unsolved_implics =" <+> ppr unsolved_implics ]
 669
 670        ; let res_bag | isEmptyBag unsolved = emptyBag
 671                      | otherwise           = unitBag (imp { ic_wanted  = unsolved })
 672
 673        ; return (res_flat_free, res_bag) }
 674
 675 floatEqualities :: TcTyVarSet -> [EvVar]
 676                 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
 677 floatEqualities skols can_given wanteds
 678   | hasEqualities can_given = (emptyBag, wanteds)
 679   | otherwise                 = partitionBag is_floatable wanteds
 680   where
 681     is_floatable :: CanonicalCt -> Bool
 682     is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
 683       | isMetaTyVar tv || isMetaTyVarTy ty
 684       = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
 685     is_floatable _ = False
 686 \end{code}
 687
 688 Note [Preparing inert set for implications]
 689 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 690 Before solving the nested implications, we convert any unsolved flat wanteds
 691 to givens, and add them to the inert set.  Reasons:
 692   a) In checking mode, suppresses unnecessary errors.  We already have
 693      on unsolved-wanted error; adding it to the givens prevents any
 694      consequential errors from showing uop
 695   b) More importantly, in inference mode, we are going to quantify over this
 696      constraint, and we *don't* want to quantify over any constraints that
 697      are deducible from it.
 698
 699 The unsolved wanteds are *canonical* but they may not be *inert*,
 700 because when made into a given they might interact with other givens.
 701 Hence the call to solveInteract.  Example:
 702
 703  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta])
 704
 705 We were not able to solve (a ~w [beta]) but we can't just assume it as
 706 given because the resulting set is not inert. Hence we have to do a
 707 'solveInteract' step first
 708
 709 *********************************************************************************
 710 *                                                                               *
 711 *                          Defaulting and disamgiguation                        *
 712 *                                                                               *
 713 *********************************************************************************
 714
 715 Basic plan behind applyDefaulting rules:
 716
 717  Step 1:
 718     Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
 719     For each defaultable group, do:
 720       For each possible substitution for [alpha |-> tau] where `alpha' is the
 721       group's variable, do:
 722         1) Make up new TcEvBinds
 723         2) Extend TcS with (groupVariable
 724         3) given_inert <- solveOne inert (given : a ~ tau)
 725         4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
 726         5) if unsolved == empty then
 727                  sneakyUnify a |-> tau
 728                  write the evidence bins
 729                  return (final_inert ++ group_constraints,[])
 730                       -- will contain the info (alpha |-> tau)!!
 731                  goto next defaultable group
 732            if unsolved <> empty then
 733                  throw away evidence binds
 734                  try next substitution
 735      If you've run out of substitutions for this group, too bad, you failed
 736                  return (inert,group)
 737                  goto next defaultable group
 738
 739  Step 2:
 740    Collect all the (canonical-cts, wanteds) gathered this way.
 741    - Do a solveGiven over the canonical-cts to make sure they are inert
 742 ------------------------------------------------------------------------------------------
 743
 744
 745 \begin{code}
 746 applyDefaultingRules :: InertSet
 747                      -> CanonicalCts    -- All wanteds
 748                      -> TcS CanonicalCts
 749 -- Return some *extra* givens, which express the
 750 -- type-class-default choice
 751
 752 applyDefaultingRules inert wanteds
 753   | isEmptyBag wanteds
 754   = return emptyBag
 755   | otherwise
 756   = do { untch <- getUntouchablesTcS
 757        ; tv_cts <- mapM (defaultTyVar untch) $
 758                    varSetElems (tyVarsOfCanonicals wanteds)
 759
 760        ; info@(_, default_tys, _) <- getDefaultInfo
 761        ; let groups = findDefaultableGroups info untch wanteds
 762        ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups
 763
 764        ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
 765                                  , text "Type defaults =" <+> ppr deflt_cts])
 766
 767        ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
 768
 769 ------------------
 770 defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
 771 -- defaultTyVar is used on any un-instantiated meta type variables to
 772 -- default the kind of ? and ?? etc to *.  This is important to ensure
 773 -- that instance declarations match.  For example consider
 774 --      instance Show (a->b)
 775 --      foo x = show (\_ -> True)
 776 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
 777 -- and that won't match the typeKind (*) in the instance decl.
 778 -- See test tc217.
 779 --
 780 -- We look only at touchable type variables. No further constraints
 781 -- are going to affect these type variables, so it's time to do it by
 782 -- hand.  However we aren't ready to default them fully to () or
 783 -- whatever, because the type-class defaulting rules have yet to run.
 784
 785 defaultTyVar untch the_tv
 786   | isMetaTyVar the_tv
 787   , not (the_tv `elemVarSet` untch)
 788   , not (k `eqKind` default_k)
 789   = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
 790        ; let loc = CtLoc TypeEqOrigin (getSrcSpan the_tv) [] -- Yuk
 791              wanted_eq  = CTyEqCan { cc_id     = ev
 792                                    , cc_flavor = Wanted loc
 793                                    , cc_tyvar  = the_tv
 794                                    , cc_rhs    = better_ty }
 795        ; return (unitBag wanted_eq) }
 796
 797   | otherwise
 798   = return emptyCCan     -- The common case
 799   where
 800     k = tyVarKind the_tv
 801     default_k = defaultKind k
 802
 803
 804 ----------------
 805 findDefaultableGroups
 806     :: ( SimplContext
 807        , [Type]
 808        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
 809     -> TcTyVarSet       -- Untouchable
 810     -> CanonicalCts     -- Unsolved
 811     -> [[(CanonicalCt,TcTyVar)]]
 812 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
 813                       untch wanteds
 814   | not (performDefaulting ctxt) = []
 815   | null default_tys             = []
 816   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
 817   where
 818     unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
 819     non_unaries :: [CanonicalCt]             -- and *other* constraints
 820
 821     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
 822         -- Finds unary type-class constraints
 823     find_unary cc@(CDictCan { cc_tyargs = [ty] })
 824         | Just tv <- tcGetTyVar_maybe ty
 825         = Left (cc, tv)
 826     find_unary cc = Right cc  -- Non unary or non dictionary
 827
 828     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries
 829     bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
 830
 831     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
 832
 833     is_defaultable_group ds@((_,tv):_)
 834         = isTyConableTyVar tv   -- Note [Avoiding spurious errors]
 835         && not (tv `elemVarSet` bad_tvs)
 836         && not (tv `elemVarSet` untch)    -- Non untouchable
 837         && defaultable_classes [cc_class cc | (cc,_) <- ds]
 838     is_defaultable_group [] = panic "defaultable_group"
 839
 840     defaultable_classes clss
 841         | extended_defaults = any isInteractiveClass clss
 842         | otherwise         = all is_std_class clss && (any is_num_class clss)
 843
 844     -- In interactive mode, or with -XExtendedDefaultRules,
 845     -- we default Show a to Show () to avoid graututious errors on "show []"
 846     isInteractiveClass cls
 847         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
 848
 849     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
 850     -- is_num_class adds IsString to the standard numeric classes,
 851     -- when -foverloaded-strings is enabled
 852
 853     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
 854     -- Similarly is_std_class
 855
 856 ------------------------------
 857 disambigGroup :: [Type]                    -- The default types
 858               -> TcTyVarSet                -- Untouchables
 859               -> InertSet                  -- Given inert
 860               -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
 861                                            --  sharing same type variable
 862               -> TcS CanonicalCts
 863
 864 disambigGroup [] _inert _untch _grp
 865   = return emptyBag
 866 disambigGroup (default_ty:default_tys) untch inert group
 867   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
 868        ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
 869                          -- We know this equality is canonical,
 870                          -- so we directly construct it as such
 871        ; let given_eq = CTyEqCan { cc_id     = ev
 872                                  , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
 873                                  , cc_tyvar  = the_tv
 874                                  , cc_rhs    = default_ty }
 875
 876        ; success <- tryTcS (extendVarSet untch the_tv) $
 877                     do { given_inert <- solveOne inert given_eq
 878                        ; final_inert <- solveInteract given_inert (listToBag wanteds)
 879                        ; let (_, unsolved) = extractUnsolved final_inert
 880                        ; return (isEmptyBag unsolved) }
 881
 882        ; case success of
 883            True  ->   -- Success: record the type variable binding, and return
 884                     do { setWantedTyBind the_tv default_ty
 885                        ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
 886                        ; traceTcS "disambigGoup succeeded" (ppr default_ty)
 887                        ; return (unitBag given_eq) }
 888            False ->    -- Failure: try with the next type
 889                     do { traceTcS "disambigGoup succeeded" (ppr default_ty)
 890                        ; disambigGroup default_tys untch inert group } }
 891   where
 892     ((the_ct,the_tv):_) = group
 893     wanteds = map fst group
 894     wanted_ev_vars = map deCanonicaliseWanted wanteds
 895 \end{code}
 896
 897 Note [Avoiding spurious errors]
 898 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 899 When doing the unification for defaulting, we check for skolem
 900 type variables, and simply don't default them.  For example:
 901    f = (*)      -- Monomorphic
 902    g :: Num a => a -> a
 903    g x = f x x
 904 Here, we get a complaint when checking the type signature for g,
 905 that g isn't polymorphic enough; but then we get another one when
 906 dealing with the (Num a) context arising from f's definition;
 907 we try to unify a with Int (to default it), but find that it's
 908 already been unified with the rigid variable from g's type sig
 909
 910