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