TcSimplify.lhs 40 KB
Newer Older
1
\begin{code}
2 3 4 5 6
module TcSimplify( 
       simplifyInfer, simplifySuperClass,
       simplifyDefault, simplifyDeriv, simplifyBracket,
       simplifyRule, simplifyTop, simplifyInteractive
  ) where
7

8
#include "HsVersions.h"
9

10
import HsSyn	       
11
import TcRnMonad
12 13
import TcErrors
import TcCanonical
14
import TcMType
15 16 17 18
import TcType 
import TcSMonad 
import TcInteract
import Inst
19
import Var
20
import VarSet
21 22
import VarEnv ( varEnvElts ) 

23 24
import Name
import NameEnv	( emptyNameEnv )
25
import Bag
26 27
import ListSetOps
import Util
28 29 30 31 32 33
import PrelInfo
import PrelNames
import Class		( classKey )
import BasicTypes	( RuleName )
import Data.List	( partition )
import Outputable
34
import FastString
35 36 37
\end{code}


38 39 40 41 42
*********************************************************************************
*                                                                               * 
*                           External interface                                  *
*                                                                               *
*********************************************************************************
43

44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67
\begin{code}
simplifyTop :: WantedConstraints -> TcM (Bag EvBind)
-- Simplify top-level constraints
-- Usually these will be implications, when there is
--   nothing to quanitfy we don't wrap in a degenerate implication,
--   so we do that here instead
simplifyTop wanteds 
  = simplifyCheck SimplCheck wanteds

------------------
simplifyInteractive :: WantedConstraints -> TcM (Bag EvBind)
simplifyInteractive wanteds 
  = simplifyCheck SimplInteractive wanteds

------------------
simplifyDefault :: ThetaType	-- Wanted; has no type variables in it
                -> TcM ()	-- Succeeds iff the constraint is soluble
simplifyDefault theta
  = do { loc <- getCtLoc DefaultOrigin
       ; wanted <- newWantedEvVars theta
       ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]
       ; _ignored_ev_binds <- simplifyCheck SimplCheck wanted_bag
       ; return () }
\end{code}
68

69 70 71 72 73 74
simplifyBracket is used when simplifying the constraints arising from
a Template Haskell bracket [| ... |].  We want to check that there aren't
any constraints that can't be satisfied (e.g. Show Foo, where Foo has no
Show instance), but we aren't otherwise interested in the results.
Nor do we care about ambiguous dictionaries etc.  We will type check
this bracket again at its usage site.
75

76 77 78 79 80 81 82
\begin{code}
simplifyBracket :: WantedConstraints -> TcM ()
simplifyBracket wanteds
  = do	{ zonked_wanteds <- mapBagM zonkWanted wanteds 
        ; _ <- simplifyAsMuchAsPossible SimplInfer zonked_wanteds
	; return () }
\end{code}
83

84

85 86 87 88 89
*********************************************************************************
*                                                                                 * 
*                            Deriving
*                                                                                 *
***********************************************************************************
90

91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121
\begin{code}
simplifyDeriv :: CtOrigin
		-> [TyVar]	
		-> ThetaType		-- Wanted
	        -> TcM ThetaType	-- Needed
-- Given  instance (wanted) => C inst_ty 
-- Simplify 'wanted' as much as possibles
simplifyDeriv orig tvs theta 
  = do { tvs_skols <- tcInstSkolTyVars InstSkol tvs -- Skolemize 
       	 	   -- One reason is that the constraint solving machinery
		   -- expects *TcTyVars* not TyVars.  Another is that
		   -- when looking up instances we don't want overlap
		   -- of type variables

       ; let skol_subst = zipTopTvSubst tvs $ map mkTyVarTy tvs_skols
             
       ; loc    <- getCtLoc orig
       ; wanted <- newWantedEvVars (substTheta skol_subst theta)
       ; let wanted_bag = listToBag [WcEvVar (WantedEvVar w loc) | w <- wanted]

       ; traceTc "simlifyDeriv" (ppr tvs $$ ppr theta $$ ppr wanted)
       ; (unsolved, _binds) <- simplifyAsMuchAsPossible SimplInfer wanted_bag

       ; let (good, bad) = partition validDerivPred $
                           foldrBag ((:) . wantedEvVarPred) [] unsolved
		-- See Note [Exotic derived instance contexts]
             subst_skol = zipTopTvSubst tvs_skols $ map mkTyVarTy tvs 

       ; reportUnsolvedDeriv bad loc
       ; return $ substTheta subst_skol good }
\end{code}
122

123 124 125 126 127 128 129
Note [Exotic derived instance contexts]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In a 'derived' instance declaration, we *infer* the context.  It's a
bit unclear what rules we should apply for this; the Haskell report is
silent.  Obviously, constraints like (Eq a) are fine, but what about
	data T f a = MkT (f a) deriving( Eq )
where we'd get an Eq (f a) constraint.  That's probably fine too.
130

131 132 133
One could go further: consider
	data T a b c = MkT (Foo a b c) deriving( Eq )
	instance (C Int a, Eq b, Eq c) => Eq (Foo a b c)
134

135 136
Notice that this instance (just) satisfies the Paterson termination 
conditions.  Then we *could* derive an instance decl like this:
137

138 139 140 141
	instance (C Int a, Eq b, Eq c) => Eq (T a b c) 
even though there is no instance for (C Int a), because there just
*might* be an instance for, say, (C Int Bool) at a site where we
need the equality instance for T's.  
142

143 144 145
However, this seems pretty exotic, and it's quite tricky to allow
this, and yet give sensible error messages in the (much more common)
case where we really want that instance decl for C.
146

147 148
So for now we simply require that the derived instance context
should have only type-variable constraints.
149

150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
Here is another example:
	data Fix f = In (f (Fix f)) deriving( Eq )
Here, if we are prepared to allow -XUndecidableInstances we
could derive the instance
	instance Eq (f (Fix f)) => Eq (Fix f)
but this is so delicate that I don't think it should happen inside
'deriving'. If you want this, write it yourself!

NB: if you want to lift this condition, make sure you still meet the
termination conditions!  If not, the deriving mechanism generates
larger and larger constraints.  Example:
  data Succ a = S a
  data Seq a = Cons a (Seq (Succ a)) | Nil deriving Show

Note the lack of a Show instance for Succ.  First we'll generate
  instance (Show (Succ a), Show a) => Show (Seq a)
and then
  instance (Show (Succ (Succ a)), Show (Succ a), Show a) => Show (Seq a)
and so on.  Instead we want to complain of no instance for (Show (Succ a)).

The bottom line
~~~~~~~~~~~~~~~
Allow constraints which consist only of type variables, with no repeats.

*********************************************************************************
*                                                                                 * 
*                            Inference
*                                                                                 *
***********************************************************************************
179

180 181 182 183 184 185 186 187 188 189
\begin{code}
simplifyInfer :: Bool		    -- Apply monomorphism restriction
              -> TcTyVarSet         -- These type variables are free in the
                                    -- types to be generalised
              -> WantedConstraints
              -> TcM ([TcTyVar],    -- Quantify over these type variables
                      [EvVar],      -- ... and these constraints
                      TcEvBinds)    -- ... binding these evidence variables
simplifyInfer apply_mr tau_tvs wanted
  | isEmptyBag wanted	  -- Trivial case is quite common
190
  = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
191 192 193
       ; gbl_tvs        <- tcGetGlobalTyVars	     -- Already zonked
       ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
       ; return (qtvs, [], emptyTcEvBinds) }
194

195 196 197 198 199 200 201 202
  | otherwise
  = do { zonked_wanted <- mapBagM zonkWanted wanted 
       ; traceTc "simplifyInfer {"  $ vcat
             [ ptext (sLit "apply_mr =") <+> ppr apply_mr
             , ptext (sLit "wanted =") <+> ppr zonked_wanted
             , ptext (sLit "tau_tvs =") <+> ppr tau_tvs
             ]

203 204 205 206 207 208
	     -- Make a guess at the quantified type variables
	     -- Then split the constraints on the baisis of those tyvars
	     -- to avoid unnecessarily simplifying a class constraint
	     -- See Note [Avoid unecessary constraint simplification]
       ; gbl_tvs <- tcGetGlobalTyVars
       ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
209 210
       ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
                          zonked_tau_tvs `minusVarSet` gbl_tvs
211 212
             (perhaps_bound, surely_free) 
                  = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
213
      
214
       ; emitConstraints surely_free
215 216 217 218
       ; traceTc "sinf"  $ vcat
             [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
             , ptext (sLit "surely_free   =") <+> ppr surely_free
             ]
219 220 221 222

       	      -- Now simplify the possibly-bound constraints
       ; (simplified_perhaps_bound, tc_binds) 
              <- simplifyAsMuchAsPossible SimplInfer perhaps_bound
223

224 225
	      -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
	      --       may have done some unification
226
       ; gbl_tvs <- tcGetGlobalTyVars
227
       ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
228
       ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
229 230 231 232 233 234 235
       ; let init_tvs 	     = zonked_tau_tvs `minusVarSet` gbl_tvs
             mr_qtvs  	     = init_tvs `minusVarSet` constrained_tvs
             constrained_tvs = tyVarsOfWantedEvVars zonked_simples
             qtvs            = growWantedEVs gbl_tvs zonked_simples init_tvs
             (final_qtvs, (bound, free))
                | apply_mr  = (mr_qtvs, (emptyBag, zonked_simples))
                | otherwise = (qtvs,    partitionBag (quantifyMe qtvs) zonked_simples)
236 237 238 239

       ; traceTc "end simplifyInfer }" $
              vcat [ ptext (sLit "apply_mr =") <+> ppr apply_mr
                   , text "wanted = " <+> ppr zonked_wanted
240
                   , text "qtvs =   " <+> ppr final_qtvs
241 242 243 244 245
                   , text "free =   " <+> ppr free
                   , text "bound =  " <+> ppr bound ]

       -- Turn the quantified meta-type variables into real type variables 
       ; emitConstraints (mapBag WcEvVar free)
246
       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) 
247 248 249 250 251 252 253 254 255
       ; let bound_evvars = bagToList $ mapBag wantedEvVarToVar bound
       ; return (qtvs_to_return, bound_evvars, EvBinds tc_binds) }

------------------------
simplifyAsMuchAsPossible :: SimplContext -> WantedConstraints
                         -> TcM (Bag WantedEvVar, Bag EvBind) 
-- We use this function when inferring the type of a function
-- The wanted constraints are already zonked
simplifyAsMuchAsPossible ctxt wanteds
256
  = do { let untch = NoUntouchables
257 258 259 260 261 262 263 264
	     	 -- We allow ourselves to unify environment 
		 -- variables; hence *no untouchables*

       ; ((unsolved_flats, unsolved_implics), ev_binds) 
           <- runTcS ctxt untch $
              simplifyApproxLoop 0 wanteds

	      -- Report any errors
265
       ; reportUnsolved (emptyBag, unsolved_implics)
266 267 268

       ; let final_wanted_evvars = mapBag deCanonicaliseWanted unsolved_flats
       ; return (final_wanted_evvars, ev_binds) }
269

270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
  where 
    simplifyApproxLoop :: Int -> WantedConstraints
                       -> TcS (CanonicalCts, Bag Implication)
    simplifyApproxLoop n wanteds
     | n > 10 
     = pprPanic "simplifyApproxLoop loops!" (ppr n <+> text "iterations") 
     | otherwise 
     = do { traceTcS "simplifyApproxLoop" (vcat 
               [ ptext (sLit "Wanted = ") <+> ppr wanteds ])
          ; (unsolved_flats, unsolved_implics) <- solveWanteds emptyInert wanteds

	  ; let (extra_flats, thiner_unsolved_implics) 
                    = approximateImplications unsolved_implics
                unsolved 
                    = mkWantedConstraints unsolved_flats thiner_unsolved_implics

          ;-- If no new work was produced then we are done with simplifyApproxLoop
            if isEmptyBag extra_flats
            then do { traceTcS "simplifyApproxLoopRes" (vcat 
              		      [ ptext (sLit "Wanted = ") <+> ppr wanteds
                              , ptext (sLit "Result = ") <+> ppr unsolved_flats ])
                    ; return (unsolved_flats, unsolved_implics) }

            else -- Produced new flat work wanteds, go round the loop
                simplifyApproxLoop (n+1) (extra_flats `unionBags` unsolved)
          }     

approximateImplications :: Bag Implication -> (WantedConstraints, Bag Implication) 
-- (wc1, impls2) <- approximateImplications impls 
-- splits 'impls' into two parts
--    wc1:    a bag of constraints that do not mention any skolems 
--    impls2: a bag of *thiner* implication constraints
approximateImplications impls 
  = splitBag (do_implic emptyVarSet) impls
  where 
    ------------------
    do_wanted :: TcTyVarSet -> WantedConstraint
              -> (WantedConstraints, WantedConstraints) 
    do_wanted skols (WcImplic impl) 
        = let (fl_w, mb_impl) = do_implic skols impl 
          in (fl_w, mapBag WcImplic mb_impl)
    do_wanted skols wc@(WcEvVar wev) 
      | tyVarsOfWantedEvVar wev `disjointVarSet` skols = (unitBag wc, emptyBag) 
      | otherwise                                      = (emptyBag, unitBag wc) 
     
    ------------------
    do_implic :: TcTyVarSet -> Implication
              -> (WantedConstraints, Bag Implication)
    do_implic skols impl@(Implic { ic_skols = skols', ic_wanted = wanted })
     = (floatable_wanted, if isEmptyBag rest_wanted then emptyBag
                          else unitBag impl{ ic_wanted = rest_wanted } ) 
     where
        (floatable_wanted, rest_wanted) 
            = splitBag (do_wanted (skols `unionVarSet` skols')) wanted

    ------------------
    splitBag :: (a -> (WantedConstraints, Bag a))
             -> Bag a -> (WantedConstraints, Bag a)
    splitBag f bag = foldrBag do_one (emptyBag,emptyBag) bag
       where
         do_one x (b1,b2) 
           = (wcs `unionBags` b1, imps `unionBags` b2)
	   where
              (wcs, imps) = f x 
\end{code}
335

336
\begin{code}
337 338 339 340 341 342 343 344 345
growWantedEVs :: TyVarSet -> Bag WantedEvVar      -> TyVarSet -> TyVarSet
growWanteds   :: TyVarSet -> Bag WantedConstraint -> TyVarSet -> TyVarSet
growWanteds   gbl_tvs ws tvs
  | isEmptyBag ws = tvs
  | otherwise     = fixVarSet (\tvs -> foldrBag (growWanted   gbl_tvs) tvs ws) tvs
growWantedEVs gbl_tvs ws tvs 
  | isEmptyBag ws = tvs
  | otherwise     = fixVarSet (\tvs -> foldrBag (growWantedEV gbl_tvs) tvs ws) tvs

346
growEvVar    :: TyVarSet -> EvVar            -> TyVarSet -> TyVarSet
347 348 349 350
growWantedEV :: TyVarSet -> WantedEvVar      -> TyVarSet -> TyVarSet
growWanted   :: TyVarSet -> WantedConstraint -> TyVarSet -> TyVarSet
-- (growX gbls wanted tvs) grows a seed 'tvs' against the 
-- X-constraint 'wanted', nuking the 'gbls' at each stage
351 352

growEvVar gbl_tvs ev tvs
353
  = tvs `unionVarSet` (ev_tvs `minusVarSet` gbl_tvs)
354
  where
355 356 357
    ev_tvs = growPredTyVars (evVarPred ev) tvs

growWantedEV gbl_tvs wev tvs = growEvVar gbl_tvs (wantedEvVarToVar wev) tvs
358

359 360 361
growWanted gbl_tvs (WcEvVar wev) tvs
  = growWantedEV gbl_tvs wev tvs
growWanted gbl_tvs (WcImplic implic) tvs
362 363 364 365 366 367
  = foldrBag (growWanted inner_gbl_tvs) 
             (foldr (growEvVar inner_gbl_tvs) tvs (ic_given implic))
	     	    -- Must grow over inner givens too
             (ic_wanted implic)
  where
    inner_gbl_tvs = gbl_tvs `unionVarSet` ic_skols implic
368 369 370 371 372 373 374 375 376 377

--------------------
quantifyMe :: TyVarSet      -- Quantifying over these
	   -> WantedEvVar
	   -> Bool	    -- True <=> quantify over this wanted
quantifyMe qtvs wev
  | isIPPred pred = True  -- Note [Inheriting implicit parameters]
  | otherwise	  = tyVarsOfPred pred `intersectsVarSet` qtvs
  where
    pred = wantedEvVarPred wev
378 379

quantifyMeWC :: TyVarSet -> WantedConstraint -> Bool
380
-- False => we can *definitely* float the WantedConstraint out
381
quantifyMeWC qtvs (WcImplic implic)
382 383 384 385 386
  =  (tyVarsOfEvVars (ic_given implic) `intersectsVarSet` inner_qtvs)
  || anyBag (quantifyMeWC inner_qtvs) (ic_wanted implic)
  where
    inner_qtvs = qtvs `minusVarSet` ic_skols implic

387 388
quantifyMeWC qtvs (WcEvVar wev)
  = quantifyMe qtvs wev
389
\end{code}
390

391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408
Note [Avoid unecessary constraint simplification]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When inferring the type of a let-binding, with simplifyInfer,
try to avoid unnecessariliy simplifying class constraints.
Doing so aids sharing, but it also helps with delicate 
situations like
   instance C t => C [t] where ..
   f :: C [t] => ....
   f x = let g y = ...(constraint C [t])... 
         in ...
When inferring a type for 'g', we don't want to apply the
instance decl, because then we can't satisfy (C t).  So we
just notice that g isn't quantified over 't' and partition
the contraints before simplifying.

This only half-works, but then let-generalisation only half-works.


409 410
Note [Inheriting implicit parameters]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
411 412 413
Consider this:

	f x = (x::Int) + ?y
414

415 416 417
where f is *not* a top-level binding.
From the RHS of f we'll get the constraint (?y::Int).
There are two types we might infer for f:
418

419 420 421
	f :: Int -> Int

(so we get ?y from the context of f's definition), or
422 423 424

	f :: (?y::Int) => Int -> Int

425 426 427 428 429 430
At first you might think the first was better, becuase then
?y behaves like a free variable of the definition, rather than
having to be passed at each call site.  But of course, the WHOLE
IDEA is that ?y should be passed at each call site (that's what
dynamic binding means) so we'd better infer the second.

431 432
BOTTOM LINE: when *inferring types* you *must* quantify 
over implicit parameters. See the predicate isFreeWhenInferring.
433

434

435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
*********************************************************************************
*                                                                                 * 
*                             Superclasses                                        *
*                                                                                 *
***********************************************************************************

When constructing evidence for superclasses in an instance declaration, 
  * we MUST have the "self" dictionary available, but
  * we must NOT have its superclasses derived from "self"

Moreover, we must *completely* solve the constraints right now,
not wrap them in an implication constraint to solve later.  Why?
Because when that implication constraint is solved there may
be some unrelated other solved top-level constraints that
recursively depend on the superclass we are building. Consider
   class Ord a => C a where
   instance C [Int] where ...
Then we get
   dCListInt :: C [Int]
   dCListInt = MkC $cNum ...

   $cNum :: Ord [Int] -- The superclass
   $cNum = let self = dCListInt in <solve Ord [Int]>

Now, if there is some *other* top-level constraint solved
looking like
	foo :: Ord [Int]
        foo = scsel dCInt
we must not solve the (Ord [Int]) wanted from foo!!
464

465
\begin{code}
466 467 468 469 470 471 472
simplifySuperClass :: EvVar	-- The "self" dictionary
		   -> WantedConstraints
		   -> TcM ()
simplifySuperClass self wanteds
  = do { wanteds <- mapBagM zonkWanted wanteds
       ; loc <- getCtLoc NoScSkol
       ; (unsolved, ev_binds) 
473
             <- runTcS SimplCheck NoUntouchables $
474
         	do { can_self <- canGivens loc [self]
475
         	   ; let inert = foldlBag updInertSet emptyInert can_self
476 477 478 479 480 481
	 	     -- No need for solveInteract; we know it's inert

	 	   ; solveWanteds inert wanteds }

       ; ASSERT2( isEmptyBag ev_binds, ppr ev_binds )
         reportUnsolved unsolved }
482 483 484
\end{code}


485 486 487 488 489
*********************************************************************************
*                                                                                 * 
*                             RULES                                               *
*                                                                                 *
***********************************************************************************
490

491 492 493 494 495 496 497
Note [Simplifying RULE lhs constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
On the LHS of transformation rules we only simplify only equalitis,
but not dictionaries.  We want to keep dictionaries unsimplified, to
serve as the available stuff for the RHS of the rule.  We *do* want to
simplify equalities, however, to detect ill-typed rules that cannot be
applied.
498

499 500 501
Implementation: the TcSFlags carried by the TcSMonad controls the
amount of simplification, so simplifyRuleLhs just sets the flag
appropriately.
502

503 504 505 506 507 508 509 510 511 512
Example.  Consider the following left-hand side of a rule
	f (x == y) (y > z) = ...
If we typecheck this expression we get constraints
	d1 :: Ord a, d2 :: Eq a
We do NOT want to "simplify" to the LHS
	forall x::a, y::a, z::a, d1::Ord a.
	  f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
Instead we want	
	forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
	  f ((==) d2 x y) ((>) d1 y z) = ...
513

514
Here is another example:
515 516
	fromIntegral :: (Integral a, Num b) => a -> b
	{-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
517 518
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
519
	forall dIntegralInt.
520
	   fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
521
because the scsel will mess up RULE matching.  Instead we want
522
	forall dIntegralInt, dNumInt.
523
	  fromIntegral Int Int dIntegralInt dNumInt = id Int
524

525 526 527 528 529 530 531
Even if we have 
	g (x == y) (y == z) = ..
where the two dictionaries are *identical*, we do NOT WANT
	forall x::a, y::a, z::a, d1::Eq a
	  f ((==) d1 x y) ((>) d1 y z) = ...
because that will only match if the dict args are (visibly) equal.
Instead we want to quantify over the dictionaries separately.
532

533 534
In short, simplifyRuleLhs must *only* squash equalities, leaving
all dicts unchanged, with absolutely no sharing.  
535

536 537 538 539 540 541 542 543 544
HOWEVER, under a nested implication things are different
Consider
  f :: (forall a. Eq a => a->a) -> Bool -> ...
  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
       f b True = ...
    #=}
Here we *must* solve the wanted (Eq a) from the given (Eq a)
resulting from skolemising the agument type of g.  So we 
revert to SimplCheck when going under an implication.  
545 546

\begin{code}
547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581
simplifyRule :: RuleName 
             -> [TcTyVar]		-- Explicit skolems
             -> WantedConstraints	-- Constraints from LHS
             -> WantedConstraints	-- Constraints from RHS
             -> TcM ([EvVar], 		-- LHS dicts
                     TcEvBinds,		-- Evidence for LHS
                     TcEvBinds)		-- Evidence for RHS
-- See Note [Simplifying RULE lhs constraints]
simplifyRule name tv_bndrs lhs_wanted rhs_wanted
  = do { zonked_lhs <- mapBagM zonkWanted lhs_wanted
       ; (lhs_residual, lhs_binds) <- simplifyAsMuchAsPossible SimplRuleLhs zonked_lhs

       -- Don't quantify over equalities (judgement call here)
       ; let (eqs, dicts) = partitionBag (isEqPred . wantedEvVarPred) lhs_residual
             lhs_dicts    = map wantedEvVarToVar (bagToList dicts)  
	     	     	       	 -- Dicts and implicit parameters
       ; reportUnsolvedWantedEvVars eqs

	     -- Notice that we simplify the RHS with only the explicitly
	     -- introduced skolems, allowing the RHS to constrain any 
	     -- unification variables.
	     -- Then, and only then, we call zonkQuantifiedTypeVariables
	     -- Example   foo :: Ord a => a -> a
	     --		  foo_spec :: Int -> Int
	     --		  {-# RULE "foo"  foo = foo_spec #-}
	     --	    Here, it's the RHS that fixes the type variable

	     -- So we don't want to make untouchable the type
	     -- variables in the envt of the RHS, because they include
	     -- the template variables of the RULE

	     -- Hence the rather painful ad-hoc treatement here
       ; rhs_binds_var@(EvBindsVar evb_ref _)  <- newTcEvBinds
       ; loc        <- getCtLoc (RuleSkol name)
       ; rhs_binds1 <- simplifyCheck SimplCheck $ unitBag $ WcImplic $ 
582
             Implic { ic_untch = NoUntouchables
583 584 585 586 587 588 589 590 591 592 593 594
             	    , ic_env = emptyNameEnv
             	    , ic_skols = mkVarSet tv_bndrs
             	    , ic_scoped = panic "emitImplication"
             	    , ic_given = lhs_dicts
             	    , ic_wanted = rhs_wanted
             	    , ic_binds = rhs_binds_var
             	    , ic_loc = loc }
       ; rhs_binds2 <- readTcRef evb_ref

       ; return ( lhs_dicts
                , EvBinds lhs_binds 
                , EvBinds (rhs_binds1 `unionBags` evBindMapBinds rhs_binds2)) }
595 596 597
\end{code}


598 599 600 601 602
*********************************************************************************
*                                                                                 * 
*                                 Main Simplifier                                 *
*                                                                                 *
***********************************************************************************
603 604

\begin{code}
605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625
simplifyCheck :: SimplContext
	      -> WantedConstraints	-- Wanted
              -> TcM (Bag EvBind)
-- Solve a single, top-level implication constraint
-- e.g. typically one created from a top-level type signature
-- 	    f :: forall a. [a] -> [a]
--          f x = rhs
-- We do this even if the function has no polymorphism:
--    	    g :: Int -> Int

--          g y = rhs
-- (whereas for *nested* bindings we would not create
--  an implication constraint for g at all.)
--
-- Fails if can't solve something in the input wanteds
simplifyCheck ctxt wanteds
  = do { wanteds <- mapBagM zonkWanted wanteds

       ; traceTc "simplifyCheck {" (vcat
             [ ptext (sLit "wanted =") <+> ppr wanteds ])

626
       ; (unsolved, ev_binds) <- runTcS ctxt NoUntouchables $
627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650
                                 solveWanteds emptyInert wanteds

       ; traceTc "simplifyCheck }" $
             ptext (sLit "unsolved =") <+> ppr unsolved

       ; reportUnsolved unsolved

       ; return ev_binds }

----------------
solveWanteds :: InertSet	       -- Given 
             -> WantedConstraints      -- Wanted
             -> TcS (CanonicalCts,     -- Unsolved flats
                     Bag Implication)  -- Unsolved implications
-- solveWanteds iterates when it is able to float equalities
-- out of one or more of the implications 
solveWanteds inert wanteds
  = do { let (flat_wanteds, implic_wanteds) = splitWanteds wanteds
       ; can_flats <- canWanteds $ bagToList flat_wanteds
       ; traceTcS "solveWanteds {" $
                 vcat [ text "wanteds =" <+> ppr wanteds
                      , text "inert =" <+> ppr inert ]
       ; (unsolved_flats, unsolved_implics) 
               <- simpl_loop 1 can_flats implic_wanteds
651
       ; bb <- getTcEvBindsBag 
652 653 654
       ; traceTcS "solveWanteds }" $
                 vcat [ text "wanteds =" <+> ppr wanteds
                      , text "unsolved_flats =" <+> ppr unsolved_flats
655 656 657
                      , text "unsolved_implics =" <+> ppr unsolved_implics 
                      , text "current evbinds =" <+> vcat (map ppr (varEnvElts bb))
                      ] 
658
       ; return (unsolved_flats, unsolved_implics)  }
659
  where
660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714
    simpl_loop :: Int 
               -> CanonicalCts	-- May inlude givens (in the recursive call)
               -> Bag Implication
               -> TcS (CanonicalCts, Bag Implication)
    simpl_loop n can_ws implics
      | n>10
      = trace "solveWanteds: loop" $	-- Always bleat
        do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
           ; return (can_ws, implics) }

      | otherwise
      = do { inert1 <- solveInteract inert can_ws
           ; let (inert2, unsolved_flats) = extractUnsolved inert1

           ; traceTcS "solveWanteds/done flats"  $ 
                 vcat [ text "inerts =" <+> ppr inert2
                      , text "unsolved =" <+> ppr unsolved_flats ]

                   -- See Note [Preparing inert set for implications]
           ; inert_for_implics <- solveInteract inert2 (makeGivens unsolved_flats)
           ; (implic_eqs, unsolved_implics) 
                <- flatMapBagPairM (solveImplication inert_for_implics) implics

		-- Apply defaulting rules if and only if there 
		-- no floated equalities.  If there are, they may
		-- solve the remaining wanteds, so don't do defaulting.
           ; final_eqs <- if not (isEmptyBag implic_eqs)
			  then return implic_eqs
                          else applyDefaultingRules inert2 unsolved_flats
	        -- default_eqs are *givens*, so simpl_loop may 
		-- recurse with givens in the argument

           ; if isEmptyBag final_eqs then
                 return (unsolved_flats, unsolved_implics)
             else 
                 do { traceTcS ("solveWanteds iteration " ++ show n) $ vcat
                        [ text "floated_unsolved_eqs =" <+> ppr final_eqs
                        , text "unsolved_implics = " <+> ppr unsolved_implics ]
                    ; simpl_loop (n+1) 
                             	 (unsolved_flats `unionBags` final_eqs)
                             	 unsolved_implics 
           }        }

solveImplication :: InertSet     -- Given 
                    -> Implication  -- Wanted 
                    -> TcS (CanonicalCts,	-- Unsolved unification var = type
                            Bag Implication) 	-- Unsolved rest (always empty or singleton)
-- Returns: 
--  1. A bag of floatable wanted constraints, not mentioning any skolems, 
--     that are of the form unification var = type
-- 
--  2. Maybe a unsolved implication, empty if entirely solved! 
-- 
-- Precondition: everything is zonked by now
solveImplication inert 
715 716 717 718
     imp@(Implic { ic_untch  = untch 
                 , ic_binds  = ev_binds
                 , ic_skols  = skols 
                 , ic_given  = givens
719
                 , ic_wanted = wanteds
720
                 , ic_loc    = loc })
721
  = nestImplicTcS ev_binds untch $
722 723 724 725
    recoverTcS (return (emptyBag, emptyBag)) $
       -- Recover from nested failures.  Even the top level is
       -- just a bunch of implications, so failing at the first
       -- one is bad
726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752
    do { traceTcS "solveImplication {" (ppr imp) 

         -- Solve flat givens
       ; can_givens  <- canGivens loc givens
       ; given_inert <- solveInteract inert can_givens

         -- Simplify the wanteds
       ; (unsolved_flats, unsolved_implics) <- solveWanteds given_inert wanteds

       ; let (res_flat_free, res_flat_bound) 
                      = floatEqualities skols givens unsolved_flats
             unsolved = mkWantedConstraints res_flat_bound unsolved_implics

       ; traceTcS "solveImplication end }" $ vcat
             [ text "res_flat_free =" <+> ppr res_flat_free
             , text "res_flat_bound =" <+> ppr res_flat_bound
             , text "unsolved_implics =" <+> ppr unsolved_implics ]

       ; let res_bag | isEmptyBag unsolved = emptyBag
                     | otherwise           = unitBag (imp { ic_wanted  = unsolved })

       ; return (res_flat_free, res_bag) }

floatEqualities :: TcTyVarSet -> [EvVar]
                -> CanonicalCts -> (CanonicalCts, CanonicalCts)
floatEqualities skols can_given wanteds
  | hasEqualities can_given = (emptyBag, wanteds)
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
753
  | otherwise               = partitionBag is_floatable wanteds
754
  where
755 756 757 758 759
    is_floatable :: CanonicalCt -> Bool
    is_floatable (CTyEqCan { cc_tyvar = tv, cc_rhs = ty })
      | isMetaTyVar tv || isMetaTyVarTy ty
      = skols `disjointVarSet` (extendVarSet (tyVarsOfType ty) tv)
    is_floatable _ = False
760
\end{code}
761

762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789
Note [Preparing inert set for implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before solving the nested implications, we convert any unsolved flat wanteds
to givens, and add them to the inert set.  Reasons:
  a) In checking mode, suppresses unnecessary errors.  We already have 
     on unsolved-wanted error; adding it to the givens prevents any 
     consequential errors from showing uop
  b) More importantly, in inference mode, we are going to quantify over this
     constraint, and we *don't* want to quantify over any constraints that
     are deducible from it.

The unsolved wanteds are *canonical* but they may not be *inert*,
because when made into a given they might interact with other givens.
Hence the call to solveInteract.  Example:

 Original inert set = (d :_g D a) /\ (co :_w  a ~ [beta]) 

We were not able to solve (a ~w [beta]) but we can't just assume it as
given because the resulting set is not inert. Hence we have to do a
'solveInteract' step first

*********************************************************************************
*                                                                               * 
*                          Defaulting and disamgiguation                        *
*                                                                               *
*********************************************************************************

Basic plan behind applyDefaulting rules: 
790
 
791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816
 Step 1:  
    Split wanteds into defaultable groups, `groups' and the rest `rest_wanted' 
    For each defaultable group, do: 
      For each possible substitution for [alpha |-> tau] where `alpha' is the 
      group's variable, do: 
        1) Make up new TcEvBinds
        2) Extend TcS with (groupVariable 
        3) given_inert <- solveOne inert (given : a ~ tau) 
        4) (final_inert,unsolved) <- solveWanted (given_inert) (group_constraints)
        5) if unsolved == empty then 
                 sneakyUnify a |-> tau 
                 write the evidence bins
                 return (final_inert ++ group_constraints,[]) 
                      -- will contain the info (alpha |-> tau)!!
                 goto next defaultable group 
           if unsolved <> empty then 
                 throw away evidence binds
                 try next substitution 
     If you've run out of substitutions for this group, too bad, you failed 
                 return (inert,group) 
                 goto next defaultable group
 
 Step 2: 
   Collect all the (canonical-cts, wanteds) gathered this way. 
   - Do a solveGiven over the canonical-cts to make sure they are inert 
------------------------------------------------------------------------------------------
817

818 819

\begin{code}
820 821 822 823 824 825 826 827 828
applyDefaultingRules :: InertSet
                     -> CanonicalCts 	-- All wanteds
                     -> TcS CanonicalCts
-- Return some *extra* givens, which express the 
-- type-class-default choice

applyDefaultingRules inert wanteds
  | isEmptyBag wanteds 
  = return emptyBag
829
  | otherwise
830
  = do { untch <- getUntouchables
831
       ; tv_cts <- mapM (defaultTyVar untch) $
832
                   varSetElems (tyVarsOfCDicts wanteds) 
833 834 835

       ; info@(_, default_tys, _) <- getDefaultInfo
       ; let groups = findDefaultableGroups info untch wanteds
836
       ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
837 838 839 840 841 842 843

       ; traceTcS "deflt2" (vcat [ text "Tyvar defaults =" <+> ppr tv_cts
                                 , text "Type defaults =" <+> ppr deflt_cts])

       ; return (unionManyBags deflt_cts `andCCan` unionManyBags tv_cts) }

------------------
844
defaultTyVar :: Untouchables -> TcTyVar -> TcS CanonicalCts
845 846 847 848 849 850 851 852
-- defaultTyVar is used on any un-instantiated meta type variables to
-- default the kind of ? and ?? etc to *.  This is important to ensure
-- that instance declarations match.  For example consider
--	instance Show (a->b)
--	foo x = show (\_ -> True)
-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
-- and that won't match the typeKind (*) in the instance decl.  
-- See test tc217.
853
--
854 855 856 857 858 859
-- We look only at touchable type variables. No further constraints
-- are going to affect these type variables, so it's time to do it by
-- hand.  However we aren't ready to default them fully to () or
-- whatever, because the type-class defaulting rules have yet to run.

defaultTyVar untch the_tv 
860
  | isTouchableMetaTyVar_InRange untch the_tv
861
  , not (k `eqKind` default_k)
862
  = do { (ev, better_ty) <- TcSMonad.newKindConstraint the_tv default_k
863 864
       ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
       	     	   -- 'DefaultOrigin' is strictly the declaration, but it's convenient
865 866 867 868 869 870 871 872
             wanted_eq  = CTyEqCan { cc_id     = ev
                                   , cc_flavor = Wanted loc
                                   , cc_tyvar  = the_tv
           	                   , cc_rhs    = better_ty }
       ; return (unitBag wanted_eq) }

  | otherwise            
  = return emptyCCan	 -- The common case
873
  where
874 875 876 877 878 879 880 881 882
    k = tyVarKind the_tv
    default_k = defaultKind k


----------------
findDefaultableGroups 
    :: ( SimplContext 
       , [Type]
       , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
883
    -> Untouchables	-- Untouchable
884 885 886 887 888 889 890
    -> CanonicalCts	-- Unsolved
    -> [[(CanonicalCt,TcTyVar)]]
findDefaultableGroups (ctxt, default_tys, (ovl_strings, extended_defaults)) 
                      untch wanteds
  | not (performDefaulting ctxt) = []
  | null default_tys             = []
  | otherwise = filter is_defaultable_group (equivClasses cmp_tv unaries)
891
  where 
892
    unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
893
    non_unaries :: [CanonicalCt]             -- and *other* constraints
894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909
    
    (unaries, non_unaries) = partitionWith find_unary (bagToList wanteds)
        -- Finds unary type-class constraints
    find_unary cc@(CDictCan { cc_tyargs = [ty] })
        | Just tv <- tcGetTyVar_maybe ty
        = Left (cc, tv)
    find_unary cc = Right cc  -- Non unary or non dictionary 

    bad_tvs :: TcTyVarSet  -- TyVars mentioned by non-unaries 
    bad_tvs = foldr (unionVarSet . tyVarsOfCanonical) emptyVarSet non_unaries 

    cmp_tv (_,tv1) (_,tv2) = tv1 `compare` tv2

    is_defaultable_group ds@((_,tv):_)
        = isTyConableTyVar tv	-- Note [Avoiding spurious errors]
        && not (tv `elemVarSet` bad_tvs)
910
        && isTouchableMetaTyVar_InRange untch tv 
911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936
        && defaultable_classes [cc_class cc | (cc,_) <- ds]
    is_defaultable_group [] = panic "defaultable_group"

    defaultable_classes clss 
        | extended_defaults = any isInteractiveClass clss
        | otherwise         = all is_std_class clss && (any is_num_class clss)

    -- In interactive mode, or with -XExtendedDefaultRules,
    -- we default Show a to Show () to avoid graututious errors on "show []"
    isInteractiveClass cls 
        = is_num_class cls || (classKey cls `elem` [showClassKey, eqClassKey, ordClassKey])

    is_num_class cls = isNumericClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
    -- is_num_class adds IsString to the standard numeric classes, 
    -- when -foverloaded-strings is enabled

    is_std_class cls = isStandardClass cls || (ovl_strings && (cls `hasKey` isStringClassKey))
    -- Similarly is_std_class

------------------------------
disambigGroup :: [Type]                    -- The default types 
              -> InertSet                  -- Given inert 
              -> [(CanonicalCt, TcTyVar)]  -- All classes of the form (C a)
	      	 		           --  sharing same type variable
              -> TcS CanonicalCts

937
disambigGroup [] _inert _grp 
938
  = return emptyBag
939
disambigGroup (default_ty:default_tys) inert group
940 941 942 943 944 945 946 947 948
  = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
       ; ev <- newGivOrDerCoVar (mkTyVarTy the_tv) default_ty default_ty -- Refl 
		       	 -- We know this equality is canonical,
			 -- so we directly construct it as such
       ; let given_eq = CTyEqCan { cc_id     = ev
                                 , cc_flavor = mkGivenFlavor (cc_flavor the_ct) UnkSkol
                               	 , cc_tyvar  = the_tv
           	                 , cc_rhs    = default_ty }

949
       ; success <- tryTcS $ 
950 951 952 953 954 955 956 957 958 959 960 961 962
           	    do { given_inert <- solveOne inert given_eq
           	       ; final_inert <- solveInteract given_inert (listToBag wanteds)
           	       ; let (_, unsolved) = extractUnsolved final_inert
           	       ; return (isEmptyBag unsolved) }

       ; case success of
           True  ->   -- Success: record the type variable binding, and return
                    do { setWantedTyBind the_tv default_ty
		       ; wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
		       ; traceTcS "disambigGoup succeeded" (ppr default_ty)
                       ; return (unitBag given_eq) }
           False ->    -- Failure: try with the next type
		    do { traceTcS "disambigGoup succeeded" (ppr default_ty)
963
                       ; disambigGroup default_tys inert group } }
964
  where
965 966 967
    ((the_ct,the_tv):_) = group
    wanteds = map fst group
    wanted_ev_vars = map deCanonicaliseWanted wanteds
968 969
\end{code}

970 971 972 973 974 975 976 977 978 979 980 981
Note [Avoiding spurious errors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When doing the unification for defaulting, we check for skolem
type variables, and simply don't default them.  For example:
   f = (*)	-- Monomorphic
   g :: Num a => a -> a
   g x = f x x
Here, we get a complaint when checking the type signature for g,
that g isn't polymorphic enough; but then we get another one when
dealing with the (Num a) context arising from f's definition;
we try to unify a with Int (to default it), but find that it's
already been unified with the rigid variable from g's type sig
982

983