Hurrah! This major commit adds support for scoped kind variables,
[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        ; (subst, tvs1) <- tcInstSkolTyVars tvs
156        ; ev_vars1 <- newEvVars (substTheta subst theta)
157        ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
158        ; return ( mkWpLams ids1
159                    <.> mkWpTyLams tvs1
160                    <.> mkWpLams ev_vars1
161                    <.> wrap
162                    <.> mkWpEvVarApps ids1
163                 , tvs1     ++ tvs2
164                 , ev_vars1 ++ ev_vars2
165                 , mkFunTys arg_tys rho ) }
166
167   | otherwise
168   = return (idHsWrapper, [], [], ty)
169
170 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
171 --   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
172 -- In general if
173 -- if    deeplyInstantiate ty = (wrap, rho)
174 -- and   e :: ty
175 -- then  wrap e :: rho
176
177 deeplyInstantiate orig ty
178   | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
179   = do { (_, tys, subst) <- tcInstTyVars tvs
180        ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
181        ; wrap1 <- instCall orig tys (substTheta subst theta)
182        ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
183        ; return (mkWpLams ids1 
184                     <.> wrap2
185                     <.> wrap1 
186                     <.> mkWpEvVarApps ids1,
187                  mkFunTys arg_tys rho2) }
188
189   | otherwise = return (idHsWrapper, ty)
190 \end{code}
191
192
193 %************************************************************************
194 %*                                                                      *
195             Instantiating a call
196 %*                                                                      *
197 %************************************************************************
198
199 \begin{code}
200 ----------------
201 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
202 -- Instantiate the constraints of a call
203 --      (instCall o tys theta)
204 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
205 -- (b) Throws these dictionaries into the LIE
206 -- (c) Returns an HsWrapper ([.] tys dicts)
207
208 instCall orig tys theta 
209   = do  { dict_app <- instCallConstraints orig theta
210         ; return (dict_app <.> mkWpTyApps tys) }
211
212 ----------------
213 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
214 -- Instantiates the TcTheta, puts all constraints thereby generated
215 -- into the LIE, and returns a HsWrapper to enclose the call site.
216
217 instCallConstraints _ [] = return idHsWrapper
218
219 instCallConstraints origin (pred : preds)
220   | Just (ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut
221   = do  { traceTc "instCallConstraints" $ ppr (mkEqPred ty1 ty2)
222         ; co <- unifyType ty1 ty2
223         ; co_fn <- instCallConstraints origin preds
224         ; return (co_fn <.> WpEvApp (EvCoercion co)) }
225
226   | otherwise
227   = do  { ev_var <- emitWanted origin pred
228         ; co_fn <- instCallConstraints origin preds
229         ; return (co_fn <.> WpEvApp (EvId ev_var)) }
230
231 ----------------
232 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
233 -- Similar to instCall, but only emit the constraints in the LIE
234 -- Used exclusively for the 'stupid theta' of a data constructor
235 instStupidTheta orig theta
236   = do  { _co <- instCallConstraints orig theta -- Discard the coercion
237         ; return () }
238 \end{code}
239
240 %************************************************************************
241 %*                                                                      *
242                 Literals
243 %*                                                                      *
244 %************************************************************************
245
246 In newOverloadedLit we convert directly to an Int or Integer if we
247 know that's what we want.  This may save some time, by not
248 temporarily generating overloaded literals, but it won't catch all
249 cases (the rest are caught in lookupInst).
250
251 \begin{code}
252 newOverloadedLit :: CtOrigin
253                  -> HsOverLit Name
254                  -> TcRhoType
255                  -> TcM (HsOverLit TcId)
256 newOverloadedLit orig 
257   lit@(OverLit { ol_val = val, ol_rebindable = rebindable
258                , ol_witness = meth_name }) res_ty
259
260   | not rebindable
261   , Just expr <- shortCutLit val res_ty 
262         -- Do not generate a LitInst for rebindable syntax.  
263         -- Reason: If we do, tcSimplify will call lookupInst, which
264         --         will call tcSyntaxName, which does unification, 
265         --         which tcSimplify doesn't like
266   = return (lit { ol_witness = expr, ol_type = res_ty })
267
268   | otherwise
269   = do  { hs_lit <- mkOverLit val
270         ; let lit_ty = hsLitType hs_lit
271         ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
272                 -- Overloaded literals must have liftedTypeKind, because
273                 -- we're instantiating an overloaded function here,
274                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
275                 -- However this'll be picked up by tcSyntaxOp if necessary
276         ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
277         ; return (lit { ol_witness = witness, ol_type = res_ty }) }
278
279 ------------
280 mkOverLit :: OverLitVal -> TcM HsLit
281 mkOverLit (HsIntegral i) 
282   = do  { integer_ty <- tcMetaTy integerTyConName
283         ; return (HsInteger i integer_ty) }
284
285 mkOverLit (HsFractional r)
286   = do  { rat_ty <- tcMetaTy rationalTyConName
287         ; return (HsRat r rat_ty) }
288
289 mkOverLit (HsIsString s) = return (HsString s)
290 \end{code}
291
292
293
294
295 %************************************************************************
296 %*                                                                      *
297                 Re-mappable syntax
298     
299      Used only for arrow syntax -- find a way to nuke this
300 %*                                                                      *
301 %************************************************************************
302
303 Suppose we are doing the -XRebindableSyntax thing, and we encounter
304 a do-expression.  We have to find (>>) in the current environment, which is
305 done by the rename. Then we have to check that it has the same type as
306 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
307 this:
308
309   (>>) :: HB m n mn => m a -> n b -> mn b
310
311 So the idea is to generate a local binding for (>>), thus:
312
313         let then72 :: forall a b. m a -> m b -> m b
314             then72 = ...something involving the user's (>>)...
315         in
316         ...the do-expression...
317
318 Now the do-expression can proceed using then72, which has exactly
319 the expected type.
320
321 In fact tcSyntaxName just generates the RHS for then72, because we only
322 want an actual binding in the do-expression case. For literals, we can 
323 just use the expression inline.
324
325 \begin{code}
326 tcSyntaxName :: CtOrigin
327              -> TcType                  -- Type to instantiate it at
328              -> (Name, HsExpr Name)     -- (Standard name, user name)
329              -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
330 --      *** NOW USED ONLY FOR CmdTop (sigh) ***
331 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
332 -- So we do not call it from lookupInst, which is called from tcSimplify
333
334 tcSyntaxName orig ty (std_nm, HsVar user_nm)
335   | std_nm == user_nm
336   = do rhs <- newMethodFromName orig std_nm ty
337        return (std_nm, rhs)
338
339 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
340     std_id <- tcLookupId std_nm
341     let 
342         -- C.f. newMethodAtLoc
343         ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
344         sigma1          = substTyWith [tv] [ty] tau
345         -- Actually, the "tau-type" might be a sigma-type in the
346         -- case of locally-polymorphic methods.
347
348     addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
349
350         -- Check that the user-supplied thing has the
351         -- same type as the standard one.  
352         -- Tiresome jiggling because tcCheckSigma takes a located expression
353      span <- getSrcSpanM
354      expr <- tcPolyExpr (L span user_nm_expr) sigma1
355      return (std_nm, unLoc expr)
356
357 syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
358                -> TcRn (TidyEnv, SDoc)
359 syntaxNameCtxt name orig ty tidy_env = do
360     inst_loc <- getCtLoc orig
361     let
362         msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+> 
363                                 ptext (sLit "(needed by a syntactic construct)"),
364                     nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
365                     nest 2 (pprArisingAt inst_loc)]
366     return (tidy_env, msg)
367 \end{code}
368
369
370 %************************************************************************
371 %*                                                                      *
372                 Instances
373 %*                                                                      *
374 %************************************************************************
375
376 \begin{code}
377 getOverlapFlag :: TcM OverlapFlag
378 getOverlapFlag 
379   = do  { dflags <- getDynFlags
380         ; let overlap_ok    = xopt Opt_OverlappingInstances dflags
381               incoherent_ok = xopt Opt_IncoherentInstances  dflags
382               safeOverlap   = safeLanguageOn dflags
383               overlap_flag | incoherent_ok = Incoherent safeOverlap
384                            | overlap_ok    = OverlapOk safeOverlap
385                            | otherwise     = NoOverlap safeOverlap
386
387         ; return overlap_flag }
388
389 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
390 -- Gets both the external-package inst-env
391 -- and the home-pkg inst env (includes module being compiled)
392 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
393                      return (eps_inst_env eps, tcg_inst_env env) }
394
395 tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
396   -- Add new locally-defined instances
397 tcExtendLocalInstEnv dfuns thing_inside
398  = do { traceDFuns dfuns
399       ; env <- getGblEnv
400       ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
401       ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
402                          tcg_inst_env = inst_env' }
403       ; setGblEnv env' thing_inside }
404
405 addLocalInst :: InstEnv -> ClsInst -> TcM InstEnv
406 -- Check that the proposed new instance is OK, 
407 -- and then add it to the home inst env
408 -- If overwrite_inst, then we can overwrite a direct match
409 addLocalInst home_ie ispec = do
410     -- Instantiate the dfun type so that we extend the instance
411     -- envt with completely fresh template variables
412     -- This is important because the template variables must
413     -- not overlap with anything in the things being looked up
414     -- (since we do unification).  
415         --
416         -- We use tcInstSkolType because we don't want to allocate fresh
417         --  *meta* type variables.
418         --
419         -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
420         -- these variables must be bindable by tcUnifyTys.  See
421         -- the call to tcUnifyTys in InstEnv, and the special
422         -- treatment that instanceBindFun gives to isOverlappableTyVar
423         -- This is absurdly delicate.
424
425     let dfun = instanceDFunId ispec
426     (tvs', theta', tau') <- tcInstSkolType (idType dfun)
427     let (cls, tys') = tcSplitDFunHead tau'
428         dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')           
429         ispec'      = setInstanceDFunId ispec dfun'
430
431         -- Load imported instances, so that we report
432         -- duplicates correctly
433     eps <- getEps
434     let inst_envs = (eps_inst_env eps, home_ie)
435
436         -- Check functional dependencies
437     case checkFunDeps inst_envs ispec' of
438         Just specs -> funDepErr ispec' specs
439         Nothing    -> return ()
440
441         -- Check for duplicate instance decls
442     let (matches, unifs, _) = lookupInstEnv inst_envs cls tys'
443         dup_ispecs = [ dup_ispec 
444                         | (dup_ispec, _) <- matches
445                         , let (_,_,_,dup_tys) = instanceHead dup_ispec
446                         , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)]
447                         
448         -- Find memebers of the match list which ispec itself matches.
449         -- If the match is 2-way, it's a duplicate
450         -- If it's a duplicate, but we can overwrite home package dups, then overwrite
451     isGHCi <- getIsGHCi
452     overlapFlag <- getOverlapFlag
453     case isGHCi of
454         False -> case dup_ispecs of
455             dup : _ -> dupInstErr ispec' dup >> return (extendInstEnv home_ie ispec')
456             []      -> return (extendInstEnv home_ie ispec')
457         True  -> case (dup_ispecs, home_ie_matches, unifs, overlapFlag) of
458             (_, _:_, _, _)      -> return (overwriteInstEnv home_ie ispec')
459             (dup:_, [], _, _)   -> dupInstErr ispec' dup >> return (extendInstEnv home_ie ispec')
460             ([], _, u:_, NoOverlap _)    -> overlappingInstErr ispec' u >> return (extendInstEnv home_ie ispec')
461             _                   -> return (extendInstEnv home_ie ispec')
462           where (homematches, _) = lookupInstEnv' home_ie cls tys'
463                 home_ie_matches = [ dup_ispec 
464                     | (dup_ispec, _) <- homematches
465                     , let (_,_,_,dup_tys) = instanceHead dup_ispec
466                     , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)]
467
468 traceDFuns :: [ClsInst] -> TcRn ()
469 traceDFuns ispecs
470   = traceTc "Adding instances:" (vcat (map pp ispecs))
471   where
472     pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
473         -- Print the dfun name itself too
474
475 funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
476 funDepErr ispec ispecs
477   = addDictLoc ispec $
478     addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
479                2 (pprInstances (ispec:ispecs)))
480 dupInstErr :: ClsInst -> ClsInst -> TcRn ()
481 dupInstErr ispec dup_ispec
482   = addDictLoc ispec $
483     addErr (hang (ptext (sLit "Duplicate instance declarations:"))
484                2 (pprInstances [ispec, dup_ispec]))
485 overlappingInstErr :: ClsInst -> ClsInst -> TcRn ()
486 overlappingInstErr ispec dup_ispec
487   = addDictLoc ispec $
488     addErr (hang (ptext (sLit "Overlapping instance declarations:"))
489                2 (pprInstances [ispec, dup_ispec]))
490
491 addDictLoc :: ClsInst -> TcRn a -> TcRn a
492 addDictLoc ispec thing_inside
493   = setSrcSpan (mkSrcSpan loc loc) thing_inside
494   where
495    loc = getSrcLoc ispec
496 \end{code}
497
498 %************************************************************************
499 %*                                                                      *
500         Simple functions over evidence variables
501 %*                                                                      *
502 %************************************************************************
503
504 \begin{code}
505 unitImplication :: Implication -> Bag Implication
506 unitImplication implic
507   | isEmptyWC (ic_wanted implic) = emptyBag
508   | otherwise                    = unitBag implic
509
510 hasEqualities :: [EvVar] -> Bool
511 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
512 hasEqualities givens = any (has_eq . evVarPred) givens
513   where
514     has_eq = has_eq' . classifyPredType
515
516     has_eq' (EqPred {})          = True
517     has_eq' (IPPred {})          = False
518     has_eq' (ClassPred cls _tys) = any has_eq (classSCTheta cls)
519     has_eq' (TuplePred ts)       = any has_eq ts
520     has_eq' (IrredPred _)        = True -- Might have equalities in it after reduction?
521
522 ---------------- Getting free tyvars -------------------------
523
524 tyVarsOfCt :: Ct -> TcTyVarSet
525 tyVarsOfCt (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
526 tyVarsOfCt (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
527 tyVarsOfCt (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
528 tyVarsOfCt (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
529 tyVarsOfCt (CIrredEvCan { cc_ty = ty })                 = tyVarsOfType ty
530 tyVarsOfCt (CNonCanonical { cc_id = ev })               = tyVarsOfEvVar ev
531
532 tyVarsOfCDict :: Ct -> TcTyVarSet 
533 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
534 tyVarsOfCDict _ct                            = emptyVarSet 
535
536 tyVarsOfCDicts :: Cts -> TcTyVarSet 
537 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
538
539 tyVarsOfCts :: Cts -> TcTyVarSet
540 tyVarsOfCts = foldrBag (unionVarSet . tyVarsOfCt) emptyVarSet
541
542 tyVarsOfWC :: WantedConstraints -> TyVarSet
543 tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
544   = tyVarsOfCts flat `unionVarSet`
545     tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
546     tyVarsOfCts insol
547
548 tyVarsOfImplication :: Implication -> TyVarSet
549 tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
550   = tyVarsOfWC wanted `delVarSetList` skols
551
552 tyVarsOfEvVar :: EvVar -> TyVarSet
553 tyVarsOfEvVar ev = tyVarsOfType $ evVarPred ev
554
555 tyVarsOfEvVars :: [EvVar] -> TyVarSet
556 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
557
558 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
559 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
560
561 ---------------- Tidying -------------------------
562
563 tidyCt :: TidyEnv -> Ct -> Ct
564 -- Also converts it to non-canonical
565 tidyCt env ct 
566   = CNonCanonical { cc_id     = tidyEvVar env (cc_id ct)
567                   , cc_flavor = tidyFlavor env (cc_flavor ct)
568                   , cc_depth  = cc_depth ct } 
569
570 tidyEvVar :: TidyEnv -> EvVar -> EvVar
571 tidyEvVar env var = setVarType var (tidyType env (varType var))
572
573 tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
574 tidyFlavor env (Given loc gk) = Given (tidyGivenLoc env loc) gk
575 tidyFlavor _   fl          = fl
576
577 tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
578 tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
579
580 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
581 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
582 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
583 tidySkolemInfo env (UnifyForAllSkol skol_tvs ty) 
584   = UnifyForAllSkol (map tidy_tv skol_tvs) (tidyType env ty)
585   where
586     tidy_tv tv = case getTyVar_maybe ty' of
587                    Just tv' -> tv'
588                    Nothing  -> pprPanic "ticySkolemInfo" (ppr tv <+> ppr ty')
589                where
590                  ty' = tidyTyVarOcc env tv
591 tidySkolemInfo _   info            = info
592
593 ---------------- Substitution -------------------------
594 substCt :: TvSubst -> Ct -> Ct 
595 -- Conservatively converts it to non-canonical:
596 -- Postcondition: if the constraint does not get rewritten
597 substCt subst ct
598   | ev <- cc_id ct, pty <- evVarPred (cc_id ct) 
599   , sty <- substTy subst pty 
600   = if sty `eqType` pty then 
601         ct { cc_flavor = substFlavor subst (cc_flavor ct) }
602     else 
603         CNonCanonical { cc_id  = setVarType ev sty 
604                       , cc_flavor = substFlavor subst (cc_flavor ct)
605                       , cc_depth  = cc_depth ct }
606
607 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
608 substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
609   = WC { wc_flat  = mapBag (substCt subst) flat
610        , wc_impl  = mapBag (substImplication subst) implic
611        , wc_insol = mapBag (substCt subst) insol }
612
613 substImplication :: TvSubst -> Implication -> Implication
614 substImplication subst implic@(Implic { ic_skols = tvs
615                                       , ic_given = given
616                                       , ic_wanted = wanted
617                                       , ic_loc = loc })
618   = implic { ic_skols  = tvs'
619            , ic_given  = map (substEvVar subst1) given
620            , ic_wanted = substWC subst1 wanted
621            , ic_loc    = substGivenLoc subst1 loc }
622   where
623    (subst1, tvs') = mapAccumL substTyVarBndr subst tvs
624
625 substEvVar :: TvSubst -> EvVar -> EvVar
626 substEvVar subst var = setVarType var (substTy subst (varType var))
627
628 substFlavor :: TvSubst -> CtFlavor -> CtFlavor
629 substFlavor subst (Given loc gk) = Given (substGivenLoc subst loc) gk
630 substFlavor _     fl             = fl
631
632 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
633 substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
634
635 substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
636 substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
637 substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
638 substSkolemInfo _     info            = info
639 \end{code}