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