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