a194d748ed5f216a2bc576caaddccf3b3665a383
[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 = do { loc <- getCtLoc origin
87                             ; ev  <- newWantedEvVar pred
88                             ; emitFlat (mkNonCanonical ev (Wanted loc))
89                             ; return ev }
90
91 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
92 -- Used when Name is the wired-in name for a wired-in class method,
93 -- so the caller knows its type for sure, which should be of form
94 --    forall a. C a => <blah>
95 -- newMethodFromName is supposed to instantiate just the outer 
96 -- type variable and constraint
97
98 newMethodFromName origin name inst_ty
99   = do { id <- tcLookupId name
100               -- Use tcLookupId not tcLookupGlobalId; the method is almost
101               -- always a class op, but with -XRebindableSyntax GHC is
102               -- meant to find whatever thing is in scope, and that may
103               -- be an ordinary function. 
104
105        ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
106              (the_tv:rest) = tvs
107              subst = zipOpenTvSubst [the_tv] [inst_ty]
108
109        ; wrap <- ASSERT( null rest && isSingleton theta )
110                  instCall origin [inst_ty] (substTheta subst theta)
111        ; return (mkHsWrap wrap (HsVar id)) }
112 \end{code}
113
114
115 %************************************************************************
116 %*                                                                      *
117         Deep instantiation and skolemisation
118 %*                                                                      *
119 %************************************************************************
120
121 Note [Deep skolemisation]
122 ~~~~~~~~~~~~~~~~~~~~~~~~~
123 deeplySkolemise decomposes and skolemises a type, returning a type
124 with all its arrows visible (ie not buried under foralls)
125
126 Examples:
127
128   deeplySkolemise (Int -> forall a. Ord a => blah)  
129     =  ( wp, [a], [d:Ord a], Int -> blah )
130     where wp = \x:Int. /\a. \(d:Ord a). <hole> x
131
132   deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)  
133     =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
134     where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
135
136 In general,
137   if      deeplySkolemise ty = (wrap, tvs, evs, rho)
138     and   e :: rho
139   then    wrap e :: ty
140     and   'wrap' binds tvs, evs
141
142 ToDo: this eta-abstraction plays fast and loose with termination,
143       because it can introduce extra lambdas.  Maybe add a `seq` to
144       fix this
145
146
147 \begin{code}
148 deeplySkolemise
149   :: TcSigmaType
150   -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)
151
152 deeplySkolemise ty
153   | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
154   = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
155        ; tvs1 <- tcInstSkolTyVars tvs
156        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1)
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   = addDictLoc ispec $
479     addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
480                2 (pprInstances (ispec:ispecs)))
481 dupInstErr :: ClsInst -> ClsInst -> TcRn ()
482 dupInstErr ispec dup_ispec
483   = addDictLoc ispec $
484     addErr (hang (ptext (sLit "Duplicate instance declarations:"))
485                2 (pprInstances [ispec, dup_ispec]))
486 overlappingInstErr :: ClsInst -> ClsInst -> TcRn ()
487 overlappingInstErr ispec dup_ispec
488   = addDictLoc ispec $
489     addErr (hang (ptext (sLit "Overlapping instance declarations:"))
490                2 (pprInstances [ispec, dup_ispec]))
491
492 addDictLoc :: ClsInst -> TcRn a -> TcRn a
493 addDictLoc ispec thing_inside
494   = setSrcSpan (mkSrcSpan loc loc) thing_inside
495   where
496    loc = getSrcLoc ispec
497 \end{code}
498
499 %************************************************************************
500 %*                                                                      *
501         Simple functions over evidence variables
502 %*                                                                      *
503 %************************************************************************
504
505 \begin{code}
506 unitImplication :: Implication -> Bag Implication
507 unitImplication implic
508   | isEmptyWC (ic_wanted implic) = emptyBag
509   | otherwise                    = unitBag implic
510
511 hasEqualities :: [EvVar] -> Bool
512 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
513 hasEqualities givens = any (has_eq . evVarPred) givens
514   where
515     has_eq = has_eq' . classifyPredType
516
517     has_eq' (EqPred {})          = True
518     has_eq' (IPPred {})          = False
519     has_eq' (ClassPred cls _tys) = any has_eq (classSCTheta cls)
520     has_eq' (TuplePred ts)       = any has_eq ts
521     has_eq' (IrredPred _)        = True -- Might have equalities in it after reduction?
522
523 ---------------- Getting free tyvars -------------------------
524
525 tyVarsOfCt :: Ct -> TcTyVarSet
526 tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
527 tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
528 tyVarsOfCt (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
529 tyVarsOfCt (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
530 tyVarsOfCt (CIrredEvCan { cc_ty = ty })                 = tyVarsOfType ty
531 tyVarsOfCt (CNonCanonical { cc_id = ev })               = tyVarsOfEvVar ev
532
533 tyVarsOfCDict :: Ct -> TcTyVarSet 
534 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
535 tyVarsOfCDict _ct                            = emptyVarSet 
536
537 tyVarsOfCDicts :: Cts -> TcTyVarSet 
538 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
539
540 tyVarsOfCts :: Cts -> TcTyVarSet
541 tyVarsOfCts = foldrBag (unionVarSet . tyVarsOfCt) emptyVarSet
542
543 tyVarsOfWC :: WantedConstraints -> TyVarSet
544 tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
545   = tyVarsOfCts flat `unionVarSet`
546     tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
547     tyVarsOfCts insol
548
549 tyVarsOfImplication :: Implication -> TyVarSet
550 tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
551   = tyVarsOfWC wanted `delVarSetList` skols
552
553 tyVarsOfEvVar :: EvVar -> TyVarSet
554 tyVarsOfEvVar ev = tyVarsOfType $ evVarPred ev
555
556 tyVarsOfEvVars :: [EvVar] -> TyVarSet
557 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
558
559 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
560 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
561
562 ---------------- Tidying -------------------------
563
564 tidyCt :: TidyEnv -> Ct -> Ct
565 -- Also converts it to non-canonical
566 tidyCt env ct 
567   = CNonCanonical { cc_id     = tidyEvVar env (cc_id ct)
568                   , cc_flavor = tidyFlavor env (cc_flavor ct)
569                   , cc_depth  = cc_depth ct } 
570
571 tidyEvVar :: TidyEnv -> EvVar -> EvVar
572 tidyEvVar env var = setVarType var (tidyType env (varType var))
573
574 tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
575 tidyFlavor env (Given loc gk) = Given (tidyGivenLoc env loc) gk
576 tidyFlavor _   fl          = fl
577
578 tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
579 tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
580
581 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
582 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
583 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
584 tidySkolemInfo env (UnifyForAllSkol skol_tvs ty) 
585   = UnifyForAllSkol (map tidy_tv skol_tvs) (tidyType env ty)
586   where
587     tidy_tv tv = case getTyVar_maybe ty' of
588                    Just tv' -> tv'
589                    Nothing  -> pprPanic "ticySkolemInfo" (ppr tv <+> ppr ty')
590                where
591                  ty' = tidyTyVarOcc env tv
592 tidySkolemInfo _   info            = info
593
594 ---------------- Substitution -------------------------
595 substCt :: TvSubst -> Ct -> Ct 
596 -- Conservatively converts it to non-canonical:
597 -- Postcondition: if the constraint does not get rewritten
598 substCt subst ct
599   | ev <- cc_id ct, pty <- evVarPred (cc_id ct) 
600   , sty <- substTy subst pty 
601   = if sty `eqType` pty then 
602         ct { cc_flavor = substFlavor subst (cc_flavor ct) }
603     else 
604         CNonCanonical { cc_id  = setVarType ev sty 
605                       , cc_flavor = substFlavor subst (cc_flavor ct)
606                       , cc_depth  = cc_depth ct }
607
608 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
609 substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
610   = WC { wc_flat  = mapBag (substCt subst) flat
611        , wc_impl  = mapBag (substImplication subst) implic
612        , wc_insol = mapBag (substCt subst) insol }
613
614 substImplication :: TvSubst -> Implication -> Implication
615 substImplication subst implic@(Implic { ic_skols = tvs
616                                       , ic_given = given
617                                       , ic_wanted = wanted
618                                       , ic_loc = loc })
619   = implic { ic_skols  = tvs'
620            , ic_given  = map (substEvVar subst1) given
621            , ic_wanted = substWC subst1 wanted
622            , ic_loc    = substGivenLoc subst1 loc }
623   where
624    (subst1, tvs') = mapAccumL substTyVarBndr subst tvs
625
626 substEvVar :: TvSubst -> EvVar -> EvVar
627 substEvVar subst var = setVarType var (substTy subst (varType var))
628
629 substFlavor :: TvSubst -> CtFlavor -> CtFlavor
630 substFlavor subst (Given loc gk) = Given (substGivenLoc subst loc) gk
631 substFlavor _     fl             = fl
632
633 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
634 substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
635
636 substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
637 substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
638 substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
639 substSkolemInfo _     info            = info
640 \end{code}