Document SCC determinism
[ghc.git] / compiler / typecheck / TcEvidence.hs
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE CPP, DeriveDataTypeable #-}
4
5 module TcEvidence (
6
7 -- HsWrapper
8 HsWrapper(..),
9 (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
10 mkWpLams, mkWpLet, mkWpCastN, mkWpCastR,
11 mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,
12
13 -- Evidence bindings
14 TcEvBinds(..), EvBindsVar(..),
15 EvBindMap(..), emptyEvBindMap, extendEvBinds,
16 lookupEvBind, evBindMapBinds, foldEvBindMap,
17 EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
18 sccEvBinds, evBindVar,
19 EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
20 EvLit(..), evTermCoercion,
21 EvCallStack(..),
22 EvTypeable(..),
23
24 -- TcCoercion
25 TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
26 Role(..), LeftOrRight(..), pickLR,
27 mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
28 mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
29 mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
30 mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
31 tcDowngradeRole,
32 mkTcAxiomRuleCo, mkTcCoherenceLeftCo, mkTcCoherenceRightCo, mkTcPhantomCo,
33 mkTcKindCo,
34 tcCoercionKind, coVarsOfTcCo,
35 mkTcCoVarCo,
36 isTcReflCo,
37 tcCoercionRole,
38 unwrapIP, wrapIP
39 ) where
40 #include "HsVersions.h"
41
42 import Var
43 import CoAxiom
44 import Coercion
45 import PprCore () -- Instance OutputableBndr TyVar
46 import TcType
47 import Type
48 import TyCon
49 import Class( Class )
50 import PrelNames
51 import DynFlags ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
52 import VarEnv
53 import VarSet
54 import Name
55 import Pair
56
57 import Util
58 import Bag
59 import Digraph
60 import qualified Data.Data as Data
61 import Outputable
62 import FastString
63 import SrcLoc
64 import Data.IORef( IORef )
65 import UniqFM
66
67 {-
68 Note [TcCoercions]
69 ~~~~~~~~~~~~~~~~~~
70 | TcCoercions are a hack used by the typechecker. Normally,
71 Coercions have free variables of type (a ~# b): we call these
72 CoVars. However, the type checker passes around equality evidence
73 (boxed up) at type (a ~ b).
74
75 An TcCoercion is simply a Coercion whose free variables have may be either
76 boxed or unboxed. After we are done with typechecking the desugarer finds the
77 boxed free variables, unboxes them, and creates a resulting real Coercion with
78 kosher free variables.
79
80 -}
81
82 type TcCoercion = Coercion
83 type TcCoercionN = CoercionN -- A Nominal corecion ~N
84 type TcCoercionR = CoercionR -- A Representational corecion ~R
85 type TcCoercionP = CoercionP -- a phantom coercion
86
87 mkTcReflCo :: Role -> TcType -> TcCoercion
88 mkTcSymCo :: TcCoercion -> TcCoercion
89 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
90 mkTcNomReflCo :: TcType -> TcCoercionN
91 mkTcRepReflCo :: TcType -> TcCoercionR
92 mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
93 mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion
94 mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
95 mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex
96 -> [TcType] -> [TcCoercion] -> TcCoercion
97 mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
98 -> [TcCoercion] -> TcCoercionR
99 mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
100 mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
101 mkTcNthCo :: Int -> TcCoercion -> TcCoercion
102 mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
103 mkTcSubCo :: TcCoercionN -> TcCoercionR
104 maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
105 tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
106 mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
107 mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion
108 mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion
109 mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP
110 mkTcKindCo :: TcCoercion -> TcCoercionN
111 mkTcCoVarCo :: CoVar -> TcCoercion
112
113 tcCoercionKind :: TcCoercion -> Pair TcType
114 tcCoercionRole :: TcCoercion -> Role
115 coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet
116 isTcReflCo :: TcCoercion -> Bool
117
118 mkTcReflCo = mkReflCo
119 mkTcSymCo = mkSymCo
120 mkTcTransCo = mkTransCo
121 mkTcNomReflCo = mkNomReflCo
122 mkTcRepReflCo = mkRepReflCo
123 mkTcTyConAppCo = mkTyConAppCo
124 mkTcAppCo = mkAppCo
125 mkTcFunCo = mkFunCo
126 mkTcAxInstCo = mkAxInstCo
127 mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational
128 mkTcForAllCo = mkForAllCo
129 mkTcForAllCos = mkForAllCos
130 mkTcNthCo = mkNthCo
131 mkTcLRCo = mkLRCo
132 mkTcSubCo = mkSubCo
133 maybeTcSubCo = maybeSubCo
134 tcDowngradeRole = downgradeRole
135 mkTcAxiomRuleCo = mkAxiomRuleCo
136 mkTcCoherenceLeftCo = mkCoherenceLeftCo
137 mkTcCoherenceRightCo = mkCoherenceRightCo
138 mkTcPhantomCo = mkPhantomCo
139 mkTcKindCo = mkKindCo
140 mkTcCoVarCo = mkCoVarCo
141
142 tcCoercionKind = coercionKind
143 tcCoercionRole = coercionRole
144 coVarsOfTcCo = coVarsOfCo
145 isTcReflCo = isReflCo
146
147
148 {-
149 %************************************************************************
150 %* *
151 HsWrapper
152 * *
153 ************************************************************************
154 -}
155
156 data HsWrapper
157 = WpHole -- The identity coercion
158
159 | WpCompose HsWrapper HsWrapper
160 -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
161 --
162 -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
163 -- But ([] a) `WpCompose` ([] b) = ([] b a)
164
165 | WpFun HsWrapper HsWrapper TcType
166 -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ]
167 -- So note that if wrap1 :: exp_arg <= act_arg
168 -- wrap2 :: act_res <= exp_res
169 -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
170 -- This isn't the same as for mkFunCo, but it has to be this way
171 -- because we can't use 'sym' to flip around these HsWrappers
172 -- The TcType is the "from" type of the first wrapper
173
174 | WpCast TcCoercionR -- A cast: [] `cast` co
175 -- Guaranteed not the identity coercion
176 -- At role Representational
177
178 -- Evidence abstraction and application
179 -- (both dictionaries and coercions)
180 | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable
181 | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint
182 -- Kind and Type abstraction and application
183 | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var)
184 | WpTyApp KindOrType -- [] t the 't' is a type (not coercion)
185
186
187 | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings,
188 -- so that the identity coercion is always exactly WpHole
189 deriving (Data.Data, Data.Typeable)
190
191
192 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
193 WpHole <.> c = c
194 c <.> WpHole = c
195 c1 <.> c2 = c1 `WpCompose` c2
196
197 mkWpFun :: HsWrapper -> HsWrapper
198 -> TcType -- the "from" type of the first wrapper
199 -> TcType -- either type of the second wrapper (used only when the
200 -- second wrapper is the identity)
201 -> HsWrapper
202 mkWpFun WpHole WpHole _ _ = WpHole
203 mkWpFun WpHole (WpCast co2) t1 _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
204 mkWpFun (WpCast co1) WpHole _ t2 = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
205 mkWpFun (WpCast co1) (WpCast co2) _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
206 mkWpFun co1 co2 t1 _ = WpFun co1 co2 t1
207
208 -- | @mkWpFuns [(ty1, wrap1), (ty2, wrap2)] ty_res wrap_res@,
209 -- where @wrap1 :: ty1 "->" ty1'@ and @wrap2 :: ty2 "->" ty2'@,
210 -- @wrap3 :: ty3 "->" ty3'@ and @ty_res@ is /either/ @ty3@ or @ty3'@,
211 -- gives a wrapper @(ty1' -> ty2' -> ty3) "->" (ty1 -> ty2 -> ty3')@.
212 -- Notice that the result wrapper goes the other way round to all
213 -- the others. This is a result of sub-typing contravariance.
214 mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> HsWrapper
215 mkWpFuns args res_ty res_wrap = snd $ go args res_ty res_wrap
216 where
217 go [] res_ty res_wrap = (res_ty, res_wrap)
218 go ((arg_ty, arg_wrap) : args) res_ty res_wrap
219 = let (tail_ty, tail_wrap) = go args res_ty res_wrap in
220 (arg_ty `mkFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty)
221
222 mkWpCastR :: TcCoercionR -> HsWrapper
223 mkWpCastR co
224 | isTcReflCo co = WpHole
225 | otherwise = ASSERT2(tcCoercionRole co == Representational, ppr co)
226 WpCast co
227
228 mkWpCastN :: TcCoercionN -> HsWrapper
229 mkWpCastN co
230 | isTcReflCo co = WpHole
231 | otherwise = ASSERT2(tcCoercionRole co == Nominal, ppr co)
232 WpCast (mkTcSubCo co)
233 -- The mkTcSubCo converts Nominal to Representational
234
235 mkWpTyApps :: [Type] -> HsWrapper
236 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
237
238 mkWpEvApps :: [EvTerm] -> HsWrapper
239 mkWpEvApps args = mk_co_app_fn WpEvApp args
240
241 mkWpEvVarApps :: [EvVar] -> HsWrapper
242 mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map EvId vs)
243
244 mkWpTyLams :: [TyVar] -> HsWrapper
245 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
246
247 mkWpLams :: [Var] -> HsWrapper
248 mkWpLams ids = mk_co_lam_fn WpEvLam ids
249
250 mkWpLet :: TcEvBinds -> HsWrapper
251 -- This no-op is a quite a common case
252 mkWpLet (EvBinds b) | isEmptyBag b = WpHole
253 mkWpLet ev_binds = WpLet ev_binds
254
255 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
256 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
257
258 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
259 -- For applications, the *first* argument must
260 -- come *last* in the composition sequence
261 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
262
263 idHsWrapper :: HsWrapper
264 idHsWrapper = WpHole
265
266 isIdHsWrapper :: HsWrapper -> Bool
267 isIdHsWrapper WpHole = True
268 isIdHsWrapper _ = False
269
270 {-
271 ************************************************************************
272 * *
273 Evidence bindings
274 * *
275 ************************************************************************
276 -}
277
278 data TcEvBinds
279 = TcEvBinds -- Mutable evidence bindings
280 EvBindsVar -- Mutable because they are updated "later"
281 -- when an implication constraint is solved
282
283 | EvBinds -- Immutable after zonking
284 (Bag EvBind)
285
286 deriving( Data.Typeable )
287
288 data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
289 -- The Unique is for debug printing only
290
291 instance Data.Data TcEvBinds where
292 -- Placeholder; we can't travers into TcEvBinds
293 toConstr _ = abstractConstr "TcEvBinds"
294 gunfold _ _ = error "gunfold"
295 dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
296
297 -----------------
298 newtype EvBindMap
299 = EvBindMap {
300 ev_bind_varenv :: DVarEnv EvBind
301 } -- Map from evidence variables to evidence terms
302 -- We use @DVarEnv@ here to get deterministic ordering when we
303 -- turn it into a Bag.
304 -- If we don't do that, when we generate let bindings for
305 -- dictionaries in dsTcEvBinds they will be generated in random
306 -- order.
307 --
308 -- For example:
309 --
310 -- let $dEq = GHC.Classes.$fEqInt in
311 -- let $$dNum = GHC.Num.$fNumInt in ...
312 --
313 -- vs
314 --
315 -- let $dNum = GHC.Num.$fNumInt in
316 -- let $dEq = GHC.Classes.$fEqInt in ...
317 --
318 -- See Note [Deterministic UniqFM] in UniqDFM for explanation why
319 -- @UniqFM@ can lead to nondeterministic order.
320
321 emptyEvBindMap :: EvBindMap
322 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
323
324 extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
325 extendEvBinds bs ev_bind
326 = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
327 (eb_lhs ev_bind)
328 ev_bind }
329
330 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
331 lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
332
333 evBindMapBinds :: EvBindMap -> Bag EvBind
334 evBindMapBinds = foldEvBindMap consBag emptyBag
335
336 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
337 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
338
339 -----------------
340 -- All evidence is bound by EvBinds; no side effects
341 data EvBind
342 = EvBind { eb_lhs :: EvVar
343 , eb_rhs :: EvTerm
344 , eb_is_given :: Bool -- True <=> given
345 -- See Note [Tracking redundant constraints] in TcSimplify
346 }
347
348 evBindVar :: EvBind -> EvVar
349 evBindVar = eb_lhs
350
351 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
352 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
353
354
355 mkGivenEvBind :: EvVar -> EvTerm -> EvBind
356 mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
357
358 data EvTerm
359 = EvId EvId -- Any sort of evidence Id, including coercions
360
361 | EvCoercion TcCoercion -- coercion bindings
362 -- See Note [Coercion evidence terms]
363
364 | EvCast EvTerm TcCoercionR -- d |> co
365
366 | EvDFunApp DFunId -- Dictionary instance application
367 [Type] [EvTerm]
368
369 | EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
370 -- See Note [Deferring coercion errors to runtime]
371 -- in TcSimplify
372
373 | EvSuperClass EvTerm Int -- n'th superclass. Used for both equalities and
374 -- dictionaries, even though the former have no
375 -- selector Id. We count up from _0_
376
377 | EvLit EvLit -- Dictionary for KnownNat and KnownSymbol classes.
378 -- Note [KnownNat & KnownSymbol and EvLit]
379
380 | EvCallStack EvCallStack -- Dictionary for CallStack implicit parameters
381
382 | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
383
384 deriving( Data.Data, Data.Typeable )
385
386
387 -- | Instructions on how to make a 'Typeable' dictionary.
388 -- See Note [Typeable evidence terms]
389 data EvTypeable
390 = EvTypeableTyCon [EvTerm] -- ^ Dictionary for @Typeable (T k1..kn)@.
391 -- The EvTerms are for the arguments
392
393 | EvTypeableTyApp EvTerm EvTerm
394 -- ^ Dictionary for @Typeable (s t)@,
395 -- given a dictionaries for @s@ and @t@
396
397 | EvTypeableTyLit EvTerm
398 -- ^ Dictionary for a type literal,
399 -- e.g. @Typeable "foo"@ or @Typeable 3@
400 -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
401 -- (see Trac #10348)
402
403 deriving ( Data.Data, Data.Typeable )
404
405 data EvLit
406 = EvNum Integer
407 | EvStr FastString
408 deriving( Data.Data, Data.Typeable )
409
410 -- | Evidence for @CallStack@ implicit parameters.
411 data EvCallStack
412 -- See Note [Overview of implicit CallStacks]
413 = EvCsEmpty
414 | EvCsPushCall Name RealSrcSpan EvTerm
415 -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
416 -- @loc@, in a calling context @stk@.
417 deriving( Data.Data, Data.Typeable )
418
419 {-
420 Note [Typeable evidence terms]
421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
422 The EvTypeable data type looks isomorphic to Type, but the EvTerms
423 inside can be EvIds. Eg
424 f :: forall a. Typeable a => a -> TypeRep
425 f x = typeRep (undefined :: Proxy [a])
426 Here for the (Typeable [a]) dictionary passed to typeRep we make
427 evidence
428 dl :: Typeable [a] = EvTypeable [a]
429 (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
430 where
431 d :: Typable a
432 is the lambda-bound dictionary passed into f.
433
434 Note [Coercion evidence terms]
435 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
436 A "coercion evidence term" takes one of these forms
437 co_tm ::= EvId v where v :: t1 ~# t2
438 | EvCoercion co
439 | EvCast co_tm co
440
441 We do quite often need to get a TcCoercion from an EvTerm; see
442 'evTermCoercion'.
443
444 INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
445 a coercion evidence term. Consider for example
446 [G] d :: F Int a
447 If we have
448 ax7 a :: F Int a ~ (a ~ Bool)
449 then we do NOT generate the constraint
450 [G] (d |> ax7 a) :: a ~ Bool
451 because that does not satisfy the invariant (d is not a coercion variable).
452 Instead we make a binding
453 g1 :: a~Bool = g |> ax7 a
454 and the constraint
455 [G] g1 :: a~Bool
456 See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
457
458 Note [EvBinds/EvTerm]
459 ~~~~~~~~~~~~~~~~~~~~~
460 How evidence is created and updated. Bindings for dictionaries,
461 and coercions and implicit parameters are carried around in TcEvBinds
462 which during constraint generation and simplification is always of the
463 form (TcEvBinds ref). After constraint simplification is finished it
464 will be transformed to t an (EvBinds ev_bag).
465
466 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
467 However, all EvVars that correspond to *wanted* coercion terms in
468 an EvBind must be mutable variables so that they can be readily
469 inlined (by zonking) after constraint simplification is finished.
470
471 Conclusion: a new wanted coercion variable should be made mutable.
472 [Notice though that evidence variables that bind coercion terms
473 from super classes will be "given" and hence rigid]
474
475
476 Note [KnownNat & KnownSymbol and EvLit]
477 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
478 A part of the type-level literals implementation are the classes
479 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
480 defining singleton values. Here is the key stuff from GHC.TypeLits
481
482 class KnownNat (n :: Nat) where
483 natSing :: SNat n
484
485 newtype SNat (n :: Nat) = SNat Integer
486
487 Conceptually, this class has infinitely many instances:
488
489 instance KnownNat 0 where natSing = SNat 0
490 instance KnownNat 1 where natSing = SNat 1
491 instance KnownNat 2 where natSing = SNat 2
492 ...
493
494 In practice, we solve `KnownNat` predicates in the type-checker
495 (see typecheck/TcInteract.hs) because we can't have infinately many instances.
496 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
497
498 We make the following assumptions about dictionaries in GHC:
499 1. The "dictionary" for classes with a single method---like `KnownNat`---is
500 a newtype for the type of the method, so using a evidence amounts
501 to a coercion, and
502 2. Newtypes use the same representation as their definition types.
503
504 So, the evidence for `KnownNat` is just a value of the representation type,
505 wrapped in two newtype constructors: one to make it into a `SNat` value,
506 and another to make it into a `KnownNat` dictionary.
507
508 Also note that `natSing` and `SNat` are never actually exposed from the
509 library---they are just an implementation detail. Instead, users see
510 a more convenient function, defined in terms of `natSing`:
511
512 natVal :: KnownNat n => proxy n -> Integer
513
514 The reason we don't use this directly in the class is that it is simpler
515 and more efficient to pass around an integer rather than an entier function,
516 especially when the `KnowNat` evidence is packaged up in an existential.
517
518 The story for kind `Symbol` is analogous:
519 * class KnownSymbol
520 * newtype SSymbol
521 * Evidence: EvLit (EvStr n)
522
523
524 Note [Overview of implicit CallStacks]
525 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
526 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
527
528 The goal of CallStack evidence terms is to reify locations
529 in the program source as runtime values, without any support
530 from the RTS. We accomplish this by assigning a special meaning
531 to constraints of type GHC.Stack.Types.HasCallStack, an alias
532
533 type HasCallStack = (?callStack :: CallStack)
534
535 Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
536 important) are solved in three steps:
537
538 1. Occurrences of CallStack IPs are solved directly from the given IP,
539 just like a regular IP. For example, the occurrence of `?stk` in
540
541 error :: (?stk :: CallStack) => String -> a
542 error s = raise (ErrorCall (s ++ prettyCallStack ?stk))
543
544 will be solved for the `?stk` in `error`s context as before.
545
546 2. In a function call, instead of simply passing the given IP, we first
547 append the current call-site to it. For example, consider a
548 call to the callstack-aware `error` above.
549
550 undefined :: (?stk :: CallStack) => a
551 undefined = error "undefined!"
552
553 Here we want to take the given `?stk` and append the current
554 call-site, before passing it to `error`. In essence, we want to
555 rewrite `error "undefined!"` to
556
557 let ?stk = pushCallStack <error's location> ?stk
558 in error "undefined!"
559
560 We achieve this effect by emitting a NEW wanted
561
562 [W] d :: IP "stk" CallStack
563
564 from which we build the evidence term
565
566 EvCsPushCall "error" <error's location> (EvId d)
567
568 that we use to solve the call to `error`. The new wanted `d` will
569 then be solved per rule (1), ie as a regular IP.
570
571 (see TcInteract.interactDict)
572
573 3. We default any insoluble CallStacks to the empty CallStack. Suppose
574 `undefined` did not request a CallStack, ie
575
576 undefinedNoStk :: a
577 undefinedNoStk = error "undefined!"
578
579 Under the usual IP rules, the new wanted from rule (2) would be
580 insoluble as there's no given IP from which to solve it, so we
581 would get an "unbound implicit parameter" error.
582
583 We don't ever want to emit an insoluble CallStack IP, so we add a
584 defaulting pass to default any remaining wanted CallStacks to the
585 empty CallStack with the evidence term
586
587 EvCsEmpty
588
589 (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks)
590
591 This provides a lightweight mechanism for building up call-stacks
592 explicitly, but is notably limited by the fact that the stack will
593 stop at the first function whose type does not include a CallStack IP.
594 For example, using the above definition of `undefined`:
595
596 head :: [a] -> a
597 head [] = undefined
598 head (x:_) = x
599
600 g = head []
601
602 the resulting CallStack will include the call to `undefined` in `head`
603 and the call to `error` in `undefined`, but *not* the call to `head`
604 in `g`, because `head` did not explicitly request a CallStack.
605
606
607 Important Details:
608 - GHC should NEVER report an insoluble CallStack constraint.
609
610 - GHC should NEVER infer a CallStack constraint unless one was requested
611 with a partial type signature (See TcType.pickQuantifiablePreds).
612
613 - A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
614 where the String is the name of the binder that is used at the
615 SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
616 package/module/file name, as well as the full source-span. Both
617 CallStack and SrcLoc are kept abstract so only GHC can construct new
618 values.
619
620 - We will automatically solve any wanted CallStack regardless of the
621 name of the IP, i.e.
622
623 f = show (?stk :: CallStack)
624 g = show (?loc :: CallStack)
625
626 are both valid. However, we will only push new SrcLocs onto existing
627 CallStacks when the IP names match, e.g. in
628
629 head :: (?loc :: CallStack) => [a] -> a
630 head [] = error (show (?stk :: CallStack))
631
632 the printed CallStack will NOT include head's call-site. This reflects the
633 standard scoping rules of implicit-parameters.
634
635 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
636 The desugarer will need to unwrap the IP newtype before pushing a new
637 call-site onto a given stack (See DsBinds.dsEvCallStack)
638
639 - When we emit a new wanted CallStack from rule (2) we set its origin to
640 `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
641 (see TcInteract.interactDict).
642
643 This is a bit shady, but is how we ensure that the new wanted is
644 solved like a regular IP.
645
646 -}
647
648 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
649 mkEvCast ev lco
650 | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
651 isTcReflCo lco = ev
652 | otherwise = EvCast ev lco
653
654 mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
655 mkEvScSelectors ev cls tys
656 = zipWith mk_pr (immSuperClasses cls tys) [0..]
657 where
658 mk_pr pred i = (pred, EvSuperClass ev i)
659
660 emptyTcEvBinds :: TcEvBinds
661 emptyTcEvBinds = EvBinds emptyBag
662
663 isEmptyTcEvBinds :: TcEvBinds -> Bool
664 isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
665 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
666
667
668 evTermCoercion :: EvTerm -> TcCoercion
669 -- Applied only to EvTerms of type (s~t)
670 -- See Note [Coercion evidence terms]
671 evTermCoercion (EvId v) = mkCoVarCo v
672 evTermCoercion (EvCoercion co) = co
673 evTermCoercion (EvCast tm co) = mkCoCast (evTermCoercion tm) co
674 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
675
676 evVarsOfTerm :: EvTerm -> VarSet
677 evVarsOfTerm (EvId v) = unitVarSet v
678 evVarsOfTerm (EvCoercion co) = coVarsOfCo co
679 evVarsOfTerm (EvDFunApp _ _ evs) = mapUnionVarSet evVarsOfTerm evs
680 evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
681 evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfCo co
682 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
683 evVarsOfTerm (EvLit _) = emptyVarSet
684 evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs
685 evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
686
687 evVarsOfTerms :: [EvTerm] -> VarSet
688 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
689
690 -- | Do SCC analysis on a bag of 'EvBind's.
691 sccEvBinds :: Bag EvBind -> [SCC EvBind]
692 sccEvBinds bs = stronglyConnCompFromEdgedVertices edges
693 where
694 edges :: [(EvBind, EvVar, [EvVar])]
695 edges = foldrBag ((:) . mk_node) [] bs
696
697 mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
698 mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
699 = (b, var, nonDetEltsUFM (evVarsOfTerm term `unionVarSet`
700 coVarsOfType (varType var)))
701 -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
702 -- is still deterministic even if the edges are in nondeterministic order
703 -- as explained in Note [Deterministic SCC] in Digraph.
704
705 evVarsOfCallStack :: EvCallStack -> VarSet
706 evVarsOfCallStack cs = case cs of
707 EvCsEmpty -> emptyVarSet
708 EvCsPushCall _ _ tm -> evVarsOfTerm tm
709
710 evVarsOfTypeable :: EvTypeable -> VarSet
711 evVarsOfTypeable ev =
712 case ev of
713 EvTypeableTyCon es -> evVarsOfTerms es
714 EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
715 EvTypeableTyLit e -> evVarsOfTerm e
716
717 {-
718 ************************************************************************
719 * *
720 Pretty printing
721 * *
722 ************************************************************************
723 -}
724
725 instance Outputable HsWrapper where
726 ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
727
728 pprHsWrapper ::HsWrapper -> (Bool -> SDoc) -> SDoc
729 -- With -fprint-typechecker-elaboration, print the wrapper
730 -- otherwise just print what's inside
731 -- The pp_thing_inside function takes Bool to say whether
732 -- it's in a position that needs parens for a non-atomic thing
733 pprHsWrapper wrap pp_thing_inside
734 = sdocWithDynFlags $ \ dflags ->
735 if gopt Opt_PrintTypecheckerElaboration dflags
736 then help pp_thing_inside wrap False
737 else pp_thing_inside False
738 where
739 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
740 -- True <=> appears in function application position
741 -- False <=> appears as body of let or lambda
742 help it WpHole = it
743 help it (WpCompose f1 f2) = help (help it f2) f1
744 help it (WpFun f1 f2 t1) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
745 help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
746 help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
747 <+> pprParendCo co)]
748 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
749 help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <+> pprParendType ty]
750 help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pp_bndr id, it False]
751 help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pp_bndr tv, it False]
752 help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
753
754 pp_bndr v = pprBndr LambdaBind v <> dot
755
756 add_parens, no_parens :: SDoc -> Bool -> SDoc
757 add_parens d True = parens d
758 add_parens d False = d
759 no_parens d _ = d
760
761 instance Outputable TcEvBinds where
762 ppr (TcEvBinds v) = ppr v
763 ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
764
765 instance Outputable EvBindsVar where
766 ppr (EvBindsVar _ u) = text "EvBindsVar" <> angleBrackets (ppr u)
767
768 instance Uniquable EvBindsVar where
769 getUnique (EvBindsVar _ u) = u
770
771 instance Outputable EvBind where
772 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
773 = sep [ pp_gw <+> ppr v
774 , nest 2 $ equals <+> ppr e ]
775 where
776 pp_gw = brackets (if is_given then char 'G' else char 'W')
777 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
778
779 instance Outputable EvTerm where
780 ppr (EvId v) = ppr v
781 ppr (EvCast v co) = ppr v <+> (text "`cast`") <+> pprParendCo co
782 ppr (EvCoercion co) = text "CO" <+> ppr co
783 ppr (EvSuperClass d n) = text "sc" <> parens (ppr (d,n))
784 ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
785 ppr (EvLit l) = ppr l
786 ppr (EvCallStack cs) = ppr cs
787 ppr (EvDelayedError ty msg) = text "error"
788 <+> sep [ char '@' <> ppr ty, ppr msg ]
789 ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
790
791 instance Outputable EvLit where
792 ppr (EvNum n) = integer n
793 ppr (EvStr s) = text (show s)
794
795 instance Outputable EvCallStack where
796 ppr EvCsEmpty
797 = text "[]"
798 ppr (EvCsPushCall name loc tm)
799 = ppr (name,loc) <+> text ":" <+> ppr tm
800
801 instance Outputable EvTypeable where
802 ppr (EvTypeableTyCon ts) = text "TC" <+> ppr ts
803 ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
804 ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1
805
806
807 ----------------------------------------------------------------------
808 -- Helper functions for dealing with IP newtype-dictionaries
809 ----------------------------------------------------------------------
810
811 -- | Create a 'Coercion' that unwraps an implicit-parameter or
812 -- overloaded-label dictionary to expose the underlying value. We
813 -- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
814 -- and return a 'Coercion' `co :: IP sym ty ~ ty` or
815 -- `co :: IsLabel sym ty ~ Proxy# sym -> ty`. See also
816 -- Note [Type-checking overloaded labels] in TcExpr.
817 unwrapIP :: Type -> CoercionR
818 unwrapIP ty =
819 case unwrapNewTyCon_maybe tc of
820 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
821 Nothing -> pprPanic "unwrapIP" $
822 text "The dictionary for" <+> quotes (ppr tc)
823 <+> text "is not a newtype!"
824 where
825 (tc, tys) = splitTyConApp ty
826
827 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
828 -- dictionary. See 'unwrapIP'.
829 wrapIP :: Type -> CoercionR
830 wrapIP ty = mkSymCo (unwrapIP ty)