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