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