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