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