TcSMonad.lhs 28.2 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
    singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, 
8
9
    isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
    isCFrozenErr,
10

11
    CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
12
13
    deCanonicalise, mkFrozenError,
    makeSolvedByInst,
14

15
16
    isWanted, isGiven, isDerived,
    isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
17

18
19
    isFlexiTcsTv,

20
    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
    SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,

28
29
30
       -- Creation of evidence variables
    newEvVar, newCoVar, newWantedCoVar, newGivenCoVar,
    newDerivedId, 
31
32
33
    newIPVar, newDictVar, newKindConstraint,

       -- Setting evidence variables 
34
    setWantedCoBind,
35
36
37
38
    setIPBind, setDictBind, setEvBind,

    setWantedTyBind,

39
    getInstEnvs, getFamInstEnvs,                -- Getting the environments
40
    getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
41
    getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
42
43

    newFlattenSkolemTy,                         -- Flatten skolems 
44

45
46

    instDFunTypes,                              -- Instantiation
47
48
    instDFunConstraints,          
    newFlexiTcSTy, 
49

50
51
    compatKind,

52
    TcsUntouchables,
53
    isTouchableMetaTyVar,
54
    isTouchableMetaTyVar_InRange, 
55
56
57
58
59
60
61
62
63
64
65
66
67

    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 


68
    mkDerivedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91

) 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
92
93
import TypeRep 

94
95
import Name
import Var
96
import VarEnv
97
98
99
100
101
102
103
104
105
106
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
107
108
import TcRnTypes

109
import Control.Monad
110
111
112
113
114
115
116
117
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
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,
143
      cc_flavor :: CtFlavor,
144
145
146
147
148
149
150
      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)
151
152
       --   * typeKind xi `compatKind` typeKind tv
       --       See Note [Spontaneous solving and kind compatibility]
153
       --   * We prefer unification variables on the left *JUST* for efficiency
154
155
      cc_id     :: EvVar, 
      cc_flavor :: CtFlavor, 
156
157
      cc_tyvar  :: TcTyVar, 
      cc_rhs    :: Xi
158
159
160
161
    }

  | CFunEqCan {  -- F xis ~ xi  
                 -- Invariant: * isSynFamilyTyCon cc_fun 
162
                 --            * typeKind (F xis) `compatKind` typeKind xi
163
164
165
166
167
168
169
170
171
      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)
                   
    }

172
173
174
175
176
  | CFrozenErr {      -- A "frozen error" does not interact with anything
                      -- See Note [Frozen Errors]
      cc_id     :: EvVar,
      cc_flavor :: CtFlavor
    }
177

178
179
180
181
182
mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }

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

184
makeSolvedByInst :: CanonicalCt -> CanonicalCt
185
-- Record that a constraint is now solved
186
-- 	  Wanted         -> Given
187
--	  Given, Derived -> no-op
188
makeSolvedByInst ct 
189
190
191
192
  | Wanted loc <- cc_flavor ct
  = ct { cc_flavor = Given (setCtLocOrigin loc UnkSkol) }
  | otherwise	   -- Only called on wanteds
  = pprPanic "makeSolvedByInst" (ppr ct)
193

194
195
deCanonicalise :: CanonicalCt -> FlavoredEvVar
deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
196
197
198
199
200

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
201
202
tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
203

204
205
206
207
208
209
210
tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
tyVarsOfCDict _ct                            = emptyVarSet 

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

211
212
213
214
215
216
217
218
219
220
221
222
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)
223
224
  ppr (CFrozenErr co fl)
      = ppr fl <+> pprEvVarWithType co
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
\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
256

257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
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
273

274
275
276
isCFrozenErr :: CanonicalCt -> Bool
isCFrozenErr (CFrozenErr {}) = True
isCFrozenErr _               = False
277
278
279
280
281
282
283
284
285
286
\end{code}

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

\begin{code}
287
288
289
290
291
292
293
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

294
isWantedCt :: CanonicalCt -> Bool
295
isWantedCt ct = isWanted (cc_flavor ct)
296
297
298
299
isGivenCt :: CanonicalCt -> Bool
isGivenCt ct = isGiven (cc_flavor ct)
isDerivedCt :: CanonicalCt -> Bool
isDerivedCt ct = isDerived (cc_flavor ct)
300

301
302
303
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
304
305
306
307
308
309
-- "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 
-----------------------------------------
310
canSolve (Given {})   _            = True 
311
312
canSolve (Derived {}) (Wanted {})  = False -- DV: changing the semantics
canSolve (Derived {}) (Derived {}) = True  -- DV: changing the semantics of derived 
313
314
315
canSolve (Wanted {})  (Wanted {})  = True
canSolve _ _ = False

316
317
canRewrite :: CtFlavor -> CtFlavor -> Bool 
-- canRewrite ctid1 ctid2 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
318
-- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
319
canRewrite = canSolve 
dimitris@microsoft.com's avatar
dimitris@microsoft.com committed
320

321
322
combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
-- Precondition: At least one of them should be wanted 
323
324
combineCtLoc (Wanted loc) _    = loc 
combineCtLoc _ (Wanted loc)    = loc 
325
326
combineCtLoc (Derived loc ) _  = loc 
combineCtLoc _ (Derived loc )  = loc 
327
combineCtLoc _ _ = panic "combineCtLoc: both given"
328
329

mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
330
331
332
mkGivenFlavor (Wanted  loc) sk = Given (setCtLocOrigin loc sk)
mkGivenFlavor (Derived loc) sk = Given (setCtLocOrigin loc sk)
mkGivenFlavor (Given   loc) sk = Given (setCtLocOrigin loc sk)
333
334

mkWantedFlavor :: CtFlavor -> CtFlavor
335
336
337
mkWantedFlavor (Wanted  loc) = Wanted loc
mkWantedFlavor (Derived loc) = Wanted loc
mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
\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

365
      tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
366
367
          -- Global type bindings

368
      tcs_context :: SimplContext,
369
                     
370
      tcs_untch :: TcsUntouchables
371
372
    }

373
374
375
376
type TcsUntouchables = (Untouchables,TcTyVarSet)
-- Like the TcM Untouchables, 
-- but records extra TcsTv variables generated during simplification
-- See Note [Extra TcsTv untouchables] in TcSimplify
377
378
379
\end{code}

\begin{code}
380
381
382
383
384
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
385
  deriving Eq
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
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

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
450
       -> Untouchables 	       -- Untouchables
451
       -> TcS a		       -- What to run
452
       -> TcM (a, Bag EvBind)
453
runTcS context untouch tcs 
454
  = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
455
456
457
       ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
       ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
                          , tcs_ty_binds = ty_binds_var
458
                          , tcs_context  = context
459
                          , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
460
                          }
461
462

	     -- Run the computation
463
       ; res <- unTcS tcs env
464
465
	     -- Perform the type unifications required
       ; ty_binds <- TcM.readTcRef ty_binds_var
466
       ; mapM_ do_unification (varEnvElts ty_binds)
467
468

             -- And return
469
       ; ev_binds      <- TcM.readTcRef evb_ref
470
       ; return (res, evBindMapBinds ev_binds) }
471
472
  where
    do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
473

474
nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
475
nestImplicTcS ref untch (TcS thing_inside)
476
  = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, 
477
                     tcs_context = ctxt } ->
478
479
480
    let 
       nest_env = TcSEnv { tcs_ev_binds = ref
                         , tcs_ty_binds = ty_binds
481
                         , tcs_untch    = untch
482
                         , tcs_context  = ctxtUnderImplic ctxt }
483
    in 
484
    thing_inside nest_env
485

486
487
488
489
490
recoverTcS :: TcS a -> TcS a -> TcS a
recoverTcS (TcS recovery_code) (TcS thing_inside)
  = TcS $ \ env ->
    TcM.recoverM (recovery_code env) (thing_inside env)

491
492
493
494
495
ctxtUnderImplic :: SimplContext -> SimplContext
-- See Note [Simplifying RULE lhs constraints] in TcSimplify
ctxtUnderImplic SimplRuleLhs = SimplCheck
ctxtUnderImplic ctxt         = ctxt

496
tryTcS :: TcS a -> TcS a
497
498
-- Like runTcS, but from within the TcS monad 
-- Ignore all the evidence generated, and do not affect caller's evidence!
499
tryTcS tcs 
500
  = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
501
502
                    ; ev_binds_var <- TcM.newTcEvBinds
                    ; let env1 = env { tcs_ev_binds = ev_binds_var
503
                                     , tcs_ty_binds = ty_binds_var }
504
                    ; unTcS tcs env1 })
505
506
507
508
509
510
511
512
513
514
515
516
517

-- 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) 

518
getUntouchables :: TcS TcsUntouchables
519
520
getUntouchables = TcS (return . tcs_untch)

521
getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
522
523
getTcSTyBinds = TcS (return . tcs_ty_binds)

524
getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
525
getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
526
527


528
529
530
531
532
533
534
535
536
537
538
539
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 

setWantedTyBind :: TcTyVar -> TcType -> TcS () 
-- Add a type binding
540
-- We never do this twice!
541
542
543
544
setWantedTyBind tv ty 
  = do { ref <- getTcSTyBinds
       ; wrapTcS $ 
         do { ty_binds <- TcM.readTcRef ref
545
546
547
548
549
550
#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
551
            ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
552
553
554
555
556
557
558
559
560
561

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

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

setEvBind :: EvVar -> EvTerm -> TcS () 
-- Internal
setEvBind ev rhs 
562
  = do { tc_evbinds <- getTcEvBinds
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
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
       ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }

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) }

-- 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
607
isTouchableMetaTyVar tv 
608
609
610
  = do { untch <- getUntouchables
       ; return $ isTouchableMetaTyVar_InRange untch tv } 

611
612
isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
613
  = case tcTyVarDetails tv of 
614
615
      MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
                        -- See Note [Touchable meta type variables] 
616
617
618
619
      MetaTv {}      -> inTouchableRange untch tv 
      _              -> False 


620
621
\end{code}

622

623
624
625
626
627
628
629
630
631
632
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.
633
634


635
\begin{code}
636
637
638
639
640
-- Flatten skolems
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

newFlattenSkolemTy :: TcType -> TcS TcType
newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
641
642
643

newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
newFlattenSkolemTyVar ty
644
  = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
645
                            ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
646
647
648
649
                            ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
       ; traceTcS "New Flatten Skolem Born" $ 
           (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
       ; return tv }
650
651
652
653
654

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

instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
655
656
657
658
instDFunTypes mb_inst_tys 
  = mapM inst_tv mb_inst_tys
  where
    inst_tv :: Either TyVar TcType -> TcS Type
659
    inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
660
    inst_tv (Right ty) = return ty 
661
662
663
664

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

665

666
instFlexiTcS :: TyVar -> TcS TcTyVar 
667
668
669
-- 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] 
670
instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
671

672
673
674
675
676
newFlexiTcSTy :: Kind -> TcS TcType  
newFlexiTcSTy knd 
  = wrapTcS $
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
677
       ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
678
679
       ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }

680
681
682
683
684
685
isFlexiTcsTv :: TyVar -> Bool
isFlexiTcsTv tv
  | not (isTcTyVar tv)                  = False
  | MetaTv TcsTv _ <- tcTyVarDetails tv = True
  | otherwise                           = False

686
newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
687
688
-- Create new wanted CoVar that constrains the type to have the specified kind. 
newKindConstraint tv knd 
689
  = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
690
691
       ; let ty_k = mkTyVarTy tv_k
       ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
692
       ; return co_var }
693

694
695
instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
instFlexiTcSHelper tvname tvkind
696
697
698
699
700
701
  = wrapTcS $ 
    do { uniq <- TcM.newUnique 
       ; ref  <- TcM.newMutVar  Flexi 
       ; let name = setNameUnique tvname uniq 
             kind = tvkind 
       ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
702
703
704
705

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

706
707
newEvVar :: TcPredType -> TcS EvVar
newEvVar pty = wrapTcS $ TcM.newEvVar pty
708

709
710
711
712
newDerivedId :: TcPredType -> TcS EvVar 
newDerivedId pty = wrapTcS $ TcM.newEvVar pty

newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
713
714
715
716
-- 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 
717
newGivenCoVar ty1 ty2 co 
718
719
720
721
722
723
724
  = do { cv <- newCoVar ty1 ty2
       ; setEvBind cv (EvCoercion co) 
       ; return cv } 

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

725
newCoVar :: TcType -> TcType -> TcS EvVar
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
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} 
-- 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
751
        ; case lookupInstEnv instEnvs clas tys of {
752
753
754
755
756
757
758
759
760
761
762
            ([], 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
763
                                           <+> ppr (idType dfun_id) ])
764
				  -- Record that this dfun is needed
765
                        ; return $ MatchInstSingle (dfun_id, inst_tys)
766
767
768
769
770
771
772
773
774
775
                        } ;
     	    (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 
		        }
	}
        }
776
777

matchFam :: TyCon
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
         -> [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
-------------------------------------------------------

793
mkDerivedFunDepEqns :: WantedLoc
794
                   -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
795
796
797
                   -> TcS [FlavoredEvVar]    -- All Derived
mkDerivedFunDepEqns _   [] = return []
mkDerivedFunDepEqns loc eqns
798
  = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
799
800
       ; evvars <- mapM to_work_item eqns
       ; return $ concat evvars }
801
  where
802
    to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [FlavoredEvVar]
803
    to_work_item ((qtvs, pairs), d1, d2)
804
      = do { let tvs = varSetElems qtvs
805
           ; tvs' <- mapM instFlexiTcS tvs
806
           ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
807
                 loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
808
809
                 flav  = Derived loc'
           ; mapM (do_one subst flav) pairs }
810

811
    do_one subst flav (ty1, ty2)
812
813
       = do { let sty1 = substTy subst ty1
                  sty2 = substTy subst ty2
814
815
            ; ev <- newCoVar sty1 sty2
            ; return (mkEvVarX ev flav) }
816
817
818
819

pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
pprEquationDoc (eqn, (p1, _), (p2, _)) 
  = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
820
821
822
823
824
825
826
827
828
829
830
831

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) }
832
\end{code}