Less verbose debug print
[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
10     CanonicalCt(..), Xi, tyVarsOfCanonical, tyVarsOfCanonicals, tyVarsOfCDicts, 
11     mkWantedConstraints, deCanonicaliseWanted, 
12     makeGivens, makeSolvedByInst,
13
14     CtFlavor (..), isWanted, isGiven, isDerived, 
15     isGivenCt, isWantedCt, pprFlavorArising,
16
17     isFlexiTcsTv,
18
19     DerivedOrig (..), 
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
30     newWantedCoVar, newGivOrDerCoVar, newGivOrDerEvVar, 
31     newIPVar, newDictVar, newKindConstraint,
32
33        -- Setting evidence variables 
34     setWantedCoBind, setDerivedCoBind, 
35     setIPBind, setDictBind, setEvBind,
36
37     setWantedTyBind,
38
39     newTcEvBindsTcS,
40  
41     getInstEnvs, getFamInstEnvs,                -- Getting the environments 
42     getTopEnv, getGblEnv, getTcEvBinds, getUntouchables,
43     getTcEvBindsBag, getTcSContext, getTcSTyBinds, getTcSTyBindsMap, getTcSErrors,
44     getTcSErrorsBag, FrozenError (..),
45     addErrorTcS,
46     ErrorKind(..),
47
48     newFlattenSkolemTy,                         -- Flatten skolems 
49
50
51     instDFunTypes,                              -- Instantiation
52     instDFunConstraints,          
53     newFlexiTcSTy, 
54
55     isGoodRecEv,
56
57     compatKind,
58
59
60     TcsUntouchables,
61     isTouchableMetaTyVar,
62     isTouchableMetaTyVar_InRange, 
63
64     getDefaultInfo, getDynFlags,
65
66     matchClass, matchFam, MatchInstResult (..), 
67     checkWellStagedDFun, 
68     warnTcS,
69     pprEq,                                   -- Smaller utils, re-exported from TcM 
70                                              -- TODO (DV): these are only really used in the 
71                                              -- instance matcher in TcSimplify. I am wondering
72                                              -- if the whole instance matcher simply belongs
73                                              -- here 
74
75
76     mkWantedFunDepEqns                       -- Instantiation of 'Equations' from FunDeps
77
78 ) where 
79
80 #include "HsVersions.h"
81
82 import HscTypes
83 import BasicTypes 
84
85 import Inst
86 import InstEnv 
87 import FamInst 
88 import FamInstEnv
89
90 import qualified TcRnMonad as TcM
91 import qualified TcMType as TcM
92 import qualified TcEnv as TcM 
93        ( checkWellStaged, topIdLvl, tcLookupFamInst, tcGetDefaultTys )
94 import TcType
95 import DynFlags
96
97 import Coercion
98 import Class
99 import TyCon
100 import TypeRep 
101
102 import Name
103 import Var
104 import VarEnv
105 import Outputable
106 import Bag
107 import MonadUtils
108 import VarSet
109 import FastString
110
111 import HsBinds               -- for TcEvBinds stuff 
112 import Id 
113 import FunDeps
114
115 import TcRnTypes
116
117 import Control.Monad
118 import Data.IORef
119 \end{code}
120
121
122 %************************************************************************
123 %*                                                                      *
124 %*                       Canonical constraints                          *
125 %*                                                                      *
126 %*   These are the constraints the low-level simplifier works with      *
127 %*                                                                      *
128 %************************************************************************
129
130 \begin{code}
131 -- Types without any type functions inside.  However, note that xi
132 -- types CAN contain unexpanded type synonyms; however, the
133 -- (transitive) expansions of those type synonyms will not contain any
134 -- type functions.
135 type Xi = Type       -- In many comments, "xi" ranges over Xi
136
137 type CanonicalCts = Bag CanonicalCt
138  
139 data CanonicalCt
140   -- Atomic canonical constraints 
141   = CDictCan {  -- e.g.  Num xi
142       cc_id     :: EvVar,
143       cc_flavor :: CtFlavor, 
144       cc_class  :: Class, 
145       cc_tyargs :: [Xi]
146     }
147
148   | CIPCan {    -- ?x::tau
149       -- See note [Canonical implicit parameter constraints].
150       cc_id     :: EvVar,
151       cc_flavor :: CtFlavor,
152       cc_ip_nm  :: IPName Name,
153       cc_ip_ty  :: TcTauType
154     }
155
156   | CTyEqCan {  -- tv ~ xi      (recall xi means function free)
157        -- Invariant: 
158        --   * tv not in tvs(xi)   (occurs check)
159        --   * If constraint is given then typeKind xi `compatKind` typeKind tv 
160        --                See Note [Spontaneous solving and kind compatibility] 
161        --   * We prefer unification variables on the left *JUST* for efficiency
162       cc_id     :: EvVar, 
163       cc_flavor :: CtFlavor, 
164       cc_tyvar  :: TcTyVar, 
165       cc_rhs    :: Xi
166     }
167
168   | CFunEqCan {  -- F xis ~ xi  
169                  -- Invariant: * isSynFamilyTyCon cc_fun 
170                  --            * If constraint is given then 
171                  --                 typeKind (F xis) `compatKind` typeKind xi
172       cc_id     :: EvVar,
173       cc_flavor :: CtFlavor, 
174       cc_fun    :: TyCon,       -- A type function
175       cc_tyargs :: [Xi],        -- Either under-saturated or exactly saturated
176       cc_rhs    :: Xi           --    *never* over-saturated (because if so
177                                 --    we should have decomposed)
178                    
179     }
180
181 compatKind :: Kind -> Kind -> Bool 
182 compatKind k1 k2 = k1 `isSubKind` k2 || k2 `isSubKind` k1 
183
184 makeGivens :: Bag WantedEvVar -> Bag (CtFlavor,EvVar) 
185 makeGivens = mapBag (\(WantedEvVar ev wloc) -> (mkGivenFlavor (Wanted wloc) UnkSkol, ev))
186 -- ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
187            -- The UnkSkol doesn't matter because these givens are
188            -- not contradictory (else we'd have rejected them already)
189
190 makeSolvedByInst :: CanonicalCt -> CanonicalCt
191 -- Record that a constraint is now solved
192 --        Wanted         -> Derived
193 --        Given, Derived -> no-op
194 makeSolvedByInst ct 
195   | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
196   | otherwise                  = ct
197
198 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
199 mkWantedConstraints flats implics 
200   = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
201
202 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
203 deCanonicaliseWanted ct 
204   = WARN( not (isWanted $ cc_flavor ct), ppr ct ) 
205     let Wanted loc = cc_flavor ct 
206     in WantedEvVar (cc_id ct) loc
207
208 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
209 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
210 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
211 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
212 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
213
214 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
215 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
216 tyVarsOfCDict _ct                            = emptyVarSet 
217
218 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
219 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
220
221 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
222 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
223
224 instance Outputable CanonicalCt where
225   ppr (CDictCan d fl cls tys)     
226       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
227   ppr (CIPCan ip fl ip_nm ty)     
228       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
229   ppr (CTyEqCan co fl tv ty)      
230       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
231   ppr (CFunEqCan co fl tc tys ty) 
232       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
233 \end{code}
234
235 Note [Canonical implicit parameter constraints]
236 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
237 The type in a canonical implicit parameter constraint doesn't need to
238 be a xi (type-function-free type) since we can defer the flattening
239 until checking this type for equality with another type.  If we
240 encounter two IP constraints with the same name, they MUST have the
241 same type, and at that point we can generate a flattened equality
242 constraint between the types.  (On the other hand, the types in two
243 class constraints for the same class MAY be equal, so they need to be
244 flattened in the first place to facilitate comparing them.)
245
246 \begin{code}
247 singleCCan :: CanonicalCt -> CanonicalCts 
248 singleCCan = unitBag 
249
250 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
251 andCCan = unionBags
252
253 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
254 extendCCans = snocBag 
255
256 andCCans :: [CanonicalCts] -> CanonicalCts 
257 andCCans = unionManyBags
258
259 emptyCCan :: CanonicalCts 
260 emptyCCan = emptyBag
261
262 isEmptyCCan :: CanonicalCts -> Bool
263 isEmptyCCan = isEmptyBag
264
265 isCTyEqCan :: CanonicalCt -> Bool 
266 isCTyEqCan (CTyEqCan {})  = True 
267 isCTyEqCan (CFunEqCan {}) = False
268 isCTyEqCan _              = False 
269
270 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
271 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
272 isCDictCan_Maybe _              = Nothing
273
274 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
275 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
276 isCIPCan_Maybe _                = Nothing
277
278 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
279 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
280 isCFunEqCan_Maybe _ = Nothing
281
282 \end{code}
283
284 %************************************************************************
285 %*                                                                      *
286                     CtFlavor
287          The "flavor" of a canonical constraint
288 %*                                                                      *
289 %************************************************************************
290
291 \begin{code}
292 data CtFlavor 
293   = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
294   | Derived WantedLoc DerivedOrig
295                       -- We have evidence for this constraint in TcEvBinds;
296                       --   *however* this evidence can contain wanteds, so 
297                       --   it's valid only provisionally to the solution of
298                       --   these wanteds 
299   | Wanted WantedLoc  -- We have no evidence bindings for this constraint. 
300
301 data DerivedOrig = DerSC | DerInst | DerSelf
302 -- Deriveds are either superclasses of other wanteds or deriveds, or partially 
303 -- solved wanteds from instances, or 'self' dictionaries containing yet wanted
304 -- superclasses. 
305
306 instance Outputable CtFlavor where 
307   ppr (Given _)    = ptext (sLit "[Given]")
308   ppr (Wanted _)   = ptext (sLit "[Wanted]")
309   ppr (Derived {}) = ptext (sLit "[Derived]") 
310
311 isWanted :: CtFlavor -> Bool 
312 isWanted (Wanted {}) = True
313 isWanted _           = False
314
315 isGiven :: CtFlavor -> Bool 
316 isGiven (Given {}) = True 
317 isGiven _          = False 
318
319 isDerived :: CtFlavor -> Bool 
320 isDerived (Derived {}) = True
321 isDerived _            = False
322
323 pprFlavorArising :: CtFlavor -> SDoc
324 pprFlavorArising (Derived wl _) = pprArisingAt wl
325 pprFlavorArising (Wanted  wl)   = pprArisingAt wl
326 pprFlavorArising (Given gl)     = pprArisingAt gl
327
328 getWantedLoc :: CanonicalCt -> WantedLoc
329 getWantedLoc ct 
330   = ASSERT (isWanted (cc_flavor ct))
331     case cc_flavor ct of 
332       Wanted wl -> wl 
333       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
334
335
336 isWantedCt :: CanonicalCt -> Bool 
337 isWantedCt ct = isWanted (cc_flavor ct)
338 isGivenCt :: CanonicalCt -> Bool 
339 isGivenCt ct = isGiven (cc_flavor ct) 
340
341 canSolve :: CtFlavor -> CtFlavor -> Bool 
342 -- canSolve ctid1 ctid2 
343 -- The constraint ctid1 can be used to solve ctid2 
344 -- "to solve" means a reaction where the active parts of the two constraints match.
345 --  active(F xis ~ xi) = F xis 
346 --  active(tv ~ xi)    = tv 
347 --  active(D xis)      = D xis 
348 --  active(IP nm ty)   = nm 
349 -----------------------------------------
350 canSolve (Given {})   _            = True 
351 canSolve (Derived {}) (Wanted {})  = True 
352 canSolve (Derived {}) (Derived {}) = True 
353 canSolve (Wanted {})  (Wanted {})  = True
354 canSolve _ _ = False
355
356 canRewrite :: CtFlavor -> CtFlavor -> Bool 
357 -- canRewrite ctid1 ctid2 
358 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
359 canRewrite = canSolve 
360
361 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
362 -- Precondition: At least one of them should be wanted 
363 combineCtLoc (Wanted loc) _    = loc 
364 combineCtLoc _ (Wanted loc)    = loc 
365 combineCtLoc (Derived loc _) _ = loc 
366 combineCtLoc _ (Derived loc _) = loc 
367 combineCtLoc _ _ = panic "combineCtLoc: both given"
368
369 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
370 mkGivenFlavor (Wanted  loc)   sk = Given (setCtLocOrigin loc sk)
371 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
372 mkGivenFlavor (Given   loc)   sk = Given (setCtLocOrigin loc sk)
373
374 mkWantedFlavor :: CtFlavor -> CtFlavor
375 mkWantedFlavor (Wanted  loc)   = Wanted loc
376 mkWantedFlavor (Derived loc _) = Wanted loc
377 mkWantedFlavor fl@(Given {})   = pprPanic "mkWantedFlavour" (ppr fl)
378 \end{code}
379
380
381 %************************************************************************
382 %*                                                                      *
383 %*              The TcS solver monad                                    *
384 %*                                                                      *
385 %************************************************************************
386
387 Note [The TcS monad]
388 ~~~~~~~~~~~~~~~~~~~~
389 The TcS monad is a weak form of the main Tc monad
390
391 All you can do is
392     * fail
393     * allocate new variables
394     * fill in evidence variables
395
396 Filling in a dictionary evidence variable means to create a binding
397 for it, so TcS carries a mutable location where the binding can be
398 added.  This is initialised from the innermost implication constraint.
399
400 \begin{code}
401 data TcSEnv
402   = TcSEnv { 
403       tcs_ev_binds :: EvBindsVar,
404           -- Evidence bindings
405
406       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
407           -- Global type bindings
408
409       tcs_context :: SimplContext,
410                      
411       tcs_errors :: IORef (Bag FrozenError), 
412           -- Frozen errors that we defer reporting as much as possible, in order to
413           -- make them as informative as possible. See Note [Frozen Errors]
414
415       tcs_untch :: TcsUntouchables 
416     }
417
418 type TcsUntouchables = (Untouchables,TcTyVarSet)
419 -- Like the TcM Untouchables, 
420 -- but records extra TcsTv variables generated during simplification
421 -- See Note [Extra TcsTv untouchables] in TcSimplify
422
423 data FrozenError
424   = FrozenError ErrorKind CtFlavor TcType TcType 
425
426 data ErrorKind
427   = MisMatchError | OccCheckError | KindError
428
429 instance Outputable FrozenError where 
430   ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
431
432 \end{code}
433
434 Note [Frozen Errors] 
435 ~~~~~~~~~~~~~~~~~~~~
436 Some of the errors that we get during canonicalization are best reported when all constraints
437 have been simplified as much as possible. For instance, assume that during simplification
438 the following constraints arise: 
439    
440  [Wanted]   F alpha ~  uf1 
441  [Wanted]   beta ~ uf1 beta 
442
443 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply 
444 see a message: 
445     'Can't construct the infinite type  beta ~ uf1 beta' 
446 and the user has no idea what the uf1 variable is.
447
448 Instead our plan is that we will NOT fail immediately, but:
449     (1) Record the "frozen" error in the tcs_errors field 
450     (2) Isolate the offending constraint from the rest of the inerts 
451     (3) Keep on simplifying/canonicalizing
452
453 At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to 
454 report a more informative error: 
455     'Can't construct the infinite type beta ~ F alpha beta'
456 \begin{code}
457
458 data SimplContext
459   = SimplInfer          -- Inferring type of a let-bound thing
460   | SimplRuleLhs        -- Inferring type of a RULE lhs
461   | SimplInteractive    -- Inferring type at GHCi prompt
462   | SimplCheck          -- Checking a type signature or RULE rhs
463   deriving Eq
464
465 instance Outputable SimplContext where
466   ppr SimplInfer       = ptext (sLit "SimplInfer")
467   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
468   ppr SimplInteractive = ptext (sLit "SimplInteractive")
469   ppr SimplCheck       = ptext (sLit "SimplCheck")
470
471 isInteractive :: SimplContext -> Bool
472 isInteractive SimplInteractive = True
473 isInteractive _                = False
474
475 simplEqsOnly :: SimplContext -> Bool
476 -- Simplify equalities only, not dictionaries
477 -- This is used for the LHS of rules; ee
478 -- Note [Simplifying RULE lhs constraints] in TcSimplify
479 simplEqsOnly SimplRuleLhs = True
480 simplEqsOnly _            = False
481
482 performDefaulting :: SimplContext -> Bool
483 performDefaulting SimplInfer       = False
484 performDefaulting SimplRuleLhs     = False
485 performDefaulting SimplInteractive = True
486 performDefaulting SimplCheck       = True
487
488 ---------------
489 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
490
491 instance Functor TcS where
492   fmap f m = TcS $ fmap f . unTcS m
493
494 instance Monad TcS where 
495   return x  = TcS (\_ -> return x) 
496   fail err  = TcS (\_ -> fail err) 
497   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
498
499 -- Basic functionality 
500 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
501 wrapTcS :: TcM a -> TcS a 
502 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
503 -- and TcS is supposed to have limited functionality
504 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
505
506 wrapErrTcS :: TcM a -> TcS a 
507 -- The thing wrapped should just fail
508 -- There's no static check; it's up to the user
509 -- Having a variant for each error message is too painful
510 wrapErrTcS = wrapTcS
511
512 wrapWarnTcS :: TcM a -> TcS a 
513 -- The thing wrapped should just add a warning, or no-op
514 -- There's no static check; it's up to the user
515 wrapWarnTcS = wrapTcS
516
517 failTcS, panicTcS :: SDoc -> TcS a
518 failTcS      = wrapTcS . TcM.failWith
519 panicTcS doc = pprPanic "TcCanonical" doc
520
521 traceTcS :: String -> SDoc -> TcS ()
522 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
523
524 traceTcS0 :: String -> SDoc -> TcS ()
525 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
526
527 runTcS :: SimplContext
528        -> Untouchables         -- Untouchables
529        -> TcS a                -- What to run
530        -> TcM (a, Bag FrozenError, Bag EvBind)
531 runTcS context untouch tcs 
532   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
533        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
534        ; err_ref <- TcM.newTcRef emptyBag
535        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
536                           , tcs_ty_binds = ty_binds_var
537                           , tcs_context  = context
538                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
539                           , tcs_errors   = err_ref
540                           }
541
542              -- Run the computation
543        ; res <- unTcS tcs env
544              -- Perform the type unifications required
545        ; ty_binds <- TcM.readTcRef ty_binds_var
546        ; mapM_ do_unification (varEnvElts ty_binds)
547
548              -- And return
549        ; frozen_errors <- TcM.readTcRef err_ref
550        ; ev_binds      <- TcM.readTcRef evb_ref
551        ; return (res, frozen_errors, evBindMapBinds ev_binds) }
552   where
553     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
554
555 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
556 nestImplicTcS ref untch (TcS thing_inside)
557   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, 
558                      tcs_context = ctxt, 
559                      tcs_errors = err_ref } ->
560     let 
561        nest_env = TcSEnv { tcs_ev_binds = ref
562                          , tcs_ty_binds = ty_binds
563                          , tcs_untch    = untch
564                          , tcs_context  = ctxtUnderImplic ctxt 
565                          , tcs_errors   = err_ref }
566     in 
567     thing_inside nest_env
568
569 recoverTcS :: TcS a -> TcS a -> TcS a
570 recoverTcS (TcS recovery_code) (TcS thing_inside)
571   = TcS $ \ env ->
572     TcM.recoverM (recovery_code env) (thing_inside env)
573
574 ctxtUnderImplic :: SimplContext -> SimplContext
575 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
576 ctxtUnderImplic SimplRuleLhs = SimplCheck
577 ctxtUnderImplic ctxt         = ctxt
578
579 tryTcS :: TcS a -> TcS a
580 -- Like runTcS, but from within the TcS monad 
581 -- Ignore all the evidence generated, and do not affect caller's evidence!
582 tryTcS tcs 
583   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
584                     ; ev_binds_var <- TcM.newTcEvBinds
585                     ; err_ref      <- TcM.newTcRef emptyBag
586                     ; let env1 = env { tcs_ev_binds = ev_binds_var
587                                      , tcs_ty_binds = ty_binds_var 
588                                      , tcs_errors   = err_ref }
589                     ; unTcS tcs env1 })
590
591 -- Update TcEvBinds 
592 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
593
594 getDynFlags :: TcS DynFlags
595 getDynFlags = wrapTcS TcM.getDOpts
596
597 getTcSContext :: TcS SimplContext
598 getTcSContext = TcS (return . tcs_context)
599
600 getTcEvBinds :: TcS EvBindsVar
601 getTcEvBinds = TcS (return . tcs_ev_binds) 
602
603 getUntouchables :: TcS TcsUntouchables
604 getUntouchables = TcS (return . tcs_untch)
605
606 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
607 getTcSTyBinds = TcS (return . tcs_ty_binds)
608
609 getTcSErrors :: TcS (IORef (Bag FrozenError))
610 getTcSErrors = TcS (return . tcs_errors)
611
612 getTcSErrorsBag :: TcS (Bag FrozenError) 
613 getTcSErrorsBag = do { err_ref <- getTcSErrors 
614                      ; wrapTcS $ TcM.readTcRef err_ref }
615
616 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) 
617 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
618
619
620 getTcEvBindsBag :: TcS EvBindMap
621 getTcEvBindsBag
622   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
623        ; wrapTcS $ TcM.readTcRef ev_ref }
624
625 setWantedCoBind :: CoVar -> Coercion -> TcS () 
626 setWantedCoBind cv co 
627   = setEvBind cv (EvCoercion co)
628      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 
629
630 setDerivedCoBind :: CoVar -> Coercion -> TcS () 
631 setDerivedCoBind cv co 
632   = setEvBind cv (EvCoercion co)
633
634 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
635 -- Add a type binding
636 -- We never do this twice!
637 setWantedTyBind tv ty 
638   = do { ref <- getTcSTyBinds
639        ; wrapTcS $ 
640          do { ty_binds <- TcM.readTcRef ref
641 #ifdef DEBUG
642             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
643               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
644                    , ppr tv <+> text ":=" <+> ppr ty
645                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
646 #endif
647             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
648
649 setIPBind :: EvVar -> EvTerm -> TcS () 
650 setIPBind = setEvBind 
651
652 setDictBind :: EvVar -> EvTerm -> TcS () 
653 setDictBind = setEvBind 
654
655 setEvBind :: EvVar -> EvTerm -> TcS () 
656 -- Internal
657 setEvBind ev rhs 
658   = do { tc_evbinds <- getTcEvBinds 
659        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
660
661 newTcEvBindsTcS :: TcS EvBindsVar
662 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
663
664 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
665 warnTcS loc warn_if doc 
666   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
667   | otherwise = return ()
668
669 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
670 getDefaultInfo 
671   = do { ctxt <- getTcSContext
672        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
673        ; return (ctxt, tys, flags) }
674
675
676
677 -- Recording errors in the TcS monad
678 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
679
680 addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
681 addErrorTcS frknd fl ty1 ty2
682   = do { err_ref <- getTcSErrors
683        ; wrapTcS $ do
684        { TcM.updTcRef err_ref $ \ errs ->
685            consBag (FrozenError frknd fl ty1 ty2) errs
686
687            -- If there's an error in the *given* constraints,
688            -- stop right now, to avoid a cascade of errors
689            -- in the wanteds
690        ; when (isGiven fl) TcM.failM
691
692        ; return () } }
693
694 -- Just get some environments needed for instance looking up and matching
695 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
696
697 getInstEnvs :: TcS (InstEnv, InstEnv) 
698 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
699
700 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
701 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
702
703 getTopEnv :: TcS HscEnv 
704 getTopEnv = wrapTcS $ TcM.getTopEnv 
705
706 getGblEnv :: TcS TcGblEnv 
707 getGblEnv = wrapTcS $ TcM.getGblEnv 
708
709 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
710 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
711
712 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
713 checkWellStagedDFun pred dfun_id loc 
714   = wrapTcS $ TcM.setCtLoc loc $ 
715     do { use_stage <- TcM.getStage
716        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
717   where
718     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
719     bind_lvl = TcM.topIdLvl dfun_id
720
721 pprEq :: TcType -> TcType -> SDoc
722 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
723
724 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
725 isTouchableMetaTyVar tv 
726   = do { untch <- getUntouchables
727        ; return $ isTouchableMetaTyVar_InRange untch tv } 
728
729 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
730 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
731   = case tcTyVarDetails tv of 
732       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
733                         -- See Note [Touchable meta type variables] 
734       MetaTv {}      -> inTouchableRange untch tv 
735       _              -> False 
736
737
738 \end{code}
739
740
741 Note [Touchable meta type variables]
742 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
743 Meta type variables allocated *by the constraint solver itself* are always
744 touchable.  Example: 
745    instance C a b => D [a] where...
746 if we use this instance declaration we "make up" a fresh meta type
747 variable for 'b', which we must later guess.  (Perhaps C has a
748 functional dependency.)  But since we aren't in the constraint *generator*
749 we can't allocate a Unique in the touchable range for this implication
750 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
751
752
753 \begin{code}
754 -- Flatten skolems
755 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
756
757 newFlattenSkolemTy :: TcType -> TcS TcType
758 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
759
760 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
761 newFlattenSkolemTyVar ty
762   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
763                             ; let name = mkSysTvName uniq (fsLit "f")
764                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
765        ; traceTcS "New Flatten Skolem Born" $ 
766            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
767        ; return tv }
768
769 -- Instantiations 
770 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
771
772 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
773 instDFunTypes mb_inst_tys 
774   = mapM inst_tv mb_inst_tys
775   where
776     inst_tv :: Either TyVar TcType -> TcS Type
777     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
778     inst_tv (Right ty) = return ty 
779
780 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
781 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
782
783
784 instFlexiTcS :: TyVar -> TcS TcTyVar 
785 -- Like TcM.instMetaTyVar but the variable that is created is always
786 -- touchable; we are supposed to guess its instantiation. 
787 -- See Note [Touchable meta type variables] 
788 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
789
790 newFlexiTcSTy :: Kind -> TcS TcType  
791 newFlexiTcSTy knd 
792   = wrapTcS $
793     do { uniq <- TcM.newUnique 
794        ; ref  <- TcM.newMutVar  Flexi 
795        ; let name = mkSysTvName uniq (fsLit "uf")
796        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
797
798 isFlexiTcsTv :: TyVar -> Bool
799 isFlexiTcsTv tv
800   | not (isTcTyVar tv)                  = False
801   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
802   | otherwise                           = False
803
804 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
805 -- Create new wanted CoVar that constrains the type to have the specified kind. 
806 newKindConstraint tv knd 
807   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
808        ; let ty_k = mkTyVarTy tv_k
809        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
810        ; return co_var }
811
812 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
813 instFlexiTcSHelper tvname tvkind
814   = wrapTcS $ 
815     do { uniq <- TcM.newUnique 
816        ; ref  <- TcM.newMutVar  Flexi 
817        ; let name = setNameUnique tvname uniq 
818              kind = tvkind 
819        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
820
821 -- Superclasses and recursive dictionaries 
822 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
823
824 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar 
825 newGivOrDerEvVar pty evtrm 
826   = do { ev <- wrapTcS $ TcM.newEvVar pty 
827        ; setEvBind ev evtrm 
828        ; return ev }
829
830 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
831 -- Note we create immutable variables for given or derived, since we
832 -- must bind them to TcEvBinds (because their evidence may involve 
833 -- superclasses). However we should be able to override existing
834 -- 'derived' evidence, even in TcEvBinds 
835 newGivOrDerCoVar ty1 ty2 co 
836   = do { cv <- newCoVar ty1 ty2
837        ; setEvBind cv (EvCoercion co) 
838        ; return cv } 
839
840 newWantedCoVar :: TcType -> TcType -> TcS EvVar 
841 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
842
843
844 newCoVar :: TcType -> TcType -> TcS EvVar 
845 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
846
847 newIPVar :: IPName Name -> TcType -> TcS EvVar 
848 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
849
850 newDictVar :: Class -> [TcType] -> TcS EvVar 
851 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
852 \end{code} 
853
854
855 \begin{code} 
856 isGoodRecEv :: EvVar -> EvVar -> TcS Bool
857 -- In a call (isGoodRecEv ev wv), we are considering solving wv 
858 -- using some term that involves ev, such as:
859 -- by setting           wv = ev
860 -- or                   wv = EvCast x |> ev
861 -- etc. 
862 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
863 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev 
864 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
865 --
866 -- Guarded means: more instance calls than superclass selections. We
867 -- compute this by chasing the evidence, adding +1 for every instance
868 -- call (constructor) and -1 for every superclass selection (destructor).
869 --
870 -- See Note [Superclasses and recursive dictionaries] in TcInteract
871 isGoodRecEv ev_var wv
872   = do { tc_evbinds <- getTcEvBindsBag 
873        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var 
874        ; return $ case mb of 
875                     Nothing -> True 
876                     Just min_guardedness -> min_guardedness > 0
877        }
878
879   where chase_ev_var :: EvBindMap   -- Evidence binds 
880                  -> EvVar           -- Target variable whose gravity we want to return
881                  -> Int             -- Current gravity 
882                  -> [EvVar]         -- Visited nodes
883                  -> EvVar           -- Current node 
884                  -> TcS (Maybe Int)
885         chase_ev_var assocs trg curr_grav visited orig
886             | trg == orig         = return $ Just curr_grav
887             | orig `elem` visited = return $ Nothing 
888             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
889             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
890
891             | otherwise = return Nothing
892
893         chase_ev assocs trg curr_grav visited (EvId v) 
894             = chase_ev_var assocs trg curr_grav visited v
895         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) 
896             = chase_ev_var assocs trg (curr_grav-1) visited d_id
897         chase_ev assocs trg curr_grav visited (EvCast v co)
898             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
899                  ; m2 <- chase_co assocs trg curr_grav visited co
900                  ; return (comb_chase_res Nothing [m1,m2]) } 
901
902         chase_ev assocs trg curr_grav visited (EvCoercion co)
903             = chase_co assocs trg curr_grav visited co
904         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ ev_deps)
905             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
906                  ; return (comb_chase_res Nothing chase_results) }
907
908         chase_co assocs trg curr_grav visited co 
909             = -- Look for all the coercion variables in the coercion 
910               -- chase them, and combine the results. This is OK since the
911               -- coercion will not contain any superclass terms -- anything 
912               -- that involves dictionaries will be bound in assocs. 
913               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
914                                              (tyVarsOfType co)
915               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
916                     ; return (comb_chase_res Nothing chase_results) } 
917
918         comb_chase_res f []                   = f 
919         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest 
920         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
921         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest 
922
923
924 -- Matching and looking up classes and family instances
925 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
926
927 data MatchInstResult mi
928   = MatchInstNo         -- No matching instance 
929   | MatchInstSingle mi  -- Single matching instance
930   | MatchInstMany       -- Multiple matching instances
931
932
933 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
934 -- Look up a class constraint in the instance environment
935 matchClass clas tys
936   = do  { let pred = mkClassPred clas tys 
937         ; instEnvs <- getInstEnvs
938         ; case lookupInstEnv instEnvs clas tys of {
939             ([], unifs)               -- Nothing matches  
940                 -> do { traceTcS "matchClass not matching"
941                                  (vcat [ text "dict" <+> ppr pred, 
942                                          text "unifs" <+> ppr unifs ]) 
943                       ; return MatchInstNo  
944                       } ;  
945             ([(ispec, inst_tys)], []) -- A single match 
946                 -> do   { let dfun_id = is_dfun ispec
947                         ; traceTcS "matchClass success"
948                                    (vcat [text "dict" <+> ppr pred, 
949                                           text "witness" <+> ppr dfun_id
950                                            <+> ppr (idType dfun_id) ])
951                                   -- Record that this dfun is needed
952                         ; return $ MatchInstSingle (dfun_id, inst_tys)
953                         } ;
954             (matches, unifs)          -- More than one matches 
955                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
956                                    (vcat [text "dict" <+> ppr pred,
957                                           text "matches" <+> ppr matches,
958                                           text "unifs" <+> ppr unifs])
959                         ; return MatchInstMany 
960                         }
961         }
962         }
963
964 matchFam :: TyCon
965          -> [Type] 
966          -> TcS (MatchInstResult (TyCon, [Type]))
967 matchFam tycon args
968   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
969        ; case mb of 
970            Nothing  -> return MatchInstNo 
971            Just res -> return $ MatchInstSingle res
972        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
973        -- multiple matches. Check. 
974        }
975
976
977 -- Functional dependencies, instantiation of equations
978 -------------------------------------------------------
979
980 mkWantedFunDepEqns :: WantedLoc
981                    -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
982                    -> TcS [WantedEvVar] 
983 mkWantedFunDepEqns _   [] = return []
984 mkWantedFunDepEqns loc eqns
985   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
986        ; wevvars <- mapM to_work_item eqns
987        ; return $ concat wevvars }
988   where
989     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
990     to_work_item ((qtvs, pairs), d1, d2)
991       = do { let tvs = varSetElems qtvs
992            ; tvs' <- mapM instFlexiTcS tvs
993            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
994                  loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
995            ; mapM (do_one subst loc') pairs }
996
997     do_one subst loc' (ty1, ty2)
998        = do { let sty1 = substTy subst ty1
999                   sty2 = substTy subst ty2
1000             ; ev <- newWantedCoVar sty1 sty2
1001             ; return (WantedEvVar ev loc') }
1002
1003 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
1004 pprEquationDoc (eqn, (p1, _), (p2, _)) 
1005   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1006
1007 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1008          -> TcM (TidyEnv, SDoc)
1009 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1010   = do  { pred1' <- TcM.zonkTcPredType pred1
1011         ; pred2' <- TcM.zonkTcPredType pred2
1012         ; let { pred1'' = tidyPred tidy_env pred1'
1013               ; pred2'' = tidyPred tidy_env pred2' }
1014         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1015                           nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
1016                           nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1017         ; return (tidy_env, msg) }
1018 \end{code}