compiler/typecheck/TcSimplify.lhs

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