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 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              -- Make a guess at the quantified type variables
 202              -- Then split the constraints on the baisis of those tyvars
 203              -- to avoid unnecessarily simplifying a class constraint
 204              -- See Note [Avoid unecessary constraint simplification]
 205        ; gbl_tvs <- tcGetGlobalTyVars
 206        ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
 207        ; let proto_qtvs = zonked_tau_tvs `minusVarSet` gbl_tvs
 208              (perhaps_bound, surely_free)
 209                   = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
 210        ; emitConstraints surely_free
 211
 212               -- Now simplify the possibly-bound constraints
 213        ; (simplified_perhaps_bound, tc_binds)
 214               <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
 215
 216               -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
 217               --       may have done some unification
 218        ; gbl_tvs <- tcGetGlobalTyVars
 219        ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
 220        ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
 221        ; let qtvs = findQuantifiedTyVars apply_mr zonked_simples zonked_tau_tvs gbl_tvs
 222              (bound, free) | apply_mr  = (emptyBag, zonked_simples)
 223                            | otherwise = partitionBag (quantifyMe qtvs) zonked_simples
 224
 225        ; traceTc "end simplifyInfer }" $
 226               vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
 227                    , text "wanted = " <+> ppr zonked_wanted
 228                    , text "qtvs =   " <+> ppr qtvs
 229                    , text "free =   " <+> ppr free
 230                    , text "bound =  " <+> ppr bound ]
 231
 232        -- Turn the quantified meta-type variables into real type variables
 233        ; emitConstraints (mapBag WcEvVar free)
 234        ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems qtvs)
 235        ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
 236        ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }
 237
 238 ------------------------
 239 simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
 240                          -> TcM (Bag WantedEvVar, Bag EvBind)
 241 -- We use this function when inferring the type of a function
 242 -- The wanted constraints are already zonked
 243 simplifyAsMuchAsPossible ctxt wanteds
 244   = do { let untch = emptyVarSet
 245                  -- We allow ourselves to unify environment
 246                  -- variables; hence *no untouchables*
 247
 248        ; ((unsolved_flats, unsolved_implics), ev_binds)
 249            <- runTcS ctxt untch $
 250               simplifyApproxLoop 0 wanteds
 251
 252               -- Report any errors
 253        ; reportUnsolved (emptyBag, unsolved_implics)
 254
 255        ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
 256        ; return (final_wanted_evvars, ev_binds) }
 257
 258   where
 259     simplifyApproxLoop :: Int -> WantedConstraints
 260                        -> TcS (CanonicalCts, Bag Implication)
 261     simplifyApproxLoop n wanteds
 262      | n > 10
 263      = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations")
 264      | otherwise
 265      = do { traceTcS "simplifyApproxLoop" (vcat
 266                [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
 267           ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds
 268
 269           ; let (extra_flats, thiner_unsolved_implics)
 270                     = approximateImplications unsolved_implics
 271                 unsolved
 272                     = mkWantedConstraints unsolved_flats thiner_unsolved_implics
 273
 274           ;-- If no new work was produced then we are done with simplifyApproxLoop
 275             if isEmptyBag extra_flats
 276             then do { traceTcS "simplifyApproxLoopRes" (vcat
 277                               [ ptext (sLit "Wanted = ") <+> ppr wanteds
 278                               , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
 279                     ; return (unsolved_flats, unsolved_implics) }
 280
 281             else -- Produced new flat work wanteds, go round the loop
 282                 simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
 283           }
 284
 285 approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication)
 286 -- (wc1, impls2) <- approximateImplications impls
 287 -- splits 'impls' into two parts
 288 --    wc1:    a bag of constraints that do not mention any skolems
 289 --    impls2: a bag of *thiner* implication constraints
 290 approximateImplications impls
 291   = splitBag (do_implic emptyVarSet) impls
 292   where
 293     ------------------
 294     do_wanted :: TcTyVarSet -> WantedConstraint
 295               -> (WantedConstraints, WantedConstraints)
 296     do_wanted skols (WcImplic impl)
 297         = let (fl_w, mb_impl) = do_implic skols impl
 298           in (fl_w, mapBag WcImplic mb_impl)
 299     do_wanted skols wc@(WcEvVar wev)
 300       | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag)
 301       | otherwise                                      = (emptyBag, unitBag wc)
 302
 303     ------------------
 304     do_implic :: TcTyVarSet -> Implication
 305               -> (WantedConstraints, Bag Implication)
 306     do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
 307      = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
 308                           else unitBag impl{ ic_wanted = rest_wanted } )
 309      where
 310         (floatable_wanted, rest_wanted)
 311             = splitBag (do_wanted (skols `unionVarSet` skols')) wanted
 312
 313     ------------------
 314     splitBag :: (a -> (WantedConstraints, Bag a))
 315              -> Bag a -> (WantedConstraints, Bag a)
 316     splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
 317        where
 318          do_one x (b1,b2)
 319            = (wcs `unionBags` b1, imps `unionBags` b2)
 320            where
 321               (wcs, imps) = f x
 322 \end{code}
 323
 324 \begin{code}
 325 findQuantifiedTyVars :: Bool            -- Apply the MR
 326                      -> Bag WantedEvVar -- Simplified constraints from RHS
 327                      -> TyVarSet        -- Free in tau-type of definition
 328                      -> TyVarSet        -- Free in the envt
 329                      -> TyVarSet        -- Quantify over these
 330
 331 findQuantifiedTyVars apply_mr wanteds tau_tvs gbl_tvs
 332   | isEmptyBag wanteds = init_tvs
 333   | apply_mr           = init_tvs `minusVarSet` constrained_tvs
 334   | otherwise          = fixVarSet mk_next init_tvs
 335   where
 336     init_tvs    = tau_tvs `minusVarSet` gbl_tvs
 337     mk_next tvs = foldrBag grow_one tvs wanteds
 338
 339     grow_one wev tvs = tvs `unionVarSet` (extra_tvs `minusVarSet` gbl_tvs)
 340        where
 341          extra_tvs = growPredTyVars (wantedEvVarPred wev) tvs
 342
 343     constrained_tvs = tyVarsOfWantedEvVars wanteds
 344
 345 --------------------
 346 quantifyMe :: TyVarSet      -- Quantifying over these
 347            -> WantedEvVar
 348            -> Bool          -- True <=> quantify over this wanted
 349 quantifyMe qtvs wev
 350   | isIPPred pred = True  -- Note [Inheriting implicit parameters]
 351   | otherwise     = tyVarsOfPred pred `intersectsVarSet` qtvs
 352   where
 353     pred = wantedEvVarPred wev
 354
 355 quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
 356 quantifyMeWC qtvs (WcImplic implic)
 357   = anyBag (quantifyMeWC (qtvs `minusVarSet` ic_skols implic)) (ic_wanted implic)
 358 quantifyMeWC qtvs (WcEvVar wev)
 359   = quantifyMe qtvs wev
 360 \end{code}
 361
 362 Note [Avoid unecessary constraint simplification]
 363 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 364 When inferring the type of a let-binding, with simplifyInfer,
 365 try to avoid unnecessariliy simplifying class constraints.
 366 Doing so aids sharing, but it also helps with delicate
 367 situations like
 368    instance C t => C [t] where ..
 369    f :: C [t] => ....
 370    f x = let g y = ...(constraint C [t])...
 371          in ...
 372 When inferring a type for 'g', we don't want to apply the
 373 instance decl, because then we can't satisfy (C t).  So we
 374 just notice that g isn't quantified over 't' and partition
 375 the contraints before simplifying.
 376
 377 This only half-works, but then let-generalisation only half-works.
 378
 379
 380 Note [Inheriting implicit parameters]
 381 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 382 Consider this:
 383
 384         f x = (x::Int) + ?y
 385
 386 where f is *not* a top-level binding.
 387 From the RHS of f we'll get the constraint (?y::Int).
 388 There are two types we might infer for f:
 389
 390         f :: Int -> Int
 391
 392 (so we get ?y from the context of f's definition), or
 393
 394         f :: (?y::Int) => Int -> Int
 395
 396 At first you might think the first was better, becuase then
 397 ?y behaves like a free variable of the definition, rather than
 398 having to be passed at each call site.  But of course, the WHOLE
 399 IDEA is that ?y should be passed at each call site (that's what
 400 dynamic binding means) so we'd better infer the second.
 401
 402 BOTTOM LINE: when *inferring types* you *must* quantify
 403 over implicit parameters. See the predicate isFreeWhenInferring.
 404
 405
 406 *********************************************************************************
 407 *                                                                                 *
 408 *                             Superclasses                                        *
 409 *                                                                                 *
 410 ***********************************************************************************
 411
 412 When constructing evidence for superclasses in an instance declaration,
 413   * we MUST have the "self" dictionary available, but
 414   * we must NOT have its superclasses derived from "self"
 415
 416 Moreover, we must *completely* solve the constraints right now,
 417 not wrap them in an implication constraint to solve later.  Why?
 418 Because when that implication constraint is solved there may
 419 be some unrelated other solved top-level constraints that
 420 recursively depend on the superclass we are building. Consider
 421    class Ord a => C a where
 422    instance C [Int] where ...
 423 Then we get
 424    dCListInt :: C [Int]
 425    dCListInt = MkC $cNum ...
 426
 427    $cNum :: Ord [Int] -- The superclass
 428    $cNum = let self = dCListInt in <solve Ord [Int]>
 429
 430 Now, if there is some *other* top-level constraint solved
 431 looking like
 432         foo :: Ord [Int]
 433         foo = scsel dCInt
 434 we must not solve the (Ord [Int]) wanted from foo!!
 435
 436 \begin{code}
 437 simplifySuperClass :: EvVar     -- The "self" dictionary
 438                    -> WantedConstraints
 439                    -> TcM ()
 440 simplifySuperClass self wanteds
 441   = do { wanteds <- mapBagM zonkWanted wanteds
 442        ; loc <- getCtLoc NoScSkol
 443        ; (unsolved, ev_binds)
 444              <- runTcS SimplCheck emptyVarSet $
 445                 do { can_self <- canGivens loc [self]
 446                    ; let inert = foldlBag updInertSet emptyInert can_self
 447                      -- No need for solveInteract; we know it's inert
 448
 449                    ; solveWanteds inert wanteds }
 450
 451        ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
 452          reportUnsolved unsolved }
 453 \end{code}
 454
 455
 456 *********************************************************************************
 457 *                                                                                 *
 458 *                             RULES                                               *
 459 *                                                                                 *
 460 ***********************************************************************************
 461
 462 Note [Simplifying RULE lhs constraints]
 463 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 464 On the LHS of transformation rules we only simplify only equalitis,
 465 but not dictionaries.  We want to keep dictionaries unsimplified, to
 466 serve as the available stuff for the RHS of the rule.  We *do* want to
 467 simplify equalities, however, to detect ill-typed rules that cannot be
 468 applied.
 469
 470 Implementation: the TcSFlags carried by the TcSMonad controls the
 471 amount of simplification, so simplifyRuleLhs just sets the flag
 472 appropriately.
 473
 474 Example.  Consider the following left-hand side of a rule
 475         f (x == y) (y > z) = ...
 476 If we typecheck this expression we get constraints
 477         d1 :: Ord a, d2 :: Eq a
 478 We do NOT want to "simplify" to the LHS
 479         forall x::a, y::a, z::a, d1::Ord a.
 480           f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
 481 Instead we want
 482         forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
 483           f ((==) d2 x y) ((>) d1 y z) = ...
 484
 485 Here is another example:
 486         fromIntegral :: (Integral a, Num b) => a -> b
 487         {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
 488 In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
 489 we *dont* want to get
 490         forall dIntegralInt.
 491            fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
 492 because the scsel will mess up RULE matching.  Instead we want
 493         forall dIntegralInt, dNumInt.
 494           fromIntegral Int Int dIntegralInt dNumInt = id Int
 495
 496 Even if we have
 497         g (x == y) (y == z) = ..
 498 where the two dictionaries are *identical*, we do NOT WANT
 499         forall x::a, y::a, z::a, d1::Eq a
 500           f ((==) d1 x y) ((>) d1 y z) = ...
 501 because that will only match if the dict args are (visibly) equal.
 502 Instead we want to quantify over the dictionaries separately.
 503
 504 In short, simplifyRuleLhs must *only* squash equalities, leaving
 505 all dicts unchanged, with absolutely no sharing.
 506
 507 HOWEVER, under a nested implication things are different
 508 Consider
 509   f :: (forall a. Eq a => a->a) -> Bool -> ...
 510   {-# RULES "foo" forall (v::forall b. Eq b => b->b).
 511        f b True = ...
 512     #=}
 513 Here we *must* solve the wanted (Eq a) from the given (Eq a)
 514 resulting from skolemising the agument type of g.  So we
 515 revert to SimplCheck when going under an implication.
 516
 517 \begin{code}
 518 simplifyRule :: RuleName
 519              -> [TcTyVar]               -- Explicit skolems
 520              -> WantedConstraints       -- Constraints from LHS
 521              -> WantedConstraints       -- Constraints from RHS
 522              -> TcM ([EvVar],           -- LHS dicts
 523                      TcEvBinds,         -- Evidence for LHS
 524                      TcEvBinds)         -- Evidence for RHS
 525 -- See Note [Simplifying RULE lhs constraints]
 526 simplifyRule name tv_bndrs lhs_wanted rhs_wanted
 527   = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
 528        ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs
 529
 530        -- Don't quantify over equalities (judgement call here)
 531        ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
 532              lhs_dicts    = map wantedEvVarToVar (bagToList dicts)
 533                                  -- Dicts and implicit parameters
 534        ; reportUnsolvedWantedEvVars eqs
 535
 536              -- Notice that we simplify the RHS with only the explicitly
 537              -- introduced skolems, allowing the RHS to constrain any
 538              -- unification variables.
 539              -- Then, and only then, we call zonkQuantifiedTypeVariables
 540              -- Example   foo :: Ord a => a -> a
 541              --           foo_spec :: Int -> Int
 542              --           {-# RULE "foo"  foo = foo_spec #-}
 543              --     Here, it's the RHS that fixes the type variable
 544
 545              -- So we don't want to make untouchable the type
 546              -- variables in the envt of the RHS, because they include
 547              -- the template variables of the RULE
 548
 549              -- Hence the rather painful ad-hoc treatement here
 550        ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
 551        ; loc        <- getCtLoc (RuleSkol name)
 552        ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $
 553              Implic { ic_untch = emptyVarSet      -- No untouchables
 554                     , ic_env = emptyNameEnv
 555                     , ic_skols = mkVarSet tv_bndrs
 556                     , ic_scoped = panic "emitImplication"
 557                     , ic_given = lhs_dicts
 558                     , ic_wanted = rhs_wanted
 559                     , ic_binds = rhs_binds_var
 560                     , ic_loc = loc }
 561        ; rhs_binds2 <- readTcRef evb_ref
 562
 563        ; return ( lhs_dicts
 564                 , EvBinds lhs_binds
 565                 , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
 566 \end{code}
 567
 568
 569 *********************************************************************************
 570 *                                                                                 *
 571 *                                 Main Simplifier                                 *
 572 *                                                                                 *
 573 ***********************************************************************************
 574
 575 \begin{code}
 576 simplifyCheck :: SimplContext
 577               -> WantedConstraints      -- Wanted
 578               -> TcM (Bag EvBind)
 579 -- Solve a single, top-level implication constraint
 580 -- e.g. typically one created from a top-level type signature
 581 --          f :: forall a. [a] -> [a]
 582 --          f x = rhs
 583 -- We do this even if the function has no polymorphism:
 584 --          g :: Int -> Int
 585
 586 --          g y = rhs
 587 -- (whereas for *nested* bindings we would not create
 588 --  an implication constraint for g at all.)
 589 --
 590 -- Fails if can't solve something in the input wanteds
 591 simplifyCheck ctxt wanteds
 592   = do { wanteds <- mapBagM zonkWanted wanteds
 593
 594        ; traceTc "simplifyCheck {" (vcat
 595              [ ptext (sLit "wanted =") <+> ppr wanteds ])
 596
 597        ; (unsolved, ev_binds) <- runTcS ctxt emptyVarSet $
 598                                  solveWanteds emptyInert wanteds
 599
 600        ; traceTc "simplifyCheck }" $
 601              ptext (sLit "unsolved =") <+> ppr unsolved
 602
 603        ; reportUnsolved unsolved
 604
 605        ; return ev_binds }
 606
 607 ----------------
 608 solveWanteds :: InertSet               -- Given
 609              -> WantedConstraints      -- Wanted
 610              -> TcS (CanonicalCts,     -- Unsolved flats
 611                      Bag Implication)  -- Unsolved implications
 612 -- solveWanteds iterates when it is able to float equalities
 613 -- out of one or more of the implications
 614 solveWanteds inert wanteds
 615   = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
 616        ; can_flats <- canWanteds $ bagToList flat_wanteds
 617        ; traceTcS "solveWanteds {" $
 618                  vcat [ text "wanteds =" <+> ppr wanteds
 619                       , text "inert =" <+> ppr inert ]
 620        ; (unsolved_flats, unsolved_implics)
 621                <- simpl_loop 1 can_flats implic_wanteds
 622        ; traceTcS "solveWanteds }" $
 623                  vcat [ text "wanteds =" <+> ppr wanteds
 624                       , text "unsolved_flats =" <+> ppr unsolved_flats
 625                       , text "unsolved_implics =" <+> ppr unsolved_implics ]
 626        ; return (unsolved_flats, unsolved_implics)  }
 627   where
 628     simpl_loop :: Int
 629                -> CanonicalCts  -- May inlude givens (in the recursive call)
 630                -> Bag Implication
 631                -> TcS (CanonicalCts, Bag Implication)
 632     simpl_loop n can_ws implics
 633       | n>10
 634       = trace "solveWanteds: loop" $    -- Always bleat
 635         do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
 636            ; return (can_ws, implics) }
 637
 638       | otherwise
 639       = do { inert1 <- solveInteract inert can_ws
 640            ; let (inert2, unsolved_flats) = extractUnsolved inert1
 641
 642            ; traceTcS "solveWanteds/done flats"  $
 643                  vcat [ text "inerts =" <+> ppr inert2
 644                       , text "unsolved =" <+> ppr unsolved_flats ]
 645
 646                    -- See Note [Preparing inert set for implications]
 647            ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
 648            ; (implic_eqs, unsolved_implics)
 649                 <- flatMapBagPairM (solveImplication inert_for_implics) implics
 650
 651                 -- Apply defaulting rules if and only if there
 652                 -- no floated equalities.  If there are, they may
 653                 -- solve the remaining wanteds, so don't do defaulting.
 654            ; final_eqs <- if not (isEmptyBag implic_eqs)
 655                           then return implic_eqs
 656                           else applyDefaultingRules inert2 unsolved_flats
 657                 -- default_eqs are *givens*, so simpl_loop may
 658                 -- recurse with givens in the argument
 659
 660            ; if isEmptyBag final_eqs then
 661                  return (unsolved_flats, unsolved_implics)
 662              else
 663                  do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
 664                         [ text "floated_unsolved_eqs =" <+> ppr final_eqs
 665                         , text "unsolved_implics = " <+> ppr unsolved_implics ]
 666                     ; simpl_loop (n+1)
 667                                  (unsolved_flats `unionBags` final_eqs)
 668                                  unsolved_implics
 669            }        }
 670
 671 solveImplication :: InertSet     -- Given
 672                     -> Implication  -- Wanted
 673                     -> TcS (CanonicalCts,       -- Unsolved unification var = type
 674                             Bag Implication)    -- Unsolved rest (always empty or singleton)
 675 -- Returns:
 676 --  1. A bag of floatable wanted constraints, not mentioning any skolems,
 677 --     that are of the form unification var = type
 678 --
 679 --  2. Maybe a unsolved implication, empty if entirely solved!
 680 --
 681 -- Precondition: everything is zonked by now
 682 solveImplication inert
 683      imp@(Implic { ic_untch  = untch
 684                  , ic_binds  = ev_binds
 685                  , ic_skols  = skols
 686                  , ic_given  = givens
 687                  , ic_wanted = wanteds
 688                  , ic_loc    = loc })
 689   = nestImplicTcS ev_binds untch $
 690     do { traceTcS "solveImplication {" (ppr imp)
 691
 692          -- Solve flat givens
 693        ; can_givens  <- canGivens loc givens
 694        ; given_inert <- solveInteract inert can_givens
 695
 696          -- Simplify the wanteds
 697        ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds
 698
 699        ; let (res_flat_free, res_flat_bound)
 700                       = floatEqualities skols givens unsolved_flats
 701              unsolved = mkWantedConstraints res_flat_bound unsolved_implics
 702
 703        ; traceTcS "solveImplication end }" $ vcat
 704              [ text "res_flat_free =" <+> ppr res_flat_free
 705              , text "res_flat_bound =" <+> ppr res_flat_bound
 706              , text "unsolved_implics =" <+> ppr unsolved_implics ]
 707
 708        ; let res_bag | isEmptyBag unsolved = emptyBag
 709                      | otherwise           = unitBag (imp { ic_wanted  = unsolved })
 710
 711        ; return (res_flat_free, res_bag) }
 712
 713 floatEqualities :: TcTyVarSet -> [EvVar]
 714                 -> CanonicalCts -> (CanonicalCts, CanonicalCts)
 715 floatEqualities skols can_given wanteds
 716   | hasEqualities can_given = (emptyBag, wanteds)
 717   | otherwise               = partitionBag is_floatable wanteds
 718   where
 719     is_floatable :: CanonicalCt -> Bool
 720     is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
 721       | isMetaTyVar tv || isMetaTyVarTy ty
 722       = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
 723     is_floatable _ = False
 724 \end{code}
 725
 726 Note [Preparing inert set for implications]
 727 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 728 Before solving the nested implications, we convert any unsolved flat wanteds
 729 to givens, and add them to the inert set.  Reasons:
 730   a) In checking mode, suppresses unnecessary errors.  We already have
 731      on unsolved-wanted error; adding it to the givens prevents any
 732      consequential errors from showing uop
 733   b) More importantly, in inference mode, we are going to quantify over this
 734      constraint, and we *don't* want to quantify over any constraints that
 735      are deducible from it.
 736
 737 The unsolved wanteds are *canonical* but they may not be *inert*,
 738 because when made into a given they might interact with other givens.
 739 Hence the call to solveInteract.  Example:
 740
 741  Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta])
 742
 743 We were not able to solve (a ~w [beta]) but we can't just assume it as
 744 given because the resulting set is not inert. Hence we have to do a
 745 'solveInteract' step first
 746
 747 *********************************************************************************
 748 *                                                                               *
 749 *                          Defaulting and disamgiguation                        *
 750 *                                                                               *
 751 *********************************************************************************
 752
 753 Basic plan behind applyDefaulting rules:
 754
 755  Step 1:
 756     Split wanteds into defaultable groups, `groups' and the rest `rest_wanted'
 757     For each defaultable group, do:
 758       For each possible substitution for [alpha |-> tau] where `alpha' is the
 759       group's variable, do:
 760         1) Make up new TcEvBinds
 761         2) Extend TcS with (groupVariable
 762         3) given_inert <- solveOne inert (given : a ~ tau)
 763         4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
 764         5) if unsolved == empty then
 765                  sneakyUnify a |-> tau
 766                  write the evidence bins
 767                  return (final_inert ++ group_constraints,[])
 768                       -- will contain the info (alpha |-> tau)!!
 769                  goto next defaultable group
 770            if unsolved <> empty then
 771                  throw away evidence binds
 772                  try next substitution
 773      If you've run out of substitutions for this group, too bad, you failed
 774                  return (inert,group)
 775                  goto next defaultable group
 776
 777  Step 2:
 778    Collect all the (canonical-cts, wanteds) gathered this way.
 779    - Do a solveGiven over the canonical-cts to make sure they are inert
 780 ------------------------------------------------------------------------------------------
 781
 782
 783 \begin{code}
 784 applyDefaultingRules :: InertSet
 785                      -> CanonicalCts    -- All wanteds
 786                      -> TcS CanonicalCts
 787 -- Return some *extra* givens, which express the
 788 -- type-class-default choice
 789
 790 applyDefaultingRules inert wanteds
 791   | isEmptyBag wanteds
 792   = return emptyBag
 793   | otherwise
 794   = do { untch <- getUntouchablesTcS
 795        ; tv_cts <- mapM (defaultTyVar untch) $
 796                    varSetElems (tyVarsOfCanonicals wanteds)
 797
 798        ; info@(_, default_tys, _) <- getDefaultInfo
 799        ; let groups = findDefaultableGroups info untch wanteds
 800        ; deflt_cts <- mapM (disambigGroup default_tys untch inert) groups
 801
 802        ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
 803                                  , text "Type defaults =" <+> ppr deflt_cts])
 804
 805        ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }
 806
 807 ------------------
 808 defaultTyVar :: TcTyVarSet -> TcTyVar -> TcS CanonicalCts
 809 -- defaultTyVar is used on any un-instantiated meta type variables to
 810 -- default the kind of ? and ?? etc to *.  This is important to ensure
 811 -- that instance declarations match.  For example consider
 812 --      instance Show (a->b)
 813 --      foo x = show (\_ -> True)
 814 -- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??),
 815 -- and that won't match the typeKind (*) in the instance decl.
 816 -- See test tc217.
 817 --
 818 -- We look only at touchable type variables. No further constraints
 819 -- are going to affect these type variables, so it's time to do it by
 820 -- hand.  However we aren't ready to default them fully to () or
 821 -- whatever, because the type-class defaulting rules have yet to run.
 822
 823 defaultTyVar untch the_tv
 824   | isMetaTyVar the_tv
 825   , not (the_tv `elemVarSet` untch)
 826   , not (k `eqKind` default_k)
 827   = do { (ev, better_ty) <- TcSMonad.newKindConstraint (mkTyVarTy the_tv) default_k
 828        ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
 829                    -- 'DefaultOrigin' is strictly the declaration, but it's convenient
 830              wanted_eq  = CTyEqCan { cc_id     = ev
 831                                    , cc_flavor = Wanted loc
 832                                    , cc_tyvar  = the_tv
 833                                    , cc_rhs    = better_ty }
 834        ; return (unitBag wanted_eq) }
 835
 836   | otherwise
 837   = return emptyCCan     -- The common case
 838   where
 839     k = tyVarKind the_tv
 840     default_k = defaultKind k
 841
 842
 843 ----------------
 844 findDefaultableGroups
 845     :: ( SimplContext
 846        , [Type]
 847        , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
 848     -> TcTyVarSet       -- Untouchable
 849     -> CanonicalCts     -- Unsolved
 850     -> [[(CanonicalCt,TcTyVar)]]
 851 findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults))
 852                       untch wanteds
 853   | not (performDefaulting ctxt) = []
 854   | null default_tys             = []
 855   | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
 856   where
 857     unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
 858     non_unaries :: [CanonicalCt]             -- and *other* constraints
 859
 860     (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
 861         -- Finds unary type-class constraints
 862     find_unary cc@(CDictCan { cc_tyargs = [ty] })
 863         | Just tv <- tcGetTyVar_maybe ty
 864         = Left (cc, tv)
 865     find_unary cc = Right cc  -- Non unary or non dictionary
 866
 867     bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries
 868     bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries
 869
 870     cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2
 871
 872     is_defaultable_group ds@((_,tv):_)
 873         = isTyConableTyVar tv   -- Note [Avoiding spurious errors]
 874         && not (tv `elemVarSet` bad_tvs)
 875         && not (tv `elemVarSet` untch)    -- Non untouchable
 876         && defaultable_classes [cc_class cc | (cc,_) <- ds]
 877     is_defaultable_group [] = panic "defaultable_group"
 878
 879     defaultable_classes clss
 880         | extended_defaults = any isInteractiveClass clss
 881         | otherwise         = all is_std_class clss && (any is_num_class clss)
 882
 883     -- In interactive mode, or with -XExtendedDefaultRules,
 884     -- we default Show a to Show () to avoid graututious errors on "show []"
 885     isInteractiveClass cls
 886         = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])
 887
 888     is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
 889     -- is_num_class adds IsString to the standard numeric classes,
 890     -- when -foverloaded-strings is enabled
 891
 892     is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
 893     -- Similarly is_std_class
 894
 895 ------------------------------
 896 disambigGroup :: [Type]                    -- The default types
 897               -> TcTyVarSet                -- Untouchables
 898               -> InertSet                  -- Given inert
 899               -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
 900                                            --  sharing same type variable
 901               -> TcS CanonicalCts
 902
 903 disambigGroup [] _inert _untch _grp
 904   = return emptyBag
 905 disambigGroup (default_ty:default_tys) untch inert group
 906   = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
 907        ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl
 908                          -- We know this equality is canonical,
 909                          -- so we directly construct it as such
 910        ; let given_eq = CTyEqCan { cc_id     = ev
 911                                  , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
 912                                  , cc_tyvar  = the_tv
 913                                  , cc_rhs    = default_ty }
 914
 915        ; success <- tryTcS (extendVarSet untch the_tv) $
 916                     do { given_inert <- solveOne inert given_eq
 917                        ; final_inert <- solveInteract given_inert (listToBag wanteds)
 918                        ; let (_, unsolved) = extractUnsolved final_inert
 919                        ; return (isEmptyBag unsolved) }
 920
 921        ; case success of
 922            True  ->   -- Success: record the type variable binding, and return
 923                     do { setWantedTyBind the_tv default_ty
 924                        ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
 925                        ; traceTcS "disambigGoup succeeded" (ppr default_ty)
 926                        ; return (unitBag given_eq) }
 927            False ->    -- Failure: try with the next type
 928                     do { traceTcS "disambigGoup succeeded" (ppr default_ty)
 929                        ; disambigGroup default_tys untch inert group } }
 930   where
 931     ((the_ct,the_tv):_) = group
 932     wanteds = map fst group
 933     wanted_ev_vars = map deCanonicaliseWanted wanteds
 934 \end{code}
 935
 936 Note [Avoiding spurious errors]
 937 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 938 When doing the unification for defaulting, we check for skolem
 939 type variables, and simply don't default them.  For example:
 940    f = (*)      -- Monomorphic
 941    g :: Num a => a -> a
 942    g x = f x x
 943 Here, we get a complaint when checking the type signature for g,
 944 that g isn't polymorphic enough; but then we get another one when
 945 dealing with the (Num a) context arising from f's definition;
 946 we try to unify a with Int (to default it), but find that it's
 947 already been unified with the rigid variable from g's type sig
 948
 949