TcSimplify.lhs 54 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
import TcErrors
13
import TcMType
14 15 16 17
import TcType 
import TcSMonad 
import TcInteract
import Inst
18
import Var
19
import VarSet
20 21
import VarEnv 
import TypeRep
22

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
import Control.Monad    ( unless )
36 37 38
\end{code}


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

45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68
\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}
69

70 71 72 73 74 75
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.
76

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

85

86 87 88 89 90
*********************************************************************************
*                                                                                 * 
*                            Deriving
*                                                                                 *
***********************************************************************************
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 122
\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}
123

124 125 126 127 128 129 130
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.
131

132 133 134
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)
135

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

139 140 141 142
	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.  
143

144 145 146
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.
147

148 149
So for now we simply require that the derived instance context
should have only type-variable constraints.
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 179
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
*                                                                                 *
***********************************************************************************
180

181 182 183 184 185 186 187 188 189 190
\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
191
  = do { zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
192 193 194
       ; gbl_tvs        <- tcGetGlobalTyVars	     -- Already zonked
       ; qtvs <- zonkQuantifiedTyVars (varSetElems (zonked_tau_tvs `minusVarSet` gbl_tvs))
       ; return (qtvs, [], emptyTcEvBinds) }
195

196 197 198 199 200 201 202 203
  | 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
             ]

204 205 206 207 208 209
	     -- 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
210 211
       ; let proto_qtvs = growWanteds gbl_tvs zonked_wanted $
                          zonked_tau_tvs `minusVarSet` gbl_tvs
212 213
             (perhaps_bound, surely_free) 
                  = partitionBag (quantifyMeWC proto_qtvs) zonked_wanted
214
      
215
       ; emitConstraints surely_free
216 217 218 219
       ; traceTc "sinf"  $ vcat
             [ ptext (sLit "perhaps_bound =") <+> ppr perhaps_bound
             , ptext (sLit "surely_free   =") <+> ppr surely_free
             ]
220 221 222 223

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

225 226
	      -- Sigh: must re-zonk because because simplifyAsMuchAsPossible
	      --       may have done some unification
227
       ; gbl_tvs <- tcGetGlobalTyVars
228
       ; zonked_tau_tvs <- zonkTcTyVarsAndFV tau_tvs
229
       ; zonked_simples <- mapBagM zonkWantedEvVar simplified_perhaps_bound
230 231 232 233 234 235 236
       ; 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)
237 238 239 240

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

       -- Turn the quantified meta-type variables into real type variables 
       ; emitConstraints (mapBag WcEvVar free)
247
       ; qtvs_to_return <- zonkQuantifiedTyVars (varSetElems final_qtvs) 
248 249 250 251 252 253 254 255 256
       ; 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
257
  = do { let untch = NoUntouchables
258 259 260
	     	 -- We allow ourselves to unify environment 
		 -- variables; hence *no untouchables*

261
       ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds) 
262 263 264 265
           <- runTcS ctxt untch $
              simplifyApproxLoop 0 wanteds

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

268
       ; return (unsolved_flats, ev_binds) }
269

270 271
  where 
    simplifyApproxLoop :: Int -> WantedConstraints
272
                       -> TcS (Bag WantedEvVar, Bag Implication)
273 274 275 276 277 278 279 280 281 282 283
    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 
284 285
                    = Bag.mapBag WcEvVar unsolved_flats `unionBags` 
                                    Bag.mapBag WcImplic thiner_unsolved_implics
286

287
          ; -- If no new work was produced then we are done with simplifyApproxLoop
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 335
            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}
336

337
\begin{code}
338 339 340 341 342 343 344 345 346
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

347
growEvVar    :: TyVarSet -> EvVar            -> TyVarSet -> TyVarSet
348 349 350 351
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
352 353

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

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

360 361 362
growWanted gbl_tvs (WcEvVar wev) tvs
  = growWantedEV gbl_tvs wev tvs
growWanted gbl_tvs (WcImplic implic) tvs
363 364 365 366 367 368
  = 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
369 370 371 372 373 374 375 376 377 378

--------------------
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
379 380

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

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

392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409
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.


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

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

416 417 418
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:
419

420 421 422
	f :: Int -> Int

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

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

426 427 428 429 430 431
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.

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

435

436 437 438 439 440 441 442
*********************************************************************************
*                                                                                 * 
*                             Superclasses                                        *
*                                                                                 *
***********************************************************************************

When constructing evidence for superclasses in an instance declaration, 
443
  * we MUST have the "self" dictionary available
444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462

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
463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
we must not solve the (Ord [Int]) wanted from foo!

Note [Dependencies in self dictionaries] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Moreover, notice that when solving for a superclass, we record the dependency of 
self on the superclass. This is because this dependency is not evident in the 
EvBind of the self dictionary, which only involves a call to a DFun. Example: 

class A a => C a 
instance B a => C a 

When we check the instance declaration, we pass in a self dictionary that is merely
     self = dfun b
But we will be asked to solve that from: 
   [Given] d : B a 
   [Derived] self : C a 
We can show: 
   [Wanted] sc : A a
The problem is that self *depends* on the sc variable, but that is not apparent in 
the binding self = dfun b. So we record the extra dependency, using the evidence bind: 
   EvBind self (EvDFunApp dfun [b] [b,sc])
It is these dependencies that are the ''true'' dependencies in an EvDFunApp, and those 
that we must chase in function isGoodRecEv (in TcSMonad) 
487

488
\begin{code}
489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513
simplifySuperClass :: [TyVar]
                   -> [EvVar]          -- givens
                   -> EvVar            -- the superclass we must solve for
                   -> EvBind           -- the 'self' evidence bind 
                   -> TcM TcEvBinds
-- Post:  
--   ev_binds <- simplifySuperClasses tvs inst_givens sc_dict self_ev_bind
-- Then: 
--    1) ev_binds already contains self_ev_bind
--    2) if successful then ev_binds contains binding for
--       the wanted superclass, sc_dict
simplifySuperClass tvs inst_givens sc_dict (EvBind self_dict self_ev)
  = do { giv_loc      <- getCtLoc InstSkol  -- For the inst_givens
       ; want_loc     <- getCtLoc ScOrigin  -- As wanted/derived (for the superclass and self)
       ; lcl_env      <- getLclTypeEnv

       -- Record the dependency of self_dict to sc_dict, see Note [Dependencies in self dictionaries]
       ; let wanted = unitBag $ WcEvVar $ WantedEvVar sc_dict want_loc
             self_ev_with_dep
               = case self_ev of 
                   EvDFunApp df tys insts deps -> EvDFunApp df tys insts (sc_dict:deps)
                   _ -> panic "Self-dictionary not EvDFunApp!"

       -- And solve for it
       ; ((unsolved_flats, unsolved_implics), frozen_errors, ev_binds)
514
             <- runTcS SimplCheck NoUntouchables $
515 516 517 518 519 520
                do {   -- Record a binding for self_dict that *depends on sc_dict*
                       -- And canonicalise self_dict (which adds its superclasses)
                       -- with a Derived origin, which in turn triggers the
                       -- goodRecEv recursive-evidence check
                   ; setEvBind self_dict self_ev_with_dep
                       -- The rest is just like solveImplication
521 522 523 524
                   ; let cts = mapBag (\d -> (Given giv_loc, d)) (listToBag inst_givens)
                                          `snocBag` (Derived want_loc DerSelf, self_dict)
                   ; inert           <- solveInteract emptyInert cts
                                        
525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541
                   ; solveWanteds inert wanted }

       -- For error reporting, conjure up a fake implication,
       -- so that we get decent error messages
       ; let implic = Implic { ic_untch  = NoUntouchables
                             , ic_env    = lcl_env
                             , ic_skols  = mkVarSet tvs
                             , ic_given  = inst_givens
                             , ic_wanted = mapBag WcEvVar unsolved_flats
                             , ic_scoped = panic "super1"
                             , ic_binds  = panic "super2"
                             , ic_loc    = giv_loc }
        ; ASSERT (isEmptyBag unsolved_implics) -- Impossible to have any implications!
          unless (isEmptyBag unsolved_flats) $
          reportUnsolved (emptyBag, unitBag implic) frozen_errors

        ; return (EvBinds ev_binds) }
542 543 544
\end{code}


545 546 547 548 549
*********************************************************************************
*                                                                                 * 
*                             RULES                                               *
*                                                                                 *
***********************************************************************************
550

551 552 553 554 555 556 557
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.
558

559 560 561
Implementation: the TcSFlags carried by the TcSMonad controls the
amount of simplification, so simplifyRuleLhs just sets the flag
appropriately.
562

563 564 565 566 567 568 569 570 571 572
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) = ...
573

574
Here is another example:
575 576
	fromIntegral :: (Integral a, Num b) => a -> b
	{-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
577 578
In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
we *dont* want to get
579
	forall dIntegralInt.
580
	   fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
581
because the scsel will mess up RULE matching.  Instead we want
582
	forall dIntegralInt, dNumInt.
583
	  fromIntegral Int Int dIntegralInt dNumInt = id Int
584

585 586 587 588 589 590 591
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.
592

593 594
In short, simplifyRuleLhs must *only* squash equalities, leaving
all dicts unchanged, with absolutely no sharing.  
595

596 597 598 599 600 601 602 603 604
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.  
605 606

\begin{code}
607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641
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 $ 
642
             Implic { ic_untch = NoUntouchables
643 644 645 646 647 648 649 650 651 652 653 654
             	    , 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)) }
655 656 657
\end{code}


658 659 660 661 662
*********************************************************************************
*                                                                                 * 
*                                 Main Simplifier                                 *
*                                                                                 *
***********************************************************************************
663 664

\begin{code}
665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685
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 ])

686 687
       ; (unsolved, frozen_errors, ev_binds) 
           <- runTcS ctxt NoUntouchables $ solveWanteds emptyInert wanteds
688 689 690 691

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

692
       ; reportUnsolved unsolved frozen_errors
693 694 695 696

       ; return ev_binds }

----------------
697 698 699 700 701
solveWanteds :: InertSet	      -- Given 
             -> WantedConstraints     -- Wanted
             -> TcS (Bag WantedEvVar, -- Unsolved constraints, but unflattened, this is why 
                                      -- they are WantedConstraints and not CanonicalCts
                     Bag Implication) -- Unsolved implications
702 703 704 705 706 707 708 709
-- 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
       ; traceTcS "solveWanteds {" $
                 vcat [ text "wanteds =" <+> ppr wanteds
                      , text "inert =" <+> ppr inert ]
       ; (unsolved_flats, unsolved_implics) 
710
               <- simpl_loop 1 inert flat_wanteds implic_wanteds
711 712
       ; bb <- getTcEvBindsBag
       ; tb <- getTcSTyBindsMap
713
       ; traceTcS "solveWanteds }" $
714
                 vcat [ text "unsolved_flats   =" <+> ppr unsolved_flats
715
                      , text "unsolved_implics =" <+> ppr unsolved_implics 
716 717 718 719 720 721 722
                      , text "current evbinds  =" <+> vcat (map ppr (varEnvElts bb))
                      , text "current tybinds  =" <+> vcat (map ppr (varEnvElts tb))
                      ]

       ; solveCTyFunEqs unsolved_flats unsolved_implics
                -- See Note [Solving Family Equations]
       }
723
  where
724
    simpl_loop :: Int 
725
               -> InertSet 
726
               -> Bag WantedEvVar
727 728
               -> Bag Implication
               -> TcS (CanonicalCts, Bag Implication)
729
    simpl_loop n inert work_items implics
730
      | n>10
731
      = trace "solveWanteds: loop" $	                -- Always bleat
732
        do { traceTcS "solveWanteds: loop" (ppr inert)  -- Bleat more informatively
733 734 735 736 737 738 739

             -- We don't want to call the canonicalizer on those wanted ev vars
             -- so try one last time to solveInteract them 
           ; inert1 <- solveInteract inert $ 
                       mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc, ev)) work_items
           ; let (_, unsolved_cans) = extractUnsolved inert1
           ; return (unsolved_cans, implics) }
740 741

      | otherwise
742 743
      = do { traceTcS "solveWanteds: simpl_loop start {" $
                 vcat [ text "n =" <+> ppr n
744
                      , text "work_items =" <+> ppr work_items
745 746
                      , text "implics =" <+> ppr implics
                      , text "inert =" <+> ppr inert ]
747 748 749 750 751
           ; inert1 <- solveInteract inert $ 
                       mapBag (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) work_items
           ; let (inert2, unsolved_cans) = extractUnsolved inert1
                 unsolved_wevvars 
                     = mapBag (\ct -> WantedEvVar (cc_id ct) (getWantedLoc ct)) unsolved_cans
752

753 754 755
           -- NB: Importantly, inerts2 may contain *more* givens than inert 
           -- because of having solved equalities from can_ws 
           ; traceTcS "solveWanteds: done flats"  $
756
                 vcat [ text "inerts =" <+> ppr inert2
757
                      , text "unsolved =" <+> ppr unsolved_cans ]
758

759 760
                -- Go inside each implication
           ; (implic_eqs, unsolved_implics) 
761
               <- solveNestedImplications inert2 unsolved_wevvars implics
762 763

                -- Apply defaulting rules if and only if there
764 765 766 767
		-- 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
768
                          else applyDefaultingRules inert2 unsolved_cans
769

770 771
           ; traceTcS "solveWanteds: simpl_loop end }" $
                 vcat [ text "final_eqs =" <+> ppr final_eqs
772
                      , text "unsolved_flats =" <+> ppr unsolved_cans
773 774
                      , text "unsolved_implics =" <+> ppr unsolved_implics ]

775
           ; if isEmptyBag final_eqs then
776
                 return (unsolved_cans, unsolved_implics)
777
             else 
778 779
                 simpl_loop (n+1) inert2 -- final_eqs are just some WantedEvVars
                            (final_eqs `unionBags` unsolved_wevvars) unsolved_implics
780 781
                       -- Important: reiterate with inert2, not plainly inert
                       -- because inert2 may contain more givens, as the result of solving
782
                       -- some wanteds in the incoming can_ws
783 784
           }

785
solveNestedImplications :: InertSet -> Bag WantedEvVar -> Bag Implication
786 787 788 789 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
                        -> TcS (Bag WantedEvVar, Bag Implication)
solveNestedImplications inerts unsolved implics
  | isEmptyBag implics
  = return (emptyBag, emptyBag)
  | otherwise 
  = do { -- See Note [Preparing inert set for implications]
         traceTcS "solveWanteds: preparing inerts for implications {"  empty
       ; inert_for_implics <- solveInteract inerts (makeGivens unsolved)
       ; traceTcS "}" empty

       ; traceTcS "solveWanteds: doing nested implications {" $
         vcat [ text "inerts_for_implics =" <+> ppr inert_for_implics
              , text "implics =" <+> ppr implics ]

       ; let tcs_untouchables = filterVarSet isFlexiTcsTv $
                                tyVarsOfInert inert_for_implics
             -- See Note [Extra TcsTv untouchables]
       ; (implic_eqs, unsolved_implics)
           <- flatMapBagPairM (solveImplication tcs_untouchables inert_for_implics) implics

       ; traceTcS "solveWanteds: done nested implications }" $
                  vcat [ text "implic_eqs ="       <+> ppr implic_eqs
                       , text "unsolved_implics =" <+> ppr unsolved_implics ]

       ; return (implic_eqs, unsolved_implics) }

solveImplication :: TcTyVarSet            -- Untouchable TcS unification variables
                 -> InertSet              -- Given
                 -> Implication           -- Wanted
                 -> TcS (Bag WantedEvVar, -- Unsolved unification var = type
                         Bag Implication) -- Unsolved rest (always empty or singleton)
817 818 819 820 821 822 823
-- 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
824
solveImplication tcs_untouchables inert
825 826 827 828
     imp@(Implic { ic_untch  = untch 
                 , ic_binds  = ev_binds
                 , ic_skols  = skols 
                 , ic_given  = givens
829
                 , ic_wanted = wanteds
830
                 , ic_loc    = loc })
831
  = nestImplicTcS ev_binds (untch, tcs_untouchables) $
832 833 834 835
    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
836 837 838
    do { traceTcS "solveImplication {" (ppr imp) 

         -- Solve flat givens
839 840 841 842
--       ; can_givens  <- canGivens loc givens
--       ; let given_fl = Given loc
       ; given_inert <- solveInteract inert $ 
                        mapBag (\c -> (Given loc,c)) (listToBag givens)
843 844 845 846 847 848

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

       ; let (res_flat_free, res_flat_bound) 
                      = floatEqualities skols givens unsolved_flats
849 850
             unsolved = Bag.mapBag WcEvVar res_flat_bound `unionBags`
                              Bag.mapBag WcImplic unsolved_implics
851 852 853 854 855 856 857 858 859 860 861

       ; 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) }

862 863 864 865
floatEqualities :: TcTyVarSet -> [EvVar] 
                -> Bag WantedEvVar -> (Bag WantedEvVar, Bag WantedEvVar)
                   -- The CanonicalCts will be floated out to be used later, whereas
                   -- the remaining WantedEvVars will remain inside the implication. 
866 867
floatEqualities skols can_given wanteds
  | hasEqualities can_given = (emptyBag, wanteds)
868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900
          -- Note [Float Equalities out of Implications]
  | otherwise = partitionBag is_floatable wanteds 
  where is_floatable :: WantedEvVar -> Bool 
        is_floatable (WantedEvVar cv _) 
          | isCoVar cv = skols `disjointVarSet` predTvs_under_fsks (coVarPred cv)
        is_floatable _wv = False

        tvs_under_fsks :: Type -> TyVarSet
        -- ^ NB: for type synonyms tvs_under_fsks does /not/ expand the synonym
        tvs_under_fsks (TyVarTy tv)     
          | not (isTcTyVar tv)               = unitVarSet tv
          | FlatSkol ty <- tcTyVarDetails tv = tvs_under_fsks ty
          | otherwise                        = unitVarSet tv
        tvs_under_fsks (TyConApp _ tys) = unionVarSets (map tvs_under_fsks tys)
        tvs_under_fsks (PredTy sty)     = predTvs_under_fsks sty
        tvs_under_fsks (FunTy arg res)  = tvs_under_fsks arg `unionVarSet` tvs_under_fsks res
        tvs_under_fsks (AppTy fun arg)  = tvs_under_fsks fun `unionVarSet` tvs_under_fsks arg
        tvs_under_fsks (ForAllTy tv ty) -- The kind of a coercion binder 
        	     	       	      -- can mention type variables!
          | isTyVar tv		      = inner_tvs `delVarSet` tv
          | otherwise  {- Coercion -} = -- ASSERT( not (tv `elemVarSet` inner_tvs) )
                                        inner_tvs `unionVarSet` tvs_under_fsks (tyVarKind tv)
          where
            inner_tvs = tvs_under_fsks ty

        predTvs_under_fsks :: PredType -> TyVarSet
        predTvs_under_fsks (IParam _ ty)    = tvs_under_fsks ty
        predTvs_under_fsks (ClassP _ tys)   = unionVarSets (map tvs_under_fsks tys)
        predTvs_under_fsks (EqPred ty1 ty2) = tvs_under_fsks ty1 `unionVarSet` tvs_under_fsks ty2




901
\end{code}
902

903 904 905 906 907
Note [Float Equalities out of Implications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
We want to float equalities out of vanilla existentials, but *not* out 
of GADT pattern matches. 

908 909 910 911
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:
912 913

  a) In checking mode, suppresses unnecessary errors.  We already have
914 915
     on unsolved-wanted error; adding it to the givens prevents any 
     consequential errors from showing uop
916

917 918 919 920 921 922 923 924 925 926 927 928
  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
929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956
'solveInteract' step first. 

Note [Extra TcsTv untouchables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Furthemore, we record the inert set simplifier-generated unification variables of the TcsTv
kind (such as variables from instance that have been applied, or unification flattens). These
variables must be passed to the implications as extra untouchable variables. Otherwise
we have the danger of double unifications. Example (from trac ticket #4494):

   (F Int ~ uf)  /\  (forall a. C a => F Int ~ beta) 

In this example, beta is touchable inside the implication. The first solveInteract step
leaves 'uf' ununified. Then we move inside the implication where a new constraint
       uf  ~  beta  
emerges. We may spontaneously solve it to get uf := beta, so the whole implication disappears
but when we pop out again we are left with (F Int ~ uf) which will be unified by our final 
solveCTyFunEqs stage and uf will get unified *once more* to  (F Int). 

The solution is to record the TcsTvs (i.e. the simplifier-generated unification variables)
that are generated when solving the flats, and make them untouchables for the nested 
implication. In the example above uf would become untouchable, so beta would be forced to 
be unified as beta := uf.

NB: A consequence is that every simplifier-generated TcsTv variable that gets floated out 
    of an implication becomes now untouchable next time we go inside that implication to 
    solve any residual constraints. In effect, by floating an equality out of the implication 
    we are committing to have it solved in the outside. 

957

958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008
\begin{code}

solveCTyFunEqs :: CanonicalCts -> Bag Implication -> TcS (Bag WantedEvVar, Bag Implication)
-- Default equalities (F xi ~ alpha) by setting (alpha := F xi), whenever possible
-- See Note [Solving Family Equations]
-- Returns: a bunch of unsolved constraints from the original CanonicalCts and implications
--          where the newly generated equalities (alpha := F xi) have been substituted through.
solveCTyFunEqs cts implics
 = do { untch   <- getUntouchables 
      ; let (unsolved_can_cts, funeq_bnds) = getSolvableCTyFunEqs untch cts
      ; traceTcS "defaultCTyFunEqs" (vcat [text "Trying to default family equations:"
                                          , ppr funeq_bnds
                                          ])
      ; mapM_ solve_one funeq_bnds

             -- Apply the substitution through to eliminate the flatten 
             -- unification variables we substituted both in the unsolved flats and implics
      ; let final_unsolved 
              = Bag.mapBag (subst_wevar funeq_bnds . deCanonicaliseWanted) unsolved_can_cts
            final_implics 
              = Bag.mapBag (subst_impl funeq_bnds) implics

      ; return (final_unsolved, final_implics) }

  where solve_one (tv,(ty,cv,fl)) 
          | not (typeKind ty `isSubKind` tyVarKind tv) 
          = addErrorTcS KindError fl (mkTyVarTy tv) ty
             -- Must do a small kind check since TcCanonical invariants 
             -- on family equations only impose compatibility, not subkinding
          | otherwise = setWantedTyBind tv ty >> setWantedCoBind cv ty

        subst_wanted :: FunEqBinds -> WantedConstraint -> WantedConstraint
        subst_wanted funeq_bnds (WcEvVar wv)    = WcEvVar  (subst_wevar funeq_bnds wv)
        subst_wanted funeq_bnds (WcImplic impl) = WcImplic (subst_impl funeq_bnds impl)

        subst_wevar :: FunEqBinds -> WantedEvVar -> WantedEvVar        
        subst_wevar funeq_bnds (WantedEvVar v loc)
          = let orig_ty  = varType v
                new_ty   = substFunEqBnds funeq_bnds orig_ty
            in WantedEvVar (setVarType v new_ty) loc
               
        subst_impl :: FunEqBinds -> Implication -> Implication
        subst_impl funeq_bnds impl@(Implic { ic_wanted = ws })
          = impl { ic_wanted = Bag.mapBag (subst_wanted funeq_bnds) ws }


type FunEqBinds = [(TcTyVar,(TcType,CoVar,CtFlavor))]
-- Invariant: if it contains:
--       [... a -> (ta,...) ... b -> (tb,...) ... ] 
-- then 'ta' cannot mention 'b'

1009
getSolvableCTyFunEqs :: TcsUntouchables
1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062
                     -> CanonicalCts                -- Precondition: all wanteds 
                     -> (CanonicalCts, FunEqBinds)  -- Postcondition: returns the unsolvables
getSolvableCTyFunEqs untch cts
  = Bag.foldlBag dflt_funeq (emptyCCan, []) cts
  where dflt_funeq (cts_in, extra_binds) ct@(CFunEqCan { cc_id = cv
                                                       , cc_flavor = fl
                                                       , cc_fun = tc
                                                       , cc_tyargs = xis
                                                       , cc_rhs = xi })
          | Just tv <- tcGetTyVar_maybe xi
          , isTouchableMetaTyVar_InRange untch tv -- If RHS is a touchable unif. variable
          , Nothing <- lookup tv extra_binds      -- or in extra_binds
               -- See Note [Solving Family Equations], Point 1
          = ASSERT ( isWanted fl )
            let ty_orig   = mkTyConApp tc xis 
                ty_bind   = substFunEqBnds extra_binds ty_orig
            in if tv `elemVarSet` tyVarsOfType ty_bind 
               then (cts_in `extendCCans` ct, extra_binds)     
                      -- See Note [Solving Family Equations], Point 2
               else (cts_in, (tv,(ty_bind,cv,fl)):extra_binds) 
                      -- Postcondition met because extra_binds is already applied to ty_bind

        dflt_funeq (cts_in, extra_binds) ct = (cts_in `extendCCans` ct, extra_binds)

substFunEqBnds :: FunEqBinds -> TcType -> TcType 
substFunEqBnds bnds ty 
  = foldr (\(x,(t,_cv,_fl)) xy -> substTyWith [x] [t] xy) ty bnds
    -- foldr works because of the FunEqBinds invariant


\end{code}

Note [Solving Family Equations] 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
After we are done with simplification we may be left with constraints of the form:
     [Wanted] F xis ~ beta 
If 'beta' is a touchable unification variable not already bound in the TyBinds 
then we'd like to create a binding for it, effectively "defaulting" it to be 'F xis'.

When is it ok to do so? 
    1) 'beta' must not already be defaulted to something. Example: 

           [Wanted] F Int  ~ beta   <~ Will default [beta := F Int]
           [Wanted] F Char ~ beta   <~ Already defaulted, can't default again. We 
                                       have to report this as unsolved.

    2) However, we must still do an occurs check when defaulting (F xis ~ beta), to 
       set [beta := F xis] only if beta is not among the free variables of xis.

    3) Notice that 'beta' can't be bound in ty binds already because we rewrite RHS 
       of type family equations. See Inert Set invariants in TcInteract. 


1063 1064 1065 1066 1067 1068 1069
*********************************************************************************
*                                                                               * 
*                          Defaulting and disamgiguation                        *
*                                                                               *
*********************************************************************************

Basic plan behind applyDefaulting rules: 
1070
 
1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096
 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 
------------------------------------------------------------------------------------------
1097

1098 1099

\begin{code}
1100
applyDefaultingRules :: InertSet
1101
                     -> CanonicalCts        -- All wanteds
1102
                     -> TcS (Bag WantedEvVar)  -- All wanteds again!  
1103 1104 1105 1106 1107 1108
-- Return some *extra* givens, which express the 
-- type-class-default choice

applyDefaultingRules inert wanteds
  | isEmptyBag wanteds 
  = return emptyBag
1109
  | otherwise
1110
  = do { untch <- getUntouchables
1111
       ; tv_cts <- mapM (defaultTyVar untch) $
1112
                   varSetElems (tyVarsOfCDicts wanteds) 
1113 1114 1115

       ; info@(_, default_tys, _) <- getDefaultInfo
       ; let groups = findDefaultableGroups info untch wanteds
1116
       ; deflt_cts <- mapM (disambigGroup default_tys inert) groups
1117 1118 1119 1120

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

1121
       ; return (unionManyBags deflt_cts `unionBags` unionManyBags tv_cts) }
1122 1123

------------------
1124
defaultTyVar :: TcsUntouchables -> TcTyVar -> TcS (Bag WantedEvVar)
1125 1126 1127 1128 1129 1130 1131 1132
-- 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.
1133
--
1134 1135 1136 1137 1138 1139
-- 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 
1140
  | isTouchableMetaTyVar_InRange untch the_tv
1141
  , not (k `eqKind` default_k)
1142
  = do { ev <- TcSMonad.newKindConstraint the_tv default_k
1143
       ; let loc = CtLoc DefaultOrigin (getSrcSpan the_tv) [] -- Yuk
1144
       ; return (unitBag (WantedEvVar ev loc)) }
1145
  | otherwise            
1146
  = return emptyBag	 -- The common case
1147
  where
1148 1149 1150 1151 1152 1153 1154 1155 1156
    k = tyVarKind the_tv
    default_k = defaultKind k


----------------
findDefaultableGroups 
    :: ( SimplContext 
       , [Type]
       , (Bool,Bool) )  -- (Overloaded strings, extended default rules)
1157
    -> TcsUntouchables	-- Untouchable
1158 1159 1160 1161 1162 1163 1164
    -> 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)
1165
  where 
1166
    unaries     :: [(CanonicalCt, TcTyVar)]  -- (C tv) constraints
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
1167
    non_unaries :: [CanonicalCt]             -- and *other* constraints
1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183
    
    (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)
1184
        && isTouchableMetaTyVar_InRange untch tv 
1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208
        && 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
1209
              -> TcS (Bag WantedEvVar)
1210

1211
disambigGroup [] _inert _grp 
1212
  = return emptyBag
1213
disambigGroup (default_ty:default_tys) inert group
1214
  = do { traceTcS "disambigGroup" (ppr group $$ ppr default_ty)
1215 1216
       ; let ct_loc = get_ct_loc (cc_flavor the_ct) 
       ; ev <- TcSMonad.newWantedCoVar (mkTyVarTy the_tv) default_ty
1217
       ; success <- tryTcS $ 
1218 1219 1220 1221
           	    do { final_inert <- solveInteract inert $
                                        consBag (Wanted ct_loc, ev) wanted_to_solve
           	       ; let (_, unsolved) = extractUnsolved final_inert                         
                       ; errs <- getTcSErrorsBag
1222
           	       ; return (isEmptyBag unsolved && isEmptyBag errs) }
1223
       ; case success of
1224 1225 1226 1227
           True  ->  -- Success: record the type variable binding, and return
                    do { wrapWarnTcS $ warnDefaulting wanted_ev_vars default_ty
                       ; traceTcS "disambigGroup succeeded" (ppr default_ty)
                       ; return (unitBag $ WantedEvVar ev ct_loc) }
1228
           False ->    -- Failure: try with the next type
1229
		    do { traceTcS "disambigGroup failed, will try other default types" (ppr default_ty)
1230
                       ; disambigGroup default_tys inert group } }
1231
  where
1232
    ((the_ct,the_tv):_) = group
1233 1234 1235 1236
    wanteds             = map fst group
    wanted_ev_vars      = map deCanonicaliseWanted wanteds
    wanted_to_solve     = listToBag $ 
                          map (\(WantedEvVar ev wloc) -> (Wanted wloc,ev)) wanted_ev_vars
1237 1238 1239 1240 1241

    get_ct_loc (Wanted l) = l
    get_ct_loc _ = panic "Asked  to disambiguate given or derived!"


1242 1243
\end{code}

1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255
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