Yet another major refactoring of the constraint solver
[ghc.git] / compiler / typecheck / Inst.lhs
1 %
2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4 %
5
6 The @Inst@ type: dictionaries or method instances
7
8 \begin{code}
9 {-# OPTIONS -fno-warn-tabs #-}
10 -- The above warning supression flag is a temporary kludge.
11 -- While working on this module you are encouraged to remove it and
12 -- detab the module (please do the detabbing in a separate patch). See
13 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces
14 -- for details
15
16 module Inst ( 
17        deeplySkolemise, 
18        deeplyInstantiate, instCall, instStupidTheta,
19        emitWanted, emitWanteds,
20
21        newOverloadedLit, mkOverLit, 
22      
23        tcGetInstEnvs, getOverlapFlag,
24        tcExtendLocalInstEnv, instCallConstraints, newMethodFromName,
25        tcSyntaxName,
26
27        -- Simple functions over evidence variables
28        hasEqualities, unitImplication,
29        
30        tyVarsOfWC, tyVarsOfBag, 
31        tyVarsOfEvVar, tyVarsOfEvVars, tyVarsOfImplication,
32        tyVarsOfCt, tyVarsOfCts, tyVarsOfCDict, tyVarsOfCDicts,
33
34        tidyEvVar, tidyCt, tidyGivenLoc,
35
36        substEvVar, substImplication, substCt
37     ) where
38
39 #include "HsVersions.h"
40
41 import {-# SOURCE #-}   TcExpr( tcPolyExpr, tcSyntaxOp )
42 import {-# SOURCE #-}   TcUnify( unifyType )
43
44 import FastString
45 import HsSyn
46 import TcHsSyn
47 import TcRnMonad
48 import TcEnv
49 import TcEvidence
50 import InstEnv
51 import FunDeps
52 import TcMType
53 import Type
54 import TcType
55 import Class
56 import Unify
57 import HscTypes
58 import Id
59 import Name
60 import Var      ( Var, EvVar, varType, setVarType )
61 import VarEnv
62 import VarSet
63 import PrelNames
64 import SrcLoc
65 import DynFlags
66 import Bag
67 import Maybes
68 import Util
69 import Outputable
70 import Data.List( mapAccumL )
71 \end{code}
72
73
74
75 %************************************************************************
76 %*                                                                      *
77                 Emitting constraints
78 %*                                                                      *
79 %************************************************************************
80
81 \begin{code}
82 emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
83 emitWanteds origin theta = mapM (emitWanted origin) theta
84
85 emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
86 emitWanted origin pred 
87   = do { loc <- getCtLoc origin
88        ; ev  <- newWantedEvVar pred
89        ; emitFlat (mkNonCanonical (Wanted { ctev_wloc = loc, ctev_pred = pred, ctev_evar = ev }))
90        ; return ev }
91
92 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
93 -- Used when Name is the wired-in name for a wired-in class method,
94 -- so the caller knows its type for sure, which should be of form
95 --    forall a. C a => <blah>
96 -- newMethodFromName is supposed to instantiate just the outer 
97 -- type variable and constraint
98
99 newMethodFromName origin name inst_ty
100   = do { id <- tcLookupId name
101               -- Use tcLookupId not tcLookupGlobalId; the method is almost
102               -- always a class op, but with -XRebindableSyntax GHC is
103               -- meant to find whatever thing is in scope, and that may
104               -- be an ordinary function. 
105
106        ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
107              (the_tv:rest) = tvs
108              subst = zipOpenTvSubst [the_tv] [inst_ty]
109
110        ; wrap <- ASSERT( null rest && isSingleton theta )
111                  instCall origin [inst_ty] (substTheta subst theta)
112        ; return (mkHsWrap wrap (HsVar id)) }
113 \end{code}
114
115
116 %************************************************************************
117 %*                                                                      *
118         Deep instantiation and skolemisation
119 %*                                                                      *
120 %************************************************************************
121
122 Note [Deep skolemisation]
123 ~~~~~~~~~~~~~~~~~~~~~~~~~
124 deeplySkolemise decomposes and skolemises a type, returning a type
125 with all its arrows visible (ie not buried under foralls)
126
127 Examples:
128
129   deeplySkolemise (Int -> forall a. Ord a => blah)  
130     =  ( wp, [a], [d:Ord a], Int -> blah )
131     where wp = \x:Int. /\a. \(d:Ord a). <hole> x
132
133   deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)  
134     =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
135     where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
136
137 In general,
138   if      deeplySkolemise ty = (wrap, tvs, evs, rho)
139     and   e :: rho
140   then    wrap e :: ty
141     and   'wrap' binds tvs, evs
142
143 ToDo: this eta-abstraction plays fast and loose with termination,
144       because it can introduce extra lambdas.  Maybe add a `seq` to
145       fix this
146
147
148 \begin{code}
149 deeplySkolemise
150   :: TcSigmaType
151   -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)
152
153 deeplySkolemise ty
154   | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
155   = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
156        ; (subst, tvs1) <- tcInstSkolTyVars tvs
157        ; ev_vars1 <- newEvVars (substTheta subst theta)
158        ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
159        ; return ( mkWpLams ids1
160                    <.> mkWpTyLams tvs1
161                    <.> mkWpLams ev_vars1
162                    <.> wrap
163                    <.> mkWpEvVarApps ids1
164                 , tvs1     ++ tvs2
165                 , ev_vars1 ++ ev_vars2
166                 , mkFunTys arg_tys rho ) }
167
168   | otherwise
169   = return (idHsWrapper, [], [], ty)
170
171 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
172 --   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
173 -- In general if
174 -- if    deeplyInstantiate ty = (wrap, rho)
175 -- and   e :: ty
176 -- then  wrap e :: rho
177
178 deeplyInstantiate orig ty
179   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
180   = do { (_, tys, subst) <- tcInstTyVars tvs
181        ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
182        ; wrap1 <- instCall orig tys (substTheta subst theta)
183        ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
184        ; return (mkWpLams ids1 
185                     <.> wrap2
186                     <.> wrap1 
187                     <.> mkWpEvVarApps ids1,
188                  mkFunTys arg_tys rho2) }
189
190   | otherwise = return (idHsWrapper, ty)
191 \end{code}
192
193
194 %************************************************************************
195 %*                                                                      *
196             Instantiating a call
197 %*                                                                      *
198 %************************************************************************
199
200 \begin{code}
201 ----------------
202 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
203 -- Instantiate the constraints of a call
204 --      (instCall o tys theta)
205 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
206 -- (b) Throws these dictionaries into the LIE
207 -- (c) Returns an HsWrapper ([.] tys dicts)
208
209 instCall orig tys theta 
210   = do  { dict_app <- instCallConstraints orig theta
211         ; return (dict_app <.> mkWpTyApps tys) }
212
213 ----------------
214 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
215 -- Instantiates the TcTheta, puts all constraints thereby generated
216 -- into the LIE, and returns a HsWrapper to enclose the call site.
217
218 instCallConstraints _ [] = return idHsWrapper
219
220 instCallConstraints origin (pred : preds)
221   | Just (ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
222   = do  { traceTc "instCallConstraints" $ ppr (mkEqPred ty1 ty2)
223         ; co <- unifyType ty1 ty2
224         ; co_fn <- instCallConstraints origin preds
225         ; return (co_fn <.> WpEvApp (EvCoercion co)) }
226
227   | otherwise
228   = do  { ev_var <- emitWanted origin pred
229         ; co_fn <- instCallConstraints origin preds
230         ; return (co_fn <.> WpEvApp (EvId ev_var)) }
231
232 ----------------
233 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
234 -- Similar to instCall, but only emit the constraints in the LIE
235 -- Used exclusively for the 'stupid theta' of a data constructor
236 instStupidTheta orig theta
237   = do  { _co <- instCallConstraints orig theta -- Discard the coercion
238         ; return () }
239 \end{code}
240
241 %************************************************************************
242 %*                                                                      *
243                 Literals
244 %*                                                                      *
245 %************************************************************************
246
247 In newOverloadedLit we convert directly to an Int or Integer if we
248 know that's what we want.  This may save some time, by not
249 temporarily generating overloaded literals, but it won't catch all
250 cases (the rest are caught in lookupInst).
251
252 \begin{code}
253 newOverloadedLit :: CtOrigin
254                  -> HsOverLit Name
255                  -> TcRhoType
256                  -> TcM (HsOverLit TcId)
257 newOverloadedLit orig 
258   lit@(OverLit { ol_val = val, ol_rebindable = rebindable
259                , ol_witness = meth_name }) res_ty
260
261   | not rebindable
262   , Just expr <- shortCutLit val res_ty 
263         -- Do not generate a LitInst for rebindable syntax.  
264         -- Reason: If we do, tcSimplify will call lookupInst, which
265         --         will call tcSyntaxName, which does unification, 
266         --         which tcSimplify doesn't like
267   = return (lit { ol_witness = expr, ol_type = res_ty })
268
269   | otherwise
270   = do  { hs_lit <- mkOverLit val
271         ; let lit_ty = hsLitType hs_lit
272         ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
273                 -- Overloaded literals must have liftedTypeKind, because
274                 -- we're instantiating an overloaded function here,
275                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
276                 -- However this'll be picked up by tcSyntaxOp if necessary
277         ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
278         ; return (lit { ol_witness = witness, ol_type = res_ty }) }
279
280 ------------
281 mkOverLit :: OverLitVal -> TcM HsLit
282 mkOverLit (HsIntegral i) 
283   = do  { integer_ty <- tcMetaTy integerTyConName
284         ; return (HsInteger i integer_ty) }
285
286 mkOverLit (HsFractional r)
287   = do  { rat_ty <- tcMetaTy rationalTyConName
288         ; return (HsRat r rat_ty) }
289
290 mkOverLit (HsIsString s) = return (HsString s)
291 \end{code}
292
293
294
295
296 %************************************************************************
297 %*                                                                      *
298                 Re-mappable syntax
299     
300      Used only for arrow syntax -- find a way to nuke this
301 %*                                                                      *
302 %************************************************************************
303
304 Suppose we are doing the -XRebindableSyntax thing, and we encounter
305 a do-expression.  We have to find (>>) in the current environment, which is
306 done by the rename. Then we have to check that it has the same type as
307 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
308 this:
309
310   (>>) :: HB m n mn => m a -> n b -> mn b
311
312 So the idea is to generate a local binding for (>>), thus:
313
314         let then72 :: forall a b. m a -> m b -> m b
315             then72 = ...something involving the user's (>>)...
316         in
317         ...the do-expression...
318
319 Now the do-expression can proceed using then72, which has exactly
320 the expected type.
321
322 In fact tcSyntaxName just generates the RHS for then72, because we only
323 want an actual binding in the do-expression case. For literals, we can 
324 just use the expression inline.
325
326 \begin{code}
327 tcSyntaxName :: CtOrigin
328              -> TcType                  -- Type to instantiate it at
329              -> (Name, HsExpr Name)     -- (Standard name, user name)
330              -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
331 --      *** NOW USED ONLY FOR CmdTop (sigh) ***
332 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
333 -- So we do not call it from lookupInst, which is called from tcSimplify
334
335 tcSyntaxName orig ty (std_nm, HsVar user_nm)
336   | std_nm == user_nm
337   = do rhs <- newMethodFromName orig std_nm ty
338        return (std_nm, rhs)
339
340 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
341     std_id <- tcLookupId std_nm
342     let 
343         -- C.f. newMethodAtLoc
344         ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
345         sigma1          = substTyWith [tv] [ty] tau
346         -- Actually, the "tau-type" might be a sigma-type in the
347         -- case of locally-polymorphic methods.
348
349     addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
350
351         -- Check that the user-supplied thing has the
352         -- same type as the standard one.  
353         -- Tiresome jiggling because tcCheckSigma takes a located expression
354      span <- getSrcSpanM
355      expr <- tcPolyExpr (L span user_nm_expr) sigma1
356      return (std_nm, unLoc expr)
357
358 syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
359                -> TcRn (TidyEnv, SDoc)
360 syntaxNameCtxt name orig ty tidy_env = do
361     inst_loc <- getCtLoc orig
362     let
363         msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+> 
364                                 ptext (sLit "(needed by a syntactic construct)"),
365                     nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
366                     nest 2 (pprArisingAt inst_loc)]
367     return (tidy_env, msg)
368 \end{code}
369
370
371 %************************************************************************
372 %*                                                                      *
373                 Instances
374 %*                                                                      *
375 %************************************************************************
376
377 \begin{code}
378 getOverlapFlag :: TcM OverlapFlag
379 getOverlapFlag 
380   = do  { dflags <- getDynFlags
381         ; let overlap_ok    = xopt Opt_OverlappingInstances dflags
382               incoherent_ok = xopt Opt_IncoherentInstances  dflags
383               safeOverlap   = safeLanguageOn dflags
384               overlap_flag | incoherent_ok = Incoherent safeOverlap
385                            | overlap_ok    = OverlapOk safeOverlap
386                            | otherwise     = NoOverlap safeOverlap
387
388         ; return overlap_flag }
389
390 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
391 -- Gets both the external-package inst-env
392 -- and the home-pkg inst env (includes module being compiled)
393 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
394                      return (eps_inst_env eps, tcg_inst_env env) }
395
396 tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
397   -- Add new locally-defined instances
398 tcExtendLocalInstEnv dfuns thing_inside
399  = do { traceDFuns dfuns
400       ; env <- getGblEnv
401       ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
402       ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
403                          tcg_inst_env = inst_env' }
404       ; setGblEnv env' thing_inside }
405
406 addLocalInst :: InstEnv -> ClsInst -> TcM InstEnv
407 -- Check that the proposed new instance is OK, 
408 -- and then add it to the home inst env
409 -- If overwrite_inst, then we can overwrite a direct match
410 addLocalInst home_ie ispec = do
411     -- Instantiate the dfun type so that we extend the instance
412     -- envt with completely fresh template variables
413     -- This is important because the template variables must
414     -- not overlap with anything in the things being looked up
415     -- (since we do unification).  
416         --
417         -- We use tcInstSkolType because we don't want to allocate fresh
418         --  *meta* type variables.
419         --
420         -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
421         -- these variables must be bindable by tcUnifyTys.  See
422         -- the call to tcUnifyTys in InstEnv, and the special
423         -- treatment that instanceBindFun gives to isOverlappableTyVar
424         -- This is absurdly delicate.
425
426     let dfun = instanceDFunId ispec
427     (tvs', theta', tau') <- tcInstSkolType (idType dfun)
428     let (cls, tys') = tcSplitDFunHead tau'
429         dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')           
430         ispec'      = setInstanceDFunId ispec dfun'
431
432         -- Load imported instances, so that we report
433         -- duplicates correctly
434     eps <- getEps
435     let inst_envs = (eps_inst_env eps, home_ie)
436
437         -- Check functional dependencies
438     case checkFunDeps inst_envs ispec' of
439         Just specs -> funDepErr ispec' specs
440         Nothing    -> return ()
441
442         -- Check for duplicate instance decls
443     let (matches, unifs, _) = lookupInstEnv inst_envs cls tys'
444         dup_ispecs = [ dup_ispec 
445                         | (dup_ispec, _) <- matches
446                         , let (_,_,_,dup_tys) = instanceHead dup_ispec
447                         , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)]
448                         
449         -- Find memebers of the match list which ispec itself matches.
450         -- If the match is 2-way, it's a duplicate
451         -- If it's a duplicate, but we can overwrite home package dups, then overwrite
452     isGHCi <- getIsGHCi
453     overlapFlag <- getOverlapFlag
454     case isGHCi of
455         False -> case dup_ispecs of
456             dup : _ -> dupInstErr ispec' dup >> return (extendInstEnv home_ie ispec')
457             []      -> return (extendInstEnv home_ie ispec')
458         True  -> case (dup_ispecs, home_ie_matches, unifs, overlapFlag) of
459             (_, _:_, _, _)      -> return (overwriteInstEnv home_ie ispec')
460             (dup:_, [], _, _)   -> dupInstErr ispec' dup >> return (extendInstEnv home_ie ispec')
461             ([], _, u:_, NoOverlap _)    -> overlappingInstErr ispec' u >> return (extendInstEnv home_ie ispec')
462             _                   -> return (extendInstEnv home_ie ispec')
463           where (homematches, _) = lookupInstEnv' home_ie cls tys'
464                 home_ie_matches = [ dup_ispec 
465                     | (dup_ispec, _) <- homematches
466                     , let (_,_,_,dup_tys) = instanceHead dup_ispec
467                     , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)]
468
469 traceDFuns :: [ClsInst] -> TcRn ()
470 traceDFuns ispecs
471   = traceTc "Adding instances:" (vcat (map pp ispecs))
472   where
473     pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
474         -- Print the dfun name itself too
475
476 funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
477 funDepErr ispec ispecs
478   = addClsInstsErr (ptext (sLit "Functional dependencies conflict between instance declarations:"))
479                     (ispec : ispecs)
480
481 dupInstErr :: ClsInst -> ClsInst -> TcRn ()
482 dupInstErr ispec dup_ispec
483   = addClsInstsErr (ptext (sLit "Duplicate instance declarations:"))
484                     [ispec, dup_ispec]
485
486 overlappingInstErr :: ClsInst -> ClsInst -> TcRn ()
487 overlappingInstErr ispec dup_ispec
488   = addClsInstsErr (ptext (sLit "Overlapping instance declarations:")) 
489                     [ispec, dup_ispec]
490
491 addClsInstsErr :: SDoc -> [ClsInst] -> TcRn ()
492 addClsInstsErr herald ispecs
493   = setSrcSpan (getSrcSpan (head sorted)) $
494     addErr (hang herald 2 (pprInstances sorted))
495  where
496    sorted = sortWith getSrcLoc ispecs
497    -- The sortWith just arranges that instances are dislayed in order
498    -- of source location, which reduced wobbling in error messages,
499    -- and is better for users
500 \end{code}
501
502 %************************************************************************
503 %*                                                                      *
504         Simple functions over evidence variables
505 %*                                                                      *
506 %************************************************************************
507
508 \begin{code}
509 unitImplication :: Implication -> Bag Implication
510 unitImplication implic
511   | isEmptyWC (ic_wanted implic) = emptyBag
512   | otherwise                    = unitBag implic
513
514 hasEqualities :: [EvVar] -> Bool
515 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
516 hasEqualities givens = any (has_eq . evVarPred) givens
517   where
518     has_eq = has_eq' . classifyPredType
519
520     has_eq' (EqPred {})          = True
521     has_eq' (IPPred {})          = False
522     has_eq' (ClassPred cls _tys) = any has_eq (classSCTheta cls)
523     has_eq' (TuplePred ts)       = any has_eq ts
524     has_eq' (IrredPred _)        = True -- Might have equalities in it after reduction?
525
526 ---------------- Getting free tyvars -------------------------
527
528 tyVarsOfCt :: Ct -> TcTyVarSet
529 tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
530 tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
531 tyVarsOfCt (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
532 tyVarsOfCt (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
533 tyVarsOfCt (CIrredEvCan { cc_ty = ty })                 = tyVarsOfType ty
534 tyVarsOfCt (CNonCanonical { cc_ev = fl })           = tyVarsOfType (ctEvPred fl)
535
536 tyVarsOfCDict :: Ct -> TcTyVarSet 
537 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
538 tyVarsOfCDict _ct                            = emptyVarSet 
539
540 tyVarsOfCDicts :: Cts -> TcTyVarSet 
541 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
542
543 tyVarsOfCts :: Cts -> TcTyVarSet
544 tyVarsOfCts = foldrBag (unionVarSet . tyVarsOfCt) emptyVarSet
545
546 tyVarsOfWC :: WantedConstraints -> TyVarSet
547 tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
548   = tyVarsOfCts flat `unionVarSet`
549     tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
550     tyVarsOfCts insol
551
552 tyVarsOfImplication :: Implication -> TyVarSet
553 tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
554   = tyVarsOfWC wanted `delVarSetList` skols
555
556 tyVarsOfEvVar :: EvVar -> TyVarSet
557 tyVarsOfEvVar ev = tyVarsOfType $ evVarPred ev
558
559 tyVarsOfEvVars :: [EvVar] -> TyVarSet
560 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
561
562 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
563 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
564
565 ---------------- Tidying -------------------------
566
567 tidyCt :: TidyEnv -> Ct -> Ct
568 -- Used only in error reporting
569 -- Also converts it to non-canonical
570 tidyCt env ct 
571   = CNonCanonical { cc_ev = tidy_flavor env (cc_ev ct)
572                   , cc_depth  = cc_depth ct } 
573   where 
574     tidy_flavor :: TidyEnv -> CtEvidence -> CtEvidence
575      -- NB: we do not tidy the ctev_evtm/var field because we don't 
576      --     show it in error messages
577     tidy_flavor env ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
578       = ctev { ctev_gloc = tidyGivenLoc env gloc
579              , ctev_pred = tidyType env pred }
580     tidy_flavor env ctev@(Wanted { ctev_pred = pred })
581       = ctev { ctev_pred = tidyType env pred }
582     tidy_flavor env ctev@(Derived { ctev_pred = pred })
583       = ctev { ctev_pred = tidyType env pred }
584
585 tidyEvVar :: TidyEnv -> EvVar -> EvVar
586 tidyEvVar env var = setVarType var (tidyType env (varType var))
587
588 tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
589 tidyGivenLoc env (CtLoc skol span ctxt) 
590   = CtLoc (tidySkolemInfo env skol) span ctxt
591
592 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
593 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
594 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
595 tidySkolemInfo env (UnifyForAllSkol skol_tvs ty) 
596   = UnifyForAllSkol (map tidy_tv skol_tvs) (tidyType env ty)
597   where
598     tidy_tv tv = case getTyVar_maybe ty' of
599                    Just tv' -> tv'
600                    Nothing  -> pprPanic "ticySkolemInfo" (ppr tv <+> ppr ty')
601                where
602                  ty' = tidyTyVarOcc env tv
603 tidySkolemInfo _   info            = info
604
605 ---------------- Substitution -------------------------
606 -- This is used only in TcSimpify, for substituations that are *also* 
607 -- reflected in the unification variables.  So we don't substitute
608 -- in the evidence.
609
610 substCt :: TvSubst -> Ct -> Ct 
611 -- Conservatively converts it to non-canonical:
612 -- Postcondition: if the constraint does not get rewritten
613 substCt subst ct
614   | pty <- ctPred ct
615   , sty <- substTy subst pty 
616   = if sty `eqType` pty then 
617         ct { cc_ev = substFlavor subst (cc_ev ct) }
618     else 
619         CNonCanonical { cc_ev = substFlavor subst (cc_ev ct)
620                       , cc_depth  = cc_depth ct }
621
622 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
623 substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
624   = WC { wc_flat  = mapBag (substCt subst) flat
625        , wc_impl  = mapBag (substImplication subst) implic
626        , wc_insol = mapBag (substCt subst) insol }
627
628 substImplication :: TvSubst -> Implication -> Implication
629 substImplication subst implic@(Implic { ic_skols = tvs
630                                       , ic_given = given
631                                       , ic_wanted = wanted
632                                       , ic_loc = loc })
633   = implic { ic_skols  = tvs'
634            , ic_given  = map (substEvVar subst1) given
635            , ic_wanted = substWC subst1 wanted
636            , ic_loc    = substGivenLoc subst1 loc }
637   where
638    (subst1, tvs') = mapAccumL substTyVarBndr subst tvs
639
640 substEvVar :: TvSubst -> EvVar -> EvVar
641 substEvVar subst var = setVarType var (substTy subst (varType var))
642
643 substFlavor :: TvSubst -> CtEvidence -> CtEvidence
644 substFlavor subst ctev@(Given { ctev_gloc = gloc, ctev_pred = pred })
645   = ctev { ctev_gloc = substGivenLoc subst gloc
646           , ctev_pred = substTy subst pred }
647
648 substFlavor subst ctev@(Wanted { ctev_pred = pred })
649   = ctev  { ctev_pred = substTy subst pred }
650
651 substFlavor subst ctev@(Derived { ctev_pred = pty })
652   = ctev { ctev_pred = substTy subst pty }
653
654 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
655 substGivenLoc subst (CtLoc skol span ctxt) 
656   = CtLoc (substSkolemInfo subst skol) span ctxt
657
658 substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
659 substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
660 substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
661 substSkolemInfo _     info            = info
662 \end{code}