Collect coercion variables, not type variables
[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, isEmptyEvBindMap,
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 coercion ~N
84 type TcCoercionR = CoercionR -- A Representational coercion ~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
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 data EvBindsVar
287 = EvBindsVar {
288 ebv_uniq :: Unique,
289 -- The Unique is for debug printing only
290
291 ebv_binds :: IORef EvBindMap,
292 -- The main payload: the value-level evidence bindings
293 -- (dictionaries etc)
294
295 ebv_tcvs :: IORef CoVarSet
296 -- The free coercion vars of the (rhss of) the coercion bindings
297 --
298 -- Coercions don't actually have bindings
299 -- because we plug them in-place (via a mutable
300 -- variable); but we keep their free variables
301 -- so that we can report unused given constraints
302 -- See Note [Tracking redundant constraints] in TcSimplify
303 }
304
305 instance Data.Data TcEvBinds where
306 -- Placeholder; we can't travers into TcEvBinds
307 toConstr _ = abstractConstr "TcEvBinds"
308 gunfold _ _ = error "gunfold"
309 dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
310
311 -----------------
312 newtype EvBindMap
313 = EvBindMap {
314 ev_bind_varenv :: DVarEnv EvBind
315 } -- Map from evidence variables to evidence terms
316 -- We use @DVarEnv@ here to get deterministic ordering when we
317 -- turn it into a Bag.
318 -- If we don't do that, when we generate let bindings for
319 -- dictionaries in dsTcEvBinds they will be generated in random
320 -- order.
321 --
322 -- For example:
323 --
324 -- let $dEq = GHC.Classes.$fEqInt in
325 -- let $$dNum = GHC.Num.$fNumInt in ...
326 --
327 -- vs
328 --
329 -- let $dNum = GHC.Num.$fNumInt in
330 -- let $dEq = GHC.Classes.$fEqInt in ...
331 --
332 -- See Note [Deterministic UniqFM] in UniqDFM for explanation why
333 -- @UniqFM@ can lead to nondeterministic order.
334
335 emptyEvBindMap :: EvBindMap
336 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
337
338 extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
339 extendEvBinds bs ev_bind
340 = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
341 (eb_lhs ev_bind)
342 ev_bind }
343
344 isEmptyEvBindMap :: EvBindMap -> Bool
345 isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
346
347 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
348 lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
349
350 evBindMapBinds :: EvBindMap -> Bag EvBind
351 evBindMapBinds = foldEvBindMap consBag emptyBag
352
353 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
354 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
355
356 instance Outputable EvBindMap where
357 ppr (EvBindMap m) = ppr m
358
359 -----------------
360 -- All evidence is bound by EvBinds; no side effects
361 data EvBind
362 = EvBind { eb_lhs :: EvVar
363 , eb_rhs :: EvTerm
364 , eb_is_given :: Bool -- True <=> given
365 -- See Note [Tracking redundant constraints] in TcSimplify
366 }
367
368 evBindVar :: EvBind -> EvVar
369 evBindVar = eb_lhs
370
371 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
372 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
373
374
375 mkGivenEvBind :: EvVar -> EvTerm -> EvBind
376 mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
377
378 data EvTerm
379 = EvId EvId -- Any sort of evidence Id, including coercions
380
381 | EvCoercion TcCoercion -- coercion bindings
382 -- See Note [Coercion evidence terms]
383
384 | EvCast EvTerm TcCoercionR -- d |> co
385
386 | EvDFunApp DFunId -- Dictionary instance application
387 [Type] [EvTerm]
388
389 | EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
390 -- See Note [Deferring coercion errors to runtime]
391 -- in TcSimplify
392
393 | EvSuperClass EvTerm Int -- n'th superclass. Used for both equalities and
394 -- dictionaries, even though the former have no
395 -- selector Id. We count up from _0_
396
397 | EvLit EvLit -- Dictionary for KnownNat and KnownSymbol classes.
398 -- Note [KnownNat & KnownSymbol and EvLit]
399
400 | EvCallStack EvCallStack -- Dictionary for CallStack implicit parameters
401
402 | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
403
404 deriving Data.Data
405
406
407 -- | Instructions on how to make a 'Typeable' dictionary.
408 -- See Note [Typeable evidence terms]
409 data EvTypeable
410 = EvTypeableTyCon [EvTerm] -- ^ Dictionary for @Typeable (T k1..kn)@.
411 -- The EvTerms are for the arguments
412
413 | EvTypeableTyApp EvTerm EvTerm
414 -- ^ Dictionary for @Typeable (s t)@,
415 -- given a dictionaries for @s@ and @t@
416
417 | EvTypeableTyLit EvTerm
418 -- ^ Dictionary for a type literal,
419 -- e.g. @Typeable "foo"@ or @Typeable 3@
420 -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
421 -- (see Trac #10348)
422
423 deriving Data.Data
424
425 data EvLit
426 = EvNum Integer
427 | EvStr FastString
428 deriving Data.Data
429
430 -- | Evidence for @CallStack@ implicit parameters.
431 data EvCallStack
432 -- See Note [Overview of implicit CallStacks]
433 = EvCsEmpty
434 | EvCsPushCall Name RealSrcSpan EvTerm
435 -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
436 -- @loc@, in a calling context @stk@.
437 deriving Data.Data
438
439 {-
440 Note [Typeable evidence terms]
441 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
442 The EvTypeable data type looks isomorphic to Type, but the EvTerms
443 inside can be EvIds. Eg
444 f :: forall a. Typeable a => a -> TypeRep
445 f x = typeRep (undefined :: Proxy [a])
446 Here for the (Typeable [a]) dictionary passed to typeRep we make
447 evidence
448 dl :: Typeable [a] = EvTypeable [a]
449 (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
450 where
451 d :: Typable a
452 is the lambda-bound dictionary passed into f.
453
454 Note [Coercion evidence terms]
455 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
456 A "coercion evidence term" takes one of these forms
457 co_tm ::= EvId v where v :: t1 ~# t2
458 | EvCoercion co
459 | EvCast co_tm co
460
461 We do quite often need to get a TcCoercion from an EvTerm; see
462 'evTermCoercion'.
463
464 INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
465 a coercion evidence term. Consider for example
466 [G] d :: F Int a
467 If we have
468 ax7 a :: F Int a ~ (a ~ Bool)
469 then we do NOT generate the constraint
470 [G] (d |> ax7 a) :: a ~ Bool
471 because that does not satisfy the invariant (d is not a coercion variable).
472 Instead we make a binding
473 g1 :: a~Bool = g |> ax7 a
474 and the constraint
475 [G] g1 :: a~Bool
476 See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
477
478 Note [EvBinds/EvTerm]
479 ~~~~~~~~~~~~~~~~~~~~~
480 How evidence is created and updated. Bindings for dictionaries,
481 and coercions and implicit parameters are carried around in TcEvBinds
482 which during constraint generation and simplification is always of the
483 form (TcEvBinds ref). After constraint simplification is finished it
484 will be transformed to t an (EvBinds ev_bag).
485
486 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
487 However, all EvVars that correspond to *wanted* coercion terms in
488 an EvBind must be mutable variables so that they can be readily
489 inlined (by zonking) after constraint simplification is finished.
490
491 Conclusion: a new wanted coercion variable should be made mutable.
492 [Notice though that evidence variables that bind coercion terms
493 from super classes will be "given" and hence rigid]
494
495
496 Note [KnownNat & KnownSymbol and EvLit]
497 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
498 A part of the type-level literals implementation are the classes
499 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
500 defining singleton values. Here is the key stuff from GHC.TypeLits
501
502 class KnownNat (n :: Nat) where
503 natSing :: SNat n
504
505 newtype SNat (n :: Nat) = SNat Integer
506
507 Conceptually, this class has infinitely many instances:
508
509 instance KnownNat 0 where natSing = SNat 0
510 instance KnownNat 1 where natSing = SNat 1
511 instance KnownNat 2 where natSing = SNat 2
512 ...
513
514 In practice, we solve `KnownNat` predicates in the type-checker
515 (see typecheck/TcInteract.hs) because we can't have infinately many instances.
516 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
517
518 We make the following assumptions about dictionaries in GHC:
519 1. The "dictionary" for classes with a single method---like `KnownNat`---is
520 a newtype for the type of the method, so using a evidence amounts
521 to a coercion, and
522 2. Newtypes use the same representation as their definition types.
523
524 So, the evidence for `KnownNat` is just a value of the representation type,
525 wrapped in two newtype constructors: one to make it into a `SNat` value,
526 and another to make it into a `KnownNat` dictionary.
527
528 Also note that `natSing` and `SNat` are never actually exposed from the
529 library---they are just an implementation detail. Instead, users see
530 a more convenient function, defined in terms of `natSing`:
531
532 natVal :: KnownNat n => proxy n -> Integer
533
534 The reason we don't use this directly in the class is that it is simpler
535 and more efficient to pass around an integer rather than an entier function,
536 especially when the `KnowNat` evidence is packaged up in an existential.
537
538 The story for kind `Symbol` is analogous:
539 * class KnownSymbol
540 * newtype SSymbol
541 * Evidence: EvLit (EvStr n)
542
543
544 Note [Overview of implicit CallStacks]
545 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
546 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
547
548 The goal of CallStack evidence terms is to reify locations
549 in the program source as runtime values, without any support
550 from the RTS. We accomplish this by assigning a special meaning
551 to constraints of type GHC.Stack.Types.HasCallStack, an alias
552
553 type HasCallStack = (?callStack :: CallStack)
554
555 Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
556 important) are solved in three steps:
557
558 1. Occurrences of CallStack IPs are solved directly from the given IP,
559 just like a regular IP. For example, the occurrence of `?stk` in
560
561 error :: (?stk :: CallStack) => String -> a
562 error s = raise (ErrorCall (s ++ prettyCallStack ?stk))
563
564 will be solved for the `?stk` in `error`s context as before.
565
566 2. In a function call, instead of simply passing the given IP, we first
567 append the current call-site to it. For example, consider a
568 call to the callstack-aware `error` above.
569
570 undefined :: (?stk :: CallStack) => a
571 undefined = error "undefined!"
572
573 Here we want to take the given `?stk` and append the current
574 call-site, before passing it to `error`. In essence, we want to
575 rewrite `error "undefined!"` to
576
577 let ?stk = pushCallStack <error's location> ?stk
578 in error "undefined!"
579
580 We achieve this effect by emitting a NEW wanted
581
582 [W] d :: IP "stk" CallStack
583
584 from which we build the evidence term
585
586 EvCsPushCall "error" <error's location> (EvId d)
587
588 that we use to solve the call to `error`. The new wanted `d` will
589 then be solved per rule (1), ie as a regular IP.
590
591 (see TcInteract.interactDict)
592
593 3. We default any insoluble CallStacks to the empty CallStack. Suppose
594 `undefined` did not request a CallStack, ie
595
596 undefinedNoStk :: a
597 undefinedNoStk = error "undefined!"
598
599 Under the usual IP rules, the new wanted from rule (2) would be
600 insoluble as there's no given IP from which to solve it, so we
601 would get an "unbound implicit parameter" error.
602
603 We don't ever want to emit an insoluble CallStack IP, so we add a
604 defaulting pass to default any remaining wanted CallStacks to the
605 empty CallStack with the evidence term
606
607 EvCsEmpty
608
609 (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks)
610
611 This provides a lightweight mechanism for building up call-stacks
612 explicitly, but is notably limited by the fact that the stack will
613 stop at the first function whose type does not include a CallStack IP.
614 For example, using the above definition of `undefined`:
615
616 head :: [a] -> a
617 head [] = undefined
618 head (x:_) = x
619
620 g = head []
621
622 the resulting CallStack will include the call to `undefined` in `head`
623 and the call to `error` in `undefined`, but *not* the call to `head`
624 in `g`, because `head` did not explicitly request a CallStack.
625
626
627 Important Details:
628 - GHC should NEVER report an insoluble CallStack constraint.
629
630 - GHC should NEVER infer a CallStack constraint unless one was requested
631 with a partial type signature (See TcType.pickQuantifiablePreds).
632
633 - A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
634 where the String is the name of the binder that is used at the
635 SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
636 package/module/file name, as well as the full source-span. Both
637 CallStack and SrcLoc are kept abstract so only GHC can construct new
638 values.
639
640 - We will automatically solve any wanted CallStack regardless of the
641 name of the IP, i.e.
642
643 f = show (?stk :: CallStack)
644 g = show (?loc :: CallStack)
645
646 are both valid. However, we will only push new SrcLocs onto existing
647 CallStacks when the IP names match, e.g. in
648
649 head :: (?loc :: CallStack) => [a] -> a
650 head [] = error (show (?stk :: CallStack))
651
652 the printed CallStack will NOT include head's call-site. This reflects the
653 standard scoping rules of implicit-parameters.
654
655 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
656 The desugarer will need to unwrap the IP newtype before pushing a new
657 call-site onto a given stack (See DsBinds.dsEvCallStack)
658
659 - When we emit a new wanted CallStack from rule (2) we set its origin to
660 `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
661 (see TcInteract.interactDict).
662
663 This is a bit shady, but is how we ensure that the new wanted is
664 solved like a regular IP.
665
666 -}
667
668 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
669 mkEvCast ev lco
670 | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
671 isTcReflCo lco = ev
672 | otherwise = EvCast ev lco
673
674 mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
675 mkEvScSelectors ev cls tys
676 = zipWith mk_pr (immSuperClasses cls tys) [0..]
677 where
678 mk_pr pred i = (pred, EvSuperClass ev i)
679
680 emptyTcEvBinds :: TcEvBinds
681 emptyTcEvBinds = EvBinds emptyBag
682
683 isEmptyTcEvBinds :: TcEvBinds -> Bool
684 isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
685 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
686
687
688 evTermCoercion :: EvTerm -> TcCoercion
689 -- Applied only to EvTerms of type (s~t)
690 -- See Note [Coercion evidence terms]
691 evTermCoercion (EvId v) = mkCoVarCo v
692 evTermCoercion (EvCoercion co) = co
693 evTermCoercion (EvCast tm co) = mkCoCast (evTermCoercion tm) co
694 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
695
696 evVarsOfTerm :: EvTerm -> VarSet
697 evVarsOfTerm (EvId v) = unitVarSet v
698 evVarsOfTerm (EvCoercion co) = coVarsOfCo co
699 evVarsOfTerm (EvDFunApp _ _ evs) = mapUnionVarSet evVarsOfTerm evs
700 evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
701 evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfCo co
702 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
703 evVarsOfTerm (EvLit _) = emptyVarSet
704 evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs
705 evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
706
707 evVarsOfTerms :: [EvTerm] -> VarSet
708 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
709
710 -- | Do SCC analysis on a bag of 'EvBind's.
711 sccEvBinds :: Bag EvBind -> [SCC EvBind]
712 sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
713 where
714 edges :: [(EvBind, EvVar, [EvVar])]
715 edges = foldrBag ((:) . mk_node) [] bs
716
717 mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
718 mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
719 = (b, var, nonDetEltsUFM (evVarsOfTerm term `unionVarSet`
720 coVarsOfType (varType var)))
721 -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
722 -- is still deterministic even if the edges are in nondeterministic order
723 -- as explained in Note [Deterministic SCC] in Digraph.
724
725 evVarsOfCallStack :: EvCallStack -> VarSet
726 evVarsOfCallStack cs = case cs of
727 EvCsEmpty -> emptyVarSet
728 EvCsPushCall _ _ tm -> evVarsOfTerm tm
729
730 evVarsOfTypeable :: EvTypeable -> VarSet
731 evVarsOfTypeable ev =
732 case ev of
733 EvTypeableTyCon es -> evVarsOfTerms es
734 EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
735 EvTypeableTyLit e -> evVarsOfTerm e
736
737 {-
738 ************************************************************************
739 * *
740 Pretty printing
741 * *
742 ************************************************************************
743 -}
744
745 instance Outputable HsWrapper where
746 ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
747
748 pprHsWrapper ::HsWrapper -> (Bool -> SDoc) -> SDoc
749 -- With -fprint-typechecker-elaboration, print the wrapper
750 -- otherwise just print what's inside
751 -- The pp_thing_inside function takes Bool to say whether
752 -- it's in a position that needs parens for a non-atomic thing
753 pprHsWrapper wrap pp_thing_inside
754 = sdocWithDynFlags $ \ dflags ->
755 if gopt Opt_PrintTypecheckerElaboration dflags
756 then help pp_thing_inside wrap False
757 else pp_thing_inside False
758 where
759 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
760 -- True <=> appears in function application position
761 -- False <=> appears as body of let or lambda
762 help it WpHole = it
763 help it (WpCompose f1 f2) = help (help it f2) f1
764 help it (WpFun f1 f2 t1) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
765 help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
766 help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
767 <+> pprParendCo co)]
768 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
769 help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <+> pprParendType ty]
770 help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pp_bndr id, it False]
771 help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pp_bndr tv, it False]
772 help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
773
774 pp_bndr v = pprBndr LambdaBind v <> dot
775
776 add_parens, no_parens :: SDoc -> Bool -> SDoc
777 add_parens d True = parens d
778 add_parens d False = d
779 no_parens d _ = d
780
781 instance Outputable TcEvBinds where
782 ppr (TcEvBinds v) = ppr v
783 ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
784
785 instance Outputable EvBindsVar where
786 ppr (EvBindsVar { ebv_uniq = u })
787 = text "EvBindsVar" <> angleBrackets (ppr u)
788
789 instance Uniquable EvBindsVar where
790 getUnique (EvBindsVar { ebv_uniq = u }) = u
791
792 instance Outputable EvBind where
793 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
794 = sep [ pp_gw <+> ppr v
795 , nest 2 $ equals <+> ppr e ]
796 where
797 pp_gw = brackets (if is_given then char 'G' else char 'W')
798 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
799
800 instance Outputable EvTerm where
801 ppr (EvId v) = ppr v
802 ppr (EvCast v co) = ppr v <+> (text "`cast`") <+> pprParendCo co
803 ppr (EvCoercion co) = text "CO" <+> ppr co
804 ppr (EvSuperClass d n) = text "sc" <> parens (ppr (d,n))
805 ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
806 ppr (EvLit l) = ppr l
807 ppr (EvCallStack cs) = ppr cs
808 ppr (EvDelayedError ty msg) = text "error"
809 <+> sep [ char '@' <> ppr ty, ppr msg ]
810 ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
811
812 instance Outputable EvLit where
813 ppr (EvNum n) = integer n
814 ppr (EvStr s) = text (show s)
815
816 instance Outputable EvCallStack where
817 ppr EvCsEmpty
818 = text "[]"
819 ppr (EvCsPushCall name loc tm)
820 = ppr (name,loc) <+> text ":" <+> ppr tm
821
822 instance Outputable EvTypeable where
823 ppr (EvTypeableTyCon ts) = text "TC" <+> ppr ts
824 ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
825 ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1
826
827
828 ----------------------------------------------------------------------
829 -- Helper functions for dealing with IP newtype-dictionaries
830 ----------------------------------------------------------------------
831
832 -- | Create a 'Coercion' that unwraps an implicit-parameter or
833 -- overloaded-label dictionary to expose the underlying value. We
834 -- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
835 -- and return a 'Coercion' `co :: IP sym ty ~ ty` or
836 -- `co :: IsLabel sym ty ~ Proxy# sym -> ty`. See also
837 -- Note [Type-checking overloaded labels] in TcExpr.
838 unwrapIP :: Type -> CoercionR
839 unwrapIP ty =
840 case unwrapNewTyCon_maybe tc of
841 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
842 Nothing -> pprPanic "unwrapIP" $
843 text "The dictionary for" <+> quotes (ppr tc)
844 <+> text "is not a newtype!"
845 where
846 (tc, tys) = splitTyConApp ty
847
848 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
849 -- dictionary. See 'unwrapIP'.
850 wrapIP :: Type -> CoercionR
851 wrapIP ty = mkSymCo (unwrapIP ty)