Fix a recomp bug: make classes/datatypes depend directly on DFuns (#4469)
[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 :: CanonicalCts -> CanonicalCts
185 makeGivens = mapBag (\ct -> ct { cc_flavor = mkGivenFlavor (cc_flavor ct) UnkSkol })
186            -- The UnkSkol doesn't matter because these givens are
187            -- not contradictory (else we'd have rejected them already)
188
189 makeSolvedByInst :: CanonicalCt -> CanonicalCt
190 -- Record that a constraint is now solved
191 --        Wanted         -> Derived
192 --        Given, Derived -> no-op
193 makeSolvedByInst ct 
194   | Wanted loc <- cc_flavor ct = ct { cc_flavor = Derived loc DerInst }
195   | otherwise                  = ct
196
197 mkWantedConstraints :: CanonicalCts -> Bag Implication -> WantedConstraints
198 mkWantedConstraints flats implics 
199   = mapBag (WcEvVar . deCanonicaliseWanted) flats `unionBags` mapBag WcImplic implics
200
201 deCanonicaliseWanted :: CanonicalCt -> WantedEvVar
202 deCanonicaliseWanted ct 
203   = WARN( not (isWanted $ cc_flavor ct), ppr ct ) 
204     let Wanted loc = cc_flavor ct 
205     in WantedEvVar (cc_id ct) loc
206
207 tyVarsOfCanonical :: CanonicalCt -> TcTyVarSet
208 tyVarsOfCanonical (CTyEqCan { cc_tyvar = tv, cc_rhs = xi })    = extendVarSet (tyVarsOfType xi) tv
209 tyVarsOfCanonical (CFunEqCan { cc_tyargs = tys, cc_rhs = xi }) = tyVarsOfTypes (xi:tys)
210 tyVarsOfCanonical (CDictCan { cc_tyargs = tys })               = tyVarsOfTypes tys
211 tyVarsOfCanonical (CIPCan { cc_ip_ty = ty })                   = tyVarsOfType ty
212
213 tyVarsOfCDict :: CanonicalCt -> TcTyVarSet 
214 tyVarsOfCDict (CDictCan { cc_tyargs = tys }) = tyVarsOfTypes tys
215 tyVarsOfCDict _ct                            = emptyVarSet 
216
217 tyVarsOfCDicts :: CanonicalCts -> TcTyVarSet 
218 tyVarsOfCDicts = foldrBag (unionVarSet . tyVarsOfCDict) emptyVarSet
219
220 tyVarsOfCanonicals :: CanonicalCts -> TcTyVarSet
221 tyVarsOfCanonicals = foldrBag (unionVarSet . tyVarsOfCanonical) emptyVarSet
222
223 instance Outputable CanonicalCt where
224   ppr (CDictCan d fl cls tys)     
225       = ppr fl <+> ppr d  <+> dcolon <+> pprClassPred cls tys
226   ppr (CIPCan ip fl ip_nm ty)     
227       = ppr fl <+> ppr ip <+> dcolon <+> parens (ppr ip_nm <> dcolon <> ppr ty)
228   ppr (CTyEqCan co fl tv ty)      
229       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyVarTy tv, ty)
230   ppr (CFunEqCan co fl tc tys ty) 
231       = ppr fl <+> ppr co <+> dcolon <+> pprEqPred (mkTyConApp tc tys, ty)
232 \end{code}
233
234 Note [Canonical implicit parameter constraints]
235 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
236 The type in a canonical implicit parameter constraint doesn't need to
237 be a xi (type-function-free type) since we can defer the flattening
238 until checking this type for equality with another type.  If we
239 encounter two IP constraints with the same name, they MUST have the
240 same type, and at that point we can generate a flattened equality
241 constraint between the types.  (On the other hand, the types in two
242 class constraints for the same class MAY be equal, so they need to be
243 flattened in the first place to facilitate comparing them.)
244
245 \begin{code}
246 singleCCan :: CanonicalCt -> CanonicalCts 
247 singleCCan = unitBag 
248
249 andCCan :: CanonicalCts -> CanonicalCts -> CanonicalCts 
250 andCCan = unionBags
251
252 extendCCans :: CanonicalCts -> CanonicalCt -> CanonicalCts 
253 extendCCans = snocBag 
254
255 andCCans :: [CanonicalCts] -> CanonicalCts 
256 andCCans = unionManyBags
257
258 emptyCCan :: CanonicalCts 
259 emptyCCan = emptyBag
260
261 isEmptyCCan :: CanonicalCts -> Bool
262 isEmptyCCan = isEmptyBag
263
264 isCTyEqCan :: CanonicalCt -> Bool 
265 isCTyEqCan (CTyEqCan {})  = True 
266 isCTyEqCan (CFunEqCan {}) = False
267 isCTyEqCan _              = False 
268
269 isCDictCan_Maybe :: CanonicalCt -> Maybe Class
270 isCDictCan_Maybe (CDictCan {cc_class = cls })  = Just cls
271 isCDictCan_Maybe _              = Nothing
272
273 isCIPCan_Maybe :: CanonicalCt -> Maybe (IPName Name)
274 isCIPCan_Maybe  (CIPCan {cc_ip_nm = nm }) = Just nm
275 isCIPCan_Maybe _                = Nothing
276
277 isCFunEqCan_Maybe :: CanonicalCt -> Maybe TyCon
278 isCFunEqCan_Maybe (CFunEqCan { cc_fun = tc }) = Just tc
279 isCFunEqCan_Maybe _ = Nothing
280
281 \end{code}
282
283 %************************************************************************
284 %*                                                                      *
285                     CtFlavor
286          The "flavor" of a canonical constraint
287 %*                                                                      *
288 %************************************************************************
289
290 \begin{code}
291 data CtFlavor 
292   = Given   GivenLoc  -- We have evidence for this constraint in TcEvBinds
293   | Derived WantedLoc DerivedOrig
294                       -- We have evidence for this constraint in TcEvBinds;
295                       --   *however* this evidence can contain wanteds, so 
296                       --   it's valid only provisionally to the solution of
297                       --   these wanteds 
298   | Wanted WantedLoc  -- We have no evidence bindings for this constraint. 
299
300 data DerivedOrig = DerSC | DerInst | DerSelf
301 -- Deriveds are either superclasses of other wanteds or deriveds, or partially 
302 -- solved wanteds from instances, or 'self' dictionaries containing yet wanted
303 -- superclasses. 
304
305 instance Outputable CtFlavor where 
306   ppr (Given _)    = ptext (sLit "[Given]")
307   ppr (Wanted _)   = ptext (sLit "[Wanted]")
308   ppr (Derived {}) = ptext (sLit "[Derived]") 
309
310 isWanted :: CtFlavor -> Bool 
311 isWanted (Wanted {}) = True
312 isWanted _           = False
313
314 isGiven :: CtFlavor -> Bool 
315 isGiven (Given {}) = True 
316 isGiven _          = False 
317
318 isDerived :: CtFlavor -> Bool 
319 isDerived (Derived {}) = True
320 isDerived _            = False
321
322 pprFlavorArising :: CtFlavor -> SDoc
323 pprFlavorArising (Derived wl _) = pprArisingAt wl
324 pprFlavorArising (Wanted  wl)   = pprArisingAt wl
325 pprFlavorArising (Given gl)     = pprArisingAt gl
326
327 getWantedLoc :: CanonicalCt -> WantedLoc
328 getWantedLoc ct 
329   = ASSERT (isWanted (cc_flavor ct))
330     case cc_flavor ct of 
331       Wanted wl -> wl 
332       _         -> pprPanic "Can't get WantedLoc of non-wanted constraint!" empty
333
334
335 isWantedCt :: CanonicalCt -> Bool 
336 isWantedCt ct = isWanted (cc_flavor ct)
337 isGivenCt :: CanonicalCt -> Bool 
338 isGivenCt ct = isGiven (cc_flavor ct) 
339
340 canSolve :: CtFlavor -> CtFlavor -> Bool 
341 -- canSolve ctid1 ctid2 
342 -- The constraint ctid1 can be used to solve ctid2 
343 -- "to solve" means a reaction where the active parts of the two constraints match.
344 --  active(F xis ~ xi) = F xis 
345 --  active(tv ~ xi)    = tv 
346 --  active(D xis)      = D xis 
347 --  active(IP nm ty)   = nm 
348 -----------------------------------------
349 canSolve (Given {})   _            = True 
350 canSolve (Derived {}) (Wanted {})  = True 
351 canSolve (Derived {}) (Derived {}) = True 
352 canSolve (Wanted {})  (Wanted {})  = True
353 canSolve _ _ = False
354
355 canRewrite :: CtFlavor -> CtFlavor -> Bool 
356 -- canRewrite ctid1 ctid2 
357 -- The *equality_constraint* ctid1 can be used to rewrite inside ctid2 
358 canRewrite = canSolve 
359
360 combineCtLoc :: CtFlavor -> CtFlavor -> WantedLoc
361 -- Precondition: At least one of them should be wanted 
362 combineCtLoc (Wanted loc) _    = loc 
363 combineCtLoc _ (Wanted loc)    = loc 
364 combineCtLoc (Derived loc _) _ = loc 
365 combineCtLoc _ (Derived loc _) = loc 
366 combineCtLoc _ _ = panic "combineCtLoc: both given"
367
368 mkGivenFlavor :: CtFlavor -> SkolemInfo -> CtFlavor
369 mkGivenFlavor (Wanted  loc)   sk = Given (setCtLocOrigin loc sk)
370 mkGivenFlavor (Derived loc _) sk = Given (setCtLocOrigin loc sk)
371 mkGivenFlavor (Given   loc)   sk = Given (setCtLocOrigin loc sk)
372
373 mkWantedFlavor :: CtFlavor -> CtFlavor
374 mkWantedFlavor (Wanted  loc)   = Wanted loc
375 mkWantedFlavor (Derived loc _) = Wanted loc
376 mkWantedFlavor fl@(Given {})   = pprPanic "mkWantedFlavour" (ppr fl)
377 \end{code}
378
379
380 %************************************************************************
381 %*                                                                      *
382 %*              The TcS solver monad                                    *
383 %*                                                                      *
384 %************************************************************************
385
386 Note [The TcS monad]
387 ~~~~~~~~~~~~~~~~~~~~
388 The TcS monad is a weak form of the main Tc monad
389
390 All you can do is
391     * fail
392     * allocate new variables
393     * fill in evidence variables
394
395 Filling in a dictionary evidence variable means to create a binding
396 for it, so TcS carries a mutable location where the binding can be
397 added.  This is initialised from the innermost implication constraint.
398
399 \begin{code}
400 data TcSEnv
401   = TcSEnv { 
402       tcs_ev_binds :: EvBindsVar,
403           -- Evidence bindings
404
405       tcs_ty_binds :: IORef (TyVarEnv (TcTyVar, TcType)),
406           -- Global type bindings
407
408       tcs_context :: SimplContext,
409                      
410       tcs_errors :: IORef (Bag FrozenError), 
411           -- Frozen errors that we defer reporting as much as possible, in order to
412           -- make them as informative as possible. See Note [Frozen Errors]
413
414       tcs_untch :: TcsUntouchables 
415     }
416
417 type TcsUntouchables = (Untouchables,TcTyVarSet)
418 -- Like the TcM Untouchables, 
419 -- but records extra TcsTv variables generated during simplification
420 -- See Note [Extra TcsTv untouchables] in TcSimplify
421
422 data FrozenError
423   = FrozenError ErrorKind CtFlavor TcType TcType 
424
425 data ErrorKind
426   = MisMatchError | OccCheckError | KindError
427
428 instance Outputable FrozenError where 
429   ppr (FrozenError _frknd fl ty1 ty2) = ppr fl <+> pprEq ty1 ty2 <+> text "(frozen)"
430
431 \end{code}
432
433 Note [Frozen Errors] 
434 ~~~~~~~~~~~~~~~~~~~~
435 Some of the errors that we get during canonicalization are best reported when all constraints
436 have been simplified as much as possible. For instance, assume that during simplification
437 the following constraints arise: 
438    
439  [Wanted]   F alpha ~  uf1 
440  [Wanted]   beta ~ uf1 beta 
441
442 When canonicalizing the wanted (beta ~ uf1 beta), if we eagerly fail we will simply 
443 see a message: 
444     'Can't construct the infinite type  beta ~ uf1 beta' 
445 and the user has no idea what the uf1 variable is.
446
447 Instead our plan is that we will NOT fail immediately, but:
448     (1) Record the "frozen" error in the tcs_errors field 
449     (2) Isolate the offending constraint from the rest of the inerts 
450     (3) Keep on simplifying/canonicalizing
451
452 At the end, we will hopefully have substituted uf1 := F alpha, and we will be able to 
453 report a more informative error: 
454     'Can't construct the infinite type beta ~ F alpha beta'
455 \begin{code}
456
457 data SimplContext
458   = SimplInfer          -- Inferring type of a let-bound thing
459   | SimplRuleLhs        -- Inferring type of a RULE lhs
460   | SimplInteractive    -- Inferring type at GHCi prompt
461   | SimplCheck          -- Checking a type signature or RULE rhs
462
463 instance Outputable SimplContext where
464   ppr SimplInfer       = ptext (sLit "SimplInfer")
465   ppr SimplRuleLhs     = ptext (sLit "SimplRuleLhs")
466   ppr SimplInteractive = ptext (sLit "SimplInteractive")
467   ppr SimplCheck       = ptext (sLit "SimplCheck")
468
469 isInteractive :: SimplContext -> Bool
470 isInteractive SimplInteractive = True
471 isInteractive _                = False
472
473 simplEqsOnly :: SimplContext -> Bool
474 -- Simplify equalities only, not dictionaries
475 -- This is used for the LHS of rules; ee
476 -- Note [Simplifying RULE lhs constraints] in TcSimplify
477 simplEqsOnly SimplRuleLhs = True
478 simplEqsOnly _            = False
479
480 performDefaulting :: SimplContext -> Bool
481 performDefaulting SimplInfer       = False
482 performDefaulting SimplRuleLhs     = False
483 performDefaulting SimplInteractive = True
484 performDefaulting SimplCheck       = True
485
486 ---------------
487 newtype TcS a = TcS { unTcS :: TcSEnv -> TcM a } 
488
489 instance Functor TcS where
490   fmap f m = TcS $ fmap f . unTcS m
491
492 instance Monad TcS where 
493   return x  = TcS (\_ -> return x) 
494   fail err  = TcS (\_ -> fail err) 
495   m >>= k   = TcS (\ebs -> unTcS m ebs >>= \r -> unTcS (k r) ebs)
496
497 -- Basic functionality 
498 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
499 wrapTcS :: TcM a -> TcS a 
500 -- Do not export wrapTcS, because it promotes an arbitrary TcM to TcS,
501 -- and TcS is supposed to have limited functionality
502 wrapTcS = TcS . const -- a TcM action will not use the TcEvBinds
503
504 wrapErrTcS :: TcM a -> TcS a 
505 -- The thing wrapped should just fail
506 -- There's no static check; it's up to the user
507 -- Having a variant for each error message is too painful
508 wrapErrTcS = wrapTcS
509
510 wrapWarnTcS :: TcM a -> TcS a 
511 -- The thing wrapped should just add a warning, or no-op
512 -- There's no static check; it's up to the user
513 wrapWarnTcS = wrapTcS
514
515 failTcS, panicTcS :: SDoc -> TcS a
516 failTcS      = wrapTcS . TcM.failWith
517 panicTcS doc = pprPanic "TcCanonical" doc
518
519 traceTcS :: String -> SDoc -> TcS ()
520 traceTcS herald doc = TcS $ \_env -> TcM.traceTc herald doc
521
522 traceTcS0 :: String -> SDoc -> TcS ()
523 traceTcS0 herald doc = TcS $ \_env -> TcM.traceTcN 0 herald doc
524
525 runTcS :: SimplContext
526        -> Untouchables         -- Untouchables
527        -> TcS a                -- What to run
528        -> TcM (a, Bag FrozenError, Bag EvBind)
529 runTcS context untouch tcs 
530   = do { ty_binds_var <- TcM.newTcRef emptyVarEnv
531        ; ev_binds_var@(EvBindsVar evb_ref _) <- TcM.newTcEvBinds
532        ; err_ref <- TcM.newTcRef emptyBag
533        ; let env = TcSEnv { tcs_ev_binds = ev_binds_var
534                           , tcs_ty_binds = ty_binds_var
535                           , tcs_context  = context
536                           , tcs_untch    = (untouch, emptyVarSet) -- No Tcs untouchables yet
537                           , tcs_errors   = err_ref
538                           }
539
540              -- Run the computation
541        ; res <- unTcS tcs env
542              -- Perform the type unifications required
543        ; ty_binds <- TcM.readTcRef ty_binds_var
544        ; mapM_ do_unification (varEnvElts ty_binds)
545
546              -- And return
547        ; frozen_errors <- TcM.readTcRef err_ref
548        ; ev_binds      <- TcM.readTcRef evb_ref
549        ; return (res, frozen_errors, evBindMapBinds ev_binds) }
550   where
551     do_unification (tv,ty) = TcM.writeMetaTyVar tv ty
552
553 nestImplicTcS :: EvBindsVar -> TcsUntouchables -> TcS a -> TcS a
554 nestImplicTcS ref untch (TcS thing_inside)
555   = TcS $ \ TcSEnv { tcs_ty_binds = ty_binds, 
556                      tcs_context = ctxt, 
557                      tcs_errors = err_ref } ->
558     let 
559        nest_env = TcSEnv { tcs_ev_binds = ref
560                          , tcs_ty_binds = ty_binds
561                          , tcs_untch    = untch
562                          , tcs_context  = ctxtUnderImplic ctxt 
563                          , tcs_errors   = err_ref }
564     in 
565     thing_inside nest_env
566
567 recoverTcS :: TcS a -> TcS a -> TcS a
568 recoverTcS (TcS recovery_code) (TcS thing_inside)
569   = TcS $ \ env ->
570     TcM.recoverM (recovery_code env) (thing_inside env)
571
572 ctxtUnderImplic :: SimplContext -> SimplContext
573 -- See Note [Simplifying RULE lhs constraints] in TcSimplify
574 ctxtUnderImplic SimplRuleLhs = SimplCheck
575 ctxtUnderImplic ctxt         = ctxt
576
577 tryTcS :: TcS a -> TcS a
578 -- Like runTcS, but from within the TcS monad 
579 -- Ignore all the evidence generated, and do not affect caller's evidence!
580 tryTcS tcs 
581   = TcS (\env -> do { ty_binds_var <- TcM.newTcRef emptyVarEnv
582                     ; ev_binds_var <- TcM.newTcEvBinds
583                     ; err_ref      <- TcM.newTcRef emptyBag
584                     ; let env1 = env { tcs_ev_binds = ev_binds_var
585                                      , tcs_ty_binds = ty_binds_var 
586                                      , tcs_errors   = err_ref }
587                     ; unTcS tcs env1 })
588
589 -- Update TcEvBinds 
590 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
591
592 getDynFlags :: TcS DynFlags
593 getDynFlags = wrapTcS TcM.getDOpts
594
595 getTcSContext :: TcS SimplContext
596 getTcSContext = TcS (return . tcs_context)
597
598 getTcEvBinds :: TcS EvBindsVar
599 getTcEvBinds = TcS (return . tcs_ev_binds) 
600
601 getUntouchables :: TcS TcsUntouchables
602 getUntouchables = TcS (return . tcs_untch)
603
604 getTcSTyBinds :: TcS (IORef (TyVarEnv (TcTyVar, TcType)))
605 getTcSTyBinds = TcS (return . tcs_ty_binds)
606
607 getTcSErrors :: TcS (IORef (Bag FrozenError))
608 getTcSErrors = TcS (return . tcs_errors)
609
610 getTcSErrorsBag :: TcS (Bag FrozenError) 
611 getTcSErrorsBag = do { err_ref <- getTcSErrors 
612                      ; wrapTcS $ TcM.readTcRef err_ref }
613
614 getTcSTyBindsMap :: TcS (TyVarEnv (TcTyVar, TcType)) 
615 getTcSTyBindsMap = getTcSTyBinds >>= wrapTcS . (TcM.readTcRef) 
616
617
618 getTcEvBindsBag :: TcS EvBindMap
619 getTcEvBindsBag
620   = do { EvBindsVar ev_ref _ <- getTcEvBinds 
621        ; wrapTcS $ TcM.readTcRef ev_ref }
622
623 setWantedCoBind :: CoVar -> Coercion -> TcS () 
624 setWantedCoBind cv co 
625   = setEvBind cv (EvCoercion co)
626      -- Was: wrapTcS $ TcM.writeWantedCoVar cv co 
627
628 setDerivedCoBind :: CoVar -> Coercion -> TcS () 
629 setDerivedCoBind cv co 
630   = setEvBind cv (EvCoercion co)
631
632 setWantedTyBind :: TcTyVar -> TcType -> TcS () 
633 -- Add a type binding
634 -- We never do this twice!
635 setWantedTyBind tv ty 
636   = do { ref <- getTcSTyBinds
637        ; wrapTcS $ 
638          do { ty_binds <- TcM.readTcRef ref
639 #ifdef DEBUG
640             ; TcM.checkErr (not (tv `elemVarEnv` ty_binds)) $
641               vcat [ text "TERRIBLE ERROR: double set of meta type variable"
642                    , ppr tv <+> text ":=" <+> ppr ty
643                    , text "Old value =" <+> ppr (lookupVarEnv_NF ty_binds tv)]
644 #endif
645             ; TcM.writeTcRef ref (extendVarEnv ty_binds tv (tv,ty)) } }
646
647 setIPBind :: EvVar -> EvTerm -> TcS () 
648 setIPBind = setEvBind 
649
650 setDictBind :: EvVar -> EvTerm -> TcS () 
651 setDictBind = setEvBind 
652
653 setEvBind :: EvVar -> EvTerm -> TcS () 
654 -- Internal
655 setEvBind ev rhs 
656   = do { tc_evbinds <- getTcEvBinds 
657        ; wrapTcS (TcM.addTcEvBind tc_evbinds ev rhs) }
658
659 newTcEvBindsTcS :: TcS EvBindsVar
660 newTcEvBindsTcS = wrapTcS (TcM.newTcEvBinds)
661
662 warnTcS :: CtLoc orig -> Bool -> SDoc -> TcS ()
663 warnTcS loc warn_if doc 
664   | warn_if   = wrapTcS $ TcM.setCtLoc loc $ TcM.addWarnTc doc
665   | otherwise = return ()
666
667 getDefaultInfo ::  TcS (SimplContext, [Type], (Bool, Bool))
668 getDefaultInfo 
669   = do { ctxt <- getTcSContext
670        ; (tys, flags) <- wrapTcS (TcM.tcGetDefaultTys (isInteractive ctxt))
671        ; return (ctxt, tys, flags) }
672
673
674
675 -- Recording errors in the TcS monad
676 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
677
678 addErrorTcS :: ErrorKind -> CtFlavor -> TcType -> TcType -> TcS ()
679 addErrorTcS frknd fl ty1 ty2
680   = do { err_ref <- getTcSErrors
681        ; wrapTcS $ do
682        { TcM.updTcRef err_ref $ \ errs ->
683            consBag (FrozenError frknd fl ty1 ty2) errs
684
685            -- If there's an error in the *given* constraints,
686            -- stop right now, to avoid a cascade of errors
687            -- in the wanteds
688        ; when (isGiven fl) TcM.failM
689
690        ; return () } }
691
692 -- Just get some environments needed for instance looking up and matching
693 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
694
695 getInstEnvs :: TcS (InstEnv, InstEnv) 
696 getInstEnvs = wrapTcS $ Inst.tcGetInstEnvs 
697
698 getFamInstEnvs :: TcS (FamInstEnv, FamInstEnv) 
699 getFamInstEnvs = wrapTcS $ FamInst.tcGetFamInstEnvs
700
701 getTopEnv :: TcS HscEnv 
702 getTopEnv = wrapTcS $ TcM.getTopEnv 
703
704 getGblEnv :: TcS TcGblEnv 
705 getGblEnv = wrapTcS $ TcM.getGblEnv 
706
707 -- Various smaller utilities [TODO, maybe will be absorbed in the instance matcher]
708 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
709
710 checkWellStagedDFun :: PredType -> DFunId -> WantedLoc -> TcS () 
711 checkWellStagedDFun pred dfun_id loc 
712   = wrapTcS $ TcM.setCtLoc loc $ 
713     do { use_stage <- TcM.getStage
714        ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
715   where
716     pp_thing = ptext (sLit "instance for") <+> quotes (ppr pred)
717     bind_lvl = TcM.topIdLvl dfun_id
718
719 pprEq :: TcType -> TcType -> SDoc
720 pprEq ty1 ty2 = pprPred $ mkEqPred (ty1,ty2)
721
722 isTouchableMetaTyVar :: TcTyVar -> TcS Bool
723 isTouchableMetaTyVar tv 
724   = do { untch <- getUntouchables
725        ; return $ isTouchableMetaTyVar_InRange untch tv } 
726
727 isTouchableMetaTyVar_InRange :: TcsUntouchables -> TcTyVar -> Bool 
728 isTouchableMetaTyVar_InRange (untch,untch_tcs) tv 
729   = case tcTyVarDetails tv of 
730       MetaTv TcsTv _ -> not (tv `elemVarSet` untch_tcs)
731                         -- See Note [Touchable meta type variables] 
732       MetaTv {}      -> inTouchableRange untch tv 
733       _              -> False 
734
735
736 \end{code}
737
738
739 Note [Touchable meta type variables]
740 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
741 Meta type variables allocated *by the constraint solver itself* are always
742 touchable.  Example: 
743    instance C a b => D [a] where...
744 if we use this instance declaration we "make up" a fresh meta type
745 variable for 'b', which we must later guess.  (Perhaps C has a
746 functional dependency.)  But since we aren't in the constraint *generator*
747 we can't allocate a Unique in the touchable range for this implication
748 constraint.  Instead, we mark it as a "TcsTv", which makes it always-touchable.
749
750
751 \begin{code}
752 -- Flatten skolems
753 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
754
755 newFlattenSkolemTy :: TcType -> TcS TcType
756 newFlattenSkolemTy ty = mkTyVarTy <$> newFlattenSkolemTyVar ty
757
758 newFlattenSkolemTyVar :: TcType -> TcS TcTyVar
759 newFlattenSkolemTyVar ty
760   = do { tv <- wrapTcS $ do { uniq <- TcM.newUnique
761                             ; let name = mkSysTvName uniq (fsLit "f")
762                             ; return $ mkTcTyVar name (typeKind ty) (FlatSkol ty) } 
763        ; traceTcS "New Flatten Skolem Born" $ 
764            (ppr tv <+> text "[:= " <+> ppr ty <+> text "]")
765        ; return tv }
766
767 -- Instantiations 
768 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
769
770 instDFunTypes :: [Either TyVar TcType] -> TcS [TcType] 
771 instDFunTypes mb_inst_tys 
772   = mapM inst_tv mb_inst_tys
773   where
774     inst_tv :: Either TyVar TcType -> TcS Type
775     inst_tv (Left tv)  = mkTyVarTy <$> instFlexiTcS tv
776     inst_tv (Right ty) = return ty 
777
778 instDFunConstraints :: TcThetaType -> TcS [EvVar] 
779 instDFunConstraints preds = wrapTcS $ TcM.newWantedEvVars preds 
780
781
782 instFlexiTcS :: TyVar -> TcS TcTyVar 
783 -- Like TcM.instMetaTyVar but the variable that is created is always
784 -- touchable; we are supposed to guess its instantiation. 
785 -- See Note [Touchable meta type variables] 
786 instFlexiTcS tv = instFlexiTcSHelper (tyVarName tv) (tyVarKind tv) 
787
788 newFlexiTcSTy :: Kind -> TcS TcType  
789 newFlexiTcSTy knd 
790   = wrapTcS $
791     do { uniq <- TcM.newUnique 
792        ; ref  <- TcM.newMutVar  Flexi 
793        ; let name = mkSysTvName uniq (fsLit "uf")
794        ; return $ mkTyVarTy (mkTcTyVar name knd (MetaTv TcsTv ref)) }
795
796 isFlexiTcsTv :: TyVar -> Bool
797 isFlexiTcsTv tv
798   | not (isTcTyVar tv)                  = False
799   | MetaTv TcsTv _ <- tcTyVarDetails tv = True
800   | otherwise                           = False
801
802 newKindConstraint :: TcTyVar -> Kind -> TcS CoVar
803 -- Create new wanted CoVar that constrains the type to have the specified kind. 
804 newKindConstraint tv knd 
805   = do { tv_k <- instFlexiTcSHelper (tyVarName tv) knd 
806        ; let ty_k = mkTyVarTy tv_k
807        ; co_var <- newWantedCoVar (mkTyVarTy tv) ty_k
808        ; return co_var }
809
810 instFlexiTcSHelper :: Name -> Kind -> TcS TcTyVar
811 instFlexiTcSHelper tvname tvkind
812   = wrapTcS $ 
813     do { uniq <- TcM.newUnique 
814        ; ref  <- TcM.newMutVar  Flexi 
815        ; let name = setNameUnique tvname uniq 
816              kind = tvkind 
817        ; return (mkTcTyVar name kind (MetaTv TcsTv ref)) }
818
819 -- Superclasses and recursive dictionaries 
820 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
821
822 newGivOrDerEvVar :: TcPredType -> EvTerm -> TcS EvVar 
823 newGivOrDerEvVar pty evtrm 
824   = do { ev <- wrapTcS $ TcM.newEvVar pty 
825        ; setEvBind ev evtrm 
826        ; return ev }
827
828 newGivOrDerCoVar :: TcType -> TcType -> Coercion -> TcS EvVar 
829 -- Note we create immutable variables for given or derived, since we
830 -- must bind them to TcEvBinds (because their evidence may involve 
831 -- superclasses). However we should be able to override existing
832 -- 'derived' evidence, even in TcEvBinds 
833 newGivOrDerCoVar ty1 ty2 co 
834   = do { cv <- newCoVar ty1 ty2
835        ; setEvBind cv (EvCoercion co) 
836        ; return cv } 
837
838 newWantedCoVar :: TcType -> TcType -> TcS EvVar 
839 newWantedCoVar ty1 ty2 =  wrapTcS $ TcM.newWantedCoVar ty1 ty2 
840
841
842 newCoVar :: TcType -> TcType -> TcS EvVar 
843 newCoVar ty1 ty2 = wrapTcS $ TcM.newCoVar ty1 ty2 
844
845 newIPVar :: IPName Name -> TcType -> TcS EvVar 
846 newIPVar nm ty = wrapTcS $ TcM.newIP nm ty 
847
848 newDictVar :: Class -> [TcType] -> TcS EvVar 
849 newDictVar cl tys = wrapTcS $ TcM.newDict cl tys 
850 \end{code} 
851
852
853 \begin{code} 
854 isGoodRecEv :: EvVar -> EvVar -> TcS Bool
855 -- In a call (isGoodRecEv ev wv), we are considering solving wv 
856 -- using some term that involves ev, such as:
857 -- by setting           wv = ev
858 -- or                   wv = EvCast x |> ev
859 -- etc. 
860 -- But that would be Very Bad if the evidence for 'ev' mentions 'wv',
861 -- in an "unguarded" way. So isGoodRecEv looks at the evidence ev 
862 -- recursively through the evidence binds, to see if uses of 'wv' are guarded.
863 --
864 -- Guarded means: more instance calls than superclass selections. We
865 -- compute this by chasing the evidence, adding +1 for every instance
866 -- call (constructor) and -1 for every superclass selection (destructor).
867 --
868 -- See Note [Superclasses and recursive dictionaries] in TcInteract
869 isGoodRecEv ev_var wv
870   = do { tc_evbinds <- getTcEvBindsBag 
871        ; mb <- chase_ev_var tc_evbinds wv 0 [] ev_var 
872        ; return $ case mb of 
873                     Nothing -> True 
874                     Just min_guardedness -> min_guardedness > 0
875        }
876
877   where chase_ev_var :: EvBindMap   -- Evidence binds 
878                  -> EvVar           -- Target variable whose gravity we want to return
879                  -> Int             -- Current gravity 
880                  -> [EvVar]         -- Visited nodes
881                  -> EvVar           -- Current node 
882                  -> TcS (Maybe Int)
883         chase_ev_var assocs trg curr_grav visited orig
884             | trg == orig         = return $ Just curr_grav
885             | orig `elem` visited = return $ Nothing 
886             | Just (EvBind _ ev_trm) <- lookupEvBind assocs orig
887             = chase_ev assocs trg curr_grav (orig:visited) ev_trm
888
889             | otherwise = return Nothing
890
891         chase_ev assocs trg curr_grav visited (EvId v) 
892             = chase_ev_var assocs trg curr_grav visited v
893         chase_ev assocs trg curr_grav visited (EvSuperClass d_id _) 
894             = chase_ev_var assocs trg (curr_grav-1) visited d_id
895         chase_ev assocs trg curr_grav visited (EvCast v co)
896             = do { m1 <- chase_ev_var assocs trg curr_grav visited v
897                  ; m2 <- chase_co assocs trg curr_grav visited co
898                  ; return (comb_chase_res Nothing [m1,m2]) } 
899
900         chase_ev assocs trg curr_grav visited (EvCoercion co)
901             = chase_co assocs trg curr_grav visited co
902         chase_ev assocs trg curr_grav visited (EvDFunApp _ _ _ev_vars ev_deps)
903             = do { chase_results <- mapM (chase_ev_var assocs trg (curr_grav+1) visited) ev_deps
904                                     -- Notice that we chase the ev_deps and not the ev_vars
905                                     -- See Note [Dependencies in self dictionaries] in TcSimplify
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}