0930d7afd8cf5e5f1e2283881dd88693cc3534f2
[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 :: 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 instance Data.Data TcEvBinds where
405 -- Placeholder; we can't travers into TcEvBinds
406 toConstr _ = abstractConstr "TcEvBinds"
407 gunfold _ _ = error "gunfold"
408 dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
409
410 -----------------
411 newtype EvBindMap
412 = EvBindMap {
413 ev_bind_varenv :: DVarEnv EvBind
414 } -- Map from evidence variables to evidence terms
415 -- We use @DVarEnv@ here to get deterministic ordering when we
416 -- turn it into a Bag.
417 -- If we don't do that, when we generate let bindings for
418 -- dictionaries in dsTcEvBinds they will be generated in random
419 -- order.
420 --
421 -- For example:
422 --
423 -- let $dEq = GHC.Classes.$fEqInt in
424 -- let $$dNum = GHC.Num.$fNumInt in ...
425 --
426 -- vs
427 --
428 -- let $dNum = GHC.Num.$fNumInt in
429 -- let $dEq = GHC.Classes.$fEqInt in ...
430 --
431 -- See Note [Deterministic UniqFM] in UniqDFM for explanation why
432 -- @UniqFM@ can lead to nondeterministic order.
433
434 emptyEvBindMap :: EvBindMap
435 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
436
437 extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
438 extendEvBinds bs ev_bind
439 = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
440 (eb_lhs ev_bind)
441 ev_bind }
442
443 isEmptyEvBindMap :: EvBindMap -> Bool
444 isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
445
446 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
447 lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
448
449 evBindMapBinds :: EvBindMap -> Bag EvBind
450 evBindMapBinds = foldEvBindMap consBag emptyBag
451
452 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
453 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
454
455 filterEvBindMap :: (EvBind -> Bool) -> EvBindMap -> EvBindMap
456 filterEvBindMap k (EvBindMap { ev_bind_varenv = env })
457 = EvBindMap { ev_bind_varenv = filterDVarEnv k env }
458
459 instance Outputable EvBindMap where
460 ppr (EvBindMap m) = ppr m
461
462 -----------------
463 -- All evidence is bound by EvBinds; no side effects
464 data EvBind
465 = EvBind { eb_lhs :: EvVar
466 , eb_rhs :: EvTerm
467 , eb_is_given :: Bool -- True <=> given
468 -- See Note [Tracking redundant constraints] in TcSimplify
469 }
470
471 evBindVar :: EvBind -> EvVar
472 evBindVar = eb_lhs
473
474 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
475 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
476
477 -- EvTypeable are never given, so we can work with EvExpr here instead of EvTerm
478 mkGivenEvBind :: EvVar -> EvExpr -> EvBind
479 mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = EvExpr tm }
480
481
482 -- An EvTerm is, conceptually, a CoreExpr that implements the constraint.
483 -- Unfortunately, we cannot just do
484 -- type EvTerm = CoreExpr
485 -- Because of staging problems issues around EvTypeable
486 data EvTerm
487 = EvExpr EvExpr
488 | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
489 deriving Data.Data
490
491 type EvExpr = CoreExpr
492
493 -- An EvTerm is (usually) constructed by any of the constructors here
494 -- and those more complicates ones who were moved to module TcEvTerm
495
496 -- | Any sort of evidence Id, including coercions
497 evId :: EvId -> EvExpr
498 evId = Var
499
500 -- coercion bindings
501 -- See Note [Coercion evidence terms]
502 evCoercion :: TcCoercion -> EvExpr
503 evCoercion = Coercion
504
505 -- | d |> co
506 evCast :: EvExpr -> TcCoercion -> EvExpr
507 evCast et tc | isReflCo tc = et
508 | otherwise = Cast et tc
509
510 -- Dictionary instance application
511 evDFunApp :: DFunId -> [Type] -> [EvExpr] -> EvExpr
512 evDFunApp df tys ets = Var df `mkTyApps` tys `mkApps` ets
513
514 -- Selector id plus the types at which it
515 -- should be instantiated, used for HasField
516 -- dictionaries; see Note [HasField instances]
517 -- in TcInterface
518 evSelector :: Id -> [Type] -> [EvExpr] -> EvExpr
519 evSelector sel_id tys tms = Var sel_id `mkTyApps` tys `mkApps` tms
520
521
522 -- Dictionary for (Typeable ty)
523 evTypeable :: Type -> EvTypeable -> EvTerm
524 evTypeable = EvTypeable
525
526 -- | Instructions on how to make a 'Typeable' dictionary.
527 -- See Note [Typeable evidence terms]
528 data EvTypeable
529 = EvTypeableTyCon TyCon [EvTerm]
530 -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
531 -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
532 -- the applied kinds..
533
534 | EvTypeableTyApp EvTerm EvTerm
535 -- ^ Dictionary for @Typeable (s t)@,
536 -- given a dictionaries for @s@ and @t@.
537
538 | EvTypeableTrFun EvTerm EvTerm
539 -- ^ Dictionary for @Typeable (s -> t)@,
540 -- given a dictionaries for @s@ and @t@.
541
542 | EvTypeableTyLit EvTerm
543 -- ^ Dictionary for a type literal,
544 -- e.g. @Typeable "foo"@ or @Typeable 3@
545 -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
546 -- (see Trac #10348)
547 deriving Data.Data
548
549 -- | Evidence for @CallStack@ implicit parameters.
550 data EvCallStack
551 -- See Note [Overview of implicit CallStacks]
552 = EvCsEmpty
553 | EvCsPushCall Name RealSrcSpan EvExpr
554 -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
555 -- @loc@, in a calling context @stk@.
556 deriving Data.Data
557
558 {-
559 Note [Typeable evidence terms]
560 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
561 The EvTypeable data type looks isomorphic to Type, but the EvTerms
562 inside can be EvIds. Eg
563 f :: forall a. Typeable a => a -> TypeRep
564 f x = typeRep (undefined :: Proxy [a])
565 Here for the (Typeable [a]) dictionary passed to typeRep we make
566 evidence
567 dl :: Typeable [a] = EvTypeable [a]
568 (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
569 where
570 d :: Typable a
571 is the lambda-bound dictionary passed into f.
572
573 Note [Coercion evidence terms]
574 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
575 A "coercion evidence term" takes one of these forms
576 co_tm ::= EvId v where v :: t1 ~# t2
577 | EvCoercion co
578 | EvCast co_tm co
579
580 We do quite often need to get a TcCoercion from an EvTerm; see
581 'evTermCoercion'.
582
583 INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
584 a coercion evidence term. Consider for example
585 [G] d :: F Int a
586 If we have
587 ax7 a :: F Int a ~ (a ~ Bool)
588 then we do NOT generate the constraint
589 [G] (d |> ax7 a) :: a ~ Bool
590 because that does not satisfy the invariant (d is not a coercion variable).
591 Instead we make a binding
592 g1 :: a~Bool = g |> ax7 a
593 and the constraint
594 [G] g1 :: a~Bool
595 See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
596
597 Note [EvBinds/EvTerm]
598 ~~~~~~~~~~~~~~~~~~~~~
599 How evidence is created and updated. Bindings for dictionaries,
600 and coercions and implicit parameters are carried around in TcEvBinds
601 which during constraint generation and simplification is always of the
602 form (TcEvBinds ref). After constraint simplification is finished it
603 will be transformed to t an (EvBinds ev_bag).
604
605 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
606 However, all EvVars that correspond to *wanted* coercion terms in
607 an EvBind must be mutable variables so that they can be readily
608 inlined (by zonking) after constraint simplification is finished.
609
610 Conclusion: a new wanted coercion variable should be made mutable.
611 [Notice though that evidence variables that bind coercion terms
612 from super classes will be "given" and hence rigid]
613
614
615 Note [Overview of implicit CallStacks]
616 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
617 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
618
619 The goal of CallStack evidence terms is to reify locations
620 in the program source as runtime values, without any support
621 from the RTS. We accomplish this by assigning a special meaning
622 to constraints of type GHC.Stack.Types.HasCallStack, an alias
623
624 type HasCallStack = (?callStack :: CallStack)
625
626 Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
627 important) are solved in three steps:
628
629 1. Occurrences of CallStack IPs are solved directly from the given IP,
630 just like a regular IP. For example, the occurrence of `?stk` in
631
632 error :: (?stk :: CallStack) => String -> a
633 error s = raise (ErrorCall (s ++ prettyCallStack ?stk))
634
635 will be solved for the `?stk` in `error`s context as before.
636
637 2. In a function call, instead of simply passing the given IP, we first
638 append the current call-site to it. For example, consider a
639 call to the callstack-aware `error` above.
640
641 undefined :: (?stk :: CallStack) => a
642 undefined = error "undefined!"
643
644 Here we want to take the given `?stk` and append the current
645 call-site, before passing it to `error`. In essence, we want to
646 rewrite `error "undefined!"` to
647
648 let ?stk = pushCallStack <error's location> ?stk
649 in error "undefined!"
650
651 We achieve this effect by emitting a NEW wanted
652
653 [W] d :: IP "stk" CallStack
654
655 from which we build the evidence term
656
657 EvCsPushCall "error" <error's location> (EvId d)
658
659 that we use to solve the call to `error`. The new wanted `d` will
660 then be solved per rule (1), ie as a regular IP.
661
662 (see TcInteract.interactDict)
663
664 3. We default any insoluble CallStacks to the empty CallStack. Suppose
665 `undefined` did not request a CallStack, ie
666
667 undefinedNoStk :: a
668 undefinedNoStk = error "undefined!"
669
670 Under the usual IP rules, the new wanted from rule (2) would be
671 insoluble as there's no given IP from which to solve it, so we
672 would get an "unbound implicit parameter" error.
673
674 We don't ever want to emit an insoluble CallStack IP, so we add a
675 defaulting pass to default any remaining wanted CallStacks to the
676 empty CallStack with the evidence term
677
678 EvCsEmpty
679
680 (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks)
681
682 This provides a lightweight mechanism for building up call-stacks
683 explicitly, but is notably limited by the fact that the stack will
684 stop at the first function whose type does not include a CallStack IP.
685 For example, using the above definition of `undefined`:
686
687 head :: [a] -> a
688 head [] = undefined
689 head (x:_) = x
690
691 g = head []
692
693 the resulting CallStack will include the call to `undefined` in `head`
694 and the call to `error` in `undefined`, but *not* the call to `head`
695 in `g`, because `head` did not explicitly request a CallStack.
696
697
698 Important Details:
699 - GHC should NEVER report an insoluble CallStack constraint.
700
701 - GHC should NEVER infer a CallStack constraint unless one was requested
702 with a partial type signature (See TcType.pickQuantifiablePreds).
703
704 - A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
705 where the String is the name of the binder that is used at the
706 SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
707 package/module/file name, as well as the full source-span. Both
708 CallStack and SrcLoc are kept abstract so only GHC can construct new
709 values.
710
711 - We will automatically solve any wanted CallStack regardless of the
712 name of the IP, i.e.
713
714 f = show (?stk :: CallStack)
715 g = show (?loc :: CallStack)
716
717 are both valid. However, we will only push new SrcLocs onto existing
718 CallStacks when the IP names match, e.g. in
719
720 head :: (?loc :: CallStack) => [a] -> a
721 head [] = error (show (?stk :: CallStack))
722
723 the printed CallStack will NOT include head's call-site. This reflects the
724 standard scoping rules of implicit-parameters.
725
726 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
727 The desugarer will need to unwrap the IP newtype before pushing a new
728 call-site onto a given stack (See DsBinds.dsEvCallStack)
729
730 - When we emit a new wanted CallStack from rule (2) we set its origin to
731 `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
732 (see TcInteract.interactDict).
733
734 This is a bit shady, but is how we ensure that the new wanted is
735 solved like a regular IP.
736
737 -}
738
739 mkEvCast :: EvExpr -> TcCoercion -> EvExpr
740 mkEvCast ev lco
741 | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
742 isTcReflCo lco = ev
743 | otherwise = evCast ev lco
744
745 mkEvScSelectors :: EvExpr -> Class -> [TcType] -> [(TcPredType, EvExpr)]
746 mkEvScSelectors ev cls tys
747 = zipWith mk_pr (immSuperClasses cls tys) [0..]
748 where
749 mk_pr pred i = (pred, Var sc_sel_id `mkTyApps` tys `App` ev)
750 where
751 sc_sel_id = classSCSelId cls i -- Zero-indexed
752
753 emptyTcEvBinds :: TcEvBinds
754 emptyTcEvBinds = EvBinds emptyBag
755
756 isEmptyTcEvBinds :: TcEvBinds -> Bool
757 isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
758 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
759
760 evTermCoercion :: EvTerm -> TcCoercion
761 -- Applied only to EvTerms of type (s~t)
762 -- See Note [Coercion evidence terms]
763 evTermCoercion (EvExpr (Var v)) = mkCoVarCo v
764 evTermCoercion (EvExpr (Coercion co)) = co
765 evTermCoercion (EvExpr (Cast tm co)) = mkCoCast (evTermCoercion (EvExpr tm)) co
766 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
767
768
769 {-
770 ************************************************************************
771 * *
772 Free variables
773 * *
774 ************************************************************************
775 -}
776
777 findNeededEvVars :: EvBindMap -> VarSet -> VarSet
778 findNeededEvVars ev_binds seeds
779 = transCloVarSet also_needs seeds
780 where
781 also_needs :: VarSet -> VarSet
782 also_needs needs = nonDetFoldUniqSet add emptyVarSet needs
783 -- It's OK to use nonDetFoldUFM here because we immediately
784 -- forget about the ordering by creating a set
785
786 add :: Var -> VarSet -> VarSet
787 add v needs
788 | Just ev_bind <- lookupEvBind ev_binds v
789 , EvBind { eb_is_given = is_given, eb_rhs = rhs } <- ev_bind
790 , is_given
791 = evVarsOfTerm rhs `unionVarSet` needs
792 | otherwise
793 = needs
794
795 evVarsOfTerm :: EvTerm -> VarSet
796 evVarsOfTerm (EvExpr e) = exprSomeFreeVars isEvVar e
797 evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
798
799 evVarsOfTerms :: [EvTerm] -> VarSet
800 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
801
802 evVarsOfTypeable :: EvTypeable -> VarSet
803 evVarsOfTypeable ev =
804 case ev of
805 EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e
806 EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
807 EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
808 EvTypeableTyLit e -> evVarsOfTerm e
809
810 -- | Do SCC analysis on a bag of 'EvBind's.
811 sccEvBinds :: Bag EvBind -> [SCC EvBind]
812 sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
813 where
814 edges :: [ Node EvVar EvBind ]
815 edges = foldrBag ((:) . mk_node) [] bs
816
817 mk_node :: EvBind -> Node EvVar EvBind
818 mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
819 = DigraphNode b var (nonDetEltsUniqSet (evVarsOfTerm term `unionVarSet`
820 coVarsOfType (varType var)))
821 -- It's OK to use nonDetEltsUniqSet here as stronglyConnCompFromEdgedVertices
822 -- is still deterministic even if the edges are in nondeterministic order
823 -- as explained in Note [Deterministic SCC] in Digraph.
824
825 {-
826 ************************************************************************
827 * *
828 Pretty printing
829 * *
830 ************************************************************************
831 -}
832
833 instance Outputable HsWrapper where
834 ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
835
836 pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
837 -- With -fprint-typechecker-elaboration, print the wrapper
838 -- otherwise just print what's inside
839 -- The pp_thing_inside function takes Bool to say whether
840 -- it's in a position that needs parens for a non-atomic thing
841 pprHsWrapper wrap pp_thing_inside
842 = sdocWithDynFlags $ \ dflags ->
843 if gopt Opt_PrintTypecheckerElaboration dflags
844 then help pp_thing_inside wrap False
845 else pp_thing_inside False
846 where
847 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
848 -- True <=> appears in function application position
849 -- False <=> appears as body of let or lambda
850 help it WpHole = it
851 help it (WpCompose f1 f2) = help (help it f2) f1
852 help it (WpFun f1 f2 t1 _) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
853 help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
854 help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
855 <+> pprParendCo co)]
856 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
857 help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <+> pprParendType ty]
858 help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pp_bndr id, it False]
859 help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pp_bndr tv, it False]
860 help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
861
862 pp_bndr v = pprBndr LambdaBind v <> dot
863
864 add_parens, no_parens :: SDoc -> Bool -> SDoc
865 add_parens d True = parens d
866 add_parens d False = d
867 no_parens d _ = d
868
869 instance Outputable TcEvBinds where
870 ppr (TcEvBinds v) = ppr v
871 ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
872
873 instance Outputable EvBindsVar where
874 ppr (EvBindsVar { ebv_uniq = u })
875 = text "EvBindsVar" <> angleBrackets (ppr u)
876
877 instance Uniquable EvBindsVar where
878 getUnique (EvBindsVar { ebv_uniq = u }) = u
879
880 instance Outputable EvBind where
881 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
882 = sep [ pp_gw <+> ppr v
883 , nest 2 $ equals <+> ppr e ]
884 where
885 pp_gw = brackets (if is_given then char 'G' else char 'W')
886 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
887
888 instance Outputable EvTerm where
889 ppr (EvExpr e) = ppr e
890 ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
891
892 instance Outputable EvCallStack where
893 ppr EvCsEmpty
894 = text "[]"
895 ppr (EvCsPushCall name loc tm)
896 = ppr (name,loc) <+> text ":" <+> ppr tm
897
898 instance Outputable EvTypeable where
899 ppr (EvTypeableTyCon ts _) = text "TyCon" <+> ppr ts
900 ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
901 ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2)
902 ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1
903
904
905 ----------------------------------------------------------------------
906 -- Helper functions for dealing with IP newtype-dictionaries
907 ----------------------------------------------------------------------
908
909 -- | Create a 'Coercion' that unwraps an implicit-parameter or
910 -- overloaded-label dictionary to expose the underlying value. We
911 -- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
912 -- and return a 'Coercion' `co :: IP sym ty ~ ty` or
913 -- `co :: IsLabel sym ty ~ Proxy# sym -> ty`. See also
914 -- Note [Type-checking overloaded labels] in TcExpr.
915 unwrapIP :: Type -> CoercionR
916 unwrapIP ty =
917 case unwrapNewTyCon_maybe tc of
918 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
919 Nothing -> pprPanic "unwrapIP" $
920 text "The dictionary for" <+> quotes (ppr tc)
921 <+> text "is not a newtype!"
922 where
923 (tc, tys) = splitTyConApp ty
924
925 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
926 -- dictionary. See 'unwrapIP'.
927 wrapIP :: Type -> CoercionR
928 wrapIP ty = mkSymCo (unwrapIP ty)