Fix another fundep error (fixes Trac #4969)
[ghc.git] / compiler / typecheck / TcSMonad.lhs
1 \begin{code}
2 -- Type definitions for the constraint solver
3 module TcSMonad ( 
4
5        -- Canonical constraints
6     CanonicalCts, emptyCCan, andCCan, andCCans, 
7     singleCCan, extendCCans, isEmptyCCan, isCTyEqCan, 
8     isCDictCan_Maybe, isCIPCan_Maybe, isCFunEqCan_Maybe,
9     isCFrozenErr,
10
11     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
12     deCanonicalise, mkFrozenError,
13
14     isWanted, isGiven, isDerived,
15     isGivenCt, isWantedCt, isDerivedCt, pprFlavorArising,
16
17     isFlexiTcsTv,
18
19     canRewrite, canSolve,
20     combineCtLoc, mkGivenFlavor, mkWantedFlavor,
21     getWantedLoc,
22
23     TcS, runTcS, failTcS, panicTcS, traceTcS, -- Basic functionality 
24     traceFireTcS, bumpStepCountTcS,
25     tryTcS, nestImplicTcS, recoverTcS, wrapErrTcS, wrapWarnTcS,
26     SimplContext(..), isInteractive, simplEqsOnly, performDefaulting,
27
28        -- Creation of evidence variables
29     newEvVar, newCoVar, newGivenCoVar,
30     newDerivedId, 
31     newIPVar, newDictVar, newKindConstraint,
32
33        -- Setting evidence variables 
34     setCoBind, setIPBind, setDictBind, setEvBind,
35
36     setWantedTyBind,
37
38     getInstEnvs, getFamInstEnvs,                -- Getting the environments
39     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
40     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap,
41
42     newFlattenSkolemTy,                         -- Flatten skolems 
43
44
45     instDFunTypes,                              -- Instantiation
46     instDFunConstraints,          
47     newFlexiTcSTy, instFlexiTcS,
48
49     compatKind,
50
51     TcsUntouchables,
52     isTouchableMetaTyVar,
53     isTouchableMetaTyVar_InRange, 
54
55     getDefaultInfo, getDynFlags,
56
57     matchClass, matchFam, MatchInstResult (..), 
58     checkWellStagedDFun, 
59     warnTcS,
60     pprEq                                   -- Smaller utils, re-exported from TcM 
61                                              -- TODO (DV): these are only really used in the 
62                                              -- instance matcher in TcSimplify. I am wondering
63                                              -- if the whole instance matcher simply belongs
64                                              -- here 
65 ) where 
66
67 #include "HsVersions.h"
68
69 import HscTypes
70 import BasicTypes 
71
72 import Inst
73 import InstEnv 
74 import FamInst 
75 import FamInstEnv
76
77 import qualified TcRnMonad as TcM
78 import qualified TcMType as TcM
79 import qualified TcEnv as TcM 
80        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
81 import TcType
82 import DynFlags
83
84 import Coercion
85 import Class
86 import TyCon
87 import TypeRep 
88
89 import Name
90 import Var
91 import VarEnv
92 import Outputable
93 import Bag
94 import MonadUtils
95 import VarSet
96 import FastString
97
98 import HsBinds               -- for TcEvBinds stuff 
99 import Id 
100
101 import TcRnTypes
102
103 import Data.IORef
104 \end{code}
105
106
107 %************************************************************************
108 %*                                                                      *
109 %*                       Canonical constraints                          *
110 %*                                                                      *
111 %*   These are the constraints the low-level simplifier works with      *
112 %*                                                                      *
113 %************************************************************************
114
115 \begin{code}
116 -- Types without any type functions inside.  However, note that xi
117 -- types CAN contain unexpanded type synonyms; however, the
118 -- (transitive) expansions of those type synonyms will not contain any
119 -- type functions.
120 type Xi = Type       -- In many comments, "xi" ranges over Xi
121
122 type CanonicalCts = Bag CanonicalCt
123  
124 data CanonicalCt
125   -- Atomic canonical constraints 
126   = CDictCan {  -- e.g.  Num xi
127       cc_id     :: EvVar,
128       cc_flavor :: CtFlavor, 
129       cc_class  :: Class, 
130       cc_tyargs :: [Xi]
131     }
132
133   | CIPCan {    -- ?x::tau
134       -- See note [Canonical implicit parameter constraints].
135       cc_id     :: EvVar,
136       cc_flavor :: CtFlavor,
137       cc_ip_nm  :: IPName Name,
138       cc_ip_ty  :: TcTauType
139     }
140
141   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
142        -- Invariant: 
143        --   * tv not in tvs(xi)   (occurs check)
144        --   * typeKind xi `compatKind` typeKind tv
145        --       See Note [Spontaneous solving and kind compatibility]
146        --   * We prefer unification variables on the left *JUST* for efficiency
147       cc_id     :: EvVar, 
148       cc_flavor :: CtFlavor, 
149       cc_tyvar  :: TcTyVar, 
150       cc_rhs    :: Xi
151     }
152
153   | CFunEqCan {  -- F xis ~ xi  
154                  -- Invariant: * isSynFamilyTyCon cc_fun 
155                  --            * typeKind (F xis) `compatKind` typeKind xi
156       cc_id     :: EvVar,
157       cc_flavor :: CtFlavor, 
158       cc_fun    :: TyCon,       -- A type function
159       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
160       cc_rhs    :: Xi           --    *never* over-saturated (because if so
161                                 --    we should have decomposed)
162                    
163     }
164
165   | CFrozenErr {      -- A "frozen error" does not interact with anything
166                       -- See Note [Frozen Errors]
167       cc_id     :: EvVar,
168       cc_flavor :: CtFlavor
169     }
170
171 mkFrozenError :: CtFlavor -> EvVar -> CanonicalCt
172 mkFrozenError fl ev = CFrozenErr { cc_id = ev, cc_flavor = fl }
173
174 compatKind :: Kind -> Kind -> Bool
175 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
176
177 deCanonicalise :: CanonicalCt -> FlavoredEvVar
178 deCanonicalise ct = mkEvVarX (cc_id ct) (cc_flavor ct)
179
180 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
181 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
182 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
183 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
184 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
185 tyVarsOfCanonical (CFrozenErr { cc_id = ev })                  = tyVarsOfEvVar ev
186
187 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
188 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
189 tyVarsOfCDict _ct                            = emptyVarSet 
190
191 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
192 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
193
194 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
195 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
196
197 instance Outputable CanonicalCt where
198   ppr (CDictCan d fl cls tys)     
199       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
200   ppr (CIPCan ip fl ip_nm ty)     
201       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
202   ppr (CTyEqCan co fl tv ty)      
203       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
204   ppr (CFunEqCan co fl tc tys ty) 
205       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
206   ppr (CFrozenErr co fl)
207       = ppr fl <+> pprEvVarWithType co
208 \end{code}
209
210 Note [Canonical implicit parameter constraints]
211 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
212 The type in a canonical implicit parameter constraint doesn't need to
213 be a xi (type-function-free type) since we can defer the flattening
214 until checking this type for equality with another type.  If we
215 encounter two IP constraints with the same name, they MUST have the
216 same type, and at that point we can generate a flattened equality
217 constraint between the types.  (On the other hand, the types in two
218 class constraints for the same class MAY be equal, so they need to be
219 flattened in the first place to facilitate comparing them.)
220
221 \begin{code}
222 singleCCan :: CanonicalCt -> CanonicalCts 
223 singleCCan = unitBag 
224
225 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
226 andCCan = unionBags
227
228 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
229 extendCCans = snocBag 
230
231 andCCans :: [CanonicalCts] -> CanonicalCts 
232 andCCans = unionManyBags
233
234 emptyCCan :: CanonicalCts 
235 emptyCCan = emptyBag
236
237 isEmptyCCan :: CanonicalCts -> Bool
238 isEmptyCCan = isEmptyBag
239
240 isCTyEqCan :: CanonicalCt -> Bool 
241 isCTyEqCan (CTyEqCan {})  = True 
242 isCTyEqCan (CFunEqCan {}) = False
243 isCTyEqCan _              = False 
244
245 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
246 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
247 isCDictCan_Maybe _              = Nothing
248
249 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
250 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
251 isCIPCan_Maybe _                = Nothing
252
253 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
254 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
255 isCFunEqCan_Maybe _ = Nothing
256
257 isCFrozenErr :: CanonicalCt -> Bool
258 isCFrozenErr (CFrozenErr {}) = True
259 isCFrozenErr _               = False
260 \end{code}
261
262 %************************************************************************
263 %*                                                                      *
264                     CtFlavor
265          The "flavor" of a canonical constraint
266 %*                                                                      *
267 %************************************************************************
268
269 \begin{code}
270 getWantedLoc :: CanonicalCt -> WantedLoc
271 getWantedLoc ct 
272   = ASSERT (isWanted (cc_flavor ct))
273     case cc_flavor ct of 
274       Wanted wl -> wl 
275       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
276
277 isWantedCt :: CanonicalCt -> Bool
278 isWantedCt ct = isWanted (cc_flavor ct)
279 isGivenCt :: CanonicalCt -> Bool
280 isGivenCt ct = isGiven (cc_flavor ct)
281 isDerivedCt :: CanonicalCt -> Bool
282 isDerivedCt ct = isDerived (cc_flavor ct)
283
284 canSolve :: CtFlavor -> CtFlavor -> Bool 
285 -- canSolve ctid1 ctid2 
286 -- The constraint ctid1 can be used to solve ctid2 
287 -- "to solve" means a reaction where the active parts of the two constraints match.
288 --  active(F xis ~ xi) = F xis 
289 --  active(tv ~ xi)    = tv 
290 --  active(D xis)      = D xis 
291 --  active(IP nm ty)   = nm 
292 --
293 -- NB:  either (a `canSolve` b) or (b `canSolve` a) must hold
294 -----------------------------------------
295 canSolve (Given {})   _            = True 
296 canSolve (Wanted {})  (Derived {}) = True
297 canSolve (Wanted {})  (Wanted {})  = True
298 canSolve (Derived {}) (Derived {}) = True  -- Important: derived can't solve wanted/given
299 canSolve _ _ = False                       -- (There is no *evidence* for a derived.)
300
301 canRewrite :: CtFlavor -> CtFlavor -> Bool 
302 -- canRewrite ctid1 ctid2 
303 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
304 canRewrite = canSolve 
305
306 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
307 -- Precondition: At least one of them should be wanted 
308 combineCtLoc (Wanted loc) _    = loc 
309 combineCtLoc _ (Wanted loc)    = loc 
310 combineCtLoc (Derived loc ) _  = loc 
311 combineCtLoc _ (Derived loc )  = loc 
312 combineCtLoc _ _ = panic "combineCtLoc: both given"
313
314 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
315 mkGivenFlavor (Wanted  loc) sk  = Given (setCtLocOrigin loc sk)
316 mkGivenFlavor (Derived loc) sk  = Given (setCtLocOrigin loc sk)
317 mkGivenFlavor (Given   loc) sk  = Given (setCtLocOrigin loc sk)
318
319
320 mkWantedFlavor :: CtFlavor -> CtFlavor
321 mkWantedFlavor (Wanted  loc) = Wanted loc
322 mkWantedFlavor (Derived loc) = Wanted loc
323 mkWantedFlavor fl@(Given {}) = pprPanic "mkWantedFlavour" (ppr fl)
324 \end{code}
325
326 %************************************************************************
327 %*                                                                      *
328 %*              The TcS solver monad                                    *
329 %*                                                                      *
330 %************************************************************************
331
332 Note [The TcS monad]
333 ~~~~~~~~~~~~~~~~~~~~
334 The TcS monad is a weak form of the main Tc monad
335
336 All you can do is
337     * fail
338     * allocate new variables
339     * fill in evidence variables
340
341 Filling in a dictionary evidence variable means to create a binding
342 for it, so TcS carries a mutable location where the binding can be
343 added.  This is initialised from the innermost implication constraint.
344
345 \begin{code}
346 data TcSEnv
347   = TcSEnv { 
348       tcs_ev_binds :: EvBindsVar,
349           -- Evidence bindings
350
351       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
352           -- Global type bindings
353
354       tcs_context :: SimplContext,
355                      
356       tcs_untch :: TcsUntouchables,
357
358       tcs_ic_depth :: Int,      -- Implication nesting depth
359       tcs_count    :: IORef Int -- Global step count
360     }
361
362 type TcsUntouchables = (Untouchables,TcTyVarSet)
363 -- Like the TcM Untouchables, 
364 -- but records extra TcsTv variables generated during simplification
365 -- See Note [Extra TcsTv untouchables] in TcSimplify
366 \end{code}
367
368 \begin{code}
369 data SimplContext
370   = SimplInfer          -- Inferring type of a let-bound thing
371   | SimplRuleLhs        -- Inferring type of a RULE lhs
372   | SimplInteractive    -- Inferring type at GHCi prompt
373   | SimplCheck          -- Checking a type signature or RULE rhs
374   deriving Eq
375
376 instance Outputable SimplContext where
377   ppr SimplInfer       = ptext (sLit "SimplInfer")
378   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
379   ppr SimplInteractive = ptext (sLit "SimplInteractive")
380   ppr SimplCheck       = ptext (sLit "SimplCheck")
381
382 isInteractive :: SimplContext -> Bool
383 isInteractive SimplInteractive = True
384 isInteractive _                = False
385
386 simplEqsOnly :: SimplContext -> Bool
387 -- Simplify equalities only, not dictionaries
388 -- This is used for the LHS of rules; ee
389 -- Note [Simplifying RULE lhs constraints] in TcSimplify
390 simplEqsOnly SimplRuleLhs = True
391 simplEqsOnly _            = False
392
393 performDefaulting :: SimplContext -> Bool
394 performDefaulting SimplInfer       = False
395 performDefaulting SimplRuleLhs     = False
396 performDefaulting SimplInteractive = True
397 performDefaulting SimplCheck       = True
398
399 ---------------
400 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
401
402 instance Functor TcS where
403   fmap f m = TcS $ fmap f . unTcS m
404
405 instance Monad TcS where 
406   return x  = TcS (\_ -> return x) 
407   fail err  = TcS (\_ -> fail err) 
408   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
409
410 -- Basic functionality 
411 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
412 wrapTcS :: TcM a -> TcS a 
413 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
414 -- and TcS is supposed to have limited functionality
415 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
416
417 wrapErrTcS :: TcM a -> TcS a 
418 -- The thing wrapped should just fail
419 -- There's no static check; it's up to the user
420 -- Having a variant for each error message is too painful
421 wrapErrTcS = wrapTcS
422
423 wrapWarnTcS :: TcM a -> TcS a 
424 -- The thing wrapped should just add a warning, or no-op
425 -- There's no static check; it's up to the user
426 wrapWarnTcS = wrapTcS
427
428 failTcS, panicTcS :: SDoc -> TcS a
429 failTcS      = wrapTcS . TcM.failWith
430 panicTcS doc = pprPanic "TcCanonical" doc
431
432 traceTcS :: String -> SDoc -> TcS ()
433 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
434
435 bumpStepCountTcS :: TcS ()
436 bumpStepCountTcS = TcS $ \env -> do { let ref = tcs_count env
437                                     ; n <- TcM.readTcRef ref
438                                     ; TcM.writeTcRef ref (n+1) }
439
440 traceFireTcS :: Int -> SDoc -> TcS ()
441 -- Dump a rule-firing trace
442 traceFireTcS depth doc 
443   = TcS $ \env -> 
444     TcM.ifDOptM Opt_D_dump_cs_trace $ 
445     do { n <- TcM.readTcRef (tcs_count env)
446        ; let msg = int n 
447                 <> text (replicate (tcs_ic_depth env) '>')
448                 <> brackets (int depth) <+> doc
449        ; TcM.dumpTcRn msg }
450
451 runTcS :: SimplContext
452        -> Untouchables         -- Untouchables
453        -> TcS a                -- What to run
454        -> TcM (a, Bag EvBind)
455 runTcS context untouch tcs 
456   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
457        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
458        ; step_count <- TcM.newTcRef 0
459        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
460                           , tcs_ty_binds = ty_binds_var
461                           , tcs_context  = context
462                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
463                           , tcs_count    = step_count
464                           , tcs_ic_depth = 0
465                           }
466
467              -- Run the computation
468        ; res <- unTcS tcs env
469              -- Perform the type unifications required
470        ; ty_binds <- TcM.readTcRef ty_binds_var
471        ; mapM_ do_unification (varEnvElts ty_binds)
472
473 #ifdef DEBUG
474        ; count <- TcM.readTcRef step_count
475        ; TcM.dumpTcRn (ptext (sLit "Constraint solver steps =") <+> int count)
476 #endif
477              -- And return
478        ; ev_binds      <- TcM.readTcRef evb_ref
479        ; return (res, evBindMapBinds ev_binds) }
480   where
481     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
482
483 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
484 nestImplicTcS ref (inner_range, inner_tcs) (TcS thing_inside)
485   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds 
486                    , tcs_untch = (_outer_range, outer_tcs)
487                    , tcs_count = count
488                    , tcs_ic_depth = idepth
489                    , tcs_context = ctxt } ->
490     let 
491        inner_untch = (inner_range, outer_tcs `unionVarSet` inner_tcs)
492                    -- The inner_range should be narrower than the outer one
493                    -- (thus increasing the set of untouchables) but 
494                    -- the inner Tcs-untouchables must be unioned with the
495                    -- outer ones!
496        nest_env = TcSEnv { tcs_ev_binds = ref
497                          , tcs_ty_binds = ty_binds
498                          , tcs_untch    = inner_untch
499                          , tcs_count    = count
500                          , tcs_ic_depth = idepth+1
501                          , tcs_context  = ctxtUnderImplic ctxt }
502     in 
503     thing_inside nest_env
504
505 recoverTcS :: TcS a -> TcS a -> TcS a
506 recoverTcS (TcS recovery_code) (TcS thing_inside)
507   = TcS $ \ env ->
508     TcM.recoverM (recovery_code env) (thing_inside env)
509
510 ctxtUnderImplic :: SimplContext -> SimplContext
511 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
512 ctxtUnderImplic SimplRuleLhs = SimplCheck
513 ctxtUnderImplic ctxt         = ctxt
514
515 tryTcS :: TcS a -> TcS a
516 -- Like runTcS, but from within the TcS monad 
517 -- Ignore all the evidence generated, and do not affect caller's evidence!
518 tryTcS tcs 
519   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
520                     ; ev_binds_var <- TcM.newTcEvBinds
521                     ; let env1 = env { tcs_ev_binds = ev_binds_var
522                                      , tcs_ty_binds = ty_binds_var }
523                     ; unTcS tcs env1 })
524
525 -- Update TcEvBinds 
526 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
527
528 getDynFlags :: TcS DynFlags
529 getDynFlags = wrapTcS TcM.getDOpts
530
531 getTcSContext :: TcS SimplContext
532 getTcSContext = TcS (return . tcs_context)
533
534 getTcEvBinds :: TcS EvBindsVar
535 getTcEvBinds = TcS (return . tcs_ev_binds) 
536
537 getUntouchables :: TcS TcsUntouchables
538 getUntouchables = TcS (return . tcs_untch)
539
540 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
541 getTcSTyBinds = TcS (return . tcs_ty_binds)
542
543 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType))
544 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
545
546
547 getTcEvBindsBag :: TcS EvBindMap
548 getTcEvBindsBag
549   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
550        ; wrapTcS $ TcM.readTcRef ev_ref }
551
552 setCoBind :: CoVar -> Coercion -> TcS () 
553 setCoBind cv co = setEvBind cv (EvCoercion co)
554
555 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
556 -- Add a type binding
557 -- We never do this twice!
558 setWantedTyBind tv ty 
559   = do { ref <- getTcSTyBinds
560        ; wrapTcS $ 
561          do { ty_binds <- TcM.readTcRef ref
562 #ifdef DEBUG
563             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
564               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
565                    , ppr tv <+> text ":=" <+> ppr ty
566                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
567 #endif
568             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
569
570 setIPBind :: EvVar -> EvTerm -> TcS () 
571 setIPBind = setEvBind 
572
573 setDictBind :: EvVar -> EvTerm -> TcS () 
574 setDictBind = setEvBind 
575
576 setEvBind :: EvVar -> EvTerm -> TcS () 
577 -- Internal
578 setEvBind ev rhs 
579   = do { tc_evbinds <- getTcEvBinds
580        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
581
582 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
583 warnTcS loc warn_if doc 
584   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
585   | otherwise = return ()
586
587 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
588 getDefaultInfo 
589   = do { ctxt <- getTcSContext
590        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
591        ; return (ctxt, tys, flags) }
592
593 -- Just get some environments needed for instance looking up and matching
594 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
595
596 getInstEnvs :: TcS (InstEnv, InstEnv) 
597 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
598
599 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
600 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
601
602 getTopEnv :: TcS HscEnv 
603 getTopEnv = wrapTcS $ TcM.getTopEnv 
604
605 getGblEnv :: TcS TcGblEnv 
606 getGblEnv = wrapTcS $ TcM.getGblEnv 
607
608 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
609 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
610
611 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
612 checkWellStagedDFun pred dfun_id loc 
613   = wrapTcS $ TcM.setCtLoc loc $ 
614     do { use_stage <- TcM.getStage
615        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
616   where
617     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
618     bind_lvl = TcM.topIdLvl dfun_id
619
620 pprEq :: TcType -> TcType -> SDoc
621 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
622
623 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
624 isTouchableMetaTyVar tv 
625   = do { untch <- getUntouchables
626        ; return $ isTouchableMetaTyVar_InRange untch tv } 
627
628 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
629 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
630   = case tcTyVarDetails tv of 
631       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
632                         -- See Note [Touchable meta type variables] 
633       MetaTv {}      -> inTouchableRange untch tv 
634       _              -> False 
635
636
637 \end{code}
638
639
640 Note [Touchable meta type variables]
641 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
642 Meta type variables allocated *by the constraint solver itself* are always
643 touchable.  Example: 
644    instance C a b => D [a] where...
645 if we use this instance declaration we "make up" a fresh meta type
646 variable for 'b', which we must later guess.  (Perhaps C has a
647 functional dependency.)  But since we aren't in the constraint *generator*
648 we can't allocate a Unique in the touchable range for this implication
649 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
650
651
652 \begin{code}
653 -- Flatten skolems
654 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
655
656 newFlattenSkolemTy :: TcType -> TcS TcType
657 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
658
659 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
660 newFlattenSkolemTyVar ty
661   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
662                             ; let name = TcM.mkTcTyVarName uniq (fsLit "f")
663                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
664        ; traceTcS "New Flatten Skolem Born" $ 
665            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
666        ; return tv }
667
668 -- Instantiations 
669 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
670
671 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
672 instDFunTypes mb_inst_tys 
673   = mapM inst_tv mb_inst_tys
674   where
675     inst_tv :: Either TyVar TcType -> TcS Type
676     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
677     inst_tv (Right ty) = return ty 
678
679 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
680 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
681
682
683 instFlexiTcS :: TyVar -> TcS TcTyVar 
684 -- Like TcM.instMetaTyVar but the variable that is created is always
685 -- touchable; we are supposed to guess its instantiation. 
686 -- See Note [Touchable meta type variables] 
687 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
688
689 newFlexiTcSTy :: Kind -> TcS TcType  
690 newFlexiTcSTy knd 
691   = wrapTcS $
692     do { uniq <- TcM.newUnique 
693        ; ref  <- TcM.newMutVar  Flexi 
694        ; let name = TcM.mkTcTyVarName uniq (fsLit "uf")
695        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
696
697 isFlexiTcsTv :: TyVar -> Bool
698 isFlexiTcsTv tv
699   | not (isTcTyVar tv)                  = False
700   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
701   | otherwise                           = False
702
703 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
704 -- Create new wanted CoVar that constrains the type to have the specified kind. 
705 newKindConstraint tv knd 
706   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
707        ; let ty_k = mkTyVarTy tv_k
708        ; co_var <- newCoVar (mkTyVarTy tv) ty_k
709        ; return co_var }
710
711 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
712 instFlexiTcSHelper tvname tvkind
713   = wrapTcS $ 
714     do { uniq <- TcM.newUnique 
715        ; ref  <- TcM.newMutVar  Flexi 
716        ; let name = setNameUnique tvname uniq 
717              kind = tvkind 
718        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
719
720 -- Superclasses and recursive dictionaries 
721 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
722
723 newEvVar :: TcPredType -> TcS EvVar
724 newEvVar pty = wrapTcS $ TcM.newEvVar pty
725
726 newDerivedId :: TcPredType -> TcS EvVar 
727 newDerivedId pty = wrapTcS $ TcM.newEvVar pty
728
729 newGivenCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
730 -- Note we create immutable variables for given or derived, since we
731 -- must bind them to TcEvBinds (because their evidence may involve 
732 -- superclasses). However we should be able to override existing
733 -- 'derived' evidence, even in TcEvBinds 
734 newGivenCoVar ty1 ty2 co 
735   = do { cv <- newCoVar ty1 ty2
736        ; setEvBind cv (EvCoercion co) 
737        ; return cv } 
738
739 newCoVar :: TcType -> TcType -> TcS EvVar
740 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
741
742 newIPVar :: IPName Name -> TcType -> TcS EvVar 
743 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
744
745 newDictVar :: Class -> [TcType] -> TcS EvVar 
746 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
747 \end{code} 
748
749
750 \begin{code} 
751 -- Matching and looking up classes and family instances
752 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
753
754 data MatchInstResult mi
755   = MatchInstNo         -- No matching instance 
756   | MatchInstSingle mi  -- Single matching instance
757   | MatchInstMany       -- Multiple matching instances
758
759
760 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
761 -- Look up a class constraint in the instance environment
762 matchClass clas tys
763   = do  { let pred = mkClassPred clas tys 
764         ; instEnvs <- getInstEnvs
765         ; case lookupInstEnv instEnvs clas tys of {
766             ([], unifs)               -- Nothing matches  
767                 -> do { traceTcS "matchClass not matching"
768                                  (vcat [ text "dict" <+> ppr pred, 
769                                          text "unifs" <+> ppr unifs ]) 
770                       ; return MatchInstNo  
771                       } ;  
772             ([(ispec, inst_tys)], []) -- A single match 
773                 -> do   { let dfun_id = is_dfun ispec
774                         ; traceTcS "matchClass success"
775                                    (vcat [text "dict" <+> ppr pred, 
776                                           text "witness" <+> ppr dfun_id
777                                            <+> ppr (idType dfun_id) ])
778                                   -- Record that this dfun is needed
779                         ; return $ MatchInstSingle (dfun_id, inst_tys)
780                         } ;
781             (matches, unifs)          -- More than one matches 
782                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
783                                    (vcat [text "dict" <+> ppr pred,
784                                           text "matches" <+> ppr matches,
785                                           text "unifs" <+> ppr unifs])
786                         ; return MatchInstMany 
787                         }
788         }
789         }
790
791 matchFam :: TyCon
792          -> [Type] 
793          -> TcS (MatchInstResult (TyCon, [Type]))
794 matchFam tycon args
795   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
796        ; case mb of 
797            Nothing  -> return MatchInstNo 
798            Just res -> return $ MatchInstSingle res
799        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
800        -- multiple matches. Check. 
801        }
802 \end{code}