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