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