Inst.lhs 21 KB
Newer Older
1
%
Simon Marlow's avatar
Simon Marlow committed
2
% (c) The University of Glasgow 2006
3
% (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
%
Simon Marlow's avatar
Simon Marlow committed
5
6

The @Inst@ type: dictionaries or method instances
7
8

\begin{code}
9
module Inst ( 
10
11
12
13
14
15
16
17
18
19
20
       deeplySkolemise, 
       deeplyInstantiate, instCall, instStupidTheta,
       emitWanted, emitWanteds,

       newOverloadedLit, mkOverLit, 
     
       tcGetInstEnvs, getOverlapFlag, tcExtendLocalInstEnv,
       instCallConstraints, newMethodFromName,
       tcSyntaxName,

       -- Simple functions over evidence variables
21
       hasEqualities, unitImplication,
22
       
23
       tyVarsOfWC, tyVarsOfBag, tyVarsOfEvVarXs, tyVarsOfEvVarX,
24
       tyVarsOfEvVar, tyVarsOfEvVars, tyVarsOfImplication,
25

26
27
28
29
30
       tidyWantedEvVar, tidyWantedEvVars, tidyWC,
       tidyEvVar, tidyImplication, tidyFlavoredEvVar,

       substWantedEvVar, substWantedEvVars, substFlavoredEvVar,
       substEvVar, substImplication
31
32
    ) where

33
#include "HsVersions.h"
34

35
36
import {-# SOURCE #-}	TcExpr( tcPolyExpr, tcSyntaxOp )
import {-# SOURCE #-}	TcUnify( unifyType )
37

38
import FastString
Simon Marlow's avatar
Simon Marlow committed
39
40
import HsSyn
import TcHsSyn
41
import TcRnMonad
Simon Marlow's avatar
Simon Marlow committed
42
43
44
45
46
import TcEnv
import InstEnv
import FunDeps
import TcMType
import TcType
47
import Class
Simon Marlow's avatar
Simon Marlow committed
48
49
50
51
52
import Unify
import Coercion
import HscTypes
import Id
import Name
53
import Var
Simon Marlow's avatar
Simon Marlow committed
54
55
56
57
58
import VarEnv
import VarSet
import PrelNames
import SrcLoc
import DynFlags
59
import Bag
Simon Marlow's avatar
Simon Marlow committed
60
import Maybes
61
import Util
62
import Outputable
63
import Data.List( mapAccumL )
64
65
\end{code}

66
67


68
69
70
71
72
%************************************************************************
%*									*
		Emitting constraints
%*									*
%************************************************************************
73
74

\begin{code}
75
76
77
78
79
80
emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
emitWanteds origin theta = mapM (emitWanted origin) theta

emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
emitWanted origin pred = do { loc <- getCtLoc origin
                            ; ev  <- newWantedEvVar pred
81
                            ; emitFlat (mkEvVarX ev loc)
82
83
84
85
86
87
88
89
90
91
92
93
                            ; return ev }

newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
-- Used when Name is the wired-in name for a wired-in class method,
-- so the caller knows its type for sure, which should be of form
--    forall a. C a => <blah>
-- newMethodFromName is supposed to instantiate just the outer 
-- type variable and constraint

newMethodFromName origin name inst_ty
  = do { id <- tcLookupId name
 	      -- Use tcLookupId not tcLookupGlobalId; the method is almost
94
	      -- always a class op, but with -XRebindableSyntax GHC is
95
96
97
98
99
100
101
102
103
104
	      -- meant to find whatever thing is in scope, and that may
	      -- be an ordinary function. 

       ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
             (the_tv:rest) = tvs
             subst = zipOpenTvSubst [the_tv] [inst_ty]

       ; wrap <- ASSERT( null rest && isSingleton theta )
                 instCall origin [inst_ty] (substTheta subst theta)
       ; return (mkHsWrap wrap (HsVar id)) }
105
106
107
108
109
\end{code}


%************************************************************************
%*									*
110
	Deep instantiation and skolemisation
111
112
113
%*									*
%************************************************************************

114
115
116
117
Note [Deep skolemisation]
~~~~~~~~~~~~~~~~~~~~~~~~~
deeplySkolemise decomposes and skolemises a type, returning a type
with all its arrows visible (ie not buried under foralls)
118

119
Examples:
120

121
122
123
  deeplySkolemise (Int -> forall a. Ord a => blah)  
    =  ( wp, [a], [d:Ord a], Int -> blah )
    where wp = \x:Int. /\a. \(d:Ord a). <hole> x
124

125
126
127
  deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)  
    =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
    where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
128

129
130
131
132
133
In general,
  if      deeplySkolemise ty = (wrap, tvs, evs, rho)
    and   e :: rho
  then    wrap e :: ty
    and   'wrap' binds tvs, evs
134

135
136
137
ToDo: this eta-abstraction plays fast and loose with termination,
      because it can introduce extra lambdas.  Maybe add a `seq` to
      fix this
138

139

140
141
\begin{code}
deeplySkolemise
142
  :: TcSigmaType
143
144
  -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)

145
deeplySkolemise ty
146
  | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
147
  = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
148
       ; tvs1 <- tcInstSkolTyVars tvs
149
150
       ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1)
       ; ev_vars1 <- newEvVars (substTheta subst theta)
151
       ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
152
153
154
155
156
157
158
159
       ; return ( mkWpLams ids1
                   <.> mkWpTyLams tvs1
                   <.> mkWpLams ev_vars1
                   <.> wrap
                   <.> mkWpEvVarApps ids1
                , tvs1     ++ tvs2
                , ev_vars1 ++ ev_vars2
                , mkFunTys arg_tys rho ) }
160

161
162
163
164
165
166
167
168
169
170
171
172
173
  | otherwise
  = return (idHsWrapper, [], [], ty)

deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
--   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
-- In general if
-- if    deeplyInstantiate ty = (wrap, rho)
-- and   e :: ty
-- then  wrap e :: rho

deeplyInstantiate orig ty
  | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
  = do { (_, tys, subst) <- tcInstTyVars tvs
174
       ; ids1  <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
175
       ; wrap1 <- instCall orig tys (substTheta subst theta)
176
       ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
177
       ; return (mkWpLams ids1 
178
                    <.> wrap2
179
                    <.> wrap1 
180
181
                    <.> mkWpEvVarApps ids1,
                 mkFunTys arg_tys rho2) }
182
183

  | otherwise = return (idHsWrapper, ty)
184
\end{code}
185

186

187
188
%************************************************************************
%*									*
189
            Instantiating a call
190
191
%*									*
%************************************************************************
192

193
194
\begin{code}
----------------
195
instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
196
197
198
199
-- Instantiate the constraints of a call
--	(instCall o tys theta)
-- (a) Makes fresh dictionaries as necessary for the constraints (theta)
-- (b) Throws these dictionaries into the LIE
200
-- (c) Returns an HsWrapper ([.] tys dicts)
201
202

instCall orig tys theta 
203
  = do	{ dict_app <- instCallConstraints orig theta
204
	; return (dict_app <.> mkWpTyApps tys) }
205
206

----------------
207
instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
208
209
-- Instantiates the TcTheta, puts all constraints thereby generated
-- into the LIE, and returns a HsWrapper to enclose the call site.
210

211
instCallConstraints _ [] = return idHsWrapper
212

213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
instCallConstraints origin (EqPred ty1 ty2 : preds)	-- Try short-cut
  = do  { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2)
	; coi   <- unifyType ty1 ty2
	; co_fn <- instCallConstraints origin preds
	; let co = case coi of
                       IdCo ty -> ty
                       ACo  co -> co
        ; return (co_fn <.> WpEvApp (EvCoercion co)) }

instCallConstraints origin (pred : preds)
  = do	{ ev_var <- emitWanted origin pred
	; co_fn <- instCallConstraints origin preds
	; return (co_fn <.> WpEvApp (EvId ev_var)) }

----------------
instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
-- Similar to instCall, but only emit the constraints in the LIE
-- Used exclusively for the 'stupid theta' of a data constructor
instStupidTheta orig theta
  = do	{ _co <- instCallConstraints orig theta -- Discard the coercion
	; return () }
234
\end{code}
235

236
237
%************************************************************************
%*									*
238
		Literals
239
240
241
%*									*
%************************************************************************

242
243
244
245
In newOverloadedLit we convert directly to an Int or Integer if we
know that's what we want.  This may save some time, by not
temporarily generating overloaded literals, but it won't catch all
cases (the rest are caught in lookupInst).
246

247
\begin{code}
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
newOverloadedLit :: CtOrigin
		 -> HsOverLit Name
		 -> TcRhoType
		 -> TcM (HsOverLit TcId)
newOverloadedLit orig 
  lit@(OverLit { ol_val = val, ol_rebindable = rebindable
	       , ol_witness = meth_name }) res_ty

  | not rebindable
  , Just expr <- shortCutLit val res_ty 
	-- Do not generate a LitInst for rebindable syntax.  
	-- Reason: If we do, tcSimplify will call lookupInst, which
	--	   will call tcSyntaxName, which does unification, 
	--	   which tcSimplify doesn't like
  = return (lit { ol_witness = expr, ol_type = res_ty })
263

264
265
266
267
268
269
270
271
272
273
274
275
  | otherwise
  = do	{ hs_lit <- mkOverLit val
	; let lit_ty = hsLitType hs_lit
	; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
	 	-- Overloaded literals must have liftedTypeKind, because
	 	-- we're instantiating an overloaded function here,
	 	-- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
		-- However this'll be picked up by tcSyntaxOp if necessary
	; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
	; return (lit { ol_witness = witness, ol_type = res_ty }) }

------------
276
277
278
279
280
281
282
283
mkOverLit :: OverLitVal -> TcM HsLit
mkOverLit (HsIntegral i) 
  = do	{ integer_ty <- tcMetaTy integerTyConName
	; return (HsInteger i integer_ty) }

mkOverLit (HsFractional r)
  = do	{ rat_ty <- tcMetaTy rationalTyConName
	; return (HsRat r rat_ty) }
Ian Lynagh's avatar
Ian Lynagh committed
284

285
mkOverLit (HsIsString s) = return (HsString s)
286
287
288
\end{code}


289
290


291
292
%************************************************************************
%*									*
293
294
295
		Re-mappable syntax
    
     Used only for arrow syntax -- find a way to nuke this
296
297
%*									*
%************************************************************************
298

299
Suppose we are doing the -XRebindableSyntax thing, and we encounter
300
301
302
303
a do-expression.  We have to find (>>) in the current environment, which is
done by the rename. Then we have to check that it has the same type as
Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
this:
304

305
  (>>) :: HB m n mn => m a -> n b -> mn b
306

307
So the idea is to generate a local binding for (>>), thus:
308

309
310
311
312
313
314
315
	let then72 :: forall a b. m a -> m b -> m b
	    then72 = ...something involving the user's (>>)...
	in
	...the do-expression...

Now the do-expression can proceed using then72, which has exactly
the expected type.
316

317
318
319
In fact tcSyntaxName just generates the RHS for then72, because we only
want an actual binding in the do-expression case. For literals, we can 
just use the expression inline.
320
321

\begin{code}
322
323
324
325
326
327
328
tcSyntaxName :: CtOrigin
	     -> TcType			-- Type to instantiate it at
	     -> (Name, HsExpr Name)	-- (Standard name, user name)
	     -> TcM (Name, HsExpr TcId)	-- (Standard name, suitable expression)
--	*** NOW USED ONLY FOR CmdTop (sigh) ***
-- NB: tcSyntaxName calls tcExpr, and hence can do unification.
-- So we do not call it from lookupInst, which is called from tcSimplify
329

330
331
332
333
tcSyntaxName orig ty (std_nm, HsVar user_nm)
  | std_nm == user_nm
  = do rhs <- newMethodFromName orig std_nm ty
       return (std_nm, rhs)
334

335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
tcSyntaxName orig ty (std_nm, user_nm_expr) = do
    std_id <- tcLookupId std_nm
    let	
	-- C.f. newMethodAtLoc
	([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
 	sigma1		= substTyWith [tv] [ty] tau
	-- Actually, the "tau-type" might be a sigma-type in the
	-- case of locally-polymorphic methods.

    addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do

	-- Check that the user-supplied thing has the
	-- same type as the standard one.  
	-- Tiresome jiggling because tcCheckSigma takes a located expression
     span <- getSrcSpanM
     expr <- tcPolyExpr (L span user_nm_expr) sigma1
     return (std_nm, unLoc expr)
352

353
354
355
356
357
358
359
360
361
362
syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
               -> TcRn (TidyEnv, SDoc)
syntaxNameCtxt name orig ty tidy_env = do
    inst_loc <- getCtLoc orig
    let
	msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+> 
				ptext (sLit "(needed by a syntactic construct)"),
		    nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
		    nest 2 (pprArisingAt inst_loc)]
    return (tidy_env, msg)
363
364
365
\end{code}


366
367
%************************************************************************
%*									*
368
		Instances
369
370
371
372
%*									*
%************************************************************************

\begin{code}
373
374
375
getOverlapFlag :: TcM OverlapFlag
getOverlapFlag 
  = do 	{ dflags <- getDOpts
376
377
	; let overlap_ok    = xopt Opt_OverlappingInstances dflags
	      incoherent_ok = xopt Opt_IncoherentInstances  dflags
378
379
380
381
382
383
384
385
386
387
388
389
	      overlap_flag | incoherent_ok = Incoherent
			   | overlap_ok    = OverlapOk
			   | otherwise     = NoOverlap
			   
	; return overlap_flag }

tcGetInstEnvs :: TcM (InstEnv, InstEnv)
-- Gets both the external-package inst-env
-- and the home-pkg inst env (includes module being compiled)
tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
		     return (eps_inst_env eps, tcg_inst_env env) }

390
tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
391
392
393
394
  -- Add new locally-defined instances
tcExtendLocalInstEnv dfuns thing_inside
 = do { traceDFuns dfuns
      ; env <- getGblEnv
395
      ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
396
397
398
      ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
			 tcg_inst_env = inst_env' }
      ; setGblEnv env' thing_inside }
399

400
addLocalInst :: InstEnv -> Instance -> TcM InstEnv
401
402
-- Check that the proposed new instance is OK, 
-- and then add it to the home inst env
403
addLocalInst home_ie ispec
404
405
  = do	{ 	-- Instantiate the dfun type so that we extend the instance
		-- envt with completely fresh template variables
406
407
408
		-- This is important because the template variables must
		-- not overlap with anything in the things being looked up
		-- (since we do unification).  
409
410
411
412
413
414
415
416
417
418
                --
                -- We use tcInstSkolType because we don't want to allocate fresh
                --  *meta* type variables.
                --
                -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
                -- these variables must be bindable by tcUnifyTys.  See
                -- the call to tcUnifyTys in InstEnv, and the special
                -- treatment that instanceBindFun gives to isOverlappableTyVar
                -- This is absurdly delicate.

419
	  let dfun = instanceDFunId ispec
420
        ; (tvs', theta', tau') <- tcInstSkolType (idType dfun)
421
422
	; let	(cls, tys') = tcSplitDFunHead tau'
		dfun' 	    = setIdType dfun (mkSigmaTy tvs' theta' tau')	    
423
	  	ispec'      = setInstanceDFunId ispec dfun'
424
425

		-- Load imported instances, so that we report
426
		-- duplicates correctly
427
428
	; eps <- getEps
	; let inst_envs = (eps_inst_env eps, home_ie)
429
430

		-- Check functional dependencies
431
432
	; case checkFunDeps inst_envs ispec' of
		Just specs -> funDepErr ispec' specs
433
		Nothing    -> return ()
434
435

		-- Check for duplicate instance decls
436
437
	; let { (matches, _) = lookupInstEnv inst_envs cls tys'
	      ;	dup_ispecs = [ dup_ispec 
438
			     | (dup_ispec, _) <- matches
439
440
441
442
443
444
445
			     , let (_,_,_,dup_tys) = instanceHead dup_ispec
			     , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
		-- Find memebers of the match list which ispec itself matches.
		-- If the match is 2-way, it's a duplicate
	; case dup_ispecs of
	    dup_ispec : _ -> dupInstErr ispec' dup_ispec
	    []            -> return ()
446
447

		-- OK, now extend the envt
448
449
	; return (extendInstEnv home_ie ispec') }

Ian Lynagh's avatar
Ian Lynagh committed
450
traceDFuns :: [Instance] -> TcRn ()
451
traceDFuns ispecs
452
  = traceTc "Adding instances:" (vcat (map pp ispecs))
453
  where
454
455
    pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
	-- Print the dfun name itself too
456

Ian Lynagh's avatar
Ian Lynagh committed
457
funDepErr :: Instance -> [Instance] -> TcRn ()
458
459
funDepErr ispec ispecs
  = addDictLoc ispec $
Ian Lynagh's avatar
Ian Lynagh committed
460
    addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
461
	       2 (pprInstances (ispec:ispecs)))
Ian Lynagh's avatar
Ian Lynagh committed
462
dupInstErr :: Instance -> Instance -> TcRn ()
463
464
dupInstErr ispec dup_ispec
  = addDictLoc ispec $
Ian Lynagh's avatar
Ian Lynagh committed
465
    addErr (hang (ptext (sLit "Duplicate instance declarations:"))
466
	       2 (pprInstances [ispec, dup_ispec]))
467

Ian Lynagh's avatar
Ian Lynagh committed
468
addDictLoc :: Instance -> TcRn a -> TcRn a
469
addDictLoc ispec thing_inside
470
  = setSrcSpan (mkSrcSpan loc loc) thing_inside
471
  where
472
   loc = getSrcLoc ispec
473
474
\end{code}

475
476
%************************************************************************
%*									*
477
	Simple functions over evidence variables
478
479
480
481
%*									*
%************************************************************************

\begin{code}
482
483
484
485
486
unitImplication :: Implication -> Bag Implication
unitImplication implic
  | isEmptyWC (ic_wanted implic) = emptyBag
  | otherwise                    = unitBag implic

487
488
489
hasEqualities :: [EvVar] -> Bool
-- Has a bunch of canonical constraints (all givens) got any equalities in it?
hasEqualities givens = any (has_eq . evVarPred) givens
490
  where
491
492
493
    has_eq (EqPred {}) 	     = True
    has_eq (IParam {}) 	     = False
    has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls)
494

495
496
497
498
499
500
---------------- Getting free tyvars -------------------------
tyVarsOfWC :: WantedConstraints -> TyVarSet
tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
  = tyVarsOfEvVarXs flat `unionVarSet`
    tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
    tyVarsOfEvVarXs insol
501

502
tyVarsOfImplication :: Implication -> TyVarSet
503
504
tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
  = tyVarsOfWC wanted `minusVarSet` skols
505

506
507
tyVarsOfEvVarX :: EvVarX a -> TyVarSet
tyVarsOfEvVarX (EvVarX ev _) = tyVarsOfEvVar ev
508

509
510
tyVarsOfEvVarXs :: Bag (EvVarX a) -> TyVarSet
tyVarsOfEvVarXs = tyVarsOfBag tyVarsOfEvVarX
511

512
513
tyVarsOfEvVar :: EvVar -> TyVarSet
tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev
514

515
516
tyVarsOfEvVars :: [EvVar] -> TyVarSet
tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
517

518
519
520
521
522
523
524
525
526
tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet

---------------- Tidying -------------------------
tidyWC :: TidyEnv -> WantedConstraints -> WantedConstraints
tidyWC env (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
  = WC { wc_flat  = tidyWantedEvVars env flat
       , wc_impl  = mapBag (tidyImplication env) implic
       , wc_insol = mapBag (tidyFlavoredEvVar env) insol }
527

528
529
530
531
532
533
534
535
536
537
538
539
540
541
tidyImplication :: TidyEnv -> Implication -> Implication
tidyImplication env implic@(Implic { ic_skols = tvs
                                   , ic_given = given
                                   , ic_wanted = wanted
                                   , ic_loc = loc })
  = implic { ic_skols = mkVarSet tvs'
           , ic_given = map (tidyEvVar env1) given
           , ic_wanted = tidyWC env1 wanted
           , ic_loc = tidyGivenLoc env1 loc }
  where
   (env1, tvs') = mapAccumL tidyTyVarBndr env (varSetElems tvs)

tidyEvVar :: TidyEnv -> EvVar -> EvVar
tidyEvVar env var = setVarType var (tidyType env (varType var))
542

543
tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar
544
tidyWantedEvVar env (EvVarX v l) = EvVarX (tidyEvVar env v) l
545

546
547
tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar
tidyWantedEvVars env = mapBag (tidyWantedEvVar env)
548

549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
tidyFlavoredEvVar :: TidyEnv -> FlavoredEvVar -> FlavoredEvVar
tidyFlavoredEvVar env (EvVarX v fl)
  = EvVarX (tidyEvVar env v) (tidyFlavor env fl)

tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc)
tidyFlavor _   fl          = fl

tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt

tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
tidySkolemInfo _   info            = info

---------------- Substitution -------------------------
substWC :: TvSubst -> WantedConstraints -> WantedConstraints
substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
  = WC { wc_flat = substWantedEvVars subst flat
       , wc_impl = mapBag (substImplication subst) implic
       , wc_insol = mapBag (substFlavoredEvVar subst) insol }

substImplication :: TvSubst -> Implication -> Implication
substImplication subst implic@(Implic { ic_skols = tvs
                                      , ic_given = given
                                      , ic_wanted = wanted
                                      , ic_loc = loc })
  = implic { ic_skols  = mkVarSet tvs'
           , ic_given  = map (substEvVar subst1) given
           , ic_wanted = substWC subst1 wanted
           , ic_loc    = substGivenLoc subst1 loc }
581
  where
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
   (subst1, tvs') = mapAccumL substTyVarBndr subst (varSetElems tvs)

substEvVar :: TvSubst -> EvVar -> EvVar
substEvVar subst var = setVarType var (substTy subst (varType var))

substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar
substWantedEvVars subst = mapBag (substWantedEvVar subst)

substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar
substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l

substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar
substFlavoredEvVar subst (EvVarX v fl)
  = EvVarX (substEvVar subst v) (substFlavor subst fl)

substFlavor :: TvSubst -> CtFlavor -> CtFlavor
substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
substFlavor _     fl          = fl

substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt

substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
substSkolemInfo _     info            = info
608
\end{code}