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