never executed always true always false
1 -- (c) The University of Glasgow 2006
2
3 {-# LANGUAGE DeriveDataTypeable #-}
4 {-# LANGUAGE LambdaCase #-}
5
6 module GHC.Tc.Types.Evidence (
7
8 -- * HsWrapper
9 HsWrapper(..),
10 (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams,
11 mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
12 idHsWrapper, isIdHsWrapper,
13 pprHsWrapper, hsWrapDictBinders,
14
15 -- * Evidence bindings
16 TcEvBinds(..), EvBindsVar(..),
17 EvBindMap(..), emptyEvBindMap, extendEvBinds,
18 lookupEvBind, evBindMapBinds,
19 foldEvBindMap, nonDetStrictFoldEvBindMap,
20 filterEvBindMap,
21 isEmptyEvBindMap,
22 evBindMapToVarSet,
23 varSetMinusEvBindMap,
24 EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
25 evBindVar, isCoEvBindsVar,
26
27 -- * EvTerm (already a CoreExpr)
28 EvTerm(..), EvExpr,
29 evId, evCoercion, evCast, evDFunApp, evDataConApp, evSelector,
30 mkEvCast, evVarsOfTerm, mkEvScSelectors, evTypeable, findNeededEvVars,
31
32 evTermCoercion, evTermCoercion_maybe,
33 EvCallStack(..),
34 EvTypeable(..),
35
36 -- * HoleExprRef
37 HoleExprRef(..),
38
39 -- * TcCoercion
40 TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
41 TcMCoercion, TcMCoercionN, TcMCoercionR,
42 Role(..), LeftOrRight(..), pickLR,
43 mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
44 mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
45 mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
46 mkTcSymCo, mkTcSymMCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSymCo,
47 maybeTcSubCo, tcDowngradeRole,
48 mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflRightMCo, mkTcGReflLeftCo, mkTcGReflLeftMCo,
49 mkTcPhantomCo,
50 mkTcCoherenceLeftCo,
51 mkTcCoherenceRightCo,
52 mkTcKindCo,
53 tcCoercionKind,
54 mkTcCoVarCo,
55 mkTcFamilyTyConAppCo,
56 isTcReflCo, isTcReflexiveCo,
57 tcCoercionRole,
58 unwrapIP, wrapIP,
59
60 -- * QuoteWrapper
61 QuoteWrapper(..), applyQuoteWrapper, quoteWrapperTyVarTy
62 ) where
63
64 import GHC.Prelude
65
66 import GHC.Types.Unique.DFM
67 import GHC.Types.Unique.FM
68 import GHC.Types.Var
69 import GHC.Core.Coercion.Axiom
70 import GHC.Core.Coercion
71 import GHC.Core.Ppr () -- Instance OutputableBndr TyVar
72 import GHC.Tc.Utils.TcType
73 import GHC.Core.Type
74 import GHC.Core.TyCon
75 import GHC.Core.DataCon ( DataCon, dataConWrapId )
76 import GHC.Builtin.Names
77 import GHC.Types.Var.Env
78 import GHC.Types.Var.Set
79 import GHC.Core.Predicate
80 import GHC.Data.Pair
81 import GHC.Types.Basic
82
83 import GHC.Core
84 import GHC.Core.Class (Class, classSCSelId )
85 import GHC.Core.FVs ( exprSomeFreeVars )
86
87 import GHC.Utils.Misc
88 import GHC.Utils.Panic
89 import GHC.Utils.Outputable
90
91 import GHC.Data.Bag
92 import GHC.Data.FastString
93
94 import qualified Data.Data as Data
95 import GHC.Types.SrcLoc
96 import Data.IORef( IORef )
97 import GHC.Types.Unique.Set
98 import GHC.Core.Multiplicity
99
100 import qualified Data.Semigroup as S
101
102 {-
103 Note [TcCoercions]
104 ~~~~~~~~~~~~~~~~~~
105 | TcCoercions are a hack used by the typechecker. Normally,
106 Coercions have free variables of type (a ~# b): we call these
107 CoVars. However, the type checker passes around equality evidence
108 (boxed up) at type (a ~ b).
109
110 An TcCoercion is simply a Coercion whose free variables have may be either
111 boxed or unboxed. After we are done with typechecking the desugarer finds the
112 boxed free variables, unboxes them, and creates a resulting real Coercion with
113 kosher free variables.
114
115 -}
116
117 type TcCoercion = Coercion
118 type TcCoercionN = CoercionN -- A Nominal coercion ~N
119 type TcCoercionR = CoercionR -- A Representational coercion ~R
120 type TcCoercionP = CoercionP -- a phantom coercion
121 type TcMCoercion = MCoercion
122 type TcMCoercionN = MCoercionN -- nominal
123 type TcMCoercionR = MCoercionR -- representational
124
125 mkTcReflCo :: Role -> TcType -> TcCoercion
126 mkTcSymCo :: TcCoercion -> TcCoercion
127 mkTcSymMCo :: TcMCoercion -> TcMCoercion
128 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
129 mkTcNomReflCo :: TcType -> TcCoercionN
130 mkTcRepReflCo :: TcType -> TcCoercionR
131 mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
132 mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion
133 mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion -> TcCoercion
134 mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex
135 -> [TcType] -> [TcCoercion] -> TcCoercion
136 mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
137 -> [TcCoercion] -> TcCoercionR
138 mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
139 mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
140 mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion
141 mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
142 mkTcSubCo :: HasDebugCallStack => TcCoercionN -> TcCoercionR
143 tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
144 mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
145 mkTcGReflRightCo :: Role -> TcType -> TcCoercionN -> TcCoercion
146 mkTcGReflRightMCo :: Role -> TcType -> TcMCoercionN -> TcCoercion
147 mkTcGReflLeftCo :: Role -> TcType -> TcCoercionN -> TcCoercion
148 mkTcGReflLeftMCo :: Role -> TcType -> TcMCoercionN -> TcCoercion
149 mkTcCoherenceLeftCo :: Role -> TcType -> TcCoercionN
150 -> TcCoercion -> TcCoercion
151 mkTcCoherenceRightCo :: Role -> TcType -> TcCoercionN
152 -> TcCoercion -> TcCoercion
153 mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP
154 mkTcKindCo :: TcCoercion -> TcCoercionN
155 mkTcCoVarCo :: CoVar -> TcCoercion
156 mkTcFamilyTyConAppCo :: TyCon -> [TcCoercionN] -> TcCoercionN
157
158 tcCoercionKind :: TcCoercion -> Pair TcType
159 tcCoercionRole :: TcCoercion -> Role
160 isTcReflCo :: TcCoercion -> Bool
161
162 -- | This version does a slow check, calculating the related types and seeing
163 -- if they are equal.
164 isTcReflexiveCo :: TcCoercion -> Bool
165
166 mkTcReflCo = mkReflCo
167 mkTcSymCo = mkSymCo
168 mkTcSymMCo = mkSymMCo
169 mkTcTransCo = mkTransCo
170 mkTcNomReflCo = mkNomReflCo
171 mkTcRepReflCo = mkRepReflCo
172 mkTcTyConAppCo = mkTyConAppCo
173 mkTcAppCo = mkAppCo
174 mkTcFunCo = mkFunCo
175 mkTcAxInstCo = mkAxInstCo
176 mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational
177 mkTcForAllCo = mkForAllCo
178 mkTcForAllCos = mkForAllCos
179 mkTcNthCo = mkNthCo
180 mkTcLRCo = mkLRCo
181 mkTcSubCo = mkSubCo
182 tcDowngradeRole = downgradeRole
183 mkTcAxiomRuleCo = mkAxiomRuleCo
184 mkTcGReflRightCo = mkGReflRightCo
185 mkTcGReflRightMCo = mkGReflRightMCo
186 mkTcGReflLeftCo = mkGReflLeftCo
187 mkTcGReflLeftMCo = mkGReflLeftMCo
188 mkTcCoherenceLeftCo = mkCoherenceLeftCo
189 mkTcCoherenceRightCo = mkCoherenceRightCo
190 mkTcPhantomCo = mkPhantomCo
191 mkTcKindCo = mkKindCo
192 mkTcCoVarCo = mkCoVarCo
193 mkTcFamilyTyConAppCo = mkFamilyTyConAppCo
194
195 tcCoercionKind = coercionKind
196 tcCoercionRole = coercionRole
197 isTcReflCo = isReflCo
198 isTcReflexiveCo = isReflexiveCo
199
200 -- | If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing.
201 -- Note that the input coercion should always be nominal.
202 maybeTcSubCo :: HasDebugCallStack => EqRel -> TcCoercionN -> TcCoercion
203 maybeTcSubCo NomEq = id
204 maybeTcSubCo ReprEq = mkTcSubCo
205
206 -- | If a 'SwapFlag' is 'IsSwapped', flip the orientation of a coercion
207 maybeTcSymCo :: SwapFlag -> TcCoercion -> TcCoercion
208 maybeTcSymCo IsSwapped co = mkTcSymCo co
209 maybeTcSymCo NotSwapped co = co
210
211 {-
212 %************************************************************************
213 %* *
214 HsWrapper
215 * *
216 ************************************************************************
217 -}
218
219 data HsWrapper
220 = WpHole -- The identity coercion
221
222 | WpCompose HsWrapper HsWrapper
223 -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
224 --
225 -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
226 -- But ([] a) `WpCompose` ([] b) = ([] b a)
227
228 | WpFun HsWrapper HsWrapper (Scaled TcType)
229 -- (WpFun wrap1 wrap2 (w, t1))[e] = \(x:_w t1). wrap2[ e wrap1[x] ]
230 -- So note that if wrap1 :: exp_arg <= act_arg
231 -- wrap2 :: act_res <= exp_res
232 -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
233 -- This isn't the same as for mkFunCo, but it has to be this way
234 -- because we can't use 'sym' to flip around these HsWrappers
235 -- The TcType is the "from" type of the first wrapper
236 --
237 -- Use 'mkWpFun' to construct such a wrapper.
238
239 | WpCast TcCoercionR -- A cast: [] `cast` co
240 -- Guaranteed not the identity coercion
241 -- At role Representational
242
243 -- Evidence abstraction and application
244 -- (both dictionaries and coercions)
245 | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable
246 | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint
247 -- Kind and Type abstraction and application
248 | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var)
249 | WpTyApp KindOrType -- [] t the 't' is a type (not coercion)
250
251
252 | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings,
253 -- so that the identity coercion is always exactly WpHole
254
255 | WpMultCoercion Coercion -- Require that a Coercion be reflexive; otherwise,
256 -- error in the desugarer. See GHC.Tc.Utils.Unify
257 -- Note [Wrapper returned from tcSubMult]
258 deriving Data.Data
259
260 -- | The Semigroup instance is a bit fishy, since @WpCompose@, as a data
261 -- constructor, is "syntactic" and not associative. Concretely, if @a@, @b@,
262 -- and @c@ aren't @WpHole@:
263 --
264 -- > (a <> b) <> c ?= a <> (b <> c)
265 --
266 -- ==>
267 --
268 -- > (a `WpCompose` b) `WpCompose` c /= @ a `WpCompose` (b `WpCompose` c)
269 --
270 -- However these two associations are are "semantically equal" in the sense
271 -- that they produce equal functions when passed to
272 -- @GHC.HsToCore.Binds.dsHsWrapper@.
273 instance S.Semigroup HsWrapper where
274 (<>) = (<.>)
275
276 instance Monoid HsWrapper where
277 mempty = WpHole
278
279 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
280 WpHole <.> c = c
281 c <.> WpHole = c
282 c1 <.> c2 = c1 `WpCompose` c2
283
284 mkWpCastR :: TcCoercionR -> HsWrapper
285 mkWpCastR co
286 | isTcReflCo co = WpHole
287 | otherwise = assertPpr (tcCoercionRole co == Representational) (ppr co) $
288 WpCast co
289
290 mkWpCastN :: TcCoercionN -> HsWrapper
291 mkWpCastN co
292 | isTcReflCo co = WpHole
293 | otherwise = assertPpr (tcCoercionRole co == Nominal) (ppr co) $
294 WpCast (mkTcSubCo co)
295 -- The mkTcSubCo converts Nominal to Representational
296
297 mkWpTyApps :: [Type] -> HsWrapper
298 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
299
300 mkWpEvApps :: [EvTerm] -> HsWrapper
301 mkWpEvApps args = mk_co_app_fn WpEvApp args
302
303 mkWpEvVarApps :: [EvVar] -> HsWrapper
304 mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map (EvExpr . evId) vs)
305
306 mkWpTyLams :: [TyVar] -> HsWrapper
307 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
308
309 mkWpLams :: [Var] -> HsWrapper
310 mkWpLams ids = mk_co_lam_fn WpEvLam ids
311
312 mkWpLet :: TcEvBinds -> HsWrapper
313 -- This no-op is a quite a common case
314 mkWpLet (EvBinds b) | isEmptyBag b = WpHole
315 mkWpLet ev_binds = WpLet ev_binds
316
317 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
318 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
319
320 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
321 -- For applications, the *first* argument must
322 -- come *last* in the composition sequence
323 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
324
325 idHsWrapper :: HsWrapper
326 idHsWrapper = WpHole
327
328 isIdHsWrapper :: HsWrapper -> Bool
329 isIdHsWrapper WpHole = True
330 isIdHsWrapper _ = False
331
332 hsWrapDictBinders :: HsWrapper -> Bag DictId
333 -- ^ Identifies the /lambda-bound/ dictionaries of an 'HsWrapper'. This is used
334 -- (only) to allow the pattern-match overlap checker to know what Given
335 -- dictionaries are in scope.
336 --
337 -- We specifically do not collect dictionaries bound in a 'WpLet'. These are
338 -- either superclasses of lambda-bound ones, or (extremely numerous) results of
339 -- binding Wanted dictionaries. We definitely don't want all those cluttering
340 -- up the Given dictionaries for pattern-match overlap checking!
341 hsWrapDictBinders wrap = go wrap
342 where
343 go (WpEvLam dict_id) = unitBag dict_id
344 go (w1 `WpCompose` w2) = go w1 `unionBags` go w2
345 go (WpFun _ w _) = go w
346 go WpHole = emptyBag
347 go (WpCast {}) = emptyBag
348 go (WpEvApp {}) = emptyBag
349 go (WpTyLam {}) = emptyBag
350 go (WpTyApp {}) = emptyBag
351 go (WpLet {}) = emptyBag
352 go (WpMultCoercion {}) = emptyBag
353
354 collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
355 -- Collect the outer lambda binders of a HsWrapper,
356 -- stopping as soon as you get to a non-lambda binder
357 collectHsWrapBinders wrap = go wrap []
358 where
359 -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn)
360 go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
361 go (WpEvLam v) wraps = add_lam v (gos wraps)
362 go (WpTyLam v) wraps = add_lam v (gos wraps)
363 go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
364 go wrap wraps = ([], foldl' (<.>) wrap wraps)
365
366 gos [] = ([], WpHole)
367 gos (w:ws) = go w ws
368
369 add_lam v (vs,w) = (v:vs, w)
370
371 {-
372 ************************************************************************
373 * *
374 Evidence bindings
375 * *
376 ************************************************************************
377 -}
378
379 data TcEvBinds
380 = TcEvBinds -- Mutable evidence bindings
381 EvBindsVar -- Mutable because they are updated "later"
382 -- when an implication constraint is solved
383
384 | EvBinds -- Immutable after zonking
385 (Bag EvBind)
386
387 data EvBindsVar
388 = EvBindsVar {
389 ebv_uniq :: Unique,
390 -- The Unique is for debug printing only
391
392 ebv_binds :: IORef EvBindMap,
393 -- The main payload: the value-level evidence bindings
394 -- (dictionaries etc)
395 -- Some Given, some Wanted
396
397 ebv_tcvs :: IORef CoVarSet
398 -- The free Given coercion vars needed by Wanted coercions that
399 -- are solved by filling in their HoleDest in-place. Since they
400 -- don't appear in ebv_binds, we keep track of their free
401 -- variables so that we can report unused given constraints
402 -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
403 }
404
405 | CoEvBindsVar { -- See Note [Coercion evidence only]
406
407 -- See above for comments on ebv_uniq, ebv_tcvs
408 ebv_uniq :: Unique,
409 ebv_tcvs :: IORef CoVarSet
410 }
411
412 instance Data.Data TcEvBinds where
413 -- Placeholder; we can't travers into TcEvBinds
414 toConstr _ = abstractConstr "TcEvBinds"
415 gunfold _ _ = error "gunfold"
416 dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
417
418 {- Note [Coercion evidence only]
419 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
420 Class constraints etc give rise to /term/ bindings for evidence, and
421 we have nowhere to put term bindings in /types/. So in some places we
422 use CoEvBindsVar (see newCoTcEvBinds) to signal that no term-level
423 evidence bindings are allowed. Notebly ():
424
425 - Places in types where we are solving kind constraints (all of which
426 are equalities); see solveEqualities
427
428 - When unifying forall-types
429 -}
430
431 isCoEvBindsVar :: EvBindsVar -> Bool
432 isCoEvBindsVar (CoEvBindsVar {}) = True
433 isCoEvBindsVar (EvBindsVar {}) = False
434
435 -----------------
436 newtype EvBindMap
437 = EvBindMap {
438 ev_bind_varenv :: DVarEnv EvBind
439 } -- Map from evidence variables to evidence terms
440 -- We use @DVarEnv@ here to get deterministic ordering when we
441 -- turn it into a Bag.
442 -- If we don't do that, when we generate let bindings for
443 -- dictionaries in dsTcEvBinds they will be generated in random
444 -- order.
445 --
446 -- For example:
447 --
448 -- let $dEq = GHC.Classes.$fEqInt in
449 -- let $$dNum = GHC.Num.$fNumInt in ...
450 --
451 -- vs
452 --
453 -- let $dNum = GHC.Num.$fNumInt in
454 -- let $dEq = GHC.Classes.$fEqInt in ...
455 --
456 -- See Note [Deterministic UniqFM] in GHC.Types.Unique.DFM for explanation why
457 -- @UniqFM@ can lead to nondeterministic order.
458
459 emptyEvBindMap :: EvBindMap
460 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
461
462 extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
463 extendEvBinds bs ev_bind
464 = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
465 (eb_lhs ev_bind)
466 ev_bind }
467
468 isEmptyEvBindMap :: EvBindMap -> Bool
469 isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
470
471 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
472 lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
473
474 evBindMapBinds :: EvBindMap -> Bag EvBind
475 evBindMapBinds = foldEvBindMap consBag emptyBag
476
477 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
478 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
479
480 -- See Note [Deterministic UniqFM] to learn about nondeterminism.
481 -- If you use this please provide a justification why it doesn't introduce
482 -- nondeterminism.
483 nonDetStrictFoldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
484 nonDetStrictFoldEvBindMap k z bs = nonDetStrictFoldDVarEnv k z (ev_bind_varenv bs)
485
486 filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
487 filterEvBindMap k (EvBindMap { ev_bind_varenv = env })
488 = EvBindMap { ev_bind_varenv = filterDVarEnv k env }
489
490 evBindMapToVarSet :: EvBindMap -> VarSet
491 evBindMapToVarSet (EvBindMap dve) = unsafeUFMToUniqSet (mapUFM evBindVar (udfmToUfm dve))
492
493 varSetMinusEvBindMap :: VarSet -> EvBindMap -> VarSet
494 varSetMinusEvBindMap vs (EvBindMap dve) = vs `uniqSetMinusUDFM` dve
495
496 instance Outputable EvBindMap where
497 ppr (EvBindMap m) = ppr m
498
499 -----------------
500 -- All evidence is bound by EvBinds; no side effects
501 data EvBind
502 = EvBind { eb_lhs :: EvVar
503 , eb_rhs :: EvTerm
504 , eb_is_given :: Bool -- True <=> given
505 -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
506 }
507
508 evBindVar :: EvBind -> EvVar
509 evBindVar = eb_lhs
510
511 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
512 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
513
514 -- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
515 mkGivenEvBind :: EvVar -> EvTerm -> EvBind
516 mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
517
518
519 -- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
520 -- Unfortunately, we cannot just do
521 -- type EvTerm = CoreExpr
522 -- Because of staging problems issues around EvTypeable
523 data EvTerm
524 = EvExpr EvExpr
525
526 | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
527
528 | EvFun -- /\as \ds. let binds in v
529 { et_tvs :: [TyVar]
530 , et_given :: [EvVar]
531 , et_binds :: TcEvBinds -- This field is why we need an EvFun
532 -- constructor, and can't just use EvExpr
533 , et_body :: EvVar }
534
535 deriving Data.Data
536
537 type EvExpr = CoreExpr
538
539 -- An EvTerm is (usually) constructed by any of the constructors here
540 -- and those more complicates ones who were moved to module GHC.Tc.Types.EvTerm
541
542 -- | Any sort of evidence Id, including coercions
543 evId :: EvId -> EvExpr
544 evId = Var
545
546 -- coercion bindings
547 -- See Note [Coercion evidence terms]
548 evCoercion :: TcCoercion -> EvTerm
549 evCoercion co = EvExpr (Coercion co)
550
551 -- | d |> co
552 evCast :: EvExpr -> TcCoercion -> EvTerm
553 evCast et tc | isReflCo tc = EvExpr et
554 | otherwise = EvExpr (Cast et tc)
555
556 -- Dictionary instance application
557 evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvTerm
558 evDFunApp df tys ets = EvExpr $ Var df `mkTyApps` tys `mkApps` ets
559
560 evDataConApp :: DataCon -> [Type] -> [EvExpr] -> EvTerm
561 evDataConApp dc tys ets = evDFunApp (dataConWrapId dc) tys ets
562
563 -- Selector id plus the types at which it
564 -- should be instantiated, used for HasField
565 -- dictionaries; see Note [HasField instances]
566 -- in TcInterface
567 evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
568 evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
569
570 -- Dictionary for (Typeable ty)
571 evTypeable :: Type -> EvTypeable -> EvTerm
572 evTypeable = EvTypeable
573
574 -- | Instructions on how to make a 'Typeable' dictionary.
575 -- See Note [Typeable evidence terms]
576 data EvTypeable
577 = EvTypeableTyCon TyCon [EvTerm]
578 -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
579 -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
580 -- the applied kinds..
581
582 | EvTypeableTyApp EvTerm EvTerm
583 -- ^ Dictionary for @Typeable (s t)@,
584 -- given a dictionaries for @s@ and @t@.
585
586 | EvTypeableTrFun EvTerm EvTerm EvTerm
587 -- ^ Dictionary for @Typeable (s # w -> t)@,
588 -- given a dictionaries for @w@, @s@, and @t@.
589
590 | EvTypeableTyLit EvTerm
591 -- ^ Dictionary for a type literal,
592 -- e.g. @Typeable "foo"@ or @Typeable 3@
593 -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
594 -- (see #10348)
595 deriving Data.Data
596
597 -- | Evidence for @CallStack@ implicit parameters.
598 data EvCallStack
599 -- See Note [Overview of implicit CallStacks]
600 = EvCsEmpty
601 | EvCsPushCall
602 FastString -- Usually the name of the function being called
603 -- but can also be "the literal 42"
604 -- or "an if-then-else expression", etc
605 RealSrcSpan -- Location of the call
606 EvExpr -- Rest of the stack
607 -- ^ @EvCsPushCall origin loc stk@ represents a call from @origin@,
608 -- occurring at @loc@, in a calling context @stk@.
609 deriving Data.Data
610
611 {-
612 ************************************************************************
613 * *
614 Evidence for holes
615 * *
616 ************************************************************************
617 -}
618
619 -- | Where to store evidence for expression holes
620 -- See Note [Holes] in GHC.Tc.Types.Constraint
621 data HoleExprRef = HER (IORef EvTerm) -- ^ where to write the erroring expression
622 TcType -- ^ expected type of that expression
623 Unique -- ^ for debug output only
624
625 instance Outputable HoleExprRef where
626 ppr (HER _ _ u) = ppr u
627
628 instance Data.Data HoleExprRef where
629 -- Placeholder; we can't traverse into HoleExprRef
630 toConstr _ = abstractConstr "HoleExprRef"
631 gunfold _ _ = error "gunfold"
632 dataTypeOf _ = Data.mkNoRepType "HoleExprRef"
633
634 {-
635 Note [Typeable evidence terms]
636 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
637 The EvTypeable data type looks isomorphic to Type, but the EvTerms
638 inside can be EvIds. Eg
639 f :: forall a. Typeable a => a -> TypeRep
640 f x = typeRep (undefined :: Proxy [a])
641 Here for the (Typeable [a]) dictionary passed to typeRep we make
642 evidence
643 dl :: Typeable [a] = EvTypeable [a]
644 (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
645 where
646 d :: Typable a
647 is the lambda-bound dictionary passed into f.
648
649 Note [Coercion evidence terms]
650 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
651 A "coercion evidence term" takes one of these forms
652 co_tm ::= EvId v where v :: t1 ~# t2
653 | EvCoercion co
654 | EvCast co_tm co
655
656 We do quite often need to get a TcCoercion from an EvTerm; see
657 'evTermCoercion'.
658
659 INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
660 a coercion evidence term. Consider for example
661 [G] d :: F Int a
662 If we have
663 ax7 a :: F Int a ~ (a ~ Bool)
664 then we do NOT generate the constraint
665 [G] (d |> ax7 a) :: a ~ Bool
666 because that does not satisfy the invariant (d is not a coercion variable).
667 Instead we make a binding
668 g1 :: a~Bool = g |> ax7 a
669 and the constraint
670 [G] g1 :: a~Bool
671 See #7238 and Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint
672
673 Note [EvBinds/EvTerm]
674 ~~~~~~~~~~~~~~~~~~~~~
675 How evidence is created and updated. Bindings for dictionaries,
676 and coercions and implicit parameters are carried around in TcEvBinds
677 which during constraint generation and simplification is always of the
678 form (TcEvBinds ref). After constraint simplification is finished it
679 will be transformed to t an (EvBinds ev_bag).
680
681 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
682 However, all EvVars that correspond to *wanted* coercion terms in
683 an EvBind must be mutable variables so that they can be readily
684 inlined (by zonking) after constraint simplification is finished.
685
686 Conclusion: a new wanted coercion variable should be made mutable.
687 [Notice though that evidence variables that bind coercion terms
688 from super classes will be "given" and hence rigid]
689
690
691 Note [Overview of implicit CallStacks]
692 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
693 (See https://gitlab.haskell.org/ghc/ghc/wikis/explicit-call-stack/implicit-locations)
694
695 The goal of CallStack evidence terms is to reify locations
696 in the program source as runtime values, without any support
697 from the RTS. We accomplish this by assigning a special meaning
698 to constraints of type GHC.Stack.Types.HasCallStack, an alias
699
700 type HasCallStack = (?callStack :: CallStack)
701
702 Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
703 important) are solved in three steps:
704
705 1. Explicit, user-written occurrences of `?stk :: CallStack`
706 which have IPOccOrigin, are solved directly from the given IP,
707 just like a regular IP; see GHC.Tc.Solver.Interact.interactDict.
708
709 For example, the occurrence of `?stk` in
710
711 error :: (?stk :: CallStack) => String -> a
712 error s = raise (ErrorCall (s ++ prettyCallStack ?stk))
713
714 will be solved for the `?stk` in `error`s context as before.
715
716 2. In a function call, instead of simply passing the given IP, we first
717 append the current call-site to it. For example, consider a
718 call to the callstack-aware `error` above.
719
720 foo :: (?stk :: CallStack) => a
721 foo = error "undefined!"
722
723 Here we want to take the given `?stk` and append the current
724 call-site, before passing it to `error`. In essence, we want to
725 rewrite `foo "undefined!"` to
726
727 let ?stk = pushCallStack <foo's location> ?stk
728 in foo "undefined!"
729
730 We achieve this as follows:
731
732 * At a call of foo :: (?stk :: CallStack) => blah
733 we emit a Wanted
734 [W] d1 : IP "stk" CallStack
735 with CtOrigin = OccurrenceOf "foo"
736
737 * We /solve/ this constraint, in GHC.Tc.Solver.Canonical.canClassNC
738 by emitting a NEW Wanted
739 [W] d2 :: IP "stk" CallStack
740 with CtOrigin = IPOccOrigin
741
742 and solve d1 = EvCsPushCall "foo" <foo's location> (EvId d1)
743
744 * The new Wanted, for `d2` will be solved per rule (1), ie as a regular IP.
745
746 3. We use the predicate isPushCallStackOrigin to identify whether we
747 want to do (1) solve directly, or (2) push and then solve directly.
748 Key point (see #19918): the CtOrigin where we want to push an item on the
749 call stack can include IfThenElseOrigin etc, when RebindableSyntax is
750 involved. See the defn of fun_orig in GHC.Tc.Gen.App.tcInstFun; it is
751 this CtOrigin that is pinned on the constraints generated by functions
752 in the "expansion" for rebindable syntax. c.f. GHC.Rename.Expr
753 Note [Handling overloaded and rebindable constructs]
754
755 4. We default any insoluble CallStacks to the empty CallStack. Suppose
756 `undefined` did not request a CallStack, ie
757
758 undefinedNoStk :: a
759 undefinedNoStk = error "undefined!"
760
761 Under the usual IP rules, the new wanted from rule (2) would be
762 insoluble as there's no given IP from which to solve it, so we
763 would get an "unbound implicit parameter" error.
764
765 We don't ever want to emit an insoluble CallStack IP, so we add a
766 defaulting pass to default any remaining wanted CallStacks to the
767 empty CallStack with the evidence term
768
769 EvCsEmpty
770
771 (see GHC.Tc.Solver.simplifyTopWanteds and GHC.Tc.Solver.defaultCallStacks)
772
773 This provides a lightweight mechanism for building up call-stacks
774 explicitly, but is notably limited by the fact that the stack will
775 stop at the first function whose type does not include a CallStack IP.
776 For example, using the above definition of `undefined`:
777
778 head :: [a] -> a
779 head [] = undefined
780 head (x:_) = x
781
782 g = head []
783
784 the resulting CallStack will include the call to `undefined` in `head`
785 and the call to `error` in `undefined`, but *not* the call to `head`
786 in `g`, because `head` did not explicitly request a CallStack.
787
788
789 Important Details:
790 - GHC should NEVER report an insoluble CallStack constraint.
791
792 - GHC should NEVER infer a CallStack constraint unless one was requested
793 with a partial type signature (See TcType.pickQuantifiablePreds).
794
795 - A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
796 where the String is the name of the binder that is used at the
797 SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
798 package/module/file name, as well as the full source-span. Both
799 CallStack and SrcLoc are kept abstract so only GHC can construct new
800 values.
801
802 - We will automatically solve any wanted CallStack regardless of the
803 name of the IP, i.e.
804
805 f = show (?stk :: CallStack)
806 g = show (?loc :: CallStack)
807
808 are both valid. However, we will only push new SrcLocs onto existing
809 CallStacks when the IP names match, e.g. in
810
811 head :: (?loc :: CallStack) => [a] -> a
812 head [] = error (show (?stk :: CallStack))
813
814 the printed CallStack will NOT include head's call-site. This reflects the
815 standard scoping rules of implicit-parameters.
816
817 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
818 The desugarer will need to unwrap the IP newtype before pushing a new
819 call-site onto a given stack (See GHC.HsToCore.Binds.dsEvCallStack)
820
821 - When we emit a new wanted CallStack from rule (2) we set its origin to
822 `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
823 (see GHC.Tc.Solver.Interact.interactDict).
824
825 This is a bit shady, but is how we ensure that the new wanted is
826 solved like a regular IP.
827
828 -}
829
830 mkEvCast :: EvExpr -> TcCoercion -> EvTerm
831 mkEvCast ev lco
832 | assertPpr (tcCoercionRole lco == Representational)
833 (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]) $
834 isTcReflCo lco = EvExpr ev
835 | otherwise = evCast ev lco
836
837
838 mkEvScSelectors -- Assume class (..., D ty, ...) => C a b
839 :: Class -> [TcType] -- C ty1 ty2
840 -> [(TcPredType, -- D ty[ty1/a,ty2/b]
841 EvExpr) -- :: C ty1 ty2 -> D ty[ty1/a,ty2/b]
842 ]
843 mkEvScSelectors cls tys
844 = zipWith mk_pr (immSuperClasses cls tys) [0..]
845 where
846 mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys)
847 where
848 sc_sel_id = classSCSelId cls i -- Zero-indexed
849
850 emptyTcEvBinds :: TcEvBinds
851 emptyTcEvBinds = EvBinds emptyBag
852
853 isEmptyTcEvBinds :: TcEvBinds -> Bool
854 isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
855 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
856
857 evTermCoercion_maybe :: EvTerm -> Maybe TcCoercion
858 -- Applied only to EvTerms of type (s~t)
859 -- See Note [Coercion evidence terms]
860 evTermCoercion_maybe ev_term
861 | EvExpr e <- ev_term = go e
862 | otherwise = Nothing
863 where
864 go :: EvExpr -> Maybe TcCoercion
865 go (Var v) = return (mkCoVarCo v)
866 go (Coercion co) = return co
867 go (Cast tm co) = do { co' <- go tm
868 ; return (mkCoCast co' co) }
869 go _ = Nothing
870
871 evTermCoercion :: EvTerm -> TcCoercion
872 evTermCoercion tm = case evTermCoercion_maybe tm of
873 Just co -> co
874 Nothing -> pprPanic "evTermCoercion" (ppr tm)
875
876
877 {- *********************************************************************
878 * *
879 Free variables
880 * *
881 ********************************************************************* -}
882
883 findNeededEvVars :: EvBindMap -> VarSet -> VarSet
884 -- Find all the Given evidence needed by seeds,
885 -- looking transitively through binds
886 findNeededEvVars ev_binds seeds
887 = transCloVarSet also_needs seeds
888 where
889 also_needs :: VarSet -> VarSet
890 also_needs needs = nonDetStrictFoldUniqSet add emptyVarSet needs
891 -- It's OK to use a non-deterministic fold here because we immediately
892 -- forget about the ordering by creating a set
893
894 add :: Var -> VarSet -> VarSet
895 add v needs
896 | Just ev_bind <- lookupEvBind ev_binds v
897 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
898 , is_given
899 = evVarsOfTerm rhs `unionVarSet` needs
900 | otherwise
901 = needs
902
903 evVarsOfTerm :: EvTerm -> VarSet
904 evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
905 evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
906 evVarsOfTerm (EvFun {}) = emptyVarSet -- See Note [Free vars of EvFun]
907
908 evVarsOfTerms :: [EvTerm] -> VarSet
909 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
910
911 evVarsOfTypeable :: EvTypeable -> VarSet
912 evVarsOfTypeable ev =
913 case ev of
914 EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e
915 EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
916 EvTypeableTrFun em e1 e2 -> evVarsOfTerms [em,e1,e2]
917 EvTypeableTyLit e -> evVarsOfTerm e
918
919
920 {- Note [Free vars of EvFun]
921 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
922 Finding the free vars of an EvFun is made tricky by the fact the
923 bindings et_binds may be a mutable variable. Fortunately, we
924 can just squeeze by. Here's how.
925
926 * evVarsOfTerm is used only by GHC.Tc.Solver.neededEvVars.
927 * Each EvBindsVar in an et_binds field of an EvFun is /also/ in the
928 ic_binds field of an Implication
929 * So we can track usage via the processing for that implication,
930 (see Note [Tracking redundant constraints] in GHC.Tc.Solver).
931 We can ignore usage from the EvFun altogether.
932
933 ************************************************************************
934 * *
935 Pretty printing
936 * *
937 ************************************************************************
938 -}
939
940 instance Outputable HsWrapper where
941 ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
942
943 pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
944 -- With -fprint-typechecker-elaboration, print the wrapper
945 -- otherwise just print what's inside
946 -- The pp_thing_inside function takes Bool to say whether
947 -- it's in a position that needs parens for a non-atomic thing
948 pprHsWrapper wrap pp_thing_inside
949 = sdocOption sdocPrintTypecheckerElaboration $ \case
950 True -> help pp_thing_inside wrap False
951 False -> pp_thing_inside False
952 where
953 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
954 -- True <=> appears in function application position
955 -- False <=> appears as body of let or lambda
956 help it WpHole = it
957 help it (WpCompose f1 f2) = help (help it f2) f1
958 help it (WpFun f1 f2 (Scaled w t1)) = add_parens $ text "\\(x" <> dcolon <> brackets (ppr w) <> ppr t1 <> text ")." <+>
959 help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
960 help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
961 <+> pprParendCo co)]
962 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
963 help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <> pprParendType ty]
964 help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pprLamBndr id <> dot, it False]
965 help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pprLamBndr tv <> dot, it False]
966 help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
967 help it (WpMultCoercion co) = add_parens $ sep [it False, nest 2 (text "<multiplicity coercion>"
968 <+> pprParendCo co)]
969
970 pprLamBndr :: Id -> SDoc
971 pprLamBndr v = pprBndr LambdaBind v
972
973 add_parens, no_parens :: SDoc -> Bool -> SDoc
974 add_parens d True = parens d
975 add_parens d False = d
976 no_parens d _ = d
977
978 instance Outputable TcEvBinds where
979 ppr (TcEvBinds v) = ppr v
980 ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
981
982 instance Outputable EvBindsVar where
983 ppr (EvBindsVar { ebv_uniq = u })
984 = text "EvBindsVar" <> angleBrackets (ppr u)
985 ppr (CoEvBindsVar { ebv_uniq = u })
986 = text "CoEvBindsVar" <> angleBrackets (ppr u)
987
988 instance Uniquable EvBindsVar where
989 getUnique = ebv_uniq
990
991 instance Outputable EvBind where
992 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
993 = sep [ pp_gw <+> ppr v
994 , nest 2 $ equals <+> ppr e ]
995 where
996 pp_gw = brackets (if is_given then char 'G' else char 'W')
997 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
998
999 instance Outputable EvTerm where
1000 ppr (EvExpr e) = ppr e
1001 ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
1002 ppr (EvFun { et_tvs = tvs, et_given = gs, et_binds = bs, et_body = w })
1003 = hang (text "\\" <+> sep (map pprLamBndr (tvs ++ gs)) <+> arrow)
1004 2 (ppr bs $$ ppr w) -- Not very pretty
1005
1006 instance Outputable EvCallStack where
1007 ppr EvCsEmpty
1008 = text "[]"
1009 ppr (EvCsPushCall orig loc tm)
1010 = ppr (orig,loc) <+> text ":" <+> ppr tm
1011
1012 instance Outputable EvTypeable where
1013 ppr (EvTypeableTyCon ts _) = text "TyCon" <+> ppr ts
1014 ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
1015 ppr (EvTypeableTrFun tm t1 t2) = parens (ppr t1 <+> mulArrow (ppr tm) <+> ppr t2)
1016 ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1
1017
1018
1019 ----------------------------------------------------------------------
1020 -- Helper functions for dealing with IP newtype-dictionaries
1021 ----------------------------------------------------------------------
1022
1023 -- | Create a 'Coercion' that unwraps an implicit-parameter or
1024 -- overloaded-label dictionary to expose the underlying value. We
1025 -- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
1026 -- and return a 'Coercion' `co :: IP sym ty ~ ty` or
1027 -- `co :: IsLabel sym ty ~ ty`. See also
1028 -- Note [Type-checking overloaded labels] in "GHC.Tc.Gen.Expr".
1029 unwrapIP :: Type -> CoercionR
1030 unwrapIP ty =
1031 case unwrapNewTyCon_maybe tc of
1032 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
1033 Nothing -> pprPanic "unwrapIP" $
1034 text "The dictionary for" <+> quotes (ppr tc)
1035 <+> text "is not a newtype!"
1036 where
1037 (tc, tys) = splitTyConApp ty
1038
1039 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
1040 -- dictionary. See 'unwrapIP'.
1041 wrapIP :: Type -> CoercionR
1042 wrapIP ty = mkSymCo (unwrapIP ty)
1043
1044 ----------------------------------------------------------------------
1045 -- A datatype used to pass information when desugaring quotations
1046 ----------------------------------------------------------------------
1047
1048 -- We have to pass a `EvVar` and `Type` into `dsBracket` so that the
1049 -- correct evidence and types are applied to all the TH combinators.
1050 -- This data type bundles them up together with some convenience methods.
1051 --
1052 -- The EvVar is evidence for `Quote m`
1053 -- The Type is a metavariable for `m`
1054 --
1055 data QuoteWrapper = QuoteWrapper EvVar Type deriving Data.Data
1056
1057 quoteWrapperTyVarTy :: QuoteWrapper -> Type
1058 quoteWrapperTyVarTy (QuoteWrapper _ t) = t
1059
1060 -- | Convert the QuoteWrapper into a normal HsWrapper which can be used to
1061 -- apply its contents.
1062 applyQuoteWrapper :: QuoteWrapper -> HsWrapper
1063 applyQuoteWrapper (QuoteWrapper ev_var m_var)
1064 = mkWpEvVarApps [ev_var] <.> mkWpTyApps [m_var]