TcSMonad.lhs 35.8 KB
Newer Older
1
2
3
4
5
6
\begin{code}
-- Type definitions for the constraint solver
module TcSMonad ( 

       -- Canonical constraints
    CanonicalCts, emptyCCan, andCCan, andCCans, 
7
8
9
    singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, 
    isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe, 

10
    CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
11
    mkWantedConstraints, deCanonicaliseWanted, 
12
    makeGivens, makeSolvedByInst,
13

14
    CtFlavor (..), isWanted, isGiven, isDerived, 
15
    isGivenCt, isWantedCt, pprFlavorArising,
16

17
18
    isFlexiTcsTv,

19
20
    DerivedOrig (..), 
    canRewrite, canSolve,
21
22
    combineCtLoc, mkGivenFlavor, mkWantedFlavor,
    getWantedLoc,
23
24

    TcS, runTcS, failTcS, panicTcS, traceTcS, traceTcS0,  -- Basic functionality 
25
    tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
    SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
       
       -- Creation of evidence variables

    newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar, 
    newIPVar, newDictVar, newKindConstraint,

       -- Setting evidence variables 
    setWantedCoBind, setDerivedCoBind, 
    setIPBind, setDictBind, setEvBind,

    setWantedTyBind,

    newTcEvBindsTcS,
 
    getInstEnvs, getFamInstEnvs,                -- Getting the environments 
42
    getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
43
44
45
46
    getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
    getTcSErrorsBag, FrozenError (..),
    addErrorTcS,
    ErrorKind(..),
47
48

    newFlattenSkolemTy,                         -- Flatten skolems 
49

50
51

    instDFunTypes,                              -- Instantiation
52
53
    instDFunConstraints,          
    newFlexiTcSTy, 
54
55
56

    isGoodRecEv,

57
58
59
    compatKind,


60
    TcsUntouchables,
61
    isTouchableMetaTyVar,
62
    isTouchableMetaTyVar_InRange, 
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99

    getDefaultInfo, getDynFlags,

    matchClass, matchFam, MatchInstResult (..), 
    checkWellStagedDFun, 
    warnTcS,
    pprEq,                                   -- Smaller utils, re-exported from TcM 
                                             -- TODO (DV): these are only really used in the 
                                             -- instance matcher in TcSimplify. I am wondering
                                             -- if the whole instance matcher simply belongs
                                             -- here 


    mkWantedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps

) where 

#include "HsVersions.h"

import HscTypes
import BasicTypes 

import Inst
import InstEnv 
import FamInst 
import FamInstEnv

import qualified TcRnMonad as TcM
import qualified TcMType as TcM
import qualified TcEnv as TcM 
       ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
import TcType
import DynFlags

import Coercion
import Class
import TyCon
100
101
import TypeRep 

102
103
import Name
import Var
104
import VarEnv
105
106
107
108
109
110
111
112
113
114
import Outputable
import Bag
import MonadUtils
import VarSet
import FastString

import HsBinds               -- for TcEvBinds stuff 
import Id 
import FunDeps

Ian Lynagh's avatar
Ian Lynagh committed
115
116
import TcRnTypes

117
import Control.Monad
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
import Data.IORef
\end{code}


%************************************************************************
%*									*
%*                       Canonical constraints                          *
%*                                                                      *
%*   These are the constraints the low-level simplifier works with      *
%*									*
%************************************************************************

\begin{code}
-- Types without any type functions inside.  However, note that xi
-- types CAN contain unexpanded type synonyms; however, the
-- (transitive) expansions of those type synonyms will not contain any
-- type functions.
type Xi = Type       -- In many comments, "xi" ranges over Xi

type CanonicalCts = Bag CanonicalCt
 
data CanonicalCt
  -- Atomic canonical constraints 
  = CDictCan {  -- e.g.  Num xi
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor, 
      cc_class  :: Class, 
      cc_tyargs :: [Xi]
    }

  | CIPCan {	-- ?x::tau
      -- See note [Canonical implicit parameter constraints].
      cc_id     :: EvVar,
151
      cc_flavor :: CtFlavor,
152
153
154
155
156
157
158
      cc_ip_nm  :: IPName Name,
      cc_ip_ty  :: TcTauType
    }

  | CTyEqCan {  -- tv ~ xi	(recall xi means function free)
       -- Invariant: 
       --   * tv not in tvs(xi)   (occurs check)
159
160
       --   * If constraint is given then typeKind xi `compatKind` typeKind tv 
       --                See Note [Spontaneous solving and kind compatibility] 
161
       --   * We prefer unification variables on the left *JUST* for efficiency
162
163
      cc_id     :: EvVar, 
      cc_flavor :: CtFlavor, 
164
165
      cc_tyvar  :: TcTyVar, 
      cc_rhs    :: Xi
166
167
168
169
    }

  | CFunEqCan {  -- F xis ~ xi  
                 -- Invariant: * isSynFamilyTyCon cc_fun 
170
                 --            * If constraint is given then 
171
                 --                 typeKind (F xis) `compatKind` typeKind xi
172
173
174
175
176
177
178
179
180
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor, 
      cc_fun    :: TyCon,	-- A type function
      cc_tyargs :: [Xi],	-- Either under-saturated or exactly saturated
      cc_rhs    :: Xi      	--    *never* over-saturated (because if so
      		      		--    we should have decomposed)
                   
    }

181
182
183
compatKind :: Kind -> Kind -> Bool 
compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 

184
185
186
187
188
makeGivens :: CanonicalCts -> CanonicalCts
makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
	   -- The UnkSkol doesn't matter because these givens are
	   -- not contradictory (else we'd have rejected them already)

189
makeSolvedByInst :: CanonicalCt -> CanonicalCt
190
191
192
-- Record that a constraint is now solved
-- 	  Wanted         -> Derived
--	  Given, Derived -> no-op
193
194
makeSolvedByInst ct 
  | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
  | otherwise                  = ct

mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
mkWantedConstraints flats implics 
  = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics

deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
deCanonicaliseWanted ct 
  = WARN( not (isWanted $ cc_flavor ct), ppr ct ) 
    let Wanted loc = cc_flavor ct 
    in WantedEvVar (cc_id ct) loc

tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
tyVarsOfCanonical (CDictCan { cc_tyargs = tys }) 	       = tyVarsOfTypes tys
tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })     	       = tyVarsOfType ty

213
214
215
216
217
218
219
tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCDict _ct                            = emptyVarSet 

tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet

220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet

instance Outputable CanonicalCt where
  ppr (CDictCan d fl cls tys)     
      = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
  ppr (CIPCan ip fl ip_nm ty)     
      = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
  ppr (CTyEqCan co fl tv ty)      
      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
  ppr (CFunEqCan co fl tc tys ty) 
      = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
\end{code}

Note [Canonical implicit parameter constraints]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The type in a canonical implicit parameter constraint doesn't need to
be a xi (type-function-free type) since we can defer the flattening
until checking this type for equality with another type.  If we
encounter two IP constraints with the same name, they MUST have the
same type, and at that point we can generate a flattened equality
constraint between the types.  (On the other hand, the types in two
class constraints for the same class MAY be equal, so they need to be
flattened in the first place to facilitate comparing them.)

\begin{code}
singleCCan :: CanonicalCt -> CanonicalCts 
singleCCan = unitBag 

andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
andCCan = unionBags

extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
extendCCans = snocBag 

andCCans :: [CanonicalCts] -> CanonicalCts 
andCCans = unionManyBags

emptyCCan :: CanonicalCts 
emptyCCan = emptyBag

isEmptyCCan :: CanonicalCts -> Bool
isEmptyCCan = isEmptyBag
263

264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
isCTyEqCan :: CanonicalCt -> Bool 
isCTyEqCan (CTyEqCan {})  = True 
isCTyEqCan (CFunEqCan {}) = False
isCTyEqCan _              = False 

isCDictCan_Maybe :: CanonicalCt -> Maybe Class
isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
isCDictCan_Maybe _              = Nothing

isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
isCIPCan_Maybe _                = Nothing

isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
isCFunEqCan_Maybe _ = Nothing
280

281
282
283
284
285
286
287
288
289
290
291
292
\end{code}

%************************************************************************
%*									*
                    CtFlavor
         The "flavor" of a canonical constraint
%*									*
%************************************************************************

\begin{code}
data CtFlavor 
  = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
293
294
  | Derived WantedLoc DerivedOrig
                      -- We have evidence for this constraint in TcEvBinds;
295
296
297
298
299
                      --   *however* this evidence can contain wanteds, so 
                      --   it's valid only provisionally to the solution of
                      --   these wanteds 
  | Wanted WantedLoc  -- We have no evidence bindings for this constraint. 

300
data DerivedOrig = DerSC | DerInst | DerSelf
301
-- Deriveds are either superclasses of other wanteds or deriveds, or partially 
302
303
-- solved wanteds from instances, or 'self' dictionaries containing yet wanted
-- superclasses. 
304

305
instance Outputable CtFlavor where 
306
307
308
  ppr (Given _)    = ptext (sLit "[Given]")
  ppr (Wanted _)   = ptext (sLit "[Wanted]")
  ppr (Derived {}) = ptext (sLit "[Derived]") 
309
310
311
312
313
314
315
316
317
318

isWanted :: CtFlavor -> Bool 
isWanted (Wanted {}) = True
isWanted _           = False

isGiven :: CtFlavor -> Bool 
isGiven (Given {}) = True 
isGiven _          = False 

isDerived :: CtFlavor -> Bool 
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
319
320
isDerived (Derived {}) = True
isDerived _            = False
321

322
323
324
325
326
327
328
329
330
331
332
333
334
pprFlavorArising :: CtFlavor -> SDoc
pprFlavorArising (Derived wl _) = pprArisingAt wl
pprFlavorArising (Wanted  wl)   = pprArisingAt wl
pprFlavorArising (Given gl)     = pprArisingAt gl

getWantedLoc :: CanonicalCt -> WantedLoc
getWantedLoc ct 
  = ASSERT (isWanted (cc_flavor ct))
    case cc_flavor ct of 
      Wanted wl -> wl 
      _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty


335
336
337
338
339
isWantedCt :: CanonicalCt -> Bool 
isWantedCt ct = isWanted (cc_flavor ct)
isGivenCt :: CanonicalCt -> Bool 
isGivenCt ct = isGiven (cc_flavor ct) 

340
341
342
canSolve :: CtFlavor -> CtFlavor -> Bool 
-- canSolve ctid1 ctid2 
-- The constraint ctid1 can be used to solve ctid2 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
343
344
345
346
347
348
-- "to solve" means a reaction where the active parts of the two constraints match.
--  active(F xis ~ xi) = F xis 
--  active(tv ~ xi)    = tv 
--  active(D xis)      = D xis 
--  active(IP nm ty)   = nm 
-----------------------------------------
349
350
351
352
353
354
canSolve (Given {})   _            = True 
canSolve (Derived {}) (Wanted {})  = True 
canSolve (Derived {}) (Derived {}) = True 
canSolve (Wanted {})  (Wanted {})  = True
canSolve _ _ = False

355
356
canRewrite :: CtFlavor -> CtFlavor -> Bool 
-- canRewrite ctid1 ctid2 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
357
-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
358
canRewrite = canSolve 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
359

360
361
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted 
362
363
364
365
combineCtLoc (Wanted loc) _    = loc 
combineCtLoc _ (Wanted loc)    = loc 
combineCtLoc (Derived loc _) _ = loc 
combineCtLoc _ (Derived loc _) = loc 
366
combineCtLoc _ _ = panic "combineCtLoc: both given"
367
368

mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
369
370
371
mkGivenFlavor (Wanted  loc)   sk = Given (setCtLocOrigin loc sk)
mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
mkGivenFlavor (Given   loc)   sk = Given (setCtLocOrigin loc sk)
372
373
374
375
376

mkWantedFlavor :: CtFlavor -> CtFlavor
mkWantedFlavor (Wanted  loc)   = Wanted loc
mkWantedFlavor (Derived loc _) = Wanted loc
mkWantedFlavor fl@(Given {})   = pprPanic "mkWantedFlavour" (ppr fl)
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
\end{code}


%************************************************************************
%*									*
%*		The TcS solver monad                                    *
%*									*
%************************************************************************

Note [The TcS monad]
~~~~~~~~~~~~~~~~~~~~
The TcS monad is a weak form of the main Tc monad

All you can do is
    * fail
    * allocate new variables
    * fill in evidence variables

Filling in a dictionary evidence variable means to create a binding
for it, so TcS carries a mutable location where the binding can be
added.  This is initialised from the innermost implication constraint.

\begin{code}
data TcSEnv
  = TcSEnv { 
      tcs_ev_binds :: EvBindsVar,
          -- Evidence bindings

405
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
406
407
          -- Global type bindings

408
      tcs_context :: SimplContext,
409
410
411
412
                     
      tcs_errors :: IORef (Bag FrozenError), 
          -- Frozen errors that we defer reporting as much as possible, in order to
          -- make them as informative as possible. See Note [Frozen Errors]
413

414
      tcs_untch :: TcsUntouchables 
415
416
    }

417
418
419
420
421
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables, 
-- but records extra TcsTv variables generated during simplification
-- See Note [Extra TcsTv untouchables] in TcSimplify

422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
data FrozenError
  = FrozenError ErrorKind CtFlavor TcType TcType 

data ErrorKind
  = MisMatchError | OccCheckError | KindError

instance Outputable FrozenError where 
  ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"

\end{code}

Note [Frozen Errors] 
~~~~~~~~~~~~~~~~~~~~
Some of the errors that we get during canonicalization are best reported when all constraints
have been simplified as much as possible. For instance, assume that during simplification
the following constraints arise: 
   
 [Wanted]   F alpha ~  uf1 
 [Wanted]   beta ~ uf1 beta 

When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply 
see a message: 
    'Can't construct the infinite type  beta ~ uf1 beta' 
and the user has no idea what the uf1 variable is.

Instead our plan is that we will NOT fail immediately, but:
    (1) Record the "frozen" error in the tcs_errors field 
    (2) Isolate the offending constraint from the rest of the inerts 
    (3) Keep on simplifying/canonicalizing

At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to 
report a more informative error: 
    'Can't construct the infinite type beta ~ F alpha beta'
\begin{code}

457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
data SimplContext
  = SimplInfer		-- Inferring type of a let-bound thing
  | SimplRuleLhs	-- Inferring type of a RULE lhs
  | SimplInteractive	-- Inferring type at GHCi prompt
  | SimplCheck		-- Checking a type signature or RULE rhs

instance Outputable SimplContext where
  ppr SimplInfer       = ptext (sLit "SimplInfer")
  ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
  ppr SimplInteractive = ptext (sLit "SimplInteractive")
  ppr SimplCheck       = ptext (sLit "SimplCheck")

isInteractive :: SimplContext -> Bool
isInteractive SimplInteractive = True
isInteractive _                = False

simplEqsOnly :: SimplContext -> Bool
-- Simplify equalities only, not dictionaries
-- This is used for the LHS of rules; ee
-- Note [Simplifying RULE lhs constraints] in TcSimplify
simplEqsOnly SimplRuleLhs = True
simplEqsOnly _            = False

performDefaulting :: SimplContext -> Bool
performDefaulting SimplInfer   	   = False
performDefaulting SimplRuleLhs 	   = False
performDefaulting SimplInteractive = True
performDefaulting SimplCheck       = True

---------------
newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 

instance Functor TcS where
  fmap f m = TcS $ fmap f . unTcS m

instance Monad TcS where 
  return x  = TcS (\_ -> return x) 
  fail err  = TcS (\_ -> fail err) 
  m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)

-- Basic functionality 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
wrapTcS :: TcM a -> TcS a 
-- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
-- and TcS is supposed to have limited functionality
wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds

wrapErrTcS :: TcM a -> TcS a 
-- The thing wrapped should just fail
-- There's no static check; it's up to the user
-- Having a variant for each error message is too painful
wrapErrTcS = wrapTcS

wrapWarnTcS :: TcM a -> TcS a 
-- The thing wrapped should just add a warning, or no-op
-- There's no static check; it's up to the user
wrapWarnTcS = wrapTcS

failTcS, panicTcS :: SDoc -> TcS a
failTcS      = wrapTcS . TcM.failWith
panicTcS doc = pprPanic "TcCanonical" doc

traceTcS :: String -> SDoc -> TcS ()
traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc

traceTcS0 :: String -> SDoc -> TcS ()
traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc

runTcS :: SimplContext
526
       -> Untouchables 	       -- Untouchables
527
       -> TcS a		       -- What to run
528
       -> TcM (a, Bag FrozenError, Bag EvBind)
529
runTcS context untouch tcs 
530
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
531
       ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
532
       ; err_ref <- TcM.newTcRef emptyBag
533
534
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
535
                          , tcs_context  = context
536
                          , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
537
538
                          , tcs_errors   = err_ref
                          }
539
540

	     -- Run the computation
541
       ; res <- unTcS tcs env
542
543
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
544
       ; mapM_ do_unification (varEnvElts ty_binds)
545
546

             -- And return
547
548
549
       ; frozen_errors <- TcM.readTcRef err_ref
       ; ev_binds      <- TcM.readTcRef evb_ref
       ; return (res, frozen_errors, evBindMapBinds ev_binds) }
550
551
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
552

553
nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
554
nestImplicTcS ref untch (TcS thing_inside)
555
556
557
  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, 
                     tcs_context = ctxt, 
                     tcs_errors = err_ref } ->
558
559
560
    let 
       nest_env = TcSEnv { tcs_ev_binds = ref
                         , tcs_ty_binds = ty_binds
561
                         , tcs_untch    = untch
562
563
                         , tcs_context  = ctxtUnderImplic ctxt 
                         , tcs_errors   = err_ref }
564
    in 
565
    thing_inside nest_env
566

567
568
569
570
571
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

572
573
574
575
576
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
ctxtUnderImplic SimplRuleLhs = SimplCheck
ctxtUnderImplic ctxt         = ctxt

577
tryTcS :: TcS a -> TcS a
578
579
-- Like runTcS, but from within the TcS monad 
-- Ignore all the evidence generated, and do not affect caller's evidence!
580
tryTcS tcs 
581
  = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
582
                    ; ev_binds_var <- TcM.newTcEvBinds
583
                    ; err_ref      <- TcM.newTcRef emptyBag
584
                    ; let env1 = env { tcs_ev_binds = ev_binds_var
585
586
                                     , tcs_ty_binds = ty_binds_var 
                                     , tcs_errors   = err_ref }
587
                    ; unTcS tcs env1 })
588
589
590
591
592
593
594
595
596
597
598
599
600

-- Update TcEvBinds 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

getDynFlags :: TcS DynFlags
getDynFlags = wrapTcS TcM.getDOpts

getTcSContext :: TcS SimplContext
getTcSContext = TcS (return . tcs_context)

getTcEvBinds :: TcS EvBindsVar
getTcEvBinds = TcS (return . tcs_ev_binds) 

601
getUntouchables :: TcS TcsUntouchables
602
603
getUntouchables = TcS (return . tcs_untch)

604
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
605
606
getTcSTyBinds = TcS (return . tcs_ty_binds)

607
608
609
610
611
612
613
getTcSErrors :: TcS (IORef (Bag FrozenError))
getTcSErrors = TcS (return . tcs_errors)

getTcSErrorsBag :: TcS (Bag FrozenError) 
getTcSErrorsBag = do { err_ref <- getTcSErrors 
                     ; wrapTcS $ TcM.readTcRef err_ref }

614
615
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) 
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
616
617


618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
getTcEvBindsBag :: TcS EvBindMap
getTcEvBindsBag
  = do { EvBindsVar ev_ref _ <- getTcEvBinds 
       ; wrapTcS $ TcM.readTcRef ev_ref }

setWantedCoBind :: CoVar -> Coercion -> TcS () 
setWantedCoBind cv co 
  = setEvBind cv (EvCoercion co)
     -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 

setDerivedCoBind :: CoVar -> Coercion -> TcS () 
setDerivedCoBind cv co 
  = setEvBind cv (EvCoercion co)

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
634
-- We never do this twice!
635
636
637
638
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
639
640
641
642
643
644
#ifdef DEBUG
            ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
              vcat [ text "TERRIBLE ERROR: double set of meta type variable"
                   , ppr tv <+> text ":=" <+> ppr ty
                   , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
#endif
645
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672

setIPBind :: EvVar -> EvTerm -> TcS () 
setIPBind = setEvBind 

setDictBind :: EvVar -> EvTerm -> TcS () 
setDictBind = setEvBind 

setEvBind :: EvVar -> EvTerm -> TcS () 
-- Internal
setEvBind ev rhs 
  = do { tc_evbinds <- getTcEvBinds 
       ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }

newTcEvBindsTcS :: TcS EvBindsVar
newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)

warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
warnTcS loc warn_if doc 
  | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
  | otherwise = return ()

getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
getDefaultInfo 
  = do { ctxt <- getTcSContext
       ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
       ; return (ctxt, tys, flags) }

673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691


-- Recording errors in the TcS monad
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
addErrorTcS frknd fl ty1 ty2
  = do { err_ref <- getTcSErrors
       ; wrapTcS $ do
       { TcM.updTcRef err_ref $ \ errs ->
           consBag (FrozenError frknd fl ty1 ty2) errs

           -- If there's an error in the *given* constraints,
           -- stop right now, to avoid a cascade of errors
           -- in the wanteds
       ; when (isGiven fl) TcM.failM

       ; return () } }

692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
-- Just get some environments needed for instance looking up and matching
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

getInstEnvs :: TcS (InstEnv, InstEnv) 
getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 

getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs

getTopEnv :: TcS HscEnv 
getTopEnv = wrapTcS $ TcM.getTopEnv 

getGblEnv :: TcS TcGblEnv 
getGblEnv = wrapTcS $ TcM.getGblEnv 

-- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
checkWellStagedDFun pred dfun_id loc 
  = wrapTcS $ TcM.setCtLoc loc $ 
    do { use_stage <- TcM.getStage
       ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
  where
    pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
    bind_lvl = TcM.topIdLvl dfun_id

pprEq :: TcType -> TcType -> SDoc
pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)

isTouchableMetaTyVar :: TcTyVar -> TcS Bool
723
isTouchableMetaTyVar tv 
724
725
726
  = do { untch <- getUntouchables
       ; return $ isTouchableMetaTyVar_InRange untch tv } 

727
728
isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
729
  = case tcTyVarDetails tv of 
730
731
      MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
                        -- See Note [Touchable meta type variables] 
732
733
734
735
      MetaTv {}      -> inTouchableRange untch tv 
      _              -> False 


736
737
\end{code}

738

739
740
741
742
743
744
745
746
747
748
Note [Touchable meta type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Meta type variables allocated *by the constraint solver itself* are always
touchable.  Example: 
   instance C a b => D [a] where...
if we use this instance declaration we "make up" a fresh meta type
variable for 'b', which we must later guess.  (Perhaps C has a
functional dependency.)  But since we aren't in the constraint *generator*
we can't allocate a Unique in the touchable range for this implication
constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
749
750


751
\begin{code}
752
753
754
755
756
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
757
758
759

newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
newFlattenSkolemTyVar ty
760
761
762
763
764
765
  = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
                            ; let name = mkSysTvName uniq (fsLit "f")
                            ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
       ; traceTcS "New Flatten Skolem Born" $ 
           (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
       ; return tv }
766
767
768
769
770

-- Instantiations 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
771
772
773
774
instDFunTypes mb_inst_tys 
  = mapM inst_tv mb_inst_tys
  where
    inst_tv :: Either TyVar TcType -> TcS Type
775
    inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
776
    inst_tv (Right ty) = return ty 
777
778
779
780

instDFunConstraints :: TcThetaType -> TcS [EvVar] 
instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 

781

782
instFlexiTcS :: TyVar -> TcS TcTyVar 
783
784
785
-- Like TcM.instMetaTyVar but the variable that is created is always
-- touchable; we are supposed to guess its instantiation. 
-- See Note [Touchable meta type variables] 
786
instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
787

788
789
790
791
792
793
794
795
newFlexiTcSTy :: Kind -> TcS TcType  
newFlexiTcSTy knd 
  = wrapTcS $
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
       ; let name = mkSysTvName uniq (fsLit "uf")
       ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }

796
797
798
799
800
801
isFlexiTcsTv :: TyVar -> Bool
isFlexiTcsTv tv
  | not (isTcTyVar tv)                  = False
  | MetaTv TcsTv _ <- tcTyVarDetails tv = True
  | otherwise                           = False

802
newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
803
804
-- Create new wanted CoVar that constrains the type to have the specified kind. 
newKindConstraint tv knd 
805
  = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
806
807
       ; let ty_k = mkTyVarTy tv_k
       ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
808
       ; return co_var }
809

810
811
instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
instFlexiTcSHelper tvname tvkind
812
813
814
815
816
817
  = wrapTcS $ 
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
       ; let name = setNameUnique tvname uniq 
             kind = tvkind 
       ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853

-- Superclasses and recursive dictionaries 
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar 
newGivOrDerEvVar pty evtrm 
  = do { ev <- wrapTcS $ TcM.newEvVar pty 
       ; setEvBind ev evtrm 
       ; return ev }

newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
-- Note we create immutable variables for given or derived, since we
-- must bind them to TcEvBinds (because their evidence may involve 
-- superclasses). However we should be able to override existing
-- 'derived' evidence, even in TcEvBinds 
newGivOrDerCoVar ty1 ty2 co 
  = do { cv <- newCoVar ty1 ty2
       ; setEvBind cv (EvCoercion co) 
       ; return cv } 

newWantedCoVar :: TcType -> TcType -> TcS EvVar 
newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 


newCoVar :: TcType -> TcType -> TcS EvVar 
newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 

newIPVar :: IPName Name -> TcType -> TcS EvVar 
newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 

newDictVar :: Class -> [TcType] -> TcS EvVar 
newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
\end{code} 


\begin{code} 
854
isGoodRecEv :: EvVar -> EvVar -> TcS Bool
855
856
857
858
859
860
861
862
863
864
865
866
867
868
-- In a call (isGoodRecEv ev wv), we are considering solving wv 
-- using some term that involves ev, such as:
-- by setting		wv = ev
-- or                   wv = EvCast x |> ev
-- etc. 
-- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
-- in an "unguarded" way. So isGoodRecEv looks at the evidence ev 
-- recursively through the evidence binds, to see if uses of 'wv' are guarded.
--
-- Guarded means: more instance calls than superclass selections. We
-- compute this by chasing the evidence, adding +1 for every instance
-- call (constructor) and -1 for every superclass selection (destructor).
--
-- See Note [Superclasses and recursive dictionaries] in TcInteract
869
isGoodRecEv ev_var wv
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
  = do { tc_evbinds <- getTcEvBindsBag 
       ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var 
       ; return $ case mb of 
                    Nothing -> True 
                    Just min_guardedness -> min_guardedness > 0
       }

  where chase_ev_var :: EvBindMap   -- Evidence binds 
                 -> EvVar           -- Target variable whose gravity we want to return
                 -> Int             -- Current gravity 
                 -> [EvVar]         -- Visited nodes
                 -> EvVar           -- Current node 
                 -> TcS (Maybe Int)
        chase_ev_var assocs trg curr_grav visited orig
            | trg == orig         = return $ Just curr_grav
            | orig `elem` visited = return $ Nothing 
            | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
            = chase_ev assocs trg curr_grav (orig:visited) ev_trm

889
            | otherwise = return Nothing
890
891
892
893
894
895
896
897
898
899
900
901

        chase_ev assocs trg curr_grav visited (EvId v) 
            = chase_ev_var assocs trg curr_grav visited v
        chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) 
            = chase_ev_var assocs trg (curr_grav-1) visited d_id
        chase_ev assocs trg curr_grav visited (EvCast v co)
            = do { m1 <- chase_ev_var assocs trg curr_grav visited v
                 ; m2 <- chase_co assocs trg curr_grav visited co
                 ; return (comb_chase_res Nothing [m1,m2]) } 

        chase_ev assocs trg curr_grav visited (EvCoercion co)
            = chase_co assocs trg curr_grav visited co
902
903
904
905
906
        chase_ev assocs trg curr_grav visited (EvDFunApp _ _ _ev_vars ev_deps)
            = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
                                    -- Notice that we chase the ev_deps and not the ev_vars
                                    -- See Note [Dependencies in self dictionaries] in TcSimplify
                 ; return (comb_chase_res Nothing chase_results) }
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951

        chase_co assocs trg curr_grav visited co 
            = -- Look for all the coercion variables in the coercion 
              -- chase them, and combine the results. This is OK since the
              -- coercion will not contain any superclass terms -- anything 
              -- that involves dictionaries will be bound in assocs. 
              let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
                                             (tyVarsOfType co)
              in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
                    ; return (comb_chase_res Nothing chase_results) } 

        comb_chase_res f []                   = f 
        comb_chase_res f (Nothing:rest)       = comb_chase_res f rest 
        comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
        comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest 


-- Matching and looking up classes and family instances
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

data MatchInstResult mi
  = MatchInstNo         -- No matching instance 
  | MatchInstSingle mi  -- Single matching instance
  | MatchInstMany       -- Multiple matching instances


matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
-- Look up a class constraint in the instance environment
matchClass clas tys
  = do	{ let pred = mkClassPred clas tys 
        ; instEnvs <- getInstEnvs
	; case lookupInstEnv instEnvs clas tys of {
            ([], unifs)               -- Nothing matches  
                -> do { traceTcS "matchClass not matching"
                                 (vcat [ text "dict" <+> ppr pred, 
                                         text "unifs" <+> ppr unifs ]) 
                      ; return MatchInstNo  
                      } ;  
	    ([(ispec, inst_tys)], []) -- A single match 
		-> do	{ let dfun_id = is_dfun ispec
			; traceTcS "matchClass success"
				   (vcat [text "dict" <+> ppr pred, 
				          text "witness" <+> ppr dfun_id
					   <+> ppr (idType dfun_id) ])
				  -- Record that this dfun is needed
952
                        ; return $ MatchInstSingle (dfun_id, inst_tys)
953
954
955
956
957
958
959
960
961
962
                        } ;
     	    (matches, unifs)          -- More than one matches 
		-> do	{ traceTcS "matchClass multiple matches, deferring choice"
			           (vcat [text "dict" <+> ppr pred,
				   	  text "matches" <+> ppr matches,
				   	  text "unifs" <+> ppr unifs])
                        ; return MatchInstMany 
		        }
	}
        }
963
964

matchFam :: TyCon
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
         -> [Type] 
         -> TcS (MatchInstResult (TyCon, [Type]))
matchFam tycon args
  = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
       ; case mb of 
           Nothing  -> return MatchInstNo 
           Just res -> return $ MatchInstSingle res
       -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
       -- multiple matches. Check. 
       }


-- Functional dependencies, instantiation of equations
-------------------------------------------------------

980
981
mkWantedFunDepEqns :: WantedLoc
                   -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
982
983
984
985
986
987
988
989
                   -> TcS [WantedEvVar] 
mkWantedFunDepEqns _   [] = return []
mkWantedFunDepEqns loc eqns
  = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
       ; wevvars <- mapM to_work_item eqns
       ; return $ concat wevvars }
  where
    to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
990
    to_work_item ((qtvs, pairs), d1, d2)
991
      = do { let tvs = varSetElems qtvs
992
           ; tvs' <- mapM instFlexiTcS tvs
993
           ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
994
995
                 loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
           ; mapM (do_one subst loc') pairs }
996

997
998
999
1000
1001
    do_one subst loc' (ty1, ty2)
       = do { let sty1 = substTy subst ty1
                  sty2 = substTy subst ty2
            ; ev <- newWantedCoVar sty1 sty2
            ; return (WantedEvVar ev loc') }
1002
1003
1004
1005

pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
pprEquationDoc (eqn, (p1, _), (p2, _)) 
  = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017

mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
         -> TcM (TidyEnv, SDoc)
mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
  = do  { pred1' <- TcM.zonkTcPredType pred1
        ; pred2' <- TcM.zonkTcPredType pred2
	; let { pred1'' = tidyPred tidy_env pred1'
              ; pred2'' = tidyPred tidy_env pred2' }
	; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
			  nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
			  nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
	; return (tidy_env, msg) }
1018
\end{code}