Moved canonicalisation inside solveInteract
[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
464 instance Outputable SimplContext where
465   ppr SimplInfer       = ptext (sLit "SimplInfer")
466   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
467   ppr SimplInteractive = ptext (sLit "SimplInteractive")
468   ppr SimplCheck       = ptext (sLit "SimplCheck")
469
470 isInteractive :: SimplContext -> Bool
471 isInteractive SimplInteractive = True
472 isInteractive _                = False
473
474 simplEqsOnly :: SimplContext -> Bool
475 -- Simplify equalities only, not dictionaries
476 -- This is used for the LHS of rules; ee
477 -- Note [Simplifying RULE lhs constraints] in TcSimplify
478 simplEqsOnly SimplRuleLhs = True
479 simplEqsOnly _            = False
480
481 performDefaulting :: SimplContext -> Bool
482 performDefaulting SimplInfer       = False
483 performDefaulting SimplRuleLhs     = False
484 performDefaulting SimplInteractive = True
485 performDefaulting SimplCheck       = True
486
487 ---------------
488 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
489
490 instance Functor TcS where
491   fmap f m = TcS $ fmap f . unTcS m
492
493 instance Monad TcS where 
494   return x  = TcS (\_ -> return x) 
495   fail err  = TcS (\_ -> fail err) 
496   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
497
498 -- Basic functionality 
499 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
500 wrapTcS :: TcM a -> TcS a 
501 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
502 -- and TcS is supposed to have limited functionality
503 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
504
505 wrapErrTcS :: TcM a -> TcS a 
506 -- The thing wrapped should just fail
507 -- There's no static check; it's up to the user
508 -- Having a variant for each error message is too painful
509 wrapErrTcS = wrapTcS
510
511 wrapWarnTcS :: TcM a -> TcS a 
512 -- The thing wrapped should just add a warning, or no-op
513 -- There's no static check; it's up to the user
514 wrapWarnTcS = wrapTcS
515
516 failTcS, panicTcS :: SDoc -> TcS a
517 failTcS      = wrapTcS . TcM.failWith
518 panicTcS doc = pprPanic "TcCanonical" doc
519
520 traceTcS :: String -> SDoc -> TcS ()
521 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
522
523 traceTcS0 :: String -> SDoc -> TcS ()
524 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
525
526 runTcS :: SimplContext
527        -> Untouchables         -- Untouchables
528        -> TcS a                -- What to run
529        -> TcM (a, Bag FrozenError, Bag EvBind)
530 runTcS context untouch tcs 
531   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
532        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
533        ; err_ref <- TcM.newTcRef emptyBag
534        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
535                           , tcs_ty_binds = ty_binds_var
536                           , tcs_context  = context
537                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
538                           , tcs_errors   = err_ref
539                           }
540
541              -- Run the computation
542        ; res <- unTcS tcs env
543              -- Perform the type unifications required
544        ; ty_binds <- TcM.readTcRef ty_binds_var
545        ; mapM_ do_unification (varEnvElts ty_binds)
546
547              -- And return
548        ; frozen_errors <- TcM.readTcRef err_ref
549        ; ev_binds      <- TcM.readTcRef evb_ref
550        ; return (res, frozen_errors, evBindMapBinds ev_binds) }
551   where
552     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
553
554 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
555 nestImplicTcS ref untch (TcS thing_inside)
556   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, 
557                      tcs_context = ctxt, 
558                      tcs_errors = err_ref } ->
559     let 
560        nest_env = TcSEnv { tcs_ev_binds = ref
561                          , tcs_ty_binds = ty_binds
562                          , tcs_untch    = untch
563                          , tcs_context  = ctxtUnderImplic ctxt 
564                          , tcs_errors   = err_ref }
565     in 
566     thing_inside nest_env
567
568 recoverTcS :: TcS a -> TcS a -> TcS a
569 recoverTcS (TcS recovery_code) (TcS thing_inside)
570   = TcS $ \ env ->
571     TcM.recoverM (recovery_code env) (thing_inside env)
572
573 ctxtUnderImplic :: SimplContext -> SimplContext
574 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
575 ctxtUnderImplic SimplRuleLhs = SimplCheck
576 ctxtUnderImplic ctxt         = ctxt
577
578 tryTcS :: TcS a -> TcS a
579 -- Like runTcS, but from within the TcS monad 
580 -- Ignore all the evidence generated, and do not affect caller's evidence!
581 tryTcS tcs 
582   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
583                     ; ev_binds_var <- TcM.newTcEvBinds
584                     ; err_ref      <- TcM.newTcRef emptyBag
585                     ; let env1 = env { tcs_ev_binds = ev_binds_var
586                                      , tcs_ty_binds = ty_binds_var 
587                                      , tcs_errors   = err_ref }
588                     ; unTcS tcs env1 })
589
590 -- Update TcEvBinds 
591 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
592
593 getDynFlags :: TcS DynFlags
594 getDynFlags = wrapTcS TcM.getDOpts
595
596 getTcSContext :: TcS SimplContext
597 getTcSContext = TcS (return . tcs_context)
598
599 getTcEvBinds :: TcS EvBindsVar
600 getTcEvBinds = TcS (return . tcs_ev_binds) 
601
602 getUntouchables :: TcS TcsUntouchables
603 getUntouchables = TcS (return . tcs_untch)
604
605 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
606 getTcSTyBinds = TcS (return . tcs_ty_binds)
607
608 getTcSErrors :: TcS (IORef (Bag FrozenError))
609 getTcSErrors = TcS (return . tcs_errors)
610
611 getTcSErrorsBag :: TcS (Bag FrozenError) 
612 getTcSErrorsBag = do { err_ref <- getTcSErrors 
613                      ; wrapTcS $ TcM.readTcRef err_ref }
614
615 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) 
616 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
617
618
619 getTcEvBindsBag :: TcS EvBindMap
620 getTcEvBindsBag
621   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
622        ; wrapTcS $ TcM.readTcRef ev_ref }
623
624 setWantedCoBind :: CoVar -> Coercion -> TcS () 
625 setWantedCoBind cv co 
626   = setEvBind cv (EvCoercion co)
627      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 
628
629 setDerivedCoBind :: CoVar -> Coercion -> TcS () 
630 setDerivedCoBind cv co 
631   = setEvBind cv (EvCoercion co)
632
633 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
634 -- Add a type binding
635 -- We never do this twice!
636 setWantedTyBind tv ty 
637   = do { ref <- getTcSTyBinds
638        ; wrapTcS $ 
639          do { ty_binds <- TcM.readTcRef ref
640 #ifdef DEBUG
641             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
642               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
643                    , ppr tv <+> text ":=" <+> ppr ty
644                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
645 #endif
646             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
647
648 setIPBind :: EvVar -> EvTerm -> TcS () 
649 setIPBind = setEvBind 
650
651 setDictBind :: EvVar -> EvTerm -> TcS () 
652 setDictBind = setEvBind 
653
654 setEvBind :: EvVar -> EvTerm -> TcS () 
655 -- Internal
656 setEvBind ev rhs 
657   = do { tc_evbinds <- getTcEvBinds 
658        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
659
660 newTcEvBindsTcS :: TcS EvBindsVar
661 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
662
663 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
664 warnTcS loc warn_if doc 
665   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
666   | otherwise = return ()
667
668 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
669 getDefaultInfo 
670   = do { ctxt <- getTcSContext
671        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
672        ; return (ctxt, tys, flags) }
673
674
675
676 -- Recording errors in the TcS monad
677 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
678
679 addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
680 addErrorTcS frknd fl ty1 ty2
681   = do { err_ref <- getTcSErrors
682        ; wrapTcS $ do
683        { TcM.updTcRef err_ref $ \ errs ->
684            consBag (FrozenError frknd fl ty1 ty2) errs
685
686            -- If there's an error in the *given* constraints,
687            -- stop right now, to avoid a cascade of errors
688            -- in the wanteds
689        ; when (isGiven fl) TcM.failM
690
691        ; return () } }
692
693 -- Just get some environments needed for instance looking up and matching
694 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
695
696 getInstEnvs :: TcS (InstEnv, InstEnv) 
697 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
698
699 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
700 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
701
702 getTopEnv :: TcS HscEnv 
703 getTopEnv = wrapTcS $ TcM.getTopEnv 
704
705 getGblEnv :: TcS TcGblEnv 
706 getGblEnv = wrapTcS $ TcM.getGblEnv 
707
708 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
709 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
710
711 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
712 checkWellStagedDFun pred dfun_id loc 
713   = wrapTcS $ TcM.setCtLoc loc $ 
714     do { use_stage <- TcM.getStage
715        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
716   where
717     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
718     bind_lvl = TcM.topIdLvl dfun_id
719
720 pprEq :: TcType -> TcType -> SDoc
721 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
722
723 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
724 isTouchableMetaTyVar tv 
725   = do { untch <- getUntouchables
726        ; return $ isTouchableMetaTyVar_InRange untch tv } 
727
728 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
729 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
730   = case tcTyVarDetails tv of 
731       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
732                         -- See Note [Touchable meta type variables] 
733       MetaTv {}      -> inTouchableRange untch tv 
734       _              -> False 
735
736
737 \end{code}
738
739
740 Note [Touchable meta type variables]
741 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
742 Meta type variables allocated *by the constraint solver itself* are always
743 touchable.  Example: 
744    instance C a b => D [a] where...
745 if we use this instance declaration we "make up" a fresh meta type
746 variable for 'b', which we must later guess.  (Perhaps C has a
747 functional dependency.)  But since we aren't in the constraint *generator*
748 we can't allocate a Unique in the touchable range for this implication
749 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
750
751
752 \begin{code}
753 -- Flatten skolems
754 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
755
756 newFlattenSkolemTy :: TcType -> TcS TcType
757 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
758
759 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
760 newFlattenSkolemTyVar ty
761   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
762                             ; let name = mkSysTvName uniq (fsLit "f")
763                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
764        ; traceTcS "New Flatten Skolem Born" $ 
765            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
766        ; return tv }
767
768 -- Instantiations 
769 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
770
771 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
772 instDFunTypes mb_inst_tys 
773   = mapM inst_tv mb_inst_tys
774   where
775     inst_tv :: Either TyVar TcType -> TcS Type
776     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
777     inst_tv (Right ty) = return ty 
778
779 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
780 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
781
782
783 instFlexiTcS :: TyVar -> TcS TcTyVar 
784 -- Like TcM.instMetaTyVar but the variable that is created is always
785 -- touchable; we are supposed to guess its instantiation. 
786 -- See Note [Touchable meta type variables] 
787 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
788
789 newFlexiTcSTy :: Kind -> TcS TcType  
790 newFlexiTcSTy knd 
791   = wrapTcS $
792     do { uniq <- TcM.newUnique 
793        ; ref  <- TcM.newMutVar  Flexi 
794        ; let name = mkSysTvName uniq (fsLit "uf")
795        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
796
797 isFlexiTcsTv :: TyVar -> Bool
798 isFlexiTcsTv tv
799   | not (isTcTyVar tv)                  = False
800   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
801   | otherwise                           = False
802
803 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
804 -- Create new wanted CoVar that constrains the type to have the specified kind. 
805 newKindConstraint tv knd 
806   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
807        ; let ty_k = mkTyVarTy tv_k
808        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
809        ; return co_var }
810
811 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
812 instFlexiTcSHelper tvname tvkind
813   = wrapTcS $ 
814     do { uniq <- TcM.newUnique 
815        ; ref  <- TcM.newMutVar  Flexi 
816        ; let name = setNameUnique tvname uniq 
817              kind = tvkind 
818        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
819
820 -- Superclasses and recursive dictionaries 
821 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
822
823 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar 
824 newGivOrDerEvVar pty evtrm 
825   = do { ev <- wrapTcS $ TcM.newEvVar pty 
826        ; setEvBind ev evtrm 
827        ; return ev }
828
829 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
830 -- Note we create immutable variables for given or derived, since we
831 -- must bind them to TcEvBinds (because their evidence may involve 
832 -- superclasses). However we should be able to override existing
833 -- 'derived' evidence, even in TcEvBinds 
834 newGivOrDerCoVar ty1 ty2 co 
835   = do { cv <- newCoVar ty1 ty2
836        ; setEvBind cv (EvCoercion co) 
837        ; return cv } 
838
839 newWantedCoVar :: TcType -> TcType -> TcS EvVar 
840 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
841
842
843 newCoVar :: TcType -> TcType -> TcS EvVar 
844 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
845
846 newIPVar :: IPName Name -> TcType -> TcS EvVar 
847 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
848
849 newDictVar :: Class -> [TcType] -> TcS EvVar 
850 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
851 \end{code} 
852
853
854 \begin{code} 
855 isGoodRecEv :: EvVar -> EvVar -> TcS Bool
856 -- In a call (isGoodRecEv ev wv), we are considering solving wv 
857 -- using some term that involves ev, such as:
858 -- by setting           wv = ev
859 -- or                   wv = EvCast x |> ev
860 -- etc. 
861 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
862 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev 
863 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
864 --
865 -- Guarded means: more instance calls than superclass selections. We
866 -- compute this by chasing the evidence, adding +1 for every instance
867 -- call (constructor) and -1 for every superclass selection (destructor).
868 --
869 -- See Note [Superclasses and recursive dictionaries] in TcInteract
870 isGoodRecEv ev_var wv
871   = do { tc_evbinds <- getTcEvBindsBag 
872        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var 
873        ; return $ case mb of 
874                     Nothing -> True 
875                     Just min_guardedness -> min_guardedness > 0
876        }
877
878   where chase_ev_var :: EvBindMap   -- Evidence binds 
879                  -> EvVar           -- Target variable whose gravity we want to return
880                  -> Int             -- Current gravity 
881                  -> [EvVar]         -- Visited nodes
882                  -> EvVar           -- Current node 
883                  -> TcS (Maybe Int)
884         chase_ev_var assocs trg curr_grav visited orig
885             | trg == orig         = return $ Just curr_grav
886             | orig `elem` visited = return $ Nothing 
887             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
888             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
889
890             | otherwise = return Nothing
891
892         chase_ev assocs trg curr_grav visited (EvId v) 
893             = chase_ev_var assocs trg curr_grav visited v
894         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) 
895             = chase_ev_var assocs trg (curr_grav-1) visited d_id
896         chase_ev assocs trg curr_grav visited (EvCast v co)
897             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
898                  ; m2 <- chase_co assocs trg curr_grav visited co
899                  ; return (comb_chase_res Nothing [m1,m2]) } 
900
901         chase_ev assocs trg curr_grav visited (EvCoercion co)
902             = chase_co assocs trg curr_grav visited co
903         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ _ev_vars ev_deps)
904             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
905                                     -- Notice that we chase the ev_deps and not the ev_vars
906                                     -- See Note [Dependencies in self dictionaries] in TcSimplify
907                  ; return (comb_chase_res Nothing chase_results) }
908
909         chase_co assocs trg curr_grav visited co 
910             = -- Look for all the coercion variables in the coercion 
911               -- chase them, and combine the results. This is OK since the
912               -- coercion will not contain any superclass terms -- anything 
913               -- that involves dictionaries will be bound in assocs. 
914               let co_vars       = foldVarSet (\v vrs -> if isCoVar v then (v:vrs) else vrs) []
915                                              (tyVarsOfType co)
916               in do { chase_results <- mapM (chase_ev_var assocs trg curr_grav visited) co_vars
917                     ; return (comb_chase_res Nothing chase_results) } 
918
919         comb_chase_res f []                   = f 
920         comb_chase_res f (Nothing:rest)       = comb_chase_res f rest 
921         comb_chase_res Nothing (Just n:rest)  = comb_chase_res (Just n) rest
922         comb_chase_res (Just m) (Just n:rest) = comb_chase_res (Just (min n m)) rest 
923
924
925 -- Matching and looking up classes and family instances
926 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
927
928 data MatchInstResult mi
929   = MatchInstNo         -- No matching instance 
930   | MatchInstSingle mi  -- Single matching instance
931   | MatchInstMany       -- Multiple matching instances
932
933
934 matchClass :: Class -> [Type] -> TcS (MatchInstResult (DFunId, [Either TyVar TcType])) 
935 -- Look up a class constraint in the instance environment
936 matchClass clas tys
937   = do  { let pred = mkClassPred clas tys 
938         ; instEnvs <- getInstEnvs
939         ; case lookupInstEnv instEnvs clas tys of {
940             ([], unifs)               -- Nothing matches  
941                 -> do { traceTcS "matchClass not matching"
942                                  (vcat [ text "dict" <+> ppr pred, 
943                                          text "unifs" <+> ppr unifs ]) 
944                       ; return MatchInstNo  
945                       } ;  
946             ([(ispec, inst_tys)], []) -- A single match 
947                 -> do   { let dfun_id = is_dfun ispec
948                         ; traceTcS "matchClass success"
949                                    (vcat [text "dict" <+> ppr pred, 
950                                           text "witness" <+> ppr dfun_id
951                                            <+> ppr (idType dfun_id) ])
952                                   -- Record that this dfun is needed
953                         ; return $ MatchInstSingle (dfun_id, inst_tys)
954                         } ;
955             (matches, unifs)          -- More than one matches 
956                 -> do   { traceTcS "matchClass multiple matches, deferring choice"
957                                    (vcat [text "dict" <+> ppr pred,
958                                           text "matches" <+> ppr matches,
959                                           text "unifs" <+> ppr unifs])
960                         ; return MatchInstMany 
961                         }
962         }
963         }
964
965 matchFam :: TyCon
966          -> [Type] 
967          -> TcS (MatchInstResult (TyCon, [Type]))
968 matchFam tycon args
969   = do { mb <- wrapTcS $ TcM.tcLookupFamInst tycon args
970        ; case mb of 
971            Nothing  -> return MatchInstNo 
972            Just res -> return $ MatchInstSingle res
973        -- DV: We never return MatchInstMany, since tcLookupFamInst never returns 
974        -- multiple matches. Check. 
975        }
976
977
978 -- Functional dependencies, instantiation of equations
979 -------------------------------------------------------
980
981 mkWantedFunDepEqns :: WantedLoc
982                    -> [(Equation, (PredType, SDoc), (PredType, SDoc))]
983                    -> TcS [WantedEvVar] 
984 mkWantedFunDepEqns _   [] = return []
985 mkWantedFunDepEqns loc eqns
986   = do { traceTcS "Improve:" (vcat (map pprEquationDoc eqns))
987        ; wevvars <- mapM to_work_item eqns
988        ; return $ concat wevvars }
989   where
990     to_work_item :: (Equation, (PredType,SDoc), (PredType,SDoc)) -> TcS [WantedEvVar]
991     to_work_item ((qtvs, pairs), d1, d2)
992       = do { let tvs = varSetElems qtvs
993            ; tvs' <- mapM instFlexiTcS tvs
994            ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs')
995                  loc'  = pushErrCtxt FunDepOrigin (False, mkEqnMsg d1 d2) loc
996            ; mapM (do_one subst loc') pairs }
997
998     do_one subst loc' (ty1, ty2)
999        = do { let sty1 = substTy subst ty1
1000                   sty2 = substTy subst ty2
1001             ; ev <- newWantedCoVar sty1 sty2
1002             ; return (WantedEvVar ev loc') }
1003
1004 pprEquationDoc :: (Equation, (PredType, SDoc), (PredType, SDoc)) -> SDoc
1005 pprEquationDoc (eqn, (p1, _), (p2, _)) 
1006   = vcat [pprEquation eqn, nest 2 (ppr p1), nest 2 (ppr p2)]
1007
1008 mkEqnMsg :: (TcPredType, SDoc) -> (TcPredType, SDoc) -> TidyEnv
1009          -> TcM (TidyEnv, SDoc)
1010 mkEqnMsg (pred1,from1) (pred2,from2) tidy_env
1011   = do  { pred1' <- TcM.zonkTcPredType pred1
1012         ; pred2' <- TcM.zonkTcPredType pred2
1013         ; let { pred1'' = tidyPred tidy_env pred1'
1014               ; pred2'' = tidyPred tidy_env pred2' }
1015         ; let msg = vcat [ptext (sLit "When using functional dependencies to combine"),
1016                           nest 2 (sep [ppr pred1'' <> comma, nest 2 from1]), 
1017                           nest 2 (sep [ppr pred2'' <> comma, nest 2 from2])]
1018         ; return (tidy_env, msg) }
1019 \end{code}