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